Merge pull request #69 from AllanBlanchard/config/move-from-z3-to-cvc5

Use CVC5 instead of Z3
AllanBlanchard · Nov 9, 2024 · 78dc1dd · 78dc1dd
2 parents 5e17c2f + ad5afd2
commit 78dc1dd
Show file tree

Hide file tree

Showing 13 changed files with 29 additions and 28 deletions.
diff --git a/code/Dockerfile b/code/Dockerfile
@@ -1,22 +1,23 @@
-FROM alpine:latest
+FROM debian:trixie
 
-RUN apk add \
+RUN apt-get update && apt-get install -y \
   bash \
-  build-base \
+  build-essential \
   bzip2 \
   ca-certificates \
+  cvc5 \
   curl \
   diffutils \
   gcc \
   git \
   make \
   opam \
   patch \
+  rsync \
   tar \
   unzip \
   wget \
-  which \
-  z3
+  which
 
 RUN opam init -c 4.14.2 --disable-sandboxing
 

diff --git a/code/acsl-properties/functions/facto-1.c b/code/acsl-properties/functions/facto-1.c
@@ -1,5 +1,5 @@
 /* run.config
-   STDOPT:+"-wp-prover alt-ergo,z3"
+   STDOPT:+"-wp-prover alt-ergo,cvc5"
 */
 
 /*@

diff --git a/code/acsl-properties/functions/oracle/facto-1.res.oracle b/code/acsl-properties/functions/oracle/facto-1.res.oracle
@@ -10,8 +10,8 @@
 [wp] [Valid] typed_facto_loop_invariant_established (Qed)
 [wp] [Valid] typed_facto_loop_invariant_2_preserved (Alt-Ergo) (Cached)
 [wp] [Valid] typed_facto_loop_invariant_2_established (Alt-Ergo) (Cached)
-[wp] [Valid] typed_facto_assert_rte_signed_overflow (Z3) (Cached)
-[wp] [Valid] typed_facto_assert_rte_signed_overflow_2 (Z3) (Cached)
+[wp] [Valid] typed_facto_assert_rte_signed_overflow (CVC5) (Cached)
+[wp] [Valid] typed_facto_assert_rte_signed_overflow_2 (CVC5) (Cached)
 [wp] [Valid] typed_facto_assert_rte_signed_overflow_3 (Qed)
 [wp] [Valid] typed_facto_loop_assigns (Qed)
 [wp] [Valid] typed_facto_assigns_part1 (Qed)
@@ -24,4 +24,4 @@
   Unreachable:     1
   Qed:             9
   Alt-Ergo:        3
-  Z3:              2
+  CVC5:            2
diff --git a/code/acsl-properties/lemmas/linear-0.c b/code/acsl-properties/lemmas/linear-0.c
@@ -1,5 +1,5 @@
 /* run.config
-   STDOPT:+"-wp-prover alt-ergo,z3"
+   STDOPT:+"-wp-prover alt-ergo,cvc5"
 */
 
 #include <limits.h>

diff --git a/code/acsl-properties/lemmas/oracle/linear-0.res.oracle b/code/acsl-properties/lemmas/oracle/linear-0.res.oracle
@@ -6,9 +6,9 @@
 [wp] [Valid] Goal function_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal function_terminates (Cfg) (Trivial)
 [wp] 27 goals scheduled
-[wp] [Valid] typed_lemma_ax_b_monotonic_neg (Z3) (Cached)
+[wp] [Valid] typed_lemma_ax_b_monotonic_neg (CVC5) (Cached)
 [wp] [Valid] typed_lemma_ax_b_monotonic_nul (Alt-Ergo) (Cached)
-[wp] [Valid] typed_lemma_ax_b_monotonic_pos (Z3) (Cached)
+[wp] [Valid] typed_lemma_ax_b_monotonic_pos (CVC5) (Cached)
 [wp] [Valid] typed_function_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] typed_function_assert_rte_signed_overflow (Qed)
 [wp] [Valid] typed_function_assert_rte_signed_overflow_2 (Qed)
@@ -38,4 +38,4 @@
   Unreachable:     1
   Qed:            21
   Alt-Ergo:        4
-  Z3:              2
+  CVC5:            2
diff --git a/english/acsl-properties/functions.tex b/english/acsl-properties/functions.tex
@@ -126,8 +126,8 @@
 
 
 If we ask for a proof on this input, Alt-ergo will probably fail,
-whereas Z3 can compute the proof in less than a second. The reason is
-that in this case, the heuristics that are used by Z3 consider that it
+whereas CVC5 can compute the proof in less than a second. The reason is
+that in this case, the heuristics that are used by CVC5 consider that it
 is a good idea to spend a bit more time on the evaluation of the
 function.
 

diff --git a/english/acsl-properties/lemmas.tex b/english/acsl-properties/lemmas.tex
@@ -67,7 +67,7 @@
 
 
 For these proofs, Alt-ergo, will probably not be able to discharge all
-generated verification conditions. In this case, Z3 will certainly succeed
+generated verification conditions. In this case, CVC5 will certainly succeed
 in finishing the remaining ones. We can then write the following example code:
 
 
