Skip to content

Commit c2690ab

Browse files
authored
Fix crash when using public fns reachability (rust-lang#2065)
Filter roots to only collect public functions. Also, make the collection function more robust and to account for associated functions.
1 parent 280d3eb commit c2690ab

File tree

5 files changed

+85
-14
lines changed

5 files changed

+85
-14
lines changed

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

+6-5
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ use std::process::Command;
4848
use std::rc::Rc;
4949
use std::time::Instant;
5050
use tempfile::Builder as TempFileBuilder;
51-
use tracing::{debug, error, info, warn};
51+
use tracing::{debug, error, info};
5252

5353
#[derive(Clone)]
5454
pub struct GotocCodegenBackend {
@@ -310,10 +310,10 @@ fn check_crate_items(gcx: &GotocCtx) {
310310
);
311311
tcx.sess.err(&error_msg);
312312
} else {
313-
warn!(
313+
tcx.sess.warn(format!(
314314
"Ignoring global ASM in crate {}. Verification results may be impacted.",
315315
gcx.short_crate_name()
316-
);
316+
));
317317
}
318318
}
319319
}
@@ -371,7 +371,7 @@ fn codegen_results(
371371
fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec<MonoItem<'tcx>> {
372372
let tcx = gcx.tcx;
373373
let reach = gcx.queries.get_reachability_analysis();
374-
debug!(?reach, "starting_points");
374+
debug!(?reach, "collect_codegen_items");
375375
match reach {
376376
ReachabilityType::Legacy => {
377377
// Use rustc monomorphizer to retrieve items to codegen.
@@ -399,7 +399,8 @@ fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec<MonoItem<'tcx>> {
399399
ReachabilityType::PubFns => {
400400
let entry_fn = tcx.entry_fn(()).map(|(id, _)| id);
401401
let local_reachable = filter_crate_items(tcx, |_, def_id| {
402-
tcx.is_reachable_non_generic(def_id) || entry_fn == Some(def_id)
402+
(tcx.is_reachable_non_generic(def_id) && tcx.def_kind(def_id).is_fn_like())
403+
|| entry_fn == Some(def_id)
403404
});
404405
collect_reachable_items(tcx, &local_reachable).into_iter().collect()
405406
}

kani-compiler/src/kani_middle/reachability.rs

+46-9
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,9 @@ use tracing::{debug, debug_span, trace, warn};
1818
use rustc_data_structures::fingerprint::Fingerprint;
1919
use rustc_data_structures::fx::FxHashSet;
2020
use rustc_data_structures::stable_hasher::{HashStable, StableHasher};
21+
use rustc_hir::def::DefKind;
2122
use rustc_hir::def_id::DefId;
23+
use rustc_hir::ItemId;
2224
use rustc_middle::mir::interpret::{AllocId, ConstValue, ErrorHandled, GlobalAlloc, Scalar};
2325
use rustc_middle::mir::mono::MonoItem;
2426
use rustc_middle::mir::visit::Visitor as MirVisitor;
@@ -57,18 +59,35 @@ pub fn collect_reachable_items<'tcx>(
5759
}
5860

5961
/// Collect all (top-level) items in the crate that matches the given predicate.
62+
/// An item can only be a root if they are: non-generic Fn / Static / GlobalASM
6063
pub fn filter_crate_items<F>(tcx: TyCtxt, predicate: F) -> Vec<MonoItem>
6164
where
62-
F: FnMut(TyCtxt, DefId) -> bool,
65+
F: Fn(TyCtxt, DefId) -> bool,
6366
{
64-
let mut filter = predicate;
65-
tcx.hir_crate_items(())
66-
.items()
67-
.filter_map(|hir_id| {
68-
let def_id = hir_id.owner_id.def_id.to_def_id();
69-
filter(tcx, def_id).then(|| MonoItem::Fn(Instance::mono(tcx, def_id)))
70-
})
71-
.collect()
67+
let crate_items = tcx.hir_crate_items(());
68+
// Filter regular items.
69+
let root_items = crate_items.items().filter_map(|item| {
70+
let def_id = item.owner_id.def_id.to_def_id();
71+
if !is_generic(tcx, def_id) && predicate(tcx, def_id) {
72+
to_mono_root(tcx, item, def_id)
73+
} else {
74+
None
75+
}
76+
});
77+
78+
// Filter items from implementation blocks.
79+
let impl_items = crate_items.impl_items().filter_map(|impl_item| {
80+
let def_id = impl_item.owner_id.def_id.to_def_id();
81+
if matches!(tcx.def_kind(def_id), DefKind::AssocFn)
82+
&& !is_generic(tcx, def_id)
83+
&& predicate(tcx, def_id)
84+
{
85+
Some(MonoItem::Fn(Instance::mono(tcx, def_id)))
86+
} else {
87+
None
88+
}
89+
});
90+
root_items.chain(impl_items).collect()
7291
}
7392

7493
/// Use a predicate to find `const` declarations, then extract all closures from those declarations
@@ -96,6 +115,24 @@ where
96115
roots
97116
}
98117

118+
fn is_generic(tcx: TyCtxt, def_id: DefId) -> bool {
119+
let generics = tcx.generics_of(def_id);
120+
generics.requires_monomorphization(tcx)
121+
}
122+
123+
fn to_mono_root(tcx: TyCtxt, item_id: ItemId, def_id: DefId) -> Option<MonoItem> {
124+
let kind = tcx.def_kind(def_id);
125+
match kind {
126+
DefKind::Static(..) => Some(MonoItem::Static(def_id)),
127+
DefKind::Fn => Some(MonoItem::Fn(Instance::mono(tcx, def_id))),
128+
DefKind::GlobalAsm => Some(MonoItem::GlobalAsm(item_id)),
129+
_ => {
130+
debug!(?def_id, ?kind, "Ignored item. Not a root type.");
131+
None
132+
}
133+
}
134+
}
135+
99136
struct MonoItemsCollector<'tcx> {
100137
/// The compiler context.
101138
tcx: TyCtxt<'tcx>,
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
// Copyright Kani Contributors
2+
// SPDX-License-Identifier: Apache-2.0 OR MIT
3+
// kani-flags: --enable-unstable --function new
4+
//! This ensures our public functions reachability module works for associated functions.
5+
6+
struct Dummy {
7+
c: char,
8+
}
9+
10+
impl Dummy {
11+
#[no_mangle]
12+
pub fn new() -> Self {
13+
Dummy { c: ' ' }
14+
}
15+
}

tests/expected/associated-fn/expected

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
Checking harness new...
2+
VERIFICATION:- SUCCESSFUL
3+

tests/kani/Static/pub_static.rs

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

0 commit comments

Comments
 (0)