Merge pull request #11467 from ethereum/smt_fix_external_call_from_constructor

[SMTChecker] Fix ICE on external calls from constructor

Changelog.md

@@ -17,6 +17,7 @@ Compiler Features:
 Bugfixes:
  * AST: Do not output value of Yul literal if it is not a valid UTF-8 string.
  * SMTChecker: Fix internal error on struct constructor with fixed bytes member initialized with string literal.
+ * SMTChecker: Fix internal error on external calls from the constructor.
  * Source Locations: Properly set source location of scoped blocks.
  * Standard JSON: Properly allow the ``inliner`` setting under ``settings.optimizer.details``.
  * Type Checker: Fix internal compiler error related to having mapping types in constructor parameter for abstract contracts.

libsolidity/formal/CHC.cpp

@@ -773,7 +773,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	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.
-	solAssert(m_currentContract && m_currentFunction, "");
+	if (m_currentFunction)
 		for (auto const* definedFunction: contractFunctions(*m_currentContract))
 			if (!definedFunction->isConstructor() && definedFunction->isPublic())
 				m_callGraph[m_currentFunction].insert(definedFunction);
@@ -788,7 +788,6 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 	auto kind = funType.kind();
 	solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
-	solAssert(m_currentContract, "");
 	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
 	if (!function)
 		return;

test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_1.sol

@@ -0,0 +1,19 @@
+contract State {
+	function f(uint _x) public pure returns (uint) {
+		assert(_x < 100);
+		return _x;
+	}
+}
+contract C {
+	State s;
+	uint z = s.f(2);
+
+	function f() public view {
+		assert(z == 2); // should fail since we don't trust s.f's code
+	}
+}
+// ====
+// 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()

test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_2.sol

@@ -0,0 +1,16 @@
+contract C {
+	uint z = this.g(2);
+
+	function g(uint _x) public pure returns (uint) {
+		assert(_x > 0);
+		return _x;
+	}
+
+	function f() public view {
+		assert(z == 2); // should fail since we don't trust s.f's code
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (87-101): CHC: Assertion violation happens here.\nCounterexample:\nz = 2\n_x = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: z = 2\nC.g(0)

test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol

@@ -0,0 +1,23 @@
+contract State {
+	function f(uint _x) public pure returns (uint) {
+		assert(_x < 100);
+		return _x;
+	}
+}
+contract C {
+	State s;
+	uint z;
+
+	constructor() {
+		z = s.f(2);
+	}
+
+	function f() public view {
+		assert(z == 2); // should fail since we don't trust s.f's code
+	}
+}
+// ====
+// 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 = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f()