Work around loop identification issues with CBMC

kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs

@@ -3,6 +3,7 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use rustc_middle::mir::{BasicBlock, BasicBlockData};
+use tracing::debug;
 
 impl<'tcx> GotocCtx<'tcx> {
     /// Generates Goto-C for a basic block.
@@ -12,6 +13,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This function does not return a value, but mutates state with
     /// `self.current_fn_mut().push_onto_block(...)`
     pub fn codegen_block(&mut self, bb: BasicBlock, bbd: &BasicBlockData<'tcx>) {
+        debug!(?bb, "Codegen basicblock");
         self.current_fn_mut().set_current_bb(bb);
         let label: String = self.current_fn().find_label(&bb);
         // the first statement should be labelled. if there is no statements, then the

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -12,6 +12,7 @@ use kani_queries::UserInput;
 use rustc_ast::Attribute;
 use rustc_hir::def::DefKind;
 use rustc_hir::def_id::DefId;
+use rustc_middle::mir::traversal::reverse_postorder;
 use rustc_middle::mir::{Body, HasLocalDecls, Local};
 use rustc_middle::ty::layout::FnAbiOf;
 use rustc_middle::ty::{self, Instance};
@@ -88,7 +89,7 @@ impl<'tcx> GotocCtx<'tcx> {
             self.codegen_function_prelude();
             self.codegen_declare_variables();
 
-            mir.basic_blocks.iter_enumerated().for_each(|(bb, bbd)| self.codegen_block(bb, bbd));
+            reverse_postorder(mir).for_each(|(bb, bbd)| self.codegen_block(bb, bbd));
 
             let loc = self.codegen_span(&mir.span);
             let stmts = self.current_fn_mut().extract_block();

tests/kani/Loops/loop_free.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Ensure that Kani identifies that there is not loop in this code.
+//! This was related to https://github.com/model-checking/kani/issues/2164
+fn loop_free<T: Default>(b: bool, other: T) -> T {
+    match b {
+        true => T::default(),
+        false => other,
+    }
+}
+
+/// Set the unwind to 1 so this test will fail instead of running forever.
+#[kani::proof]
+#[kani::unwind(1)]
+fn check_no_loop() {
+    let b: bool = kani::any();
+    let result = loop_free(b, 5);
+    assert!(result == 5 || (b && result == 0))
+}

tests/kani/Loops/loop_with_drop.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Ensure that Kani correctly unwind the loop with drop instructions which may .
+//! This was related to https://github.com/model-checking/kani/issues/2164
+/// Dummy function with a for loop that only runs 2 iterations.
+fn bounded_loop<T: Default>(b: bool, other: T) -> T {
+    let mut ret = other;
+    for i in 0..2 {
+        ret = match b {
+            true => T::default(),
+            false => ret,
+        };
+    }
+    return ret;
+}
+
+/// Harness that should succeed. We add a conservative loop bound.
+#[kani::proof]
+#[kani::unwind(3)]
+fn harness() {
+    let _ = bounded_loop(kani::any(), ());
+}