Merge pull request #927 from arnaudgolfouse/box-borrow-resolve

Box borrow resolve
creusot-rs · Jan 10, 2024 · a4348d7 · a4348d7
2 parents c05eead + 91e867f
commit a4348d7
Show file tree

Hide file tree

Showing 73 changed files with 1,047 additions and 799 deletions.
diff --git a/creusot-contracts/src/resolve.rs b/creusot-contracts/src/resolve.rs
@@ -9,7 +9,7 @@ pub trait Resolve {
 }
 
 #[trusted]
-impl<T1, T2> Resolve for (T1, T2) {
+impl<T1, T2: ?Sized> Resolve for (T1, T2) {
     #[predicate]
     #[open]
     fn resolve(self) -> bool {
@@ -26,9 +26,18 @@ impl<T: ?Sized> Resolve for &mut T {
     }
 }
 
+#[trusted]
+impl<T: ?Sized> Resolve for Box<T> {
+    #[predicate]
+    #[open]
+    fn resolve(self) -> bool {
+        Resolve::resolve(*self)
+    }
+}
+
 #[cfg(creusot)]
 #[trusted]
-impl<T> Resolve for T {
+impl<T: ?Sized> Resolve for T {
     #[predicate]
     #[open]
     #[rustc_diagnostic_item = "creusot_resolve_default"]

diff --git a/creusot/tests/should_fail/bug/492.mlcfg b/creusot/tests/should_fail/bug/492.mlcfg
@@ -154,21 +154,21 @@ module CreusotContracts_Resolve_Impl0_Resolve
     ensures { result = resolve self }
 
 end
-module CreusotContracts_Resolve_Impl2_Resolve_Stub
+module CreusotContracts_Resolve_Impl3_Resolve_Stub
   type t
   predicate resolve (self : t)
 end
-module CreusotContracts_Resolve_Impl2_Resolve_Interface
+module CreusotContracts_Resolve_Impl3_Resolve_Interface
   type t
   predicate resolve (self : t)
   val resolve (self : t) : bool
     ensures { result = resolve self }
 
 end
-module CreusotContracts_Resolve_Impl2_Resolve
+module CreusotContracts_Resolve_Impl3_Resolve
   type t
   predicate resolve (self : t) =
-    [#"../../../../../creusot-contracts/src/resolve.rs" 36 8 36 12] true
+    [#"../../../../../creusot-contracts/src/resolve.rs" 45 8 45 12] true
   val resolve (self : t) : bool
     ensures { result = resolve self }
 
@@ -197,7 +197,7 @@ module C492_Test
     axiom .
   clone CreusotContracts_Resolve_Impl1_Resolve as Resolve1 with
     type t = int32
-  clone CreusotContracts_Resolve_Impl2_Resolve as Resolve2 with
+  clone CreusotContracts_Resolve_Impl3_Resolve as Resolve2 with
     type t = uint32
   clone CreusotContracts_Resolve_Impl0_Resolve as Resolve0 with
     type t1 = borrowed int32,

diff --git a/creusot/tests/should_fail/bug/692.mlcfg b/creusot/tests/should_fail/bug/692.mlcfg
@@ -835,21 +835,21 @@ module C692_Incorrect
   }
 
 end
-module CreusotContracts_Resolve_Impl2_Resolve_Stub
+module CreusotContracts_Resolve_Impl3_Resolve_Stub
   type t
   predicate resolve (self : t)
 end
-module CreusotContracts_Resolve_Impl2_Resolve_Interface
+module CreusotContracts_Resolve_Impl3_Resolve_Interface
   type t
   predicate resolve (self : t)
   val resolve (self : t) : bool
     ensures { result = resolve self }
 
 end
-module CreusotContracts_Resolve_Impl2_Resolve
+module CreusotContracts_Resolve_Impl3_Resolve
   type t
   predicate resolve (self : t) =
-    [#"../../../../../creusot-contracts/src/resolve.rs" 36 8 36 12] true
+    [#"../../../../../creusot-contracts/src/resolve.rs" 45 8 45 12] true
   val resolve (self : t) : bool
     ensures { result = resolve self }
 

diff --git a/creusot/tests/should_fail/bug/695.mlcfg b/creusot/tests/should_fail/bug/695.mlcfg
@@ -1037,21 +1037,21 @@ module C695_InversedIf
   }
 
 end
-module CreusotContracts_Resolve_Impl2_Resolve_Stub
+module CreusotContracts_Resolve_Impl3_Resolve_Stub
   type t
   predicate resolve (self : t)
 end
-module CreusotContracts_Resolve_Impl2_Resolve_Interface
+module CreusotContracts_Resolve_Impl3_Resolve_Interface
   type t
   predicate resolve (self : t)
   val resolve (self : t) : bool
     ensures { result = resolve self }
 
 end
-module CreusotContracts_Resolve_Impl2_Resolve
+module CreusotContracts_Resolve_Impl3_Resolve
   type t
   predicate resolve (self : t) =
-    [#"../../../../../creusot-contracts/src/resolve.rs" 36 8 36 12] true
+    [#"../../../../../creusot-contracts/src/resolve.rs" 45 8 45 12] true
   val resolve (self : t) : bool
     ensures { result = resolve self }
 

diff --git a/creusot/tests/should_succeed/100doors.mlcfg b/creusot/tests/should_succeed/100doors.mlcfg
@@ -1054,21 +1054,21 @@ module CreusotContracts_Std1_Slice_Impl5_ResolveElswhere
     ensures { result = resolve_elswhere self old' fin }
 
 end
-module CreusotContracts_Resolve_Impl2_Resolve_Stub
+module CreusotContracts_Resolve_Impl3_Resolve_Stub
   type t
   predicate resolve (self : t)
 end
-module CreusotContracts_Resolve_Impl2_Resolve_Interface
+module CreusotContracts_Resolve_Impl3_Resolve_Interface
   type t
   predicate resolve (self : t)
   val resolve (self : t) : bool
     ensures { result = resolve self }
 
 end
-module CreusotContracts_Resolve_Impl2_Resolve
+module CreusotContracts_Resolve_Impl3_Resolve
   type t
   predicate resolve (self : t) =
-    [#"../../../../creusot-contracts/src/resolve.rs" 36 8 36 12] true
+    [#"../../../../creusot-contracts/src/resolve.rs" 45 8 45 12] true
   val resolve (self : t) : bool
     ensures { result = resolve self }
 
@@ -1175,7 +1175,7 @@ module C100doors_F
     type t = Core_Ops_Range_Range_Type.t_range usize,
     predicate Inv0.inv = Inv0.inv,
     axiom .
-  clone CreusotContracts_Resolve_Impl2_Resolve as Resolve3 with
+  clone CreusotContracts_Resolve_Impl3_Resolve as Resolve3 with
     type t = bool
   clone Core_Num_Impl11_Max as Max0
   clone CreusotContracts_Std1_Vec_Impl0_ShallowModel_Interface as ShallowModel0 with

diff --git a/creusot/tests/should_succeed/bdd.mlcfg b/creusot/tests/should_succeed/bdd.mlcfg
@@ -895,21 +895,21 @@ module Core_Cmp_Impls_Impl25_Eq_Interface
     ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 11 26 11 75] result = (DeepModel0.deep_model self = DeepModel0.deep_model other) }
 
 end
-module CreusotContracts_Resolve_Impl2_Resolve_Stub
+module CreusotContracts_Resolve_Impl3_Resolve_Stub
   type t
   predicate resolve (self : t)
 end
-module CreusotContracts_Resolve_Impl2_Resolve_Interface
+module CreusotContracts_Resolve_Impl3_Resolve_Interface
   type t
   predicate resolve (self : t)
   val resolve (self : t) : bool
     ensures { result = resolve self }
 
 end
-module CreusotContracts_Resolve_Impl2_Resolve
+module CreusotContracts_Resolve_Impl3_Resolve
   type t
   predicate resolve (self : t) =
-    [#"../../../../creusot-contracts/src/resolve.rs" 36 8 36 12] true
+    [#"../../../../creusot-contracts/src/resolve.rs" 45 8 45 12] true
   val resolve (self : t) : bool
     ensures { result = resolve self }
 
@@ -1003,7 +1003,7 @@ module Bdd_Impl14_Eq
     function ShallowModel0.shallow_model = ShallowModel1.shallow_model
   clone Bdd_Impl7_Eq_Interface as Eq0 with
     function ShallowModel0.shallow_model = ShallowModel0.shallow_model
-  clone CreusotContracts_Resolve_Impl2_Resolve as Resolve1 with
+  clone CreusotContracts_Resolve_Impl3_Resolve as Resolve1 with
     type t = Bdd_Node_Type.t_node
   clone CreusotContracts_Resolve_Impl0_Resolve as Resolve0 with
     type t1 = Bdd_Node_Type.t_node,
@@ -4359,7 +4359,7 @@ module Bdd_Impl11_And
     function Interp0.interp = Interp0.interp,
     val Max0.mAX' = Max0.mAX',
     function Leastvar0.leastvar = Leastvar0.leastvar
-  clone CreusotContracts_Resolve_Impl2_Resolve as Resolve4 with
+  clone CreusotContracts_Resolve_Impl3_Resolve as Resolve4 with
     type t = Bdd_Node_Type.t_node
   clone CreusotContracts_Resolve_Impl0_Resolve as Resolve2 with
     type t1 = Bdd_Node_Type.t_node,
@@ -4368,7 +4368,7 @@ module Bdd_Impl11_And
     predicate Resolve1.resolve = Resolve4.resolve
   clone CreusotContracts_Resolve_Impl1_Resolve as Resolve1 with
     type t = Bdd_Context_Type.t_context
-  clone CreusotContracts_Resolve_Impl2_Resolve as Resolve3 with
+  clone CreusotContracts_Resolve_Impl3_Resolve as Resolve3 with
     type t = Bdd_Bdd_Type.t_bdd
   clone CreusotContracts_Resolve_Impl0_Resolve as Resolve0 with
     type t1 = Bdd_Bdd_Type.t_bdd,