From cd66caf9eff80e0131235bf06c3a2fb9c77ac480 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Fri, 20 Oct 2023 14:01:36 +0000 Subject: [PATCH 1/4] Add regression tests --- .../tests/verify/fail/loops/iter_range.rs | 35 +++++++++++++++++++ .../verify_overflow/pass/loops/iter_range.rs | 35 +++++++++++++++++++ 2 files changed, 70 insertions(+) create mode 100644 prusti-tests/tests/verify/fail/loops/iter_range.rs create mode 100644 prusti-tests/tests/verify_overflow/pass/loops/iter_range.rs diff --git a/prusti-tests/tests/verify/fail/loops/iter_range.rs b/prusti-tests/tests/verify/fail/loops/iter_range.rs new file mode 100644 index 00000000000..2a550d896fb --- /dev/null +++ b/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 { + 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); +} diff --git a/prusti-tests/tests/verify_overflow/pass/loops/iter_range.rs b/prusti-tests/tests/verify_overflow/pass/loops/iter_range.rs new file mode 100644 index 00000000000..c3dbc0b48b1 --- /dev/null +++ b/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 { + 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); +} From 78d60472c475b23e125490f8adf3eabbf9ba44cb Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Tue, 24 Oct 2023 10:41:19 +0200 Subject: [PATCH 2/4] Fix purification of exhale --- .../src/vir/optimizations/methods/purifier.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/prusti-common/src/vir/optimizations/methods/purifier.rs b/prusti-common/src/vir/optimizations/methods/purifier.rs index f465e7c54bf..07f1dd42756 100644 --- a/prusti-common/src/vir/optimizations/methods/purifier.rs +++ b/prusti-common/src/vir/optimizations/methods/purifier.rs @@ -258,6 +258,19 @@ 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 havoc as non-purifiable. + // See: https://github.com/viperproject/prusti-dev/pull/1464 + self.walk_expr(expr); + } } struct VarPurifier { From f2f3ed252d023f1ed766c0a639d8edbd5ad35fcb Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Tue, 24 Oct 2023 10:57:56 +0200 Subject: [PATCH 3/4] Format code --- prusti-common/src/vir/optimizations/methods/purifier.rs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/prusti-common/src/vir/optimizations/methods/purifier.rs b/prusti-common/src/vir/optimizations/methods/purifier.rs index 07f1dd42756..022d6b52cf4 100644 --- a/prusti-common/src/vir/optimizations/methods/purifier.rs +++ b/prusti-common/src/vir/optimizations/methods/purifier.rs @@ -258,13 +258,7 @@ impl ast::StmtWalker for VarCollector { } self.is_pure_context = old_pure_context; } - fn walk_exhale( - &mut self, - ast::Exhale { - expr, - .. - }: &ast::Exhale, - ) { + 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 havoc as non-purifiable. From 599e078cf4c84e2cda65ca9c624b4c863ad0ace1 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Tue, 24 Oct 2023 11:20:47 +0200 Subject: [PATCH 4/4] Fix comment --- prusti-common/src/vir/optimizations/methods/purifier.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prusti-common/src/vir/optimizations/methods/purifier.rs b/prusti-common/src/vir/optimizations/methods/purifier.rs index 022d6b52cf4..9064bd92524 100644 --- a/prusti-common/src/vir/optimizations/methods/purifier.rs +++ b/prusti-common/src/vir/optimizations/methods/purifier.rs @@ -261,7 +261,7 @@ impl ast::StmtWalker for VarCollector { 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 havoc as non-purifiable. + // variables used in an exhale as non-purifiable. // See: https://github.com/viperproject/prusti-dev/pull/1464 self.walk_expr(expr); }