Skip to content

Commit 2620796

Browse files
author
Leonardo
authored
Merge pull request #11820 from ethereum/smt_barecall
[SMTChecker] CALL
2 parents 45a910c + 55d197f commit 2620796

21 files changed

+239
-24
lines changed

‎Changelog.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Language Features:
55

66
Compiler Features:
77
* Immutable variables can be read at construction time once they are initialized.
8+
* SMTChecker: Support low level ``call`` as external calls to unknown code.
89

910

1011
Bugfixes:

‎libsolidity/formal/CHC.cpp

Lines changed: 16 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -529,11 +529,11 @@ void CHC::endVisit(FunctionCall const& _funCall)
529529
break;
530530
case FunctionType::Kind::External:
531531
case FunctionType::Kind::BareStaticCall:
532+
case FunctionType::Kind::BareCall:
532533
externalFunctionCall(_funCall);
533534
SMTEncoder::endVisit(_funCall);
534535
break;
535536
case FunctionType::Kind::DelegateCall:
536-
case FunctionType::Kind::BareCall:
537537
case FunctionType::Kind::BareCallCode:
538538
case FunctionType::Kind::BareDelegateCall:
539539
case FunctionType::Kind::Creation:
@@ -746,23 +746,29 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
746746

747747
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
748748
auto kind = funType.kind();
749-
solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
749+
solAssert(
750+
kind == FunctionType::Kind::External ||
751+
kind == FunctionType::Kind::BareCall ||
752+
kind == FunctionType::Kind::BareStaticCall,
753+
""
754+
);
755+
756+
bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall;
750757

751758
solAssert(m_currentContract, "");
752759
auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
753-
if (!function)
754-
return;
755-
756-
for (auto var: function->returnParameters())
757-
m_context.variable(*var)->increaseIndex();
760+
if (function)
761+
{
762+
usesStaticCall |= function->stateMutability() == StateMutability::Pure ||
763+
function->stateMutability() == StateMutability::View;
764+
for (auto var: function->returnParameters())
765+
m_context.variable(*var)->increaseIndex();
766+
}
758767

759768
if (!m_currentFunction || m_currentFunction->isConstructor())
760769
return;
761770

762771
auto preCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
763-
bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall ||
764-
function->stateMutability() == StateMutability::Pure ||
765-
function->stateMutability() == StateMutability::View;
766772

767773
if (!usesStaticCall)
768774
{

‎libsolidity/formal/SMTEncoder.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -611,6 +611,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
611611
break;
612612
case FunctionType::Kind::Internal:
613613
case FunctionType::Kind::BareStaticCall:
614+
case FunctionType::Kind::BareCall:
614615
break;
615616
case FunctionType::Kind::KECCAK256:
616617
case FunctionType::Kind::ECRecover:
@@ -653,7 +654,6 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
653654
visitObjectCreation(_funCall);
654655
return;
655656
case FunctionType::Kind::DelegateCall:
656-
case FunctionType::Kind::BareCall:
657657
case FunctionType::Kind::BareCallCode:
658658
case FunctionType::Kind::BareDelegateCall:
659659
case FunctionType::Kind::Creation:

‎test/libsolidity/smtCheckerTests/complex/slither/external_function.sol

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -84,9 +84,7 @@ contract InternalCall {
8484
// Warning 2018: (1179-1241): Function state mutability can be restricted to pure
8585
// Warning 2018: (1247-1309): Function state mutability can be restricted to pure
8686
// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
87-
// Warning 4588: (727-782): Assertion checker does not yet implement this type of function call.
8887
// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
8988
// Warning 4588: (681-716): Assertion checker does not yet implement this type of function call.
90-
// Warning 4588: (727-782): Assertion checker does not yet implement this type of function call.
9189
// Warning 4588: (854-886): Assertion checker does not yet implement this type of function call.
9290
// Warning 5729: (1370-1375): BMC does not yet implement this type of function call.

‎test/libsolidity/smtCheckerTests/external_calls/call_constructor_1.sol

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
contract C {
2+
uint x;
3+
constructor(address _a) {
4+
_a.call("aaaa");
5+
assert(x == 0); // should hold
6+
}
7+
}
8+
// ====
9+
// SMTEngine: all
10+
// ----
11+
// Warning 9302: (51-66): Return value of low-level calls not used.

‎test/libsolidity/smtCheckerTests/external_calls/call_constructor_2.sol

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
contract C {
2+
uint x;
3+
function f(uint _x) public {
4+
x = _x;
5+
}
6+
constructor(address _a) {
7+
_a.call("aaaa");
8+
assert(x == 0); // should hold
9+
}
10+
}
11+
// ====
12+
// SMTEngine: all
13+
// ----
14+
// Warning 9302: (94-109): Return value of low-level calls not used.

‎test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
contract C {
2+
uint x;
3+
4+
bool lock;
5+
modifier mutex {
6+
require(!lock);
7+
lock = true;
8+
_;
9+
lock = false;
10+
}
11+
12+
function set(uint _x) mutex public {
13+
x = _x;
14+
}
15+
16+
function f(address _a) mutex public {
17+
uint y = x;
18+
_a.call("aaaaa");
19+
assert(y == x); // should hold
20+
}
21+
}
22+
// ====
23+
// SMTEngine: all
24+
// ----
25+
// Warning 9302: (218-234): Return value of low-level calls not used.

‎test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
contract C {
2+
uint x;
3+
4+
bool lock;
5+
modifier mutex {
6+
require(!lock);
7+
lock = true;
8+
_;
9+
lock = false;
10+
}
11+
12+
function set(uint _x) mutex public {
13+
x = _x;
14+
}
15+
16+
function f(address _a) public {
17+
uint y = x;
18+
_a.call("aaaaa");
19+
assert(y == x); // should fail
20+
}
21+
}
22+
// ====
23+
// SMTEngine: all
24+
// ----
25+
// Warning 9302: (212-228): Return value of low-level calls not used.
26+
// Warning 6328: (232-246): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, lock = false\n_a = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, lock = false\nC.f(0)\n _a.call("aaaaa") -- untrusted external call, synthesized as:\n C.set(1) -- reentrant call

‎test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_1.sol

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
contract C {
2+
uint x;
3+
function s(uint _x) public {
4+
x = _x;
5+
}
6+
function f(address a) public {
7+
(bool s, bytes memory data) = a.call("");
8+
assert(x == 0); // should fail
9+
}
10+
}
11+
// ====
12+
// SMTEngine: all
13+
// ----
14+
// Warning 2519: (100-106): This declaration shadows an existing declaration.
15+
// Warning 2072: (100-106): Unused local variable.
16+
// Warning 2072: (108-125): Unused local variable.
17+
// Warning 6328: (143-157): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\na = 0\ns = false\ndata = [36, 5, 5, 5, 5, 5]\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.s(1)\nState: x = 1\nC.f(0)\n a.call("") -- untrusted external call

‎test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
contract C {
2+
uint x;
3+
function s(uint _x) public view {
4+
x == _x;
5+
}
6+
function f(address a) public {
7+
(bool s, bytes memory data) = a.call("");
8+
assert(x == 0); // should hold
9+
}
10+
}
11+
// ====
12+
// SMTEngine: all
13+
// ----
14+
// Warning 2519: (106-112): This declaration shadows an existing declaration.
15+
// Warning 2072: (106-112): Unused local variable.
16+
// Warning 2072: (114-131): Unused local variable.

0 commit comments

Comments
 (0)