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 #8939 from ethereum/updateZ3

Browse Source 
Update z3 to version 4.8.8.
This commit is contained in:
chriseth 2020-05-14 16:36:49 +02:00 committed by GitHub
commit b71a3f1f1d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
22 changed files with 50 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
.circleci/config.yml
View File

@ -12,10 +12,10 @@ parameters:
default: "4" default: "4"
ubuntu-2004-docker-image-rev: ubuntu-2004-docker-image-rev:
type: string type: string
default: "1" default: "2"
ubuntu-2004-clang-docker-image-rev: ubuntu-2004-clang-docker-image-rev:
type: string type: string
default: "1" default: "2"
ubuntu-1604-clang-ossfuzz-docker-image-rev: ubuntu-1604-clang-ossfuzz-docker-image-rev:
type: string type: string
default: "2" default: "2"

5
.circleci/docker/Dockerfile.ubuntu2004
View File

@ -26,6 +26,9 @@ FROM buildpack-deps:focal AS base
ARG DEBIAN_FRONTEND=noninteractive ARG DEBIAN_FRONTEND=noninteractive
RUN set -ex; \ RUN set -ex; \
dist=$(grep DISTRIB_CODENAME /etc/lsb-release | cut -d= -f2); \
echo "deb http://ppa.launchpad.net/ethereum/cpp-build-deps/ubuntu $dist main" >> /etc/apt/sources.list ; \
apt-key adv --keyserver keyserver.ubuntu.com --recv-keys 1c52189c923f6ca9 ; \
apt-get update; \ apt-get update; \
apt-get install -qqy --no-install-recommends \ apt-get install -qqy --no-install-recommends \
build-essential \ build-essential \
@ -33,7 +36,7 @@ RUN set -ex; \
cmake ninja-build \ cmake ninja-build \
libboost-filesystem-dev libboost-test-dev libboost-system-dev \ libboost-filesystem-dev libboost-test-dev libboost-system-dev \
libboost-program-options-dev \ libboost-program-options-dev \
libcvc4-dev z3 libz3-dev \ libcvc4-dev libz3-static-dev \
; \ ; \
apt-get install -qy python3-pip python3-sphinx; \ apt-get install -qy python3-pip python3-sphinx; \
pip3 install codecov; \ pip3 install codecov; \

7
.circleci/docker/Dockerfile.ubuntu2004.clang
View File

