Merge pull request #1464 from viperproject/fpoli-patch-3

Fix purification

prusti-common/src/vir/optimizations/methods/purifier.rs

@@ -258,6 +258,13 @@ impl ast::StmtWalker for VarCollector {
         }
         self.is_pure_context = old_pure_context;
     }
+    fn walk_exhale(&mut self, ast::Exhale { expr, .. }: &ast::Exhale) {
+        // When a field is fully exhaled, the purified encoding should havoc the purified variable.
+        // This pass currently does not generate such havoc statement, which is why we mark the
+        // variables used in an exhale as non-purifiable.
+        // See: https://github.com/viperproject/prusti-dev/pull/1464
+        self.walk_expr(expr);
+    }
 }
 
 struct VarPurifier {

prusti-tests/tests/verify/fail/loops/iter_range.rs

@@ -0,0 +1,35 @@
+use prusti_contracts::*;
+
+struct IterRange {
+    from: usize,
+    to: usize,
+}
+
+#[requires(iter.from < iter.to)] // WRONG, should be `<=`
+#[ensures(iter.to == old(iter.to))]
+#[ensures(old(iter.from < iter.to) ==> iter.from == old(iter.from) + 1)]
+#[ensures(old(iter.from < iter.to) == matches!(result, Some(_)))]
+#[ensures(old(iter.from == iter.to) == matches!(result, None))]
+fn next(iter: &mut IterRange) -> Option<usize> {
+    if iter.from < iter.to {
+        let v = iter.from;
+        iter.from = v + 1;
+        Some(v)
+    } else {
+        None
+    }
+}
+
+fn main() {
+    let mut iter = IterRange { from: 0, to: 10 };
+    let mut i = 0;
+    loop {
+        body_invariant!(i == iter.from && iter.from <= iter.to && iter.to == 10);
+        match next(&mut iter) { //~ ERROR: precondition might not hold
+            Some(_) => {}
+            None => break,
+        }
+        i += 1;
+    }
+    assert!(i == 10);
+}

prusti-tests/tests/verify_overflow/pass/loops/iter_range.rs

@@ -0,0 +1,35 @@
+use prusti_contracts::*;
+
+struct IterRange {
+    from: usize,
+    to: usize,
+}
+
+#[requires(iter.from <= iter.to)]
+#[ensures(iter.to == old(iter.to))]
+#[ensures(old(iter.from < iter.to) ==> iter.from == old(iter.from) + 1)]
+#[ensures(old(iter.from < iter.to) == matches!(result, Some(_)))]
+#[ensures(old(iter.from == iter.to) == matches!(result, None))]
+fn next(iter: &mut IterRange) -> Option<usize> {
+    if iter.from < iter.to {
+        let v = iter.from;
+        iter.from = v + 1;
+        Some(v)
+    } else {
+        None
+    }
+}
+
+fn main() {
+    let mut iter = IterRange { from: 0, to: 10 };
+    let mut i = 0;
+    loop {
+        body_invariant!(i == iter.from && iter.from <= iter.to && iter.to == 10);
+        match next(&mut iter) {
+            Some(_) => {}
+            None => break,
+        }
+        i += 1;
+    }
+    assert!(i == 10);
+}