Merge pull request #11820 from ethereum/smt_barecall

[SMTChecker] CALL

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:

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<FunctionType const&>(*_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<smtutil::Expression>{state().state()} + currentStateVariables();
-	bool usesStaticCall = kind == FunctionType::Kind::BareStaticCall ||
-		function->stateMutability() == StateMutability::Pure ||
-		function->stateMutability() == StateMutability::View;
 
 	if (!usesStaticCall)
 	{

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:

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.

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.

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.

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.

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

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

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.

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.

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.

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.

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.

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

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

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.

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

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

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.

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.