Merge pull request #1005 from Armael/upgrade-altergo-2.5.3

Upgrade alt-ergo to version 2.5.3
creusot-rs · May 20, 2024 · c21469b · c21469b
2 parents 1bcd8ef + 6ea9810
commit c21469b
Show file tree

Hide file tree

Showing 188 changed files with 2,357 additions and 2,377 deletions.
diff --git a/HACKING.md b/HACKING.md
@@ -51,7 +51,7 @@ If the proof of a test is broken (e.g.
 ./ide creusot/tests/should_succeed/cell/01
 ```
 
-## Calling why3 & why3_tools: shell environment setup
+## Calling why3 (and why3_tools, etc): shell environment setup
 
 To invoke why3 (manually or in scripts) with the same binary/configuration as
 setup by `cargo creusot setup`, one needs to setup a shell environment with the
@@ -66,11 +66,21 @@ After that, the `why3` binary in PATH will be the one configured by
 `cargo creusot setup`, using the adequate configuration file (through the
 `WHY3CONFIG` environment variable).
 
-## Upgrading the revision of Why3 used by Creusot
+## Upgrading Why3
 
 Edit `creusot-deps.opam` to use the hash of the git commit of the latest commit
 in Why3's master branch. (But first make sure that the Nightly CI job passes.)
 
 There are several places to edit in the file: the `pin-depends` field at the end
 of the file (URLs and `git-XXXX` versions), and the `git-XXXX` versions in the
 `depends:` field.
+
+## Upgrading a prover to a newer version 
+
+- Install why3-tools: `opam pin git+https://github.com/xldenis/why3-tools`
+- Install the newer prover, make it available in `$PATH`
+- Setup Creusot to use it: `cargo creusot setup install --no-check-version <PROVER> --external <PROVER>`
+- Run `eval $(cargo run --bin dev-env)`
+- Use the `./testsuite_upgrade_prover` script to update why3 sessions in the testsuite.
+  Launch the script without arguments to have some usage instructions.
+- Once the testsuite is migrated, update `creusot-setup/src/{tools,tools_versions_urls}.rs` 
diff --git a/ci/creusot-deps-nightly.opam b/ci/creusot-deps-nightly.opam
@@ -10,7 +10,7 @@ depends: [
   "camlzip"
   "zarith"
 # the alt-ergo solver
-  "alt-ergo" {= "2.4.3"}
+  "alt-ergo" {= "2.5.3"}
 ]
 pin-depends: [
   [ "why3.git" "git+https://gitlab.inria.fr/why3/why3.git" ]

diff --git a/creusot-deps.opam b/creusot-deps.opam
@@ -11,7 +11,7 @@ depends: [
   "camlzip"
   "zarith"
 # the alt-ergo solver
-  "alt-ergo" {= "2.4.3"}
+  "alt-ergo" {= "2.5.3"}
 ]
 # When updating the hash and git-XXX below, don't forget to update them in the
 # depends: field above!

diff --git a/creusot-setup/src/tools.rs b/creusot-setup/src/tools.rs
@@ -215,9 +215,7 @@ pub fn generate_why3_conf(
 fn detect_altergo_version(altergo: &Path) -> Option<String> {
     let output = Command::new(&altergo).arg("--version").output().ok()?;
     let out_s = String::from_utf8(output.stdout).ok()?;
-    // will be needed for more recent altergo versions
-    // out_s.trim_end().strip_prefix("v").map(String::from)
-    Some(out_s.trim_end().to_owned())
+    out_s.trim_end().strip_prefix("v").map(String::from)
 }
 
 // helpers: Z3

diff --git a/creusot-setup/src/tools_versions_urls.rs b/creusot-setup/src/tools_versions_urls.rs
@@ -7,7 +7,7 @@
 
 // tools without binary releases
 pub const WHY3_VERSION: &'static str = "1.7.1";
-pub const ALTERGO_VERSION: &'static str = "2.4.3";
+pub const ALTERGO_VERSION: &'static str = "2.5.3";
 // tools with binary releases
 pub const Z3_VERSION: &'static str = "4.12.4";
 pub const CVC4_VERSION: &'static str = "1.8";

diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3session.xml b/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3session.xml
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
-"http://why3.lri.fr/why3session.dtd">
+"https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Z3" version="4.12.1" timelimit="5" steplimit="0" memlimit="1000"/>
@@ -12,34 +12,38 @@
  <goal name="make_vec_of_size&#39;vc" expl="VC for make_vec_of_size">
  <transf name="split_vc" >
   <goal name="make_vec_of_size&#39;vc.0" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.04" steps="12763"/></proof>
+  <proof prover="0"><result status="valid" time="0.040000" steps="13246"/></proof>
   </goal>
   <goal name="make_vec_of_size&#39;vc.1" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.03" steps="12225"/></proof>
+  <proof prover="0"><result status="valid" time="0.030000" steps="12458"/></proof>
   </goal>
-  <goal name="make_vec_of_size&#39;vc.2" expl="integer overflow">
-  <proof prover="0" timelimit="5"><result status="timeout" time="5.00" steps="719150"/></proof>
-  <proof prover="1"><result status="timeout" time="5.00" steps="2658667"/></proof>
-  <proof prover="2"><result status="timeout" time="5.00" steps="848172"/></proof>
-  <proof prover="3"><result status="timeout" time="5.00"/></proof>
+  <goal name="make_vec_of_size&#39;vc.2" expl="precondition">
+  <proof prover="0" timelimit="5" obsolete="true"><result status="timeout" time="5.000000" steps="719150"/></proof>
+  <proof prover="1" obsolete="true"><result status="timeout" time="5.000000" steps="2658667"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="5.000000" steps="848172"/></proof>
+  <proof prover="3" obsolete="true"><result status="timeout" time="5.000000"/></proof>
   </goal>
-  <goal name="make_vec_of_size&#39;vc.3" expl="loop invariant preservation">
-  <proof prover="0"><result status="timeout" time="1.00" steps="259158"/></proof>
-  <proof prover="1" timelimit="1"><result status="timeout" time="1.00" steps="922192"/></proof>
-  <proof prover="2" timelimit="1"><result status="timeout" time="1.00" steps="182790"/></proof>
-  <proof prover="3" timelimit="1"><result status="timeout" time="1.00"/></proof>
-  <transf name="split_vc" >
-   <goal name="make_vec_of_size&#39;vc.3.0" expl="loop invariant preservation" proved="true">
-   <proof prover="0"><result status="valid" time="0.03" steps="13116"/></proof>
+  <goal name="make_vec_of_size&#39;vc.3" expl="precondition" proved="true">
+  <proof prover="0" obsolete="true"><result status="timeout" time="1.000000" steps="259158"/></proof>
+  <proof prover="1" timelimit="1" obsolete="true"><result status="timeout" time="1.000000" steps="922192"/></proof>
+  <proof prover="2" timelimit="1" obsolete="true"><result status="timeout" time="1.000000" steps="182790"/></proof>
+  <proof prover="3" timelimit="1" obsolete="true"><result status="timeout" time="1.000000"/></proof>
+  <transf name="split_vc" proved="true" >
+   <goal name="make_vec_of_size&#39;vc.3.0" expl="precondition" proved="true">
+   <proof prover="0"><result status="valid" time="0.030000" steps="12666"/></proof>
    </goal>
    <goal name="make_vec_of_size&#39;vc.3.1" expl="loop invariant preservation">
-   <proof prover="0" timelimit="5"><result status="timeout" time="5.00" steps="762584"/></proof>
-   <proof prover="1"><result status="timeout" time="5.00" steps="2657404"/></proof>
-   <proof prover="2"><result status="timeout" time="5.00" steps="825919"/></proof>
-   <proof prover="3"><result status="timeout" time="5.00"/></proof>
+   <proof prover="0" timelimit="5"><result status="timeout" time="5.000000" steps="762584"/></proof>
+   <proof prover="1"><result status="timeout" time="5.000000" steps="2657404"/></proof>
+   <proof prover="2"><result status="timeout" time="5.000000" steps="825919"/></proof>
+   <proof prover="3"><result status="timeout" time="5.000000"/></proof>
    </goal>
   </transf>
   </goal>
+  <goal name="make_vec_of_size&#39;vc.4" expl="integer overflow">
+  </goal>
+  <goal name="make_vec_of_size&#39;vc.5" expl="loop invariant preservation">
+  </goal>
  </transf>
  </goal>
 </theory>

diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3shapes.gz b/creusot/tests/should_fail/bug/01_resolve_unsoundness/why3shapes.gz
diff --git a/creusot/tests/should_fail/bug/222/why3session.xml b/creusot/tests/should_fail/bug/222/why3session.xml
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
-"http://why3.lri.fr/why3session.dtd">
+"https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -9,15 +9,15 @@
 <file format="mlcfg">
 <path name=".."/><path name="222.mlcfg"/>
 <theory name="C222_A_IsTrue_Impl">
- <goal name="is_true&#39;vc" expl="VC for is_true">
- <proof prover="0"><result status="timeout" time="1.00"/></proof>
- <proof prover="1"><result status="unknown" time="0.03" steps="4649"/></proof>
- <proof prover="2"><result status="unknown" time="0.01" steps="1031"/></proof>
+ <goal name="vc_is_true">
+ <proof prover="0" obsolete="true"><result status="timeout" time="1.000000"/></proof>
+ <proof prover="1" obsolete="true"><result status="unknown" time="0.030000" steps="4649"/></proof>
+ <proof prover="2" obsolete="true"><result status="unknown" time="0.010000" steps="1031"/></proof>
  </goal>
 </theory>
-<theory name="C222_UsesInvariant" proved="true">
- <goal name="uses_invariant&#39;vc" expl="VC for uses_invariant" proved="true">
- <proof prover="4"><result status="valid" time="0.00" steps="0"/></proof>
+<theory name="C222_UsesInvariant">
+ <goal name="uses_invariant&#39;vc" expl="VC for uses_invariant">
+ <proof prover="4" obsolete="true"><result status="valid" time="0.000000" steps="0"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/creusot/tests/should_fail/bug/222/why3shapes.gz b/creusot/tests/should_fail/bug/222/why3shapes.gz
diff --git a/creusot/tests/should_fail/bug/492/why3session.xml b/creusot/tests/should_fail/bug/492/why3session.xml
@@ -1,22 +1,22 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
-"http://why3.lri.fr/why3session.dtd">
+"https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
 <prover id="0" name="Alt-Ergo" version="2.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Z3" version="4.11.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="mlcfg">
 <path name=".."/><path name="492.mlcfg"/>
-<theory name="C492_ReborrowTuple" proved="true">
- <goal name="reborrow_tuple&#39;vc" expl="VC for reborrow_tuple" proved="true">
- <proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
+<theory name="C492_ReborrowTuple">
+ <goal name="reborrow_tuple&#39;vc" expl="VC for reborrow_tuple">
+ <proof prover="0" obsolete="true"><result status="valid" time="0.010000" steps="18"/></proof>
  </goal>
 </theory>
 <theory name="C492_Test">
  <goal name="test&#39;vc" expl="VC for test">
- <proof prover="0"><result status="timeout" time="1.00"/></proof>
- <proof prover="1"><result status="timeout" time="1.00"/></proof>
- <proof prover="2"><result status="unknown" time="0.07" steps="15326"/></proof>
+ <proof prover="0" obsolete="true"><result status="timeout" time="1.000000"/></proof>
+ <proof prover="1" obsolete="true"><result status="timeout" time="1.000000"/></proof>
+ <proof prover="2" obsolete="true"><result status="unknown" time="0.070000" steps="15326"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/creusot/tests/should_fail/bug/492/why3shapes.gz b/creusot/tests/should_fail/bug/492/why3shapes.gz
diff --git a/creusot/tests/should_fail/bug/692/why3session.xml b/creusot/tests/should_fail/bug/692/why3session.xml
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
-"http://why3.lri.fr/why3session.dtd">
+"https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Z3" version="4.11.0" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -10,25 +10,25 @@
 <path name=".."/><path name="692.mlcfg"/>
 <theory name="C692_Incorrect">
  <goal name="incorrect&#39;vc" expl="VC for incorrect">
- <proof prover="0"><result status="unknown" time="0.02" steps="1932"/></proof>
- <proof prover="1"><result status="timeout" time="1.00"/></proof>
- <proof prover="2"><result status="unknown" time="0.01" steps="1360"/></proof>
- <proof prover="3"><result status="unknown" time="0.02"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.020000" steps="1932"/></proof>
+ <proof prover="1" obsolete="true"><result status="timeout" time="1.000000"/></proof>
+ <proof prover="2" obsolete="true"><result status="unknown" time="0.010000" steps="1360"/></proof>
+ <proof prover="3" obsolete="true"><result status="unknown" time="0.020000"/></proof>
  </goal>
 </theory>
-<theory name="C692_ValidNormal_Closure1" proved="true">
- <goal name="c692_ValidNormal_Closure1&#39;vc" expl="VC for c692_ValidNormal_Closure1" proved="true">
- <proof prover="3"><result status="valid" time="0.00" steps="11"/></proof>
+<theory name="C692_ValidNormal_Closure2">
+ <goal name="c692_validnormal_closure2&#39;vc" expl="VC for c692_validnormal_closure2">
+ <proof prover="3" obsolete="true"><result status="valid" time="0.010000" steps="49"/></proof>
  </goal>
 </theory>
-<theory name="C692_ValidNormal_Closure2" proved="true">
- <goal name="c692_ValidNormal_Closure2&#39;vc" expl="VC for c692_ValidNormal_Closure2" proved="true">
- <proof prover="3"><result status="valid" time="0.01" steps="49"/></proof>
+<theory name="C692_ValidNormal_Closure1">
+ <goal name="c692_validnormal_closure1&#39;vc" expl="VC for c692_validnormal_closure1">
+ <proof prover="3" obsolete="true"><result status="valid" time="0.000000" steps="11"/></proof>
  </goal>
 </theory>
-<theory name="C692_ValidNormal" proved="true">
- <goal name="valid_normal&#39;vc" expl="VC for valid_normal" proved="true">
- <proof prover="3"><result status="valid" time="0.01" steps="201"/></proof>
+<theory name="C692_ValidNormal">
+ <goal name="valid_normal&#39;vc" expl="VC for valid_normal">
+ <proof prover="3" obsolete="true"><result status="valid" time="0.010000" steps="201"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/creusot/tests/should_fail/bug/692/why3shapes.gz b/creusot/tests/should_fail/bug/692/why3shapes.gz
diff --git a/creusot/tests/should_fail/bug/695/why3session.xml b/creusot/tests/should_fail/bug/695/why3session.xml
@@ -1,34 +1,34 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
-"http://why3.lri.fr/why3session.dtd">
+"https://www.why3.org/why3session.dtd">
 <why3session shape_version="6">
 <prover id="0" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="1" name="Z3" version="4.11.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="CVC5" version="1.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Alt-Ergo" version="2.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
 <file format="mlcfg">
 <path name=".."/><path name="695.mlcfg"/>
-<theory name="C695_InversedIf" proved="true">
- <goal name="inversed_if&#39;vc" expl="VC for inversed_if" proved="true">
- <proof prover="3"><result status="valid" time="0.00" steps="50"/></proof>
+<theory name="C695_InversedIf">
+ <goal name="inversed_if&#39;vc" expl="VC for inversed_if">
+ <proof prover="3" obsolete="true"><result status="valid" time="0.000000" steps="50"/></proof>
  </goal>
 </theory>
-<theory name="C695_Valid_Closure1" proved="true">
- <goal name="c695_Valid_Closure1&#39;vc" expl="VC for c695_Valid_Closure1" proved="true">
- <proof prover="3"><result status="valid" time="0.00" steps="11"/></proof>
+<theory name="C695_Valid_Closure2">
+ <goal name="c695_valid_closure2&#39;vc" expl="VC for c695_valid_closure2">
+ <proof prover="3" obsolete="true"><result status="valid" time="0.010000" steps="49"/></proof>
  </goal>
 </theory>
-<theory name="C695_Valid_Closure2" proved="true">
- <goal name="c695_Valid_Closure2&#39;vc" expl="VC for c695_Valid_Closure2" proved="true">
- <proof prover="3"><result status="valid" time="0.01" steps="49"/></proof>
+<theory name="C695_Valid_Closure1">
+ <goal name="c695_valid_closure1&#39;vc" expl="VC for c695_valid_closure1">
+ <proof prover="3" obsolete="true"><result status="valid" time="0.000000" steps="11"/></proof>
  </goal>
 </theory>
 <theory name="C695_Valid">
  <goal name="valid&#39;vc" expl="VC for valid">
- <proof prover="0"><result status="unknown" time="0.06" steps="16049"/></proof>
- <proof prover="1"><result status="timeout" time="1.00"/></proof>
- <proof prover="2"><result status="unknown" time="0.06" steps="13355"/></proof>
- <proof prover="3"><result status="timeout" time="1.00"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.060000" steps="16049"/></proof>
+ <proof prover="1" obsolete="true"><result status="timeout" time="1.000000"/></proof>
+ <proof prover="2" obsolete="true"><result status="unknown" time="0.060000" steps="13355"/></proof>
+ <proof prover="3" obsolete="true"><result status="timeout" time="1.000000"/></proof>
  </goal>
 </theory>
 </file>

diff --git a/creusot/tests/should_fail/bug/695/why3shapes.gz b/creusot/tests/should_fail/bug/695/why3shapes.gz