Docker: Update Z3 and cvc5 versions

ethereum · Oct 29, 2024 · faf0f9c · faf0f9c
1 parent 5a1fe0e
commit faf0f9c
Show file tree

Hide file tree

Showing 5 changed files with 87 additions and 64 deletions.
diff --git a/scripts/docker/buildpack-deps/Dockerfile.emscripten b/scripts/docker/buildpack-deps/Dockerfile.emscripten
@@ -33,7 +33,7 @@
 # Using $(em-config CACHE)/sysroot/usr seems to work, though, and still has cmake find the
 # dependencies automatically.
 FROM emscripten/emsdk:3.1.19 AS base
-LABEL version="18"
+LABEL version="19"
 
 ADD emscripten.jam /usr/src
 RUN set -ex && \
@@ -49,7 +49,7 @@ RUN set -ex && \
 # Install Z3
 RUN set -ex && \
 	cd /usr/src && \
-	git clone https://github.com/Z3Prover/z3.git -b z3-4.12.1 --depth 1 && \
+	git clone https://github.com/Z3Prover/z3.git -b z3-4.13.3 --depth 1 && \
 	cd z3 && \
 	mkdir build && \
 	cd build && \
@@ -86,11 +86,11 @@ RUN set -ex && \
 
 # CVC5
 RUN set -ex; \
