Fix crash when using public fns reachability (#2065)

Filter roots to only collect public functions. Also, make the collection function more robust and to account for associated functions.

Author: celinval

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -48,7 +48,7 @@ use std::process::Command;
 use std::rc::Rc;
 use std::time::Instant;
 use tempfile::Builder as TempFileBuilder;
-use tracing::{debug, error, info, warn};
+use tracing::{debug, error, info};
 
 #[derive(Clone)]
 pub struct GotocCodegenBackend {
@@ -310,10 +310,10 @@ fn check_crate_items(gcx: &GotocCtx) {
                 );
                 tcx.sess.err(&error_msg);
             } else {
-                warn!(
+                tcx.sess.warn(format!(
                     "Ignoring global ASM in crate {}. Verification results may be impacted.",
                     gcx.short_crate_name()
-                );
+                ));
             }
         }
     }
@@ -371,7 +371,7 @@ fn codegen_results(
 fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec<MonoItem<'tcx>> {
     let tcx = gcx.tcx;
     let reach = gcx.queries.get_reachability_analysis();
-    debug!(?reach, "starting_points");
+    debug!(?reach, "collect_codegen_items");
     match reach {
         ReachabilityType::Legacy => {
             // Use rustc monomorphizer to retrieve items to codegen.
@@ -399,7 +399,8 @@ fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec<MonoItem<'tcx>> {
         ReachabilityType::PubFns => {
             let entry_fn = tcx.entry_fn(()).map(|(id, _)| id);
             let local_reachable = filter_crate_items(tcx, |_, def_id| {
-                tcx.is_reachable_non_generic(def_id) || entry_fn == Some(def_id)
+                (tcx.is_reachable_non_generic(def_id) && tcx.def_kind(def_id).is_fn_like())
+                    || entry_fn == Some(def_id)
             });
             collect_reachable_items(tcx, &local_reachable).into_iter().collect()
         }

kani-compiler/src/kani_middle/reachability.rs

@@ -18,7 +18,9 @@ use tracing::{debug, debug_span, trace, warn};
 use rustc_data_structures::fingerprint::Fingerprint;
 use rustc_data_structures::fx::FxHashSet;
 use rustc_data_structures::stable_hasher::{HashStable, StableHasher};
+use rustc_hir::def::DefKind;
 use rustc_hir::def_id::DefId;
+use rustc_hir::ItemId;
 use rustc_middle::mir::interpret::{AllocId, ConstValue, ErrorHandled, GlobalAlloc, Scalar};
 use rustc_middle::mir::mono::MonoItem;
 use rustc_middle::mir::visit::Visitor as MirVisitor;
@@ -57,18 +59,35 @@ pub fn collect_reachable_items<'tcx>(
 }
 
 /// Collect all (top-level) items in the crate that matches the given predicate.
+/// An item can only be a root if they are: non-generic Fn / Static / GlobalASM
 pub fn filter_crate_items<F>(tcx: TyCtxt, predicate: F) -> Vec<MonoItem>
 where
-    F: FnMut(TyCtxt, DefId) -> bool,
+    F: Fn(TyCtxt, DefId) -> bool,
 {
-    let mut filter = predicate;
-    tcx.hir_crate_items(())
-        .items()
-        .filter_map(|hir_id| {
-            let def_id = hir_id.owner_id.def_id.to_def_id();
-            filter(tcx, def_id).then(|| MonoItem::Fn(Instance::mono(tcx, def_id)))
-        })
-        .collect()
+    let crate_items = tcx.hir_crate_items(());
+    // Filter regular items.
+    let root_items = crate_items.items().filter_map(|item| {
+        let def_id = item.owner_id.def_id.to_def_id();
+        if !is_generic(tcx, def_id) && predicate(tcx, def_id) {
+            to_mono_root(tcx, item, def_id)
+        } else {
+            None
+        }
+    });
+
+    // Filter items from implementation blocks.
+    let impl_items = crate_items.impl_items().filter_map(|impl_item| {
+        let def_id = impl_item.owner_id.def_id.to_def_id();
+        if matches!(tcx.def_kind(def_id), DefKind::AssocFn)
+            && !is_generic(tcx, def_id)
+            && predicate(tcx, def_id)
+        {
+            Some(MonoItem::Fn(Instance::mono(tcx, def_id)))
+        } else {
+            None
+        }
+    });
+    root_items.chain(impl_items).collect()
 }
 
 /// Use a predicate to find `const` declarations, then extract all closures from those declarations
@@ -96,6 +115,24 @@ where
     roots
 }
 
+fn is_generic(tcx: TyCtxt, def_id: DefId) -> bool {
+    let generics = tcx.generics_of(def_id);
+    generics.requires_monomorphization(tcx)
+}
+
+fn to_mono_root(tcx: TyCtxt, item_id: ItemId, def_id: DefId) -> Option<MonoItem> {
+    let kind = tcx.def_kind(def_id);
+    match kind {
+        DefKind::Static(..) => Some(MonoItem::Static(def_id)),
+        DefKind::Fn => Some(MonoItem::Fn(Instance::mono(tcx, def_id))),
+        DefKind::GlobalAsm => Some(MonoItem::GlobalAsm(item_id)),
+        _ => {
+            debug!(?def_id, ?kind, "Ignored item. Not a root type.");
+            None
+        }
+    }
+}
+
 struct MonoItemsCollector<'tcx> {
     /// The compiler context.
     tcx: TyCtxt<'tcx>,

tests/expected/associated-fn/associated_fn.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --enable-unstable --function new
+//! This ensures our public functions reachability module works for associated functions.
+
+struct Dummy {
+    c: char,
+}
+
+impl Dummy {
+    #[no_mangle]
+    pub fn new() -> Self {
+        Dummy { c: ' ' }
+    }
+}

tests/expected/associated-fn/expected

@@ -0,0 +1,3 @@
+Checking harness new...
+VERIFICATION:- SUCCESSFUL
+

tests/kani/Static/pub_static.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --enable-unstable --function harness
+//! This test covers an issue we had with our public-fns implementation.
+//! We were not checking if a root was a function in the first place.
+//! https://github.com/model-checking/kani/issues/2047
+
+pub static DAYS_OF_WEEK: [char; 7] = ['s', 'm', 't', 'w', 't', 'f', 's'];
+
+#[no_mangle]
+pub fn harness() {
+    let day: usize = kani::any();
+    kani::assume(day < DAYS_OF_WEEK.len());
+    assert!(['s', 'm', 't', 'w', 'f'].contains(&DAYS_OF_WEEK[day]));
+}