Merge branch 'main' into update-toolchain-02-11

model-checking · Feb 21, 2025 · 3f2322e · 3f2322e
2 parents 2c09c1c + 006e5da
commit 3f2322e
Show file tree

Hide file tree

Showing 57 changed files with 447 additions and 278 deletions.
diff --git a/Cargo.lock b/Cargo.lock
@@ -230,9 +230,9 @@ dependencies = [
 
 [[package]]
 name = "cc"
-version = "1.2.13"
+version = "1.2.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c7777341816418c02e033934a09f20dc0ccaf65a5201ef8a450ae0105a573fda"
+checksum = "0c3d1b2e905a3a7b00a6141adb0e4c0bb941d11caf55349d863942a1cc44e3c9"
 dependencies = [
  "shlex",
 ]
@@ -282,19 +282,19 @@ dependencies = [
 
 [[package]]
 name = "clap"
-version = "4.5.28"
+version = "4.5.29"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3e77c3243bd94243c03672cb5154667347c457ca271254724f9f393aee1c05ff"
+checksum = "8acebd8ad879283633b343856142139f2da2317c96b05b4dd6181c61e2480184"
 dependencies = [
  "clap_builder",
  "clap_derive",
 ]
 
 [[package]]
 name = "clap_builder"
-version = "4.5.27"
+version = "4.5.29"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1b26884eb4b57140e4d2d93652abfa49498b938b3c9179f9fc487b0acc3edad7"
+checksum = "f6ba32cbda51c7e1dfd49acc1457ba1a7dec5b64fe360e828acb13ca8dc9c2f9"
 dependencies = [
  "anstream",
  "anstyle",
@@ -471,9 +471,9 @@ dependencies = [
 
 [[package]]
 name = "csv-core"
-version = "0.1.11"
+version = "0.1.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5efa2b3d7902f4b634a20cae3c9c4e6209dc4779feb6863329607560143efa70"
+checksum = "7d02f3b0da4c6504f86e9cd789d8dbafab48c2321be74e9987593de5a894d93d"
 dependencies = [
  "memchr",
 ]
@@ -600,9 +600,9 @@ dependencies = [
 
 [[package]]
 name = "equivalent"
-version = "1.0.1"
+version = "1.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5"
+checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f"
 
 [[package]]
 name = "errno"
@@ -1004,9 +1004,9 @@ checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a"
 
 [[package]]
 name = "miniz_oxide"
-version = "0.8.3"
+version = "0.8.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b8402cab7aefae129c6977bb0ff1b8fd9a04eb5b51efc50a70bea51cda0c7924"
+checksum = "b3b1c9bd4fe1f0f8b387f6eb9eb3b4a1aa26185e5750efb9140301703f62cd1b"
 dependencies = [
  "adler2",
 ]
@@ -1303,9 +1303,9 @@ dependencies = [
 
 [[package]]
 name = "psm"
-version = "0.1.24"
+version = "0.1.25"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "200b9ff220857e53e184257720a14553b2f4aa02577d2ed9842d45d4b9654810"
+checksum = "f58e5423e24c18cc840e1c98370b3993c6649cd1678b4d24318bcf0a083cbe88"
 dependencies = [
  "cc",
 ]
@@ -1613,15 +1613,15 @@ dependencies = [
 
 [[package]]
 name = "smallvec"
-version = "1.13.2"
+version = "1.14.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
+checksum = "7fcf8323ef1faaee30a44a340193b1ac6814fd9b7b4e88e9d4519a3e4abe1cfd"
 
 [[package]]
 name = "stacker"
-version = "0.1.17"
+version = "0.1.18"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "799c883d55abdb5e98af1a7b3f23b9b6de8ecada0ecac058672d7635eb48ca7b"
+checksum = "1d08feb8f695b465baed819b03c128dc23f57a694510ab1f06c77f763975685e"
 dependencies = [
  "cc",
  "cfg-if",
@@ -1697,9 +1697,9 @@ checksum = "f764005d11ee5f36500a149ace24e00e3da98b0158b3e2d53a7495660d3f4d60"
 
 [[package]]
 name = "tempfile"
-version = "3.16.0"
+version = "3.17.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "38c246215d7d24f48ae091a2902398798e05d978b24315d6efbc00ede9a8bb91"
+checksum = "a40f762a77d2afa88c2d919489e390a12bdd261ed568e60cfa7e48d4e20f0d33"
 dependencies = [
  "cfg-if",
  "fastrand",
@@ -1845,9 +1845,9 @@ dependencies = [
 
 [[package]]
 name = "toml_edit"
-version = "0.22.23"
+version = "0.22.24"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "02a8b472d1a3d7c18e2d61a489aee3453fd9031c33e4f55bd533f4a7adca1bee"
+checksum = "17b4795ff5edd201c7cd6dca065ae59972ce77d1b80fa0a84d94950ece7d1474"
 dependencies = [
  "indexmap",
  "serde",
@@ -2193,9 +2193,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"
 
 [[package]]
 name = "winnow"
-version = "0.7.1"
+version = "0.7.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "86e376c75f4f43f44db463cf729e0d3acbf954d13e22c51e26e4c264b4ab545f"
+checksum = "59690dea168f2198d1a3b0cac23b8063efcd11012f10ae4698f284808c8ef603"
 dependencies = [
  "memchr",
 ]

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/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,
                         ),

diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/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)),

diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/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")]

diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/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())
     }
 }