Stub panics during MIR transformation

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

@@ -326,7 +326,12 @@ struct Panic;
 impl GotocHook for Panic {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
         let def_id = rustc_internal::internal(tcx, instance.def.def_id());
-        Some(def_id) == tcx.lang_items().panic_fn()
+        let kani_tool_attr = attributes::fn_marker(instance.def);
+
+        // we check the attributes to make sure this hook applies to
+        // panic functions we've stubbed too
+        kani_tool_attr.is_some_and(|kani| kani.contains("PanicStub"))
+            || Some(def_id) == tcx.lang_items().panic_fn()
             || tcx.has_attr(def_id, rustc_span::sym::rustc_const_panic_str)
             || Some(def_id) == tcx.lang_items().panic_fmt()
             || Some(def_id) == tcx.lang_items().begin_panic_fn()

kani-compiler/src/kani_middle/kani_functions.rs

@@ -99,6 +99,8 @@ pub enum KaniModel {
     SetSliceChunkPtrInitialized,
     #[strum(serialize = "SetSlicePtrInitializedModel")]
     SetSlicePtrInitialized,
+    #[strum(serialize = "PanicStub")]
+    PanicStub,
     #[strum(serialize = "SetStrPtrInitializedModel")]
     SetStrPtrInitialized,
     #[strum(serialize = "SizeOfDynObjectModel")]

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

@@ -52,15 +52,24 @@ impl TransformPass for RustcIntrinsicsPass {
     /// For every unsafe dereference or a transmute operation, we check all values are valid.
     fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
         debug!(function=?instance.name(), "transform");
+
         let mut new_body = MutableBody::from(body);
         let mut visitor =
-            ReplaceIntrinsicCallVisitor::new(&self.models, new_body.locals().to_vec());
+            ReplaceIntrinsicCallVisitor::new(&self.models, new_body.locals().to_vec(), tcx);
         visitor.visit_body(&mut new_body);
         let changed = self.replace_lowered_intrinsics(tcx, &mut new_body);
         (visitor.changed || changed, new_body.into())
     }
 }
 
+fn is_panic_function(tcx: &TyCtxt, def_id: rustc_smir::stable_mir::DefId) -> bool {
+    let def_id = rustc_internal::internal(*tcx, def_id);
+    Some(def_id) == tcx.lang_items().panic_fn()
+        || tcx.has_attr(def_id, rustc_span::sym::rustc_const_panic_str)
+        || Some(def_id) == tcx.lang_items().panic_fmt()
+        || Some(def_id) == tcx.lang_items().begin_panic_fn()
+}
+
 impl RustcIntrinsicsPass {
     pub fn new(queries: &QueryDb) -> Self {
         let models = queries
@@ -132,19 +141,24 @@ impl RustcIntrinsicsPass {
     }
 }
 
-struct ReplaceIntrinsicCallVisitor<'a> {
+struct ReplaceIntrinsicCallVisitor<'a, 'tcx> {
     models: &'a HashMap<KaniModel, FnDef>,
     locals: Vec<LocalDecl>,
+    tcx: TyCtxt<'tcx>,
     changed: bool,
 }
 
-impl<'a> ReplaceIntrinsicCallVisitor<'a> {
-    fn new(models: &'a HashMap<KaniModel, FnDef>, locals: Vec<LocalDecl>) -> Self {
-        ReplaceIntrinsicCallVisitor { models, locals, changed: false }
+impl<'a, 'tcx> ReplaceIntrinsicCallVisitor<'a, 'tcx> {
+    fn new(
+        models: &'a HashMap<KaniModel, FnDef>,
+        locals: Vec<LocalDecl>,
+        tcx: TyCtxt<'tcx>,
+    ) -> Self {
+        ReplaceIntrinsicCallVisitor { models, locals, changed: false, tcx }
     }
 }
 
-impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> {
+impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_, '_> {
     /// Replace the terminator for some rustc's intrinsics.
     ///
     /// In some cases, we replace a function call to a rustc intrinsic by a call to the
@@ -159,27 +173,40 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> {
         if let TerminatorKind::Call { func, .. } = &mut term.kind
             && let TyKind::RigidTy(RigidTy::FnDef(def, args)) =
                 func.ty(&self.locals).unwrap().kind()
-            && def.is_intrinsic()
         {
-            let instance = Instance::resolve(def, &args).unwrap();
-            let intrinsic = Intrinsic::from_instance(&instance);
-            debug!(?intrinsic, "handle_terminator");
-            let model = match intrinsic {
-                Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal],
-                Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal],
-                Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom],
-                Intrinsic::PtrOffsetFromUnsigned => self.models[&KaniModel::PtrOffsetFromUnsigned],
-                // The rest is handled in codegen.
-                _ => {
-                    return self.super_terminator(term);
-                }
-            };
-            let new_instance = Instance::resolve(model, &args).unwrap();
-            let literal = MirConst::try_new_zero_sized(new_instance.ty()).unwrap();
-            let span = term.span;
-            let new_func = ConstOperand { span, user_ty: None, const_: literal };
-            *func = Operand::Constant(new_func);
-            self.changed = true;
+            if def.is_intrinsic() {
+                let instance = Instance::resolve(def, &args).unwrap();
+                let intrinsic = Intrinsic::from_instance(&instance);
+                debug!(?intrinsic, "handle_terminator");
+                let model = match intrinsic {
+                    Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal],
+                    Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal],
+                    Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom],
+                    Intrinsic::PtrOffsetFromUnsigned => {
+                        self.models[&KaniModel::PtrOffsetFromUnsigned]
+                    }
+                    // The rest is handled in codegen.
+                    _ => {
+                        return self.super_terminator(term);
+                    }
+                };
+                let new_instance = Instance::resolve(model, &args).unwrap();
+                let literal = MirConst::try_new_zero_sized(new_instance.ty()).unwrap();
+                let span = term.span;
+                let new_func = ConstOperand { span, user_ty: None, const_: literal };
+                *func = Operand::Constant(new_func);
+                self.changed = true;
+            } else if is_panic_function(&self.tcx, def.0) {
+                // if we find a panic function, replace it with our stub
+                let new_instance =
+                    Instance::resolve(self.models[&KaniModel::PanicStub], &args).unwrap();
+
+                let literal = MirConst::try_new_zero_sized(new_instance.ty()).unwrap();
+                let span = term.span;
+                let new_func = ConstOperand { span, user_ty: None, const_: literal };
+                *func = Operand::Constant(new_func);
+                self.changed = true;
+            }
         }
         self.super_terminator(term);
     }

library/kani_core/src/models.rs

@@ -32,6 +32,13 @@ macro_rules! generate_models {
                 }
             }
 
+            #[kanitool::fn_marker = "PanicStub"]
+            pub fn panic_stub(t: &str) -> ! {
+                // Using an infinite loop here to have the function return the never (`!`) type.
+                // We could also use `exit()` / `abort()` but both require depending on std::process.
+                loop {}
+            }
+
             #[kanitool::fn_marker = "AlignOfValRawModel"]
             pub fn align_of_val_raw<T: ?Sized>(ptr: *const T) -> usize {
                 if let Some(size) = kani::mem::checked_align_of_raw(ptr) {