Fix #874

creusot-rs · Oct 13, 2023 · c785d49 · c785d49
1 parent dd4fab0
commit c785d49
Show file tree

Hide file tree

Showing 31 changed files with 1,417 additions and 210 deletions.
diff --git a/creusot-contracts/src/std/vec.rs b/creusot-contracts/src/std/vec.rs
@@ -118,12 +118,14 @@ extern_spec! {
             }
 
             impl<T, A : Allocator> Extend<T> for Vec<T, A> {
-                #[ensures(exists<done_ : &mut I, prod: Seq<T>>
-                    done_.completed() && iter.produces(prod, *done_) && (^self)@ == self@.concat(prod)
+                #[requires(iter.into_iter_pre())]
+                #[ensures(exists<start_ : I::IntoIter, done_ : &mut I::IntoIter, prod: Seq<T>>
+                    iter.into_iter_post(start_) &&
+                    done_.completed() && start_.produces(prod, *done_) && (^self)@ == self@.concat(prod)
                 )]
                 fn extend<I>(&mut self, iter: I)
                 where
-                    I : Iterator<Item = T>;
+                    I : IntoIterator<Item = T>, I::IntoIter : Iterator;
             }
 
             impl<T, I : SliceIndex<[T]>, A : Allocator> IndexMut<I> for Vec<T, A> {

diff --git a/creusot/src/ctx.rs b/creusot/src/ctx.rs
@@ -191,7 +191,8 @@ impl<'tcx, 'sess> TranslationCtx<'tcx> {
 
     pub(crate) fn body_with_facts(&mut self, def_id: LocalDefId) -> &BodyWithBorrowckFacts<'tcx> {
         if !self.bodies.contains_key(&def_id) {
-            let body = callbacks::get_body(self.tcx, def_id).unwrap();
+            let body = callbacks::get_body(self.tcx, def_id)
+                .unwrap_or_else(|| panic!("did not find body for {def_id:?}"));
 
             // Basic clean up, replace FalseEdges with Gotos. Could potentially also replace other statement with Nops.
             // Investigate if existing MIR passes do this as part of 'post borrowck cleanup'.

diff --git a/creusot/tests/should_succeed/100doors.mlcfg b/creusot/tests/should_succeed/100doors.mlcfg
@@ -367,8 +367,8 @@ module Alloc_Vec_FromElem_Interface
     type t = t
   val from_elem (elem : t) (n : usize) : Alloc_Vec_Vec_Type.t_vec t (Alloc_Alloc_Global_Type.t_global)
     requires {Inv0.inv elem}
-    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 155 22 155 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n }
-    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 156 12 156 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem }
+    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 157 22 157 41] Seq.length (ShallowModel0.shallow_model result) = UIntSize.to_int n }
+    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 158 12 158 78] forall i : int . 0 <= i /\ i < UIntSize.to_int n -> IndexLogic0.index_logic result i = elem }
     ensures { Inv1.inv result }
 
 end
@@ -677,10 +677,10 @@ module Alloc_Vec_Impl12_Index_Interface
     type t = Alloc_Vec_Vec_Type.t_vec t a,
     type ShallowModelTy0.shallowModelTy = Seq.seq t
   val index (self : Alloc_Vec_Vec_Type.t_vec t a) (index : i) : Output0.output
-    requires {[#"../../../../creusot-contracts/src/std/vec.rs" 139 27 139 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../creusot-contracts/src/std/vec.rs" 141 27 141 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)}
     requires {Inv0.inv self}
     requires {Inv1.inv index}
-    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 140 26 140 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result }
+    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 142 26 142 54] HasValue0.has_value index (ShallowModel0.shallow_model self) result }
     ensures { Inv2.inv result }
 
 end
@@ -792,13 +792,13 @@ module Alloc_Vec_Impl13_IndexMut_Interface
     type t = Alloc_Vec_Vec_Type.t_vec t a,
     type ShallowModelTy0.shallowModelTy = Seq.seq t
   val index_mut (self : borrowed (Alloc_Vec_Vec_Type.t_vec t a)) (index : i) : borrowed Output0.output
-    requires {[#"../../../../creusot-contracts/src/std/vec.rs" 130 27 130 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)}
+    requires {[#"../../../../creusot-contracts/src/std/vec.rs" 132 27 132 46] InBounds0.in_bounds index (ShallowModel0.shallow_model self)}
     requires {Inv0.inv self}
     requires {Inv1.inv index}
-    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 131 26 131 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) }
-    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 132 26 132 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) }
-    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) }
-    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) }
+    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 133 26 133 54] HasValue0.has_value index (ShallowModel0.shallow_model self) ( * result) }
+    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 134 26 134 57] HasValue0.has_value index (ShallowModel1.shallow_model ( ^ self)) ( ^ result) }
+    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 135 26 135 62] ResolveElswhere0.resolve_elswhere index (ShallowModel0.shallow_model self) (ShallowModel1.shallow_model ( ^ self)) }
+    ensures { [#"../../../../creusot-contracts/src/std/vec.rs" 136 26 136 55] Seq.length (ShallowModel1.shallow_model ( ^ self)) = Seq.length (ShallowModel0.shallow_model self) }
     ensures { Inv2.inv result }
 
 end