[SMTChecker] Use path condition when creating CHC targets

Without path condition, verification targets created inside ternary
operator ignore the condition of the operator inside the branches.
This led to false positives.

Further updates:

- Function calls should consider the conditions under which they are
called, otherwise the analysis may report false positives.
The fix proposed here is to add the current path condition to the edge
that propagates error from a function call.

- Increment error index after function call

This is necessary for the analysis of the ternary operator to work
correctly. No information should leak from a function call inside a
ternary operator in the first branch to the second branch, including
whether or not an error would have occured in the first branch.

However, for the execution that continues after the function call,
we still need to ensure that under the current path condition
the error has not occurred in that function call.

It would be better to isolate the analysis of the branches to separate
clauses, but I do not see an easy way for that now. In this way, even
though the function call in first branch is included in the clause of
the second branch, no information leaks.

- Additonal test for ternary operator

This tests the behaviour of SMTChecker on ternary operator with function
calls inside both branches. Specifically, it tests that SMTChecker
successfully detects a violation of a verification target in the second
branch when the same target is present also in the first branch, but
there it cannot be triggered because of the operator's condition.

Changelog.md

@@ -19,6 +19,7 @@ Bugfixes:
  * Antlr Grammar: Fix discrepancy with the parser, which allowed octal numbers.
  * Antlr Grammar: Fix of a discrepancy with the parser, which allowed numbers followed by an identifier with no whitespace.
  * Antlr Grammar: Stricter rules for function definitions. The grammar will no longer accept as valid free functions having specifiers which are exclusive to contract functions.
+ * SMTChecker: Fix false positives in ternary operators that contain verification targets in its branches, directly or indirectly.
 
 
 AST Changes:

libsolidity/formal/CHC.cpp

@@ -839,9 +839,10 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 	connectBlocks(
 		m_currentBlock,
 		predicate(*m_errorDest),
-		errorFlag().currentValue() > 0
+		errorFlag().currentValue() > 0 && currentPathConditions()
 	);
-	m_context.addAssertion(errorFlag().currentValue() == 0);
+	m_context.addAssertion(smtutil::Expression::implies(currentPathConditions(), errorFlag().currentValue() == 0));
+	m_context.addAssertion(errorFlag().increaseIndex() == 0);
 }
 
 void CHC::addNondetCalls(ContractDefinition const& _contract)
@@ -970,7 +971,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 
 	m_context.addAssertion(nondetCall);
 	solAssert(m_errorDest, "");
-	connectBlocks(m_currentBlock, predicate(*m_errorDest), errorFlag().currentValue() > 0);
+	connectBlocks(m_currentBlock, predicate(*m_errorDest), errorFlag().currentValue() > 0 && currentPathConditions());
 
 	// 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.
@@ -1866,6 +1867,7 @@ void CHC::verificationTargetEncountered(
 		m_functionTargetIds[m_currentContract].push_back(errorId);
 	auto previousError = errorFlag().currentValue();
 	errorFlag().increaseIndex();
+	auto extendedErrorCondition = currentPathConditions() && _errorCondition;
 
 	Predicate const* localBlock = m_currentFunction ?
 		createBlock(m_currentFunction, PredicateType::FunctionErrorBlock) :
@@ -1875,7 +1877,7 @@ void CHC::verificationTargetEncountered(
 	connectBlocks(
 		m_currentBlock,
 		pred,
-		_errorCondition && errorFlag().currentValue() == errorId
+		extendedErrorCondition && errorFlag().currentValue() == errorId
 	);
 	solAssert(m_errorDest, "");
 	addRule(smtutil::Expression::implies(pred, predicate(*m_errorDest)), pred.name);

test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json

@@ -30,7 +30,7 @@
 (check-sat)
 (get-value (|EVALEXPR_0| ))
 ",
-            "0xfb06d3f02a20bd362abded9ab80638bdc9dd43ccbf644517f3006206c0c47f67": "(set-logic HORN)
+            "0xa991e3c158410479bc0a0540fb60ce7010aec315a5b0010d254f12f3d1f0a4e5": "(set-logic HORN)
 
 (declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
 (declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.prevrandao| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int)))))
