Start final test updates

creusot-rs · Apr 10, 2024 · 6606ed0 · 6606ed0
1 parent 993bb59
commit 6606ed0
Show file tree

Hide file tree

Showing 239 changed files with 15,985 additions and 15,938 deletions.
diff --git a/creusot/src/backend.rs b/creusot/src/backend.rs
@@ -180,7 +180,7 @@ impl<'tcx> Why3Generator<'tcx> {
                         .insert(repr, TranslatedItem::Type { modl, accessors: Default::default() });
                 }
             }
-            ItemType::Field => self.translate_accessor(def_id),
+            ItemType::Field => unreachable!(),
             ItemType::Variant => {
                 self.translate(self.ctx.parent(def_id));
             }

diff --git a/creusot/src/backend/clone_map.rs b/creusot/src/backend/clone_map.rs
@@ -202,7 +202,10 @@ impl<'tcx> Namer<'tcx> for Dependencies<'tcx> {
             DefKind::Variant => {
                 let clone = self.insert(DepNode::new(tcx, (tcx.parent(def_id), subst)));
 
-                clone.qname()
+                let mut qname = clone.qname();
+                // TODO(xavier): Remove this hack
+                qname.name = DepNode::new(tcx, (def_id, subst)).base_ident(tcx).to_string().into();
+                qname
             }
             DefKind::Closure | DefKind::Struct => {
                 self.insert(DepNode::new(tcx, (def_id, subst))).ident().into()
@@ -321,6 +324,12 @@ impl<'tcx> CloneNames<'tcx> {
 
                 return kind;
             }
+            DepNode::Item(id, _) if util::item_type(self.tcx, id) == ItemType::Variant => {
+                let ty = self.tcx.parent(id);
+                let modl = module_name(self.tcx, ty);
+
+                Kind::Used(modl, key.base_ident(self.tcx))
+            }
             _ => {
                 if let DepNode::Item(id, _) = key
                     && let Some(why3_modl) = util::get_builtin(self.tcx, id)
@@ -401,7 +410,7 @@ impl<'tcx> DepGraph<'tcx> {
 
 // TODO: Get rid of the enum
 #[derive(Clone, Copy, Debug, PartialEq, Eq, TyEncodable, TyDecodable, Hash)]
-enum Kind {
+pub enum Kind {
     /// This symbol is locally defined
     Named(Symbol),
     /// This symbol must be acompanied by a `Use` statement in Why3

diff --git a/creusot/src/backend/clone_map/elaborator.rs b/creusot/src/backend/clone_map/elaborator.rs
@@ -164,6 +164,8 @@ impl<'tcx> SymbolElaborator<'tcx> {
             util::item_type(ctx.tcx, def_id).let_kind()
         };
 
+        // eprintln!("{item:?} {kind:?}");
+
         if CloneLevel::Signature == level_of_item {
             pre_sig.contract = PreContract::default();
         }
@@ -396,9 +398,11 @@ impl<'tcx> Namer<'tcx> for SymNamer<'tcx> {
 
         match util::item_type(tcx, def_id) {
             ItemType::Variant => {
-                let clone = self.insert(DepNode::new(tcx, (tcx.parent(def_id), subst)));
-
-                clone.qname()
+                let clone = self.insert(DepNode::new(tcx, (def_id, subst)));
+                let mut qname = clone.qname();
+                // TODO(xavier): Remove this hack
+                qname.name = DepNode::new(tcx, (def_id, subst)).base_ident(tcx).to_string().into();
+                qname
             }
             ItemType::Closure => self.insert(DepNode::new(tcx, (def_id, subst))).ident().into(),
             _ => unreachable!(),

diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness.coma b/creusot/tests/should_fail/bug/01_resolve_unsoundness.coma
@@ -97,77 +97,78 @@ module Alloc_Alloc_Global_Type
 end
 module C01ResolveUnsoundness_MakeVecOfSize
   use seq.Seq
-  predicate invariant3 (self : Seq.seq bool) =
+  predicate invariant'3 (self : Seq.seq bool) =
     [#"../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true
-  let rec invariant3 (self:Seq.seq bool) (return'  (ret:bool))= any 
-    [ return' (result:bool)-> {result = invariant3 self} (! return' {result}) ]
+  let rec invariant'3 (self:Seq.seq bool) (return'  (ret:bool))= any 
+    [ return' (result:bool)-> {result = invariant'3 self} (! return' {result}) ]
 
-  predicate inv3 (_x : Seq.seq bool)
-  let rec inv3 (_x:Seq.seq bool) (return'  (ret:bool))= any 
-    [ return' (result:bool)-> {result = inv3 _x} (! return' {result}) ]
+  predicate inv'3 (_x : Seq.seq bool)
+  let rec inv'3 (_x:Seq.seq bool) (return'  (ret:bool))= any 
+    [ return' (result:bool)-> {result = inv'3 _x} (! return' {result}) ]
 
-  axiom inv3 : forall x : Seq.seq bool . inv3 x = true
-  predicate invariant2 (self : bool) =
+  axiom inv'3 : forall x : Seq.seq bool . inv'3 x = true
+  predicate invariant'2 (self : bool) =
     [#"../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true
-  let rec invariant2 (self:bool) (return'  (ret:bool))= any 
-    [ return' (result:bool)-> {result = invariant2 self} (! return' {result}) ]
+  let rec invariant'2 (self:bool) (return'  (ret:bool))= any 
+    [ return' (result:bool)-> {result = invariant'2 self} (! return' {result}) ]
 
-  predicate inv2 (_x : bool)
-  let rec inv2 (_x:bool) (return'  (ret:bool))= any [ return' (result:bool)-> {result = inv2 _x} (! return' {result}) ] 
-  axiom inv2 : forall x : bool . inv2 x = true
+  predicate inv'2 (_x : bool)
+  let rec inv'2 (_x:bool) (return'  (ret:bool))= any 
+    [ return' (result:bool)-> {result = inv'2 _x} (! return' {result}) ]
+
+  axiom inv'2 : forall x : bool . inv'2 x = true
   use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
   use Alloc_Vec_Vec_Type as Alloc_Vec_Vec_Type
   use prelude.Borrow
-  predicate invariant1 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) =
+  predicate invariant'1 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) =
     [#"../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12] true
-  let rec invariant1 (self:borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) (return'  (ret:bool))= any
-    [ return' (result:bool)-> {result = invariant1 self} (! return' {result}) ] 
-  predicate inv1 (_x : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)))
-  let rec inv1 (_x:borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) (return'  (ret:bool))= any
-    [ return' (result:bool)-> {result = inv1 _x} (! return' {result}) ] 
-  axiom inv1 : forall x : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) . inv1 x = true
+  let rec invariant'1 (self:borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) (return'  (ret:bool))= any
+    [ return' (result:bool)-> {result = invariant'1 self} (! return' {result}) ] 
+  predicate inv'1 (_x : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)))
+  let rec inv'1 (_x:borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) (return'  (ret:bool))= any
+    [ return' (result:bool)-> {result = inv'1 _x} (! return' {result}) ] 
+  axiom inv'1 : forall x : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) . inv'1 x = true
   use prelude.UIntSize
   use prelude.UIntSize
   use prelude.Int
-  constant max0 : usize = (18446744073709551615 : usize)
+  constant max'0 : usize = (18446744073709551615 : usize)
   use seq.Seq
-  predicate inv0 (_x : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))
-  let rec inv0 (_x:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) (return'  (ret:bool))= any 
-    [ return' (result:bool)-> {result = inv0 _x} (! return' {result}) ]
-
-  function shallow_model0 (self : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) : Seq.seq bool
-  let rec shallow_model0 (self:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) (return'  (ret:Seq.seq bool))= {[#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] inv0 self}
-    any [ return' (result:Seq.seq bool)-> {result = shallow_model0 self} (! return' {result}) ] 
-  axiom shallow_model0_spec : forall self : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global) . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] inv0 self)
-   -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] inv3 (shallow_model0 self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model0 self) <= UIntSize.to_int (max0 : usize))
-  predicate invariant0 (self : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) =
-    [#"../../../../../creusot-contracts/src/std/vec.rs" 60 20 60 41] inv3 (shallow_model0 self)
-  let rec invariant0 (self:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) (return'  (ret:bool))= any 
-    [ return' (result:bool)-> {result = invariant0 self} (! return' {result}) ]
-
-  axiom inv0 : forall x : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global) . inv0 x = true
+  predicate inv'0 (_x : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))
+  let rec inv'0 (_x:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) (return'  (ret:bool))= any 
+    [ return' (result:bool)-> {result = inv'0 _x} (! return' {result}) ]
+
+  function shallow_model'0 (self : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) : Seq.seq bool
+  let rec shallow_model'0 (self:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) (return'  (ret:Seq.seq bool))= {[#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] inv'0 self}
+    any [ return' (result:Seq.seq bool)-> {result = shallow_model'0 self} (! return' {result}) ] 
+  axiom shallow_model'0_spec : forall self : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global) . ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25] inv'0 self)
+   -> ([#"../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36] inv'3 (shallow_model'0 self)) && ([#"../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41] Seq.length (shallow_model'0 self) <= UIntSize.to_int (max'0 : usize))
+  predicate invariant'0 (self : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) =
+    [#"../../../../../creusot-contracts/src/std/vec.rs" 60 20 60 41] inv'3 (shallow_model'0 self)
+  let rec invariant'0 (self:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) (return'  (ret:bool))= any
+    [ return' (result:bool)-> {result = invariant'0 self} (! return' {result}) ] 
+  axiom inv'0 : forall x : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global) . inv'0 x = true
   use prelude.Intrinsic
   use seq.Seq
-  function shallow_model1 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) : Seq.seq bool
+  function shallow_model'1 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) : Seq.seq bool
 
    =
-    [#"../../../../../creusot-contracts/src/model.rs" 108 8 108 31] shallow_model0 ( * self)
-  let rec shallow_model1 (self:borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) (return'  (ret:Seq.seq bool))= any
-    [ return' (result:Seq.seq bool)-> {result = shallow_model1 self} (! return' {result}) ] 
-  let rec push0 (self:borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) (value:bool) (return'  (ret:()))= {inv2 value}
-    {inv1 self}
+    [#"../../../../../creusot-contracts/src/model.rs" 108 8 108 31] shallow_model'0 ( * self)
+  let rec shallow_model'1 (self:borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) (return'  (ret:Seq.seq bool))= any
+    [ return' (result:Seq.seq bool)-> {result = shallow_model'1 self} (! return' {result}) ] 
+  let rec push'0 (self:borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) (value:bool) (return'  (ret:()))= {inv'2 value}
+    {inv'1 self}
     any 
-    [ return' (result:())-> {[#"../../../../../creusot-contracts/src/std/vec.rs" 78 26 78 51] shallow_model0 ( ^ self) = Seq.snoc (shallow_model1 self) value}
+    [ return' (result:())-> {[#"../../../../../creusot-contracts/src/std/vec.rs" 78 26 78 51] shallow_model'0 ( ^ self) = Seq.snoc (shallow_model'1 self) value}
       (! return' {result}) ]
 
-  let rec new0 (_1:()) (return'  (ret:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)))= any 
-    [ return' (result:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))-> {inv0 result}
-      {[#"../../../../../creusot-contracts/src/std/vec.rs" 68 26 68 44] Seq.length (shallow_model0 result) = 0}
+  let rec new'0 (_1:()) (return'  (ret:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)))= any 
+    [ return' (result:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))-> {inv'0 result}
+      {[#"../../../../../creusot-contracts/src/std/vec.rs" 68 26 68 44] Seq.length (shallow_model'0 result) = 0}
       (! return' {result}) ]
 
   let rec make_vec_of_size (n:usize) (return'  (ret:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)))= (! bb0
 
-    [ bb0 = new0 {[#"../01_resolve_unsoundness.rs" 10 29 10 39] ()}
+    [ bb0 = new'0 {[#"../01_resolve_unsoundness.rs" 10 29 10 39] ()}
       (fun (_ret':Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) -> [ &out <- _ret' ] bb1)
     | bb1 = [ &i <- [#"../01_resolve_unsoundness.rs" 11 16 11 17] (0 : usize) ] bb2
     | bb2 = bb2 
@@ -179,7 +180,7 @@ module C01ResolveUnsoundness_MakeVecOfSize
         | bb4 = Borrow.borrow_mut <Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)> {out}
           (fun (_ret':borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) -> 
             [ &out <-  ^ _13 ]
-            [ &_13 <- _ret' ] push0 {_13} {[#"../01_resolve_unsoundness.rs" 14 17 14 22] false} (fun (_ret':()) -> 
+            [ &_13 <- _ret' ] push'0 {_13} {[#"../01_resolve_unsoundness.rs" 14 17 14 22] false} (fun (_ret':()) -> 
               [ &_12 <- _ret' ]
               bb5))
         | bb5 = UIntSize.add {i} {[#"../01_resolve_unsoundness.rs" 15 13 15 14] (1 : usize)} (fun (_ret':usize) -> 
@@ -200,7 +201,7 @@ module C01ResolveUnsoundness_MakeVecOfSize
     | & _12 : () = any_l () : ()
     | & _13 : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) = any_l () : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) ]
 
-    [ return' (result:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))-> {[#"../01_resolve_unsoundness.rs" 8 10 8 29] Seq.length (shallow_model0 result) = UIntSize.to_int n}
+    [ return' (result:Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))-> {[#"../01_resolve_unsoundness.rs" 8 10 8 29] Seq.length (shallow_model'0 result) = UIntSize.to_int n}
       (! return' {result}) ]
 
 end
diff --git a/creusot/tests/should_fail/bug/222.stderr b/creusot/tests/should_fail/bug/222.stderr
@@ -1,4 +1,4 @@
-thread 'rustc' panicked at creusot/src/backend/clone_map.rs:415:33:
+thread 'rustc' panicked at creusot/src/backend/clone_map.rs:424:33:
 cannot get ident of used module Used("C222_Once_Type", "t_once")
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
 

diff --git a/creusot/tests/should_fail/bug/436_0.stderr b/creusot/tests/should_fail/bug/436_0.stderr
@@ -4,7 +4,7 @@ error: called Logic { prophetic: true } function in Logic { prophetic: false } c
 15 |     b.g = snapshot! { prophecy(b) + 1i32 };
    |                       ^^^^^^^^
 
-thread 'rustc' panicked at creusot/src/backend/clone_map.rs:415:33:
+thread 'rustc' panicked at creusot/src/backend/clone_map.rs:424:33:
 cannot get ident of used module Used("C4360_S_Type", "t_s")
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
 

diff --git a/creusot/tests/should_fail/bug/436_1.stderr b/creusot/tests/should_fail/bug/436_1.stderr
@@ -6,7 +6,7 @@ error: called Logic { prophetic: true } function in Logic { prophetic: false } c
    |
    = note: this error originates in the macro `pearlite` (in Nightly builds, run with -Z macro-backtrace for more info)
 
-thread 'rustc' panicked at creusot/src/backend/clone_map.rs:415:33:
+thread 'rustc' panicked at creusot/src/backend/clone_map.rs:424:33:
 cannot get ident of used module Used("C4361_S_Type", "t_s")
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace