Merge #945

945: some fixes and regression tests for #738 related to retaining domain axioms r=vakaras a=Pointerbender

I found a few more cases where the definition collector is a little too strict when removing domain axioms (#738). I included some fixes and regression tests in this PR. A short summary of the changes:

I extended the logic that determines whether to retain the domain axioms to also include cases such as:

* Retain the injectivity axiom when the constructor is "used".
* Also retain the field axiom when the field access snap function is used.

On top of that, I had to change a bit of logic in `prusti-viper/src/encoder/mir/pure/pure_functions/encoder.rs` so that Prusti encoded the type bound preconditions before the other preconditions. Apparently the order in which these are defined matters for Viper (tested by regression test `issue-738-4.rs`).

(This PR does not fully fix the related issue #738)

Co-authored-by: Pointerbender <pointerbender@gmail.com>

prusti-tests/tests/verify_overflow/pass/issues/issue-738-2.rs

@@ -0,0 +1,11 @@
+use prusti_contracts::*;
+
+fn main() {}
+
+#[pure]
+pub fn get(a: &usize) -> usize {
+    *a
+}
+fn foo(a: &usize) {
+    let v = get(a);
+}

prusti-tests/tests/verify_overflow/pass/issues/issue-738-3.rs

@@ -0,0 +1,16 @@
+use prusti_contracts::*;
+
+#[requires(test(1).a == 1)]
+fn main() {}
+
+#[derive(Clone, Copy)]
+pub struct A {
+    a: usize
+}
+
+#[pure]
+#[requires(a <= isize::MAX as usize)]
+#[ensures(result.a <= isize::MAX as usize)]
+pub fn test(a: usize) -> A {
+    A { a: a as isize as usize as isize as usize }
+}

prusti-tests/tests/verify_overflow/pass/issues/issue-738-4.rs

@@ -0,0 +1,28 @@
+use prusti_contracts::*;
+
+fn main() {
+    bar(1, 1);
+    bar(1, 2);
+    baz(1, 1);
+    baz(1, 2);
+}
+
+#[derive(Clone, Copy, PartialEq, Eq)]
+pub struct A {
+    a: usize
+}
+
+#[pure]
+pub fn foo(a: usize) -> A {
+    A { a }
+}
+
+/// Test surjectivity
+#[pure]
+#[requires(a == b ==> foo(a) == foo(b))]
+pub fn bar(a: usize, b: usize) {}
+
+/// Test injectivity
+#[pure]
+#[requires(foo(a) == foo(b) ==> a == b)]
+pub fn baz(a: usize, b: usize) {}

prusti-tests/tests/verify_overflow/pass/issues/issue-738-5.rs

@@ -0,0 +1,11 @@
+use prusti_contracts::*;
+
+fn main() {}
+
+#[pure]
+pub fn get(a: &&&usize) -> usize {
+    ***a
+}
+fn foo(a: &&&usize) {
+    let v = get(a);
+}

prusti-viper/src/encoder/definition_collector.rs

@@ -237,30 +237,38 @@ impl<'p, 'v: 'p, 'tcx: 'v> Collector<'p, 'v, 'tcx> {
                         && !predicate_name.starts_with("Slice$")
                         && !predicate_name.starts_with("Array$")
                     {
-                        // The type is never unfolded, so the snapshot should be
-                        // abstract. An exception is the discriminant function
-                        // because it can be called on a folded type.
+                        // The type is never unfolded, so the snapshot could be
+                        // abstract (not always, see #738). An exception is the discriminant
+                        // function because it can be called on a folded type.
                         // Another exception is when a snap domain function depends
                         // on an axiom, then we should also retain the axiom.
                         let mut used_snap_domain_function_prefixes = vec![];
+                        let mut used_snap_domain_constructor = false;
                         domain.functions.retain(|function| {
                             let function_name = function.get_identifier();
                             let prefix = function_name.split("__").next().map(String::from);
+                            let is_constructor = function_name.starts_with("cons");
                             if self
                                 .used_snap_domain_functions
                                 .contains(&function_name.into())
                             {
                                 used_snap_domain_function_prefixes.extend(prefix);
+                                used_snap_domain_constructor |= is_constructor;
                                 true
                             } else {
                                 false
                             }
                         });
                         domain.axioms.retain(|axiom| {
-                            axiom.name.ends_with("$valid")
-                                && used_snap_domain_function_prefixes
-                                    .iter()
-                                    .any(|prefix| axiom.name.starts_with(prefix))
+                            let used = used_snap_domain_function_prefixes
+                                .iter()
+                                .any(|prefix| axiom.name.starts_with(prefix));
+                            let retain_type_invariant = axiom.name.ends_with("$valid") && used;
+                            let retain_injectivity = used_snap_domain_constructor
+                                && axiom.name.ends_with("$injectivity");
+                            let retain_field_axiom = used_snap_domain_constructor && used;
+
+                            retain_type_invariant || retain_injectivity || retain_field_axiom
                         });
                     }
                 }

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

@@ -231,7 +231,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> {
                 self.mir.return_ty(),
                 self.encoder.env().tcx().param_env(self.proc_def_id)
             ));
-            let return_bounds: Vec<_> = self
+            let mut return_bounds: Vec<_> = self
                 .encoder
                 .encode_type_bounds(
                     &vir::Expr::local(pure_fn_return_variable),
@@ -240,18 +240,20 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionEncoder<'p, 'v, 'tcx> {
                 .into_iter()
                 .map(|p| p.set_default_pos(res_value_range_pos))
                 .collect();
-            postcondition.extend(return_bounds);
+            return_bounds.extend(postcondition);
+            postcondition = return_bounds;
 
             for (formal_arg, local) in formal_args.iter().zip(self.mir.args_iter()) {
                 let typ = self.interpreter.mir_encoder().get_local_ty(local);
                 debug_assert!(self
                     .encoder
                     .env()
                     .type_is_copy(typ, self.encoder.env().tcx().param_env(self.proc_def_id)));
-                let bounds = self
+                let mut bounds = self
                     .encoder
                     .encode_type_bounds(&vir::Expr::local(formal_arg.clone()), typ);
-                precondition.extend(bounds);
+                bounds.extend(precondition);
+                precondition = bounds;
             }
         } else if config::encode_unsigned_num_constraint() {
             if let ty::TyKind::Uint(_) = self.mir.return_ty().kind() {

prusti-viper/src/encoder/mir/types/encoder.rs

@@ -255,6 +255,7 @@ impl<'p, 'v, 'r: 'v, 'tcx: 'v> TypeEncoder<'p, 'v, 'tcx> {
                 Some(bounds)
             }
             ty::TyKind::Char => Some((0.into(), std::char::MAX.into())),
+            ty::TyKind::Ref(_, ty, _) => Self::new(self.encoder, *ty).get_integer_bounds(),
             _ => None,
         }
     }