-	cvc5_version="1.1.2"; \
-	wget "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5_version}/cvc5-Linux-static.zip" -O /opt/cvc5.zip; \
-	test "$(sha256sum /opt/cvc5.zip)" = "cf291aef67da8eaa8d425a51f67f3f72f36db8b1040655dc799b64e3d69e6086  /opt/cvc5.zip"; \
-	unzip /opt/cvc5.zip -x "cvc5-Linux-static/lib/cmake/*" -d /opt; \
-	mv /opt/cvc5-Linux-static/bin/* /usr/bin; \
-	mv /opt/cvc5-Linux-static/include/* /usr/include; \
-	mv /opt/cvc5-Linux-static/lib/* /usr/lib; \
-	rm -rf /opt/cvc5-Linux-static /opt/cvc5.zip;
+	cvc5_version="1.2.0"; \
+	wget "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5_version}/cvc5-Linux-x86_64-static.zip" -O /opt/cvc5.zip; \
+	test "$(sha256sum /opt/cvc5.zip)" = "d18f174ff9a11923c32c3f871f844ed16bd77a28f51050b8e7c8d821c98a1c2e /opt/cvc5.zip"; \
+	unzip /opt/cvc5.zip -x "cvc5-Linux-x86_64-static/lib/cmake/*" -d /opt; \
+	mv /opt/cvc5-Linux-x86_64-static/bin/* /usr/bin; \
+	mv /opt/cvc5-Linux-x86_64-static/include/* /usr/include; \
+	mv /opt/cvc5-Linux-x86_64-static/lib/* /usr/lib; \
+	rm -rf /opt/cvc5-Linux-x86_64-static /opt/cvc5.zip;
diff --git a/scripts/docker/buildpack-deps/Dockerfile.ubuntu.clang.ossfuzz b/scripts/docker/buildpack-deps/Dockerfile.ubuntu.clang.ossfuzz
@@ -22,7 +22,7 @@
 # (c) 2016-2021 solidity contributors.
 #------------------------------------------------------------------------------
 FROM gcr.io/oss-fuzz-base/base-clang:latest as base
-LABEL version="7"
+LABEL version="8"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -59,8 +59,7 @@ RUN apt-get update; \
 		pygments-lexer-solidity \
 		pylint \
 		requests \
-		tabulate \
-		z3-solver;
+		tabulate;
 
 # Install cmake 3.21.2 (minimum requirement is cmake 3.10)
 RUN wget https://github.com/Kitware/CMake/releases/download/v3.21.2/cmake-3.21.2-Linux-x86_64.sh; \
@@ -88,14 +87,14 @@ RUN set -ex; \
 
 # Z3
 RUN set -ex; \
-    git clone --depth 1 -b z3-4.12.1 https://github.com/Z3Prover/z3.git \
+    git clone --depth 1 -b z3-4.13.3 https://github.com/Z3Prover/z3.git \
     /usr/src/z3; \
     cd /usr/src/z3; \
     mkdir build; \
     cd build; \
     LDFLAGS=$CXXFLAGS cmake -DZ3_BUILD_LIBZ3_SHARED=OFF -DCMAKE_INSTALL_PREFIX=/usr \
     -DCMAKE_BUILD_TYPE=Release ..; \
-    make libz3 -j; \
+    make z3 -j; \
     make install; \
     rm -rf /usr/src/z3
 
@@ -111,14 +110,14 @@ RUN set -ex; \
 
 # CVC5
 RUN set -ex; \
-	cvc5_version="1.1.2"; \
-	wget "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5_version}/cvc5-Linux-static.zip" -O /opt/cvc5.zip; \
-	test "$(sha256sum /opt/cvc5.zip)" = "cf291aef67da8eaa8d425a51f67f3f72f36db8b1040655dc799b64e3d69e6086  /opt/cvc5.zip"; \
-	unzip /opt/cvc5.zip -x "cvc5-Linux-static/lib/cmake/*" -d /opt; \
-	mv /opt/cvc5-Linux-static/bin/* /usr/bin; \
-	mv /opt/cvc5-Linux-static/include/* /usr/include; \
-	mv /opt/cvc5-Linux-static/lib/* /usr/lib; \
-	rm -rf /opt/cvc5-Linux-static /opt/cvc5.zip;
+	cvc5_version="1.2.0"; \
+	wget "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5_version}/cvc5-Linux-x86_64-static.zip" -O /opt/cvc5.zip; \
+	test "$(sha256sum /opt/cvc5.zip)" = "d18f174ff9a11923c32c3f871f844ed16bd77a28f51050b8e7c8d821c98a1c2e  /opt/cvc5.zip"; \
+	unzip /opt/cvc5.zip -x "cvc5-Linux-x86_64-static/lib/cmake/*" -d /opt; \
+	mv /opt/cvc5-Linux-x86_64-static/bin/* /usr/bin; \
+	mv /opt/cvc5-Linux-x86_64-static/include/* /usr/include; \
+	mv /opt/cvc5-Linux-x86_64-static/lib/* /usr/lib; \
+	rm -rf /opt/cvc5-Linux-x86_64-static /opt/cvc5.zip;
 
 # OSSFUZZ: libprotobuf-mutator
 RUN set -ex; \

diff --git a/scripts/docker/buildpack-deps/Dockerfile.ubuntu2004 b/scripts/docker/buildpack-deps/Dockerfile.ubuntu2004
@@ -22,7 +22,7 @@
 # (c) 2016-2019 solidity contributors.
 #------------------------------------------------------------------------------
 FROM buildpack-deps:focal AS base
-LABEL version="25"
+LABEL version="26"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -39,15 +39,13 @@ RUN set -ex; \
 		libboost-program-options-dev \
 		libboost-system-dev \
 		libboost-test-dev \
-		libz3-static-dev \
 		lsof \
 		ninja-build \
 		python3-pip \
 		python3-sphinx \
 		software-properties-common \
 		sudo \
-		unzip \
-		z3-static; \
+		unzip; \
 	pip3 install \
 		codecov \
 		colorama \
@@ -56,8 +54,7 @@ RUN set -ex; \
 		pygments-lexer-solidity \
 		pylint \
 		requests \
-		tabulate \
-		z3-solver;
+		tabulate;
 
 # TODO: we could eliminate duplication by using a Dockerfile extension like:
 # https://github.com/edrevo/dockerfile-plus?tab=readme-ov-file#dockerfile
@@ -76,14 +73,27 @@ RUN set -ex; \
 
 # CVC5
 RUN set -ex; \
-	cvc5_version="1.1.2"; \
-	wget "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5_version}/cvc5-Linux-static.zip" -O /opt/cvc5.zip; \
-	test "$(sha256sum /opt/cvc5.zip)" = "cf291aef67da8eaa8d425a51f67f3f72f36db8b1040655dc799b64e3d69e6086  /opt/cvc5.zip"; \
-	unzip /opt/cvc5.zip -x "cvc5-Linux-static/lib/cmake/*" -d /opt; \
-	mv /opt/cvc5-Linux-static/bin/* /usr/bin; \
-	mv /opt/cvc5-Linux-static/include/* /usr/include; \
-	mv /opt/cvc5-Linux-static/lib/* /usr/lib; \
-	rm -rf /opt/cvc5-Linux-static /opt/cvc5.zip;
+	cvc5_version="1.2.0"; \
+	wget "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5_version}/cvc5-Linux-x86_64-static.zip" -O /opt/cvc5.zip; \
+	test "$(sha256sum /opt/cvc5.zip)" = "d18f174ff9a11923c32c3f871f844ed16bd77a28f51050b8e7c8d821c98a1c2e  /opt/cvc5.zip"; \
+	unzip /opt/cvc5.zip -x "cvc5-Linux-x86_64-static/lib/cmake/*" -d /opt; \
+	mv /opt/cvc5-Linux-x86_64-static/bin/* /usr/bin; \
+	mv /opt/cvc5-Linux-x86_64-static/include/* /usr/include; \
+	mv /opt/cvc5-Linux-x86_64-static/lib/* /usr/lib; \
+	rm -rf /opt/cvc5-Linux-x86_64-static /opt/cvc5.zip;
+
+# Z3
+RUN set -ex; \
+    git clone --depth 1 -b z3-4.13.3 https://github.com/Z3Prover/z3.git \
+    /usr/src/z3; \
+    cd /usr/src/z3; \
+    mkdir build; \
+    cd build; \
+    LDFLAGS=$CXXFLAGS cmake -DZ3_BUILD_LIBZ3_SHARED=OFF -DCMAKE_INSTALL_PREFIX=/usr \
+    -DCMAKE_BUILD_TYPE=Release ..; \
+    make shell -j; \
+    make install; \
+    rm -rf /usr/src/z3
 
 FROM base AS libraries
 

diff --git a/scripts/docker/buildpack-deps/Dockerfile.ubuntu2404 b/scripts/docker/buildpack-deps/Dockerfile.ubuntu2404
@@ -22,7 +22,7 @@
 # (c) 2016-2024 solidity contributors.
 #------------------------------------------------------------------------------
 FROM buildpack-deps:noble AS base
-LABEL version="1"
+LABEL version="2"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -44,7 +44,6 @@ RUN set -ex; \
 		libboost-system-dev \
 		libboost-test-dev \
 		libcln-dev \
-		libz3-static-dev \
 		locales-all \
 		lsof \
 		ninja-build \
@@ -53,7 +52,6 @@ RUN set -ex; \
 		software-properties-common \
 		sudo \
 		unzip \
-		z3-static \
 		zip; \
 	pip3 install \
 		codecov \
@@ -63,8 +61,7 @@ RUN set -ex; \
 		pygments-lexer-solidity \
 		pylint \
 		requests \
-		tabulate \
-		z3-solver;
+		tabulate;
 
 # Eldarica
 RUN set -ex; \
@@ -79,14 +76,21 @@ RUN set -ex; \
 
 # CVC5
 RUN set -ex; \
-	cvc5_version="1.1.2"; \
-	wget "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5_version}/cvc5-Linux-static.zip" -O /opt/cvc5.zip; \
-	test "$(sha256sum /opt/cvc5.zip)" = "cf291aef67da8eaa8d425a51f67f3f72f36db8b1040655dc799b64e3d69e6086  /opt/cvc5.zip"; \
-	unzip /opt/cvc5.zip -x "cvc5-Linux-static/lib/cmake/*" -d /opt; \
-	mv /opt/cvc5-Linux-static/bin/* /usr/bin; \
-	mv /opt/cvc5-Linux-static/include/* /usr/include; \
-	mv /opt/cvc5-Linux-static/lib/* /usr/lib; \
-	rm -rf /opt/cvc5-Linux-static /opt/cvc5.zip;
+	cvc5_version="1.2.0"; \
+        cvc5_archive_name="cvc5-Linux-x86_64-static"; \
+	wget "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5_version}/${cvc5_archive_name}.zip" -O /opt/cvc5.zip; \
+	test "$(sha256sum /opt/cvc5.zip)" = "d18f174ff9a11923c32c3f871f844ed16bd77a28f51050b8e7c8d821c98a1c2e  /opt/cvc5.zip"; \
+	unzip -j /opt/cvc5.zip "${cvc5_archive_name}/bin/cvc5" -d /usr/bin; \
+	rm -f /opt/cvc5.zip;
+
+# Z3
+RUN set -ex; \
+    z3_version="4.13.3"; \
+    z3_archive_name="z3-${z3_version}-x64-glibc-2.35"; \
+    wget "https://github.com/Z3Prover/z3/releases/download/z3-${z3_version}/${z3_archive_name}.zip" -O /opt/z3.zip; \
+    test "$(sha256sum /opt/z3.zip)" = "32c7377026733c9d7b33c21cd77a68f50ba682367207b031a6bfd80140a8722f  /opt/z3.zip"; \
+    unzip -j /opt/z3.zip "${z3_archive_name}/bin/z3" -d /usr/bin; \
+    rm -f /opt/z3.zip;
 
 FROM base AS libraries
 

diff --git a/scripts/docker/buildpack-deps/Dockerfile.ubuntu2404.clang b/scripts/docker/buildpack-deps/Dockerfile.ubuntu2404.clang
@@ -22,7 +22,7 @@
 # (c) 2016-2024 solidity contributors.
 #------------------------------------------------------------------------------
 FROM buildpack-deps:noble AS base
-LABEL version="2"
+LABEL version="3"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -46,13 +46,11 @@ RUN set -ex; \
 		libboost-test-dev \
 		libclang-rt-dev \
 		libcln-dev \
-		libz3-static-dev \
 		lsof \
 		ninja-build \
 		python3-pip \
 		software-properties-common \
-		sudo \
-		z3-static; \
+		sudo; \
 	pip3 install \
 		codecov \
 		colorama \
@@ -61,8 +59,7 @@ RUN set -ex; \
 		pygments-lexer-solidity \
 		pylint \
 		requests \
-		tabulate \
-		z3-solver;
+		tabulate;
 
 # Eldarica
 RUN set -ex; \
@@ -78,14 +75,27 @@ RUN set -ex; \
 
 # CVC5
 RUN set -ex; \
-	cvc5_version="1.1.2"; \
-	wget "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5_version}/cvc5-Linux-static.zip" -O /opt/cvc5.zip; \
-	test "$(sha256sum /opt/cvc5.zip)" = "cf291aef67da8eaa8d425a51f67f3f72f36db8b1040655dc799b64e3d69e6086  /opt/cvc5.zip"; \
-	unzip /opt/cvc5.zip -x "cvc5-Linux-static/lib/cmake/*" -d /opt; \
-	mv /opt/cvc5-Linux-static/bin/* /usr/bin; \
-	mv /opt/cvc5-Linux-static/lib/* /usr/lib; \
-	mv /opt/cvc5-Linux-static/include/* /usr/include; \
-	rm -rf /opt/cvc5-Linux-static /opt/cvc5.zip;
+	cvc5_version="1.2.0"; \
+	wget "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5_version}/cvc5-Linux-x86_64-static.zip" -O /opt/cvc5.zip; \
+	test "$(sha256sum /opt/cvc5.zip)" = "d18f174ff9a11923c32c3f871f844ed16bd77a28f51050b8e7c8d821c98a1c2e  /opt/cvc5.zip"; \
+	unzip /opt/cvc5.zip -x "cvc5-Linux-x86_64-static/lib/cmake/*" -d /opt; \
+	mv /opt/cvc5-Linux-x86_64-static/bin/* /usr/bin; \
+	mv /opt/cvc5-Linux-x86_64-static/lib/* /usr/lib; \
+	mv /opt/cvc5-Linux-x86_64-static/include/* /usr/include; \
+	rm -rf /opt/cvc5-Linux-x86_64-static /opt/cvc5.zip;
+
+# Z3
+RUN set -ex; \
+    git clone --depth 1 -b z3-4.13.3 https://github.com/Z3Prover/z3.git \
+    /usr/src/z3; \
+    cd /usr/src/z3; \
+    mkdir build; \
+    cd build; \
+    LDFLAGS=$CXXFLAGS cmake -DZ3_BUILD_LIBZ3_SHARED=OFF -DCMAKE_INSTALL_PREFIX=/usr \
+    -DCMAKE_BUILD_TYPE=Release ..; \
+    make shell -j; \
+    make install; \
+    rm -rf /usr/src/z3
 
 FROM base AS libraries