Work around loop identification issues with CBMC (#2181)

CBMC has a heuristic to identify loops that identifies any jump to a previously declared basic block as the back edge of a loop.

For rust, this happens often due to drop elaboration. See https://rustc-dev-guide.rust-lang.org/mir/drop-elaboration.html#drop-elaboration-1 for more details.

To avoid that issue, we now codegen basic blocks in topological order.

Author: celinval

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/cargo-kani/small-vec/src/lib.rs

@@ -4,6 +4,7 @@
 use smallvec::{smallvec, SmallVec};
 
 #[kani::proof]
+#[kani::unwind(4)]
 pub fn check_vec() {
     // Create small vec with three elements.
     let chars: SmallVec<[char; 3]> = smallvec![kani::any(), kani::any(), kani::any()];

tests/kani/Drop/drop_after_moving_across_channel.rs

@@ -0,0 +1,32 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks whether dropping objects passed through
+//! std::sync::mpsc::channel is handled.
+//! This test only passes on MacOS today, so we duplicate the test for now.
+#![cfg(target_os = "macos")]
+
+use std::sync::mpsc::*;
+
+static mut CELL: i32 = 0;
+
+struct DropSetCELLToOne {}
+
+impl Drop for DropSetCELLToOne {
+    fn drop(&mut self) {
+        unsafe {
+            CELL = 1;
+        }
+    }
+}
+
+#[kani::unwind(1)]
+#[kani::proof]
+fn main() {
+    {
+        let (send, recv) = channel::<DropSetCELLToOne>();
+        send.send(DropSetCELLToOne {}).unwrap();
+        let _to_drop: DropSetCELLToOne = recv.recv().unwrap();
+    }
+    assert_eq!(unsafe { CELL }, 1, "Drop should be called");
+}

tests/kani/Drop/fixme_drop_after_moving_across_channel.rs

@@ -9,27 +9,38 @@
 // kani::unwind(2) takes longer than 10m on a M1 Mac. For details,
 // please see: https://github.com/model-checking/kani/issues/1286
 
-use std::sync::mpsc::*;
+#[cfg(target_os = "linux")]
+mod fixme_harness {
+    use std::sync::mpsc::*;
 
-static mut CELL: i32 = 0;
+    static mut CELL: i32 = 0;
 
-struct DropSetCELLToOne {}
+    struct DropSetCELLToOne {}
 
-impl Drop for DropSetCELLToOne {
-    fn drop(&mut self) {
-        unsafe {
-            CELL = 1;
+    impl Drop for DropSetCELLToOne {
+        fn drop(&mut self) {
+            unsafe {
+                CELL = 1;
+            }
         }
     }
+
+    #[kani::unwind(1)]
+    #[kani::proof]
+    fn main() {
+        {
+            let (send, recv) = channel::<DropSetCELLToOne>();
+            send.send(DropSetCELLToOne {}).unwrap();
+            let _to_drop: DropSetCELLToOne = recv.recv().unwrap();
+        }
+        assert_eq!(unsafe { CELL }, 1, "Drop should be called");
+    }
 }
 
-#[kani::unwind(1)]
-#[kani::proof]
-fn main() {
-    {
-        let (send, recv) = channel::<DropSetCELLToOne>();
-        send.send(DropSetCELLToOne {}).unwrap();
-        let _to_drop: DropSetCELLToOne = recv.recv().unwrap();
+#[cfg(target_os = "macos")]
+mod forced_failure {
+    #[kani::proof]
+    fn just_panic() {
+        panic!("This test only fails on linux");
     }
-    assert_eq!(unsafe { CELL }, 1, "Drop should be called");
 }

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,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Ensure that Kani correctly unwinds the loop with drop instructions.
+//! 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(), ());
+}