From ad5afd2a6155ec7cfbfec7ae79b58c60faeeee09 Mon Sep 17 00:00:00 2001 From: Allan Blanchard Date: Sat, 9 Nov 2024 22:09:54 +0100 Subject: [PATCH] Use CVC5 instead of Z3 - better counter examples support - same proof capability on examples --- code/Dockerfile | 11 ++++++----- code/acsl-properties/functions/facto-1.c | 2 +- .../functions/oracle/facto-1.res.oracle | 6 +++--- code/acsl-properties/lemmas/linear-0.c | 2 +- .../acsl-properties/lemmas/oracle/linear-0.res.oracle | 6 +++--- english/acsl-properties/functions.tex | 4 ++-- english/acsl-properties/lemmas.tex | 6 +++--- english/introduction.tex | 2 +- english/program-proof-and-our-tool/frama-c.tex | 4 ++-- french/acsl-properties/functions.tex | 4 ++-- french/acsl-properties/lemmas.tex | 4 ++-- french/introduction.tex | 2 +- french/program-proof-and-our-tool/frama-c.tex | 4 ++-- 13 files changed, 29 insertions(+), 28 deletions(-) diff --git a/code/Dockerfile b/code/Dockerfile index 37bdb06..9e2d699 100644 --- a/code/Dockerfile +++ b/code/Dockerfile @@ -1,10 +1,11 @@ -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 \ @@ -12,11 +13,11 @@ RUN apk add \ 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 index 660017d..71c406f 100644 --- 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 index 483746b..3a46a20 100644 --- 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 index d9c4b9f..7a1c24f 100644 --- 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 diff --git a/code/acsl-properties/lemmas/oracle/linear-0.res.oracle b/code/acsl-properties/lemmas/oracle/linear-0.res.oracle index b7835f8..0b58465 100644 --- 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 index 924f60b..b4c6607 100644 --- 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 index a168fb9..7aded34 100644 --- 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 index 493b947..34368a4 100644 --- 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 index c3aa052..058dce8 100644 --- 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 index de274ac..99d50ec 100644 --- 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 index ab814de..c94c35e 100644 --- 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 index f838c0a..5b03c84 100644 --- 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 index 5f7a802..5fc92ea 100644 --- 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.