From 41a11f8706d69cbb918c6d5eee1b462594fdcd78 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Thu, 19 Jun 2025 15:36:26 -0700 Subject: [PATCH 1/5] add support for loop assigns --- cprover_bindings/src/goto_program/stmt.rs | 30 ++++++++- cprover_bindings/src/irep/to_irep.rs | 24 +++---- .../codegen/statement.rs | 63 ++++++++++++++++++- .../codegen_cprover_gotoc/context/goto_ctx.rs | 3 + .../codegen_cprover_gotoc/overrides/hooks.rs | 12 +++- library/kani_macros/src/lib.rs | 7 ++- .../src/sysroot/loop_contracts/mod.rs | 25 +++++++- 7 files changed, 144 insertions(+), 20 deletions(-) diff --git a/cprover_bindings/src/goto_program/stmt.rs b/cprover_bindings/src/goto_program/stmt.rs index 79afb9a7b70e..957cf61a5dd5 100644 --- a/cprover_bindings/src/goto_program/stmt.rs +++ b/cprover_bindings/src/goto_program/stmt.rs @@ -87,6 +87,7 @@ pub enum StmtBody { // The loop invariants annotated to the goto, which can be // applied as loop contracts in CBMC if it is a backward goto. loop_invariants: Option, + loop_assigns: Option>, }, /// `if (i) { t } else { e }` Ifthenelse { @@ -288,7 +289,7 @@ impl Stmt { pub fn goto>(dest: T, loc: Location) -> Self { let dest = dest.into(); assert!(!dest.is_empty()); - stmt!(Goto { dest, loop_invariants: None }, loc) + stmt!(Goto { dest, loop_invariants: None, loop_assigns: None }, loc) } /// `if (i) { t } else { e }` or `if (i) { t }` @@ -333,13 +334,36 @@ impl Stmt { /// `goto dest;` with loop invariant pub fn with_loop_contracts(self, inv: Expr) -> Self { - if let Goto { dest, loop_invariants } = self.body() { + if let Goto { dest, loop_invariants, loop_assigns } = self.body() { assert!(loop_invariants.is_none()); - stmt!(Goto { dest: *dest, loop_invariants: Some(inv) }, *self.location()) + stmt!( + Goto { + dest: *dest, + loop_invariants: Some(inv), + loop_assigns: loop_assigns.clone() + }, + *self.location() + ) } else { unreachable!("Loop contracts should be annotated only to goto stmt") } } + + pub fn with_loop_assigns(self, asg: Vec) -> Self { + if let Goto { dest, loop_invariants, loop_assigns } = self.body() { + assert!(loop_assigns.is_none()); + stmt!( + Goto { + dest: *dest, + loop_invariants: loop_invariants.clone(), + loop_assigns: Some(asg) + }, + *self.location() + ) + } else { + unreachable!("Loop assigns should be annotated only to goto stmt") + } + } } /// Predicates diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 7b5ea07f0b00..013206960892 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -548,17 +548,19 @@ impl ToIrep for StmtBody { arguments_irep(arguments.iter(), mm), ], ), - StmtBody::Goto { dest, loop_invariants } => { - let stmt_goto = code_irep(IrepId::Goto, vec![]) - .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string())); - if let Some(inv) = loop_invariants { - stmt_goto.with_named_sub( - IrepId::CSpecLoopInvariant, - inv.clone().and(Expr::bool_true()).to_irep(mm), - ) - } else { - stmt_goto - } + StmtBody::Goto { dest, loop_invariants, loop_assigns } => { + let inv = loop_invariants + .clone() + .map(|inv| inv.clone().and(Expr::bool_true()).to_irep(mm)); + let assigns = loop_assigns.clone().map(|assigns| { + Irep::just_sub(vec![Irep::just_sub( + assigns.iter().map(|assign| assign.to_irep(mm)).collect(), + )]) + }); + code_irep(IrepId::Goto, vec![]) + .with_named_sub(IrepId::Destination, Irep::just_string_id(dest.to_string())) + .with_named_sub_option(IrepId::CSpecLoopInvariant, inv) + .with_named_sub_option(IrepId::CSpecAssigns, assigns.clone()) } StmtBody::Ifthenelse { i, t, e } => code_irep( IrepId::Ifthenelse, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index acb78850c4fa..2632deb5a68a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -6,6 +6,7 @@ use super::{PropertyClass, bb_label}; use crate::codegen_cprover_gotoc::codegen::function::rustc_smir::region_from_coverage_opaque; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; +use cbmc::goto_program::ExprValue; use cbmc::goto_program::{Expr, Location, Stmt, Type}; use rustc_abi::Size; use rustc_abi::{FieldsShape, Primitive, TagEncoding, Variants}; @@ -17,12 +18,66 @@ use stable_mir::abi::{ArgAbi, FnAbi, PassMode}; use stable_mir::mir::mono::{Instance, InstanceKind}; use stable_mir::mir::{ AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place, - RETURN_LOCAL, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, + RETURN_LOCAL, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, }; use stable_mir::ty::{Abi, RigidTy, Span, Ty, TyKind, VariantIdx}; use tracing::{debug, debug_span, trace}; impl GotocCtx<'_> { + pub fn ty_to_assign_target(&self, ty: Ty, expr: &Expr) -> Expr { + match ty.kind() { + TyKind::RigidTy(RigidTy::Ref(_, unref_ty, _)) + | TyKind::RigidTy(RigidTy::RawPtr(unref_ty, _)) => match unref_ty.kind() { + TyKind::RigidTy(RigidTy::Slice(slice_ty)) => { + let size = slice_ty.layout().unwrap().shape().size.bytes(); + Expr::symbol_expression( + "__CPROVER_object_upto", + Type::code( + vec![ + Type::empty().to_pointer().as_parameter(None, Some("ptr".into())), + Type::size_t().as_parameter(None, Some("size".into())), + ], + Type::empty(), + ), + ) + .call(vec![ + expr.clone() + .member("data", &self.symbol_table) + .cast_to(Type::empty().to_pointer()), + expr.clone() + .member("len", &self.symbol_table) + .mul(Expr::size_constant(size.try_into().unwrap(), &self.symbol_table)), + ]) + } + _ => expr.clone().dereference(), + }, + _ => expr.clone().dereference(), + } + } + + pub fn rvalue_to_assign_targets(&mut self, rvalue: &Rvalue, location: Location) -> Vec { + let assigns = self.codegen_rvalue_stable(rvalue, location); + let assigns_value = assigns.value().clone(); + let assign_exprs = if let ExprValue::Struct { values } = assigns_value { + values.clone() + } else { + vec![assigns.clone()] + }; + match rvalue { + Rvalue::Aggregate(_agg_kind, operands) => { + let mut ptr_exprs = Vec::new(); + for (operand, expr) in operands.iter().zip(assign_exprs.iter()) { + let operand_ty = self.operand_ty_stable(operand); + debug!("Ty {:?}", operand_ty); + let ptr_expr = self.ty_to_assign_target(operand_ty, expr); + ptr_exprs.push(ptr_expr) + } + ptr_exprs + } + _ => vec![assigns.dereference()], + } + } + /// Generate Goto-C for MIR [Statement]s. /// This does not cover all possible "statements" because MIR distinguishes between ordinary /// statements and [Terminator]s, which can exclusively appear at the end of a basic block. @@ -36,6 +91,12 @@ impl GotocCtx<'_> { StatementKind::Assign(lhs, rhs) => { let lty = self.place_ty_stable(lhs); let rty = self.rvalue_ty_stable(rhs); + let localname = self.codegen_var_name(&lhs.local); + if localname.contains("kani_loop_assigns") { + let assigns = self.rvalue_to_assign_targets(rhs, location); + self.current_loop_assigns = assigns.clone(); + return Stmt::skip(location); + } // we ignore assignment for all zero size types if self.is_zst_stable(lty) { Stmt::skip(location) diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index e3073f87ba6b..9d5f0b64c152 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -78,6 +78,8 @@ pub struct GotocCtx<'tcx> { pub transformer: BodyTransformation, /// If there exist some usage of loop contracts int context. pub has_loop_contracts: bool, + /// Track loop assign clause + pub current_loop_assigns: Vec, } /// Constructor @@ -108,6 +110,7 @@ impl<'tcx> GotocCtx<'tcx> { concurrent_constructs: FxHashMap::default(), transformer, has_loop_contracts: false, + current_loop_assigns: Vec::new(), } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 6c6319baf4eb..72c4d38dd10a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -728,6 +728,14 @@ impl GotocHook for LoopInvariantRegister { // free(0) // goto target --- with loop contracts annotated. + let mut stmt = Stmt::goto(bb_label(target.unwrap()), loc) + .with_loop_contracts(func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool))); + let assigns = gcx.current_loop_assigns.clone(); + if !assigns.is_empty() { + stmt = stmt.with_loop_assigns(assigns.clone()); + gcx.current_loop_assigns.clear(); + } + // Add `free(0)` to make sure the body of `free` won't be dropped to // satisfy the requirement of DFCC. Stmt::block( @@ -735,9 +743,7 @@ impl GotocHook for LoopInvariantRegister { BuiltinFn::Free .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc) .as_stmt(loc), - Stmt::goto(bb_label(target.unwrap()), loc).with_loop_contracts( - func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool)), - ), + stmt, ], loc, ) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 7693eb2c38f9..c8e864aad61e 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -440,6 +440,10 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::loop_invariant(attr, item) } +#[proc_macro_attribute] +pub fn loop_assigns(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::loop_assigns(attr, item) +} /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. #[cfg(kani_sysroot)] @@ -450,7 +454,7 @@ mod sysroot { mod loop_contracts; pub use contracts::{ensures, modifies, proof_for_contract, requires, stub_verified}; - pub use loop_contracts::loop_invariant; + pub use loop_contracts::{loop_assigns, loop_invariant}; use super::*; @@ -629,4 +633,5 @@ mod regular { no_op!(proof_for_contract); no_op!(stub_verified); no_op!(loop_invariant); + no_op!(loop_assigns); } diff --git a/library/kani_macros/src/sysroot/loop_contracts/mod.rs b/library/kani_macros/src/sysroot/loop_contracts/mod.rs index 3938ed5737a1..8bf28c649a8a 100644 --- a/library/kani_macros/src/sysroot/loop_contracts/mod.rs +++ b/library/kani_macros/src/sysroot/loop_contracts/mod.rs @@ -7,9 +7,13 @@ use proc_macro::TokenStream; use proc_macro_error2::abort_call_site; use quote::{format_ident, quote}; +use syn::punctuated::Punctuated; use syn::spanned::Spanned; use syn::token::AndAnd; -use syn::{BinOp, Block, Expr, ExprBinary, Ident, Stmt, parse_quote, visit_mut::VisitMut}; +use syn::{ + BinOp, Block, Expr, ExprBinary, Ident, Stmt, Token, parse_macro_input, parse_quote, + visit_mut::VisitMut, +}; /* Transform the loop to support on_entry(expr) : the value of expr before entering the loop @@ -389,3 +393,22 @@ fn generate_unique_id_from_span(stmt: &Stmt) -> String { // Create a tuple of location information (file path, start line, start column, end line, end column) format!("_{:?}_{:?}_{:?}_{:?}", start.line(), start.column(), end.line(), end.column()) } + +pub fn loop_assigns(attr: TokenStream, item: TokenStream) -> TokenStream { + let assigns = parse_macro_input!(attr with Punctuated::::parse_terminated) + .into_iter() + .collect::>(); + let loop_assign_name: String = "kani_loop_assigns".to_owned(); + let loop_assign_ident = format_ident!("{}", loop_assign_name); + let loop_assign_stmt: Stmt = parse_quote! { + let #loop_assign_ident = (#(#assigns),*); + }; + let loop_stmt: Stmt = syn::parse(item.clone()).unwrap(); + let ret: TokenStream = quote!( + { + #loop_assign_stmt + #loop_stmt + }) + .into(); + ret +} From ec0e5bb29c3fc8f09ab243bfc085ac2613695249 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 23 Jun 2025 08:39:54 -0700 Subject: [PATCH 2/5] add expected tests --- .../loop_assigns_for_fat_ptr.expected | 13 ++++++++ .../loop-contract/loop_assigns_for_fat_ptr.rs | 23 ++++++++++++++ .../loop_assigns_for_fat_ptr_fail.expected | 7 +++++ .../loop_assigns_for_fat_ptr_fail.rs | 23 ++++++++++++++ .../loop_assigns_for_ptr.expected | 13 ++++++++ .../loop-contract/loop_assigns_for_ptr.rs | 21 +++++++++++++ .../loop_assigns_for_ptr_fail.expected | 11 +++++++ .../loop_assigns_for_ptr_fail.rs | 21 +++++++++++++ .../loop_assigns_for_ref.expected | 9 ++++++ .../loop-contract/loop_assigns_for_ref.rs | 21 +++++++++++++ .../loop_assigns_for_ref_fail.expected | 7 +++++ .../loop_assigns_for_ref_fail.rs | 23 ++++++++++++++ .../loop_assigns_for_vec.expected | 13 ++++++++ .../loop-contract/loop_assigns_for_vec.rs | 30 +++++++++++++++++++ 14 files changed, 235 insertions(+) create mode 100644 tests/expected/loop-contract/loop_assigns_for_fat_ptr.expected create mode 100644 tests/expected/loop-contract/loop_assigns_for_fat_ptr.rs create mode 100644 tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.expected create mode 100644 tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.rs create mode 100644 tests/expected/loop-contract/loop_assigns_for_ptr.expected create mode 100644 tests/expected/loop-contract/loop_assigns_for_ptr.rs create mode 100644 tests/expected/loop-contract/loop_assigns_for_ptr_fail.expected create mode 100644 tests/expected/loop-contract/loop_assigns_for_ptr_fail.rs create mode 100644 tests/expected/loop-contract/loop_assigns_for_ref.expected create mode 100644 tests/expected/loop-contract/loop_assigns_for_ref.rs create mode 100644 tests/expected/loop-contract/loop_assigns_for_ref_fail.expected create mode 100644 tests/expected/loop-contract/loop_assigns_for_ref_fail.rs create mode 100644 tests/expected/loop-contract/loop_assigns_for_vec.expected create mode 100644 tests/expected/loop-contract/loop_assigns_for_vec.rs diff --git a/tests/expected/loop-contract/loop_assigns_for_fat_ptr.expected b/tests/expected/loop-contract/loop_assigns_for_fat_ptr.expected new file mode 100644 index 000000000000..62271ee7a2a1 --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_fat_ptr.expected @@ -0,0 +1,13 @@ +main.assigns.1\ + - Status: SUCCESS\ + - Description: "Check that a[var_15] is assignable" + +main.assigns.2\ + - Status: SUCCESS\ + - Description: "Check that i is assignable" + +main.loop_invariant_step.1\ + - Status: SUCCESS\ + - Description: "Check invariant after step for loop main.0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/loop_assigns_for_fat_ptr.rs b/tests/expected/loop-contract/loop_assigns_for_fat_ptr.rs new file mode 100644 index 000000000000..6c9701d996ee --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_fat_ptr.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check the use of loop_assigns for Rust's Fat ptr + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +use std::ptr::slice_from_raw_parts; + +#[kani::proof] +fn main() { + let mut i = 0; + let mut a: [u8; 100] = kani::any(); + #[kani::loop_invariant(i <= 20)] + #[kani::loop_assigns(&i , slice_from_raw_parts(a.as_ptr(), 20))] + while i < 20 { + a[i] = 1; + i = i + 1; + } +} diff --git a/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.expected b/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.expected new file mode 100644 index 000000000000..ba0926539392 --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.expected @@ -0,0 +1,7 @@ +main.assigns.1\ + - Status: FAILURE\ + - Description: "Check that a[var_15] is assignable" + +Failed Checks: Check that a[var_15] is assignable + +VERIFICATION:- FAILED diff --git a/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.rs b/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.rs new file mode 100644 index 000000000000..479ceabea811 --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check the use of loop_assigns for Rust's Fat ptr + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +use std::ptr::slice_from_raw_parts; + +#[kani::proof] +fn main() { + let mut i = 0; + let mut a: [u8; 100] = kani::any(); + #[kani::loop_invariant(i <= 20)] + #[kani::loop_assigns(&i , slice_from_raw_parts(a.as_ptr(), 18))] + while i < 20 { + a[i] = 1; + i = i + 1; + } +} diff --git a/tests/expected/loop-contract/loop_assigns_for_ptr.expected b/tests/expected/loop-contract/loop_assigns_for_ptr.expected new file mode 100644 index 000000000000..c8d51a4544ca --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_ptr.expected @@ -0,0 +1,13 @@ +main.assigns.1\ + - Status: SUCCESS\ + - Description: "Check that a[var_14] is assignable" + +main.assigns.2\ + - Status: SUCCESS\ + - Description: "Check that i is assignable" + +main.loop_invariant_step.1\ + - Status: SUCCESS\ + - Description: "Check invariant after step for loop main.0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/loop_assigns_for_ptr.rs b/tests/expected/loop-contract/loop_assigns_for_ptr.rs new file mode 100644 index 000000000000..d14dd83d64b7 --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_ptr.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check the use of loop_assigns for Rust's ptr + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +#[kani::proof] +fn main() { + let mut i = 0; + let mut a: [u8; 20] = kani::any(); + #[kani::loop_invariant(i <= 20)] + #[kani::loop_assigns(&i as *const _, a.as_slice())] + while i < 20 { + a[i] = 1; + i = i + 1; + } +} diff --git a/tests/expected/loop-contract/loop_assigns_for_ptr_fail.expected b/tests/expected/loop-contract/loop_assigns_for_ptr_fail.expected new file mode 100644 index 000000000000..882d7607e992 --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_ptr_fail.expected @@ -0,0 +1,11 @@ +main.assigns.1\ + - Status: FAILURE\ + - Description: "Check that a[var_15] is assignable" + +main.loop_invariant_base.1\ + - Status: SUCCESS\ + - Description: "Check invariant before entry for loop main.0" + +Failed Checks: Check that a[var_15] is assignable + +VERIFICATION:- FAILED diff --git a/tests/expected/loop-contract/loop_assigns_for_ptr_fail.rs b/tests/expected/loop-contract/loop_assigns_for_ptr_fail.rs new file mode 100644 index 000000000000..5d28ed1a313d --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_ptr_fail.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check a fail case for loop_assigns for Rust's ptr. a is not a fat ptr. + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +#[kani::proof] +fn main() { + let mut i = 0; + let mut a: [u8; 20] = kani::any(); + #[kani::loop_invariant(i <= 20)] + #[kani::loop_assigns(&i as *const _, a.as_ptr())] + while i < 20 { + a[i] = 1; + i = i + 1; + } +} diff --git a/tests/expected/loop-contract/loop_assigns_for_ref.expected b/tests/expected/loop-contract/loop_assigns_for_ref.expected new file mode 100644 index 000000000000..59db3e04b3d8 --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_ref.expected @@ -0,0 +1,9 @@ +main.assigns.1\ + - Status: SUCCESS\ + - Description: "Check that a[var_12] is assignable" + +main.loop_invariant_step.1\ + - Status: SUCCESS\ + - Description: "Check invariant after step for loop main.0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/loop_assigns_for_ref.rs b/tests/expected/loop-contract/loop_assigns_for_ref.rs new file mode 100644 index 000000000000..d2faf20dc359 --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_ref.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check the use of loop_assigns for Rust's ref + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +#[kani::proof] +fn main() { + let mut i = 0; + let mut a: [u8; 20] = kani::any(); + #[kani::loop_invariant(i <= 20)] + #[kani::loop_assigns(&i, &a)] + while i < 20 { + a[i] = 1; + i = i + 1; + } +} diff --git a/tests/expected/loop-contract/loop_assigns_for_ref_fail.expected b/tests/expected/loop-contract/loop_assigns_for_ref_fail.expected new file mode 100644 index 000000000000..7c805eac7ea1 --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_ref_fail.expected @@ -0,0 +1,7 @@ +main.assigns.3\ + - Status: FAILURE\ + - Description: "Check that j is assignable" + +Failed Checks: Check that j is assignable + +VERIFICATION:- FAILED diff --git a/tests/expected/loop-contract/loop_assigns_for_ref_fail.rs b/tests/expected/loop-contract/loop_assigns_for_ref_fail.rs new file mode 100644 index 000000000000..6f11e99fedbb --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_ref_fail.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check the use of loop_assigns for Rust's ref + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +#[kani::proof] +fn main() { + let mut i = 0; + let mut j = 0; + let mut a: [u8; 20] = kani::any(); + #[kani::loop_invariant(i <= 20 && i == j)] + #[kani::loop_assigns(&i, &a)] + while i < 20 { + a[i] = 1; + i = i + 1; + j = j + 1; + } +} diff --git a/tests/expected/loop-contract/loop_assigns_for_vec.expected b/tests/expected/loop-contract/loop_assigns_for_vec.expected new file mode 100644 index 000000000000..b1d5d1c9d85e --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_vec.expected @@ -0,0 +1,13 @@ +main.assigns.1\ + - Status: SUCCESS\ + - Description: "Check that i is assignable" + +std::ptr::write::.assigns.1\ + - Status: SUCCESS\ + - Description: "Check that *dst is assignable" + +std::vec::Vec::::set_len.assigns.1\ + - Status: SUCCESS\ + - Description: "Check that self->len is assignable" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/loop_assigns_for_vec.rs b/tests/expected/loop-contract/loop_assigns_for_vec.rs new file mode 100644 index 000000000000..c1b49a742994 --- /dev/null +++ b/tests/expected/loop-contract/loop_assigns_for_vec.rs @@ -0,0 +1,30 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check the use of loop_assigns for Rust's vec + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +use std::ptr; +use std::ptr::slice_from_raw_parts; + +#[kani::proof] +fn main() { + let mut i = 0; + let a: [u8; 3] = kani::any(); + let mut v: Vec = Vec::with_capacity(12); + v.extend(a); + //unsafe {(&v as *const Vec as *const usize).add(2)} is the ptr to v.len + #[kani::loop_invariant(i <= 3)] + #[kani::loop_assigns(&i, slice_from_raw_parts(v.as_ptr(), 12), unsafe {(&v as *const Vec as *const usize).add(2)})] + while i < 3 { + unsafe { + ptr::copy_nonoverlapping(v.as_ptr(), (v.as_mut_ptr()).add(i * 3 + 3), 3); + i = i + 1; + v.set_len(i * 3 + 3) + } + } +} From 69f67d7e527c852f3078d0de1b3f0a4127719616 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Wed, 25 Jun 2025 17:06:33 -0700 Subject: [PATCH 3/5] add documentation --- .../reference/experimental/loop-contracts.md | 63 +++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md index 2a07f5c2c1aa..6bfe4b132791 100644 --- a/docs/src/reference/experimental/loop-contracts.md +++ b/docs/src/reference/experimental/loop-contracts.md @@ -164,6 +164,69 @@ fn contract_proof() { When loop contracts and function contracts are both enabled (by flags `-Z loop-contracts -Z function-contracts`), Kani automatically contracts (instead of unwinds) all loops in the functions that we want to prove contracts for. + +## Loop assigns clauses: +We allow users to manually specified the `loop_assigns` clauses for memory allocated addresses which can be assigned inside the loop body. +The concept is very similar to the `__CPROVER_assigns` clause of CBMC (https://diffblue.github.io/cbmc/contracts-assigns.html). +However, in Kani, the CBMC target is replaced by three Rust types which can be used in the `loop_assigns` clauses: +1. `RawPtr`: We don't allow variable names as targets. Users must use pointers to them instead, which also allows checking assigns using borrowed references and aliases. +```Rust +#[kani::proof] +fn main() { + let mut i = 0; + #[kani::loop_invariant(i <= 20)] + #[kani::loop_assigns(&i as *const _)] + while i < 20 { + i = i + 1; + } +} +``` +2. `Reference`: Similar to RawPtr, but we also can use it to replace `__CPROVER_object_whole(ptr-expr)`, +Example +```Rust +#[kani::proof] +fn main() { + let mut i = 0; + let mut a: [u8; 20] = kani::any(); + #[kani::loop_invariant(i <= 20)] + #[kani::loop_assigns(&i, &a)] + while i < 20 { + a[i] = 1; + i = i + 1; + } +} +``` +3. `FatPtr (Slice)`: We use this to replace `__CPROVER_object_from(ptr-expr)`, and `__CPROVER_object_upto(ptr-expr, uint-expr)`. +```Rust +#[kani::proof] +fn main() { + let mut i = 3; + let mut a: [u8; 100] = kani::any(); + #[kani::loop_invariant(i >=3 && i <= 20)] + #[kani::loop_assigns(&i , &a[3..20])] + while i < 20 { + a[i] = 1; + i = i + 1; + } +} +``` +or + +```Rust +use std::ptr::slice_from_raw_parts; +#[kani::proof] +fn main() { + let mut i = 0; + let mut a: [u8; 100] = kani::any(); + #[kani::loop_invariant(i <= 20)] + #[kani::loop_assigns(&i , slice_from_raw_parts(a.as_ptr(), 20))] + while i < 20 { + a[i] = 1; + i = i + 1; + } +} +``` + ## Limitations Loop contracts comes with the following limitations. From 5e2f4d48b057e9febdd3cf1e4810c2a53da4437e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Fri, 27 Jun 2025 09:14:03 -0700 Subject: [PATCH 4/5] change from loop_assigns to loop_modifies --- cprover_bindings/src/goto_program/stmt.rs | 16 ++++++++-------- cprover_bindings/src/irep/to_irep.rs | 4 ++-- .../reference/experimental/loop-contracts.md | 18 +++++++++--------- .../codegen_cprover_gotoc/codegen/statement.rs | 4 ++-- .../codegen_cprover_gotoc/context/goto_ctx.rs | 4 ++-- .../codegen_cprover_gotoc/overrides/hooks.rs | 6 +++--- library/kani_macros/src/lib.rs | 8 ++++---- .../src/sysroot/loop_contracts/mod.rs | 4 ++-- .../loop-contract/loop_assigns_for_fat_ptr.rs | 4 ++-- .../loop_assigns_for_fat_ptr_fail.rs | 4 ++-- .../loop-contract/loop_assigns_for_ptr.rs | 4 ++-- .../loop-contract/loop_assigns_for_ptr_fail.rs | 4 ++-- .../loop-contract/loop_assigns_for_ref.rs | 4 ++-- .../loop-contract/loop_assigns_for_ref_fail.rs | 4 ++-- .../loop-contract/loop_assigns_for_vec.rs | 4 ++-- 15 files changed, 46 insertions(+), 46 deletions(-) diff --git a/cprover_bindings/src/goto_program/stmt.rs b/cprover_bindings/src/goto_program/stmt.rs index 957cf61a5dd5..972088fe822f 100644 --- a/cprover_bindings/src/goto_program/stmt.rs +++ b/cprover_bindings/src/goto_program/stmt.rs @@ -87,7 +87,7 @@ pub enum StmtBody { // The loop invariants annotated to the goto, which can be // applied as loop contracts in CBMC if it is a backward goto. loop_invariants: Option, - loop_assigns: Option>, + loop_modifies: Option>, }, /// `if (i) { t } else { e }` Ifthenelse { @@ -289,7 +289,7 @@ impl Stmt { pub fn goto>(dest: T, loc: Location) -> Self { let dest = dest.into(); assert!(!dest.is_empty()); - stmt!(Goto { dest, loop_invariants: None, loop_assigns: None }, loc) + stmt!(Goto { dest, loop_invariants: None, loop_modifies: None }, loc) } /// `if (i) { t } else { e }` or `if (i) { t }` @@ -334,13 +334,13 @@ impl Stmt { /// `goto dest;` with loop invariant pub fn with_loop_contracts(self, inv: Expr) -> Self { - if let Goto { dest, loop_invariants, loop_assigns } = self.body() { + if let Goto { dest, loop_invariants, loop_modifies } = self.body() { assert!(loop_invariants.is_none()); stmt!( Goto { dest: *dest, loop_invariants: Some(inv), - loop_assigns: loop_assigns.clone() + loop_modifies: loop_modifies.clone() }, *self.location() ) @@ -349,14 +349,14 @@ impl Stmt { } } - pub fn with_loop_assigns(self, asg: Vec) -> Self { - if let Goto { dest, loop_invariants, loop_assigns } = self.body() { - assert!(loop_assigns.is_none()); + pub fn with_loop_modifies(self, asg: Vec) -> Self { + if let Goto { dest, loop_invariants, loop_modifies } = self.body() { + assert!(loop_modifies.is_none()); stmt!( Goto { dest: *dest, loop_invariants: loop_invariants.clone(), - loop_assigns: Some(asg) + loop_modifies: Some(asg) }, *self.location() ) diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 013206960892..67f1dce45add 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -548,11 +548,11 @@ impl ToIrep for StmtBody { arguments_irep(arguments.iter(), mm), ], ), - StmtBody::Goto { dest, loop_invariants, loop_assigns } => { + StmtBody::Goto { dest, loop_invariants, loop_modifies } => { let inv = loop_invariants .clone() .map(|inv| inv.clone().and(Expr::bool_true()).to_irep(mm)); - let assigns = loop_assigns.clone().map(|assigns| { + let assigns = loop_modifies.clone().map(|assigns| { Irep::just_sub(vec![Irep::just_sub( assigns.iter().map(|assign| assign.to_irep(mm)).collect(), )]) diff --git a/docs/src/reference/experimental/loop-contracts.md b/docs/src/reference/experimental/loop-contracts.md index 6bfe4b132791..df183cc22b9e 100644 --- a/docs/src/reference/experimental/loop-contracts.md +++ b/docs/src/reference/experimental/loop-contracts.md @@ -61,7 +61,7 @@ Check 10: simple_loop_with_loop_contracts.loop_invariant_base.1 - Description: "Check invariant before entry for loop simple_loop_with_loop_contracts.0" - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts -Check 11: simple_loop_with_loop_contracts.loop_assigns.1 +Check 11: simple_loop_with_loop_contracts.loop_modifies.1 - Status: SUCCESS - Description: "Check assigns clause inclusion for loop simple_loop_with_loop_contracts.0" - Location: simple_while_loop.rs:15:5 in function simple_loop_with_loop_contracts @@ -165,17 +165,17 @@ fn contract_proof() { When loop contracts and function contracts are both enabled (by flags `-Z loop-contracts -Z function-contracts`), Kani automatically contracts (instead of unwinds) all loops in the functions that we want to prove contracts for. -## Loop assigns clauses: -We allow users to manually specified the `loop_assigns` clauses for memory allocated addresses which can be assigned inside the loop body. +## Loop modifies clauses: +We allow users to manually specified the `loop_modifies` clauses for memory allocated addresses which can be modified inside the loop body. The concept is very similar to the `__CPROVER_assigns` clause of CBMC (https://diffblue.github.io/cbmc/contracts-assigns.html). -However, in Kani, the CBMC target is replaced by three Rust types which can be used in the `loop_assigns` clauses: -1. `RawPtr`: We don't allow variable names as targets. Users must use pointers to them instead, which also allows checking assigns using borrowed references and aliases. +However, in Kani, the CBMC target is replaced by three Rust types which can be used in the `loop_modifies` clauses: +1. `RawPtr`: We don't allow variable names as targets. Users must use pointers to them instead, which also allows checking modification using borrowed references and aliases. ```Rust #[kani::proof] fn main() { let mut i = 0; #[kani::loop_invariant(i <= 20)] - #[kani::loop_assigns(&i as *const _)] + #[kani::loop_modifies(&i as *const _)] while i < 20 { i = i + 1; } @@ -189,7 +189,7 @@ fn main() { let mut i = 0; let mut a: [u8; 20] = kani::any(); #[kani::loop_invariant(i <= 20)] - #[kani::loop_assigns(&i, &a)] + #[kani::loop_modifies(&i, &a)] while i < 20 { a[i] = 1; i = i + 1; @@ -203,7 +203,7 @@ fn main() { let mut i = 3; let mut a: [u8; 100] = kani::any(); #[kani::loop_invariant(i >=3 && i <= 20)] - #[kani::loop_assigns(&i , &a[3..20])] + #[kani::loop_modifies(&i , &a[3..20])] while i < 20 { a[i] = 1; i = i + 1; @@ -219,7 +219,7 @@ fn main() { let mut i = 0; let mut a: [u8; 100] = kani::any(); #[kani::loop_invariant(i <= 20)] - #[kani::loop_assigns(&i , slice_from_raw_parts(a.as_ptr(), 20))] + #[kani::loop_modifies(&i , slice_from_raw_parts(a.as_ptr(), 20))] while i < 20 { a[i] = 1; i = i + 1; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 2632deb5a68a..5032aaccfb3e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -92,9 +92,9 @@ impl GotocCtx<'_> { let lty = self.place_ty_stable(lhs); let rty = self.rvalue_ty_stable(rhs); let localname = self.codegen_var_name(&lhs.local); - if localname.contains("kani_loop_assigns") { + if localname.contains("kani_loop_modifies") { let assigns = self.rvalue_to_assign_targets(rhs, location); - self.current_loop_assigns = assigns.clone(); + self.current_loop_modifies = assigns.clone(); return Stmt::skip(location); } // we ignore assignment for all zero size types diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 9d5f0b64c152..879dd24870ee 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -79,7 +79,7 @@ pub struct GotocCtx<'tcx> { /// If there exist some usage of loop contracts int context. pub has_loop_contracts: bool, /// Track loop assign clause - pub current_loop_assigns: Vec, + pub current_loop_modifies: Vec, } /// Constructor @@ -110,7 +110,7 @@ impl<'tcx> GotocCtx<'tcx> { concurrent_constructs: FxHashMap::default(), transformer, has_loop_contracts: false, - current_loop_assigns: Vec::new(), + current_loop_modifies: Vec::new(), } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 72c4d38dd10a..51881c71ed5b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -730,10 +730,10 @@ impl GotocHook for LoopInvariantRegister { let mut stmt = Stmt::goto(bb_label(target.unwrap()), loc) .with_loop_contracts(func_exp.call(fargs).cast_to(Type::CInteger(CIntType::Bool))); - let assigns = gcx.current_loop_assigns.clone(); + let assigns = gcx.current_loop_modifies.clone(); if !assigns.is_empty() { - stmt = stmt.with_loop_assigns(assigns.clone()); - gcx.current_loop_assigns.clear(); + stmt = stmt.with_loop_modifies(assigns.clone()); + gcx.current_loop_modifies.clear(); } // Add `free(0)` to make sure the body of `free` won't be dropped to diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index c8e864aad61e..f22e74e9dc8b 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -441,8 +441,8 @@ pub fn loop_invariant(attr: TokenStream, item: TokenStream) -> TokenStream { } #[proc_macro_attribute] -pub fn loop_assigns(attr: TokenStream, item: TokenStream) -> TokenStream { - attr_impl::loop_assigns(attr, item) +pub fn loop_modifies(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::loop_modifies(attr, item) } /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. @@ -454,7 +454,7 @@ mod sysroot { mod loop_contracts; pub use contracts::{ensures, modifies, proof_for_contract, requires, stub_verified}; - pub use loop_contracts::{loop_assigns, loop_invariant}; + pub use loop_contracts::{loop_modifies, loop_invariant}; use super::*; @@ -633,5 +633,5 @@ mod regular { no_op!(proof_for_contract); no_op!(stub_verified); no_op!(loop_invariant); - no_op!(loop_assigns); + no_op!(loop_modifies); } diff --git a/library/kani_macros/src/sysroot/loop_contracts/mod.rs b/library/kani_macros/src/sysroot/loop_contracts/mod.rs index 8bf28c649a8a..fc129c6d92bc 100644 --- a/library/kani_macros/src/sysroot/loop_contracts/mod.rs +++ b/library/kani_macros/src/sysroot/loop_contracts/mod.rs @@ -394,11 +394,11 @@ fn generate_unique_id_from_span(stmt: &Stmt) -> String { format!("_{:?}_{:?}_{:?}_{:?}", start.line(), start.column(), end.line(), end.column()) } -pub fn loop_assigns(attr: TokenStream, item: TokenStream) -> TokenStream { +pub fn loop_modifies(attr: TokenStream, item: TokenStream) -> TokenStream { let assigns = parse_macro_input!(attr with Punctuated::::parse_terminated) .into_iter() .collect::>(); - let loop_assign_name: String = "kani_loop_assigns".to_owned(); + let loop_assign_name: String = "kani_loop_modifies".to_owned(); let loop_assign_ident = format_ident!("{}", loop_assign_name); let loop_assign_stmt: Stmt = parse_quote! { let #loop_assign_ident = (#(#assigns),*); diff --git a/tests/expected/loop-contract/loop_assigns_for_fat_ptr.rs b/tests/expected/loop-contract/loop_assigns_for_fat_ptr.rs index 6c9701d996ee..64c52ec7ba6d 100644 --- a/tests/expected/loop-contract/loop_assigns_for_fat_ptr.rs +++ b/tests/expected/loop-contract/loop_assigns_for_fat_ptr.rs @@ -3,7 +3,7 @@ // kani-flags: -Z loop-contracts -//! Check the use of loop_assigns for Rust's Fat ptr +//! Check the use of loop_modifies for Rust's Fat ptr #![feature(proc_macro_hygiene)] #![feature(stmt_expr_attributes)] @@ -15,7 +15,7 @@ fn main() { let mut i = 0; let mut a: [u8; 100] = kani::any(); #[kani::loop_invariant(i <= 20)] - #[kani::loop_assigns(&i , slice_from_raw_parts(a.as_ptr(), 20))] + #[kani::loop_modifies(&i , slice_from_raw_parts(a.as_ptr(), 20))] while i < 20 { a[i] = 1; i = i + 1; diff --git a/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.rs b/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.rs index 479ceabea811..5c35bf8a8c91 100644 --- a/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.rs +++ b/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.rs @@ -3,7 +3,7 @@ // kani-flags: -Z loop-contracts -//! Check the use of loop_assigns for Rust's Fat ptr +//! Check the use of loop_modifies for Rust's Fat ptr #![feature(proc_macro_hygiene)] #![feature(stmt_expr_attributes)] @@ -15,7 +15,7 @@ fn main() { let mut i = 0; let mut a: [u8; 100] = kani::any(); #[kani::loop_invariant(i <= 20)] - #[kani::loop_assigns(&i , slice_from_raw_parts(a.as_ptr(), 18))] + #[kani::loop_modifies(&i , slice_from_raw_parts(a.as_ptr(), 18))] while i < 20 { a[i] = 1; i = i + 1; diff --git a/tests/expected/loop-contract/loop_assigns_for_ptr.rs b/tests/expected/loop-contract/loop_assigns_for_ptr.rs index d14dd83d64b7..a8443567f231 100644 --- a/tests/expected/loop-contract/loop_assigns_for_ptr.rs +++ b/tests/expected/loop-contract/loop_assigns_for_ptr.rs @@ -3,7 +3,7 @@ // kani-flags: -Z loop-contracts -//! Check the use of loop_assigns for Rust's ptr +//! Check the use of loop_modifies for Rust's ptr #![feature(proc_macro_hygiene)] #![feature(stmt_expr_attributes)] @@ -13,7 +13,7 @@ fn main() { let mut i = 0; let mut a: [u8; 20] = kani::any(); #[kani::loop_invariant(i <= 20)] - #[kani::loop_assigns(&i as *const _, a.as_slice())] + #[kani::loop_modifies(&i as *const _, a.as_slice())] while i < 20 { a[i] = 1; i = i + 1; diff --git a/tests/expected/loop-contract/loop_assigns_for_ptr_fail.rs b/tests/expected/loop-contract/loop_assigns_for_ptr_fail.rs index 5d28ed1a313d..5870d9749446 100644 --- a/tests/expected/loop-contract/loop_assigns_for_ptr_fail.rs +++ b/tests/expected/loop-contract/loop_assigns_for_ptr_fail.rs @@ -3,7 +3,7 @@ // kani-flags: -Z loop-contracts -//! Check a fail case for loop_assigns for Rust's ptr. a is not a fat ptr. +//! Check a fail case for loop_modifies for Rust's ptr. a is not a fat ptr. #![feature(proc_macro_hygiene)] #![feature(stmt_expr_attributes)] @@ -13,7 +13,7 @@ fn main() { let mut i = 0; let mut a: [u8; 20] = kani::any(); #[kani::loop_invariant(i <= 20)] - #[kani::loop_assigns(&i as *const _, a.as_ptr())] + #[kani::loop_modifies(&i as *const _, a.as_ptr())] while i < 20 { a[i] = 1; i = i + 1; diff --git a/tests/expected/loop-contract/loop_assigns_for_ref.rs b/tests/expected/loop-contract/loop_assigns_for_ref.rs index d2faf20dc359..b8a5c580985f 100644 --- a/tests/expected/loop-contract/loop_assigns_for_ref.rs +++ b/tests/expected/loop-contract/loop_assigns_for_ref.rs @@ -3,7 +3,7 @@ // kani-flags: -Z loop-contracts -//! Check the use of loop_assigns for Rust's ref +//! Check the use of loop_modifies for Rust's ref #![feature(proc_macro_hygiene)] #![feature(stmt_expr_attributes)] @@ -13,7 +13,7 @@ fn main() { let mut i = 0; let mut a: [u8; 20] = kani::any(); #[kani::loop_invariant(i <= 20)] - #[kani::loop_assigns(&i, &a)] + #[kani::loop_modifies(&i, &a)] while i < 20 { a[i] = 1; i = i + 1; diff --git a/tests/expected/loop-contract/loop_assigns_for_ref_fail.rs b/tests/expected/loop-contract/loop_assigns_for_ref_fail.rs index 6f11e99fedbb..ff387a806658 100644 --- a/tests/expected/loop-contract/loop_assigns_for_ref_fail.rs +++ b/tests/expected/loop-contract/loop_assigns_for_ref_fail.rs @@ -3,7 +3,7 @@ // kani-flags: -Z loop-contracts -//! Check the use of loop_assigns for Rust's ref +//! Check the use of loop_modifies for Rust's ref #![feature(proc_macro_hygiene)] #![feature(stmt_expr_attributes)] @@ -14,7 +14,7 @@ fn main() { let mut j = 0; let mut a: [u8; 20] = kani::any(); #[kani::loop_invariant(i <= 20 && i == j)] - #[kani::loop_assigns(&i, &a)] + #[kani::loop_modifies(&i, &a)] while i < 20 { a[i] = 1; i = i + 1; diff --git a/tests/expected/loop-contract/loop_assigns_for_vec.rs b/tests/expected/loop-contract/loop_assigns_for_vec.rs index c1b49a742994..2025ce94b856 100644 --- a/tests/expected/loop-contract/loop_assigns_for_vec.rs +++ b/tests/expected/loop-contract/loop_assigns_for_vec.rs @@ -3,7 +3,7 @@ // kani-flags: -Z loop-contracts -//! Check the use of loop_assigns for Rust's vec +//! Check the use of loop_modifies for Rust's vec #![feature(proc_macro_hygiene)] #![feature(stmt_expr_attributes)] @@ -19,7 +19,7 @@ fn main() { v.extend(a); //unsafe {(&v as *const Vec as *const usize).add(2)} is the ptr to v.len #[kani::loop_invariant(i <= 3)] - #[kani::loop_assigns(&i, slice_from_raw_parts(v.as_ptr(), 12), unsafe {(&v as *const Vec as *const usize).add(2)})] + #[kani::loop_modifies(&i, slice_from_raw_parts(v.as_ptr(), 12), unsafe {(&v as *const Vec as *const usize).add(2)})] while i < 3 { unsafe { ptr::copy_nonoverlapping(v.as_ptr(), (v.as_mut_ptr()).add(i * 3 + 3), 3); From e5a80c5be0d5fb8560078fafc4e418b42bd560ea Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 30 Jun 2025 09:42:58 -0700 Subject: [PATCH 5/5] fix format --- library/kani_macros/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index f22e74e9dc8b..9ceed99d114b 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -454,7 +454,7 @@ mod sysroot { mod loop_contracts; pub use contracts::{ensures, modifies, proof_for_contract, requires, stub_verified}; - pub use loop_contracts::{loop_modifies, loop_invariant}; + pub use loop_contracts::{loop_invariant, loop_modifies}; use super::*;