cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

update smt tests z3 4.8.16

Browse Source
This commit is contained in:
Leo Alt 2022-05-03 10:43:19 +02:00
parent 3e3e73e380
commit 4fd7de36f1
38 changed files with 191 additions and 146 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
.circleci/config.yml
View File

@ -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

4
.circleci/osx_install_dependencies.sh
View File

@ -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

2
CMakeLists.txt
View File

@ -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})

4
scripts/build_emscripten.sh
View File

@ -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"

6
test/cmdlineTests/model_checker_invariants_all/err
View File

@ -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) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
(true || true || ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0))) || true)
(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 3 -> Assertion failed at assert(x < 10)

2
test/cmdlineTests/model_checker_invariants_contract/err
View File

@ -1,2 +1,2 @@
Info: Contract invariant(s) for model_checker_invariants_contract/input.sol:test:
(x <= 0)
((x <= 0) || true)

6
test/cmdlineTests/model_checker_invariants_contract_reentrancy/err
View File

@ -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) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
(true || true || ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0))) || true)
(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 3 -> Assertion failed at assert(x < 10)

2
test/cmdlineTests/model_checker_invariants_reentrancy/err
View File

@ -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) || (<errorCode> <= 0)))
(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)

4
test/cmdlineTests/standard_model_checker_invariants_contract/output.json
View File

@ -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}}}

12
test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json
View File

@ -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) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
(true || true || ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0))) || true)
(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 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) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0)))
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
(true || true || ((!(x <= 0) || !(<errorCode> >= 3)) && (!(x <= 0) || (x' <= 0))) || true)
(true || true || ((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
<errorCode> = 3 -> Assertion failed at assert(x < 10)

4
test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json
View File

@ -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) || (<errorCode> <= 0)))
(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
","message":"Reentrancy property(ies) for A:test:
((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0)))
(((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
<errorCode> = 0 -> no errors
<errorCode> = 1 -> Assertion failed at assert(x < 10)
","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}

12
test/libsolidity/SMTCheckerTest.cpp
View File

@ -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<SyntaxTestError>&& errors) {
vector<SyntaxTestError> 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")

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_1d.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/array_members/push_as_lhs_bytes.sol
View File

@ -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()

3
test/libsolidity/smtCheckerTests/blockchain_state/balance_receive_4.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol
View File

@ -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

4
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/external_calls/call_with_value_1.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/external_calls/call_with_value_2.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/external_calls/external_call_from_constructor_3.sol
View File

@ -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()

4
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_2.sol
View File

@ -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.

4
test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/functions/payable_2.sol
View File

@ -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

4
test/libsolidity/smtCheckerTests/loops/while_nested_continue_fail.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/operators/compound_bitwise_or_uint_2.sol
View File

@ -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.

2
test/libsolidity/smtCheckerTests/special/block_vars_chc_internal.sol
View File

@ -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

2
test/libsolidity/smtCheckerTests/special/tx_vars_reentrancy_1.sol
View File

@ -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

3
test/libsolidity/smtCheckerTests/types/array_mapping_aliasing_2.sol
View File

@ -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

3
test/libsolidity/smtCheckerTests/types/array_static_mapping_aliasing_2.sol
View File

@ -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

1
test/libsolidity/smtCheckerTests/types/struct/array_struct_array_struct_storage_safe.sol
View File

@ -53,3 +53,4 @@ contract C {
// ====
// SMTEngine: all
// ----
// Warning 6368: (212-217): CHC: Out of bounds access might happen here.

2
test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_2.sol
View File

@ -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 }

2
test/libsolidity/smtCheckerTests/types/struct/struct_aliasing_parameter_storage_3.sol
View File

@ -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()

2
test/libsolidity/smtCheckerTests/unchecked/checked_called_by_unchecked.sol
View File

@ -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)

87
test/libsolidity/smtCheckerTests/userTypes/conversion.sol
View File

@ -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.

35
test/libsolidity/smtCheckerTests/userTypes/conversion_1.sol Normal file
View File

@ -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 || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true)\n(true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true)\n(true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true)\n(true || true || true || true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(MyUInt8.unwrap(f(1)) == 1)\n<errorCode> = 2 -> Assertion failed at assert(MyUInt8.unwrap(f(2)) == 2)\n<errorCode> = 3 -> Assertion failed at assert(MyUInt8.unwrap(f(257)) == 1)\n<errorCode> = 4 -> Assertion failed at assert(MyUInt8.unwrap(f(257)) == 257)\n<errorCode> = 6 -> Assertion failed at assert(MyInt8.unwrap(g(1)) == 1)\n<errorCode> = 7 -> Assertion failed at assert(MyInt8.unwrap(g(2)) == 2)\n<errorCode> = 8 -> Assertion failed at assert(MyInt8.unwrap(g(255)) == -1)\n<errorCode> = 9 -> Assertion failed at assert(MyInt8.unwrap(g(257)) == 1)\n<errorCode> = 10 -> Assertion failed at assert(MyInt8.unwrap(g(257)) == -1)\n

32
test/libsolidity/smtCheckerTests/userTypes/conversion_2.sol Normal file
View File

@ -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(((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true || true)\n(true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true)\n(true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(1))) == 1)\n<errorCode> = 2 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(2))) == 2)\n<errorCode> = 3 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == -1)\n<errorCode> = 4 -> Assertion failed at assert(MyInt8.unwrap(h(MyUInt8.wrap(255))) == 1)\n<errorCode> = 6 -> Assertion failed at assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 250)\n<errorCode> = 7 -> Assertion failed at assert(MyUInt16.unwrap(i(MyUInt8.wrap(250))) == 0)\n

34
test/libsolidity/smtCheckerTests/userTypes/conversion_3.sol Normal file
View File

@ -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(((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true || true || true || true)\n(true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true || true)\n(true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || true || true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true)\n(true || true || true || true || true || true || true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))))\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(j(MyUInt8.wrap(1)) == 1)\n<errorCode> = 2 -> Assertion failed at assert(j(MyUInt8.wrap(2)) == 2)\n<errorCode> = 3 -> Assertion failed at assert(j(MyUInt8.wrap(255)) == 0xff)\n<errorCode> = 4 -> Assertion failed at assert(j(MyUInt8.wrap(255)) == 1)\n<errorCode> = 6 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(1))) == 1)\n<errorCode> = 7 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(2))) == 2)\n<errorCode> = 8 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 0xff)\n<errorCode> = 9 -> Assertion failed at assert(MyUInt16.unwrap(k(MyUInt8.wrap(255))) == 1)\n

23
test/libsolidity/smtCheckerTests/userTypes/conversion_4.sol Normal file
View File

@ -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(((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true || true || true)\n(true || true || ((<errorCode> = 0) && ((:var 0) = (:var 1))) || true || true)\n<errorCode> = 0 -> no errors\n<errorCode> = 1 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(1))) == 1)\n<errorCode> = 2 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(2))) == 2)\n<errorCode> = 3 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 0xff)\n<errorCode> = 4 -> Assertion failed at assert(MyUInt8.unwrap(m(MyUInt16.wrap(255))) == 1)\n