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

Merge pull request #14076 from ethereum/update_z3_tests

Browse Source 
Update z3 tests
This commit is contained in:
Leo 2023-03-29 10:35:39 +02:00 committed by GitHub
commit bca3fb8ffd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 23 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
.circleci/config.yml
View File

@ -9,24 +9,24 @@ version: 2.1
parameters: parameters:
ubuntu-2004-docker-image: ubuntu-2004-docker-image:
type: string type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-16 # solbuildpackpusher/solidity-buildpack-deps:ubuntu2004-17
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:ee1def5806f40c35d583234e172ec5769bb9a08b6f5bbc713c1a2658846dbced" default: "solbuildpackpusher/solidity-buildpack-deps@sha256:87c63f4c0e9be15b60417809cd3245892db281af0f80ed7378a1978f6f170029"
ubuntu-2204-docker-image: ubuntu-2204-docker-image:
type: string type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2204-1 # solbuildpackpusher/solidity-buildpack-deps:ubuntu2204-2
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:07419ed58537cbca9d4c30701fb84f6bb517ce2fce7f3b5dccb3db8bf1c30183" default: "solbuildpackpusher/solidity-buildpack-deps@sha256:7f0b62da2aa0920660e67cd17fb3a7f6c57d7da72454003056f3bd27bbda2075"
ubuntu-2204-clang-docker-image: ubuntu-2204-clang-docker-image:
type: string type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu2204.clang-1 # solbuildpackpusher/solidity-buildpack-deps:ubuntu2204.clang-2
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:e515710752bfb38ee0e9b2f92ca71612c03ed85290c36c3b3c0a3d9f90187aef" default: "solbuildpackpusher/solidity-buildpack-deps@sha256:0d4fa1da806f9b3daabd2d1dc0842899af794a838e475c14045c3fb289cc8103"
ubuntu-1604-clang-ossfuzz-docker-image: ubuntu-1604-clang-ossfuzz-docker-image:
type: string type: string
# solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-22 # solbuildpackpusher/solidity-buildpack-deps:ubuntu1604.clang.ossfuzz-23
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:baf46ad78b131eb6b0bf98d50e9330437a338c6893b53af3853b36f6f4ab18ae" default: "solbuildpackpusher/solidity-buildpack-deps@sha256:7a84f67829ec2fdcfc8a61ebf22f9dc27b04a9edeb1531565ab3e0ebb1cbc4a0"
emscripten-docker-image: emscripten-docker-image:
type: string type: string
# solbuildpackpusher/solidity-buildpack-deps:emscripten-14 # solbuildpackpusher/solidity-buildpack-deps:emscripten-15
default: "solbuildpackpusher/solidity-buildpack-deps@sha256:d7d4ec28cdc3e61fc6a048b88ebdff1c5e67f3353cf1739cbaea07ec2481eb16" default: "solbuildpackpusher/solidity-buildpack-deps@sha256:e2729bd6c0734bb49d04e2688fec3dcf880394f351f69358dd2bd92c0f6fd309"
evm-version: evm-version:
type: string type: string
default: london default: london

4
.circleci/osx_install_dependencies.sh
View File

@ -61,11 +61,11 @@ then
./scripts/install_obsolete_jsoncpp_1_7_4.sh ./scripts/install_obsolete_jsoncpp_1_7_4.sh
# z3 # z3
z3_version="4.11.2" z3_version="4.12.1"
z3_dir="z3-${z3_version}-x64-osx-10.16" z3_dir="z3-${z3_version}-x64-osx-10.16"
z3_package="${z3_dir}.zip" z3_package="${z3_dir}.zip"
wget "https://github.com/Z3Prover/z3/releases/download/z3-${z3_version}/${z3_package}" wget "https://github.com/Z3Prover/z3/releases/download/z3-${z3_version}/${z3_package}"
validate_checksum "$z3_package" a56b6c40d9251a963aabe1f15731dd88ad1cb801d0e7b16e45f8b232175e165c validate_checksum "$z3_package" 7601f844de6d906235140d0f76cca58be7ac716f3e2c29c35845aa24b24f73b9
unzip "$z3_package" unzip "$z3_package"
rm "$z3_package" rm "$z3_package"
cp "${z3_dir}/bin/libz3.a" /usr/local/lib cp "${z3_dir}/bin/libz3.a" /usr/local/lib

2
CMakeLists.txt
View File

