Add support for loop-contract historic values

library/kani_macros/src/sysroot/loop_contracts/mod.rs

@@ -9,7 +9,135 @@ use proc_macro_error2::abort_call_site;
 use quote::{format_ident, quote};
 use syn::spanned::Spanned;
 use syn::token::AndAnd;
-use syn::{BinOp, Expr, ExprBinary, Stmt};
+use syn::{BinOp, Block, Expr, ExprBinary, Ident, Stmt, visit_mut::VisitMut};
+
+struct TransformationResult {
+    transformed_expr: Expr,
+    declarations_block: Block,
+    assignments_block: Block,
+}
+
+struct CallReplacer {
+    old_name: String,
+    replacements: Vec<(Expr, proc_macro2::Ident)>,
+    counter: usize,
+    var_prefix: String,
+}
+
+impl CallReplacer {
+    fn new(old_name: &str, var_prefix: String) -> Self {
+        Self {
+            old_name: old_name.to_string(),
+            replacements: Vec::new(),
+            counter: 0,
+            var_prefix: var_prefix,
+        }
+    }
+
+    fn generate_var_name(&mut self) -> proc_macro2::Ident {
+        let var_name = format_ident!("{}_{}", self.var_prefix, self.counter);
+        self.counter += 1;
+        var_name
+    }
+
+    fn should_replace(&self, expr_path: &syn::ExprPath) -> bool {
+        // Check both simple and qualified paths
+        if let Some(last_segment) = expr_path.path.segments.last() {
+            if last_segment.ident == self.old_name {
+                return true;
+            }
+        }
+
+        let full_path = expr_path
+            .path
+            .segments
+            .iter()
+            .map(|seg| seg.ident.to_string())
+            .collect::<Vec<_>>()
+            .join("::");
+
+        full_path.ends_with(&self.old_name)
+    }
+}
+
+impl VisitMut for CallReplacer {
+    fn visit_expr_mut(&mut self, expr: &mut Expr) {
+        // Visit nested expressions first
+        syn::visit_mut::visit_expr_mut(self, expr);
+
+        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);
+                }
+            }
+        }
+    }
+}
+
+fn transform_function_calls(
+    expr: Expr,
+    function_name: &str,
+    var_prefix: String,
+) -> TransformationResult {
+    let mut replacer = CallReplacer::new(function_name, var_prefix);
+    let mut transformed_expr = expr;
+    replacer.visit_expr_mut(&mut transformed_expr);
+
+    let mut newreplace: Vec<(Expr, Ident)> = Vec::new();
+    for (call, var) in replacer.replacements {
+        match call {
+            Expr::Call(call_expr) => {
+                let insideexpr = call_expr.args[0].clone();
+                newreplace.push((insideexpr, var.clone()));
+            }
+            _ => {}
+        }
+    }
+
+    // Generate declarations block
+    let declarations: Vec<Stmt> =
+        newreplace.iter().map(|(call, var)| syn::parse_quote!(let mut #var = #call.clone();)).collect();
+    let declarations_block: Block = syn::parse_quote!({
+        #(#declarations)*
+    });
+
+    // Generate assignments block
+    let assignments: Vec<Stmt> =
+        newreplace.into_iter().map(|(call, var)| syn::parse_quote!(#var = #call.clone();)).collect();
+    let assignments_block: Block = syn::parse_quote!({
+        #(#assignments)*
+    });
+
+    TransformationResult { transformed_expr, declarations_block, assignments_block }
+}
+
+struct BreakContinueReplacer;
+
+impl VisitMut for BreakContinueReplacer {
+    fn visit_expr_mut(&mut self, expr: &mut Expr) {
+        // Visit nested expressions first
+        syn::visit_mut::visit_expr_mut(self, expr);
+
+        // Replace the expression
+        *expr = match expr {
+            Expr::Break(_) => {
+                syn::parse_quote!(return)
+            }
+            Expr::Continue(_) => {
+                syn::parse_quote!(return)
+            }
+            _ => return,
+        };
+    }
+}
+
+fn transform_break_continue(block: &mut Block) {
+    let mut replacer = BreakContinueReplacer;
+    replacer.visit_block_mut(block);
+}
 
 /// Expand loop contracts macros.
 ///
@@ -41,7 +169,47 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream {
     inv_name.push_str(&loop_id);
 
     // expr of the loop invariant
-    let inv_expr: Expr = syn::parse(attr).unwrap();
+    let mut inv_expr: Expr = syn::parse(attr).unwrap();
+
+    // adding old variables
+    let mut old_var_prefix: String = "__kani_old_var".to_owned();
+    old_var_prefix.push_str(&loop_id);
+    let replace_old: TransformationResult =
+        transform_function_calls(inv_expr.clone(), "old", old_var_prefix);
+    inv_expr = replace_old.transformed_expr.clone();
+    let old_decl_stms = replace_old.declarations_block.stmts.clone();
+
+    // adding prev variables
+    let mut prev_var_prefix: String = "__kani_prev_var".to_owned();
+    prev_var_prefix.push_str(&loop_id);
+    let transform_inv: TransformationResult =
+        transform_function_calls(inv_expr.clone(), "prev", prev_var_prefix);
+    let has_prev = !transform_inv.declarations_block.stmts.is_empty();
+    let decl_stms = transform_inv.declarations_block.stmts.clone();
+    let mut assign_stms = transform_inv.assignments_block.stmts.clone();
+    let (mut loop_body, loop_guard) = match loop_stmt {
+        Stmt::Expr(ref mut e, _) => match e {
+            Expr::While(ew) => (ew.body.clone(), ew.cond.clone()),
+            _ => panic!(),
+        },
+        _ => panic!(),
+    };
+    let loop_body_stms = loop_body.stmts.clone();
+    assign_stms.extend(loop_body_stms);
+    transform_break_continue(&mut loop_body);
+    let mut loop_body_closure_name: String = "__kani_loop_body_closure".to_owned();
+    loop_body_closure_name.push_str(&loop_id);
+    let loop_body_closure = format_ident!("{}", loop_body_closure_name);
+    if has_prev {
+        inv_expr = transform_inv.transformed_expr.clone();
+        match loop_stmt {
+            Stmt::Expr(ref mut e, _) => match e {
+                Expr::While(ew) => ew.body.stmts = assign_stms.clone(),
+                _ => panic!(),
+            },
+            _ => panic!(),
+        };
+    }
 
     // ident of the register function
     let mut register_name: String = "kani_register_loop_contract".to_owned();
@@ -74,8 +242,32 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream {
             note = "for now, loop contracts is only supported for while-loops.";
         ),
     }
-    quote!(
+
+    if has_prev {
+        quote!(
+        {
+        #(#old_decl_stms)*
+        assert!(#loop_guard);
+        #(#decl_stms)*
+        let mut #loop_body_closure = ||
+        #loop_body;
+        #loop_body_closure ();
+        assert!(#inv_expr);
+        // Dummy function used to force the compiler to capture the environment.
+        // We cannot call closures inside constant functions.
+        // This function gets replaced by `kani::internal::call_closure`.
+        #[inline(never)]
+        #[kanitool::fn_marker = "kani_register_loop_contract"]
+        const fn #register_ident<F: Fn() -> bool>(_f: &F, _transformed: usize) -> bool {
+            true
+        }
+        #loop_stmt
+        })
+        .into()
+    } else {
+        quote!(
         {
+        #(#old_decl_stms)*
         // Dummy function used to force the compiler to capture the environment.
         // We cannot call closures inside constant functions.
         // This function gets replaced by `kani::internal::call_closure`.
@@ -84,8 +276,10 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream {
         const fn #register_ident<F: Fn() -> bool>(_f: &F, _transformed: usize) -> bool {
             true
         }
-        #loop_stmt})
-    .into()
+        #loop_stmt
+        })
+        .into()
+    }
 }
 
 fn generate_unique_id_from_span(stmt: &Stmt) -> String {

tests/expected/loop-contract/loop_with_old.expected

@@ -0,0 +1,6 @@
+Check 10: loop_with_old.loop_invariant_base.1
+	 - Status: SUCCESS
+	 - Description: "Check invariant before entry for loop loop_with_old.0"
+	 - Location: src/loop_with_old.rs:16:5 in function loop_with_old
+
+VERIFICATION:- SUCCESSFUL

tests/expected/loop-contract/loop_with_old.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check the use of "old" in loop invariant
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+pub fn loop_with_old() {
+    let mut x: u8 = kani::any_where(|v| *v < 10);
+    let mut y: u8 = kani::any();
+    let mut i = 0;
+    #[kani::loop_invariant( (i<=5) && (x <= old(x) + i) && (old(x) + i == old(i) + x))]
+    while i < 5 {
+        if i == 0 {
+            y = x
+        }
+        x += 1;
+        i += 1;
+    }
+}

tests/expected/loop-contract/loop_with_old_and_prev.expected

@@ -0,0 +1,7 @@
+Check 24: loop_with_old_and_prev.loop_invariant_base.1
+	 - Status: SUCCESS
+	 - Description: "Check invariant before entry for loop loop_with_old_and_prev.0"
+	 - Location: src/loop_with_old_and_prev.rs:14:5 in function loop_with_old_and_prev
+
+
+VERIFICATION:- SUCCESSFUL

tests/expected/loop-contract/loop_with_old_and_prev.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check the use of both "old" and "prev" in loop invariant
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+pub fn loop_with_old_and_prev() {
+    let mut i = 100;
+    #[kani::loop_invariant((i >= 2) && (i <= 100) && (i % 2 == 0) && (old(i) == 100) && (prev(i) == i + 2))]
+    while i > 2 {
+        if i == 1 {
+            break;
+        }
+        i = i - 2;
+    }
+    assert!(i == 2);
+}

tests/expected/loop-contract/loop_with_prev.expected

@@ -0,0 +1,6 @@
+Check 33: loop_with_prev.loop_invariant_step.1
+	 - Status: SUCCESS
+	 - Description: "Check invariant after step for loop loop_with_prev.0"
+	 - Location: src/loop_with_prev.rs:15:5 in function loop_with_prev
+
+VERIFICATION:- SUCCESSFUL

tests/expected/loop-contract/loop_with_prev.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check the use of "prev" in loop invariant
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+pub fn loop_with_prev() {
+    let mut i = 100;
+    let mut j = 100;
+    #[kani::loop_invariant((i >= 2) && (i <= 100) && (i % 2 == 0) && (j == 2*i-100) && (prev(i) == i + 2) && (prev(j) == j + 4) && (prev(i-j) == i-j-2) )]
+    while i > 2 {
+        if i == 1 {
+            break;
+        }
+        i = i - 2;
+        j = j - 4
+    }
+    assert!(i == 2);
+}