Merge pull request #13974 from blishko/chc-path-condition

[SMTChecker] Use path condition in CHC engine

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.
+// Info 1391: CHC: 2 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.
 // 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: 4 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
-// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.