From a55685c04ffd040dc0de2343d4f2b5f20da50100 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Wed, 25 Aug 2021 11:29:42 +0200 Subject: [PATCH] Erase balances when delegatecall is seen --- libsolidity/formal/BMC.cpp | 1 + libsolidity/formal/CHC.cpp | 1 + libsolidity/formal/SMTEncoder.cpp | 7 +++++ libsolidity/formal/SMTEncoder.h | 1 + .../blockchain_state/free_function_1.sol | 15 ++++++++++ .../blockchain_state/free_function_2.sol | 24 +++++++++++++++ .../blockchain_state/library_internal_1.sol | 18 +++++++++++ .../blockchain_state/library_internal_2.sol | 27 +++++++++++++++++ .../blockchain_state/library_public_1.sol | 23 ++++++++++++++ .../blockchain_state/library_public_2.sol | 27 +++++++++++++++++ .../blockchain_state/library_public_3.sol | 29 ++++++++++++++++++ .../blockchain_state/library_public_4.sol | 30 +++++++++++++++++++ 12 files changed, 203 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/library_public_3.sol create mode 100644 test/libsolidity/smtCheckerTests/blockchain_state/library_public_4.sol diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index c8f89db88..ddf1152a3 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -591,6 +591,7 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall) { m_externalFunctionCallHappened = true; resetStorageVariables(); + resetBalances(); } } diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 69ee0f7dc..64f868b6a 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -995,6 +995,7 @@ void CHC::resetContractAnalysis() void CHC::eraseKnowledge() { resetStorageVariables(); + resetBalances(); } void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 8a3d11707..c1a5393e7 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -2281,6 +2281,13 @@ void SMTEncoder::resetStorageVariables() }); } +void SMTEncoder::resetBalances() +{ + // TODO this should be changed to `balances` only + // when `state` gets more members. + state().newState(); +} + void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl) { m_context.resetVariables([&](VariableDeclaration const& _var) { diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 9adf38ffe..e8f876f40 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -303,6 +303,7 @@ protected: void resetStateVariables(); void resetStorageVariables(); void resetMemoryVariables(); + void resetBalances(); /// Resets all references/pointers that have the same type or have /// a subexpression of the same type as _varDecl. void resetReferences(VariableDeclaration const& _varDecl); diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol new file mode 100644 index 000000000..9b40afa2e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol @@ -0,0 +1,15 @@ +function l(address payable a) {} + +contract C { + uint x; + function f(address payable a) public payable { + require(msg.value > 1); + uint b1 = address(this).balance; + l(a); + uint b2 = address(this).balance; + assert(b1 == b2); // should hold + assert(x == 0); // should hold + } +} +// ==== +// SMTEngine: all diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol new file mode 100644 index 000000000..cfce81c53 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol @@ -0,0 +1,24 @@ +function l(address payable a) { + a.transfer(1); +} + +contract C { + uint x; + function f(address payable a) public payable { + require(msg.value > 1); + uint b1 = address(this).balance; + l(a); + uint b2 = address(this).balance; + assert(b1 == b2); // should fail + assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet + assert(x == 0); // should hold + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 6328: (227-243): CHC: Assertion violation happens here. +// Warning 3944: (275-281): CHC: Underflow (resulting value less than 0) happens here. +// Warning 6328: (262-282): CHC: Assertion violation happens here. +// Warning 1236: (33-46): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol new file mode 100644 index 000000000..4f7497625 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol @@ -0,0 +1,18 @@ +library L { + function l(address payable a) internal {} +} + +contract C { + using L for address payable; + uint x; + function f(address payable a) public payable { + require(msg.value > 1); + uint b1 = address(this).balance; + a.l(); + uint b2 = address(this).balance; + assert(b1 == b2); // should hold + assert(x == 0); // should hold + } +} +// ==== +// SMTEngine: all diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol new file mode 100644 index 000000000..d3ad410c1 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol @@ -0,0 +1,27 @@ +library L { + function l(address payable a) internal { + a.transfer(1); + } +} + +contract C { + using L for address payable; + uint x; + function f(address payable a) public payable { + require(msg.value > 1); + uint b1 = address(this).balance; + a.l(); + uint b2 = address(this).balance; + assert(b1 == b2); // should fail + assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet + assert(x == 0); // should hold + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (284-300): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 8856\nb2 = 8855\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 11799 }\n L.l(21238){ value: 11799 } -- internal call +// Warning 3944: (332-338): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\na = 38\nb1 = 1\nb2 = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(38){ value: 21240 }\n L.l(38){ value: 21240 } -- internal call +// Warning 6328: (319-339): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 21238\nb1 = 40\nb2 = 39\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(21238){ value: 8857 }\n L.l(21238){ value: 8857 } -- internal call +// Warning 1236: (56-69): BMC: Insufficient funds happens here. +// Warning 1236: (56-69): BMC: Insufficient funds happens here. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol new file mode 100644 index 000000000..d62301509 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol @@ -0,0 +1,23 @@ +library L { + function l(address payable a) public {} +} + +contract C { + using L for address payable; + uint x; + function f(address payable a) public payable { + require(msg.value > 1); + uint b1 = address(this).balance; + a.l(); + uint b2 = address(this).balance; + assert(b1 == b2); // should fail because the called library can transfer with `this`s balance + assert(x == 0); // should fail because of `delegatecall` + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call. +// Warning 6328: (263-279): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\na = 0\nb1 = 7720\nb2 = 7719\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 5855 } +// Warning 6328: (359-373): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\nb1 = 39\nb2 = 38\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.f(0){ value: 21240 } +// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol new file mode 100644 index 000000000..a77047efb --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol @@ -0,0 +1,27 @@ +library L { + function l(address payable a) public { + a.transfer(1); + } +} + +contract C { + using L for address payable; + uint x; + function f(address payable a) public payable { + require(msg.value > 1); + uint b1 = address(this).balance; + a.l(); + uint b2 = address(this).balance; + assert(b1 == b2); // should fail + assert(x == 0); // should fail because of `delegatecall` + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call. +// Warning 6328: (282-298): CHC: Assertion violation happens here. +// Warning 6328: (317-331): CHC: Assertion violation happens here. +// Warning 1236: (54-67): BMC: Insufficient funds happens here. +// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_public_3.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_3.sol new file mode 100644 index 000000000..a7abdeef9 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_3.sol @@ -0,0 +1,29 @@ +library L { + function l(address payable a) public returns (uint) { + return msg.value; + } +} + +contract C { + using L for address payable; + uint x; + function f(address payable a) public payable { + require(msg.value > 1); + uint b1 = address(this).balance; + uint v = a.l(); + uint b2 = address(this).balance; + assert(b1 == b2); // should fail because the called library can transfer with `this`s balance + assert(x == 0); // should fail because of `delegatecall` + assert(v == msg.value); // should hold but we don't support `delegatecall` properly yet. + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 5667: (24-41): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning 4588: (265-270): Assertion checker does not yet implement this type of function call. +// Warning 6328: (309-325): CHC: Assertion violation happens here. +// Warning 6328: (405-419): CHC: Assertion violation happens here. +// Warning 6328: (464-486): CHC: Assertion violation happens here. +// Warning 4588: (265-270): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/library_public_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_4.sol new file mode 100644 index 000000000..ccda62ad5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/blockchain_state/library_public_4.sol @@ -0,0 +1,30 @@ +library L { + function l(address payable a) public returns (address) { + return msg.sender; + } +} + +contract C { + using L for address payable; + uint x; + function f(address payable a) public payable { + require(msg.value > 1); + uint b1 = address(this).balance; + address v = a.l(); + uint b2 = address(this).balance; + assert(b1 == b2); // should fail because the called library can transfer with `this`s balance + assert(x == 0); // should fail because of `delegatecall` + assert(v == msg.sender); // should hold but we don't support `delegatecall` properly yet. + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 5667: (24-41): Unused function parameter. Remove or comment out the variable name to silence this warning. +// Warning 2018: (13-93): Function state mutability can be restricted to view +// Warning 4588: (272-277): Assertion checker does not yet implement this type of function call. +// Warning 6328: (316-332): CHC: Assertion violation happens here. +// Warning 6328: (412-426): CHC: Assertion violation happens here. +// Warning 6328: (471-494): CHC: Assertion violation happens here. +// Warning 4588: (272-277): Assertion checker does not yet implement this type of function call.