Merge pull request #988 from creusot-rs/string-specs

Basic specs for strings and str
creusot-rs · Apr 7, 2024 · 6a569c9 · 6a569c9
2 parents 1357cc9 + b3221d2
commit 6a569c9
Show file tree

Hide file tree

Showing 57 changed files with 342 additions and 288 deletions.
diff --git a/creusot-contracts/src/model.rs b/creusot-contracts/src/model.rs
@@ -43,6 +43,17 @@ impl<T> ShallowModel for Rc<T> {
     }
 }
 
+impl ShallowModel for str {
+    type ShallowModelTy = Seq<char>;
+
+    #[logic]
+    #[open]
+    #[trusted]
+    fn shallow_model(self) -> Self::ShallowModelTy {
+        pearlite! { absurd }
+    }
+}
+
 impl<T: DeepModel> DeepModel for Arc<T> {
     type DeepModelTy = T::DeepModelTy;
     #[logic]
@@ -107,3 +118,14 @@ impl DeepModel for bool {
         self
     }
 }
+
+impl ShallowModel for String {
+    type ShallowModelTy = Seq<char>;
+
+    #[logic]
+    #[open(self)]
+    #[trusted]
+    fn shallow_model(self) -> Self::ShallowModelTy {
+        pearlite! { absurd }
+    }
+}
diff --git a/creusot-contracts/src/std.rs b/creusot-contracts/src/std.rs
@@ -14,6 +14,7 @@ pub mod ops;
 pub mod option;
 pub mod result;
 pub mod slice;
+pub mod string;
 pub mod time;
 mod tuples;
 pub mod vec;
diff --git a/creusot-contracts/src/std/string.rs b/creusot-contracts/src/std/string.rs
@@ -0,0 +1,31 @@
+use crate::*;
+use ::std::ops::Deref;
+
+extern_spec! {
+    mod std {
+        mod string {
+            impl Deref for String {
+                #[ensures(result@ == self@)]
+                fn deref(&self) -> &str;
+            }
+
+            impl String {
+                #[ensures(result@ == self@.len())]
+                fn len(&self) -> usize;
+
+            }
+        }
+    }
+}
+
+extern_spec! {
+    impl str {
+        #[ensures(result@ == self@)]
+        fn to_string(&self) -> String;
+
+        #[requires(ix@ < self@.len())]
+        #[ensures(result.0@.concat(result.1@) == self@)]
+        #[ensures(result.0@.len() == ix@)]
+        fn split_at(&self, ix : usize) -> (&str, &str);
+    }
+}
diff --git a/creusot/tests/should_fail/bug/01_resolve_unsoundness.mlcfg b/creusot/tests/should_fail/bug/01_resolve_unsoundness.mlcfg
@@ -106,7 +106,7 @@ module C01ResolveUnsoundness_MakeVecOfSize
   function shallow_model2 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) : Seq.seq bool
 
    =
-    [#"../../../../../creusot-contracts/src/model.rs" 97 8 97 31] shallow_model0 ( * self)
+    [#"../../../../../creusot-contracts/src/model.rs" 108 8 108 31] shallow_model0 ( * self)
   val shallow_model2 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) : Seq.seq bool
     ensures { result = shallow_model2 self }
 

diff --git a/creusot/tests/should_fail/final_borrows.mlcfg b/creusot/tests/should_fail/final_borrows.mlcfg
@@ -330,7 +330,7 @@ module FinalBorrows_Indexing
     ensures { result = index_logic1 self ix }
 
   function shallow_model0 (self : borrowed (slice t)) : Seq.seq t =
-    [#"../../../../creusot-contracts/src/model.rs" 97 8 97 31] shallow_model1 ( * self)
+    [#"../../../../creusot-contracts/src/model.rs" 108 8 108 31] shallow_model1 ( * self)
   val shallow_model0 (self : borrowed (slice t)) : Seq.seq t
     ensures { result = shallow_model0 self }
 

diff --git a/creusot/tests/should_succeed/100doors.mlcfg b/creusot/tests/should_succeed/100doors.mlcfg
@@ -299,7 +299,7 @@ module C100doors_F
   function shallow_model3 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) : Seq.seq bool
 
    =
-    [#"../../../../creusot-contracts/src/model.rs" 97 8 97 31] shallow_model0 ( * self)
+    [#"../../../../creusot-contracts/src/model.rs" 108 8 108 31] shallow_model0 ( * self)
   val shallow_model3 (self : borrowed (Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global))) : Seq.seq bool
     ensures { result = shallow_model3 self }
 
@@ -314,7 +314,7 @@ module C100doors_F
     ensures { inv10 result }
 
   function shallow_model2 (self : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) : Seq.seq bool =
-    [#"../../../../creusot-contracts/src/model.rs" 79 8 79 31] shallow_model0 self
+    [#"../../../../creusot-contracts/src/model.rs" 90 8 90 31] shallow_model0 self
   val shallow_model2 (self : Alloc_Vec_Vec_Type.t_vec bool (Alloc_Alloc_Global_Type.t_global)) : Seq.seq bool
     ensures { result = shallow_model2 self }