diff --git a/Changelog.md b/Changelog.md index 7e35275bc..531ded9a5 100644 --- a/Changelog.md +++ b/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: diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp index 3d93bf599..c6e737dbe 100644 --- a/libsolidity/formal/CHC.cpp +++ b/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); diff --git a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json b/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json index 85a221d4c..bf59a0d9d 100644 --- a/test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json +++ b/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 diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol index 1a87e1ced..32d5435d3 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/ternary_operator_1.sol b/test/libsolidity/smtCheckerTests/operators/ternary_operator_1.sol new file mode 100644 index 000000000..ce475d91b --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/ternary_operator_2.sol b/test/libsolidity/smtCheckerTests/operators/ternary_operator_2.sol new file mode 100644 index 000000000..3f2e42efd --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/ternary_operator_3.sol b/test/libsolidity/smtCheckerTests/operators/ternary_operator_3.sol new file mode 100644 index 000000000..dac62d380 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/ternary_operator_double_function_call.sol b/test/libsolidity/smtCheckerTests/operators/ternary_operator_double_function_call.sol new file mode 100644 index 000000000..96d00ff60 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/ternary_operator_external_code_1.sol b/test/libsolidity/smtCheckerTests/operators/ternary_operator_external_code_1.sol new file mode 100644 index 000000000..7da04b464 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_1.sol b/test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_1.sol new file mode 100644 index 000000000..d2722fc04 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_2.sol b/test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_2.sol new file mode 100644 index 000000000..71e294fb4 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_3.sol b/test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_3.sol new file mode 100644 index 000000000..0638e4838 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_4.sol b/test/libsolidity/smtCheckerTests/operators/ternary_operator_nested_4.sol new file mode 100644 index 000000000..295590228 --- /dev/null +++ b/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. diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol index fce586987..5ac20c96f 100644 --- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol +++ b/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.