cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #10678 from blishko/refactor

Browse Source 
[SMTChecker] Small refactoring to define a single way of gathering functions belonging to a given contract.
This commit is contained in:
Leonardo 2020-12-22 13:50:26 +01:00 committed by GitHub
commit 6bcae84610
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 68 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
libsolidity/formal/CHC.cpp
View File

@ -891,41 +891,35 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto const& iface = *m_nondetInterfaces.at(contract);
addRule(smt::nondetInterface(iface, *contract, m_context, 0, 0), "base_nondet");
for (auto const* base: contract->annotation().linearizedBaseContracts)
for (auto const* function: base->definedFunctions())
for (auto const* function: contractFunctions(*contract))
{
for (auto var: function->parameters())
createVariable(*var);
for (auto var: function->returnParameters())
createVariable(*var);
for (auto const* var: localVariablesIncludingModifiers(*function, contract))
createVariable(*var);
m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
if (!function->isConstructor() && function->isPublic())
{
for (auto var: function->parameters())
createVariable(*var);
for (auto var: function->returnParameters())
createVariable(*var);
for (auto const* var: localVariablesIncludingModifiers(*function, contract))
createVariable(*var);
auto state1 = stateVariablesAtIndex(1, *contract);
auto state2 = stateVariablesAtIndex(2, *contract);
m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
if (
!function->isConstructor() &&
function->isPublic() &&
!base->isLibrary() &&
!base->isInterface()
)
{
auto state1 = stateVariablesAtIndex(1, *contract);
auto state2 = stateVariablesAtIndex(2, *contract);
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
args += state1 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
vector<smtutil::Expression>{state().state(2)} +
state2 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
args += state1 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
vector<smtutil::Expression>{state().state(2)} +
state2 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 1); }) +
applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
connectBlocks(nondetPre, nondetPost, (*m_summaries.at(contract).at(function))(args));
}
connectBlocks(nondetPre, nondetPost, (*m_summaries.at(contract).at(function))(args));
}
}
}
}

59
libsolidity/formal/SMTEncoder.cpp
View File

@ -90,7 +90,6 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
)
node->accept(*this);
vector<FunctionDefinition const*> resolvedFunctions = _contract.definedFunctions();
for (auto const& base: _contract.annotation().linearizedBaseContracts)
{
// Look for all the constructor invocations bottom up.
@ -104,35 +103,13 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
m_baseConstructorCalls[baseContract] = invocation.get();
}
}
// Check for function overrides.
for (auto const& baseFunction: base->definedFunctions())
{
if (baseFunction->isConstructor())
continue;
bool overridden = false;
for (auto const& function: resolvedFunctions)
if (
function->name() == baseFunction->name() &&
function->kind() == baseFunction->kind() &&
FunctionType(*function).asExternallyCallableFunction(false)->
hasEqualParameterTypes(*FunctionType(*baseFunction).asExternallyCallableFunction(false))
)
{
overridden = true;
break;
}
if (!overridden)
resolvedFunctions.push_back(baseFunction);
}
}
// Functions are visited first since they might be used
// for state variable initialization which is part of
// the constructor.
// Constructors are visited as part of the constructor
// hierarchy inlining.
for (auto const& function: resolvedFunctions)
for (auto const* function: contractFunctions(_contract))
if (!function->isConstructor())
function->accept(*this);
@ -2705,6 +2682,40 @@ ModifierDefinition const* SMTEncoder::resolveModifierInvocation(ModifierInvocati
return modifier;
}
vector<FunctionDefinition const*> const& SMTEncoder::contractFunctions(ContractDefinition const& _contract)
{
if (!m_contractFunctions.count(&_contract))
{
vector<FunctionDefinition const *> resolvedFunctions = _contract.definedFunctions();
for (auto const* base: _contract.annotation().linearizedBaseContracts)
{
if (base == &_contract)
continue;
for (auto const* baseFunction: base->definedFunctions())
{
if (baseFunction->isConstructor()) // We don't want to include constructors of parent contracts
continue;
bool overridden = false;
for (auto const* function: resolvedFunctions)
if (
function->name() == baseFunction->name() &&
function->kind() == baseFunction->kind() &&
FunctionType(*function).asExternallyCallableFunction(false)->
hasEqualParameterTypes(*FunctionType(*baseFunction).asExternallyCallableFunction(false))
)
{
overridden = true;
break;
}
if (!overridden)
resolvedFunctions.push_back(baseFunction);
}
}
m_contractFunctions.emplace(&_contract, move(resolvedFunctions));
}
return m_contractFunctions.at(&_contract);
}
SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
{
for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))

6
libsolidity/formal/SMTEncoder.h
View File

@ -372,6 +372,12 @@ protected:
/// Returns true if _funDef was already visited.
bool visitedFunction(FunctionDefinition const* _funDef);
/// @returns FunctionDefinitions of the given contract (including its constructor and inherited methods),
/// taking into account overriding of the virtual functions.
std::vector<FunctionDefinition const*> const& contractFunctions(ContractDefinition const& _contract);
/// Cache for the method contractFunctions.
std::map<ContractDefinition const*, std::vector<FunctionDefinition const*>> m_contractFunctions;
/// Depth of visit to modifiers.
/// When m_modifierDepth == #modifiers the function can be visited
/// when placeholder is visited.

2
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol
View File

@ -26,6 +26,6 @@ contract C is B {
}
// ----
// Warning 5740: (152-157): Unreachable code.
// Warning 6328: (310-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 0\n\n\nTransaction trace:\nconstructor(0)
// Warning 6328: (310-324): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 1\n\n\nTransaction trace:\nconstructor(1)
// Warning 6328: (343-357): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 1\n\n\nTransaction trace:\nconstructor(1)
// Warning 6328: (376-390): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\na = 0\n\n\nTransaction trace:\nconstructor(0)

2
test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol
View File

@ -32,5 +32,5 @@ contract C is Z(5) {
}
}
// ----
// Warning 4984: (325-332): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4984: (325-332): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\nx = 1\nz = 115792089237316195423570985008687907853269984665640564039457584007913129639935\n\n\nTransaction trace:\nconstructor(115792089237316195423570985008687907853269984665640564039457584007913129639935)
// Warning 6328: (400-413): CHC: Assertion violation happens here.\nCounterexample:\nx = 6\n\n\n\nTransaction trace:\nconstructor()