diff --git a/Changelog.md b/Changelog.md index 6f97f3841..2acf382ee 100644 --- a/Changelog.md +++ b/Changelog.md @@ -27,6 +27,7 @@ Bugfixes: * SMTChecker: Fix pointer knowledge erasing in loops. * SMTChecker: Fix internal error when using compound bitwise assignment operators inside branches. * SMTChecker: Fix internal error when inlining a function that returns a tuple containing an unsupported type inside a branch. + * SMTChecker: Fix internal error when inlining functions that use state variables and belong to a different source. * View/Pure Checker: Properly detect state variable access through base class. * Yul analyzer: Check availability of data objects already in analysis phase. * Yul Optimizer: Fix an issue where memory-accessing code was removed even though ``msize`` was used in the program. diff --git a/libsolidity/ast/AST.cpp b/libsolidity/ast/AST.cpp index a6f7d3d2d..75166d654 100644 --- a/libsolidity/ast/AST.cpp +++ b/libsolidity/ast/AST.cpp @@ -109,6 +109,16 @@ TypePointer ImportDirective::type() const return TypeProvider::module(*annotation().sourceUnit); } +vector ContractDefinition::stateVariablesIncludingInherited() const +{ + vector stateVars; + for (auto const& contract: annotation().linearizedBaseContracts) + for (auto var: contract->stateVariables()) + if (*contract == *this || var->isVisibleInDerivedContracts()) + stateVars.push_back(var); + return stateVars; +} + map, FunctionTypePointer> ContractDefinition::interfaceFunctions() const { auto exportedFunctionList = interfaceFunctionList(); diff --git a/libsolidity/ast/AST.h b/libsolidity/ast/AST.h index 1cd41ac10..b84ad2c19 100644 --- a/libsolidity/ast/AST.h +++ b/libsolidity/ast/AST.h @@ -396,6 +396,7 @@ public: std::vector definedStructs() const { return filteredNodes(m_subNodes); } std::vector definedEnums() const { return filteredNodes(m_subNodes); } std::vector stateVariables() const { return filteredNodes(m_subNodes); } + std::vector stateVariablesIncludingInherited() const; std::vector functionModifiers() const { return filteredNodes(m_subNodes); } std::vector definedFunctions() const { return filteredNodes(m_subNodes); } std::vector events() const { return filteredNodes(m_subNodes); } diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 931be1022..8b83e62fe 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -120,8 +120,20 @@ bool BMC::visit(ContractDefinition const& _contract) return true; } +void BMC::endVisit(ContractDefinition const& _contract) +{ + SMTEncoder::endVisit(_contract); +} + bool BMC::visit(FunctionDefinition const& _function) { + auto contract = dynamic_cast(_function.scope()); + solAssert(contract, ""); + solAssert(m_currentContract, ""); + auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; + if (find(hierarchy.begin(), hierarchy.end(), contract) == hierarchy.end()) + initializeStateVariables(*contract); + if (m_callStack.empty()) reset(); diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index c5bd5ba57..937733574 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -74,6 +74,7 @@ private: /// or checked are visited. //@{ bool visit(ContractDefinition const& _node) override; + void endVisit(ContractDefinition const& _node) override; bool visit(FunctionDefinition const& _node) override; void endVisit(FunctionDefinition const& _node) override; bool visit(IfStatement const& _node) override; diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 1f190b19e..ea78e640d 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -36,16 +36,19 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context): bool SMTEncoder::visit(ContractDefinition const& _contract) { - for (auto const& contract: _contract.annotation().linearizedBaseContracts) - for (auto var: contract->stateVariables()) - if (*contract == _contract || var->isVisibleInDerivedContracts()) - createVariable(*var); + solAssert(m_currentContract == nullptr, ""); + m_currentContract = &_contract; + + initializeStateVariables(_contract); return true; } -void SMTEncoder::endVisit(ContractDefinition const&) +void SMTEncoder::endVisit(ContractDefinition const& _contract) { m_context.resetAllVariables(); + + solAssert(m_currentContract == &_contract, ""); + m_currentContract = nullptr; } void SMTEncoder::endVisit(VariableDeclaration const& _varDecl) @@ -1158,6 +1161,12 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu } } +void SMTEncoder::initializeStateVariables(ContractDefinition const& _contract) +{ + for (auto var: _contract.stateVariablesIncludingInherited()) + createVariable(*var); +} + void SMTEncoder::initializeLocalVariables(FunctionDefinition const& _function) { for (auto const& variable: _function.localVariables()) diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 7d0527804..46fdac831 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -156,6 +156,7 @@ protected: using CallStackEntry = std::pair; + void initializeStateVariables(ContractDefinition const& _contract); void initializeLocalVariables(FunctionDefinition const& _function); void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector const& _callArgs); void resetStateVariables(); @@ -246,6 +247,8 @@ protected: /// Needs to be a stack because of function calls. std::vector m_modifierDepthStack; + ContractDefinition const* m_currentContract = nullptr; + /// Stores the context of the encoding. smt::EncodingContext& m_context; }; diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp index 4cb7b6667..99ae85aaf 100644 --- a/test/libsolidity/SMTChecker.cpp +++ b/test/libsolidity/SMTChecker.cpp @@ -19,6 +19,7 @@ */ #include +#include #include @@ -248,6 +249,85 @@ BOOST_AUTO_TEST_CASE(mod) CHECK_SUCCESS_NO_WARNINGS(text); } +BOOST_AUTO_TEST_CASE(import_base) +{ + CompilerStack c; + c.setSources({ + {"base", R"( + pragma solidity >=0.0; + contract Base { + uint x; + function f() internal { + ++x; + } + } + )"}, + {"der", R"( + pragma solidity >=0.0; + pragma experimental SMTChecker; + import "base"; + contract Der is Base { + function g(uint y) public { + f(); + assert(y > x); + } + } + )"} + }); + c.setEVMVersion(dev::test::Options::get().evmVersion()); + BOOST_CHECK(c.compile()); + + unsigned asserts = 0; + for (auto const& e: c.errors()) + { + string const* msg = e->comment(); + BOOST_REQUIRE(msg); + if (msg->find("Assertion violation") != string::npos) + ++asserts; + } + BOOST_CHECK_EQUAL(asserts, 1); +} + +BOOST_AUTO_TEST_CASE(import_library) +{ + CompilerStack c; + c.setSources({ + {"lib", R"( + pragma solidity >=0.0; + library L { + uint constant one = 1; + function f() internal pure returns (uint) { + return one; + } + } + )"}, + {"c", R"( + pragma solidity >=0.0; + pragma experimental SMTChecker; + import "lib"; + contract C { + function g(uint x) public pure { + uint y = L.f(); + assert(x > y); + } + } + )"} + }); + c.setEVMVersion(dev::test::Options::get().evmVersion()); + BOOST_CHECK(c.compile()); + + unsigned asserts = 0; + for (auto const& e: c.errors()) + { + string const* msg = e->comment(); + BOOST_REQUIRE(msg); + if (msg->find("Assertion violation") != string::npos) + ++asserts; + } + BOOST_CHECK_EQUAL(asserts, 1); + +} + BOOST_AUTO_TEST_SUITE_END() }