@ -75,7 +75,7 @@ configure_file("${CMAKE_SOURCE_DIR}/cmake/templates/license.h.in" include/licens
include(EthOptions) include(EthOptions)
configure_project(TESTS) configure_project(TESTS)
set(LATEST_Z3_VERSION "4.11.2") set(LATEST_Z3_VERSION "4.12.1")
set(MINIMUM_Z3_VERSION "4.8.16") set(MINIMUM_Z3_VERSION "4.8.16")
find_package(Z3) find_package(Z3)
if (${Z3_FOUND}) if (${Z3_FOUND})

4
scripts/build_emscripten.sh
View File

@ -33,9 +33,9 @@ if (( $# != 0 )); then
params="$(printf "%q " "${@}")" params="$(printf "%q " "${@}")"
fi fi
# solbuildpackpusher/solidity-buildpack-deps:emscripten-14 # solbuildpackpusher/solidity-buildpack-deps:emscripten-15
# NOTE: Without `safe.directory` git would assume it's not safe to operate on /root/project since it's owned by a different user. # NOTE: Without `safe.directory` git would assume it's not safe to operate on /root/project since it's owned by a different user.
# See https://github.blog/2022-04-12-git-security-vulnerability-announced/ # See https://github.blog/2022-04-12-git-security-vulnerability-announced/
docker run -v "$(pwd):/root/project" -w /root/project \ docker run -v "$(pwd):/root/project" -w /root/project \
solbuildpackpusher/solidity-buildpack-deps@sha256:d7d4ec28cdc3e61fc6a048b88ebdff1c5e67f3353cf1739cbaea07ec2481eb16 \ solbuildpackpusher/solidity-buildpack-deps@sha256:f86cb1fb4631b1fbb927149f60caea7b095be5b85d379456eee09cb105e7f225 \
/bin/bash -c "git config --global --add safe.directory /root/project && ./scripts/ci/build_emscripten.sh ${params}" /bin/bash -c "git config --global --add safe.directory /root/project && ./scripts/ci/build_emscripten.sh ${params}"

4
test/libsolidity/smtCheckerTests/array_members/push_storage_ref_unsafe_length.sol
View File

@ -28,8 +28,8 @@ contract C {
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// ---- // ----
// Warning 6368: (238-242): CHC: Out of bounds access happens here. // Warning 6368: (238-242): CHC: Out of bounds access happens here.
// Warning 6368: (238-245): CHC: Out of bounds access might happen here. // Warning 6368: (238-245): CHC: Out of bounds access happens here.
// Warning 6368: (238-248): CHC: Out of bounds access might happen here. // Warning 6368: (238-248): CHC: Out of bounds access happens here.
// Warning 6368: (311-315): CHC: Out of bounds access happens here. // Warning 6368: (311-315): CHC: Out of bounds access happens here.
// Warning 6368: (343-347): CHC: Out of bounds access happens here. // Warning 6368: (343-347): CHC: Out of bounds access happens here.
// Warning 6328: (336-360): CHC: Assertion violation happens here. // Warning 6328: (336-360): CHC: Assertion violation happens here.

3
test/libsolidity/smtCheckerTests/deployment/deploy_trusted_flow.sol
View File

@ -24,9 +24,8 @@ contract C {
// Warning 6328: (167-185): CHC: Assertion violation might happen here. // Warning 6328: (167-185): CHC: Assertion violation might happen here.
// Warning 6328: (215-233): CHC: Assertion violation might happen here. // Warning 6328: (215-233): CHC: Assertion violation might happen here.
// Warning 6328: (267-285): CHC: Assertion violation might happen here. // Warning 6328: (267-285): CHC: Assertion violation might happen here.
// Warning 6328: (304-322): CHC: Assertion violation might happen here. // Warning 6328: (304-322): CHC: Assertion violation happens here.
// Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here. // Warning 2661: (47-50): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (167-185): BMC: Assertion violation happens here. // Warning 4661: (167-185): BMC: Assertion violation happens here.
// Warning 4661: (215-233): BMC: Assertion violation happens here. // Warning 4661: (215-233): BMC: Assertion violation happens here.
// Warning 4661: (267-285): BMC: Assertion violation happens here. // Warning 4661: (267-285): BMC: Assertion violation happens here.
// Warning 4661: (304-322): BMC: Assertion violation happens here.

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

@ -18,6 +18,4 @@ contract C {
// SMTEngine: all // SMTEngine: all
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// ---- // ----
// Warning 6328: (167-181): CHC: Assertion violation might happen here. // Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Warning 4661: (167-181): BMC: Assertion violation happens here.

1
test/libsolidity/smtCheckerTests/operators/index_access_side_effect.sol
View File

@ -21,6 +21,7 @@ contract C {
// ==== // ====
// SMTEngine: all // SMTEngine: all
// SMTIgnoreCex: yes // SMTIgnoreCex: yes
// SMTIgnoreOS: macos
// ---- // ----
// Warning 6328: (335-354): CHC: Assertion violation might happen here. // Warning 6328: (335-354): CHC: Assertion violation might happen here.
// Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Info 1391: CHC: 3 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

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

@ -34,6 +34,7 @@ contract C
// ==== // ====
// SMTEngine: all // SMTEngine: all
// SMTIgnoreCex: yes // SMTIgnoreCex: yes
// SMTIgnoreOS: macos
// ---- // ----
// Warning 6368: (439-453): CHC: Out of bounds access happens here. // 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: (465-480): CHC: Out of bounds access might happen here.

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

@ -34,5 +34,4 @@ contract C
// Warning 6368: (612-627): 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 6328: (860-880): CHC: Assertion violation happens here.
// Warning 6368: (936-952): CHC: Out of bounds access might happen 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 1391: CHC: 7 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
// Info 1391: CHC: 6 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.

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

@ -32,6 +32,5 @@ contract C {
// SMTEngine: all // SMTEngine: all
// SMTIgnoreOS: macos // SMTIgnoreOS: macos
// ---- // ----
// Warning 6368: (374-381): CHC: Out of bounds access might happen here.
// Warning 6368: (456-462): CHC: Out of bounds access happens here. // Warning 6368: (456-462): CHC: Out of bounds access happens here.
// Info 1391: CHC: 12 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. // Info 1391: CHC: 13 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.