Fix a few more issues with the std library (#3261)

- 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. Co-authored-by: Michael Tautschnig <[email protected]>
model-checking · Jun 12, 2024 · db54783 · db54783
1 parent 34b35d8
commit db54783
Show file tree

Hide file tree

Showing 14 changed files with 80 additions and 54 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/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 {

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

diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/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

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
@@ -782,10 +782,10 @@ impl<'a> UnstableAttrParseError<'a> {
         tcx.dcx()
             .struct_span_err(
                 self.attr.span,
-                format!("failed to parse `#[kani::unstable]`: {}", self.reason),
+                format!("failed to parse `#[kani::unstable_feature]`: {}", self.reason),
             )
             .with_note(format!(
-                "expected format: #[kani::unstable({}, {}, {})]",
+                "expected format: #[kani::unstable_feature({}, {}, {})]",
                 r#"feature="<IDENTIFIER>""#, r#"issue="<ISSUE>""#, r#"reason="<DESCRIPTION>""#
             ))
             .emit()

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

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

diff --git a/library/kani/src/lib.rs b/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;
diff --git a/library/kani_core/src/arbitrary.rs b/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);

diff --git a/library/kani_core/src/lib.rs b/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);
 

diff --git a/library/kani_macros/src/lib.rs b/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)
 }
 

diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/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
                         }

diff --git a/tests/cargo-ui/unstable-attr/defs/src/lib.rs b/tests/cargo-ui/unstable-attr/defs/src/lib.rs
@@ -1,13 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-#[kani::unstable(feature = "always_fails", reason = "do not enable", issue = "<link>")]
+#[kani::unstable_feature(feature = "always_fails", reason = "do not enable", issue = "<link>")]
 pub fn always_fails() {
     assert!(false, "don't call me");
 }
 
 /// We use "gen-c" since it has to be an existing feature.
-#[kani::unstable(feature = "gen-c", reason = "internal fake api", issue = "<link>")]
+#[kani::unstable_feature(feature = "gen-c", reason = "internal fake api", issue = "<link>")]
 pub fn no_op() {
     kani::cover!(true);
 }
diff --git a/tests/cargo-ui/unstable-attr/invalid/expected b/tests/cargo-ui/unstable-attr/invalid/expected
@@ -1,32 +1,32 @@
-error: failed to parse `#[kani::unstable]`: missing `feature` field\
+error: failed to parse `#[kani::unstable_feature]`: missing `feature` field\
 lib.rs
   |\
-9 | #[kani::unstable(reason = "just checking", issue = "<link>")]\
-  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+9 | #[kani::unstable_feature(reason = "just checking", issue = "<link>")]\
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
   |\
-  = note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]\
-  = note: this error originates in the attribute macro `kani::unstable` (in Nightly builds, run with -Z macro-backtrace for more info)
+  = note: expected format: #[kani::unstable_feature(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]\
+  = note: this error originates in the attribute macro `kani::unstable_feature` (in Nightly builds, run with -Z macro-backtrace for more info)
 
-error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature("invalid_args")`\
+error: failed to parse `#[kani::unstable_feature]`: expected "key = value" pair, but found `feature("invalid_args")`\
 lib.rs\
 |\
-| #[kani::unstable(feature("invalid_args"))]\
-| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+| #[kani::unstable_feature(feature("invalid_args"))]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
 |\
-   = note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]
+   = note: expected format: #[kani::unstable_feature(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]
 
-error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature`\
+error: failed to parse `#[kani::unstable_feature]`: expected "key = value" pair, but found `feature`\
 lib.rs\
 |\
-| #[kani::unstable(feature, issue)]\
-| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+| #[kani::unstable_feature(feature, issue)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
 |\
-   = note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]
+   = note: expected format: #[kani::unstable_feature(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]
 
-error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `1010`\
+error: failed to parse `#[kani::unstable_feature]`: expected "key = value" pair, but found `1010`\
 lib.rs\
 |\
-| #[kani::unstable(1010)]\
-| ^^^^^^^^^^^^^^^^^^^^^^^\
+| #[kani::unstable_feature(1010)]\
+| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
 |\
-   = note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]
+   = note: expected format: #[kani::unstable_feature(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]
diff --git a/tests/cargo-ui/unstable-attr/invalid/src/lib.rs b/tests/cargo-ui/unstable-attr/invalid/src/lib.rs
@@ -6,18 +6,18 @@
 //! we don't guarantee the order that these will be evaluated.
 //! TODO: We should break down this test to ensure all of these fail.
 
-#[kani::unstable(reason = "just checking", issue = "<link>")]
+#[kani::unstable_feature(reason = "just checking", issue = "<link>")]
 pub fn missing_feature() {
     todo!()
 }
 
-#[kani::unstable(feature("invalid_args"))]
+#[kani::unstable_feature(feature("invalid_args"))]
 pub fn invalid_fn_style() {}
 
-#[kani::unstable(feature, issue)]
+#[kani::unstable_feature(feature, issue)]
 pub fn invalid_list() {}
 
-#[kani::unstable(1010)]
+#[kani::unstable_feature(1010)]
 pub fn invalid_argument() {}
 
 #[kani::proof]