From 106c591dde4c38a7c51f30924552ac4582e61277 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Mon, 30 Aug 2021 18:21:22 +0200 Subject: [PATCH] Support the external call option --- Changelog.md | 1 + libsolidity/formal/CHC.cpp | 28 ++++++++++++++++--- libsolidity/formal/SMTEncoder.cpp | 13 ++++++++- libsolidity/formal/SMTEncoder.h | 4 +++ .../external_calls/call_with_value_1.sol | 14 ++++++++++ .../external_calls/call_with_value_2.sol | 15 ++++++++++ .../external_calls/call_with_value_3.sol | 15 ++++++++++ .../external_call_this_with_value_1.sol | 14 ++++++++++ .../external_call_this_with_value_2.sol | 15 ++++++++++ .../external_call_with_value_1.sol | 18 ++++++++++++ .../external_call_with_value_2.sol | 18 ++++++++++++ .../external_call_with_value_3.sol | 18 ++++++++++++ 12 files changed, 168 insertions(+), 5 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/call_with_value_3.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_1.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol create mode 100644 test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol diff --git a/Changelog.md b/Changelog.md index b187d009c..509d940d4 100644 --- a/Changelog.md +++ b/Changelog.md @@ -10,6 +10,7 @@ Compiler Features: * Immutable variables can be read at construction time once they are initialized. * SMTChecker: Support low level ``call`` as external calls to unknown code. * SMTChecker: Add constraints to better correlate ``address(this).balance`` and ``msg.value``. + * SMTChecker: Support the ``value`` option for external function calls. * Commandline Interface: Disallowed the ``--experimental-via-ir`` option to be used with Standard Json, Assembler and Linker modes. diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 140b2a27d..b7292221b 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -34,6 +34,7 @@ #include +#include #include #ifdef HAVE_Z3_DLOPEN @@ -743,13 +744,15 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) /// so we just add the nondet_interface predicate. solAssert(m_currentContract, ""); - if (isTrustedExternalCall(&_funCall.expression())) + auto [callExpr, callOptions] = functionCallExpression(_funCall); + + if (isTrustedExternalCall(callExpr)) { externalFunctionCallToTrustedCode(_funCall); return; } - FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); + FunctionType const& funType = dynamic_cast(*callExpr->annotation().type); auto kind = funType.kind(); solAssert( kind == FunctionType::Kind::External || @@ -773,6 +776,19 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) if (!m_currentFunction || m_currentFunction->isConstructor()) return; + if (callOptions) + { + optional valueIndex; + for (auto&& [i, name]: callOptions->names() | ranges::views::enumerate) + if (name && *name == "value") + { + valueIndex = i; + break; + } + solAssert(valueIndex, ""); + state().addBalance(state().thisAddress(), 0 - expr(*callOptions->options().at(*valueIndex))); + } + auto preCallState = vector{state().state()} + currentStateVariables(); if (!usesStaticCall) @@ -829,6 +845,8 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall) state().newTx(); // set the transaction sender as this contract m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress()); + // set the transaction value as 0 + m_context.addAssertion(state().txMember("msg.value") == 0); // set the origin to be the current transaction origin m_context.addAssertion(state().txMember("tx.origin") == txOrigin); @@ -1451,10 +1469,12 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall) return smtutil::Expression(true); auto contractAddressValue = [this](FunctionCall const& _f) { - FunctionType const& funType = dynamic_cast(*_f.expression().annotation().type); + auto [callExpr, callOptions] = functionCallExpression(_f); + + FunctionType const& funType = dynamic_cast(*callExpr->annotation().type); if (funType.kind() == FunctionType::Kind::Internal) return state().thisAddress(); - if (MemberAccess const* callBase = dynamic_cast(&_f.expression())) + if (MemberAccess const* callBase = dynamic_cast(callExpr)) return expr(callBase->expression()); solAssert(false, "Unreachable!"); }; diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 6fcc08ca8..411fa2757 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -2590,6 +2590,16 @@ Expression const* SMTEncoder::innermostTuple(Expression const& _expr) return expr; } +pair SMTEncoder::functionCallExpression(FunctionCall const& _funCall) +{ + Expression const* callExpr = &_funCall.expression(); + auto const* callOptions = dynamic_cast(callExpr); + if (callOptions) + callExpr = &callOptions->expression(); + + return {callExpr, callOptions}; +} + Expression const* SMTEncoder::cleanExpression(Expression const& _expr) { auto const* expr = &_expr; @@ -2713,7 +2723,8 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition( if (*_funCall.annotation().kind != FunctionCallKind::FunctionCall) return {}; - Expression const* calledExpr = &_funCall.expression(); + auto [calledExpr, callOptions] = functionCallExpression(_funCall); + if (TupleExpression const* fun = dynamic_cast(calledExpr)) { solAssert(fun->components().size() == 1, ""); diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 7cf4b065e..28270acc0 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -71,6 +71,10 @@ public: /// otherwise _expr. static Expression const* innermostTuple(Expression const& _expr); + /// @returns {_funCall.expression(), nullptr} if function call option values are not given, and + /// {_funCall.expression().expression(), _funCall.expression()} if they are. + static std::pair functionCallExpression(FunctionCall const& _funCall); + /// @returns the expression after stripping redundant syntactic sugar. /// Currently supports stripping: /// 1. 1-tuple; i.e. ((x)) -> x diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol new file mode 100644 index 000000000..ed27a4df8 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol @@ -0,0 +1,14 @@ +contract C { + function g(address payable i) public { + require(address(this).balance == 100); + i.call{value: 10}(""); + // Disabled due to Spacer nondeterminism + //assert(address(this).balance == 90); // should hold + // Disabled due to Spacer nondeterminism + //assert(address(this).balance == 100); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 9302: (96-117): Return value of low-level calls not used. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol new file mode 100644 index 000000000..792bb0730 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol @@ -0,0 +1,15 @@ +contract C { + function g(address payable i) public { + require(address(this).balance == 100); + i.call{value: 0}(""); + assert(address(this).balance == 100); // should hold + assert(address(this).balance == 20); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 9302: (96-116): Return value of low-level calls not used. +// Warning 6328: (120-156): CHC: Assertion violation might happen here. +// Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n i.call{value: 0}("") -- untrusted external call +// Warning 4661: (120-156): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_3.sol b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_3.sol new file mode 100644 index 000000000..6cbe24136 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_3.sol @@ -0,0 +1,15 @@ +contract C { + function g(address payable i) public { + require(address(this).balance > 100); + i.call{value: 20}(""); + assert(address(this).balance > 0); // should hold + // Disabled due to Spacer nondeterminism + //assert(address(this).balance == 0); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 9302: (95-116): Return value of low-level calls not used. +// Warning 6328: (120-153): CHC: Assertion violation might happen here. +// Warning 4661: (120-153): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol new file mode 100644 index 000000000..06390b12c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_1.sol @@ -0,0 +1,14 @@ +contract C { + function g() public { + require(address(this).balance == 100); + this.h{value: 10}(); + assert(address(this).balance == 100); // should hold + assert(address(this).balance == 90); // should fail + } + + function h() external payable {} +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (157-192): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol new file mode 100644 index 000000000..fc2d844d9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_this_with_value_2.sol @@ -0,0 +1,15 @@ +contract C { + function g(uint i) public { + require(address(this).balance == 100); + this.h{value: i}(); + assert(address(this).balance == 100); // should hold + assert(address(this).balance == 90); // should fail + } + + function h() external payable {} +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (162-197): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_1.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_1.sol new file mode 100644 index 000000000..a5ac8ded9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_1.sol @@ -0,0 +1,18 @@ +interface I { + function f() external payable; +} + +contract C { + function g(I i) public { + require(address(this).balance == 100); + i.f{value: 10}(); + assert(address(this).balance == 90); // should hold + // Disabled due to Spacer nondeterminism + //assert(address(this).balance == 100); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (151-186): CHC: Assertion violation might happen here. +// Warning 4661: (151-186): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol new file mode 100644 index 000000000..4b51d9d9e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_2.sol @@ -0,0 +1,18 @@ +interface I { + function f() external payable; +} + +contract C { + function g(I i) public { + require(address(this).balance == 100); + i.f{value: 0}(); + assert(address(this).balance == 100); // should hold + assert(address(this).balance == 90); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (150-186): CHC: Assertion violation might happen here. +// Warning 6328: (205-240): CHC: Assertion violation happens here. +// Warning 4661: (150-186): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol new file mode 100644 index 000000000..d0e4c84aa --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_with_value_3.sol @@ -0,0 +1,18 @@ +interface I { + function f() external payable; +} + +contract C { + function g(I i) public { + require(address(this).balance > 100); + i.f{value: 20}(); + assert(address(this).balance > 0); // should hold + assert(address(this).balance == 0); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (150-183): CHC: Assertion violation might happen here. +// Warning 6328: (202-236): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0\n\nTransaction trace:\nC.constructor()\nC.g(0)\n i.f{value: 20}() -- untrusted external call +// Warning 4661: (150-183): BMC: Assertion violation happens here.