Fix a few more issues with the std library

  - Enable Kani to use fallback fn body for intrinsics, so they can
    be verified.
    - Until <rust-lang/project-stable-mir#79>
      is implemented, we have to check has_body and must_be_overridden
  - Export all kani_macro definitions. Rename `unstable` to avoid
    conflict with the Rust standard library one.
  - Dump stable mir body since transformations are made at that level.
    - I just did this as I was debugging things.

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

@@ -614,7 +614,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Ensure that the given instance is in the symbol table, returning the symbol.
     fn codegen_func_symbol(&mut self, instance: Instance) -> &Symbol {
-        let sym = if instance.is_foreign_item() {
+        let sym = if instance.is_foreign_item() && !instance.has_body() {
             // Get the symbol that represents a foreign instance.
             self.codegen_foreign_fn(instance)
         } else {

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

@@ -518,13 +518,21 @@ impl<'tcx> GotocCtx<'tcx> {
         if let Some(instance) = instance_opt
             && matches!(instance.kind, InstanceKind::Intrinsic)
         {
-            return self.codegen_funcall_of_intrinsic(
-                instance,
-                &args,
-                &destination,
-                target.map(|bb| bb),
-                span,
-            );
+            let TyKind::RigidTy(RigidTy::FnDef(def, _)) = instance.ty().kind() else {
+                unreachable!("Expected function type for intrinsic: {instance:?}")
+            };
+            // The compiler is currently transitioning how to handle intrinsic fallback body.
+            // Until https://github.com/rust-lang/project-stable-mir/issues/79 is implemented
+            // we have to check `must_be_overridden` and `has_body`.
+            if def.as_intrinsic().unwrap().must_be_overridden() || !instance.has_body() {
+                return self.codegen_funcall_of_intrinsic(
+                    instance,
+                    &args,
+                    &destination,
+                    target.map(|bb| bb),
+                    span,
+                );
+            }
         }
 
         let loc = self.codegen_span_stable(span);

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -93,7 +93,7 @@ impl GotocCodegenBackend {
             || collect_reachable_items(tcx, &mut transformer, starting_items),
             "codegen reachability analysis",
         );
-        dump_mir_items(tcx, &items, &symtab_goto.with_extension("kani.mir"));
+        dump_mir_items(tcx, &mut transformer, &items, &symtab_goto.with_extension("kani.mir"));
 
         // Follow rustc naming convention (cx is abbrev for context).
         // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions

kani-compiler/src/kani_middle/mod.rs

@@ -6,9 +6,9 @@
 use std::collections::HashSet;
 use std::path::Path;
 
+use crate::kani_middle::transform::BodyTransformation;
 use crate::kani_queries::QueryDb;
 use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE};
-use rustc_middle::mir::write_mir_pretty;
 use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
     FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError,
@@ -21,9 +21,9 @@ use rustc_span::source_map::respan;
 use rustc_span::Span;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
-use stable_mir::mir::mono::{InstanceKind, MonoItem};
+use stable_mir::mir::mono::{Instance, MonoItem};
 use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, TyKind};
-use stable_mir::{CrateDef, DefId};
+use stable_mir::CrateDef;
 use std::fs::File;
 use std::io::BufWriter;
 use std::io::Write;
@@ -93,17 +93,19 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
 }
 
 /// Print MIR for the reachable items if the `--emit mir` option was provided to rustc.
-pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) {
+pub fn dump_mir_items(
+    tcx: TyCtxt,
+    transformer: &mut BodyTransformation,
+    items: &[MonoItem],
+    output: &Path,
+) {
     /// Convert MonoItem into a DefId.
     /// Skip stuff that we cannot generate the MIR items.
-    fn visible_item(item: &MonoItem) -> Option<(MonoItem, DefId)> {
+    fn get_instance(item: &MonoItem) -> Option<Instance> {
         match item {
             // Exclude FnShims and others that cannot be dumped.
-            MonoItem::Fn(instance) if matches!(instance.kind, InstanceKind::Item) => {
-                Some((item.clone(), instance.def.def_id()))
-            }
-            MonoItem::Fn(..) => None,
-            MonoItem::Static(def) => Some((item.clone(), def.def_id())),
+            MonoItem::Fn(instance) => Some(*instance),
+            MonoItem::Static(def) => Some((*def).into()),
             MonoItem::GlobalAsm(_) => None,
         }
     }
@@ -114,10 +116,10 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) {
         let mut writer = BufWriter::new(out_file);
 
         // For each def_id, dump their MIR
-        for (item, def_id) in items.iter().filter_map(visible_item) {
-            writeln!(writer, "// Item: {item:?}").unwrap();
-            write_mir_pretty(tcx, Some(rustc_internal::internal(tcx, def_id)), &mut writer)
-                .unwrap();
+        for instance in items.iter().filter_map(get_instance) {
+            writeln!(writer, "// Item: {} ({})", instance.name(), instance.mangled_name()).unwrap();
+            let body = transformer.body(tcx, instance);
+            let _ = body.dump(&mut writer, &instance.name());
         }
     }
 }

kani-compiler/src/kani_middle/reachability.rs

@@ -262,11 +262,22 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
     /// Collect an instance depending on how it is used (invoked directly or via fn_ptr).
     fn collect_instance(&mut self, instance: Instance, is_direct_call: bool) {
         let should_collect = match instance.kind {
-            InstanceKind::Virtual { .. } | InstanceKind::Intrinsic => {
+            InstanceKind::Virtual { .. } => {
                 // Instance definition has no body.
                 assert!(is_direct_call, "Expected direct call {instance:?}");
                 false
             }
+            InstanceKind::Intrinsic => {
+                // Intrinsics may have a fallback body.
+                assert!(is_direct_call, "Expected direct call {instance:?}");
+                let TyKind::RigidTy(RigidTy::FnDef(def, _)) = instance.ty().kind() else {
+                    unreachable!("Expected function type for intrinsic: {instance:?}")
+                };
+                // The compiler is currently transitioning how to handle intrinsic fallback body.
+                // Until https://github.com/rust-lang/project-stable-mir/issues/79 is implemented
+                // we have to check `must_be_overridden` and `has_body`.
+                !def.as_intrinsic().unwrap().must_be_overridden() && instance.has_body()
+            }
             InstanceKind::Shim | InstanceKind::Item => true,
         };
         if should_collect && should_codegen_locally(&instance) {

library/kani/src/lib.rs

@@ -323,4 +323,6 @@ pub use core::assert as __kani__workaround_core_assert;
 // Kani proc macros must be in a separate crate
 pub use kani_macros::*;
 
+pub(crate) use kani_macros::unstable_feature as unstable;
+
 pub mod contracts;

library/kani_core/src/arbitrary.rs

@@ -72,6 +72,8 @@ macro_rules! generate_arbitrary {
         }
 
         // Generate trivial arbitrary values
+        trivial_arbitrary!(());
+
         trivial_arbitrary!(u8);
         trivial_arbitrary!(u16);
         trivial_arbitrary!(u32);

library/kani_core/src/lib.rs

@@ -35,9 +35,8 @@ macro_rules! kani_lib {
         #[cfg(kani)]
         #[unstable(feature = "kani", issue = "none")]
         pub mod kani {
-            pub use kani_core::{
-                ensures, modifies, proof, proof_for_contract, requires, should_panic,
-            };
+            // We need to list them all today because there is conflict with unstable.
+            pub use kani_core::*;
             kani_core::kani_intrinsics!(core);
             kani_core::generate_arbitrary!(core);
 

library/kani_macros/src/lib.rs

@@ -96,7 +96,7 @@ pub fn solver(attr: TokenStream, item: TokenStream) -> TokenStream {
 /// See https://model-checking.github.io/kani/rfc/rfcs/0006-unstable-api.html for more details.
 #[doc(hidden)]
 #[proc_macro_attribute]
-pub fn unstable(attr: TokenStream, item: TokenStream) -> TokenStream {
+pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream {
     attr_impl::unstable(attr, item)
 }
 

library/kani_macros/src/sysroot/contracts/shared.rs

@@ -73,7 +73,9 @@ impl<'a> ContractConditionsHandler<'a> {
                     .filter(|attr| {
                         if let Some(ident) = attr.path().get_ident() {
                             let name = ident.to_string();
-                            !name.starts_with("rustc") && !(name == "stable")
+                            !name.starts_with("rustc")
+                                && !(name == "stable")
+                                && !(name == "unstable")
                         } else {
                             true
                         }