From fc482de695b10bd94a695f5c6b8823e7212d7f23 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 11 Apr 2019 18:14:48 +0200 Subject: [PATCH] [SMTChecker] Support address members --- Changelog.md | 1 + libsolidity/formal/EncodingContext.cpp | 44 +++++++++++++++++++ libsolidity/formal/EncodingContext.h | 12 +++++ libsolidity/formal/SMTChecker.cpp | 34 ++++++++++++++ libsolidity/formal/SMTChecker.h | 1 + .../smtCheckerTests/types/address_balance.sol | 13 ++++++ .../smtCheckerTests/types/address_call.sol | 23 ++++++++++ .../types/address_delegatecall.sol | 23 ++++++++++ .../types/address_staticcall.sol | 23 ++++++++++ .../types/address_transfer.sol | 16 +++++++ .../types/address_transfer_2.sol | 21 +++++++++ .../types/address_transfer_insufficient.sol | 18 ++++++++ .../smtCheckerTestsJSON/multi.json | 6 +-- .../smtCheckerTestsJSON/simple.json | 2 +- 14 files changed, 233 insertions(+), 4 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/types/address_balance.sol create mode 100644 test/libsolidity/smtCheckerTests/types/address_call.sol create mode 100644 test/libsolidity/smtCheckerTests/types/address_delegatecall.sol create mode 100644 test/libsolidity/smtCheckerTests/types/address_staticcall.sol create mode 100644 test/libsolidity/smtCheckerTests/types/address_transfer.sol create mode 100644 test/libsolidity/smtCheckerTests/types/address_transfer_2.sol create mode 100644 test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol diff --git a/Changelog.md b/Changelog.md index e8297bb70..c124c9cdd 100644 --- a/Changelog.md +++ b/Changelog.md @@ -19,6 +19,7 @@ Compiler Features: * SMTChecker: Support mod. * SMTChecker: Support ``contract`` type. * SMTChecker: Support ``this`` as address. + * SMTChecker: Support address members. * Optimizer: Add rule for shifts by constants larger than 255 for Constantinople. * Optimizer: Add rule to simplify certain ANDs and SHL combinations * Yul: Adds break and continue keywords to for-loop syntax. diff --git a/libsolidity/formal/EncodingContext.cpp b/libsolidity/formal/EncodingContext.cpp index 03f904d7f..176cc3d12 100644 --- a/libsolidity/formal/EncodingContext.cpp +++ b/libsolidity/formal/EncodingContext.cpp @@ -28,14 +28,58 @@ EncodingContext::EncodingContext(SolverInterface& _solver): m_solver(_solver), m_thisAddress(make_unique("this", m_solver)) { + auto sort = make_shared( + make_shared(smt::Kind::Int), + make_shared(smt::Kind::Int) + ); + m_balances = make_unique(sort, "balances", m_solver); } void EncodingContext::reset() { m_thisAddress->increaseIndex(); + m_balances->increaseIndex(); } smt::Expression EncodingContext::thisAddress() { return m_thisAddress->currentValue(); } + +smt::Expression EncodingContext::balance() +{ + return balance(m_thisAddress->currentValue()); +} + +smt::Expression EncodingContext::balance(smt::Expression _address) +{ + return smt::Expression::select(m_balances->currentValue(), move(_address)); +} + +void EncodingContext::transfer(smt::Expression _from, smt::Expression _to, smt::Expression _value) +{ + unsigned indexBefore = m_balances->index(); + addBalance(_from, 0 - _value); + addBalance(_to, move(_value)); + unsigned indexAfter = m_balances->index(); + solAssert(indexAfter > indexBefore, ""); + m_balances->increaseIndex(); + /// Do not apply the transfer operation if _from == _to. + auto newBalances = smt::Expression::ite( + move(_from) == move(_to), + m_balances->valueAtIndex(indexBefore), + m_balances->valueAtIndex(indexAfter) + ); + m_solver.addAssertion(m_balances->currentValue() == newBalances); +} + +void EncodingContext::addBalance(smt::Expression _address, smt::Expression _value) +{ + auto newBalances = smt::Expression::store( + m_balances->currentValue(), + _address, + balance(_address) + move(_value) + ); + m_balances->increaseIndex(); + m_solver.addAssertion(newBalances == m_balances->currentValue()); +} diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h index 4170341cb..df6e69c07 100644 --- a/libsolidity/formal/EncodingContext.h +++ b/libsolidity/formal/EncodingContext.h @@ -41,12 +41,24 @@ public: /// Value of `this` address. smt::Expression thisAddress(); + /// @returns the symbolic balance of address `this`. + smt::Expression balance(); + /// @returns the symbolic balance of an address. + smt::Expression balance(smt::Expression _address); + /// Transfer _value from _from to _to. + void transfer(smt::Expression _from, smt::Expression _to, smt::Expression _value); + private: + /// Adds _value to _account's balance. + void addBalance(smt::Expression _account, smt::Expression _value); + SolverInterface& m_solver; /// Symbolic `this` address. std::unique_ptr m_thisAddress; + /// Symbolic balances. + std::unique_ptr m_balances; }; } diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 997b0df70..9baab9b54 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -112,6 +112,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function) if (isRootFunction()) { m_interface->reset(); + m_context.reset(); m_pathConditions.clear(); m_callStack.clear(); m_expressions.clear(); @@ -609,6 +610,12 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) popCallStack(); break; case FunctionType::Kind::External: + case FunctionType::Kind::DelegateCall: + case FunctionType::Kind::BareCall: + case FunctionType::Kind::BareCallCode: + case FunctionType::Kind::BareDelegateCall: + case FunctionType::Kind::BareStaticCall: + case FunctionType::Kind::Creation: m_externalFunctionCallHappened = true; resetStateVariables(); resetStorageReferences(); @@ -622,6 +629,22 @@ void SMTChecker::endVisit(FunctionCall const& _funCall) case FunctionType::Kind::MulMod: abstractFunctionCall(_funCall); break; + case FunctionType::Kind::Send: + case FunctionType::Kind::Transfer: + { + auto const& memberAccess = dynamic_cast(_funCall.expression()); + auto const& address = memberAccess.expression(); + auto const& value = args.at(0); + solAssert(value, ""); + + smt::Expression thisBalance = m_context.balance(); + setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), *m_interface); + checkCondition(thisBalance < expr(*value), _funCall.location(), "Insufficient funds", "address(this).balance", &thisBalance); + + m_context.transfer(m_context.thisAddress(), expr(address), expr(*value)); + createExpr(_funCall); + break; + } default: m_errorReporter.warning( _funCall.location(), @@ -874,6 +897,17 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess) } return false; } + else if (exprType->category() == Type::Category::Address) + { + _memberAccess.expression().accept(*this); + if (_memberAccess.memberName() == "balance") + { + defineExpr(_memberAccess, m_context.balance(expr(_memberAccess.expression()))); + setSymbolicUnknownValue(*m_expressions[&_memberAccess], *m_interface); + m_uninterpretedTerms.insert(&_memberAccess); + return false; + } + } else m_errorReporter.warning( _memberAccess.location(), diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index c6fcc4982..2f24e78b3 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -286,6 +286,7 @@ private: std::unordered_map> m_expressions; std::unordered_map> m_variables; std::unordered_map> m_globalContext; + /// Stores the instances of an Uninterpreted Function applied to arguments. /// These may be direct application of UFs or Array index access. /// Used to retrieve models. diff --git a/test/libsolidity/smtCheckerTests/types/address_balance.sol b/test/libsolidity/smtCheckerTests/types/address_balance.sol new file mode 100644 index 000000000..445888f05 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/address_balance.sol @@ -0,0 +1,13 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(address a, address b) public view { + uint x = b.balance + 1000 ether; + assert(a.balance > b.balance); + } +} +// ---- +// Warning: (96-102): Unused local variable. +// Warning: (131-160): Assertion violation happens here +// Warning: (105-127): Overflow (resulting value larger than 2**256 - 1) happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_call.sol b/test/libsolidity/smtCheckerTests/types/address_call.sol new file mode 100644 index 000000000..05c423406 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/address_call.sol @@ -0,0 +1,23 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + mapping (uint => uint) map; + function f(address a, bytes memory data) public { + x = 0; + map[0] = 0; + mapping (uint => uint) storage localMap = map; + (bool success, bytes memory ret) = a.call(data); + assert(success); + assert(x == 0); + assert(map[0] == 0); + assert(localMap[0] == 0); + } +} +// ==== +// EVMVersion: >spuriousDragon +// ---- +// Warning: (224-240): Unused local variable. +// Warning: (209-256): Assertion checker does not yet support such variable declarations. +// Warning: (260-275): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol b/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol new file mode 100644 index 000000000..ce49350ef --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/address_delegatecall.sol @@ -0,0 +1,23 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + mapping (uint => uint) map; + function f(address a, bytes memory data) public { + x = 0; + map[0] = 0; + mapping (uint => uint) storage localMap = map; + (bool success, bytes memory ret) = a.delegatecall(data); + assert(success); + assert(x == 0); + assert(map[0] == 0); + assert(localMap[0] == 0); + } +} +// ==== +// EVMVersion: >spuriousDragon +// ---- +// Warning: (224-240): Unused local variable. +// Warning: (209-264): Assertion checker does not yet support such variable declarations. +// Warning: (268-283): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_staticcall.sol b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol new file mode 100644 index 000000000..5336a14e6 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/address_staticcall.sol @@ -0,0 +1,23 @@ +pragma experimental SMTChecker; + +contract C +{ + uint x; + mapping (uint => uint) map; + function f(address a, bytes memory data) public { + x = 0; + map[0] = 0; + mapping (uint => uint) storage localMap = map; + (bool success, bytes memory ret) = a.staticcall(data); + assert(success); + assert(x == 0); + assert(map[0] == 0); + assert(localMap[0] == 0); + } +} +// ==== +// EVMVersion: >spuriousDragon +// ---- +// Warning: (224-240): Unused local variable. +// Warning: (209-262): Assertion checker does not yet support such variable declarations. +// Warning: (266-281): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer.sol b/test/libsolidity/smtCheckerTests/types/address_transfer.sol new file mode 100644 index 000000000..08a5244c3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/address_transfer.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(address payable a) public { + uint x = 100; + require(x == a.balance); + a.transfer(600); + // This fails since a == this is possible. + assert(a.balance == 700); + } +} +// ---- +// Warning: (131-146): Insufficient funds happens here +// Warning: (131-146): Assertion checker does not yet implement this type. +// Warning: (195-219): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol new file mode 100644 index 000000000..d2f9e6939 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_2.sol @@ -0,0 +1,21 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(uint x, address payable a, address payable b) public { + require(a != b); + require(x == 100); + require(x == a.balance); + require(a.balance == b.balance); + a.transfer(600); + b.transfer(100); + // Fails since a == this is possible. + assert(a.balance > b.balance); + } +} +// ---- +// Warning: (217-232): Insufficient funds happens here +// Warning: (217-232): Assertion checker does not yet implement this type. +// Warning: (236-251): Insufficient funds happens here +// Warning: (236-251): Assertion checker does not yet implement this type. +// Warning: (295-324): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol new file mode 100644 index 000000000..d3bfbe302 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/types/address_transfer_insufficient.sol @@ -0,0 +1,18 @@ +pragma experimental SMTChecker; + +contract C +{ + function f(address payable a, address payable b) public { + require(a.balance == 0); + a.transfer(600); + b.transfer(1000); + // Fails since a == this is possible. + assert(a.balance == 600); + } +} +// ---- +// Warning: (134-149): Insufficient funds happens here +// Warning: (134-149): Assertion checker does not yet implement this type. +// Warning: (153-169): Insufficient funds happens here +// Warning: (153-169): Assertion checker does not yet implement this type. +// Warning: (213-237): Assertion violation happens here diff --git a/test/libsolidity/smtCheckerTestsJSON/multi.json b/test/libsolidity/smtCheckerTestsJSON/multi.json index df45fbf4b..c44198234 100644 --- a/test/libsolidity/smtCheckerTestsJSON/multi.json +++ b/test/libsolidity/smtCheckerTestsJSON/multi.json @@ -3,9 +3,9 @@ { "smtlib2responses": { - "0x47826ec8b83cfec30171b34f944aed6c33ecd12f02b9ad522ca45317c9bd5f45": "sat\n((|EVALEXPR_0| 1))", - "0x734c058efe9d6ec224de3cf2bdfa6c936a1c9c159c040c128d631145b2fed195": "unsat\n", - "0xa0c072acdbe5181dd56cbad8960cb5bb0b9e97fd598cfd895467bd73bbcca028": "sat\n((|EVALEXPR_0| 0))" + "0x47a038dd9021ecb218726ea6bf1f75c215a50b1981bae4341e89c9f2b7ac5db7": "sat\n((|EVALEXPR_0| 1))", + "0xf057b272f2ceb99a2f714cb132960babdeedfb84ff8ffb96106a58bc0c2060cb": "sat\n((|EVALEXPR_0| 0))", + "0xf49b9d0eb7b6d2f2ac9e1604288e52ee1a08cda57058e26d7843ed109ca6d7c9": "unsat\n" } } } diff --git a/test/libsolidity/smtCheckerTestsJSON/simple.json b/test/libsolidity/smtCheckerTestsJSON/simple.json index b82d93b8c..f9935ab01 100644 --- a/test/libsolidity/smtCheckerTestsJSON/simple.json +++ b/test/libsolidity/smtCheckerTestsJSON/simple.json @@ -3,7 +3,7 @@ { "smtlib2responses": { - "0xa0c072acdbe5181dd56cbad8960cb5bb0b9e97fd598cfd895467bd73bbcca028": "sat\n((|EVALEXPR_0| 0))\n" + "0xf057b272f2ceb99a2f714cb132960babdeedfb84ff8ffb96106a58bc0c2060cb": "sat\n((|EVALEXPR_0| 0))\n" } } }