Adjust PropertyClass of assertions to identify UB (#3860)

Anything listed as undefined behavior (UB) at
https://doc.rust-lang.org/reference/behavior-considered-undefined.html
must also be considered UB by Kani and should not pass under
`should_fail`. In preparation of this PR, all occurrences of
`PropertyClass` in the code base were audited and, where necessary,
adjusted.

Also, all uses of `kani::assert` were audited to confirm or adjust them.
This resulted in first-time use of the `UnsupportedCheck` hook, which
implied fixes to its implementation.

Resolves: #3571

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: Carolyn Zech <cmzech@amazon.com>

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

@@ -251,19 +251,37 @@ impl GotocCtx<'_> {
                     if *expected { r } else { Expr::not(r) }
                 };
 
-                let msg = if let AssertMessage::BoundsCheck { .. } = msg {
-                    // For bounds check the following panic message is generated at runtime:
-                    // "index out of bounds: the length is {len} but the index is {index}",
-                    // but CBMC only accepts static messages so we don't add values to the message.
-                    "index out of bounds: the length is less than or equal to the given index"
-                } else if let AssertMessage::MisalignedPointerDereference { .. } = msg {
-                    // Misaligned pointer dereference check messages is also a runtime messages.
-                    // Generate a generic one here.
-                    "misaligned pointer dereference: address must be a multiple of its type's \
-                    alignment"
-                } else {
+                let (msg, property_class) = match msg {
+                    AssertMessage::BoundsCheck { .. } => {
+                        // For bounds check the following panic message is generated at runtime:
+                        // "index out of bounds: the length is {len} but the index is {index}",
+                        // but CBMC only accepts static messages so we don't add values to the message.
+                        (
+                            "index out of bounds: the length is less than or equal to the given index",
+                            PropertyClass::Assertion,
+                        )
+                    }
+                    AssertMessage::MisalignedPointerDereference { .. } => {
+                        // Misaligned pointer dereference check messages is also a runtime messages.
+                        // Generate a generic one here.
+                        (
+                            "misaligned pointer dereference: address must be a multiple of its type's \
+                    alignment",
+                            PropertyClass::SafetyCheck,
+                        )
+                    }
                     // For all other assert kind we can get the static message.
-                    msg.description().unwrap()
+                    AssertMessage::NullPointerDereference => {
+                        (msg.description().unwrap(), PropertyClass::SafetyCheck)
+                    }
+                    AssertMessage::Overflow { .. }
+                    | AssertMessage::OverflowNeg { .. }
+                    | AssertMessage::DivisionByZero { .. }
+                    | AssertMessage::RemainderByZero { .. }
+                    | AssertMessage::ResumedAfterReturn { .. }
+                    | AssertMessage::ResumedAfterPanic { .. } => {
+                        (msg.description().unwrap(), PropertyClass::Assertion)
+                    }
                 };
 
                 let (msg_str, reach_stmt) =
@@ -274,7 +292,7 @@ impl GotocCtx<'_> {
                         reach_stmt,
                         self.codegen_assert_assume(
                             cond.cast_to(Type::bool()),
-                            PropertyClass::Assertion,
+                            property_class,
                             &msg_str,
                             loc,
                         ),

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

@@ -151,6 +151,43 @@ impl GotocHook for UnsupportedCheck {
         unreachable!("{UNEXPECTED_CALL}")
     }
 
+    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(), 1);
+        let msg = fargs.pop().unwrap();
+        let msg = gcx.extract_const_message(&msg).unwrap();
+        let caller_loc = gcx.codegen_caller_span_stable(span);
+        if let Some(target) = target {
+            Stmt::block(
+                vec![
+                    gcx.codegen_assert_assume_false(
+                        PropertyClass::UnsupportedConstruct,
+                        &msg,
+                        caller_loc,
+                    ),
+                    Stmt::goto(bb_label(target), caller_loc),
+                ],
+                caller_loc,
+            )
+        } else {
+            gcx.codegen_assert_assume_false(PropertyClass::UnsupportedConstruct, &msg, caller_loc)
+        }
+    }
+}
+
+struct SafetyCheck;
+impl GotocHook for SafetyCheck {
+    fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
+        unreachable!("{UNEXPECTED_CALL}")
+    }
+
     fn handle(
         &self,
         gcx: &mut GotocCtx,
@@ -168,21 +205,16 @@ impl GotocHook for UnsupportedCheck {
         let caller_loc = gcx.codegen_caller_span_stable(span);
         Stmt::block(
             vec![
-                gcx.codegen_assert_assume(
-                    cond,
-                    PropertyClass::UnsupportedConstruct,
-                    &msg,
-                    caller_loc,
-                ),
+                gcx.codegen_assert_assume(cond, PropertyClass::SafetyCheck, &msg, caller_loc),
                 Stmt::goto(bb_label(target), caller_loc),
             ],
             caller_loc,
         )
     }
 }
 
