[SMTChecker] Remember verification targets from trusted external calls

Previously, we did not remember trusted external calls for later phase
when we compute possible verification targets for each function.
This led to false negative in cases where verification target can be
violated, but not by calling a public function directly, but only when
it is called as an external function from other function.

The added test cases witnesses this behaviour. The underflow in
`dec` cannot happen in any other way except what the `dec` is called
from `f`.

The same problem did not occur when the functions are called internally,
because for such cases, we have already been remembering these calls in
the callgraph in the CHC engine.

Changelog.md

@@ -11,7 +11,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.