From 706e94689f64c1a8e487640cecb9113e55f300c0 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 10 Jun 2025 12:54:27 -0700 Subject: [PATCH 1/2] remove multiple temp variables for prev of same expr --- .../kani_macros/src/sysroot/loop_contracts/mod.rs | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/library/kani_macros/src/sysroot/loop_contracts/mod.rs b/library/kani_macros/src/sysroot/loop_contracts/mod.rs index d1dbfd06aaa8..3938ed5737a1 100644 --- a/library/kani_macros/src/sysroot/loop_contracts/mod.rs +++ b/library/kani_macros/src/sysroot/loop_contracts/mod.rs @@ -136,9 +136,15 @@ impl VisitMut for CallReplacer { if let Expr::Call(call) = expr { if let Expr::Path(expr_path) = &*call.func { if self.should_replace(expr_path) { - let new_var = self.generate_var_name(); - self.replacements.push((expr.clone(), new_var.clone())); - *expr = syn::parse_quote!(#new_var); + let replace_var = + self.replacements.iter().find(|(e, _)| e == expr).map(|(_, v)| v); + if let Some(var) = replace_var { + *expr = syn::parse_quote!(#var); + } else { + let new_var = self.generate_var_name(); + self.replacements.push((expr.clone(), new_var.clone())); + *expr = syn::parse_quote!(#new_var); + }; } } } From 6a80c00bc7e7e5fb1c6ac5dcbc7abbf19cfdef38 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 10 Jun 2025 12:54:49 -0700 Subject: [PATCH 2/2] add expected tests --- .../loop-contract/multiple_prev.expected | 9 +++++++ tests/expected/loop-contract/multiple_prev.rs | 25 +++++++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 tests/expected/loop-contract/multiple_prev.expected create mode 100644 tests/expected/loop-contract/multiple_prev.rs diff --git a/tests/expected/loop-contract/multiple_prev.expected b/tests/expected/loop-contract/multiple_prev.expected new file mode 100644 index 000000000000..ecab1d36ecc9 --- /dev/null +++ b/tests/expected/loop-contract/multiple_prev.expected @@ -0,0 +1,9 @@ +func::{closure#3}::{closure#0}::{closure#1}.assertion.1\ + - Status: SUCCESS\ + - Description: "attempt to add with overflow" + +func.loop_invariant_step.1\ + - Status: SUCCESS\ + - Description: "Check invariant after step for loop func.0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/multiple_prev.rs b/tests/expected/loop-contract/multiple_prev.rs new file mode 100644 index 000000000000..20f12027da11 --- /dev/null +++ b/tests/expected/loop-contract/multiple_prev.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts -Z function-contracts + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +#[kani::requires(x < 10)] +fn func(x: usize) -> Option { + let mut i: usize = 0; + let mut r: usize = x; + let N: usize = 7; + #[kani::loop_invariant((i <= N && i >=0) && (on_entry(i) == 0 && prev(i) < 7 && prev(i) + 1 == i ) ) ] + while i < N { + i = i + 1; + } + if r + i >= x + N { Some(r) } else { None } +} + +#[kani::proof] +fn harness() { + let a = kani::any_where(|x: &usize| *x < 10); + kani::assert(func(a).is_some(), "func(a) is some"); +}