Skip to content

Commit c69f919

Browse files
hrkrshnnhrkrshnn
authored
Merge pull request #11841 from ethereum/smt_fix_delegatecall
[SMTChecker] Erase balances when delegatecall is seen
2 parents 7a0295e + 718f392 commit c69f919

16 files changed

+258
-0
lines changed

‎libsolidity/formal/BMC.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -587,10 +587,16 @@ void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
587587
_funCall.location(),
588588
"BMC does not yet implement this type of function call."
589589
);
590+
else if (funType.kind() == FunctionType::Kind::BareStaticCall)
591+
{
592+
// Do nothing here.
593+
// Neither storage nor balances should be modified.
594+
}
590595
else
591596
{
592597
m_externalFunctionCallHappened = true;
593598
resetStorageVariables();
599+
resetBalances();
594600
}
595601
}
596602

‎libsolidity/formal/CHC.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -995,6 +995,7 @@ void CHC::resetContractAnalysis()
995995
void CHC::eraseKnowledge()
996996
{
997997
resetStorageVariables();
998+
resetBalances();
998999
}
9991000

10001001
void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)

‎libsolidity/formal/SMTEncoder.cpp

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2281,6 +2281,13 @@ void SMTEncoder::resetStorageVariables()
22812281
});
22822282
}
22832283

2284+
void SMTEncoder::resetBalances()
2285+
{
2286+
// TODO this should be changed to `balances` only
2287+
// when `state` gets more members.
2288+
state().newState();
2289+
}
2290+
22842291
void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl)
22852292
{
22862293
m_context.resetVariables([&](VariableDeclaration const& _var) {

‎libsolidity/formal/SMTEncoder.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -303,6 +303,7 @@ class SMTEncoder: public ASTConstVisitor
303303
void resetStateVariables();
304304
void resetStorageVariables();
305305
void resetMemoryVariables();
306+
void resetBalances();
306307
/// Resets all references/pointers that have the same type or have
307308
/// a subexpression of the same type as _varDecl.
308309
void resetReferences(VariableDeclaration const& _varDecl);

‎test/libsolidity/smtCheckerTests/blockchain_state/free_function_1.sol

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
function l(address payable a) {}
2+
3+
contract C {
4+
uint x;
5+
function f(address payable a) public payable {
6+
require(msg.value > 1);
7+
uint b1 = address(this).balance;
8+
l(a);
9+
uint b2 = address(this).balance;
10+
assert(b1 == b2); // should hold
11+
assert(x == 0); // should hold
12+
}
13+
}
14+
// ====
15+
// SMTEngine: all

‎test/libsolidity/smtCheckerTests/blockchain_state/free_function_2.sol

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
function l(address payable a) {
2+
a.transfer(1);
3+
}
4+
5+
contract C {
6+
uint x;
7+
function f(address payable a) public payable {
8+
require(msg.value > 1);
9+
uint b1 = address(this).balance;
10+
l(a);
11+
uint b2 = address(this).balance;
12+
assert(b1 == b2); // should fail
13+
assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
14+
assert(x == 0); // should hold
15+
}
16+
}
17+
// ====
18+
// SMTEngine: all
19+
// SMTIgnoreCex: yes
20+
// ----
21+
// Warning 6328: (227-243): CHC: Assertion violation happens here.
22+
// Warning 3944: (275-281): CHC: Underflow (resulting value less than 0) happens here.
23+
// Warning 6328: (262-282): CHC: Assertion violation happens here.
24+
// Warning 1236: (33-46): BMC: Insufficient funds happens here.

‎test/libsolidity/smtCheckerTests/blockchain_state/library_internal_1.sol

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
library L {
2+
function l(address payable a) internal {}
3+
}
4+
5+
contract C {
6+
using L for address payable;
7+
uint x;
8+
function f(address payable a) public payable {
9+
require(msg.value > 1);
10+
uint b1 = address(this).balance;
11+
a.l();
12+
uint b2 = address(this).balance;
13+
assert(b1 == b2); // should hold
14+
assert(x == 0); // should hold
15+
}
16+
}
17+
// ====
18+
// SMTEngine: all

‎test/libsolidity/smtCheckerTests/blockchain_state/library_internal_2.sol

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
library L {
2+
function l(address payable a) internal {
3+
a.transfer(1);
4+
}
5+
}
6+
7+
contract C {
8+
using L for address payable;
9+
uint x;
10+
function f(address payable a) public payable {
11+
require(msg.value > 1);
12+
uint b1 = address(this).balance;
13+
a.l();
14+
uint b2 = address(this).balance;
15+
assert(b1 == b2); // should fail
16+
assert(b1 == b2 - 1); // should hold but we don't keep track of balances with msg.value yet
17+
assert(x == 0); // should hold
18+
}
19+
}
20+
// ====
21+
// SMTEngine: all
22+
// ----
23+
// 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
24+
// 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
25+
// 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
26+
// Warning 1236: (56-69): BMC: Insufficient funds happens here.
27+
// Warning 1236: (56-69): BMC: Insufficient funds happens here.

‎test/libsolidity/smtCheckerTests/blockchain_state/library_public_1.sol

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
library L {
2+
function l(address payable a) public {}
3+
}
4+
5+
contract C {
6+
using L for address payable;
7+
uint x;
8+
function f(address payable a) public payable {
9+
require(msg.value > 1);
10+
uint b1 = address(this).balance;
11+
a.l();
12+
uint b2 = address(this).balance;
13+
assert(b1 == b2); // should fail because the called library can transfer with `this`s balance
14+
assert(x == 0); // should fail because of `delegatecall`
15+
}
16+
}
17+
// ====
18+
// SMTEngine: all
19+
// ----
20+
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.
21+
// 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 }
22+
// 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 }
23+
// Warning 4588: (219-224): Assertion checker does not yet implement this type of function call.

‎test/libsolidity/smtCheckerTests/blockchain_state/library_public_2.sol

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
library L {
2+
function l(address payable a) public {
3+
a.transfer(1);
4+
}
5+
}
6+
7+
contract C {
8+
using L for address payable;
9+
uint x;
10+
function f(address payable a) public payable {
11+
require(msg.value > 1);
12+
uint b1 = address(this).balance;
13+
a.l();
14+
uint b2 = address(this).balance;
15+
assert(b1 == b2); // should fail
16+
assert(x == 0); // should fail because of `delegatecall`
17+
}
18+
}
19+
// ====
20+
// SMTEngine: all
21+
// SMTIgnoreCex: yes
22+
// ----
23+
// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.
24+
// Warning 6328: (282-298): CHC: Assertion violation happens here.
25+
// Warning 6328: (317-331): CHC: Assertion violation happens here.
26+
// Warning 1236: (54-67): BMC: Insufficient funds happens here.
27+
// Warning 4588: (238-243): Assertion checker does not yet implement this type of function call.

0 commit comments

Comments
 (0)