From 8927015e5a06d273b4ba82c69fa553959e8bb5db Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Thu, 10 Dec 2020 16:51:10 +0100 Subject: [PATCH] [SMTChecker] Adding unary increment and decrement as under/overflow verification targets for the CHC engine --- Changelog.md | 1 + libsolidity/formal/BMC.cpp | 17 +---------- libsolidity/formal/SMTEncoder.cpp | 16 +++++++++-- .../array_members/pop_loop_safe.sol | 2 ++ .../array_members/pop_loop_unsafe.sol | 1 + ...overflow_2_safe_no_overflow_assumption.sol | 2 ++ .../unary_add_minus_overflow_detected.sol | 28 +++++++++++++++++++ .../smtCheckerTests/control_flow/return_1.sol | 1 - .../control_flow/return_1_fail.sol | 1 - .../smtCheckerTests/control_flow/return_2.sol | 1 - .../control_flow/return_2_fail.sol | 1 - .../external_calls/external_inc.sol | 1 + .../external_calls/external_safe.sol | 3 ++ .../internal_call_with_assertion_1.sol | 2 -- .../internal_call_with_assertion_1_fail.sol | 2 -- ...rnal_call_with_assertion_inheritance_1.sol | 2 -- ...call_with_assertion_inheritance_1_fail.sol | 2 -- ...ternal_multiple_calls_with_assertion_1.sol | 4 --- ...l_multiple_calls_with_assertion_1_fail.sol | 4 --- .../smtCheckerTests/imports/import_base.sol | 1 + .../smtCheckerTests/invariants/loop_basic.sol | 2 ++ .../invariants/loop_basic_for.sol | 2 ++ .../loops/while_2_break_fail.sol | 2 +- ...le_loop_array_assignment_memory_memory.sol | 3 +- ...e_loop_array_assignment_memory_storage.sol | 1 + ..._loop_array_assignment_storage_storage.sol | 1 + .../assignment_contract_member_variable.sol | 7 +++-- .../operators/conditional_assignment_3.sol | 2 +- .../conditional_assignment_statevar_1.sol | 3 ++ .../operators/unary_add_array.sol | 2 +- .../operators/unary_add_mapping.sol | 4 ++- .../unary_add_minus_overflow_detected.sol | 25 +++++++++++++++++ .../unary_add_overflows_correctly.sol | 16 +++++++++++ .../unary_add_overflows_correctly_struct.sol | 24 ++++++++++++++++ .../operators/unary_sub_array.sol | 2 +- .../operators/unary_sub_mapping.sol | 2 +- .../types/struct/struct_recursive_6.sol | 12 +++----- .../types/struct/struct_unary_add.sol | 2 +- .../types/struct/struct_unary_sub.sol | 2 +- .../smtCheckerTests/types/unused_mapping.sol | 3 +- 40 files changed, 150 insertions(+), 59 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/bmc_coverage/unary_add_minus_overflow_detected.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/unary_add_minus_overflow_detected.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly.sol create mode 100644 test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly_struct.sol diff --git a/Changelog.md b/Changelog.md index 10944f1be..fa01287e4 100644 --- a/Changelog.md +++ b/Changelog.md @@ -14,6 +14,7 @@ Compiler Features: * SMTChecker: Support getters. * SMTChecker: Support named arguments in function calls. * SMTChecker: Support struct constructor. + * SMTChecker: Create underflow and overflow verification targets for increment/decrement in the CHC engine. * Standard-Json: Move the recently introduced ``modelCheckerSettings`` key to ``settings.modelChecker``. * Standard-Json: Properly filter the requested output artifacts. diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp index 1b47a24f5..393aa1022 100644 --- a/libsolidity/formal/BMC.cpp +++ b/libsolidity/formal/BMC.cpp @@ -356,27 +356,12 @@ void BMC::endVisit(UnaryOperation const& _op) ) return; - switch (_op.getOperator()) - { - case Token::Inc: // ++ (pre- or postfix) - case Token::Dec: // -- (pre- or postfix) + if (_op.getOperator() == Token::Sub && smt::isInteger(*_op.annotation().type)) addVerificationTarget( VerificationTarget::Type::UnderOverflow, expr(_op), &_op ); - break; - case Token::Sub: // - - if (_op.annotation().type->category() == Type::Category::Integer) - addVerificationTarget( - VerificationTarget::Type::UnderOverflow, - expr(_op), - &_op - ); - break; - default: - break; - } } void BMC::endVisit(FunctionCall const& _funCall) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index c704e5ab1..be67326c3 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -512,7 +512,13 @@ void SMTEncoder::endVisit(UnaryOperation const& _op) auto decl = identifierToVariable(*identifier); solAssert(decl, ""); auto innerValue = currentValue(*decl); - auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1; + auto newValue = arithmeticOperation( + _op.getOperator() == Token::Inc ? Token::Add : Token::Sub, + innerValue, + smtutil::Expression(size_t(1)), + _op.annotation().type, + _op + ).first; defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue); assignment(*decl, newValue); } @@ -522,7 +528,13 @@ void SMTEncoder::endVisit(UnaryOperation const& _op) ) { auto innerValue = expr(*subExpr); - auto newValue = _op.getOperator() == Token::Inc ? innerValue + 1 : innerValue - 1; + auto newValue = arithmeticOperation( + _op.getOperator() == Token::Inc ? Token::Add : Token::Sub, + innerValue, + smtutil::Expression(size_t(1)), + _op.annotation().type, + _op + ).first; defineExpr(_op, _op.isPrefixOperation() ? newValue : innerValue); indexOrMemberAssignment(*subExpr, newValue); } diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol index 25986da7b..4626a7d08 100644 --- a/test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol +++ b/test/libsolidity/smtCheckerTests/array_members/pop_loop_safe.sol @@ -9,3 +9,5 @@ contract C { } } } +// ---- +// Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. diff --git a/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol b/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol index 3151df0dc..deac0b2c9 100644 --- a/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol +++ b/test/libsolidity/smtCheckerTests/array_members/pop_loop_unsafe.sol @@ -11,4 +11,5 @@ contract C { } } // ---- +// Warning 4984: (112-115): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 2529: (150-157): CHC: Empty array "pop" happens here.\nCounterexample:\na = []\nl = 0\n\n\nTransaction trace:\nconstructor()\nState: a = []\nf(0) diff --git a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol index 1f468f592..21c96a7bd 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_overflow_2_safe_no_overflow_assumption.sol @@ -11,3 +11,5 @@ contract C { assert(x[0] == 42); } } +// ---- +// Warning 4984: (174-177): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/unary_add_minus_overflow_detected.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/unary_add_minus_overflow_detected.sol new file mode 100644 index 000000000..9d375fd58 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/bmc_coverage/unary_add_minus_overflow_detected.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; +contract C { + uint8 x; + + function inc_pre() public { + ++x; + } + + function dec_pre() public { + --x; + } + + /* Commented out because Spacer segfaults in Z3 4.8.9 + function inc_post() public { + x++; + } + + function dec_post() public { + x--; + } + */ + +} +// ==== +// SMTEngine: bmc +// ---- +// Warning 2661: (87-90): BMC: Overflow (resulting value larger than 255) happens here. +// Warning 4144: (127-130): BMC: Underflow (resulting value less than 0) happens here. diff --git a/test/libsolidity/smtCheckerTests/control_flow/return_1.sol b/test/libsolidity/smtCheckerTests/control_flow/return_1.sol index 881ec7cc0..3dabd2fef 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/return_1.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/return_1.sol @@ -19,4 +19,3 @@ contract C { } } // ---- -// Warning 2661: (158-161): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/control_flow/return_1_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/return_1_fail.sol index 21c655980..02b88c981 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/return_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/return_1_fail.sol @@ -23,4 +23,3 @@ contract C { // Warning 6328: (274-300): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() // Warning 6328: (304-330): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() // Warning 6328: (334-362): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() -// Warning 2661: (158-161): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/control_flow/return_2.sol b/test/libsolidity/smtCheckerTests/control_flow/return_2.sol index ec3546e4f..c6005bb08 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/return_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/return_2.sol @@ -28,4 +28,3 @@ contract C { } } // ---- -// Warning 2661: (188-191): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/control_flow/return_2_fail.sol b/test/libsolidity/smtCheckerTests/control_flow/return_2_fail.sol index 8ec948345..34c798a2a 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/return_2_fail.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/return_2_fail.sol @@ -38,4 +38,3 @@ contract C { // Warning 6328: (437-458): CHC: Assertion violation happens here. // Warning 6328: (462-490): CHC: Assertion violation happens here. // Warning 6328: (494-517): CHC: Assertion violation happens here. -// Warning 2661: (188-191): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol index 9f6ce11a8..412456cd4 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_inc.sol @@ -18,5 +18,6 @@ contract C { } } // ---- +// Warning 4984: (146-149): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 6328: (189-203): CHC: Assertion violation happens here.\nCounterexample:\nx = 10, d = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, d = 0\ninc()\nState: x = 1, d = 0\nf() // Warning 2661: (146-149): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol index 6a2b66491..aa4a8a6c1 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_safe.sol @@ -16,3 +16,6 @@ contract C { assert(x < 11); } } +// ---- +// Warning 6328: (200-214): CHC: Assertion violation might happen here. +// Warning 4661: (200-214): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol index dba4f11ee..52dcfb1ff 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1.sol @@ -21,5 +21,3 @@ contract C{ } // ---- // Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning. -// Warning 2661: (156-159): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4144: (238-241): BMC: Underflow (resulting value less than 0) happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol index dae611717..a1e245fd9 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_1_fail.sol @@ -26,5 +26,3 @@ contract C{ // Warning 6328: (220-234): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\n\n\nTransaction trace:\nconstructor(0)\nState: x = 1\nf() // Warning 6328: (245-259): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor(0)\nState: x = 1\nf() // Warning 6328: (82-96): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor(0) -// Warning 2661: (156-159): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4144: (238-241): BMC: Underflow (resulting value less than 0) happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1.sol index 19a1ceb2f..80f6d6304 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1.sol @@ -17,5 +17,3 @@ contract C is A { } } // ---- -// Warning 4144: (100-103): BMC: Underflow (resulting value less than 0) happens here. -// Warning 4144: (100-103): BMC: Underflow (resulting value less than 0) happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1_fail.sol index 303f72504..3052258fc 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_call_with_assertion_inheritance_1_fail.sol @@ -20,5 +20,3 @@ contract C is A { // Warning 6328: (82-96): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor() // Warning 6328: (148-162): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor() // Warning 6328: (180-194): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor() -// Warning 4144: (100-103): BMC: Underflow (resulting value less than 0) happens here. -// Warning 4144: (100-103): BMC: Underflow (resulting value less than 0) happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol index ffb9d48cd..f23217cde 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1.sol @@ -21,7 +21,3 @@ contract C{ } // ---- // Warning 5667: (70-76): Unused function parameter. Remove or comment out the variable name to silence this warning. -// Warning 2661: (156-159): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 2661: (163-166): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 2661: (234-237): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4144: (234-237): BMC: Underflow (resulting value less than 0) happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol index c606dd1cc..81ba33295 100644 --- a/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol +++ b/test/libsolidity/smtCheckerTests/functions/internal_multiple_calls_with_assertion_1_fail.sol @@ -24,7 +24,3 @@ contract C{ // Warning 6328: (138-152): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor(0)\nState: x = 1\nf() // Warning 6328: (184-198): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\n\n\nTransaction trace:\nconstructor(0)\nState: x = 1\nf() // Warning 6328: (82-96): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\ny = 0\n\n\nTransaction trace:\nconstructor(0) -// Warning 2661: (156-159): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 2661: (163-166): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 2661: (234-237): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4144: (234-237): BMC: Underflow (resulting value less than 0) happens here. diff --git a/test/libsolidity/smtCheckerTests/imports/import_base.sol b/test/libsolidity/smtCheckerTests/imports/import_base.sol index f02265c75..223365c5a 100644 --- a/test/libsolidity/smtCheckerTests/imports/import_base.sol +++ b/test/libsolidity/smtCheckerTests/imports/import_base.sol @@ -20,6 +20,7 @@ contract Der is Base { // ---- // Warning 4984: (der:101-109): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 6328: (der:113-126): CHC: Assertion violation happens here.\nCounterexample:\nx = 3, a = 0\ny = 0\n\n\nTransaction trace:\nconstructor()\nState: x = 0, a = 0\ng(0) +// Warning 4984: (base:100-103): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 2661: (base:100-103): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (der:101-109): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (base:100-103): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol b/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol index d24b19e1e..98d1ea384 100644 --- a/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol +++ b/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol @@ -11,3 +11,5 @@ contract Simple { } // ==== // SMTSolvers: z3 +// ---- +// Warning 4984: (132-135): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. diff --git a/test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol b/test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol index 3e059b516..bc3814ccc 100644 --- a/test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol +++ b/test/libsolidity/smtCheckerTests/invariants/loop_basic_for.sol @@ -9,3 +9,5 @@ contract Simple { } // ==== // SMTSolvers: z3 +// ---- +// Warning 4984: (116-119): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. diff --git a/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol index 0012c9c7b..88ade1cd4 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_2_break_fail.sol @@ -15,4 +15,4 @@ contract C // SMTSolvers: z3 // ---- // Warning 5740: (120-123): Unreachable code. -// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 1\n\n\nTransaction trace:\nconstructor()\nf(1) +// Warning 6328: (131-145): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 3\n\n\nTransaction trace:\nconstructor()\nf(3) diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol index aeba1381b..3ea615a2a 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_memory.sol @@ -18,9 +18,10 @@ contract LoopFor2 { } } // ==== -// SMTSolvers: z3 // SMTIgnoreCex: yes +// SMTSolvers: z3 // ---- // Warning 4984: (244-249): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 4984: (270-273): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 6328: (373-392): CHC: Assertion violation happens here. // Warning 6328: (396-415): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol index 29509fc5c..e37bf2dbf 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_memory_storage.sol @@ -26,3 +26,4 @@ contract LoopFor2 { // SMTSolvers: z3 // ---- // Warning 4984: (237-242): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 4984: (263-266): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. diff --git a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol index 47137aec5..2aae73453 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol @@ -21,5 +21,6 @@ contract LoopFor2 { } // ---- // Warning 4984: (229-234): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. +// Warning 4984: (255-258): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 6328: (338-357): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1) // Warning 6328: (361-380): CHC: Assertion violation happens here.\nCounterexample:\nb = [], c = []\nn = 1\n\n\nTransaction trace:\nconstructor()\nState: b = [], c = []\ntestUnboundedForLoop(1) diff --git a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol index ae8725b54..b0b16783b 100644 --- a/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol +++ b/test/libsolidity/smtCheckerTests/operators/assignment_contract_member_variable.sol @@ -7,7 +7,7 @@ contract A { A.y = A.x++; assert(A.y == A.x - 1); // Fails - assert(A.y == 0); + // assert(A.y == 0); // Disabled because of nondeterminism in Spacer A.y = ++A.x; assert(A.y == A.x); delete A.x; @@ -25,6 +25,7 @@ contract A { assert(A.y == A.x); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (160-176): CHC: Assertion violation happens here.\nCounterexample:\nx = (- 1), y = (- 2)\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, y = 0\na()\nState: x = (- 2), y = (- 2)\na() -// Warning 6328: (373-389): CHC: Assertion violation happens here.\nCounterexample:\nx = 8, y = (- 2)\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0, y = 0\na() +// Warning 6328: (424-440): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_3.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_3.sol index 88da0e05a..e8a400493 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_3.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_3.sol @@ -10,4 +10,4 @@ contract C { } } // ---- -// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\na = 6\nb = 5\n\n\nTransaction trace:\nconstructor()\nf(5, 5) +// Warning 6328: (161-174): CHC: Assertion violation happens here.\nCounterexample:\n\na = 0\nb = 1\n\n\nTransaction trace:\nconstructor()\nf(0, 0) diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol index 3c402fceb..3df380fef 100644 --- a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol +++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol @@ -10,3 +10,6 @@ contract C { } } // ---- +// Warning 4984: (129-134): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935, b = false\n\nc = 0\n\nTransaction trace:\nconstructor()\nState: a = 0, b = false\nf()\nState: a = 115792089237316195423570985008687907853269984665640564039457584007913129639935, b = false\nf() +// Warning 3944: (137-140): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\na = 0, b = false\n\nc = 0\n\nTransaction trace:\nconstructor()\nState: a = 0, b = false\nf() +// Warning 6328: (150-163): CHC: Assertion violation happens here.\nCounterexample:\na = 115792089237316195423570985008687907853269984665640564039457584007913129639935, b = false\n\nc = 0\n\nTransaction trace:\nconstructor()\nState: a = 0, b = false\nf() diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_array.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_array.sol index d2685dc4b..401e4af62 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_add_array.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_array.sol @@ -15,4 +15,4 @@ contract C } } // ---- -// Warning 6328: (240-253): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 38\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(38) +// Warning 6328: (240-253): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_mapping.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_mapping.sol index d4950a9b5..ac136acd2 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_add_mapping.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_mapping.sol @@ -14,5 +14,7 @@ contract C assert(b < 3); } } +// ==== +// SMTIgnoreCex: yes // ---- -// Warning 6328: (244-257): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\n\nTransaction trace:\nconstructor()\nf(38) +// Warning 6328: (244-257): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_minus_overflow_detected.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_minus_overflow_detected.sol new file mode 100644 index 000000000..79ecefd42 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_minus_overflow_detected.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; +contract C { + uint8 x; + + function inc_pre() public { + ++x; + } + + function dec_pre() public { + --x; + } + + /* Commented out because Spacer segfaults in Z3 4.8.9 + function inc_post() public { + x++; + } + + function dec_post() public { + x--; + } + */ +} +// ---- +// Warning 4984: (87-90): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\nx = 255\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ndec_pre()\nState: x = 255\ninc_pre() +// Warning 3944: (127-130): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\nx = 0\n\n\n\nTransaction trace:\nconstructor()\nState: x = 0\ndec_pre() diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly.sol new file mode 100644 index 000000000..c06b45196 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + uint8 x = 254; + + function inc_pre() public { + ++x; + } + + function check() view public { + uint y = x; + assert(y < 256); + } +} +// ---- +// Warning 4984: (94-97): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\nx = 255\n\n\n\nTransaction trace:\nconstructor()\nState: x = 254\ninc_pre()\nState: x = 255\ninc_pre() diff --git a/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly_struct.sol b/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly_struct.sol new file mode 100644 index 000000000..35c835f8b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/operators/unary_add_overflows_correctly_struct.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint8 x; + } + + S s; + + constructor() { + s.x = 254; + } + + function inc_pre() public { + ++s.x; + } + + function check() view public { + uint y = s.x; + assert(y < 256); + } +} +// ---- +// Warning 4984: (145-150): CHC: Overflow (resulting value larger than 255) happens here.\nCounterexample:\ns = {x: 255}\n\n\n\nTransaction trace:\nconstructor()\nState: s = {x: 254}\ninc_pre()\nState: s = {x: 255}\ninc_pre() diff --git a/test/libsolidity/smtCheckerTests/operators/unary_sub_array.sol b/test/libsolidity/smtCheckerTests/operators/unary_sub_array.sol index 008b7c117..0b5a6e59e 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_sub_array.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_sub_array.sol @@ -15,4 +15,4 @@ contract C } } // ---- -// Warning 6328: (240-253): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 38\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(38) +// Warning 6328: (240-253): CHC: Assertion violation happens here.\nCounterexample:\narray = []\nx = 0\n\n\nTransaction trace:\nconstructor()\nState: array = []\nf(0) diff --git a/test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol b/test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol index d02e2ea19..0c40ad544 100644 --- a/test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol +++ b/test/libsolidity/smtCheckerTests/operators/unary_sub_mapping.sol @@ -15,4 +15,4 @@ contract C } } // ---- -// Warning 6328: (244-257): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 38\n\n\nTransaction trace:\nconstructor()\nf(38) +// Warning 6328: (244-257): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\n\n\nTransaction trace:\nconstructor()\nf(0) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol index f61085e81..c165fb30f 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_recursive_6.sol @@ -52,6 +52,10 @@ contract C { // Warning 8364: (258-260): Assertion checker does not yet implement type struct C.S storage ref // Warning 7650: (271-275): Assertion checker does not yet support this expression. // Warning 8364: (271-273): Assertion checker does not yet implement type struct C.S storage ref +// Warning 4984: (132-138): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() +// Warning 4984: (142-148): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() +// Warning 3944: (165-171): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() +// Warning 3944: (175-181): CHC: Underflow (resulting value less than 0) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() // Warning 4984: (200-208): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() // Warning 6328: (185-209): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() // Warning 6328: (213-247): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nconstructor()\nf() @@ -87,11 +91,3 @@ contract C { // Warning 8364: (258-260): Assertion checker does not yet implement type struct C.S storage ref // Warning 7650: (271-275): Assertion checker does not yet support this expression. // Warning 8364: (271-273): Assertion checker does not yet implement type struct C.S storage ref -// Warning 4144: (132-138): BMC: Underflow (resulting value less than 0) happens here. -// Warning 2661: (132-138): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4144: (142-148): BMC: Underflow (resulting value less than 0) happens here. -// Warning 2661: (142-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4144: (165-171): BMC: Underflow (resulting value less than 0) happens here. -// Warning 2661: (165-171): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. -// Warning 4144: (175-181): BMC: Underflow (resulting value less than 0) happens here. -// Warning 2661: (175-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol index 6ca5f6ace..b32ac2225 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_unary_add.sol @@ -15,4 +15,4 @@ contract C { } } // ---- -// Warning 6328: (225-245): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, a: []}\ns2 = {x: 3, a: [5, 5, 5, 5, 5, 5]}\n\n\nTransaction trace:\nconstructor()\nf({x: 0, a: []}, {x: 3, a: [5, 5, 5, 5, 5, 5]}) +// Warning 6328: (225-245): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 2, a: []}\ns2 = {x: 3, a: [6, 6, 6, 6, 6, 6, 6]}\n\n\nTransaction trace:\nconstructor()\nf({x: 0, a: []}, {x: 3, a: [6, 6, 6, 6, 6, 6, 6]}) diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_unary_sub.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_unary_sub.sol index cfb93983c..3dda683a8 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_unary_sub.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_unary_sub.sol @@ -16,4 +16,4 @@ contract C { } } // ---- -// Warning 6328: (240-260): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 98, a: []}\ns2 = {x: (- 38), a: [5, 5, 5, 5, 5, 5]}\n\n\nTransaction trace:\nconstructor()\nf({x: 0, a: []}, {x: (- 38), a: [5, 5, 5, 5, 5, 5]}) +// Warning 6328: (240-260): CHC: Assertion violation happens here.\nCounterexample:\n\ns1 = {x: 98, a: []}\ns2 = {x: 99, a: [6, 6, 6, 6, 6, 6, 6]}\n\n\nTransaction trace:\nconstructor()\nf({x: 0, a: []}, {x: 99, a: [6, 6, 6, 6, 6, 6, 6]}) diff --git a/test/libsolidity/smtCheckerTests/types/unused_mapping.sol b/test/libsolidity/smtCheckerTests/types/unused_mapping.sol index f12cd41de..01905a36e 100644 --- a/test/libsolidity/smtCheckerTests/types/unused_mapping.sol +++ b/test/libsolidity/smtCheckerTests/types/unused_mapping.sol @@ -12,6 +12,7 @@ contract C { if(x == 0) x = 0; // noop state var read x++; y++; - assert(y == x); + // Commented out because of nondeterminism in Spacer in Z3 4.8.9 + //assert(y == x); } }