Merge pull request #908 from xldenis/deep-model-fixes

change the deep model of Box<T> to Box<T::DeepModelTy>

creusot-contracts-proc/src/pretyping.rs

@@ -34,10 +34,16 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
         // it's impossible to handle proc macros whose parameters is not valid pearlite syntax,
         // or we don't translate parameters, but then we let the user write non-pearlite code
         // in pearlite...
-        RT::Macro(ExprMacro { mac: Macro { path, .. }, .. }) if path.is_ident("proof_assert") => {
-            Ok(term.to_token_stream())
+        RT::Macro(ExprMacro { mac, .. }) => {
+            if mac.path.is_ident("proof_assert") || mac.path.is_ident("pearlite") {
+                Ok(term.to_token_stream())
+            } else {
+                Err(EncodeError::Unsupported(
+                    term.span(),
+                    "Macros other than pearlite! or proof_assert! are unsupported".into(),
+                ))
+            }
         }
-        RT::Macro(_) => Err(EncodeError::Unsupported(term.span(), "Macro".into())),
         RT::Array(_) => Err(EncodeError::Unsupported(term.span(), "Array".into())),
         RT::Binary(TermBinary { left, op, right }) => {
             let mut left = left;

creusot-contracts/src/logic/seq.rs

@@ -154,7 +154,7 @@ impl<T> Seq<&T> {
     #[open]
     #[trusted]
     #[creusot::builtins = "prelude.Seq.to_owned"]
-    pub fn to_owned(self) -> Seq<T> {
+    pub fn to_owned_seq(self) -> Seq<T> {
         pearlite! {absurd}
     }
 }

creusot-contracts/src/num_rational.rs

@@ -1,6 +1,6 @@
 use std::marker::PhantomData;
 
-use crate::{ghost, open, trusted, DeepModel, OrdLogic};
+use crate::{ghost, open, pearlite, trusted, DeepModel, Int, OrdLogic};
 use num_rational::BigRational;
 use std::cmp::Ordering;
 
@@ -20,6 +20,15 @@ impl DeepModel for BigRational {
     }
 }
 
+impl Real {
+    #[ghost]
+    #[trusted]
+    #[open(self)]
+    pub fn from_int(i: Int) -> Self {
+        pearlite! { absurd }
+    }
+}
+
 impl OrdLogic for Real {
     #[ghost]
     #[open]

creusot-contracts/src/std/boxed.rs

@@ -3,11 +3,11 @@ pub use ::std::boxed::*;
 
 #[cfg(creusot)]
 impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Box<T, A> {
-    type DeepModelTy = T::DeepModelTy;
+    type DeepModelTy = Box<T::DeepModelTy>;
     #[ghost]
     #[open]
     fn deep_model(self) -> Self::DeepModelTy {
-        (*self).deep_model()
+        Box::new((*self).deep_model())
     }
 }
 

creusot-contracts/src/std/cmp.rs

@@ -13,6 +13,12 @@ extern_spec! {
                 where
                     Self: DeepModel,
                     Rhs: DeepModel<DeepModelTy = Self::DeepModelTy>;
+
+                #[ensures(result == (self.deep_model() != rhs.deep_model()))]
+                fn ne(&self, rhs: &Rhs) -> bool
+                where
+                    Self: DeepModel,
+                    Rhs: DeepModel<DeepModelTy = Self::DeepModelTy>;
             }
 
             // TODO: for now, we only support total orders

creusot/src/cleanup_spec_closures.rs

@@ -85,7 +85,10 @@ impl<'tcx> MutVisitor<'tcx> for NoTranslateNoMoves<'tcx> {
                 {
                     substs.iter_mut().for_each(|p| {
                         if p.is_move() {
-                            self.unused.insert(p.place().unwrap().as_local().unwrap());
+                            let place = p.place().unwrap();
+                            if let Some(loc) = place.as_local() {
+                                self.unused.insert(loc);
+                            }
                         }
                     });
                     *substs = IndexVec::new();

creusot/tests/should_succeed/syntax/derive_macros.mlcfg

@@ -1270,6 +1270,210 @@ module DeriveMacros_Impl7_Resolve
   val resolve [#"../derive_macros.rs" 56 9 56 16] (self : DeriveMacros_Sum2_Type.t_sum2 a b) : bool
     ensures { result = resolve self }
 
+end
+module Core_Option_Option_Type
+  type t_option 't =
+    | C_None
+    | C_Some 't
+
+end
+module DeriveMacros_List_Type
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  type t_list 't =
+    | C_List 't (Core_Option_Option_Type.t_option (t_list 't))
+
+  let function list_elem (self : t_list 't) : 't = [@vc:do_not_keep_trace] [@vc:sp]
+    match (self) with
+      | C_List a _ -> a
+      end
+  let function list_tail (self : t_list 't) : Core_Option_Option_Type.t_option (t_list 't)
+   = [@vc:do_not_keep_trace] [@vc:sp]
+    match (self) with
+      | C_List _ a -> a
+      end
+end
+module DeriveMacros_ListDeepModel_Type
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  type t_listdeepmodel 't 'proj0 =
+    | C_ListDeepModel 'proj0 (Core_Option_Option_Type.t_option (t_listdeepmodel 't 'proj0))
+
+end
+module CreusotContracts_Std1_Option_Impl0_DeepModel_Stub
+  type t
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  function deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy
+
+end
+module CreusotContracts_Std1_Option_Impl0_DeepModel_Interface
+  type t
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  function deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy
+
+  val deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module CreusotContracts_Std1_Option_Impl0_DeepModel
+  type t
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with
+    type self = t,
+    type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  function deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy
+
+   =
+    [#"../../../../../creusot-contracts/src/std/option.rs" 10 8 13 9] match (self) with
+      | Core_Option_Option_Type.C_Some t -> Core_Option_Option_Type.C_Some (DeepModel0.deep_model t)
+      | Core_Option_Option_Type.C_None -> Core_Option_Option_Type.C_None
+      end
+  val deep_model (self : Core_Option_Option_Type.t_option t) : Core_Option_Option_Type.t_option DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module Alloc_Boxed_Box_Type
+  use Core_Ptr_Unique_Unique_Type as Core_Ptr_Unique_Unique_Type
+  type t_box 't 'a =
+    | C_Box (Core_Ptr_Unique_Unique_Type.t_unique 't) 'a
+
+end
+module DeriveMacros_Impl8_DeepModel_Stub
+  type t
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  use DeriveMacros_ListDeepModel_Type as DeriveMacros_ListDeepModel_Type
+  use DeriveMacros_List_Type as DeriveMacros_List_Type
+  function deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+
+end
+module DeriveMacros_Impl8_DeepModel_Interface
+  type t
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  use DeriveMacros_ListDeepModel_Type as DeriveMacros_ListDeepModel_Type
+  use DeriveMacros_List_Type as DeriveMacros_List_Type
+  function deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+
+  val deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module DeriveMacros_Impl8_DeepModel
+  type t
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  use DeriveMacros_ListDeepModel_Type as DeriveMacros_ListDeepModel_Type
+  use Alloc_Boxed_Box_Type as Alloc_Boxed_Box_Type
+  use Core_Option_Option_Type as Core_Option_Option_Type
+  use DeriveMacros_List_Type as DeriveMacros_List_Type
+  clone CreusotContracts_Std1_Option_Impl0_DeepModel_Stub as DeepModel1 with
+    type t = DeriveMacros_List_Type.t_list t,
+    type DeepModelTy0.deepModelTy = DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+  clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with
+    type self = t,
+    type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy
+  function deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+
+   =
+    [#"../derive_macros.rs" 62 9 729 44] DeriveMacros_ListDeepModel_Type.C_ListDeepModel (DeepModel0.deep_model (DeriveMacros_List_Type.list_elem self)) (DeepModel1.deep_model (DeriveMacros_List_Type.list_tail self))
+  val deep_model [#"../derive_macros.rs" 62 9 62 18] (self : DeriveMacros_List_Type.t_list t) : DeriveMacros_ListDeepModel_Type.t_listdeepmodel t DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module DeriveMacros_Expr_Type
+  type t_expr 'v =
+    | C_Var 'v
+    | C_Add (t_expr 'v) (t_expr 'v)
+
+end
+module DeriveMacros_ExprDeepModel_Type
+  type t_exprdeepmodel 'v 'proj0 =
+    | C_Var 'proj0
+    | C_Add (t_exprdeepmodel 'v 'proj0) (t_exprdeepmodel 'v 'proj0)
+
+end
+module CreusotContracts_Std1_Boxed_Impl0_DeepModel_Stub
+  type t
+  type a
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  function deep_model (self : t) : DeepModelTy0.deepModelTy
+end
+module CreusotContracts_Std1_Boxed_Impl0_DeepModel_Interface
+  type t
+  type a
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  function deep_model (self : t) : DeepModelTy0.deepModelTy
+  val deep_model (self : t) : DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module CreusotContracts_Std1_Boxed_Impl0_DeepModel
+  type t
+  type a
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = t
+  clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with
+    type self = t,
+    type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy
+  function deep_model (self : t) : DeepModelTy0.deepModelTy =
+    [#"../../../../../creusot-contracts/src/std/boxed.rs" 10 17 10 37] DeepModel0.deep_model self
+  val deep_model (self : t) : DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module DeriveMacros_Impl9_DeepModel_Stub
+  type v
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = v
+  use DeriveMacros_ExprDeepModel_Type as DeriveMacros_ExprDeepModel_Type
+  use DeriveMacros_Expr_Type as DeriveMacros_Expr_Type
+  function deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+
+end
+module DeriveMacros_Impl9_DeepModel_Interface
+  type v
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = v
+  use DeriveMacros_ExprDeepModel_Type as DeriveMacros_ExprDeepModel_Type
+  use DeriveMacros_Expr_Type as DeriveMacros_Expr_Type
+  function deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+
+  val deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
+end
+module DeriveMacros_Impl9_DeepModel
+  type v
+  use Alloc_Alloc_Global_Type as Alloc_Alloc_Global_Type
+  clone CreusotContracts_Model_DeepModel_DeepModelTy_Type as DeepModelTy0 with
+    type self = v
+  use DeriveMacros_ExprDeepModel_Type as DeriveMacros_ExprDeepModel_Type
+  use DeriveMacros_Expr_Type as DeriveMacros_Expr_Type
+  clone CreusotContracts_Std1_Boxed_Impl0_DeepModel_Stub as DeepModel1 with
+    type t = DeriveMacros_Expr_Type.t_expr v,
+    type a = Alloc_Alloc_Global_Type.t_global,
+    type DeepModelTy0.deepModelTy = DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+  clone CreusotContracts_Model_DeepModel_DeepModel_Stub as DeepModel0 with
+    type self = v,
+    type DeepModelTy0.deepModelTy = DeepModelTy0.deepModelTy
+  function deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+
+   =
+    [#"../derive_macros.rs" 68 9 68 18] match (self) with
+      | DeriveMacros_Expr_Type.C_Var v0_1 -> DeriveMacros_ExprDeepModel_Type.C_Var (DeepModel0.deep_model v0_1)
+      | DeriveMacros_Expr_Type.C_Add v0_1 v1_1 -> DeriveMacros_ExprDeepModel_Type.C_Add (DeepModel1.deep_model v0_1) (DeepModel1.deep_model v1_1)
+      end
+  val deep_model [#"../derive_macros.rs" 68 9 68 18] (self : DeriveMacros_Expr_Type.t_expr v) : DeriveMacros_ExprDeepModel_Type.t_exprdeepmodel v DeepModelTy0.deepModelTy
+    ensures { result = deep_model self }
+
 end
 module DeriveMacros_Impl2
   type a
@@ -1385,6 +1589,12 @@ module DeriveMacros_Impl1
   type a
   type b
 end
+module DeriveMacros_Impl8
+  type t
+end
+module DeriveMacros_Impl9
+  type v
+end
 module DeriveMacros_Impl6
   type a
 end

creusot/tests/should_succeed/syntax/derive_macros.rs

@@ -58,3 +58,15 @@ pub enum Sum2<A, B> {
     X(A),
     Y { a: bool, x: B },
 }
+
+#[derive(DeepModel)]
+pub struct List<T> {
+    pub elem: T,
+    pub tail: Option<Box<List<T>>>,
+}
+
+#[derive(DeepModel)]
+pub enum Expr<V> {
+    Var(V),
+    Add(Box<Expr<V>>, Box<Expr<V>>),
+}