diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index e9aab19acbd3..9df0797d9d51 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -12,7 +12,7 @@ use crate::kani_middle::check_crate_items; use crate::kani_middle::check_reachable_items; use crate::kani_middle::provide; use crate::kani_middle::reachability::{ - collect_reachable_items, filter_closures_in_const_crate_items, filter_crate_items, + collect_reachable_items, filter_const_crate_items, filter_crate_items, }; use cbmc::goto_program::Location; use cbmc::irep::goto_binary_serde::write_goto_binary_file; @@ -408,7 +408,7 @@ fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec> { ReachabilityType::Tests => { // We're iterating over crate items here, so what we have to codegen is the "test description" containing the // test closure that we want to execute - let harnesses = filter_closures_in_const_crate_items(tcx, |_, def_id| { + let harnesses = filter_const_crate_items(tcx, |_, def_id| { is_test_harness_description(gcx.tcx, def_id) }); collect_reachable_items(tcx, &harnesses).into_iter().collect() diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 2847c9285e7c..5e8144be0d16 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -97,26 +97,26 @@ where root_items.chain(impl_items).collect() } -/// Use a predicate to find `const` declarations, then extract all closures from those declarations +/// Use a predicate to find `const` declarations, then extract all items reachable from them. /// /// Probably only specifically useful with a predicate to find `TestDescAndFn` const declarations from /// tests and extract the closures from them. -pub fn filter_closures_in_const_crate_items(tcx: TyCtxt, mut predicate: F) -> Vec +pub fn filter_const_crate_items(tcx: TyCtxt, mut predicate: F) -> Vec where F: FnMut(TyCtxt, DefId) -> bool, { let mut roots = Vec::new(); for hir_id in tcx.hir_crate_items(()).items() { let def_id = hir_id.owner_id.def_id.to_def_id(); - if predicate(tcx, def_id) { - // The predicate should only ever apply to monomorphic items + let def_kind = tcx.def_kind(def_id); + if matches!(def_kind, DefKind::Const) && predicate(tcx, def_id) { let instance = Instance::mono(tcx, def_id); let body = tcx.instance_mir(InstanceDef::Item(WithOptConstParam::unknown(def_id))); - let mut extrator = - ConstMonoItemExtractor { tcx, body, instance, collected: FxHashSet::default() }; - extrator.visit_body(body); + let mut collector = + MonoItemsFnCollector { tcx, body, instance, collected: FxHashSet::default() }; + collector.visit_body(body); - roots.extend(extrator.collected); + roots.extend(collector.collected); } } roots @@ -602,53 +602,6 @@ fn collect_alloc_items(tcx: TyCtxt, alloc_id: AllocId) -> Vec { items } -/// This MIR Visitor is intended for one specific purpose: -/// Find the closure that exist inside a top-level const declaration generated by -/// test declarations. This allows us to treat this closure instance as a root for -/// the reachability analysis. -/// -/// Entry into this visitor will be via `visit_body` -struct ConstMonoItemExtractor<'a, 'tcx> { - tcx: TyCtxt<'tcx>, - collected: FxHashSet>, - instance: Instance<'tcx>, - body: &'a Body<'tcx>, -} - -impl<'a, 'tcx> MirVisitor<'tcx> for ConstMonoItemExtractor<'a, 'tcx> { - #[allow(clippy::single_match)] - fn visit_rvalue(&mut self, rvalue: &Rvalue<'tcx>, location: Location) { - trace!(rvalue=?*rvalue, "visit_rvalue"); - - match *rvalue { - Rvalue::Cast(CastKind::Pointer(PointerCast::ClosureFnPointer(_)), ref operand, _) => { - let source_ty = operand.ty(self.body, self.tcx); - let source_ty = self.instance.subst_mir_and_normalize_erasing_regions( - self.tcx, - ParamEnv::reveal_all(), - source_ty, - ); - match *source_ty.kind() { - Closure(def_id, substs) => { - let instance = Instance::resolve_closure( - self.tcx, - def_id, - substs, - ClosureKind::FnOnce, - ) - .expect("failed to normalize and resolve closure during codegen"); - self.collected.insert(MonoItem::Fn(instance.polymorphize(self.tcx))); - } - _ => unreachable!("Unexpected type: {:?}", source_ty), - } - } - _ => { /* not interesting */ } - } - - self.super_rvalue(rvalue, location); - } -} - #[cfg(debug_assertions)] mod debug { #![allow(dead_code)]