Add tests for final borrows

creusot/tests/should_fail/bug/869.mlcfg

@@ -0,0 +1,74 @@
+
+module C869_Unsound
+  use prelude.Ghost
+  use prelude.Borrow
+  use prelude.Ghost
+  use prelude.Ghost
+  use prelude.Ghost
+  predicate resolve0 (self : borrowed (Ghost.ghost_ty bool)) =
+    [#"../../../../../creusot-contracts/src/resolve.rs" 25 20 25 34]  ^ self =  * self
+  val resolve0 (self : borrowed (Ghost.ghost_ty bool)) : bool
+    ensures { result = resolve0 self }
+
+  use prelude.Ghost
+  let rec cfg unsound [#"../869.rs" 4 0 4 16] [@cfg:stackify] [@cfg:subregion_analysis] (_1 : ()) : ()
+   = [@vc:do_not_keep_trace] [@vc:sp]
+  var _0 : ();
+  var x : Ghost.ghost_ty bool;
+  var xm : borrowed (Ghost.ghost_ty bool);
+  var _4 : borrowed (Ghost.ghost_ty bool);
+  var b : borrowed (Ghost.ghost_ty bool);
+  var _6 : borrowed (Ghost.ghost_ty bool);
+  var bg : Ghost.ghost_ty (borrowed (Ghost.ghost_ty bool));
+  var evil : borrowed (Ghost.ghost_ty bool);
+  var _12 : borrowed (Ghost.ghost_ty bool);
+  var _15 : Ghost.ghost_ty bool;
+  {
+    goto BB0
+  }
+  BB0 {
+    [#"../869.rs" 5 29 5 41] x <- ([#"../869.rs" 5 29 5 41] Ghost.new true);
+    goto BB1
+  }
+  BB1 {
+    [#"../869.rs" 7 31 7 37] _4 <- Borrow.borrow_mut x;
+    [#"../869.rs" 7 31 7 37] x <-  ^ _4;
+    [#"../869.rs" 7 31 7 37] xm <- Borrow.borrow_final ( * _4) (Borrow.get_id _4);
+    [#"../869.rs" 7 31 7 37] _4 <- { _4 with current = ( ^ xm) ; };
+    assume { resolve0 _4 };
+    [#"../869.rs" 9 30 9 38] _6 <- Borrow.borrow_mut ( * xm);
+    [#"../869.rs" 9 30 9 38] xm <- { xm with current = ( ^ _6) ; };
+    [#"../869.rs" 9 30 9 38] b <- Borrow.borrow_final ( * _6) (Borrow.get_id _6);
+    [#"../869.rs" 9 30 9 38] _6 <- { _6 with current = ( ^ b) ; };
+    assume { resolve0 b };
+    assume { resolve0 _6 };
+    [#"../869.rs" 10 38 10 47] bg <- ([#"../869.rs" 10 38 10 47] Ghost.new b);
+    goto BB2
+  }
+  BB2 {
+    assert { [@expl:assertion] [#"../869.rs" 11 20 11 50] Ghost.inner ( * Ghost.inner bg) = true /\ Ghost.inner ( ^ Ghost.inner bg) = true };
+    [#"../869.rs" 13 33 13 41] _12 <- Borrow.borrow_final ( * xm) (Borrow.get_id xm);
+    [#"../869.rs" 13 33 13 41] xm <- { xm with current = ( ^ _12) ; };
+    [#"../869.rs" 13 33 13 41] evil <- Borrow.borrow_final ( * _12) (Borrow.get_id _12);
+    [#"../869.rs" 13 33 13 41] _12 <- { _12 with current = ( ^ evil) ; };
+    assume { resolve0 _12 };
+    assert { [@expl:assertion] [#"../869.rs" 17 20 17 53] (evil = Ghost.inner bg) = (Ghost.inner ( ^ evil) = true) };
+    [#"../869.rs" 18 12 18 58] _15 <- ([#"../869.rs" 18 12 18 58] Ghost.new (if evil = Ghost.inner bg then
+      false
+    else
+      true
+    ));
+    goto BB3
+  }
+  BB3 {
+    [#"../869.rs" 18 4 18 58] evil <- { evil with current = ([#"../869.rs" 18 4 18 58] _15) ; };
+    [#"../869.rs" 18 4 18 58] _15 <- any Ghost.ghost_ty bool;
+    assume { resolve0 evil };
+    assume { resolve0 xm };
+    assert { [@expl:assertion] [#"../869.rs" 19 20 19 37] Ghost.inner ( * evil) = (not Ghost.inner ( ^ evil)) };
+    assert { [@expl:assertion] [#"../869.rs" 20 20 20 37] Ghost.inner ( * evil) = (not Ghost.inner ( * evil)) };
+    [#"../869.rs" 4 17 21 1] _0 <- ([#"../869.rs" 4 17 21 1] ());
+    return _0
+  }
+
+end

creusot/tests/should_fail/bug/869.rs

@@ -0,0 +1,21 @@
+extern crate creusot_contracts;
+use creusot_contracts::*;
+
+pub fn unsound() {
+    let mut x: Ghost<bool> = gh! { true };
+    //            id(xm)   = i1
+    let xm: &mut Ghost<bool> = &mut x;
+    // Not final: id(b)    = i2
+    let b: &mut Ghost<bool> = &mut *xm;
+    let bg: Ghost<&mut Ghost<bool>> = gh! { b };
+    proof_assert! { ***bg == true && *^*bg == true };
+    // Final:     id(evil) = i1
+    let evil: &mut Ghost<bool> = &mut *xm;
+    // This proof_assert does not pass !
+    // Indeed evil != *bg (because the id do not match), which causes the next line to put `true` inside `*evil`.
+    // And thus *^evil == true, disproving the assertion.
+    proof_assert! { (evil == *bg) == (*^evil == true) };
+    *evil = gh! { if evil == *bg { false } else { true } };
+    proof_assert! { **evil == !*^evil };
+    proof_assert! { **evil == !**evil };
+}

creusot/tests/should_fail/bug/869/why3session.xml

@@ -0,0 +1,48 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
+"http://why3.lri.fr/why3session.dtd">
+<why3session shape_version="6">
+<prover id="0" name="Z3" version="4.12.4" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="1" name="CVC4" version="1.8" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="2" name="CVC5" version="1.0.5" timelimit="1" steplimit="0" memlimit="1000"/>
+<prover id="3" name="Alt-Ergo" version="2.4.3" timelimit="1" steplimit="0" memlimit="1000"/>
+<file format="mlcfg">
+<path name=".."/><path name="869.mlcfg"/>
+<theory name="C869_Unsound">
+ <goal name="unsound&#39;vc" expl="VC for unsound">
+ <proof prover="0"><result status="timeout" time="1.000000" steps="1663009"/></proof>
+ <proof prover="1"><result status="unknown" time="0.028856" steps="9252"/></proof>
+ <proof prover="2"><result status="unknown" time="0.024161" steps="8166"/></proof>
+ <proof prover="3"><result status="unknown" time="0.018348" steps="395"/></proof>
+ <transf name="split_vc" >
+  <goal name="unsound&#39;vc.0" expl="assertion" proved="true">
+  <proof prover="3"><result status="valid" time="0.004540" steps="48"/></proof>
+  </goal>
+  <goal name="unsound&#39;vc.1" expl="assertion">
+  <proof prover="0"><result status="timeout" time="1.000000" steps="1730760"/></proof>
+  <proof prover="1"><result status="unknown" time="0.014481" steps="2923"/></proof>
+  <proof prover="2"><result status="unknown" time="0.014401" steps="2325"/></proof>
+  <proof prover="3"><result status="unknown" time="0.011261" steps="256"/></proof>
+  <transf name="split_vc" >
+   <goal name="unsound&#39;vc.1.0" expl="assertion" proved="true">
+   <proof prover="3"><result status="valid" time="0.006615" steps="56"/></proof>
+   </goal>
+   <goal name="unsound&#39;vc.1.1" expl="assertion">
+   <proof prover="0" timelimit="10" memlimit="4000"><result status="timeout" time="10.000000" steps="16525401"/></proof>
+   <proof prover="1" timelimit="10" memlimit="4000"><result status="unknown" time="0.016032" steps="2846"/></proof>
+   <proof prover="2" timelimit="10" memlimit="4000"><result status="unknown" time="0.003775" steps="2060"/></proof>
+   <proof prover="3" timelimit="10" memlimit="4000"><result status="unknown" time="0.015127" steps="225"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="unsound&#39;vc.2" expl="assertion" proved="true">
+  <proof prover="3"><result status="valid" time="0.007761" steps="156"/></proof>
+  </goal>
+  <goal name="unsound&#39;vc.3" expl="assertion" proved="true">
+  <proof prover="3"><result status="valid" time="0.011326" steps="97"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+</file>
+</why3session>