diff --git a/creusot-contracts-proc/src/pretyping.rs b/creusot-contracts-proc/src/pretyping.rs index 32aeb176f0..7b8be3ec93 100644 --- a/creusot-contracts-proc/src/pretyping.rs +++ b/creusot-contracts-proc/src/pretyping.rs @@ -34,10 +34,16 @@ pub fn encode_term(term: &RT) -> Result { // 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; diff --git a/creusot-contracts/src/logic/seq.rs b/creusot-contracts/src/logic/seq.rs index 2a581d6720..c8f70bfcc5 100644 --- a/creusot-contracts/src/logic/seq.rs +++ b/creusot-contracts/src/logic/seq.rs @@ -154,7 +154,7 @@ impl Seq<&T> { #[open] #[trusted] #[creusot::builtins = "prelude.Seq.to_owned"] - pub fn to_owned(self) -> Seq { + pub fn to_owned_seq(self) -> Seq { pearlite! {absurd} } } diff --git a/creusot-contracts/src/num_rational.rs b/creusot-contracts/src/num_rational.rs index f6a50878fa..eeadf5e575 100644 --- a/creusot-contracts/src/num_rational.rs +++ b/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] diff --git a/creusot-contracts/src/std/boxed.rs b/creusot-contracts/src/std/boxed.rs index 804c110dbd..2e65842d17 100644 --- a/creusot-contracts/src/std/boxed.rs +++ b/creusot-contracts/src/std/boxed.rs @@ -3,11 +3,11 @@ pub use ::std::boxed::*; #[cfg(creusot)] impl DeepModel for Box { - type DeepModelTy = T::DeepModelTy; + type DeepModelTy = Box; #[ghost] #[open] fn deep_model(self) -> Self::DeepModelTy { - (*self).deep_model() + Box::new((*self).deep_model()) } } diff --git a/creusot-contracts/src/std/cmp.rs b/creusot-contracts/src/std/cmp.rs index 73aea832b8..ea8c76d6ea 100644 --- a/creusot-contracts/src/std/cmp.rs +++ b/creusot-contracts/src/std/cmp.rs @@ -13,6 +13,12 @@ extern_spec! { where Self: DeepModel, Rhs: DeepModel; + + #[ensures(result == (self.deep_model() != rhs.deep_model()))] + fn ne(&self, rhs: &Rhs) -> bool + where + Self: DeepModel, + Rhs: DeepModel; } // TODO: for now, we only support total orders diff --git a/creusot/src/cleanup_spec_closures.rs b/creusot/src/cleanup_spec_closures.rs index 28a202d60f..b62c5d5b62 100644 --- a/creusot/src/cleanup_spec_closures.rs +++ b/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(); diff --git a/creusot/tests/should_succeed/syntax/derive_macros.mlcfg b/creusot/tests/should_succeed/syntax/derive_macros.mlcfg index af6d045fa2..d831fd0b99 100644 --- a/creusot/tests/should_succeed/syntax/derive_macros.mlcfg +++ b/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 diff --git a/creusot/tests/should_succeed/syntax/derive_macros.rs b/creusot/tests/should_succeed/syntax/derive_macros.rs index c6afd02806..fc85641c23 100644 --- a/creusot/tests/should_succeed/syntax/derive_macros.rs +++ b/creusot/tests/should_succeed/syntax/derive_macros.rs @@ -58,3 +58,15 @@ pub enum Sum2 { X(A), Y { a: bool, x: B }, } + +#[derive(DeepModel)] +pub struct List { + pub elem: T, + pub tail: Option>>, +} + +#[derive(DeepModel)] +pub enum Expr { + Var(V), + Add(Box>, Box>), +}