Merge pull request #11795 from ethereum/smt_fix_ext_constructor

[SMTChecker] Fix false positive on external calls from constructors

Author: Leonardo

Changelog.md

@@ -7,6 +7,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix false positive in external calls from constructors.
 
 
 

libsolidity/formal/CHC.cpp

@@ -756,6 +756,9 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	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 ||
@@ -787,6 +790,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	m_context.addAssertion(nondetCall);
 	solAssert(m_errorDest, "");
 	connectBlocks(m_currentBlock, predicate(*m_errorDest), errorFlag().currentValue() > 0);
+
 	// To capture the possibility of a reentrant call, we record in the call graph that the  current function
 	// can call any of the external methods of the current contract.
 	if (m_currentFunction)

test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol

@@ -16,4 +16,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
-// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()
+// Warning 6328: (177-191): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()

test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol

@@ -20,4 +20,4 @@ contract C {
 // SMTEngine: all
 // ----
 // Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100)
-// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f()
+// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()

test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_reentrancy_1.sol

@@ -0,0 +1,15 @@
+interface D {
+	function ext(C c) external returns (uint);
+}
+
+contract C {
+	uint x;
+	function s(uint _x) public { x = _x; }
+	constructor(D d) {
+		uint a = d.ext(this);
+		assert(x == 0); // should hold because there's no reentrancy from the constructor
+		assert(a == 2); // should fail
+	}
+}
+// ----
+// Warning 6328: (253-267): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\nd = 0\na = 3\n\nTransaction trace:\nC.constructor(0)