From 5ca7a24896dd6176a0717b7ac574dce8bb0f8348 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Mon, 9 Nov 2020 14:50:41 +0100 Subject: [PATCH] [SMTChecker] Added support for precise modeling of external calls to `this`. Modeling external calls to this, since we can trust these calls. fixed problem with transaction data not being restored after trusted external call update to the tests additional tests changelog entry added tests for external getters of this --- Changelog.md | 1 + libsolidity/formal/BMC.cpp | 15 +--- libsolidity/formal/CHC.cpp | 72 +++++++++++++++---- libsolidity/formal/CHC.h | 1 + libsolidity/formal/SMTEncoder.cpp | 13 ++++ libsolidity/formal/SMTEncoder.h | 4 ++ .../functions/this_external_call.sol | 2 - .../functions/this_external_call_2.sol | 16 +++++ .../functions/this_external_call_return.sol | 2 - .../functions/this_external_call_sender.sol | 28 ++++++++ .../this_external_call_tx_origin.sol | 14 ++++ .../functions/this_external_getter_1.sol | 12 ++++ .../functions/this_external_getter_2.sol | 12 ++++ .../functions/this_external_getter_3.sol | 12 ++++ .../smtCheckerTests/functions/this_state.sol | 2 - 15 files changed, 172 insertions(+), 34 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/this_external_call_sender.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/this_external_call_tx_origin.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol create mode 100644 test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol diff --git a/Changelog.md b/Changelog.md index a8af33eb4..b44121578 100644 --- a/Changelog.md +++ b/Changelog.md @@ -9,6 +9,7 @@ Compiler Features: * Command Line interface: Report proper error for each output file which could not be written. Previously an exception was thrown, and execution aborted, on the first error. * SMTChecker: Add division by zero checks in the CHC engine. * SMTChecker: Support ``selector`` for expressions with value known at compile-time. + * SMTChecker: More precise analysis of external calls using ``this``. * Command Line Interface: New option ``--model-checker-timeout`` sets a timeout in milliseconds for each individual query performed by the SMTChecker. * Standard JSON: New option ``modelCheckerSettings.timeout`` sets a timeout in milliseconds for each individual query performed by the SMTChecker. * Assembler: Perform linking in assembly mode when library addresses are provided. diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 6013f1cd1..b6e05bdd0 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -96,20 +96,7 @@ bool BMC::shouldInlineFunctionCall(FunctionCall const& _funCall) FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); if (funType.kind() == FunctionType::Kind::External) - { - auto memberAccess = dynamic_cast(&_funCall.expression()); - if (!memberAccess) - return false; - - auto identifier = dynamic_cast(&memberAccess->expression()); - if (!( - identifier && - identifier->name() == "this" && - identifier->annotation().referencedDeclaration && - dynamic_cast(identifier->annotation().referencedDeclaration) - )) - return false; - } + return isTrustedExternalCall(&_funCall.expression()); else if (funType.kind() != FunctionType::Kind::Internal) return false; diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 6fc432d06..be3413770 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -562,8 +562,6 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall) m_context.addAssertion(interface(*contract)); } - auto previousError = errorFlag().currentValue(); - m_context.addAssertion(predicate(_funCall)); connectBlocks( @@ -572,8 +570,6 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall) (errorFlag().currentValue() > 0) ); m_context.addAssertion(errorFlag().currentValue() == 0); - errorFlag().increaseIndex(); - m_context.addAssertion(errorFlag().currentValue() == previousError); } void CHC::externalFunctionCall(FunctionCall const& _funCall) @@ -583,6 +579,11 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) /// so we just add the nondet_interface predicate. solAssert(m_currentContract, ""); + if (isTrustedExternalCall(&_funCall.expression())) + { + externalFunctionCallToTrustedCode(_funCall); + return; + } FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); auto kind = funType.kind(); @@ -615,6 +616,42 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) m_context.addAssertion(errorFlag().currentValue() == 0); } +void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall) +{ + solAssert(m_currentContract, ""); + FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); + auto kind = funType.kind(); + solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); + + auto const* function = functionCallToDefinition(_funCall); + if (!function) + return; + + // External call creates a new transaction. + auto originalTx = state().tx(); + auto txOrigin = state().txMember("tx.origin"); + state().newTx(); + // set the transaction sender as this contract + m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress()); + // set the origin to be the current transaction origin + m_context.addAssertion(state().txMember("tx.origin") == txOrigin); + + smtutil::Expression pred = predicate(_funCall); + + auto txConstraints = m_context.state().txConstraints(*function); + m_context.addAssertion(pred && txConstraints); + // restore the original transaction data + state().newTx(); + m_context.addAssertion(originalTx == state().tx()); + + connectBlocks( + m_currentBlock, + (m_currentFunction && !m_currentFunction->isConstructor()) ? summary(*m_currentFunction) : summary(*m_currentContract), + (errorFlag().currentValue() > 0) + ); + m_context.addAssertion(errorFlag().currentValue() == 0); +} + void CHC::unknownFunctionCall(FunctionCall const&) { /// Function calls are not handled at the moment, @@ -1011,27 +1048,34 @@ smtutil::Expression CHC::predicate(Predicate const& _block) smtutil::Expression CHC::predicate(FunctionCall const& _funCall) { - /// Used only for internal calls. + FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); + auto kind = funType.kind(); + solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); auto const* function = functionCallToDefinition(_funCall); if (!function) return smtutil::Expression(true); + auto contractAddressValue = [this](FunctionCall const& _f) { + FunctionType const& funType = dynamic_cast(*_f.expression().annotation().type); + if (funType.kind() == FunctionType::Kind::Internal) + return state().thisAddress(); + if (MemberAccess const* callBase = dynamic_cast(&_f.expression())) + return expr(callBase->expression()); + solAssert(false, "Unreachable!"); + }; errorFlag().increaseIndex(); - vector args{errorFlag().currentValue(), state().thisAddress(), state().crypto(), state().tx(), state().state()}; + vector args{errorFlag().currentValue(), contractAddressValue(_funCall), state().crypto(), state().tx(), state().state()}; - FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); - solAssert(funType.kind() == FunctionType::Kind::Internal, ""); - - /// Internal calls can be made to the contract itself or a library. auto const* contract = function->annotation().contract; auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts; - solAssert(contract->isLibrary() || find(hierarchy.begin(), hierarchy.end(), contract) != hierarchy.end(), ""); + solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contract), ""); /// If the call is to a library, we use that library as the called contract. - /// If it is not, we use the current contract even if it is a call to a contract - /// up in the inheritance hierarchy, since the interfaces/predicates are different. - auto const* calledContract = contract->isLibrary() ? contract : m_currentContract; + /// 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; solAssert(calledContract, ""); bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View; diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h index 8a169e86d..9f712ba39 100644 --- a/libsolidity/formal/CHC.h +++ b/libsolidity/formal/CHC.h @@ -88,6 +88,7 @@ private: void visitAddMulMod(FunctionCall const& _funCall) override; void internalFunctionCall(FunctionCall const& _funCall); void externalFunctionCall(FunctionCall const& _funCall); + void externalFunctionCallToTrustedCode(FunctionCall const& _funCall); void unknownFunctionCall(FunctionCall const& _funCall); void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override; /// Creates underflow/overflow verification targets. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 7ee339b1e..d58abc2ee 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -2391,6 +2391,19 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const return nullptr; } +bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) { + auto memberAccess = dynamic_cast(_expr); + if (!memberAccess) + return false; + + auto identifier = dynamic_cast(&memberAccess->expression()); + return identifier && + identifier->name() == "this" && + identifier->annotation().referencedDeclaration && + dynamic_cast(identifier->annotation().referencedDeclaration) + ; +} + string SMTEncoder::extraComment() { string extra; diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 49cac0082..d56eeca18 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -295,6 +295,10 @@ protected: /// otherwise nullptr. MemberAccess const* isEmptyPush(Expression const& _expr) const; + /// @returns true if the given identifier is a contract which is known and trusted. + /// This means we don't have to abstract away effects of external function calls to this contract. + static bool isTrustedExternalCall(Expression const* _expr); + /// Creates symbolic expressions for the returned values /// and set them as the components of the symbolic tuple. void createReturnedExpressions(FunctionCall const& _funCall); diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call.sol index 489d7f44e..de69baf53 100644 --- a/test/libsolidity/smtCheckerTests/functions/this_external_call.sol +++ b/test/libsolidity/smtCheckerTests/functions/this_external_call.sol @@ -9,9 +9,7 @@ contract C function g(uint y) public { require(y < 1000); this.f(y); - // Fails as false positive because CHC does not support `this`. assert(x < 1000); } } // ---- -// Warning 6328: (227-243): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol new file mode 100644 index 000000000..7fca557ad --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + uint a; + function f(uint x) public { + this.g(x); + assert(a == x); + assert(a != 42); + } + + function g(uint x) public { + a = x; + } +} +// ---- +// Warning 6328: (141-156): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol index 0307490dc..cb94af867 100644 --- a/test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol +++ b/test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol @@ -10,9 +10,7 @@ contract C function g(uint y) public { require(y < 1000); uint z = this.f(y); - // Fails as false positive because CHC does not support `this`. assert(z < 1000); } } // ---- -// Warning 6328: (263-279): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call_sender.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call_sender.sol new file mode 100644 index 000000000..78f4169cc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/this_external_call_sender.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; + +contract C { + address lastCaller; + + constructor() { + lastCaller = msg.sender; + } + + modifier log { + lastCaller = msg.sender; + _; + } + + function test() log public { + assert(lastCaller == msg.sender); + this.g(); + assert(lastCaller == address(this)); + assert(lastCaller == msg.sender); + assert(lastCaller == address(0)); + } + + function g() log public { + } +} +// ---- +// Warning 6328: (347-379): CHC: Assertion violation happens here. +// Warning 6328: (389-421): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call_tx_origin.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call_tx_origin.sol new file mode 100644 index 000000000..04dd5599d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/this_external_call_tx_origin.sol @@ -0,0 +1,14 @@ +pragma experimental SMTChecker; + +contract C { + + function test() view public { + require(address(this) != tx.origin); + assert(!this.g()); + } + + function g() view public returns (bool) { + return msg.sender == tx.origin; + } +} +// ---- diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol b/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol new file mode 100644 index 000000000..60c1a57d5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + uint public x; + + function f() public view { + uint y = this.x(); + assert(y == x); // This fails as false positive because of lack of support for external getters. + } +} +// ---- +// Warning 6328: (114-128): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol b/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol new file mode 100644 index 000000000..5091da3f3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => uint) public map; + + function f() public view { + uint y = this.map(2); + assert(y == map[2]); // This fails as false positive because of lack of support for external getters. + } +} +// ---- +// Warning 6328: (137-156): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol b/test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol new file mode 100644 index 000000000..aaa9605cc --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol @@ -0,0 +1,12 @@ +pragma experimental SMTChecker; + +contract C { + mapping (uint => mapping (uint => uint)) public map; + + function f() public view { + uint y = this.map(2, 3); + assert(y == map[2][3]); // This fails as false positive because of lack of support for external getters. + } +} +// ---- +// Warning 6328: (158-180): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/this_state.sol b/test/libsolidity/smtCheckerTests/functions/this_state.sol index 7cef58b3e..9f417380e 100644 --- a/test/libsolidity/smtCheckerTests/functions/this_state.sol +++ b/test/libsolidity/smtCheckerTests/functions/this_state.sol @@ -6,7 +6,6 @@ contract C function g() public { x = 0; this.h(); - // Fails as false positive because CHC does not support `this`. assert(x == 2); } function h() public { @@ -14,4 +13,3 @@ contract C } } // ---- -// Warning 6328: (186-200): CHC: Assertion violation happens here.