From 28e2cc6263f5b30a73cbde945a2162bb12d49cfc Mon Sep 17 00:00:00 2001 From: hung1962003 <106923246+hung1962003@users.noreply.github.com> Date: Tue, 27 Oct 2026 08:28:30 +0000 Subject: [PATCH] Add a loop's dead temporaries and loop-body variables to loop_modifies An explicit `#[kani::loop_modifies]` must cover every local that the loop writes. #4947 adds the loop-only locals that Kani generates, but MIR temporaries (e.g. the scrutinee of a `match` with `return` arms) and variables of the loop body that are still live when a `return` leaves the loop cannot be named by the user, and still fail with `Check that var_N is assignable`. Add to the write set the locals that are dead at the loop head where the write set is havocked (by a MIR liveness analysis), are not storage-local to the loop, and are temporaries or declared inside the loop's span, for loops that are not nested in another contracted loop. Emit `StorageLive` for them at the latch, so that havocking an address-taken temporary whose storage the last iteration ended is not a write to a dead object. Co-Authored-By: Claude Opus 5.5 --- .../codegen/statement.rs | 40 ++-- .../codegen_cprover_gotoc/overrides/hooks.rs | 24 ++- .../kani_middle/transform/loop_contracts.rs | 182 ++++++++++++++++++ ...loop_assigns_for_empty_slice_fail.expected | 2 +- .../loop_assigns_for_fat_ptr.expected | 4 +- .../loop_assigns_for_fat_ptr_fail.expected | 2 +- .../loop_assigns_for_ptr.expected | 4 +- .../loop_assigns_for_ptr_fail.expected | 2 +- .../loop_assigns_for_ref.expected | 2 +- .../loop_assigns_for_ref_fail.expected | 2 +- .../loop_assigns_for_vec.expected | 2 +- .../loop_modifies_match_temporary.expected | 1 + .../loop_modifies_match_temporary.rs | 53 +++++ .../loop_modifies_returned_local.expected | 1 + .../loop_modifies_returned_local.rs | 30 +++ .../loop_modifies_returned_temporary.expected | 1 + .../loop_modifies_returned_temporary.rs | 39 ++++ 17 files changed, 354 insertions(+), 37 deletions(-) create mode 100644 tests/expected/loop-contract/loop_modifies_match_temporary.expected create mode 100644 tests/expected/loop-contract/loop_modifies_match_temporary.rs create mode 100644 tests/expected/loop-contract/loop_modifies_returned_local.expected create mode 100644 tests/expected/loop-contract/loop_modifies_returned_local.rs create mode 100644 tests/expected/loop-contract/loop_modifies_returned_temporary.expected create mode 100644 tests/expected/loop-contract/loop_modifies_returned_temporary.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 1b725053323e..132773c2f33d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -238,6 +238,27 @@ impl GotocCtx<'_, '_> { self.tcx.dcx().span_warn(rustc_internal::internal(self.tcx, span), msg); } + /// `StorageLive(var_id)`: see the `StorageLive` and `StorageDead` case of + /// [GotocCtx::codegen_statement]. + pub fn codegen_storage_live(&mut self, var_id: Local, location: Location) -> Stmt { + if !self.current_fn().is_address_taken_local(var_id) { + Stmt::skip(location) + } else { + let global_dead_object = cbmc::global_dead_object(&self.symbol_table); + Stmt::assign( + global_dead_object.clone(), + global_dead_object + .clone() + .eq(self + .codegen_local(var_id, location) + .address_of() + .cast_to(global_dead_object.typ().clone())) + .ternary(global_dead_object.typ().null(), global_dead_object), + location, + ) + } + } + /// 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. @@ -372,24 +393,7 @@ impl GotocCtx<'_, '_> { // This approach will also work when there are multiple occurrences of StorageLive (or // StorageDead) on a path, or across control-flow branches, and even when StorageDead // occurs without a preceding StorageLive. - StatementKind::StorageLive(var_id) => { - if !self.current_fn().is_address_taken_local(*var_id) { - Stmt::skip(location) - } else { - let global_dead_object = cbmc::global_dead_object(&self.symbol_table); - Stmt::assign( - global_dead_object.clone(), - global_dead_object - .clone() - .eq(self - .codegen_local(*var_id, location) - .address_of() - .cast_to(global_dead_object.typ().clone())) - .ternary(global_dead_object.typ().null(), global_dead_object), - location, - ) - } - } + StatementKind::StorageLive(var_id) => self.codegen_storage_live(*var_id, location), StatementKind::StorageDead(var_id) => { if !self.current_fn().is_address_taken_local(*var_id) { Stmt::skip(location) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index c80901a69593..cbc3fb804158 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -881,6 +881,7 @@ 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 current_fn = gcx.current_fn().instance_stable(); + let mut storage_live = Vec::new(); if let Some(mut assigns) = gcx.loop_modifies.remove(&(current_fn, instance)) { // The user wrote a loop modifies clause, possibly without any target. Add the // locals that the loop contract transformation makes live across iterations of @@ -888,6 +889,12 @@ impl GotocHook for LoopInvariantRegister { // clause instead). let generated = gcx.transformer.generated_loop_modifies(current_fn, instance).to_vec(); + // The storage of such a local can end in the loop body, which can make it the + // dead object (see `codegen_storage_live`) when the latch jumps back to the + // loop head, where the loop havocs it. It is dead there: mark its storage live, + // as its `StorageLive` in the body would. + storage_live = + generated.iter().map(|local| gcx.codegen_storage_live(*local, loc)).collect(); assigns.extend(generated.into_iter().map(|local| gcx.codegen_local(local, loc))); if assigns.is_empty() { // The clause has no target (e.g. `#[kani::loop_modifies()]`, or only targets @@ -913,15 +920,14 @@ impl GotocHook for LoopInvariantRegister { // Add `free(0)` to make sure the body of `free` won't be dropped to // satisfy the requirement of DFCC. - Stmt::block( - vec![ - BuiltinFn::Free - .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc) - .as_stmt(loc), - stmt, - ], - loc, - ) + let mut stmts = vec![ + BuiltinFn::Free + .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc) + .as_stmt(loc), + ]; + stmts.extend(storage_live); + stmts.push(stmt); + Stmt::block(stmts, loc) } else { // When loop-contracts is not enabled, codegen // assign_to = true diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index 178cd870df0e..b1aefe6e6d21 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -17,6 +17,9 @@ use crate::rustc_public::CrateDef; use itertools::Itertools; use rustc_middle::ty::TyCtxt; use rustc_public::mir::mono::Instance; +use rustc_public::mir::visit::{ + Location, MirVisitor, PlaceContext, statement_location, terminator_location, +}; use rustc_public::mir::{ AggregateKind, BasicBlock, BasicBlockIdx, Body, ConstOperand, Local, Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, @@ -172,6 +175,33 @@ impl FirstPatRenamer<'_> { } } +/// The locals that a statement or terminator reads, for [LoopContractPass::live_at_block_starts]. +#[derive(Default)] +struct LocalsCollector(Vec); + +impl MirVisitor for LocalsCollector { + fn visit_local(&mut self, local: &Local, _ptx: PlaceContext, _location: Location) { + self.0.push(*local); + } +} + +impl LocalsCollector { + /// A write to `place`: the local that it defines if it writes the whole local, or else (a + /// write to a part) a read of the local and of the indices. + fn write_to(&mut self, place: &Place) -> Option { + if place.projection.is_empty() { + return Some(place.local); + } + self.0.push(place.local); + for elem in &place.projection { + if let ProjectionElem::Index(local) = elem { + self.0.push(*local); + } + } + None + } +} + impl MutMirVisitor for FirstPatRenamer<'_> { fn visit_operand(&mut self, operand: &mut Operand) { if let Operand::Copy(place) | Operand::Move(place) = operand { @@ -1379,6 +1409,12 @@ impl LoopContractPass { let mut new_latches: Vec<(usize, usize)> = self.new_loop_latches.iter().map(|(head, latch)| (*head, *latch)).collect(); new_latches.sort(); + if new_latches.is_empty() { + return; + } + let live = Self::live_at_block_starts(body); + let variables: HashSet = + body.var_debug_info().iter().filter_map(|info| info.local()).collect(); for (loop_head, new_latch) in new_latches { let Some((register_fn, loop_id)) = self.register_fn(body, tcx, new_latch) else { continue; @@ -1404,6 +1440,54 @@ impl LoopContractPass { if let Some(locals) = self.generated_loop_locals.get(&loop_head) { candidates.extend(locals.iter().copied()); } + // The temporaries, and the variables that the loop body declares, that are dead at + // the loop head, where the loop havocs its write set: the target of the latch (the + // block of the original head runs before it, once). CBMC still requires them in the + // write set when the loop is left while they hold a value, e.g. a `let` in the loop + // body that a `return` in it reads. A variable declared before the loop is not + // added, even if it is dead at the loop head: the user names it in the clause. + let heads = body.blocks()[new_latch].terminator.successors(); + let loop_span: Vec = loop_id.split('_').filter_map(|n| n.parse().ok()).collect(); + let declared_in_loop = |local: usize| { + let lines = body.locals()[local].span.get_lines(); + let start = (lines.start_line, lines.start_col); + loop_span.len() == 4 + && start > (loop_span[0], loop_span[1]) + && start < (loop_span[2], loop_span[3]) + }; + // A local whose storage the loop both starts and ends is local to the loop, and CBMC + // already allows the loop to write it. The others are declared at the start of the + // function, or are still live when the loop is left (e.g. the scrutinee of a `match` + // with a `return` arm). + let in_loop = Self::natural_loop(body, new_latch); + let (mut started, mut ended_outside) = (HashSet::new(), HashSet::new()); + for (bb, block) in body.blocks().iter().enumerate() { + for stmt in &block.statements { + match stmt.kind { + StatementKind::StorageLive(local) if in_loop.contains(&bb) => { + started.insert(local); + } + StatementKind::StorageDead(local) if !in_loop.contains(&bb) => { + ended_outside.insert(local); + } + _ => {} + } + } + } + let storage_live_in_loop: HashSet = + started.difference(&ended_outside).copied().collect(); + // Not for a loop in another loop with a contract: the write set that CBMC infers for + // the outer loop does not have these locals, so its inclusion check would fail. + let nested = loop_positions + .iter() + .any(|(head, latch)| *head < loop_head && *loop_latch <= *latch); + candidates.extend( + (body.arg_count() + 1..body.locals().len()) + .filter(|_| !nested) + .filter(|local| !storage_live_in_loop.contains(local)) + .filter(|local| heads.iter().all(|head| !live[*head].contains(local))) + .filter(|local| !variables.contains(local) || declared_in_loop(*local)), + ); // Only keep the locals that the loop writes to, e.g., not a `kaniiter` whose // initialization was moved to the head of an outer loop. let written = Self::locals_written_in(body, loop_head + 1..=*loop_latch); @@ -1452,6 +1536,104 @@ impl LoopContractPass { Some((Instance::resolve(fn_def, &args).ok()?, loop_id.to_string())) } + /// The blocks of the loop whose new latch is `new_latch`: the target of the latch (the head of + /// the loop in the generated code), and the blocks that reach the latch without passing it. + fn natural_loop(body: &MutableBody, new_latch: usize) -> HashSet { + let mut predecessors = vec![Vec::new(); body.blocks().len()]; + for (bb, block) in body.blocks().iter().enumerate() { + for succ in block.terminator.successors() { + predecessors[succ].push(bb); + } + } + let mut blocks: HashSet = + body.blocks()[new_latch].terminator.successors().into_iter().collect(); + let mut stack = vec![new_latch]; + while let Some(bb) = stack.pop() { + if blocks.insert(bb) { + stack.extend(&predecessors[bb]); + } + } + blocks + } + + /// The locals that are live at the start of each block: read (in whole or in part, or + /// borrowed) on some path from there before the path overwrites them as a whole or ends + /// their storage. A loop can havoc a local that is not live at its head: no value of it + /// reaches the loop body from before the loop or from an earlier iteration. + fn live_at_block_starts(body: &MutableBody) -> Vec> { + // `statement_location` needs a `Body`; the spread argument and the span do not matter. + let body = Body::new( + body.blocks().to_vec(), + body.locals().to_vec(), + body.arg_count(), + body.var_debug_info().clone(), + None, + body.locals()[0].span, + ); + // The locals that each block reads before it defines them, and those it defines. + let mut uses = vec![HashSet::new(); body.blocks.len()]; + let mut defs = vec![HashSet::new(); body.blocks.len()]; + for (bb, block) in body.blocks.iter().enumerate() { + let mut access = |reads: Vec, def: Option| { + for local in reads { + if !defs[bb].contains(&local) { + uses[bb].insert(local); + } + } + if let Some(local) = def { + defs[bb].insert(local); + } + }; + for (idx, stmt) in block.statements.iter().enumerate() { + let location = statement_location(&body, &bb, idx); + let mut reads = LocalsCollector::default(); + let def = match &stmt.kind { + StatementKind::StorageLive(local) | StatementKind::StorageDead(local) => { + Some(*local) + } + StatementKind::Assign(place, rvalue) => { + reads.visit_rvalue(rvalue, location); + reads.write_to(place) + } + _ => { + reads.visit_statement(stmt, location); + None + } + }; + access(reads.0, def); + } + let location = terminator_location(&body, &bb); + let mut reads = LocalsCollector::default(); + let def = match &block.terminator.kind { + TerminatorKind::Call { func, args, destination, .. } => { + reads.visit_operand(func, location); + args.iter().for_each(|arg| reads.visit_operand(arg, location)); + reads.write_to(destination) + } + _ => { + reads.visit_terminator(&block.terminator, location); + None + } + }; + access(reads.0, def); + } + let mut live = uses.clone(); + let mut changed = true; + while changed { + changed = false; + for bb in (0..body.blocks.len()).rev() { + for succ in body.blocks[bb].terminator.successors() { + let flowing: Vec = + live[succ].iter().filter(|l| !defs[bb].contains(*l)).copied().collect(); + for local in flowing { + changed |= live[bb].insert(local); + } + } + } + } + live + } + /// The locals that are assigned (as the root of the assigned place, or as the destination /// of a call) in the given blocks. A write through a pointer, e.g. `(*p).f = ..`, counts as /// a write to `p`, which is fine to filter the candidates of a loop. diff --git a/tests/expected/loop-contract/loop_assigns_for_empty_slice_fail.expected b/tests/expected/loop-contract/loop_assigns_for_empty_slice_fail.expected index 09d9264060eb..2556e39330b7 100644 --- a/tests/expected/loop-contract/loop_assigns_for_empty_slice_fail.expected +++ b/tests/expected/loop-contract/loop_assigns_for_empty_slice_fail.expected @@ -1,4 +1,4 @@ -main.assigns.1\ +main.assigns.4\ - Status: FAILURE\ - Description: "Check that a[var_14] is assignable" diff --git a/tests/expected/loop-contract/loop_assigns_for_fat_ptr.expected b/tests/expected/loop-contract/loop_assigns_for_fat_ptr.expected index 62271ee7a2a1..ee0fa0dcc356 100644 --- a/tests/expected/loop-contract/loop_assigns_for_fat_ptr.expected +++ b/tests/expected/loop-contract/loop_assigns_for_fat_ptr.expected @@ -1,8 +1,8 @@ -main.assigns.1\ +main.assigns.4\ - Status: SUCCESS\ - Description: "Check that a[var_15] is assignable" -main.assigns.2\ +main.assigns.6\ - Status: SUCCESS\ - Description: "Check that i is assignable" 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 index ba0926539392..d8c9b94adf2f 100644 --- a/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.expected +++ b/tests/expected/loop-contract/loop_assigns_for_fat_ptr_fail.expected @@ -1,4 +1,4 @@ -main.assigns.1\ +main.assigns.4\ - Status: FAILURE\ - Description: "Check that a[var_15] is assignable" diff --git a/tests/expected/loop-contract/loop_assigns_for_ptr.expected b/tests/expected/loop-contract/loop_assigns_for_ptr.expected index c8d51a4544ca..219da9bb2f22 100644 --- a/tests/expected/loop-contract/loop_assigns_for_ptr.expected +++ b/tests/expected/loop-contract/loop_assigns_for_ptr.expected @@ -1,8 +1,8 @@ -main.assigns.1\ +main.assigns.4\ - Status: SUCCESS\ - Description: "Check that a[var_14] is assignable" -main.assigns.2\ +main.assigns.6\ - Status: SUCCESS\ - Description: "Check that i is assignable" diff --git a/tests/expected/loop-contract/loop_assigns_for_ptr_fail.expected b/tests/expected/loop-contract/loop_assigns_for_ptr_fail.expected index 882d7607e992..7ccab6f3d994 100644 --- a/tests/expected/loop-contract/loop_assigns_for_ptr_fail.expected +++ b/tests/expected/loop-contract/loop_assigns_for_ptr_fail.expected @@ -1,4 +1,4 @@ -main.assigns.1\ +main.assigns.4\ - Status: FAILURE\ - Description: "Check that a[var_15] is assignable" diff --git a/tests/expected/loop-contract/loop_assigns_for_ref.expected b/tests/expected/loop-contract/loop_assigns_for_ref.expected index 59db3e04b3d8..c1a67a466892 100644 --- a/tests/expected/loop-contract/loop_assigns_for_ref.expected +++ b/tests/expected/loop-contract/loop_assigns_for_ref.expected @@ -1,4 +1,4 @@ -main.assigns.1\ +main.assigns.4\ - Status: SUCCESS\ - Description: "Check that a[var_12] is assignable" diff --git a/tests/expected/loop-contract/loop_assigns_for_ref_fail.expected b/tests/expected/loop-contract/loop_assigns_for_ref_fail.expected index 7c805eac7ea1..df0120dd8f45 100644 --- a/tests/expected/loop-contract/loop_assigns_for_ref_fail.expected +++ b/tests/expected/loop-contract/loop_assigns_for_ref_fail.expected @@ -1,4 +1,4 @@ -main.assigns.3\ +main.assigns.8\ - Status: FAILURE\ - Description: "Check that j is assignable" diff --git a/tests/expected/loop-contract/loop_assigns_for_vec.expected b/tests/expected/loop-contract/loop_assigns_for_vec.expected index b1d5d1c9d85e..2309cf1d264c 100644 --- a/tests/expected/loop-contract/loop_assigns_for_vec.expected +++ b/tests/expected/loop-contract/loop_assigns_for_vec.expected @@ -1,4 +1,4 @@ -main.assigns.1\ +main.assigns.6\ - Status: SUCCESS\ - Description: "Check that i is assignable" diff --git a/tests/expected/loop-contract/loop_modifies_match_temporary.expected b/tests/expected/loop-contract/loop_modifies_match_temporary.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/loop-contract/loop_modifies_match_temporary.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/loop_modifies_match_temporary.rs b/tests/expected/loop-contract/loop_modifies_match_temporary.rs new file mode 100644 index 000000000000..2c5102b8e96e --- /dev/null +++ b/tests/expected/loop-contract/loop_modifies_match_temporary.rs @@ -0,0 +1,53 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! The scrutinee of a `match` with `return` arms is a temporary that the user cannot name. +//! It does not need to be in an explicit `#[kani::loop_modifies]` clause (the shape of the +//! provided `Searcher::next_reject` in `core::str::pattern`). + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +enum Step { + Hit(usize), + Miss, + Done, +} + +struct Cursor { + pos: usize, + end: usize, +} + +impl Cursor { + fn step(&mut self) -> Step { + if self.pos >= self.end { + return Step::Done; + } + self.pos += 1; + if kani::any() { Step::Hit(self.pos) } else { Step::Miss } + } +} + +fn next_hit(c: &mut Cursor) -> Option { + #[kani::loop_invariant(c.pos <= c.end)] + #[kani::loop_modifies(&c.pos)] + loop { + match c.step() { + Step::Hit(pos) => return Some(pos), + Step::Done => return None, + _ => continue, + } + } +} + +#[kani::proof] +fn main() { + let end: usize = kani::any(); + let mut c = Cursor { pos: 0, end }; + if let Some(pos) = next_hit(&mut c) { + assert!(0 < pos && pos <= end); + } +} diff --git a/tests/expected/loop-contract/loop_modifies_returned_local.expected b/tests/expected/loop-contract/loop_modifies_returned_local.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/loop-contract/loop_modifies_returned_local.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/loop_modifies_returned_local.rs b/tests/expected/loop-contract/loop_modifies_returned_local.rs new file mode 100644 index 000000000000..8baf2cd905ae --- /dev/null +++ b/tests/expected/loop-contract/loop_modifies_returned_local.rs @@ -0,0 +1,30 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! A variable that the loop body declares and that a `return` in the loop body reads does not +//! need to be in an explicit `#[kani::loop_modifies]` clause: it is dead at the loop head. + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +fn first_above(n: u8) -> u8 { + let mut i: u8 = 0; + #[kani::loop_invariant(i <= 10)] + #[kani::loop_modifies(&i)] + while i < 10 { + let found = i + 1; + if found > n { + return found; + } + i += 1; + } + 0 +} + +#[kani::proof] +fn main() { + let n: u8 = kani::any_where(|n| *n < 10); + assert!(first_above(n) <= 10); +} diff --git a/tests/expected/loop-contract/loop_modifies_returned_temporary.expected b/tests/expected/loop-contract/loop_modifies_returned_temporary.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/loop-contract/loop_modifies_returned_temporary.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/loop-contract/loop_modifies_returned_temporary.rs b/tests/expected/loop-contract/loop_modifies_returned_temporary.rs new file mode 100644 index 000000000000..0025fd70d026 --- /dev/null +++ b/tests/expected/loop-contract/loop_modifies_returned_temporary.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z loop-contracts + +//! A borrowed temporary that a `return` in the loop body leaves live (`x + 0`) is added to the +//! write set of an explicit `#[kani::loop_modifies]`. Its storage has ended when an iteration +//! goes back to the loop head, where the write set is havocked; that havoc must not fail as a +//! write to a dead object. + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +fn same(a: &u8, b: &u8) -> bool { + *a == *b +} + +fn find(a: &[u8; 8], x: u8) -> Option { + let mut i: usize = 0; + #[kani::loop_invariant(i <= 8)] + #[kani::loop_modifies(&i)] + while i < 8 { + let s = &a[i]; + if same(s, &(x + 0)) { + return Some(i); + } + i += 1; + } + None +} + +#[kani::proof] +fn main() { + let a: [u8; 8] = kani::any(); + let x: u8 = kani::any(); + if let Some(i) = find(&a, x) { + assert!(a[i] == x); + } +}