Fix lowering for quantifiers that use closures over function arguments

prusti-tests/tests/verify/fail/native/quantifier_closures.rs

@@ -0,0 +1,20 @@
+// compile-flags: -Pviper_backend=Lithium
+use prusti_contracts::*;
+
+#[requires(forall(|x: i32| x * x >= foo * bar))] //~ ERROR precondition might not hold
+fn test_closure_1(foo: i32, bar: i32) -> i32 {
+    foo + bar + 1
+}
+
+#[requires(forall(|x: i32| x * x >= foo * bar))] //TODO: both errors reported
+fn test_closure_2(foo: i32, bar: i32) -> i32 {
+    foo + bar + 1
+}
+
+fn main() {
+    test_closure_1(5, 3); //TODO: error reported here
+
+    let arg1 = 1;
+    let arg2 = 2;
+    test_closure_2(arg1, arg2); //TODO: error reported here
+}

prusti-tests/tests/verify/pass/native/quantifier_closures.rs

@@ -0,0 +1,15 @@
+// compile-flags: -Pviper_backend=Lithium
+use prusti_contracts::*;
+
+#[requires(forall(|x: i32| x * x >= foo * bar))]
+fn test_closure(foo: i32, bar: i32) -> i32 {
+    foo + bar + 1
+}
+
+fn main() {
+    test_closure(0, 0);
+
+    let arg1 = 0;
+    let arg2 = 0;
+    test_closure(arg1, arg2);
+}

prusti-viper/src/encoder/middle/core_proof/types/interface.rs

@@ -226,6 +226,21 @@ impl<'p, 'v: 'p, 'tcx: 'v> Private for Lowerer<'p, 'v, 'tcx> {
                 self.register_struct_constructor(&domain_name, Vec::new())?;
                 self.encode_validity_axioms_struct(&domain_name, Vec::new(), false.into())?;
             }
+            vir_mid::TypeDecl::Closure(closure) => {
+                // closure has a name and array of arguments, which represent the "saved" parameters of the function
+                // it is not a function, just a struct that remembers the arguments at entry time
+                let mut parameters = Vec::new();
+                for (ix, argument) in closure.arguments.iter().enumerate() {
+                    self.ensure_type_definition(&argument)?;
+                    parameters.push(vir_low::VariableDecl::new(
+                        format!("_{}", ix),
+                        argument.to_snapshot(self)?,
+                    ));
+                }
+
+                self.register_struct_constructor(&domain_name, parameters.clone())?;
+                self.encode_validity_axioms_struct(&domain_name, parameters, true.into())?;
+            }
             _ => unimplemented!("type: {:?}", type_decl),
         };
         Ok(())

vir/defs/high/operations_internal/expression.rs

@@ -354,7 +354,7 @@ impl Expression {
                 // (2) rename with a fresh name the quantified variables that conflict with `dst`.
                 for (src, dst) in self.replacements.iter() {
                     if quantifier.variables.contains(&src.get_base())
-                        || quantifier.variables.contains(&dst.get_base())
+                        || (dst.is_place() && quantifier.variables.contains(&dst.get_base()))
                     {
                         unimplemented!(
                             "replace_multiple_places doesn't handle replacements that conflict \
@@ -429,6 +429,11 @@ impl Expression {
                     base: box Expression::AddrOf(AddrOf { base, .. }),
                     ..
                 }) => *base,
+                Expression::Deref(Deref {
+                    base,
+                    ty: Type::Closure(_),
+                    ..
+                }) => *base,
                 Expression::Field(Field {
                     field,
                     base: box Expression::Constructor(Constructor { arguments, .. }),