@@ -69,7 +69,7 @@
 (declare-fun |block_8_function_f__13_14_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int ) Bool)
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int))
-(=> (and (and (block_6_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))))) (and (not expr_9_1) (= error_1 1))) (block_8_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
+(=> (and (and (block_6_f_12_14_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1) (and (= expr_9_1 (> expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 0) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 x_3_1) (and (and (>= x_3_1 0) (<= x_3_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))))))) (and (and true (not expr_9_1)) (= error_1 1))) (block_8_function_f__13_14_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 x_3_0 state_1 x_3_1))))
 
 
 (assert

test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol

@@ -14,8 +14,6 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 4984: (134-140): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (143-146): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
-// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Warning 2661: (134-140): BMC: Overflow (resulting value larger than 2**256 - 1) 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: (143-146): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/operators/ternary_operator_1.sol

@@ -0,0 +1,9 @@
+contract C {
+	function f(uint x) public pure returns (uint) {
+		return x > 0 ? x - 1 : 0; // Underflow cannot happen
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/operators/ternary_operator_2.sol

@@ -0,0 +1,14 @@
+contract C {
+
+	function decrement(uint x) private pure returns (uint) {
+		return x - 1; // No underflow, the method can be called only with positive value
+	}
+
+	function f(uint x) public pure returns (uint) {
+		return x > 0 ? decrement(x) : 0;
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/operators/ternary_operator_3.sol

@@ -0,0 +1,31 @@
+abstract contract D {
+	function d() external virtual returns (uint);
+}
+
+contract C {
+
+	D d;
+	uint v;
+	bool guard = true;
+
+	function inc() public {
+		++v;
+	}
+
+	function dec() public {
+		if (guard) return;
+		--v;
+	}
+
+	function f() public returns (uint) {
+		guard = false;
+		uint ret = v > 0 ? d.d() : 0;
+		guard = true;
+		return ret;
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTTargets: underflow
+// ----
+// Warning 3944: (206-209): CHC: Underflow (resulting value less than 0) happens here.

test/libsolidity/smtCheckerTests/operators/ternary_operator_double_function_call.sol

@@ -0,0 +1,4 @@
+contract C { function decrement(uint x) private pure returns (uint) { return x - 1; } function decrement2(uint x) private pure returns (uint) { return x - 1; } function f(uint x) public pure returns (uint) { return x > 0 ? decrement(x) : decrement2(x); } }
+// ----
+// Warning 3944: (151-156): CHC: Underflow (resulting value less than 0) happens here.
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/operators/ternary_operator_external_code_1.sol

@@ -0,0 +1,32 @@
+abstract contract D {
+	function d() external virtual returns (uint);
+}
+
+contract C {
+
+	D d;
+	uint v;
+	bool guard = true;
+
+	function inc() public {
+		++v;
+	}
+
+	function dec() public {
+		if (guard) return;
+		--v;
+		guard = true;
+	}
+
+	function f() public returns (uint) {
+		guard = false;
+		uint ret = v > 0 ? d.d() : 0;
+		guard = true;
+		return ret;
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTTargets: underflow
+// ----
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_1.sol

@@ -0,0 +1,15 @@
+contract C {
+
+	function unreachable() private pure returns (uint) {
+		assert(false);
+		return 0;
+	}
+
+	function f(uint x) public pure returns (uint) {
+		return x <= 1 ? 0 : x < 2 ? unreachable() : 0;
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_2.sol

@@ -0,0 +1,27 @@
+contract C {
+
+	function decrement(uint x) private pure returns (uint) {
+		return x - 1;
+	}
+
+	function decrement2(uint x) private pure returns (uint) {
+		return x - 1;
+	}
+
+	function increment(uint x) private pure returns (uint) {
+		return x + 1;
+	}
+
+	function increment2(uint x) private pure returns (uint) {
+		return x + 1;
+	}
+
+	function f(uint x) public pure returns (uint) {
+		return x < 10 ? (x > 0 ? decrement(x) : increment(x)) : (x > 100 ? increment2(x) : decrement2(x));
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 4984: (317-322): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_3.sol

@@ -0,0 +1,19 @@
+contract C {
+
+	function increment(uint x) private pure returns (uint) {
+		return x + 1;
+	}
+
+	function increment2(uint x) private pure returns (uint) {
+		return x + 1;
+	}
+
+	function f(uint x) public pure returns (uint) {
+		return x < 10 ? (x > 0 ? 0 : increment(x)) : (x > 100 ? increment2(x) : 0);
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_4.sol

@@ -0,0 +1,24 @@
+contract C {
+
+	uint s = 1;
+
+	function decrement() private returns (uint) {
+		return --s;
+	}
+
+	function increment() private returns (uint) {
+		return ++s;
+	}
+
+	function f(uint x) public returns (uint) {
+		require(s > 0 && s < 10);
+		uint olds = s;
+		uint ret = x < 1 ? increment() : decrement();
+		assert(s != olds);
+		return ret;
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol

@@ -45,5 +45,4 @@ contract C
 // Warning 6368: (850-866): CHC: Out of bounds access happens here.
 // Warning 6368: (850-869): CHC: Out of bounds access happens here.
 // Warning 6328: (936-956): CHC: Assertion violation happens here.
-// Warning 6368: (1029-1043): CHC: Out of bounds access might happen here.
-// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
+// Info 1391: CHC: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.