diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 17a481467..7b5147a4c 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -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 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{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 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{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)); + } } } } diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index b288bee6a..7226b0080 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -90,7 +90,6 @@ bool SMTEncoder::visit(ContractDefinition const& _contract) ) node->accept(*this); - vector 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 const& SMTEncoder::contractFunctions(ContractDefinition const& _contract) +{ + if (!m_contractFunctions.count(&_contract)) + { + vector 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(s->scope())) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 7a1966d0c..8ad433609 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -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 const& contractFunctions(ContractDefinition const& _contract); + /// Cache for the method contractFunctions. + std::map> m_contractFunctions; + /// Depth of visit to modifiers. /// When m_modifierDepth == #modifiers the function can be visited /// when placeholder is visited. diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol index 05595cbde..2a014ecc7 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol @@ -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) diff --git a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol index 593ee6c4e..274129c73 100644 --- a/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol +++ b/test/libsolidity/smtCheckerTests/inheritance/constructor_hierarchy_base_calls_inheritance_specifier_1.sol @@ -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()