From 9482e7de238116daf060198bf0b96261d3503277 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Tue, 22 Dec 2020 20:25:31 +0100 Subject: [PATCH] [SMTChecker] Fix calls to virtual/overriden functions --- Changelog.md | 2 +- libsolidity/formal/BMC.cpp | 14 +++--- libsolidity/formal/BMC.h | 2 +- libsolidity/formal/CHC.cpp | 23 +++++---- libsolidity/formal/SMTEncoder.cpp | 50 +++++++++++++------ libsolidity/formal/SMTEncoder.h | 6 +-- libsolidity/formal/VariableUsage.cpp | 10 ++-- libsolidity/formal/VariableUsage.h | 7 ++- .../functions/super_function_assert.sol | 32 ++++++++++++ .../functions/virtual_function_assert.sol | 21 ++++++++ 10 files changed, 122 insertions(+), 45 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/functions/super_function_assert.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol diff --git a/Changelog.md b/Changelog.md index 85e42fac8..b942c4eb5 100644 --- a/Changelog.md +++ b/Changelog.md @@ -9,7 +9,7 @@ Compiler Features: Bugfixes: * Code Generator: Fix length check when decoding malformed error data in catch clause. - * SMTChecker: Fix false negatives in overriding modifiers. + * SMTChecker: Fix false negatives in overriding modifiers and functions. * SMTChecker: Fix false negatives when analyzing external function calls. ### 0.8.0 (2020-12-16) diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 393aa1022..c3a469f8f 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -100,9 +100,9 @@ void BMC::analyze(SourceUnit const& _source, mapisImplemented()) return false; @@ -473,8 +473,8 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall) void BMC::inlineFunctionCall(FunctionCall const& _funCall) { - solAssert(shouldInlineFunctionCall(_funCall), ""); - FunctionDefinition const* funDef = functionCallToDefinition(_funCall); + solAssert(shouldInlineFunctionCall(_funCall, m_currentContract), ""); + auto [funDef, contextContract] = functionCallToDefinition(_funCall, m_currentContract); solAssert(funDef, ""); if (visitedFunction(funDef)) @@ -488,7 +488,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall) } else { - initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall)); + initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall, m_currentContract)); // The reason why we need to pushCallStack here instead of visit(FunctionDefinition) // is that there we don't have `_funCall`. @@ -498,13 +498,13 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall) popPathCondition(); } - createReturnedExpressions(_funCall); + createReturnedExpressions(_funCall, m_currentContract); } void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall) { auto const& funType = dynamic_cast(*_funCall.expression().annotation().type); - if (shouldInlineFunctionCall(_funCall)) + if (shouldInlineFunctionCall(_funCall, m_currentContract)) inlineFunctionCall(_funCall); else if (isPublicGetter(_funCall.expression())) { diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h index 3bdd0caa9..587825337 100644 --- a/libsolidity/formal/BMC.h +++ b/libsolidity/formal/BMC.h @@ -73,7 +73,7 @@ public: std::vector unhandledQueries() { return m_interface->unhandledQueries(); } /// @returns true if _funCall should be inlined, otherwise false. - static bool shouldInlineFunctionCall(FunctionCall const& _funCall); + static bool shouldInlineFunctionCall(FunctionCall const& _funCall, ContractDefinition const* _contract); private: /// AST visitors. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 53cb9352d..f5b80b25f 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -476,7 +476,8 @@ void CHC::endVisit(FunctionCall const& _funCall) break; } - createReturnedExpressions(_funCall); + + createReturnedExpressions(_funCall, m_currentContract); } void CHC::endVisit(Break const& _break) @@ -580,18 +581,17 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall) { solAssert(m_currentContract, ""); - auto const* function = functionCallToDefinition(_funCall); + auto [function, contract] = functionCallToDefinition(_funCall, m_currentContract); if (function) { if (m_currentFunction && !m_currentFunction->isConstructor()) m_callGraph[m_currentFunction].insert(function); else m_callGraph[m_currentContract].insert(function); - auto const* contract = function->annotation().contract; // Libraries can have constants as their "state" variables, // so we need to ensure they were constructed correctly. - if (contract->isLibrary()) + if (function->annotation().contract->isLibrary()) m_context.addAssertion(interface(*contract)); } @@ -623,7 +623,8 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) auto kind = funType.kind(); solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); - auto const* function = functionCallToDefinition(_funCall); + solAssert(m_currentContract, ""); + auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract); if (!function) return; @@ -667,7 +668,8 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall) auto kind = funType.kind(); solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); - auto const* function = functionCallToDefinition(_funCall); + solAssert(m_currentContract, ""); + auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract); if (!function) return; @@ -1153,7 +1155,8 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) auto kind = funType.kind(); solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); - auto const* function = functionCallToDefinition(_funCall); + solAssert(m_currentContract, ""); + auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract); if (!function) return smtutil::Expression(true); @@ -1170,19 +1173,19 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) auto const* contract = function->annotation().contract; auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; - solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contract), ""); + solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contextContract), ""); /// If the call is to a library, we use that library as the called contract. /// If the call is to a contract not in the inheritance hierarchy, we also use that as the called contract. /// Otherwise, the call is to some contract in the inheritance hierarchy of the current contract. /// In this case we use current contract as the called one since the interfaces/predicates are different. - auto const* calledContract = contains(hierarchy, contract) ? m_currentContract : contract; + auto const* calledContract = contains(hierarchy, contract) ? contextContract : contract; solAssert(calledContract, ""); bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View; args += currentStateVariables(*calledContract); - args += symbolicArguments(_funCall); + args += symbolicArguments(_funCall, m_currentContract); if (!calledContract->isLibrary() && !usesStaticCall) { state().newState(); diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 7226b0080..b809bd81c 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -744,6 +744,7 @@ void SMTEncoder::initContract(ContractDefinition const& _contract) m_context.pushSolver(); createStateVariables(_contract); clearIndices(m_currentContract, nullptr); + m_variableUsage.setCurrentContract(_contract); } void SMTEncoder::initFunction(FunctionDefinition const& _function) @@ -2598,26 +2599,43 @@ string SMTEncoder::extraComment() return extra; } -FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall const& _funCall) +pair SMTEncoder::functionCallToDefinition(FunctionCall const& _funCall, ContractDefinition const* _contract) { if (*_funCall.annotation().kind != FunctionCallKind::FunctionCall) - return nullptr; + return {}; - FunctionDefinition const* funDef = nullptr; Expression const* calledExpr = &_funCall.expression(); - if (TupleExpression const* fun = dynamic_cast(calledExpr)) { solAssert(fun->components().size() == 1, ""); calledExpr = innermostTuple(*calledExpr); } - if (Identifier const* fun = dynamic_cast(calledExpr)) - funDef = dynamic_cast(fun->annotation().referencedDeclaration); - else if (MemberAccess const* fun = dynamic_cast(calledExpr)) - funDef = dynamic_cast(fun->annotation().referencedDeclaration); + auto resolveVirtual = [&](auto const* _ref) -> pair { + VirtualLookup lookup = *_ref->annotation().requiredLookup; + solAssert(_contract || lookup == VirtualLookup::Static, "No contract context provided for function lookup resolution!"); + auto funDef = dynamic_cast(_ref->annotation().referencedDeclaration); + if (!funDef) + return {funDef, _contract}; + auto contextContract = _contract; + if (lookup == VirtualLookup::Virtual) + funDef = &funDef->resolveVirtual(*_contract); + else if (lookup == VirtualLookup::Super) + { + auto super = _contract->superContract(*_contract); + solAssert(super, "Super contract not available."); + funDef = &funDef->resolveVirtual(*_contract, super); + contextContract = super; + } + return {funDef, contextContract}; + }; - return funDef; + if (Identifier const* fun = dynamic_cast(calledExpr)) + return resolveVirtual(fun); + else if (MemberAccess const* fun = dynamic_cast(calledExpr)) + return resolveVirtual(fun); + + return {}; } vector SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract) @@ -2798,9 +2816,9 @@ set SMTEncoder::collectABICalls(ASTNode const* _node) return ABIFunctions(_node).abiCalls; } -void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) +void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contract) { - FunctionDefinition const* funDef = functionCallToDefinition(_funCall); + auto [funDef, contextContract] = functionCallToDefinition(_funCall, _contract); if (!funDef) return; @@ -2826,18 +2844,18 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall) defineExpr(_funCall, currentValue(*returnParams.front())); } -vector SMTEncoder::symbolicArguments(FunctionCall const& _funCall) +vector SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contract) { - auto const* function = functionCallToDefinition(_funCall); - solAssert(function, ""); + auto [funDef, contextContract] = functionCallToDefinition(_funCall, _contract); + solAssert(funDef, ""); vector args; Expression const* calledExpr = &_funCall.expression(); - auto const& funType = dynamic_cast(calledExpr->annotation().type); + auto funType = dynamic_cast(calledExpr->annotation().type); solAssert(funType, ""); vector> arguments = _funCall.sortedArguments(); - auto const& functionParams = function->parameters(); + auto functionParams = funDef->parameters(); unsigned firstParam = 0; if (funType->bound()) { diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 8ad433609..3f0ee21d0 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -69,7 +69,7 @@ public: /// @returns the FunctionDefinition of a FunctionCall /// if possible or nullptr. - static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall); + static std::pair functionCallToDefinition(FunctionCall const& _funCall, ContractDefinition const* _contract = nullptr); static std::vector stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract); static std::vector stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function); @@ -331,12 +331,12 @@ protected: /// Creates symbolic expressions for the returned values /// and set them as the components of the symbolic tuple. - void createReturnedExpressions(FunctionCall const& _funCall); + void createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contract); /// @returns the symbolic arguments for a function call, /// taking into account bound functions and /// type conversion. - std::vector symbolicArguments(FunctionCall const& _funCall); + std::vector symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contract); /// @returns a note to be added to warnings. std::string extraComment(); diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp index 9b1c336d7..8245bbedb 100644 --- a/libsolidity/formal/VariableUsage.cpp +++ b/libsolidity/formal/VariableUsage.cpp @@ -60,13 +60,13 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess) void VariableUsage::endVisit(FunctionCall const& _funCall) { - if (m_inlineFunctionCalls(_funCall)) - if (auto funDef = SMTEncoder::functionCallToDefinition(_funCall)) - { - solAssert(funDef, ""); + if (m_inlineFunctionCalls(_funCall, m_currentContract)) + if ( + auto [funDef, contextContract] = SMTEncoder::functionCallToDefinition(_funCall, m_currentContract); + funDef + ) if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end()) funDef->accept(*this); - } } bool VariableUsage::visit(FunctionDefinition const& _function) diff --git a/libsolidity/formal/VariableUsage.h b/libsolidity/formal/VariableUsage.h index 3f69ca5a2..2f09846a6 100644 --- a/libsolidity/formal/VariableUsage.h +++ b/libsolidity/formal/VariableUsage.h @@ -36,7 +36,9 @@ public: std::set touchedVariables(ASTNode const& _node, std::vector const& _outerCallstack); /// Sets whether to inline function calls. - void setFunctionInlining(std::function _inlineFunctionCalls) { m_inlineFunctionCalls = _inlineFunctionCalls; } + void setFunctionInlining(std::function _inlineFunctionCalls) { m_inlineFunctionCalls = _inlineFunctionCalls; } + + void setCurrentContract(ContractDefinition const& _contract) { m_currentContract = &_contract; } private: void endVisit(Identifier const& _node) override; @@ -53,8 +55,9 @@ private: std::set m_touchedVariables; std::vector m_callStack; CallableDeclaration const* m_lastCall = nullptr; + ContractDefinition const* m_currentContract = nullptr; - std::function m_inlineFunctionCalls = [](FunctionCall const&) { return false; }; + std::function m_inlineFunctionCalls = [](FunctionCall const&, ContractDefinition const*) { return false; }; }; } diff --git a/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol b/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol new file mode 100644 index 000000000..0b1cdec03 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/super_function_assert.sol @@ -0,0 +1,32 @@ +pragma experimental SMTChecker; +contract A { + int x = 0; + + function f() virtual internal { + x = 2; + } + + function proxy() public { + f(); + } +} + +contract C is A { + function f() internal virtual override { + super.f(); + assert(x == 2); + assert(x == 3); // should fail + } +} + +contract D is C { + + function f() internal override { + super.f(); + assert(x == 2); + assert(x == 3); // should fail + } +} +// ---- +// Warning 6328: (237-251): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nproxy() +// Warning 6328: (360-374): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nproxy() diff --git a/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol b/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol new file mode 100644 index 000000000..0540b759f --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/virtual_function_assert.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; +contract A { + int x = 0; + + function f() virtual internal view { + assert(x == 0); + } + + function proxy() public view { + f(); + } +} + +contract C is A { + + function f() internal view override { + assert(x == 1); + } +} +// ---- +// Warning 6328: (259-273): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\nproxy()