diff --git a/Changelog.md b/Changelog.md index 3b97bda71..0a392d173 100644 --- a/Changelog.md +++ b/Changelog.md @@ -5,6 +5,7 @@ Language Features: 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. Bugfixes: diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index d76058cc2..69ee0f7dc 100644 --- a/libsolidity/formal/CHC.cpp +++ b/libsolidity/formal/CHC.cpp @@ -529,11 +529,11 @@ void CHC::endVisit(FunctionCall const& _funCall) break; case FunctionType::Kind::External: case FunctionType::Kind::BareStaticCall: + case FunctionType::Kind::BareCall: externalFunctionCall(_funCall); SMTEncoder::endVisit(_funCall); break; case FunctionType::Kind::DelegateCall: - case FunctionType::Kind::BareCall: case FunctionType::Kind::BareCallCode: case FunctionType::Kind::BareDelegateCall: case FunctionType::Kind::Creation: @@ -746,23 +746,29 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall) FunctionType const& funType = dynamic_cast(*_funCall.expression().annotation().type); auto kind = funType.kind(); - solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, ""); + solAssert( + kind == FunctionType::Kind::External || + kind == FunctionType::Kind::BareCall || + kind == FunctionType::Kind::BareStaticCall, + "" + ); + + bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall; solAssert(m_currentContract, ""); auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract); - if (!function) - return; - - for (auto var: function->returnParameters()) - m_context.variable(*var)->increaseIndex(); + if (function) + { + usesStaticCall |= function->stateMutability() == StateMutability::Pure || + function->stateMutability() == StateMutability::View; + for (auto var: function->returnParameters()) + m_context.variable(*var)->increaseIndex(); + } if (!m_currentFunction || m_currentFunction->isConstructor()) return; auto preCallState = vector{state().state()} + currentStateVariables(); - bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall || - function->stateMutability() == StateMutability::Pure || - function->stateMutability() == StateMutability::View; if (!usesStaticCall) { diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index c5a56ac80..8a3d11707 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -611,6 +611,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) break; case FunctionType::Kind::Internal: case FunctionType::Kind::BareStaticCall: + case FunctionType::Kind::BareCall: break; case FunctionType::Kind::KECCAK256: case FunctionType::Kind::ECRecover: @@ -653,7 +654,6 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) visitObjectCreation(_funCall); return; case FunctionType::Kind::DelegateCall: - case FunctionType::Kind::BareCall: case FunctionType::Kind::BareCallCode: case FunctionType::Kind::BareDelegateCall: case FunctionType::Kind::Creation: diff --git a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol index 9c235a28a..c3ce9050e 100644 --- a/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol +++ b/test/libsolidity/smtCheckerTests/complex/slither/external_function.sol @@ -84,9 +84,7 @@ contract InternalCall { // Warning 2018: (1179-1241): Function state mutability can be restricted to pure // Warning 2018: (1247-1309): Function state mutability can be restricted to pure // Warning 4588: (681-716): Assertion checker does not yet implement this type of function call. -// Warning 4588: (727-782): Assertion checker does not yet implement this type of function call. // Warning 4588: (854-886): Assertion checker does not yet implement this type of function call. // Warning 4588: (681-716): Assertion checker does not yet implement this type of function call. -// Warning 4588: (727-782): Assertion checker does not yet implement this type of function call. // Warning 4588: (854-886): Assertion checker does not yet implement this type of function call. // Warning 5729: (1370-1375): BMC does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_constructor_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_constructor_1.sol new file mode 100644 index 000000000..a4dd5f531 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_constructor_1.sol @@ -0,0 +1,11 @@ +contract C { + uint x; + constructor(address _a) { + _a.call("aaaa"); + assert(x == 0); // should hold + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 9302: (51-66): Return value of low-level calls not used. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_constructor_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_constructor_2.sol new file mode 100644 index 000000000..2d2f32acf --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_constructor_2.sol @@ -0,0 +1,14 @@ +contract C { + uint x; + function f(uint _x) public { + x = _x; + } + constructor(address _a) { + _a.call("aaaa"); + assert(x == 0); // should hold + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 9302: (94-109): Return value of low-level calls not used. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol new file mode 100644 index 000000000..4352a7e95 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_mutex.sol @@ -0,0 +1,25 @@ +contract C { + uint x; + + bool lock; + modifier mutex { + require(!lock); + lock = true; + _; + lock = false; + } + + function set(uint _x) mutex public { + x = _x; + } + + function f(address _a) mutex public { + uint y = x; + _a.call("aaaaa"); + assert(y == x); // should hold + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 9302: (218-234): Return value of low-level calls not used. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol new file mode 100644 index 000000000..f53178198 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_mutex_unsafe.sol @@ -0,0 +1,26 @@ +contract C { + uint x; + + bool lock; + modifier mutex { + require(!lock); + lock = true; + _; + lock = false; + } + + function set(uint _x) mutex public { + x = _x; + } + + function f(address _a) public { + uint y = x; + _a.call("aaaaa"); + assert(y == x); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 9302: (212-228): Return value of low-level calls not used. +// 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 diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_1.sol new file mode 100644 index 000000000..b2730d2a3 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_1.sol @@ -0,0 +1,17 @@ +contract C { + uint x; + function s(uint _x) public { + x = _x; + } + function f(address a) public { + (bool s, bytes memory data) = a.call(""); + assert(x == 0); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 2519: (100-106): This declaration shadows an existing declaration. +// Warning 2072: (100-106): Unused local variable. +// Warning 2072: (108-125): Unused local variable. +// 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 diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol new file mode 100644 index 000000000..69c2e2953 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_reentrancy_view.sol @@ -0,0 +1,16 @@ +contract C { + uint x; + function s(uint _x) public view { + x == _x; + } + function f(address a) public { + (bool s, bytes memory data) = a.call(""); + assert(x == 0); // should hold + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 2519: (106-112): This declaration shadows an existing declaration. +// Warning 2072: (106-112): Unused local variable. +// Warning 2072: (114-131): Unused local variable. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_return_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_return_1.sol new file mode 100644 index 000000000..127d9f242 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_return_1.sol @@ -0,0 +1,15 @@ +contract C { + uint x; + function f(address a) public { + (bool s, bytes memory data) = a.call(""); + assert(s); // should fail + assert(!s); // should fail + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 2072: (65-82): Unused local variable. +// Warning 6328: (100-109): CHC: Assertion violation happens here. +// Warning 6328: (128-138): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_return_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_return_2.sol new file mode 100644 index 000000000..a9ae1d473 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_return_2.sol @@ -0,0 +1,13 @@ +contract C { + uint x; + function f(address a) public { + (bool s, bytes memory data) = a.call(""); + assert(data.length > 10); // should fail + } +} +// ==== +// SMTEngine: all +// SMTIgnoreCex: yes +// ---- +// Warning 2072: (57-63): Unused local variable. +// Warning 6328: (100-124): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_safe.sol b/test/libsolidity/smtCheckerTests/external_calls/call_safe.sol new file mode 100644 index 000000000..33791dd0d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/call_safe.sol @@ -0,0 +1,12 @@ +contract C { + uint x; + function f(address a) public { + (bool s, bytes memory data) = a.call(""); + assert(x == 0); // should hold + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 2072: (57-63): Unused local variable. +// Warning 2072: (65-82): Unused local variable. diff --git a/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol new file mode 100644 index 000000000..30f4392c5 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex.sol @@ -0,0 +1,25 @@ +contract C { + uint x; + + bool lock; + modifier mutex { + require(!lock); + lock = true; + _; + lock = false; + } + + function set(uint _x) mutex public { + x = _x; + } + + function f(address _a) mutex public { + uint y = x; + _a.staticcall("aaaaa"); + assert(y == x); // should hold + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 9302: (218-240): Return value of low-level calls not used. diff --git a/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol new file mode 100644 index 000000000..bccf18caf --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/staticcall_mutex_2.sol @@ -0,0 +1,26 @@ +contract C { + uint x; + + bool lock; + modifier mutex { + require(!lock); + lock = true; + _; + lock = false; + } + + function set(uint _x) mutex public { + x = _x; + } + + function f(address _a) public { + uint y = x; + _a.staticcall("aaaaa"); + assert(y == x); // should hold + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 9302: (212-234): Return value of low-level calls not used. +// Warning 2018: (164-271): Function state mutability can be restricted to view diff --git a/test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol b/test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol new file mode 100644 index 000000000..96a73cb5d --- /dev/null +++ b/test/libsolidity/smtCheckerTests/external_calls/staticcall_reentrancy_view.sol @@ -0,0 +1,17 @@ +contract C { + uint x; + function s(uint _x) public view { + x == _x; + } + function f(address a) public { + (bool s, bytes memory data) = a.staticcall(""); + assert(x == 0); // should hold + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 2519: (106-112): This declaration shadows an existing declaration. +// Warning 2072: (106-112): Unused local variable. +// Warning 2072: (114-131): Unused local variable. +// Warning 2018: (72-188): Function state mutability can be restricted to view diff --git a/test/libsolidity/smtCheckerTests/file_level/new_operator.sol b/test/libsolidity/smtCheckerTests/file_level/new_operator.sol index 796227041..33a30cf0c 100644 --- a/test/libsolidity/smtCheckerTests/file_level/new_operator.sol +++ b/test/libsolidity/smtCheckerTests/file_level/new_operator.sol @@ -16,5 +16,5 @@ contract D { // ---- // Warning 4588: (78-85): Assertion checker does not yet implement this type of function call. // Warning 4588: (78-85): Assertion checker does not yet implement this type of function call. -// Warning 6328: (133-152): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n test() -- internal call +// Warning 6328: (133-152): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n test() -- internal call\n (new C()).x() -- untrusted external call // Warning 4588: (78-85): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/functions/getters/function.sol b/test/libsolidity/smtCheckerTests/functions/getters/function.sol index 44120b189..95680f13d 100644 --- a/test/libsolidity/smtCheckerTests/functions/getters/function.sol +++ b/test/libsolidity/smtCheckerTests/functions/getters/function.sol @@ -15,5 +15,5 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (152-170): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f() -// Warning 6328: (262-278): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f() +// Warning 6328: (152-170): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f()\n e() -- untrusted external call\n g() -- untrusted external call +// Warning 6328: (262-278): CHC: Assertion violation happens here.\nCounterexample:\ng = 0\ne = 0\n\nTransaction trace:\nC.constructor()\nState: g = 0\nC.f()\n e() -- untrusted external call\n g() -- untrusted external call\n e() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_external.sol b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_external.sol index f04c91d0a..1a70c0783 100644 --- a/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_external.sol +++ b/test/libsolidity/smtCheckerTests/typecast/function_type_to_function_type_external.sol @@ -6,4 +6,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (123-143): CHC: Assertion violation happens here.\nCounterexample:\n\ng = 0\nh = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0) +// Warning 6328: (123-143): CHC: Assertion violation happens here.\nCounterexample:\n\ng = 0\nh = 0\n\nTransaction trace:\nC.constructor()\nC.f(0, 0)\n g(2) -- untrusted external call\n h(2) -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/types/address_call.sol b/test/libsolidity/smtCheckerTests/types/address_call.sol index 7ccde10da..021c970a5 100644 --- a/test/libsolidity/smtCheckerTests/types/address_call.sol +++ b/test/libsolidity/smtCheckerTests/types/address_call.sol @@ -19,9 +19,4 @@ contract C // SMTIgnoreCex: yes // ---- // Warning 2072: (191-207): Unused local variable. -// Warning 4588: (211-223): Assertion checker does not yet implement this type of function call. // Warning 6328: (227-242): CHC: Assertion violation happens here. -// Warning 6328: (246-260): CHC: Assertion violation happens here. -// Warning 6328: (264-283): CHC: Assertion violation happens here. -// Warning 6328: (287-311): CHC: Assertion violation happens here. -// Warning 4588: (211-223): Assertion checker does not yet implement this type of function call. diff --git a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol index adf8bddf2..f1b128162 100644 --- a/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol +++ b/test/libsolidity/smtCheckerTests/types/tuple_extra_parens_7.sol @@ -12,5 +12,3 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 4588: (110-129): Assertion checker does not yet implement this type of function call. -// Warning 4588: (110-129): Assertion checker does not yet implement this type of function call.