Work around loop identification issues with CBMC #2181

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged

celinval merged 5 commits into model-checking:main from celinval:issue-2164-topsort

Feb 3, 2023

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

-Original file line number
+Diff line change
@@ Expand Up / @@ -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.
@@ Expand All / @@ -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
@@ Expand Down @@

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

-Original file line number
+Diff line change
@@ Expand Up / @@ -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};
@@ Expand Down Expand Up / @@ -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();
@@ Expand Down @@

tests/cargo-kani/small-vec/src/lib.rs

-Original file line number
+Diff line change
@@ Expand Up / @@ -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()];
@@ Expand Down @@

tests/kani/Drop/drop_after_moving_across_channel.rs

-Original file line number
+Diff line change
@@ -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

-Original file line number
+Diff line change
@@ Expand Up / @@ -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

-Original file line number
+Diff line change
@@ -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

-Original file line number
+Diff line change
@@ -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(), ());
+    }

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Work around loop identification issues with CBMC #2181

Uh oh!

Diff view

Diff view

There are no files selected for viewing

tedinski Feb 2, 2023

Uh oh!

Work around loop identification issues with CBMC #2181

Uh oh!

Work around loop identification issues with CBMC #2181

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

tedinski Feb 2, 2023

Choose a reason for hiding this comment

Uh oh!