-struct SafetyCheck;
-impl GotocHook for SafetyCheck {
+struct SafetyCheckNoAssume;
+impl GotocHook for SafetyCheckNoAssume {
     fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
         unreachable!("{UNEXPECTED_CALL}")
     }
@@ -204,7 +236,7 @@ impl GotocHook for SafetyCheck {
         let caller_loc = gcx.codegen_caller_span_stable(span);
         Stmt::block(
             vec![
-                gcx.codegen_assert_assume(cond, PropertyClass::SafetyCheck, &msg, caller_loc),
+                gcx.codegen_assert(cond, PropertyClass::SafetyCheck, &msg, caller_loc),
                 Stmt::goto(bb_label(target), caller_loc),
             ],
             caller_loc,
@@ -738,6 +770,7 @@ pub fn fn_hooks() -> GotocHooks {
         (KaniHook::Cover, Rc::new(Cover)),
         (KaniHook::AnyRaw, Rc::new(Nondet)),
         (KaniHook::SafetyCheck, Rc::new(SafetyCheck)),
+        (KaniHook::SafetyCheckNoAssume, Rc::new(SafetyCheckNoAssume)),
         (KaniHook::IsAllocated, Rc::new(IsAllocated)),
         (KaniHook::PointerObject, Rc::new(PointerObject)),
         (KaniHook::PointerOffset, Rc::new(PointerOffset)),

kani-compiler/src/kani_middle/kani_functions.rs

@@ -148,6 +148,8 @@ pub enum KaniHook {
     PointerOffset,
     #[strum(serialize = "SafetyCheckHook")]
     SafetyCheck,
+    #[strum(serialize = "SafetyCheckNoAssumeHook")]
+    SafetyCheckNoAssume,
     #[strum(serialize = "UnsupportedCheckHook")]
     UnsupportedCheck,
     #[strum(serialize = "UntrackedDerefHook")]

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

@@ -181,23 +181,31 @@ impl MutableBody {
         check_type: &CheckType,
         source: &mut SourceInstruction,
         position: InsertPosition,
-        value: Local,
+        value: Option<Local>,
         msg: &str,
     ) {
-        assert_eq!(
-            self.locals[value].ty,
-            Ty::bool_ty(),
-            "Expected boolean value as the assert input"
-        );
         let new_bb = self.blocks.len();
         let span = source.span(&self.blocks);
-        let CheckType::Assert(assert_fn) = check_type;
+        let msg_op = self.new_str_operand(msg, span);
+        let (assert_fn, args) = match check_type {
+            CheckType::SafetyCheck(assert_fn) | CheckType::SafetyCheckNoAssume(assert_fn) => {
+                assert_eq!(
+                    self.locals[value.unwrap()].ty,
+                    Ty::bool_ty(),
+                    "Expected boolean value as the assert input"
+                );
+                (assert_fn, vec![Operand::Move(Place::from(value.unwrap())), msg_op])
+            }
+            CheckType::UnsupportedCheck(assert_fn) => {
+                assert!(value.is_none());
+                (assert_fn, vec![msg_op])
+            }
+        };
         let assert_op =
             Operand::Copy(Place::from(self.new_local(assert_fn.ty(), span, Mutability::Not)));
-        let msg_op = self.new_str_operand(msg, span);
         let kind = TerminatorKind::Call {
             func: assert_op,
-            args: vec![Operand::Move(Place::from(value)), msg_op],
+            args,
             destination: Place {
                 local: self.new_local(Ty::new_tuple(&[]), span, Mutability::Not),
                 projection: vec![],
@@ -441,30 +449,35 @@ impl MutableBody {
     }
 }
 
-// TODO: Remove this enum, since we now only support kani's assert.
 #[derive(Clone, Debug)]
 pub enum CheckType {
-    /// This is used by default when the `kani` crate is available.
-    Assert(Instance),
+    SafetyCheck(Instance),
+    SafetyCheckNoAssume(Instance),
+    UnsupportedCheck(Instance),
 }
 
 impl CheckType {
-    /// 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.
-    pub fn new_assert_assume(queries: &QueryDb) -> CheckType {
-        let fn_def = queries.kani_functions()[&KaniHook::Assert.into()];
-        CheckType::Assert(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap())
-    }
-
-    /// 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(queries: &QueryDb) -> CheckType {
-        let fn_def = queries.kani_functions()[&KaniHook::Check.into()];
-        CheckType::Assert(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap())
+    /// This will create the type of safety 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.
+    pub fn new_safety_check_assert_assume(queries: &QueryDb) -> CheckType {
+        let fn_def = queries.kani_functions()[&KaniHook::SafetyCheck.into()];
+        CheckType::SafetyCheck(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap())
+    }
+
+    /// This will create the type of safety check that is available in the current crate, attempting
+    /// to create a check that generates an assertion, but not following by an assumption.
+    pub fn new_safety_check_assert_no_assume(queries: &QueryDb) -> CheckType {
+        let fn_def = queries.kani_functions()[&KaniHook::SafetyCheckNoAssume.into()];
+        CheckType::SafetyCheckNoAssume(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap())
+    }
+
+    /// This will create the type of operation-unsupported 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.
+    pub fn new_unsupported_check_assert_assume_false(queries: &QueryDb) -> CheckType {
+        let fn_def = queries.kani_functions()[&KaniHook::UnsupportedCheck.into()];
+        CheckType::UnsupportedCheck(Instance::resolve(fn_def, &GenericArgs(vec![])).unwrap())
     }
 }
 

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

@@ -33,13 +33,22 @@ mod instrumentation_visitor;
 
 #[derive(Debug)]
 pub struct DelayedUbPass {
-    pub check_type: CheckType,
+    pub safety_check_type: CheckType,
+    pub unsupported_check_type: CheckType,
     pub mem_init_fn_cache: HashMap<KaniFunction, FnDef>,
 }
 
 impl DelayedUbPass {
-    pub fn new(check_type: CheckType, queries: &QueryDb) -> Self {
-        Self { check_type, mem_init_fn_cache: queries.kani_functions().clone() }
+    pub fn new(
+        safety_check_type: CheckType,
+        unsupported_check_type: CheckType,
+        queries: &QueryDb,
+    ) -> Self {
+        Self {
+            safety_check_type,
+            unsupported_check_type,
+            mem_init_fn_cache: queries.kani_functions().clone(),
+        }
     }
 }
 
@@ -122,7 +131,8 @@ impl GlobalPass for DelayedUbPass {
                 let (instrumentation_added, body) = UninitInstrumenter::run(
                     body,
                     instance,
-                    self.check_type.clone(),
+                    self.safety_check_type.clone(),
+                    self.unsupported_check_type.clone(),
                     &mut self.mem_init_fn_cache,
                     target_finder,
                 );