Snapshot equality

prusti-contracts/src/lib.rs

@@ -343,12 +343,33 @@ pub fn old<T>(arg: T) -> T {
     arg
 }
 
+/// Universal quantifier.
+///
+/// This is a Prusti-internal representation of the `forall` syntax.
 pub fn forall<T, F>(_trigger_set: T, _closure: F) -> bool {
     true
 }
 
+/// Existential quantifier.
+///
+/// This is a Prusti-internal representation of the `exists` syntax.
 pub fn exists<T, F>(_trigger_set: T, _closure: F) -> bool {
     true
 }
 
+/// Creates an owned copy of a reference. This should only be used from within
+/// ghost code, as it circumvents the borrow checker.
+pub fn snap<T>(_x: &T) -> T {
+    unimplemented!()
+}
+
+/// Snapshot, "logical", or "mathematical" equality. Compares the in-memory
+/// representation of two instances of the same type, even if there is no
+/// `PartialEq` nor `Copy` implementation. The in-memory representation is
+/// constructed recursively: references are followed, unsafe pointers and cells
+/// are not. Importantly, addresses are not taken into consideration.
+pub fn snapshot_equality<T>(_l: T, _r: T) -> bool {
+    true
+}
+
 pub use private::*;

prusti-specs/src/specifications/preparser.rs

@@ -797,7 +797,7 @@ impl PrustiBinaryOp {
             }
             Self::Or => quote_spanned! { span => #lhs || #rhs },
             Self::And => quote_spanned! { span => #lhs && #rhs },
-            Self::SnapEq => quote_spanned! { span => snapshot_equality(#lhs, #rhs) },
+            Self::SnapEq => quote_spanned! { span => snapshot_equality(&#lhs, &#rhs) },
         }
     }
 }
@@ -894,16 +894,15 @@ mod tests {
         );
         assert_eq!(
             parse_prusti("exists(|x: i32| a === b)".parse().unwrap()).unwrap().to_string(),
-            "exists (() , # [prusti :: spec_only] | x : i32 | -> bool { ((snapshot_equality (a , b)) : bool) })",
+            "exists (() , # [prusti :: spec_only] | x : i32 | -> bool { ((snapshot_equality (& a , & b)) : bool) })",
         );
         assert_eq!(
             parse_prusti("forall(|x: i32| a ==> b, triggers = [(c,), (d, e)])".parse().unwrap()).unwrap().to_string(),
             "forall (((# [prusti :: spec_only] | x : i32 | (c) ,) , (# [prusti :: spec_only] | x : i32 | (d) , # [prusti :: spec_only] | x : i32 | (e) ,) ,) , # [prusti :: spec_only] | x : i32 | -> bool { (((! (a) || (b))) : bool) })",
         );
-        let expr: syn::Expr = syn::parse2("assert!(a === b ==> b)".parse().unwrap()).unwrap();
         assert_eq!(
-            parse_prusti(quote! { #expr }).unwrap().to_string(),
-            "assert ! ((! (snapshot_equality (a , b)) || (b)))",
+            parse_prusti("assert!(a === b ==> b)".parse().unwrap()).unwrap().to_string(),
+            "assert ! ((! (snapshot_equality (& a , & b)) || (b)))",
         );
     }
 

prusti-tests/tests/verify_overflow/fail/generic/snap-eq.rs

@@ -0,0 +1,25 @@
+use prusti_contracts::*;
+
+#[requires(a === b)]
+fn foo<T>(a: T, b: T) {}
+
+struct X { a: i32 }
+
+fn test1() {
+    foo(4, 5); //~ ERROR precondition might not hold
+}
+
+fn test2() {
+    foo(false, true); //~ ERROR precondition might not hold
+}
+
+fn test3() {
+    foo((1, 1), (1, 2)); //~ ERROR precondition might not hold
+}
+
+fn test4() {
+    foo(X { a: 2 }, X { a: 1 }); //~ ERROR precondition might not hold
+}
+
+#[trusted]
+fn main() {}

prusti-tests/tests/verify_overflow/pass/generic/snap-eq.rs

@@ -0,0 +1,13 @@
+use prusti_contracts::*;
+
+#[requires(a === b)]
+fn foo<T>(a: T, b: T) {}
+
+struct X { a: i32 }
+
+fn main() {
+    foo(5, 5);
+    foo(true, true);
+    foo((1, 2), (1, 2));
+    foo(X { a: 1 }, X { a: 1 });
+}

prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs

@@ -566,11 +566,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx>
 
                             // Prusti-specific syntax
                             // TODO: check we are in a spec function
-                            "prusti_contracts::implication"
-                            | "prusti_contracts::exists"
+                            "prusti_contracts::exists"
                             | "prusti_contracts::forall"
                             | "prusti_contracts::specification_entailment"
-                            | "prusti_contracts::call_description" => {
+                            | "prusti_contracts::call_description"
+                            | "prusti_contracts::snap"
+                            | "prusti_contracts::snapshot_equality" => {
                                 let expr = self.encoder.encode_prusti_operation(
                                     full_func_proc_name,
                                     span,

prusti-viper/src/encoder/mir/pure/specifications/interface.rs

@@ -247,6 +247,11 @@ impl<'v, 'tcx: 'v> SpecificationEncoderInterface<'tcx> for crate::encoder::Encod
                 parent_def_id,
                 substs,
             ),
+            "prusti_contracts::snap" => Ok(vir_poly::Expr::snap_app(encoded_args[0].clone())),
+            "prusti_contracts::snapshot_equality" => Ok(vir_poly::Expr::eq_cmp(
+                vir_poly::Expr::snap_app(encoded_args[0].clone()),
+                vir_poly::Expr::snap_app(encoded_args[1].clone()),
+            )),
             _ => unimplemented!(),
         }
     }