Ensure that non-determinism is not used in assumption context

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -143,6 +143,46 @@ impl GotocHook for Assert {
     }
 }
 
+struct Check;
+impl GotocHook for Check {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance.def, "KaniCheck")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        mut fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 2);
+        let cond = fargs.remove(0).cast_to(Type::bool());
+        let msg = fargs.remove(0);
+        let msg = gcx.extract_const_message(&msg).unwrap();
+        let target = target.unwrap();
+        let caller_loc = gcx.codegen_caller_span_stable(span);
+
+        let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span);
+
+        // Since `cond` might have side effects, assign it to a temporary
+        // variable so that it's evaluated once, then assert it
+        // TODO: I don't think `cond` can have side effects, this is MIR, it's going to be temps
+        let (tmp, decl) = gcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc);
+        Stmt::block(
+            vec![
+                reach_stmt,
+                decl,
+                gcx.codegen_assert(tmp, PropertyClass::Assertion, &msg, caller_loc),
+                Stmt::goto(bb_label(target), caller_loc),
+            ],
+            caller_loc,
+        )
+    }
+}
+
 struct Nondet;
 
 impl GotocHook for Nondet {
@@ -510,6 +550,7 @@ pub fn fn_hooks() -> GotocHooks {
             Rc::new(Panic),
             Rc::new(Assume),
             Rc::new(Assert),
+            Rc::new(Check),
             Rc::new(Cover),
             Rc::new(Nondet),
             Rc::new(IsAllocated),

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

@@ -387,12 +387,13 @@ pub enum CheckType {
 }
 
 impl CheckType {
-    /// This will create the type of check that is available in the current crate.
+    /// This will create the type of check that is available in the current crate, attempting to
+    /// create a check that generates an assertion following by an assumption of the same assertion.
     ///
     /// If `kani` crate is available, this will return [CheckType::Assert], and the instance will
     /// point to `kani::assert`. Otherwise, we will collect the `core::panic_str` method and return
     /// [CheckType::Panic].
-    pub fn new(tcx: TyCtxt) -> CheckType {
+    pub fn new_assert_assume(tcx: TyCtxt) -> CheckType {
         if let Some(instance) = find_instance(tcx, "KaniAssert") {
             CheckType::Assert(instance)
         } else if find_instance(tcx, "panic_str").is_some() {
@@ -401,6 +402,22 @@ impl CheckType {
             CheckType::NoCore
         }
     }
+
+    /// This will create the type of check that is available in the current crate, attempting to
+    /// create a check that generates an assertion, without assuming the condition afterwards.
+    ///
+    /// If `kani` crate is available, this will return [CheckType::Assert], and the instance will
+    /// point to `kani::assert`. Otherwise, we will collect the `core::panic_str` method and return
+    /// [CheckType::Panic].
+    pub fn new_assert(tcx: TyCtxt) -> CheckType {
+        if let Some(instance) = find_instance(tcx, "KaniCheck") {
+            CheckType::Assert(instance)
+        } else if find_instance(tcx, "panic_str").is_some() {
+            CheckType::Panic
+        } else {
+            CheckType::NoCore
+        }
+    }
 }
 
 /// We store the index of an instruction to avoid borrow checker issues and unnecessary copies.

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

@@ -60,7 +60,7 @@ impl BodyTransformation {
             inst_passes: vec![],
             cache: Default::default(),
         };
-        let check_type = CheckType::new(tcx);
+        let check_type = CheckType::new_assert_assume(tcx);
         transformer.add_pass(queries, FnStubPass::new(&unit.stubs));
         transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs));
         // This has to come after stubs since we want this to replace the stubbed body.
@@ -73,7 +73,11 @@ impl BodyTransformation {
         // generated code for future instrumentation passes.
         transformer.add_pass(
             queries,
-            UninitPass { check_type: check_type.clone(), mem_init_fn_cache: HashMap::new() },
+            UninitPass {
+                // Since this uses demonic non-determinism under the hood, should not assume the assertion.
+                check_type: CheckType::new_assert(tcx),
+                mem_init_fn_cache: HashMap::new(),
+            },
         );
         transformer.add_pass(
             queries,

library/kani/src/lib.rs

@@ -123,6 +123,30 @@ pub const fn assert(cond: bool, msg: &'static str) {
     assert!(cond, "{}", msg);
 }
 
+/// Creates an assertion of the specified condition, but does not assume it afterwards.
+///
+/// # Example:
+///
+/// ```rust
+/// let x: bool = kani::any();
+/// let y = !x;
+/// kani::check(x || y, "ORing a boolean variable with its negation must be true")
+/// ```
+#[cfg(not(feature = "concrete_playback"))]
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniCheck"]
+pub const fn check(cond: bool, msg: &'static str) {
+    let _ = cond;
+    let _ = msg;
+}
+
+#[cfg(feature = "concrete_playback")]
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniCheck"]
+pub const fn check(cond: bool, msg: &'static str) {
+    assert!(cond, "{}", msg);
+}
+
 /// Creates a cover property with the specified condition and message.
 ///
 /// # Example:

library/kani/src/mem.rs

@@ -306,7 +306,7 @@ pub fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
 
 /// A helper to assert `is_initialized` to use it as a part of other predicates.
 fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
-    crate::assert(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer");
+    crate::check(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer");
     true
 }
 

library/kani_core/src/lib.rs

@@ -124,6 +124,30 @@ macro_rules! kani_intrinsics {
             assert!(cond, "{}", msg);
         }
 
+        /// Creates an assertion of the specified condition and message, but does not assume it afterwards.
+        ///
+        /// # Example:
+        ///
+        /// ```rust
+        /// let x: bool = kani::any();
+        /// let y = !x;
+        /// kani::check(x || y, "ORing a boolean variable with its negation must be true")
+        /// ```
+        #[cfg(not(feature = "concrete_playback"))]
+        #[inline(never)]
+        #[rustc_diagnostic_item = "KaniCheck"]
+        pub const fn check(cond: bool, msg: &'static str) {
+            let _ = cond;
+            let _ = msg;
+        }
+
+        #[cfg(feature = "concrete_playback")]
+        #[inline(never)]
+        #[rustc_diagnostic_item = "KaniCheck"]
+        pub const fn check(cond: bool, msg: &'static str) {
+            assert!(cond, "{}", msg);
+        }
+
         /// Creates a cover property with the specified condition and message.
         ///
         /// # Example:

library/kani_core/src/mem.rs

@@ -312,7 +312,7 @@ macro_rules! kani_mem {
 
         /// A helper to assert `is_initialized` to use it as a part of other predicates.
         fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
-            assert!(
+            $crate::check(
                 is_initialized(ptr),
                 "Undefined Behavior: Reading from an uninitialized pointer",
             );