diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index c989df8c0..328804d3e 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -936,9 +936,9 @@ SortPointer CHC::sort(ASTNode const* _node) return functionBodySort(*m_currentFunction, m_currentContract, state()); } -Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node) +Predicate const* CHC::createSymbolicBlock(SortPointer _sort, string const& _name, PredicateType _predType, ASTNode const* _node, ContractDefinition const* _contractContext) { - auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node); + auto const* block = Predicate::create(_sort, _name, _predType, m_context, _node, _contractContext); m_interface->registerRelation(block->functor()); return block; } @@ -1081,7 +1081,8 @@ Predicate const* CHC::createBlock(ASTNode const* _node, PredicateType _predType, sort(_node), "block_" + uniquePrefix() + "_" + _prefix + predicateName(_node), _predType, - _node + _node, + m_currentContract ); solAssert(m_currentFunction, ""); @@ -1094,7 +1095,8 @@ Predicate const* CHC::createSummaryBlock(FunctionDefinition const& _function, Co functionSort(_function, &_contract, state()), "summary_" + uniquePrefix() + "_" + predicateName(&_function, &_contract), _type, - &_function + &_function, + &_contract ); } @@ -1104,6 +1106,7 @@ Predicate const* CHC::createConstructorBlock(ContractDefinition const& _contract constructorSort(_contract, state()), _prefix + "_" + contractSuffix(_contract) + "_" + uniquePrefix(), PredicateType::ConstructorSummary, + &_contract, &_contract ); } diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 8a9772839..f08bf0ac6 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -126,7 +126,7 @@ private: /// Predicate helpers. //@{ /// @returns a new block of given _sort and _name. - Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, PredicateType _predType, ASTNode const* _node = nullptr); + Predicate const* createSymbolicBlock(smtutil::SortPointer _sort, std::string const& _name, PredicateType _predType, ASTNode const* _node = nullptr, ContractDefinition const* _contractContext = nullptr); /// Creates summary predicates for all functions of all contracts /// in a given _source. diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp index 3a31937e0..13c13f3e8 100644 --- a/libsolidity/formal/Predicate.cpp +++ b/libsolidity/formal/Predicate.cpp @@ -40,7 +40,8 @@ Predicate const* Predicate::create( string _name, PredicateType _type, EncodingContext& _context, - ASTNode const* _node + ASTNode const* _node, + ContractDefinition const* _contractContext ) { smt::SymbolicFunctionVariable predicate{_sort, move(_name), _context}; @@ -49,18 +50,20 @@ Predicate const* Predicate::create( return &m_predicates.emplace( std::piecewise_construct, std::forward_as_tuple(functorName), - std::forward_as_tuple(move(predicate), _type, _node) + std::forward_as_tuple(move(predicate), _type, _node, _contractContext) ).first->second; } Predicate::Predicate( smt::SymbolicFunctionVariable&& _predicate, PredicateType _type, - ASTNode const* _node + ASTNode const* _node, + ContractDefinition const* _contractContext ): m_predicate(move(_predicate)), m_type(_type), - m_node(_node) + m_node(_node), + m_contractContext(_contractContext) { } @@ -130,18 +133,8 @@ FunctionCall const* Predicate::programFunctionCall() const optional> Predicate::stateVariables() const { - if (auto const* fun = programFunction()) - return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun); - if (auto const* contract = programContract()) - return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*contract); - - auto const* node = m_node; - while (auto const* scopable = dynamic_cast(node)) - { - node = scopable->scope(); - if (auto const* fun = dynamic_cast(node)) - return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*fun); - } + if (m_contractContext) + return SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*m_contractContext); return nullopt; } diff --git a/libsolidity/formal/Predicate.h b/libsolidity/formal/Predicate.h index 5fe69a355..30c4fb288 100644 --- a/libsolidity/formal/Predicate.h +++ b/libsolidity/formal/Predicate.h @@ -55,13 +55,15 @@ public: std::string _name, PredicateType _type, smt::EncodingContext& _context, - ASTNode const* _node = nullptr + ASTNode const* _node = nullptr, + ContractDefinition const* _contractContext = nullptr ); Predicate( smt::SymbolicFunctionVariable&& _predicate, PredicateType _type, - ASTNode const* _node = nullptr + ASTNode const* _node = nullptr, + ContractDefinition const* _contractContext = nullptr ); /// Predicate should not be copiable. @@ -166,6 +168,12 @@ private: /// nullptr if this predicate is not associated with a specific program AST node. ASTNode const* m_node = nullptr; + /// The ContractDefinition that contains this predicate. + /// nullptr if this predicate is not associated with a specific contract. + /// This is unfortunately necessary because of virtual resolution for + /// function nodes. + ContractDefinition const* m_contractContext = nullptr; + /// Maps the name of the predicate to the actual Predicate. /// Used in counterexample generation. static std::map m_predicates; diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol new file mode 100644 index 000000000..23452fdf2 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_1.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract B { + uint x; + function f() public view { + assert(x == 0); + } +} + +contract C is B { + uint y; + function g() public { + x = 1; + f(); + } +} +// ---- +// Warning 6328: (85-99): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, x = 0\nC.g()\n B.f() -- internal call\nState: y = 0, x = 1\nB.f() diff --git a/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_2.sol b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_2.sol new file mode 100644 index 000000000..3d509cc70 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_2.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; + +contract A { + uint x; + function f() internal view { + assert(x == 0); + } +} + +contract B is A { + uint a; + uint b; +} + +contract C is B { + uint y; + uint z; + uint w; + function g() public { + x = 1; + f(); + } +} +// ---- +// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\ny = 0, z = 0, w = 0, a = 0, b = 0, x = 1\n\nTransaction trace:\nC.constructor()\nState: y = 0, z = 0, w = 0, a = 0, b = 0, x = 0\nC.g()\n A.f() -- internal call