@@ -82,8 +82,8 @@
 property is the simply an instance of the lemma
 \CodeInline{ax\_monotonic\_pos}, the proof is then trivial as our lemma is
 considered to be true when are not currently proving it. Note that on this
-generalized version of \CodeInline{function}, Z3 will be probably more efficient
-to prove the absence of runtime errors.
+generalized version of \CodeInline{function}, CVC5 will be probably more
+efficient to prove the absence of runtime errors.
 
 
 \levelThreeTitle{Example: arrays and labels}

diff --git a/english/introduction.tex b/english/introduction.tex
@@ -34,7 +34,7 @@
   \item Why3 1.7.2
   \item Alt-Ergo 2.6.0
   \item Coq 8.16.1 (for provided scripts, not used in the tutorial)
-  \item Z3 4.8.10 (in one example, it is not absolutely necessary to follow this book)
+  \item CVC5 1.1.2 (for counter examples and a few examples)
   \end{itemize}
   Depending on the versions used by the reader some differences could appear in
   what is proved and what is not. Some presented features are only available

diff --git a/english/program-proof-and-our-tool/frama-c.tex b/english/program-proof-and-our-tool/frama-c.tex
@@ -338,11 +338,11 @@
 
 
 On their website, we can find the list of
-\externalLink{supported provers}{http://why3.lri.fr/\#provers}.
+\externalLink{supported provers}{https://www.why3.org/\#provers}.
 We recommend installing
 \externalLink{Z3}{https://github.com/Z3Prover/z3/wiki} which is
 developed by Microsoft Research, and
-\externalLink{CVC4}{http://cvc4.cs.stanford.edu/web/} which is developed by many
+\externalLink{CVC5}{https://cvc5.github.io/} which is developed by many
 research teams (New York University, University of Iowa, Google, CEA
 List). Those two provers are very efficient and somewhat complementary.
 

diff --git a/french/acsl-properties/functions.tex b/french/acsl-properties/functions.tex
@@ -131,8 +131,8 @@
 
 
 Si nous demandons la preuve avec cette entrée, Alt-Ergo échouera pratiquement à
-coup sûr. En revanche, le prouveur Z3 produit la preuve en moins d'une seconde.
-Parce que dans ce cas précis, les heuristiques de Z3 considèrent que c'est une
+coup sûr. En revanche, le prouveur CVC5 produit la preuve en moins d'une seconde.
+Parce que dans ce cas précis, les heuristiques de CVC5 considèrent que c'est une
 bonne idée de passer un peu plus de temps sur l'évaluation de la fonction.
 
 

diff --git a/french/acsl-properties/lemmas.tex b/french/acsl-properties/lemmas.tex
@@ -73,7 +73,7 @@
 
 
 Pour ces preuves, il est fort possible qu'Alt-Ergo ne parvienne pas à les
-décharger. Dans ce cas, le prouveur Z3 devrait, lui, y arriver. Nous pouvons
+décharger. Dans ce cas, le prouveur CVC5 devrait, lui, y arriver. Nous pouvons
 ensuite construire cet exemple de code :
 
 
@@ -87,7 +87,7 @@
 Avec ces lemmes présents en revanche, il y parvient sans problème, car cette
 propriété est une simple instance du lemme \CodeInline{ax\_b\_monotonic\_pos}, la preuve
 étant ainsi triviale, car notre lemme nous énonce cette propriété comme étant vraie.
-Notons que sur cette version généralisée, Z3 sera probablement plus efficace pour
+Notons que sur cette version généralisée, CVC5 sera probablement plus efficace pour
 prouver l'absence d'erreurs à l'exécution.
 
 

diff --git a/french/introduction.tex b/french/introduction.tex
@@ -36,7 +36,7 @@
 \item Why3 1.7.2
 \item Alt-Ergo 2.6.0
 \item Coq 8.16.1 (pour les scripts proposés, Coq n'est pas utilisé dans le tutoriel)
-\item Z3 4.8.10 (utilisés dans un exemple, il n'est pas absolument nécessaire)
+\item CVC5 1.1.2 (pour les contre-exemples et quelques exemples)
 \end{itemize}
 Selon les versions utilisées par le lecteur, quelques différences pourraient
 apparaître avec ce qui est prouvé et ce qui ne l'est pas. Quelques fonctionnalités

diff --git a/french/program-proof-and-our-tool/frama-c.tex b/french/program-proof-and-our-tool/frama-c.tex
@@ -337,9 +337,9 @@
 
 
 Nous pouvons retrouver sur ce même site
-\externalLink{la liste des prouveurs}{http://why3.lri.fr/\#provers} qu'il supporte.
+\externalLink{la liste des prouveurs}{https://www.why3.org/\#provers} qu'il supporte.
 Il est vivement conseillé d'avoir \externalLink{Z3}{https://github.com/Z3Prover/z3/wiki},
-développé par Microsoft Research, et \externalLink{CVC4}{http://cvc4.cs.stanford.edu/web/},
+développé par Microsoft Research, et \externalLink{CVC5}{https://cvc5.github.io/},
 développé par des personnes de divers organismes de recherche (New York
 University, University of Iowa, Google, CEA List). Ces deux prouveurs sont très
 efficaces et relativement complémentaires.