Fix the merge

   - Support all instance types as part of the rechability analysis.
   - Skip assembly and closures for attribute checking due to rustc
     limitation.
   - Fix mir changes to the stats collector.

kani-compiler/src/kani_middle/analysis.rs

@@ -138,6 +138,7 @@ impl<'tcx> From<&Statement<'tcx>> for Key {
             | StatementKind::ConstEvalCounter
             | StatementKind::FakeRead(_)
             | StatementKind::Nop
+            | StatementKind::PlaceMention(_)
             | StatementKind::Retag(_, _)
             | StatementKind::StorageLive(_)
             | StatementKind::StorageDead(_) => Key("Ignored"),
@@ -148,11 +149,9 @@ impl<'tcx> From<&Statement<'tcx>> for Key {
 impl<'tcx> From<&Terminator<'tcx>> for Key {
     fn from(value: &Terminator<'tcx>) -> Self {
         match value.kind {
-            TerminatorKind::Abort => Key("Abort"),
             TerminatorKind::Assert { .. } => Key("Assert"),
             TerminatorKind::Call { .. } => Key("Call"),
             TerminatorKind::Drop { .. } => Key("Drop"),
-            TerminatorKind::DropAndReplace { .. } => Key("DropAndReplace"),
             TerminatorKind::GeneratorDrop => Key("GeneratorDrop"),
             TerminatorKind::Goto { .. } => Key("Goto"),
             TerminatorKind::FalseEdge { .. } => Key("FalseEdge"),
@@ -161,6 +160,7 @@ impl<'tcx> From<&Terminator<'tcx>> for Key {
             TerminatorKind::Resume => Key("Resume"),
             TerminatorKind::Return => Key("Return"),
             TerminatorKind::SwitchInt { .. } => Key("SwitchInt"),
+            TerminatorKind::Terminate => Key("Terminate"),
             TerminatorKind::Unreachable => Key("Unreachable"),
             TerminatorKind::Yield { .. } => Key("Yield"),
         }

kani-compiler/src/kani_middle/attributes.rs

@@ -8,7 +8,7 @@ use kani_metadata::{CbmcSolver, HarnessAttributes, Stub};
 use rustc_ast::{attr, AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem};
 use rustc_errors::ErrorGuaranteed;
 use rustc_hir::{def::DefKind, def_id::DefId};
-use rustc_middle::ty::{self, Instance, TyCtxt};
+use rustc_middle::ty::{self, Instance, TyCtxt, TyKind};
 use rustc_span::Span;
 use std::str::FromStr;
 use strum_macros::{AsRefStr, EnumString};
@@ -155,6 +155,11 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option<HarnessA
 ///
 /// TODO: Improve error message by printing the span of the callee instead of the definition.
 pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: DefId) {
+    if !matches!(tcx.type_of(def_id).0.kind(), TyKind::FnDef(..)) {
+        // skip closures due to an issue with rustc.
+        // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862
+        return;
+    }
     let attributes = extract_kani_attributes(tcx, def_id);
     if let Some(unstable_attrs) = attributes.get(&KaniAttributeKind::Unstable) {
         for attr in unstable_attrs {

kani-compiler/src/kani_middle/mod.rs

@@ -61,7 +61,7 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
 pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) {
     // Avoid printing the same error multiple times for different instantiations of the same item.
     let mut def_ids = HashSet::new();
-    for item in items {
+    for item in items.iter().filter(|i| matches!(i, MonoItem::Fn(..) | MonoItem::Static(..))) {
         let def_id = item.def_id();
         if !def_ids.contains(&def_id) {
             // Check if any unstable attribute was reached.

kani-compiler/src/kani_middle/reachability.rs

@@ -283,7 +283,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
             | InstanceDef::Item(..)
             | InstanceDef::ReifyShim(..)
             | InstanceDef::VTableShim(..) => true,
-            InstanceDef::ThreadLocalShim(_) | InstanceDef::FnPtrAddrShim(_, _) => todo!(),
+            InstanceDef::ThreadLocalShim(_) | InstanceDef::FnPtrAddrShim(_, _) => true,
         };
         if should_collect && should_codegen_locally(self.tcx, &instance) {
             trace!(?instance, "collect_instance");

tests/cargo-ui/unstable-attr/invalid/expected

@@ -1,8 +1,8 @@
-error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature("invalid_args")`\
+error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found\
 src/lib.rs\
 |\
-| #[kani::unstable(feature("invalid_args"))]\
-| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+| #[kani::unstable(\
+| ^^^^^^^^^^^^^^^^^^\
 |\
 = 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)

tests/cargo-ui/unstable-attr/invalid/src/lib.rs

@@ -1,6 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+//! All the unstable definitions below should fail.
+//! The expected file only contains a generic check since we trigger an ICE for debug builds and
+//! 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>")]
 pub fn missing_feature() {
     todo!()