Fix the bug of while loop invariant contains no local variables (#4022)

This PR fixes the bug of while loop invariant contains no local
variables.

Previously, for a while loop, if the loop invariant is
`#[kani::loop_invariant(true)]`, we will get an error:
"The assumptions for loop-contracts transformation are violated by some
other transformation.
Please report
github.com/model-checking/kani/issues/new?template=bug_report.md"

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Michael Tautschnig <[email protected]>

Author: thanhnguyen-aws

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

@@ -19,7 +19,7 @@ use stable_mir::mir::{
     AggregateKind, BasicBlock, BasicBlockIdx, Body, ConstOperand, Operand, Rvalue, Statement,
     StatementKind, Terminator, TerminatorKind, VarDebugInfoContents,
 };
-use stable_mir::ty::{FnDef, MirConst, RigidTy, UintTy};
+use stable_mir::ty::{FnDef, GenericArgKind, MirConst, RigidTy, TyKind, UintTy};
 use std::collections::{HashMap, HashSet, VecDeque};
 use std::fmt::Debug;
 
@@ -261,7 +261,7 @@ impl LoopContractPass {
         } = &terminator.kind
         {
             // Get the function signature of the terminator call.
-            let Some(RigidTy::FnDef(fn_def, ..)) = terminator_func
+            let Some(RigidTy::FnDef(fn_def, genarg)) = terminator_func
                 .ty(new_body.locals())
                 .ok()
                 .map(|fn_ty| fn_ty.kind().rigid().unwrap().clone())
@@ -286,10 +286,18 @@ impl LoopContractPass {
                     Please report github.com/model-checking/kani/issues/new?template=bug_report.md"
                     );
                 }
-
-                let ori_condition_bb_idx =
-                    new_body.blocks()[terminator_target.unwrap()].terminator.successors()[1];
-                self.make_invariant_closure_alive(new_body, ori_condition_bb_idx);
+                let GenericArgKind::Type(arg_ty) = genarg.0[0] else { return false };
+                let TyKind::RigidTy(RigidTy::Closure(_, genarg)) = arg_ty.kind() else {
+                    return false;
+                };
+                let GenericArgKind::Type(arg_ty) = genarg.0[2] 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() {
+                    let ori_condition_bb_idx =
+                        new_body.blocks()[terminator_target.unwrap()].terminator.successors()[1];
+                    self.make_invariant_closure_alive(new_body, ori_condition_bb_idx);
+                }
 
                 contain_loop_contracts = true;
 

tests/expected/loop-contract/loop_with_true_invariant.expected

@@ -0,0 +1,5 @@
+main.loop_invariant_base.1\
+	 - Status: SUCCESS\
+	 - Description: "Check invariant before entry for loop main.0"
+
+VERIFICATION:- SUCCESSFUL

tests/expected/loop-contract/loop_with_true_invariant.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: -Z loop-contracts
+
+//! Check the use of "true" in loop invariant
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+#[kani::proof]
+fn main(){
+    let mut i = 100;
+    #[kani::loop_invariant(true)]
+    while i > 1 {
+        i /= 2;
+    } 
+}