Merge pull request #14269 from blishko/smtchecker-fix-analysis-external-calls

[SMTChecker] Remember verification targets from trusted external calls

Changelog.md

@@ -15,7 +15,7 @@ Compiler Features:
 Bugfixes:
  * Commandline Interface: It is no longer possible to specify both ``--optimize-yul`` and ``--no-optimize-yul`` at the same time.
  * SMTChecker: Fix encoding of side-effects inside ``if`` and ``ternary conditional``statements in the BMC engine.
-
+ * SMTChecker: Fix false negative when a verification target can be violated only by trusted external call from another public function.
 
 AST Changes:
  * AST: Add the ``experimentalSolidity`` field to the ``SourceUnit`` nodes, which indicate whether the experimental parsing mode has been enabled via ``pragma experimental solidity``.

libsolidity/formal/CHC.cpp

@@ -1000,6 +1000,12 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 	if (!function)
 		return;
 
+	// Remember the external call in the call graph to properly detect verification targets for the current function
+	if (m_currentFunction && !m_currentFunction->isConstructor())
+		m_callGraph[m_currentFunction].insert(function);
+	else
+		m_callGraph[m_currentContract].insert(function);
+
 	// External call creates a new transaction.
 	auto originalTx = state().tx();
 	Expression const* value = valueOption(callOptions);

test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol

@@ -21,11 +21,8 @@ contract C {
 // SMTIgnoreOS: macos
 // ----
 // Warning 4984: (47-50): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Warning 6328: (167-185): CHC: Assertion violation might happen here.
 // Warning 6328: (215-233): CHC: Assertion violation might happen here.
-// Warning 6328: (267-285): CHC: Assertion violation might happen here.
 // Warning 6328: (304-322): CHC: Assertion violation happens here.
+// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
 // Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4661: (167-185): BMC: Assertion violation happens here.
 // Warning 4661: (215-233): BMC: Assertion violation happens here.
-// Warning 4661: (267-285): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/external_calls/underflow_only_in_external_call.sol

@@ -0,0 +1,23 @@
+contract C {
+
+	uint v;
+	bool guard = true;
+
+	function dec() public returns (uint) {
+		if (guard) return 0;
+		--v;
+		return v;
+	}
+
+	function f() public returns (uint) {
+		guard = false;
+		uint ret = this.dec();
+		guard = true;
+		return ret;
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTTargets: underflow
+// ----
+// Warning 3944: (109-112): CHC: Underflow (resulting value less than 0) happens here.