From e88e4d890cd5fc0ab8e868b7f9431dc7773c6d41 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 7 Aug 2025 09:56:56 -0700 Subject: [PATCH 1/3] add while let loop transformation --- .../kani_middle/transform/loop_contracts.rs | 2 +- .../src/sysroot/loop_contracts/mod.rs | 38 ++++++++++++++++--- 2 files changed, 33 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index 60dfb761d24e..2299692c2f0a 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -701,7 +701,7 @@ impl LoopContractPass { for stmt in &new_body.blocks()[bb_idx].statements { if let StatementKind::Assign(place, rvalue) = &stmt.kind { match rvalue { - Rvalue::Ref(_,_,rplace) | Rvalue::CopyForDeref(rplace) => { + Rvalue::Ref(_,_,rplace) | Rvalue::CopyForDeref(rplace) | Rvalue::Use(Operand::Copy(rplace)) => { if supported_vars.contains(&rplace.local) { supported_vars.push(place.local); } } diff --git a/library/kani_macros/src/sysroot/loop_contracts/mod.rs b/library/kani_macros/src/sysroot/loop_contracts/mod.rs index 7f8577694a8f..bc9e3a153ae9 100644 --- a/library/kani_macros/src/sysroot/loop_contracts/mod.rs +++ b/library/kani_macros/src/sysroot/loop_contracts/mod.rs @@ -6,12 +6,12 @@ use proc_macro::TokenStream; use proc_macro_error2::abort_call_site; -use quote::{format_ident, quote}; +use quote::{format_ident, quote, quote_spanned}; use syn::punctuated::Punctuated; use syn::spanned::Spanned; use syn::token::AndAnd; use syn::{ - BinOp, Block, Expr, ExprBinary, Ident, Stmt, Token, parse_macro_input, parse_quote, + BinOp, Block, Expr, ExprBinary, ExprWhile, Ident, Stmt, Token, parse_macro_input, parse_quote, visit_mut::VisitMut, }; @@ -232,9 +232,32 @@ fn transform_break_continue(block: &mut Block) { block.stmts.push(return_stmt); } +fn while_let_rewrite(loopexpr: Stmt) -> Stmt { + if let Stmt::Expr(ref expr, _) = loopexpr { + if let Expr::While(ExprWhile { cond, body, .. }) = expr { + if let Expr::Let(ref let_expr) = **cond { + let pat = &let_expr.pat; + let scrutinee = &let_expr.expr; + + // Transform to loop with match + return parse_quote! { + loop { + match #scrutinee { + #pat => #body, + _ => break, + } + }; + }; + } + } + } + return loopexpr.clone(); +} + pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream { // parse the stmt of the loop let mut loop_stmt: Stmt = syn::parse(item.clone()).unwrap(); + loop_stmt = while_let_rewrite(loop_stmt); // name of the loop invariant as closure of the form // __kani_loop_invariant_#startline_#startcol_#endline_#endcol @@ -244,6 +267,7 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream { // expr of the loop invariant let mut inv_expr: Expr = syn::parse(attr).unwrap(); + let original_span = inv_expr.span(); // adding on_entry variables let mut onentry_var_prefix: String = "__kani_onentry_var".to_owned(); @@ -302,7 +326,7 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream { &mut Stmt::Expr(ref mut e, _) => match *e { Expr::While(ref mut ew) => { let new_cond: Expr = syn::parse( - quote!( + quote_spanned!(original_span => #register_ident(&||->bool{#inv_expr}, 0)) .into(), ) @@ -316,7 +340,9 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream { } Expr::Loop(ref mut el) => { //let retexpr = get_return_statement(&el.body); - let invstmt: Stmt = syn::parse(quote!(if !(#register_ident(&||->bool{#inv_expr}, 0)) {assert!(false); unreachable!()};).into()).unwrap(); + let invstmt: Stmt = syn::parse(quote_spanned!(original_span => + if !(#register_ident(&||->bool{#inv_expr}, 0)) {assert!(false); unreachable!()};) + .into()).unwrap(); let mut new_stmts: Vec = Vec::new(); new_stmts.push(invstmt); new_stmts.extend(el.body.stmts.clone()); @@ -334,7 +360,7 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream { } if has_prev { - quote!( + quote_spanned!(original_span => { if (#loop_guard) { #(#onentry_decl_stms)* @@ -363,7 +389,7 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream { }) .into() } else { - quote!( + quote_spanned!(original_span => { #(#onentry_decl_stms)* // Dummy function used to force the compiler to capture the environment. From 2607bd75ba54f05147ea9840dc48d38670ab4457 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 7 Aug 2025 11:36:05 -0700 Subject: [PATCH 2/3] add expected test --- .../while_let_loop_for_slice.expected | 9 +++++++ .../loop-contract/while_let_loop_for_slice.rs | 27 +++++++++++++++++++ 2 files changed, 36 insertions(+) create mode 100644 tests/expected/loop-contract/while_let_loop_for_slice.expected create mode 100644 tests/expected/loop-contract/while_let_loop_for_slice.rs diff --git a/tests/expected/loop-contract/while_let_loop_for_slice.expected b/tests/expected/loop-contract/while_let_loop_for_slice.expected new file mode 100644 index 000000000000..6dba35262648 --- /dev/null +++ b/tests/expected/loop-contract/while_let_loop_for_slice.expected @@ -0,0 +1,9 @@ +trim_ascii_start.loop_invariant_base.1\ + - Status: SUCCESS\ + - Description: "Check invariant before entry for loop trim_ascii_start.0" + +trim_ascii_start.loop_invariant_step.1\ + - Status: SUCCESS\ + - Description: "Check invariant after step for loop trim_ascii_start.0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/while_let_loop_for_slice.rs b/tests/expected/loop-contract/while_let_loop_for_slice.rs new file mode 100644 index 000000000000..8ec615579899 --- /dev/null +++ b/tests/expected/loop-contract/while_let_loop_for_slice.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check if while-let invariant is correctly applied. + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +#[kani::proof] +fn trim_ascii_start() { + let mut a: [u8; 10] = kani::any(); + let s = a.as_slice(); + let mut bytes = s; + #[kani::loop_invariant( + bytes.len() <= s.len() && + (bytes.len() == 0 || (&s[s.len()-bytes.len()..]).as_ptr() == bytes.as_ptr()) + )] + while let [first, rest @ ..] = bytes { + if first.is_ascii_whitespace() { + bytes = rest; + } else { + break; + } + } +} From 9ac94a48b4493491b8144a318c32773de24696e7 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 7 Aug 2025 12:03:44 -0700 Subject: [PATCH 3/3] fix clippy --- .../src/sysroot/loop_contracts/mod.rs | 36 +++++++++---------- 1 file changed, 18 insertions(+), 18 deletions(-) diff --git a/library/kani_macros/src/sysroot/loop_contracts/mod.rs b/library/kani_macros/src/sysroot/loop_contracts/mod.rs index bc9e3a153ae9..3aa53757beed 100644 --- a/library/kani_macros/src/sysroot/loop_contracts/mod.rs +++ b/library/kani_macros/src/sysroot/loop_contracts/mod.rs @@ -233,25 +233,25 @@ fn transform_break_continue(block: &mut Block) { } fn while_let_rewrite(loopexpr: Stmt) -> Stmt { - if let Stmt::Expr(ref expr, _) = loopexpr { - if let Expr::While(ExprWhile { cond, body, .. }) = expr { - if let Expr::Let(ref let_expr) = **cond { - let pat = &let_expr.pat; - let scrutinee = &let_expr.expr; - - // Transform to loop with match - return parse_quote! { - loop { - match #scrutinee { - #pat => #body, - _ => break, - } - }; - }; - } - } + if let Stmt::Expr(ref expr, _) = loopexpr + && let Expr::While(ExprWhile { cond, body, .. }) = expr + && let Expr::Let(ref let_expr) = **cond + { + let pat = &let_expr.pat; + let scrutinee = &let_expr.expr; + + // Transform to loop with match + return parse_quote! { + loop { + match #scrutinee { + #pat => #body, + _ => break, + } + }; + }; } - return loopexpr.clone(); + + loopexpr.clone() } pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream {