From 4fd7de36f10eefa5f09c3ebda794da896a72bc9b Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Tue, 3 May 2022 10:43:19 +0200 Subject: [PATCH] update smt tests z3 4.8.16 --- .circleci/config.yml | 16 ++-- .circleci/osx_install_dependencies.sh | 4 +- CMakeLists.txt | 2 +- scripts/build_emscripten.sh | 4 +- .../model_checker_invariants_all/err | 6 +- .../model_checker_invariants_contract/err | 2 +- .../err | 6 +- .../model_checker_invariants_reentrancy/err | 2 +- .../output.json | 4 +- .../output.json | 12 +-- .../output.json | 4 +- test/libsolidity/SMTCheckerTest.cpp | 12 ++- .../array_members/push_as_lhs_1d.sol | 2 +- .../array_members/push_as_lhs_bytes.sol | 2 +- .../blockchain_state/balance_receive_4.sol | 3 +- .../branches_in_modifiers_2.sol | 2 +- ...same_input_over_state_same_output_fail.sol | 4 +- .../external_calls/call_with_value_1.sol | 2 +- .../external_calls/call_with_value_2.sol | 2 +- .../external_call_from_constructor_3.sol | 2 +- ...nal_hash_known_code_state_reentrancy_2.sol | 4 +- ...h_known_code_state_reentrancy_indirect.sol | 4 +- .../smtCheckerTests/functions/payable_2.sol | 2 +- .../loops/while_nested_continue_fail.sol | 4 +- .../operators/compound_bitwise_or_uint_2.sol | 2 +- .../special/block_vars_chc_internal.sol | 2 +- .../special/tx_vars_reentrancy_1.sol | 2 +- .../types/array_mapping_aliasing_2.sol | 3 +- .../types/array_static_mapping_aliasing_2.sol | 3 +- ...array_struct_array_struct_storage_safe.sol | 1 + .../struct_aliasing_parameter_storage_2.sol | 2 +- .../struct_aliasing_parameter_storage_3.sol | 2 +- .../unchecked/checked_called_by_unchecked.sol | 2 +- .../smtCheckerTests/userTypes/conversion.sol | 87 ------------------- .../userTypes/conversion_1.sol | 35 ++++++++ .../userTypes/conversion_2.sol | 32 +++++++ .../userTypes/conversion_3.sol | 34 ++++++++ .../userTypes/conversion_4.sol | 23 +++++ 38 files changed, 191 insertions(+), 146 deletions(-) delete mode 100644 test/libsolidity/smtCheckerTests/userTypes/conversion.sol create mode 100644 test/libsolidity/smtCheckerTests/userTypes/conversion_1.sol create mode 100644 test/libsolidity/smtCheckerTests/userTypes/conversion_2.sol create mode 100644 test/libsolidity/smtCheckerTests/userTypes/conversion_3.sol create mode 100644 test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol diff --git a/.circleci/config.yml b/.circleci/config.yml index d42021373..2d824c249 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -9,20 +9,20 @@ version: 2.1 parameters: ubuntu-2004-docker-image: type: string - # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-11 - default: "solbuildpackpusher/solidity-buildpack-deps@sha256:9928dc357829e475e8729c62a1c2d495dbb41cb9fe4c4b115a5568be8e1ed69e" + # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-12 + default: "solbuildpackpusher/solidity-buildpack-deps@sha256:5087cc068b48787e89887804e632120b3e65bc5c25086bdf7b152be4fe5fc9ba" ubuntu-2004-clang-docker-image: type: string - # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-11 - default: "solbuildpackpusher/solidity-buildpack-deps@sha256:72fb9574c90e8ef908dce4c9dd9788ff4de708b504d970cd9146eed8911c313e" + # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004.clang-12 + default: "solbuildpackpusher/solidity-buildpack-deps@sha256:7f53f1bc3d89bdfb0725f604efbbec570d80ffa9b731b47a4842f4e286de0355" ubuntu-1604-clang-ossfuzz-docker-image: type: string - # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-16 - default: "solbuildpackpusher/solidity-buildpack-deps@sha256:fe54d8e5409827d43edb0dc8ad0d9e4232a675050ceb271c873b73e5ee267938" + # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-17 + default: "solbuildpackpusher/solidity-buildpack-deps@sha256:85b298c763adf5c516238246beb283640eb555e79e7ad6a8e7a6c9ed47ef6324" emscripten-docker-image: type: string - # solbuildpackpusher/solidity-buildpack-deps:emscripten-9 - default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d51534dfdd05ece86f69ed7beafd68c15b88606da00a4b7fe2873ccfbd0dce24" + # solbuildpackpusher/solidity-buildpack-deps:emscripten-10 + default: "solbuildpackpusher/solidity-buildpack-deps@sha256:bd23831e0025e35a106005b4ac06cb3618f690bfa2833a5881b573c02d35d9fc" evm-version: type: string default: london diff --git a/.circleci/osx_install_dependencies.sh b/.circleci/osx_install_dependencies.sh index cd0637eac..6b328e5a1 100755 --- a/.circleci/osx_install_dependencies.sh +++ b/.circleci/osx_install_dependencies.sh @@ -61,11 +61,11 @@ then ./scripts/install_obsolete_jsoncpp_1_7_4.sh # z3 - z3_version="4.8.14" + z3_version="4.8.16" z3_dir="z3-${z3_version}-x64-osx-10.16" z3_package="${z3_dir}.zip" wget "https://github.com/Z3Prover/z3/releases/download/z3-${z3_version}/${z3_package}" - validate_checksum "$z3_package" 1341671670e0c4e72da80815128a68975ee90816d50ceaf6bd820f06babe2cfd + validate_checksum "$z3_package" 71ed7b6d10c01198187df72cccb8eb6de6d9aa2bf9557b3dd052032524b598a5 unzip "$z3_package" rm "$z3_package" cp "${z3_dir}/bin/libz3.a" /usr/local/lib diff --git a/CMakeLists.txt b/CMakeLists.txt index 759f69a53..a298f4044 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -65,7 +65,7 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens include(EthOptions) configure_project(TESTS) -set(LATEST_Z3_VERSION "4.8.14") +set(LATEST_Z3_VERSION "4.8.16") set(MINIMUM_Z3_VERSION "4.8.0") find_package(Z3) if (${Z3_FOUND}) diff --git a/scripts/build_emscripten.sh b/scripts/build_emscripten.sh index 16e9078f3..09d421e5a 100755 --- a/scripts/build_emscripten.sh +++ b/scripts/build_emscripten.sh @@ -34,7 +34,7 @@ else BUILD_DIR="$1" fi -# solbuildpackpusher/solidity-buildpack-deps:emscripten-9 +# solbuildpackpusher/solidity-buildpack-deps:emscripten-10 docker run -v "$(pwd):/root/project" -w /root/project \ - solbuildpackpusher/solidity-buildpack-deps@sha256:d51534dfdd05ece86f69ed7beafd68c15b88606da00a4b7fe2873ccfbd0dce24\ + solbuildpackpusher/solidity-buildpack-deps@sha256:bd23831e0025e35a106005b4ac06cb3618f690bfa2833a5881b573c02d35d9fc\ ./scripts/ci/build_emscripten.sh "$BUILD_DIR" diff --git a/test/cmdlineTests/model_checker_invariants_all/err b/test/cmdlineTests/model_checker_invariants_all/err index 2f028037b..66a76b3c8 100644 --- a/test/cmdlineTests/model_checker_invariants_all/err +++ b/test/cmdlineTests/model_checker_invariants_all/err @@ -5,10 +5,10 @@ Warning: Return value of low-level calls not used. | ^^^^^^^^^^^ Info: Contract invariant(s) for model_checker_invariants_all/input.sol:test: -(x <= 0) +((x <= 0) || true || true) Reentrancy property(ies) for model_checker_invariants_all/input.sol:test: -((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) -((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) +(true || true || ((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) || true) +(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) = 0 -> no errors = 1 -> Assertion failed at assert(x < 10) = 3 -> Assertion failed at assert(x < 10) diff --git a/test/cmdlineTests/model_checker_invariants_contract/err b/test/cmdlineTests/model_checker_invariants_contract/err index a5277bebf..e3058cca5 100644 --- a/test/cmdlineTests/model_checker_invariants_contract/err +++ b/test/cmdlineTests/model_checker_invariants_contract/err @@ -1,2 +1,2 @@ Info: Contract invariant(s) for model_checker_invariants_contract/input.sol:test: -(x <= 0) +((x <= 0) || true) diff --git a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err index fad76665e..694f512cd 100644 --- a/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err +++ b/test/cmdlineTests/model_checker_invariants_contract_reentrancy/err @@ -5,10 +5,10 @@ Warning: Return value of low-level calls not used. | ^^^^^^^^^^^ Info: Contract invariant(s) for model_checker_invariants_contract_reentrancy/input.sol:test: -(x <= 0) +((x <= 0) || true || true) Reentrancy property(ies) for model_checker_invariants_contract_reentrancy/input.sol:test: -((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) -((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) +(true || true || ((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) || true) +(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) = 0 -> no errors = 1 -> Assertion failed at assert(x < 10) = 3 -> Assertion failed at assert(x < 10) diff --git a/test/cmdlineTests/model_checker_invariants_reentrancy/err b/test/cmdlineTests/model_checker_invariants_reentrancy/err index a2fd6075a..dc939704b 100644 --- a/test/cmdlineTests/model_checker_invariants_reentrancy/err +++ b/test/cmdlineTests/model_checker_invariants_reentrancy/err @@ -5,6 +5,6 @@ Warning: Return value of low-level calls not used. | ^^^^^^^^^^^ Info: Reentrancy property(ies) for model_checker_invariants_reentrancy/input.sol:test: -((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) +(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) = 0 -> no errors = 1 -> Assertion failed at assert(x < 10) diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract/output.json b/test/cmdlineTests/standard_model_checker_invariants_contract/output.json index 1cd236baf..385fcb31f 100644 --- a/test/cmdlineTests/standard_model_checker_invariants_contract/output.json +++ b/test/cmdlineTests/standard_model_checker_invariants_contract/output.json @@ -1,7 +1,7 @@ {"errors":[{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test: -(x <= 0) +((x <= 0) || true) ","message":"Contract invariant(s) for A:test: -(x <= 0) +((x <= 0) || true) ","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}} diff --git a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json index f5ced7253..d560ff288 100644 --- a/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json +++ b/test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json @@ -5,20 +5,20 @@ | \t\t\t\t\t\t^^^^^^^^^^^ ","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test: -(x <= 0) +((x <= 0) || true || true) Reentrancy property(ies) for A:test: -((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) -((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) +(true || true || ((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) || true) +(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) = 0 -> no errors = 1 -> Assertion failed at assert(x < 10) = 3 -> Assertion failed at assert(x < 10) ","message":"Contract invariant(s) for A:test: -(x <= 0) +((x <= 0) || true || true) Reentrancy property(ies) for A:test: -((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) -((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) +(true || true || ((!(x <= 0) || !( >= 3)) && (!(x <= 0) || (x' <= 0))) || true) +(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) = 0 -> no errors = 1 -> Assertion failed at assert(x < 10) = 3 -> Assertion failed at assert(x < 10) diff --git a/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json index 4158c3ae1..d7cb43429 100644 --- a/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json +++ b/test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json @@ -5,13 +5,13 @@ | \t\t\t\t\t\t^^^^^^^^^^^ ","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Reentrancy property(ies) for A:test: -((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) +(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) = 0 -> no errors = 1 -> Assertion failed at assert(x < 10) ","message":"Reentrancy property(ies) for A:test: -((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) +(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || ( <= 0))) || true) = 0 -> no errors = 1 -> Assertion failed at assert(x < 10) ","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}} diff --git a/test/libsolidity/SMTCheckerTest.cpp b/test/libsolidity/SMTCheckerTest.cpp index 3b6b8e1b8..10084b014 100644 --- a/test/libsolidity/SMTCheckerTest.cpp +++ b/test/libsolidity/SMTCheckerTest.cpp @@ -69,7 +69,17 @@ SMTCheckerTest::SMTCheckerTest(string const& _filename): SyntaxTest(_filename, E else BOOST_THROW_EXCEPTION(runtime_error("Invalid SMT counterexample choice.")); - auto const& ignoreInv = m_reader.stringSetting("SMTIgnoreInv", "no"); + static auto removeInv = [](vector&& errors) { + vector filtered; + for (auto&& e: errors) + if (e.errorId != 1180_error) + filtered.emplace_back(e); + return filtered; + }; + if (m_modelCheckerSettings.invariants.invariants.empty()) + m_expectations = removeInv(move(m_expectations)); + + auto const& ignoreInv = m_reader.stringSetting("SMTIgnoreInv", "yes"); if (ignoreInv == "no") m_modelCheckerSettings.invariants = ModelCheckerInvariants::All(); else if (ignoreInv == "yes") diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol index 0d16306b7..b38963b59 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol @@ -19,4 +19,4 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Warning 6328: (199-229): CHC: Assertion violation happens here.\nCounterexample:\nb = [1]\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g() +// Warning 6328: (199-229): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol index 7bd74f6dc..fd0229d78 100644 --- a/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol +++ b/test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol @@ -19,4 +19,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (265-310): CHC: Assertion violation happens here. +// Warning 6328: (265-310): CHC: Assertion violation happens here.\nCounterexample:\nb = [0x01]\none = 0x01\n\nTransaction trace:\nC.constructor()\nState: b = []\nC.g() diff --git a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol index 4fa420ff1..d72da3efa 100644 --- a/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol +++ b/test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol @@ -16,8 +16,7 @@ contract C { // Warning 4984: (82-85): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (154-160): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. // Warning 4984: (212-218): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here. -// Warning 6328: (180-219): CHC: Assertion violation happens here.\nCounterexample:\nc = 1\n\nTransaction trace:\nC.constructor()\nState: c = 0\nC.f(){ msg.value: 11 }\nState: c = 1\nC.inv() -// Info 1180: Contract invariant(s) for :C:\n(((11 * c) + ((- 1) * (:var 1).balances[address(this)])) <= 0)\n +// Warning 6328: (180-219): CHC: Assertion violation happens here. // Warning 2661: (82-85): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (154-160): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (212-218): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. diff --git a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol index 98b551c17..f08a26bf7 100644 --- a/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol +++ b/test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol @@ -45,5 +45,5 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 6328: (255-269): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.test()\n C.reset_if_overflow() -- internal call -// Warning 6328: (502-519): CHC: Assertion violation happens here. +// Warning 6328: (502-519): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\noldx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(1)\nState: x = 1\nC.test()\n C.reset_if_overflow() -- internal call // Warning 6328: (615-629): CHC: Assertion violation happens here.\nCounterexample:\nx = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.set(10)\nState: x = 10\nC.test()\n C.reset_if_overflow() -- internal call diff --git a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol index fd3b55a8c..b89867c39 100644 --- a/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol +++ b/test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol @@ -48,12 +48,10 @@ contract C { // Warning 1218: (693-712): CHC: Error trying to invoke SMT solver. // Warning 1218: (716-735): CHC: Error trying to invoke SMT solver. // Warning 1218: (739-758): CHC: Error trying to invoke SMT solver. -// Warning 1218: (762-781): CHC: Error trying to invoke SMT solver. // Warning 6328: (693-712): CHC: Assertion violation might happen here. // Warning 6328: (716-735): CHC: Assertion violation might happen here. // Warning 6328: (739-758): CHC: Assertion violation might happen here. -// Warning 6328: (762-781): CHC: Assertion violation might happen here. +// Warning 6328: (762-781): CHC: Assertion violation happens here. // Warning 4661: (693-712): BMC: Assertion violation happens here. // Warning 4661: (716-735): BMC: Assertion violation happens here. // Warning 4661: (739-758): BMC: Assertion violation happens here. -// Warning 4661: (762-781): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol index 813185adf..f9293f693 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol @@ -12,5 +12,5 @@ contract C { // ---- // Warning 9302: (96-117): Return value of low-level calls not used. // Warning 6328: (121-156): CHC: Assertion violation might happen here. -// Warning 6328: (175-211): CHC: Assertion violation happens here. +// Warning 6328: (175-211): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n i.call{value: 10}("") -- untrusted external call // Warning 4661: (121-156): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol index c38658080..968095bb2 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol @@ -11,5 +11,5 @@ contract C { // ---- // Warning 9302: (96-116): Return value of low-level calls not used. // Warning 6328: (120-156): CHC: Assertion violation might happen here. -// Warning 6328: (175-210): CHC: Assertion violation happens here.\nCounterexample:\n\ni = 0x0\n\nTransaction trace:\nC.constructor()\nC.g(0x0)\n i.call{value: 0}("") -- untrusted external call +// Warning 6328: (175-210): CHC: Assertion violation happens here. // Warning 4661: (120-156): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol index eb5cd97dd..9d27d6d3b 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol @@ -20,4 +20,4 @@ contract C { // SMTEngine: all // ---- // Warning 6328: (69-85): CHC: Assertion violation happens here.\nCounterexample:\n\n_x = 100\n = 0\n\nTransaction trace:\nState.constructor()\nState.f(100) -// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 3\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 3\nC.f() +// Warning 6328: (203-217): CHC: Assertion violation happens here.\nCounterexample:\ns = 0, z = 0\n\nTransaction trace:\nC.constructor()\nState: s = 0, z = 0\nC.f() diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol index be9f698e1..37509269b 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol @@ -42,4 +42,6 @@ contract C { // SMTIgnoreOS: macos // ---- // Warning 2018: (33-88): Function state mutability can be restricted to view -// Warning 6328: (367-381): CHC: Assertion violation happens here. +// Warning 1218: (367-381): CHC: Error trying to invoke SMT solver. +// Warning 6328: (367-381): CHC: Assertion violation might happen here. +// Warning 4661: (367-381): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol index ea9764e17..bd779b56a 100644 --- a/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol +++ b/test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol @@ -44,7 +44,5 @@ contract C { // SMTIgnoreCex: yes // SMTIgnoreOS: macos // ---- -// Warning 1218: (437-463): CHC: Error trying to invoke SMT solver. // Warning 6328: (419-433): CHC: Assertion violation happens here. -// Warning 6328: (437-463): CHC: Assertion violation might happen here. -// Warning 4661: (437-463): BMC: Assertion violation happens here. +// Warning 6328: (437-463): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/functions/payable_2.sol b/test/libsolidity/smtCheckerTests/functions/payable_2.sol index 98717b133..04833ae02 100644 --- a/test/libsolidity/smtCheckerTests/functions/payable_2.sol +++ b/test/libsolidity/smtCheckerTests/functions/payable_2.sol @@ -24,4 +24,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (261-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g2(){ msg.value: 35 }\n C.i() -- internal call +// Warning 6328: (261-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g2(){ msg.value: 1 }\n C.i() -- internal call diff --git a/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol b/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol index fe43db0de..180d85adc 100644 --- a/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol +++ b/test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol @@ -27,7 +27,5 @@ contract C // ==== // SMTEngine: all // ---- -// Warning 1218: (290-305): CHC: Error trying to invoke SMT solver. -// Warning 6328: (290-305): CHC: Assertion violation might happen here. +// Warning 6328: (290-305): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 15\nb = false\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, false, false) // Warning 6328: (329-344): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 15\ny = 0\nb = true\nc = false\n\nTransaction trace:\nC.constructor()\nC.f(0, 0, true, false) -// Warning 4661: (290-305): BMC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol index 9b27a277b..edd36047c 100644 --- a/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol +++ b/test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol @@ -19,4 +19,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Info 1180: Contract invariant(s) for :C:\n!(s.x.length <= 2)\n +// Warning 6368: (196-202): CHC: Out of bounds access might happen here. diff --git a/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol b/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol index 2ebf4d326..6e4f5a620 100644 --- a/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol +++ b/test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol @@ -32,4 +32,4 @@ contract C { // ==== // SMTEngine: chc // ---- -// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x0, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n C.g() -- internal call +// Warning 6328: (770-799): CHC: Assertion violation happens here.\nCounterexample:\ncoin = 0x1e28, dif = 0, gas = 0, number = 0, timestamp = 0\n\nTransaction trace:\nC.constructor()\nState: coin = 0x0, dif = 0, gas = 0, number = 0, timestamp = 0\nC.f(){ block.coinbase: 0x1e28, block.difficulty: 0, block.gaslimit: 0, block.number: 0, block.timestamp: 0 }\n C.g() -- internal call diff --git a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol index 7729cebb9..f1fed73c0 100644 --- a/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol +++ b/test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol @@ -13,4 +13,4 @@ contract C { // SMTEngine: all // SMTIgnoreOS: macos // ---- -// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 2997\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2803 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 2446 } -- reentrant call\n _i.f() -- untrusted external call +// Warning 6328: (135-169): CHC: Assertion violation happens here.\nCounterexample:\n\n_i = 0\nx = 9726\n\nTransaction trace:\nC.constructor()\nC.g(0){ msg.value: 2070 }\n _i.f() -- untrusted external call, synthesized as:\n C.g(0){ msg.value: 0 } -- reentrant call\n _i.f() -- untrusted external call diff --git a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol index dd0d8e004..cd1d77d8d 100644 --- a/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol @@ -36,11 +36,12 @@ contract C // SMTIgnoreCex: yes // ---- // Warning 6368: (439-453): CHC: Out of bounds access happens here. +// Warning 6368: (465-480): CHC: Out of bounds access might happen here. // Warning 6368: (492-508): CHC: Out of bounds access happens here. // Warning 6368: (492-511): CHC: Out of bounds access happens here. // Warning 6368: (622-636): CHC: Out of bounds access happens here. +// Warning 6368: (737-752): CHC: Out of bounds access might happen here. // 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 1180: Contract invariant(s) for :C:\n!(severalMaps8.length <= 0)\n diff --git a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol index f9aa3a650..ca1a58018 100644 --- a/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol +++ b/test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol @@ -30,7 +30,8 @@ contract C // SMTEngine: all // SMTIgnoreCex: yes // ---- +// Warning 6368: (340-355): CHC: Out of bounds access might happen here. +// Warning 6368: (612-627): CHC: Out of bounds access might happen here. // Warning 6328: (860-880): CHC: Assertion violation happens here. // Warning 6368: (936-952): CHC: Out of bounds access might happen here. // Warning 6368: (936-955): CHC: Out of bounds access might happen here. -// Info 1180: Contract invariant(s) for :C:\n!(severalMaps8.length <= 1)\n diff --git a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol index 109fee7dc..67f56d8c6 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol @@ -53,3 +53,4 @@ contract C { // ==== // SMTEngine: all // ---- +// Warning 6368: (212-217): CHC: Out of bounds access might happen here. diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol index 698262382..9d4623ae0 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol @@ -20,4 +20,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (289-322): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 11}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 11}\nC.g(){ msg.sender: 0x0985 } +// Warning 6328: (289-322): CHC: Assertion violation happens here.\nCounterexample:\ns = {innerM, sum: 10}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: s = {innerM, sum: 10}\nC.g(){ msg.sender: 0x0985 } diff --git a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol index fcf30555e..8779cd095 100644 --- a/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol +++ b/test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol @@ -26,4 +26,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 6328: (307-327): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 11, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 11, s: {innerM, sum: 21239}}\nC.g() +// Warning 6328: (307-327): CHC: Assertion violation happens here.\nCounterexample:\nt = {x: 10, s: {innerM, sum: 21239}}\n\nTransaction trace:\nC.constructor(0){ msg.sender: 0x6dc4 }\nState: t = {x: 10, s: {innerM, sum: 21239}}\nC.g() diff --git a/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol b/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol index cb795f9c0..d3589fed5 100644 --- a/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol +++ b/test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol @@ -10,4 +10,4 @@ contract C { // ==== // SMTEngine: all // ---- -// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 65535) happens here.\nCounterexample:\n\na = 1\nb = 65535\n = 0\n\nTransaction trace:\nC.constructor()\nC.add(1, 65535) +// Warning 4984: (96-101): CHC: Overflow (resulting value larger than 65535) happens here.\nCounterexample:\n\na = 65535\nb = 1\n = 0\n\nTransaction trace:\nC.constructor()\nC.add(65535, 1) diff --git a/test/libsolidity/smtCheckerTests/userTypes/conversion.sol b/test/libsolidity/smtCheckerTests/userTypes/conversion.sol deleted file mode 100644 index cad0233a7..000000000 --- a/test/libsolidity/smtCheckerTests/userTypes/conversion.sol +++ /dev/null @@ -1,87 +0,0 @@ -pragma abicoder v2; - -type MyUInt8 is uint8; -type MyInt8 is int8; -type MyUInt16 is uint16; - -contract C { - function f(uint a) internal pure returns(MyUInt8) { - return MyUInt8.wrap(uint8(a)); - } - function g(uint a) internal pure returns(MyInt8) { - return MyInt8.wrap(int8(int(a))); - } - function h(MyUInt8 a) internal pure returns (MyInt8) { - return MyInt8.wrap(int8(MyUInt8.unwrap(a))); - } - function i(MyUInt8 a) internal pure returns(MyUInt16) { - return MyUInt16.wrap(MyUInt8.unwrap(a)); - } - function j(MyUInt8 a) internal pure returns (uint) { - return MyUInt8.unwrap(a); - } - function k(MyUInt8 a) internal pure returns (MyUInt16) { - return MyUInt16.wrap(MyUInt8.unwrap(a)); - } - function m(MyUInt16 a) internal pure returns (MyUInt8) { - return MyUInt8.wrap(uint8(MyUInt16.unwrap(a))); - } - - function p() public pure { - assert(MyUInt8.unwrap(f(1)) == 1); - assert(MyUInt8.unwrap(f(2)) == 2); - assert(MyUInt8.unwrap(f(257)) == 1); - assert(MyUInt8.unwrap(f(257)) == 257); // should fail - } - - function q() public pure { - assert(MyInt8.unwrap(g(1)) == 1); - assert(MyInt8.unwrap(g(2)) == 2); - assert(MyInt8.unwrap(g(255)) == -1); - assert(MyInt8.unwrap(g(257)) == 1); - assert(MyInt8.unwrap(g(257)) == -1); // should fail - } - - function r() public pure { - assert(MyInt8.unwrap(h(MyUInt8.wrap(1))) == 1); - assert(MyInt8.unwrap(h(MyUInt8.wrap(2))) == 2); - assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == -1); - assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == 1); // should fail - } - - function s() public pure { - assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 250); - assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 0); // should fail - } - - function t() public pure { - assert(j(MyUInt8.wrap(1)) == 1); - assert(j(MyUInt8.wrap(2)) == 2); - assert(j(MyUInt8.wrap(255)) == 0xff); - assert(j(MyUInt8.wrap(255)) == 1); // should fail - } - - function v() public pure { - assert(MyUInt16.unwrap(k(MyUInt8.wrap(1))) == 1); - assert(MyUInt16.unwrap(k(MyUInt8.wrap(2))) == 2); - assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 0xff); - assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 1); // should fail - } - - function w() public pure { - assert(MyUInt8.unwrap(m(MyUInt16.wrap(1))) == 1); - assert(MyUInt8.unwrap(m(MyUInt16.wrap(2))) == 2); - assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 0xff); - assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 1); // should fail - } -} -// ==== -// SMTEngine: all -// ---- -// Warning 6328: (937-974): CHC: Assertion violation happens here. -// Warning 6328: (1174-1209): CHC: Assertion violation happens here. -// Warning 6328: (1413-1461): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.r()\n C.h(1) -- internal call\n C.h(2) -- internal call\n C.h(255) -- internal call\n C.h(255) -- internal call -// Warning 6328: (1568-1618): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.s()\n C.i(250) -- internal call\n C.i(250) -- internal call -// Warning 6328: (1779-1812): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.t()\n C.j(1) -- internal call\n C.j(2) -- internal call\n C.j(255) -- internal call\n C.j(255) -- internal call -// Warning 6328: (2024-2074): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.v()\n C.k(1) -- internal call\n C.k(2) -- internal call\n C.k(255) -- internal call\n C.k(255) -- internal call -// Warning 6328: (2286-2336): CHC: Assertion violation happens here. diff --git a/test/libsolidity/smtCheckerTests/userTypes/conversion_1.sol b/test/libsolidity/smtCheckerTests/userTypes/conversion_1.sol new file mode 100644 index 000000000..fa56e11ab --- /dev/null +++ b/test/libsolidity/smtCheckerTests/userTypes/conversion_1.sol @@ -0,0 +1,35 @@ +pragma abicoder v2; + +type MyUInt8 is uint8; +type MyInt8 is int8; +type MyUInt16 is uint16; + +contract C { + function f(uint a) internal pure returns(MyUInt8) { + return MyUInt8.wrap(uint8(a)); + } + function g(uint a) internal pure returns(MyInt8) { + return MyInt8.wrap(int8(int(a))); + } + + function p() public pure { + assert(MyUInt8.unwrap(f(1)) == 1); + assert(MyUInt8.unwrap(f(2)) == 2); + assert(MyUInt8.unwrap(f(257)) == 1); + assert(MyUInt8.unwrap(f(257)) == 257); // should fail + } + + function q() public pure { + assert(MyInt8.unwrap(g(1)) == 1); + assert(MyInt8.unwrap(g(2)) == 2); + assert(MyInt8.unwrap(g(255)) == -1); + assert(MyInt8.unwrap(g(257)) == 1); + assert(MyInt8.unwrap(g(257)) == -1); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (428-465): CHC: Assertion violation happens here. +// Warning 6328: (665-700): CHC: Assertion violation happens here. +// Info 1180: Contract invariant(s) for :C:\n(true || true || true || true || true)\nReentrancy property(ies) for :C:\n(true || (( = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true)\n(true || true || (( = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true)\n(true || true || true || true || (( = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || true || true || true || (( = 0) && ((:var 0) = (:var 1))) || true || true || true)\n(true || true || true || true || true || true || true || (( = 0) && ((:var 0) = (:var 1))) || true)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(MyUInt8.unwrap(f(1)) == 1)\n = 2 -> Assertion failed at assert(MyUInt8.unwrap(f(2)) == 2)\n = 3 -> Assertion failed at assert(MyUInt8.unwrap(f(257)) == 1)\n = 4 -> Assertion failed at assert(MyUInt8.unwrap(f(257)) == 257)\n = 6 -> Assertion failed at assert(MyInt8.unwrap(g(1)) == 1)\n = 7 -> Assertion failed at assert(MyInt8.unwrap(g(2)) == 2)\n = 8 -> Assertion failed at assert(MyInt8.unwrap(g(255)) == -1)\n = 9 -> Assertion failed at assert(MyInt8.unwrap(g(257)) == 1)\n = 10 -> Assertion failed at assert(MyInt8.unwrap(g(257)) == -1)\n diff --git a/test/libsolidity/smtCheckerTests/userTypes/conversion_2.sol b/test/libsolidity/smtCheckerTests/userTypes/conversion_2.sol new file mode 100644 index 000000000..9b4f72d33 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/userTypes/conversion_2.sol @@ -0,0 +1,32 @@ +pragma abicoder v2; + +type MyUInt8 is uint8; +type MyInt8 is int8; +type MyUInt16 is uint16; + +contract C { + function h(MyUInt8 a) internal pure returns (MyInt8) { + return MyInt8.wrap(int8(MyUInt8.unwrap(a))); + } + function i(MyUInt8 a) internal pure returns(MyUInt16) { + return MyUInt16.wrap(MyUInt8.unwrap(a)); + } + + function r() public pure { + assert(MyInt8.unwrap(h(MyUInt8.wrap(1))) == 1); + assert(MyInt8.unwrap(h(MyUInt8.wrap(2))) == 2); + assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == -1); + assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == 1); // should fail + } + + function s() public pure { + assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 250); + assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 0); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (497-545): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.r()\n C.h(1) -- internal call\n C.h(2) -- internal call\n C.h(255) -- internal call\n C.h(255) -- internal call +// Warning 6328: (652-702): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.s()\n C.i(250) -- internal call\n C.i(250) -- internal call +// Info 1180: Contract invariant(s) for :C:\n(true || true || true || true || true)\nReentrancy property(ies) for :C:\n((( = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true || true)\n(true || (( = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true)\n(true || true || true || true || (( = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || true || true || true || (( = 0) && ((:var 0) = (:var 1))) || true || true || true)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(1))) == 1)\n = 2 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(2))) == 2)\n = 3 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == -1)\n = 4 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == 1)\n = 6 -> Assertion failed at assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 250)\n = 7 -> Assertion failed at assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 0)\n diff --git a/test/libsolidity/smtCheckerTests/userTypes/conversion_3.sol b/test/libsolidity/smtCheckerTests/userTypes/conversion_3.sol new file mode 100644 index 000000000..ea8e9804b --- /dev/null +++ b/test/libsolidity/smtCheckerTests/userTypes/conversion_3.sol @@ -0,0 +1,34 @@ +pragma abicoder v2; + +type MyUInt8 is uint8; +type MyInt8 is int8; +type MyUInt16 is uint16; + +contract C { + function j(MyUInt8 a) internal pure returns (uint) { + return MyUInt8.unwrap(a); + } + function k(MyUInt8 a) internal pure returns (MyUInt16) { + return MyUInt16.wrap(MyUInt8.unwrap(a)); + } + + function t() public pure { + assert(j(MyUInt8.wrap(1)) == 1); + assert(j(MyUInt8.wrap(2)) == 2); + assert(j(MyUInt8.wrap(255)) == 0xff); + assert(j(MyUInt8.wrap(255)) == 1); // should fail + } + + function v() public pure { + assert(MyUInt16.unwrap(k(MyUInt8.wrap(1))) == 1); + assert(MyUInt16.unwrap(k(MyUInt8.wrap(2))) == 2); + assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 0xff); + assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 1); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (434-467): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.t()\n C.j(1) -- internal call\n C.j(2) -- internal call\n C.j(255) -- internal call\n C.j(255) -- internal call +// Warning 6328: (679-729): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.v()\n C.k(1) -- internal call\n C.k(2) -- internal call\n C.k(255) -- internal call\n C.k(255) -- internal call +// Info 1180: Contract invariant(s) for :C:\n(true || true || true || true || true)\nReentrancy property(ies) for :C:\n((( = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true || true)\n(true || true || true || (( = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true)\n(true || true || true || true || (( = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || true || true || true || true || true || (( = 0) && ((:var 0) = (:var 1))) || true)\n(true || true || true || true || true || true || true || true || (( = 0) && ((:var 0) = (:var 1))))\n = 0 -> no errors\n = 1 -> Assertion failed at assert(j(MyUInt8.wrap(1)) == 1)\n = 2 -> Assertion failed at assert(j(MyUInt8.wrap(2)) == 2)\n = 3 -> Assertion failed at assert(j(MyUInt8.wrap(255)) == 0xff)\n = 4 -> Assertion failed at assert(j(MyUInt8.wrap(255)) == 1)\n = 6 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(1))) == 1)\n = 7 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(2))) == 2)\n = 8 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 0xff)\n = 9 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 1)\n diff --git a/test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol b/test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol new file mode 100644 index 000000000..ced7e37c4 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol @@ -0,0 +1,23 @@ +pragma abicoder v2; + +type MyUInt8 is uint8; +type MyInt8 is int8; +type MyUInt16 is uint16; + +contract C { + function m(MyUInt16 a) internal pure returns (MyUInt8) { + return MyUInt8.wrap(uint8(MyUInt16.unwrap(a))); + } + + function w() public pure { + assert(MyUInt8.unwrap(m(MyUInt16.wrap(1))) == 1); + assert(MyUInt8.unwrap(m(MyUInt16.wrap(2))) == 2); + assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 0xff); + assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 1); // should fail + } +} +// ==== +// SMTEngine: all +// ---- +// Warning 6328: (407-457): CHC: Assertion violation happens here. +// Info 1180: Contract invariant(s) for :C:\n(true || true || true)\nReentrancy property(ies) for :C:\n((( = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || (( = 0) && ((:var 0) = (:var 1))) || true || true)\n = 0 -> no errors\n = 1 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(1))) == 1)\n = 2 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(2))) == 2)\n = 3 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 0xff)\n = 4 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 1)\n