Merge pull request #8624 from ethereum/smt_fix_internal_call_chc

[SMTChecker] Fix ICE in CHC internal calls

Changelog.md

@@ -7,6 +7,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix internal error in the CHC engine when calling inherited functions internally.
 
 
 

libsolidity/formal/CHC.cpp

@@ -961,7 +961,11 @@ smt::Expression CHC::predicate(FunctionCall const& _funCall)
 	for (auto const& var: function->returnParameters())
 		args.push_back(m_context.variable(*var)->currentValue());
 
-	return (*m_summaries.at(contract).at(function))(args);
+	if (contract->isLibrary())
+		return (*m_summaries.at(contract).at(function))(args);
+
+	solAssert(m_currentContract, "");
+	return (*m_summaries.at(m_currentContract).at(function))(args);
 }
 
 void CHC::addRule(smt::Expression const& _rule, string const& _ruleName)

test/libsolidity/smtCheckerTests/functions/internal_call_inheritance.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function c() public pure returns (uint) { return 42; }
+}
+
+contract B is C {
+	function b() public pure returns (uint) { return c(); }
+}
+
+contract A is B {
+	uint public x;
+
+	function a() public {
+		x = b();
+		assert(x < 40);
+	}
+}
+// ----
+// Warning: (254-268): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/internal_call_inheritance_2.sol

@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint y;
+	function c(uint _y) public returns (uint) {
+		y = _y;
+		return y;
+	}
+}
+
+contract B is C {
+	function b() public returns (uint) { return c(42); }
+}
+
+contract A is B {
+	uint public x;
+
+	function a() public {
+		x = b();
+		assert(x < 40);
+	}
+}
+// ----
+// Warning: (274-288): Assertion violation happens here