From 6e42febf6eb47b0a6833166a9b4aaf4fded07548 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 21 Jul 2025 14:56:36 -0700 Subject: [PATCH 1/3] fix tuple position --- .../src/kani_middle/transform/loop_contracts.rs | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index 4d0aa6e011dc..baa51f26ff38 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -661,7 +661,16 @@ impl LoopContractPass { let TyKind::RigidTy(RigidTy::Closure(_, genarg)) = arg_ty.kind() else { return false; }; - let GenericArgKind::Type(arg_ty) = genarg.0[2] else { return false }; + let mut fnptrpos = 0; + for (i, arg) in genarg.0.iter().enumerate() { + if let GenericArgKind::Type(arg_ty) = arg + && let TyKind::RigidTy(RigidTy::FnPtr(_)) = arg_ty.kind() + { + fnptrpos = i; + break; + } + } + let GenericArgKind::Type(arg_ty) = genarg.0[fnptrpos + 1] else { return false }; let TyKind::RigidTy(RigidTy::Tuple(args)) = arg_ty.kind() else { return false }; // Check if the invariant involves any local variable if !args.is_empty() { From 1d15bb43b057ca20814a0d7845b3bf94e1404d17 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 22 Jul 2025 08:14:22 -0700 Subject: [PATCH 2/3] add expected tests --- .../loop_in_generic_function.expected | 9 ++++++ .../loop-contract/loop_in_generic_function.rs | 30 +++++++++++++++++++ 2 files changed, 39 insertions(+) create mode 100644 tests/expected/loop-contract/loop_in_generic_function.expected create mode 100644 tests/expected/loop-contract/loop_in_generic_function.rs diff --git a/tests/expected/loop-contract/loop_in_generic_function.expected b/tests/expected/loop-contract/loop_in_generic_function.expected new file mode 100644 index 000000000000..669c2cb363f6 --- /dev/null +++ b/tests/expected/loop-contract/loop_in_generic_function.expected @@ -0,0 +1,9 @@ +sum::.loop_invariant_base.1\ + - Status: SUCCESS\ + - Description: "Check invariant before entry for loop sum::.0" + +main.assertion.1\ + - Status: SUCCESS\ + - Description: "assertion failed: j <= 2560" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/loop_in_generic_function.rs b/tests/expected/loop-contract/loop_in_generic_function.rs new file mode 100644 index 000000000000..cb037e53928e --- /dev/null +++ b/tests/expected/loop-contract/loop_in_generic_function.rs @@ -0,0 +1,30 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! Check loop in generic function + +#![feature(proc_macro_hygiene)] +#![feature(stmt_expr_attributes)] + +fn sum(a: &[T]) -> u32 +where + u32: std::convert::From, +{ + let mut j: u32 = 0; + let mut i: usize = 0; + #[kani::loop_invariant(i<=10 && j <= (u8::MAX as u32) * (i as u32))] + while i < 10 { + j = j + std::convert::Into::::into(a[i].clone()); + i = i + 1; + } + j +} + +#[kani::proof] +fn main() { + let a: [u8; 10] = kani::any(); + let j = sum(a.as_slice()); + assert!(j <= 2560); +} From f5316240641b9a4b755db06535e87ab9e2109e28 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 22 Jul 2025 13:16:00 -0700 Subject: [PATCH 3/3] add comments --- kani-compiler/src/kani_middle/transform/loop_contracts.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index baa51f26ff38..ba267174f947 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -661,6 +661,9 @@ impl LoopContractPass { let TyKind::RigidTy(RigidTy::Closure(_, genarg)) = arg_ty.kind() else { return false; }; + // We look for the args' types of the kani_register_loop_contract function + // They are always stored in a tuple, which is next to the FnPtr generic args of kani_registered_loop_contract fn + // All the generic args before the FnPtr are from the outer function let mut fnptrpos = 0; for (i, arg) in genarg.0.iter().enumerate() { if let GenericArgKind::Type(arg_ty) = arg