Skip to content

Cleanup redundant logic #2437

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
celinval merged 4 commits into from
May 12, 2023
Merged

Cleanup redundant logic #2437

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
26999fe
Cleanup redundant logic
celinval May 11, 2023
a308f55
Merge branch 'main' into issue-xxxx-cleanup
celinval May 11, 2023
e67a4d4
Remove extra line from reachability.rs
celinval May 11, 2023
6403921
Merge branch 'main' into issue-xxxx-cleanup
celinval May 12, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -408,7 +408,7 @@ fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec<MonoItem<'tcx>> {
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()
Expand Down
63 changes: 8 additions & 55 deletions kani-compiler/src/kani_middle/reachability.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<F>(tcx: TyCtxt, mut predicate: F) -> Vec<MonoItem>
pub fn filter_const_crate_items<F>(tcx: TyCtxt, mut predicate: F) -> Vec<MonoItem>
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
Expand Down Expand Up @@ -602,53 +602,6 @@ fn collect_alloc_items(tcx: TyCtxt, alloc_id: AllocId) -> Vec<MonoItem> {
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<MonoItem<'tcx>>,
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)]
Expand Down