Merge pull request #15102 from ethereum/install-cvc5

Install cvc5 in buildpack-deps
ethereum · Jun 11, 2024 · e4a4c57 · e4a4c57
2 parents 0f98226 + 128b172
commit e4a4c57
Show file tree

Hide file tree

Showing 6 changed files with 86 additions and 15 deletions.
diff --git a/.circleci/osx_install_dependencies.sh b/.circleci/osx_install_dependencies.sh
@@ -84,6 +84,16 @@ then
   sudo mv /tmp/eldarica/{eld,eld-client,target,eldEnv} /usr/local/bin
   rm -rf /tmp/{eldarica,eld_binaries.zip}
 
+  #cvc5
+  cvc5_version="1.1.2"
+  wget "https://github.com/cvc5/cvc5/releases/download/cvc5-${cvc5_version}/cvc5-macOS-arm64-static.zip" -O /tmp/cvc5.zip
+  validate_checksum /tmp/cvc5.zip 2017d683d924676cb713865c6d4fcf70115c65b7ec2848f242ab938902f115b5
+  unzip /tmp/cvc5.zip -x "cvc5-macOS-arm64-static/lib/cmake/*" -d /tmp
+  sudo mv /tmp/cvc5-macOS-arm64-static/bin/* /usr/local/bin
+  sudo mv /tmp/cvc5-macOS-arm64-static/include/* /usr/local/include
+  sudo mv /tmp/cvc5-macOS-arm64-static/lib/* /usr/local/lib
+  rm -rf /tmp/{cvc5-macOS-arm64-static,cvc5.zip}
+
   # z3
   z3_version="4.12.1"
   z3_dir="z3-z3-$z3_version"

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="17"
+LABEL version="18"
 
 ADD emscripten.jam /usr/src
 RUN set -ex && \
@@ -44,8 +44,10 @@ RUN set -ex && \
 		python3 \
 		python3-pip \
 		sudo && \
-	pip3 install requests && \
-	\
+	pip3 install requests;
+
+# Install Z3
+RUN set -ex && \
 	cd /usr/src && \
 	git clone https://github.com/Z3Prover/z3.git -b z3-4.12.1 --depth 1 && \
 	cd z3 && \
@@ -63,9 +65,11 @@ RUN set -ex && \
 		.. && \
 	make && \
 	make install && \
-	rm -r /usr/src/z3 && \
+	rm -r /usr/src/z3
+
+# Install Boost
+RUN set -ex && \
 	cd /usr/src && \
-	\
 	wget -q 'https://boostorg.jfrog.io/artifactory/main/release/1.75.0/source/boost_1_75_0.tar.bz2' -O boost.tar.bz2 && \
 	test "$(sha256sum boost.tar.bz2)" = "953db31e016db7bb207f11432bef7df100516eeb746843fa0486a222e3fd49cb  boost.tar.bz2" && \
 	tar -xf boost.tar.bz2 && \
@@ -79,3 +83,14 @@ RUN set -ex && \
 		cxxflags="-s DISABLE_EXCEPTION_CATCHING=0 -Wno-unused-local-typedef -Wno-variadic-macros -Wno-c99-extensions -Wno-all" \
 	       --prefix=$(em-config CACHE)/sysroot/usr install && \
 	rm -r /usr/src/boost_1_75_0
+
+# 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;
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="6"
+LABEL version="7"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -109,6 +109,17 @@ RUN set -ex; \
 	unzip /opt/eld_binaries.zip -d /opt; \
 	rm -f /opt/eld_binaries.zip;
 
+# 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;
+
 # OSSFUZZ: libprotobuf-mutator
 RUN set -ex; \
 	git clone https://github.com/google/libprotobuf-mutator.git \

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="23"
+LABEL version="24"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -39,14 +39,14 @@ RUN set -ex; \
 		libboost-program-options-dev \
 		libboost-system-dev \
 		libboost-test-dev \
-		libcvc4-dev \
 		libz3-static-dev \
 		lsof \
 		ninja-build \
 		python3-pip \
 		python3-sphinx \
 		software-properties-common \
 		sudo \
+		unzip \
 		z3-static; \
 	pip3 install \
 		codecov \
@@ -59,18 +59,32 @@ RUN set -ex; \
 		tabulate \
 		z3-solver;
 
+# TODO: we could eliminate duplication by using a Dockerfile extension like:
+# https://github.com/edrevo/dockerfile-plus?tab=readme-ov-file#dockerfile
+# or mult-stage builds, then we could define a base image which would be included/used by all the other Dockerfiles.
+# Or we could move the common parts to a shell script, copying and calling it from the Dockerfiles.
 # Eldarica
 RUN set -ex; \
 	apt-get update; \
 	apt-get install -qqy \
-		openjdk-11-jre \
-		unzip; \
+		openjdk-11-jre; \
 	eldarica_version="2.1"; \
 	wget "https://github.com/uuverifiers/eldarica/releases/download/v${eldarica_version}/eldarica-bin-${eldarica_version}.zip" -O /opt/eld_binaries.zip; \
 	test "$(sha256sum /opt/eld_binaries.zip)" = "0ac43f45c0925383c9d2077f62bbb515fd792375f3b2b101b30c9e81dcd7785c  /opt/eld_binaries.zip"; \
 	unzip /opt/eld_binaries.zip -d /opt; \
 	rm -f /opt/eld_binaries.zip;
 
+# 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;
+
 FROM base AS libraries
 
 # EVMONE

diff --git a/scripts/docker/buildpack-deps/Dockerfile.ubuntu2204 b/scripts/docker/buildpack-deps/Dockerfile.ubuntu2204
@@ -22,7 +22,7 @@
 # (c) 2016-2019 solidity contributors.
 #------------------------------------------------------------------------------
 FROM buildpack-deps:jammy AS base
-LABEL version="8"
+LABEL version="9"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -40,7 +40,6 @@ RUN set -ex; \
 		libboost-system-dev \
 		libboost-test-dev \
 		libcln-dev \
-		libcvc4-dev \
 		libz3-static-dev \
 		locales-all \
 		lsof \
@@ -49,6 +48,7 @@ RUN set -ex; \
 		python3-sphinx \
 		software-properties-common \
 		sudo \
+		unzip \
 		z3-static \
 		zip; \
 	pip3 install \
@@ -66,14 +66,24 @@ RUN set -ex; \
 RUN set -ex; \
 	apt-get update; \
 	apt-get install -qqy \
-		openjdk-11-jre \
-		unzip; \
+		openjdk-11-jre; \
 	eldarica_version="2.1"; \
 	wget "https://github.com/uuverifiers/eldarica/releases/download/v${eldarica_version}/eldarica-bin-${eldarica_version}.zip" -O /opt/eld_binaries.zip; \
 	test "$(sha256sum /opt/eld_binaries.zip)" = "0ac43f45c0925383c9d2077f62bbb515fd792375f3b2b101b30c9e81dcd7785c  /opt/eld_binaries.zip"; \
 	unzip /opt/eld_binaries.zip -d /opt; \
 	rm -f /opt/eld_binaries.zip;
 
+# 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;
+
 FROM base AS libraries
 
 # EVMONE

diff --git a/scripts/docker/buildpack-deps/Dockerfile.ubuntu2204.clang b/scripts/docker/buildpack-deps/Dockerfile.ubuntu2204.clang
@@ -22,7 +22,7 @@
 # (c) 2016-2019 solidity contributors.
 #------------------------------------------------------------------------------
 FROM buildpack-deps:jammy AS base
-LABEL version="7"
+LABEL version="8"
 
 ARG DEBIAN_FRONTEND=noninteractive
 
@@ -71,6 +71,17 @@ RUN set -ex; \
 	unzip /opt/eld_binaries.zip -d /opt; \
 	rm -f /opt/eld_binaries.zip;
 
+# 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;
+
 FROM base AS libraries
 
 ENV CC clang