Add support for struct field accessing in loop contracts

kani-compiler/src/kani_middle/transform/loop_contracts.rs

@@ -16,8 +16,8 @@ use rustc_middle::ty::TyCtxt;
 use rustc_span::Symbol;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
-    AggregateKind, BasicBlock, BasicBlockIdx, Body, ConstOperand, Operand, Place, Rvalue,
-    Statement, StatementKind, Terminator, TerminatorKind, VarDebugInfoContents,
+    AggregateKind, BasicBlock, BasicBlockIdx, Body, ConstOperand, Operand, Rvalue, Statement,
+    StatementKind, Terminator, TerminatorKind, VarDebugInfoContents,
 };
 use stable_mir::ty::{FnDef, MirConst, RigidTy, UintTy};
 use std::collections::{HashMap, HashSet, VecDeque};
@@ -295,11 +295,11 @@ impl LoopContractPass {
 
                 // Collect supported vars assigned in the block.
                 // And check if all arguments of the closure is supported.
-                let mut supported_vars: Vec<Place> = Vec::new();
+                let mut supported_vars: Vec<usize> = Vec::new();
                 // All user variables are support
                 supported_vars.extend(new_body.var_debug_info().iter().filter_map(|info| {
                     match &info.value {
-                        VarDebugInfoContents::Place(debug_place) => Some(debug_place.clone()),
+                        VarDebugInfoContents::Place(debug_place) => Some(debug_place.local),
                         _ => None,
                     }
                 }));
@@ -310,8 +310,12 @@ impl LoopContractPass {
                 for stmt in &new_body.blocks()[bb_idx].statements {
                     if let StatementKind::Assign(place, rvalue) = &stmt.kind {
                         match rvalue {
+                            Rvalue::Ref(_,_,rplace) => {
+                                if supported_vars.contains(&rplace.local) {
+                                    supported_vars.push(place.local);
+                                } }
                             Rvalue::Aggregate(AggregateKind::Closure(..), closure_args) => {
-                                if closure_args.iter().any(|arg| !matches!(arg, Operand::Copy(arg_place) | Operand::Move(arg_place) if supported_vars.contains(arg_place))) {
+                                if closure_args.iter().any(|arg| !matches!(arg, Operand::Copy(arg_place) | Operand::Move(arg_place) if supported_vars.contains(&arg_place.local))) {
                                     unreachable!(
                                             "The loop invariant support only reference of user variables. The provided invariants contain unsupported dereference. \
                                             Please report github.com/model-checking/kani/issues/new?template=bug_report.md"
@@ -320,7 +324,7 @@ impl LoopContractPass {
                             }
                             _ => {
                                 if self.is_supported_argument_of_closure(rvalue, new_body) {
-                                    supported_vars.push(place.clone());
+                                    supported_vars.push(place.local);
                                 }
                             }
                         }

tests/expected/loop-contract/struct_projection.expected

@@ -0,0 +1,14 @@
+struct_projection.loop_invariant_step.1\
+	 - Status: SUCCESS\
+	 - Description: "Check invariant after step for loop struct_projection.0"
+
+struct_projection.loop_invariant_step.2\
+	 - Status: SUCCESS\
+	 - Description: "Check invariant after step for loop struct_projection.0"
+
+struct_projection.assertion.3\
+	 - Status: SUCCESS\
+	 - Description: "assertion failed: s.b == 2"
+
+
+VERIFICATION:- SUCCESSFUL

tests/expected/loop-contract/struct_projection.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! add support for struct field projection for loop-contract
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+struct mystruct {
+    a: i32,
+    b: i32,
+}
+
+#[kani::proof]
+fn struct_projection() {
+    let mut s = mystruct { a: 0, b: 2 };
+    let mut i = 0;
+    #[kani::loop_invariant((i<=10) && (s.a == i) && (s.b == 2))]
+    while i < 10 {
+        s.a += 1;
+        i += 1;
+    }
+    assert!(s.b == 2)
+}