@ -26,6 +26,9 @@ FROM buildpack-deps:focal AS base
ARG DEBIAN_FRONTEND=noninteractive ARG DEBIAN_FRONTEND=noninteractive
RUN set -ex; \ RUN set -ex; \
dist=$(grep DISTRIB_CODENAME /etc/lsb-release | cut -d= -f2); \
echo "deb http://ppa.launchpad.net/ethereum/cpp-build-deps/ubuntu $dist main" >> /etc/apt/sources.list ; \
apt-key adv --keyserver keyserver.ubuntu.com --recv-keys 1c52189c923f6ca9 ; \
apt-get update; \ apt-get update; \
apt-get install -qqy --no-install-recommends \ apt-get install -qqy --no-install-recommends \
build-essential \ build-essential \
@ -33,8 +36,8 @@ RUN set -ex; \
cmake ninja-build \ cmake ninja-build \
libboost-filesystem-dev libboost-test-dev libboost-system-dev \ libboost-filesystem-dev libboost-test-dev libboost-system-dev \
libboost-program-options-dev \ libboost-program-options-dev \
clang llvm-dev \ clang \
z3 libz3-dev \ libz3-static-dev \
; \ ; \
rm -rf /var/lib/apt/lists/* rm -rf /var/lib/apt/lists/*

14
.circleci/osx_install_dependencies.sh
View File

@ -43,13 +43,13 @@ then
./scripts/install_obsolete_jsoncpp_1_7_4.sh ./scripts/install_obsolete_jsoncpp_1_7_4.sh
# z3 # z3
wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x64-osx-10.14.6.zip wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.8/z3-4.8.8-x64-osx-10.14.6.zip
unzip z3-4.8.7-x64-osx-10.14.6.zip unzip z3-4.8.8-x64-osx-10.14.6.zip
rm -f z3-4.8.7-x64-osx-10.14.6.zip rm -f z3-4.8.8-x64-osx-10.14.6.zip
cp z3-4.8.7-x64-osx-10.14.6/bin/libz3.a /usr/local/lib cp z3-4.8.8-x64-osx-10.14.6/bin/libz3.a /usr/local/lib
cp z3-4.8.7-x64-osx-10.14.6/bin/z3 /usr/local/bin cp z3-4.8.8-x64-osx-10.14.6/bin/z3 /usr/local/bin
cp z3-4.8.7-x64-osx-10.14.6/include/* /usr/local/include cp z3-4.8.8-x64-osx-10.14.6/include/* /usr/local/include
rm -rf z3-4.8.7-x64-osx-10.14.6 rm -rf z3-4.8.8-x64-osx-10.14.6
# evmone # evmone
wget https://github.com/ethereum/evmone/releases/download/v0.4.0/evmone-0.4.0-darwin-x86_64.tar.gz wget https://github.com/ethereum/evmone/releases/download/v0.4.0/evmone-0.4.0-darwin-x86_64.tar.gz

14
scripts/deps-ppa/static_z3.sh
View File

@ -25,11 +25,9 @@ set -ev
keyid=70D110489D66E2F6 keyid=70D110489D66E2F6
email=builds@ethereum.org email=builds@ethereum.org
packagename=libz3-static-dev packagename=libz3-static-dev
# On the next version the git cherry-pick below should be removed and the patch suffix removed from the version string. version=4.8.8
version=4.8.7
version_patchsuffix=-1
DISTRIBUTIONS="bionic disco eoan focal" DISTRIBUTIONS="bionic eoan focal"
for distribution in $DISTRIBUTIONS for distribution in $DISTRIBUTIONS
do do
@ -44,10 +42,8 @@ ppafilesurl=https://launchpad.net/~ethereum/+archive/ubuntu/${pparepo}/+files
# Fetch source # Fetch source
git clone --branch z3-${version} https://github.com/Z3Prover/z3.git git clone --branch z3-${version} https://github.com/Z3Prover/z3.git
cd z3 cd z3
# Patch build failure.
git cherry-pick e212159f4e
debversion="${version}${version_patchsuffix}" debversion="${version}"
CMAKE_OPTIONS="-DZ3_BUILD_LIBZ3_SHARED=OFF -DCMAKE_BUILD_TYPE=Release" CMAKE_OPTIONS="-DZ3_BUILD_LIBZ3_SHARED=OFF -DCMAKE_BUILD_TYPE=Release"
@ -181,7 +177,7 @@ This program is free software: you can redistribute it and/or modify
Public License version 3 can be found in "/usr/share/common-licenses/GPL-3". Public License version 3 can be found in "/usr/share/common-licenses/GPL-3".
EOF EOF
cat <<EOF > debian/changelog cat <<EOF > debian/changelog
libz3-static-dev (0.0.1-2ubuntu0) saucy; urgency=low libz3-static-dev (0.0.1-1ubuntu0) saucy; urgency=low
* Initial release. * Initial release.
@ -191,7 +187,7 @@ mkdir debian/source
echo "3.0 (quilt)" > debian/source/format echo "3.0 (quilt)" > debian/source/format
chmod +x debian/rules chmod +x debian/rules
versionsuffix=2ubuntu0~${distribution} versionsuffix=1ubuntu0~${distribution}
EMAIL="$email" dch -v 1:${debversion}-${versionsuffix} "build of ${version}" EMAIL="$email" dch -v 1:${debversion}-${versionsuffix} "build of ${version}"
# build source package # build source package

6
scripts/release_ppa.sh
View File

@ -55,9 +55,9 @@ keyid=70D110489D66E2F6
email=builds@ethereum.org email=builds@ethereum.org
packagename=solc packagename=solc
static_build_distribution=disco static_build_distribution=focal
DISTRIBUTIONS="bionic disco eoan focal" DISTRIBUTIONS="bionic eoan focal"
if is_release if is_release
then then
@ -85,7 +85,7 @@ else
fi fi
if [ $distribution = focal ] if [ $distribution = focal ]
then then
SMTDEPENDENCY="libz3-dev, SMTDEPENDENCY="libz3-static-dev,
libcvc4-dev, libcvc4-dev,
" "
elif [ $distribution = disco ] elif [ $distribution = disco ]

1
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_memory.sol
View File

@ -19,5 +19,4 @@ contract LoopFor2 {
} }
} }
// ---- // ----
// Warning: (316-336): Assertion violation happens here
// Warning: (363-382): Assertion violation happens here // Warning: (363-382): Assertion violation happens here

1
test/libsolidity/smtCheckerTests/loops/for_loop_array_assignment_storage_storage.sol
View File

@ -19,6 +19,5 @@ contract LoopFor2 {
} }
} }
// ---- // ----
// Warning: (317-337): Assertion violation happens here
// Warning: (341-360): Assertion violation happens here // Warning: (341-360): Assertion violation happens here
// Warning: (364-383): Assertion violation happens here // Warning: (364-383): Assertion violation happens here

1
test/libsolidity/smtCheckerTests/loops/while_loop_array_assignment_storage_storage.sol
View File

@ -21,6 +21,5 @@ contract LoopFor2 {
} }
} }
// ---- // ----
// Warning: (296-316): Assertion violation happens here
// Warning: (320-339): Assertion violation happens here // Warning: (320-339): Assertion violation happens here
// Warning: (343-362): Assertion violation happens here // Warning: (343-362): Assertion violation happens here

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

@ -9,4 +9,6 @@ contract C {
} }
} }
// ---- // ----
// Warning: (129-143): Error trying to invoke SMT solver.
// Warning: (147-161): Error trying to invoke SMT solver.
// Warning: (147-161): Assertion violation happens here // Warning: (147-161): Assertion violation happens here

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

@ -10,4 +10,6 @@ contract C {
} }
} }
// ---- // ----
// Warning: (163-184): Error trying to invoke SMT solver.
// Warning: (188-209): Error trying to invoke SMT solver.
// Warning: (188-209): Assertion violation happens here // Warning: (188-209): Assertion violation happens here

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

@ -10,4 +10,6 @@ contract C {
} }
} }
// ---- // ----
// Warning: (171-190): Error trying to invoke SMT solver.
// Warning: (194-213): Error trying to invoke SMT solver.
// Warning: (194-213): Assertion violation happens here // Warning: (194-213): Assertion violation happens here

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

@ -16,4 +16,3 @@ contract C
// ==== // ====
// SMTSolvers: z3 // SMTSolvers: z3
// ---- // ----
// Warning: (174-194): Assertion violation happens here

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

@ -6,3 +6,5 @@ contract C {
assert(x / y == 3); assert(x / y == 3);
} }
} }
// ----
// Warning: (107-125): Error trying to invoke SMT solver.

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

@ -6,3 +6,5 @@ contract C {
assert(x / y == 3); assert(x / y == 3);
} }
} }
// ----
// Warning: (105-123): Error trying to invoke SMT solver.

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

@ -6,3 +6,5 @@ contract C {
assert(x / y == -3); assert(x / y == -3);
} }
} }
// ----
// Warning: (106-125): Error trying to invoke SMT solver.

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

@ -6,3 +6,5 @@ contract C {
assert(x / y == -3); assert(x / y == -3);
} }
} }
// ----
// Warning: (106-125): Error trying to invoke SMT solver.

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

@ -6,3 +6,5 @@ contract C {
assert(x / y == 3); assert(x / y == 3);
} }
} }
// ----
// Warning: (107-125): Error trying to invoke SMT solver.

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

@ -8,3 +8,5 @@ contract C {
assert(z1 == z2); assert(z1 == z2);
} }
} }
// ----
// Warning: (166-182): Error trying to invoke SMT solver.

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

@ -8,3 +8,5 @@ contract C
assert((y % 2) == 0); assert((y % 2) == 0);
} }
} }
// ----
// Warning: (122-142): Error trying to invoke SMT solver.

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

@ -8,3 +8,5 @@ contract C
assert(z < y); assert(z < y);
} }
} }
// ----
// Warning: (126-139): Error trying to invoke SMT solver.

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

@ -8,3 +8,5 @@ contract C
assert(z < 100_000); assert(z < 100_000);
} }
} }
// ----
// Warning: (130-149): Error trying to invoke SMT solver.