Ugly commit.

prusti-common/src/vir/low_to_viper/ast.rs

@@ -141,6 +141,11 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for statement::Fold {
             "Statement with default position: {}",
             self
         );
+        assert!(
+            self.expression.is_predicate_access_predicate(),
+            "fold {}",
+            self.expression
+        );
         ast.fold_with_pos(
             self.expression.to_viper(context, ast),
             self.position.to_viper(context, ast),
@@ -155,6 +160,11 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for statement::Unfold {
             "Statement with default position: {}",
             self
         );
+        assert!(
+            self.expression.is_predicate_access_predicate(),
+            "unfold {}",
+            self.expression
+        );
         ast.unfold_with_pos(
             self.expression.to_viper(context, ast),
             self.position.to_viper(context, ast),
@@ -235,7 +245,7 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expression {
             Expression::MagicWand(expression) => expression.to_viper(context, ast),
             Expression::PredicateAccessPredicate(expression) => expression.to_viper(context, ast),
             // Expression::FieldAccessPredicate(expression) => expression.to_viper(context, ast),
-            // Expression::Unfolding(expression) => expression.to_viper(context, ast),
+            Expression::Unfolding(expression) => expression.to_viper(context, ast),
             Expression::UnaryOp(expression) => expression.to_viper(context, ast),
             Expression::BinaryOp(expression) => expression.to_viper(context, ast),
             Expression::PermBinaryOp(expression) => expression.to_viper(context, ast),
@@ -361,6 +371,16 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for expression::PredicateAccessPredicate {
     }
 }
 
+impl<'v> ToViper<'v, viper::Expr<'v>> for expression::Unfolding {
+    fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> viper::Expr<'v> {
+        ast.unfolding_with_pos(
+            self.predicate.to_viper(context, ast),
+            self.base.to_viper(context, ast),
+            self.position.to_viper(context, ast),
+        )
+    }
+}
+
 impl<'v> ToViper<'v, viper::Expr<'v>> for expression::UnaryOp {
     fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> viper::Expr<'v> {
         match self.op_kind {

prusti-contracts/prusti-contracts-proc-macros/src/lib.rs

@@ -16,6 +16,12 @@ pub fn invariant(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
     tokens
 }
 
+#[cfg(not(feature = "prusti"))]
+#[proc_macro_attribute]
+pub fn structural_invariant(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    tokens
+}
+
 #[cfg(not(feature = "prusti"))]
 #[proc_macro_attribute]
 pub fn ensures(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
@@ -118,6 +124,36 @@ pub fn body_variant(_tokens: TokenStream) -> TokenStream {
     TokenStream::new()
 }
 
+#[cfg(not(feature = "prusti"))]
+#[proc_macro]
+pub fn pack(_tokens: TokenStream) -> TokenStream {
+    TokenStream::new()
+}
+
+#[cfg(not(feature = "prusti"))]
+#[proc_macro]
+pub fn unpack(_tokens: TokenStream) -> TokenStream {
+    TokenStream::new()
+}
+
+#[cfg(not(feature = "prusti"))]
+#[proc_macro]
+pub fn forget_initialization(_tokens: TokenStream) -> TokenStream {
+    TokenStream::new()
+}
+
+#[cfg(not(feature = "prusti"))]
+#[proc_macro]
+pub fn restore(_tokens: TokenStream) -> TokenStream {
+    TokenStream::new()
+}
+
+#[cfg(not(feature = "prusti"))]
+#[proc_macro]
+pub fn set_union_active_field(_tokens: TokenStream) -> TokenStream {
+    TokenStream::new()
+}
+
 // ----------------------
 // --- PRUSTI ENABLED ---
 
@@ -204,7 +240,13 @@ pub fn extern_spec(attr: TokenStream, tokens: TokenStream) -> TokenStream {
 #[cfg(feature = "prusti")]
 #[proc_macro_attribute]
 pub fn invariant(attr: TokenStream, tokens: TokenStream) -> TokenStream {
-    prusti_specs::invariant(attr.into(), tokens.into()).into()
+    prusti_specs::invariant(attr.into(), tokens.into(), false).into()
+}
+
+#[cfg(feature = "prusti")]
+#[proc_macro_attribute]
+pub fn structural_invariant(attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    prusti_specs::invariant(attr.into(), tokens.into(), true).into()
 }
 
 #[cfg(feature = "prusti")]
@@ -254,5 +296,35 @@ pub fn body_variant(tokens: TokenStream) -> TokenStream {
     prusti_specs::body_variant(tokens.into()).into()
 }
 
+#[cfg(feature = "prusti")]
+#[proc_macro]
+pub fn pack(tokens: TokenStream) -> TokenStream {
+    prusti_specs::pack(tokens.into()).into()
+}
+
+#[cfg(feature = "prusti")]
+#[proc_macro]
+pub fn unpack(tokens: TokenStream) -> TokenStream {
+    prusti_specs::unpack(tokens.into()).into()
+}
+
+#[cfg(feature = "prusti")]
+#[proc_macro]
+pub fn forget_initialization(tokens: TokenStream) -> TokenStream {
+    prusti_specs::forget_initialization(tokens.into()).into()
+}
+
+#[cfg(feature = "prusti")]
+#[proc_macro]
+pub fn restore(tokens: TokenStream) -> TokenStream {
+    prusti_specs::restore(tokens.into()).into()
+}
+
+#[cfg(feature = "prusti")]
+#[proc_macro]
+pub fn set_union_active_field(tokens: TokenStream) -> TokenStream {
+    prusti_specs::set_union_active_field(tokens.into()).into()
+}
+
 // Ensure that you've also crated a transparent `#[cfg(not(feature = "prusti"))]`
 // version of your new macro above!

prusti-contracts/prusti-contracts/src/core_spec.rs

@@ -16,3 +16,48 @@ impl<T, E: ::core::fmt::Debug> ::core::result::Result<T, E> {
     #[requires(matches!(self, Ok(_)))]
     fn unwrap(self) -> T;
 }
+
+// Crashes ☹
+type Pointer<T> = *const T;
+#[extern_spec]
+impl<T> Pointer<T> {
+    #[trusted]
+    #[pure]
+    // FIXME: This is needed because this function is special cased only in the
+    // pure encoder and not in the impure one.
+    #[ensures(result == self.is_null())]
+    fn is_null(self) -> bool;
+}
+
+type MutPointer<T> = *mut T;
+#[extern_spec]
+impl<T> MutPointer<T> {
+    #[trusted]
+    #[pure]
+    // FIXME: This is needed because this function is special cased only in the
+    // pure encoder and not in the impure one.
+    #[ensures(result == self.is_null())]
+    fn is_null(self) -> bool;
+}
+
+#[extern_spec]
+mod core {
+    mod mem {
+        use crate::*;
+
+        #[pure]
+        // FIXME: This is needed because this function is special cased only in the
+        // pure encoder and not in the impure one.
+        #[ensures(result == core::mem::size_of::<T>())]
+        pub fn size_of<T>() -> usize;
+
+        #[pure]
+        // FIXME: What are the guarantees?
+        // https://doc.rust-lang.org/std/mem/fn.align_of.html says nothing…
+        #[ensures(result > 0)]
+        // FIXME: This is needed because this function is special cased only in the
+        // pure encoder and not in the impure one.
+        #[ensures(result == core::mem::align_of::<T>())]
+        pub fn align_of<T>() -> usize;
+    }
+}

prusti-contracts/prusti-contracts/src/lib.rs

@@ -21,6 +21,10 @@ pub use prusti_contracts_proc_macros::trusted;
 /// A macro for type invariants.
 pub use prusti_contracts_proc_macros::invariant;
 
+/// A macro for structural type invariants. A type with a structural
+/// invariant needs to be managed manually by the user.
+pub use prusti_contracts_proc_macros::structural_invariant;
+
 /// A macro for writing a loop body invariant.
 pub use prusti_contracts_proc_macros::body_invariant;
 
@@ -60,6 +64,21 @@ pub use prusti_contracts_proc_macros::terminates;
 /// A macro to annotate body variant of a loop to prove termination
 pub use prusti_contracts_proc_macros::body_variant;
 
+/// A macro to manually pack a place capability.
+pub use prusti_contracts_proc_macros::pack;
+
+/// A macro to manually unpack a place capability.
+pub use prusti_contracts_proc_macros::unpack;
+
+/// A macro to forget that a place is initialized.
+pub use prusti_contracts_proc_macros::forget_initialization;
+
+/// A macro to restore a place capability.
+pub use prusti_contracts_proc_macros::restore;
+
+/// A macro to set a specific field of the union as active.
+pub use prusti_contracts_proc_macros::set_union_active_field;
+
 #[cfg(not(feature = "prusti"))]
 mod private {
     use core::marker::PhantomData;
@@ -338,4 +357,76 @@ pub fn snapshot_equality<T>(_l: T, _r: T) -> bool {
     true
 }
 
+#[doc(hidden)]
+#[trusted]
+pub fn prusti_pack_place<T>(_arg: T) {
+    unreachable!();
+}
+
+#[doc(hidden)]
+#[trusted]
+pub fn prusti_unpack_place<T>(_arg: T) {
+    unreachable!();
+}
+
+#[doc(hidden)]
+#[trusted]
+pub fn prusti_forget_initialization<T>(_arg: T) {
+    unreachable!();
+}
+
+#[doc(hidden)]
+#[trusted]
+pub fn prusti_restore_place<T>(_arg1: T, _arg2: T) {
+    unreachable!();
+}
+
+#[doc(hidden)]
+#[trusted]
+pub fn prusti_set_union_active_field<T>(_arg: T) {
+    unreachable!();
+}
+
+/// Indicates that we have the `own` capability to the specified place.
+#[doc(hidden)]
+#[trusted]
+pub fn prusti_own<T>(_place: T) -> bool {
+    true
+}
+
+#[macro_export]
+macro_rules! own {
+    ($place:expr) => {
+        $crate::prusti_own(unsafe { core::ptr::addr_of!($place) })
+    };
+}
+
+/// Indicates that we have the `raw` capability to the specified address.
+#[doc(hidden)]
+#[trusted]
+pub fn prusti_raw<T>(_address: T, _size: usize) -> bool {
+    true
+}
+
+#[macro_export]
+macro_rules! raw {
+    ($place:expr, $size: expr) => {
+        $crate::prusti_raw(unsafe { core::ptr::addr_of!($place) }, $size)
+    };
+}
+
+/// Indicates that we have the capability to deallocate.
+#[doc(hidden)]
+#[trusted]
+pub fn prusti_raw_dealloc<T>(_address: T, _size: usize) -> bool {
+    true
+}
+
+#[macro_export]
+macro_rules! raw_dealloc {
+    ($place:expr, $size: expr, $align: expr) => {
+        $crate::prusti_raw_dealloc(unsafe { core::ptr::addr_of!($place) }, $size)
+    };
+}
+
 pub use private::*;