Skip to content

Commit 0367992

Browse files
Add support for global transformations (rust-lang#3348)
This PR adds basic support for global transformations, which will be useful to implement full support of rust-lang#3324 Changes: - Add edge annotations to the call graph - Implement global transformation pass infrastructure - Implement `dump_mir` as a global transformation pass By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val <[email protected]>
1 parent 96d1147 commit 0367992

File tree

5 files changed

+336
-169
lines changed

5 files changed

+336
-169
lines changed

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

Lines changed: 26 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,14 @@ use crate::args::ReachabilityType;
77
use crate::codegen_cprover_gotoc::GotocCtx;
88
use crate::kani_middle::analysis;
99
use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes};
10+
use crate::kani_middle::check_reachable_items;
1011
use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits};
1112
use crate::kani_middle::metadata::gen_test_metadata;
1213
use crate::kani_middle::provide;
1314
use crate::kani_middle::reachability::{
1415
collect_reachable_items, filter_const_crate_items, filter_crate_items,
1516
};
16-
use crate::kani_middle::transform::BodyTransformation;
17-
use crate::kani_middle::{check_reachable_items, dump_mir_items};
17+
use crate::kani_middle::transform::{BodyTransformation, GlobalPasses};
1818
use crate::kani_queries::QueryDb;
1919
use cbmc::goto_program::Location;
2020
use cbmc::irep::goto_binary_serde::write_goto_binary_file;
@@ -87,11 +87,33 @@ impl GotocCodegenBackend {
8787
check_contract: Option<InternalDefId>,
8888
mut transformer: BodyTransformation,
8989
) -> (GotocCtx<'tcx>, Vec<MonoItem>, Option<AssignsContract>) {
90-
let items = with_timer(
90+
let (items, call_graph) = with_timer(
9191
|| collect_reachable_items(tcx, &mut transformer, starting_items),
9292
"codegen reachability analysis",
9393
);
94-
dump_mir_items(tcx, &mut transformer, &items, &symtab_goto.with_extension("kani.mir"));
94+
95+
// Retrieve all instances from the currently codegened items.
96+
let instances = items
97+
.iter()
98+
.filter_map(|item| match item {
99+
MonoItem::Fn(instance) => Some(*instance),
100+
MonoItem::Static(static_def) => {
101+
let instance: Instance = (*static_def).into();
102+
instance.has_body().then_some(instance)
103+
}
104+
MonoItem::GlobalAsm(_) => None,
105+
})
106+
.collect();
107+
108+
// Apply all transformation passes, including global passes.
109+
let mut global_passes = GlobalPasses::new(&self.queries.lock().unwrap(), tcx);
110+
global_passes.run_global_passes(
111+
&mut transformer,
112+
tcx,
113+
starting_items,
114+
instances,
115+
call_graph,
116+
);
95117

96118
// Follow rustc naming convention (cx is abbrev for context).
97119
// https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions

kani-compiler/src/kani_middle/mod.rs

Lines changed: 1 addition & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,7 @@
44
//! and transformations.
55
66
use std::collections::HashSet;
7-
use std::path::Path;
87

9-
use crate::kani_middle::transform::BodyTransformation;
108
use crate::kani_queries::QueryDb;
119
use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE};
1210
use rustc_middle::span_bug;
@@ -15,18 +13,14 @@ use rustc_middle::ty::layout::{
1513
LayoutOfHelpers, TyAndLayout,
1614
};
1715
use rustc_middle::ty::{self, Instance as InstanceInternal, Ty as TyInternal, TyCtxt};
18-
use rustc_session::config::OutputType;
1916
use rustc_smir::rustc_internal;
2017
use rustc_span::source_map::respan;
2118
use rustc_span::Span;
2219
use rustc_target::abi::call::FnAbi;
2320
use rustc_target::abi::{HasDataLayout, TargetDataLayout};
24-
use stable_mir::mir::mono::{Instance, MonoItem};
21+
use stable_mir::mir::mono::MonoItem;
2522
use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, TyKind};
2623
use stable_mir::CrateDef;
27-
use std::fs::File;
28-
use std::io::BufWriter;
29-
use std::io::Write;
3024

3125
use self::attributes::KaniAttributes;
3226

@@ -92,41 +86,6 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
9286
tcx.dcx().abort_if_errors();
9387
}
9488

95-
/// Print MIR for the reachable items if the `--emit mir` option was provided to rustc.
96-
pub fn dump_mir_items(
97-
tcx: TyCtxt,
98-
transformer: &mut BodyTransformation,
99-
items: &[MonoItem],
100-
output: &Path,
101-
) {
102-
/// Convert MonoItem into a DefId.
103-
/// Skip stuff that we cannot generate the MIR items.
104-
fn get_instance(item: &MonoItem) -> Option<Instance> {
105-
match item {
106-
// Exclude FnShims and others that cannot be dumped.
107-
MonoItem::Fn(instance) => Some(*instance),
108-
MonoItem::Static(def) => {
109-
let instance: Instance = (*def).into();
110-
instance.has_body().then_some(instance)
111-
}
112-
MonoItem::GlobalAsm(_) => None,
113-
}
114-
}
115-
116-
if tcx.sess.opts.output_types.contains_key(&OutputType::Mir) {
117-
// Create output buffer.
118-
let out_file = File::create(output).unwrap();
119-
let mut writer = BufWriter::new(out_file);
120-
121-
// For each def_id, dump their MIR
122-
for instance in items.iter().filter_map(get_instance) {
123-
writeln!(writer, "// Item: {} ({})", instance.name(), instance.mangled_name()).unwrap();
124-
let body = transformer.body(tcx, instance);
125-
let _ = body.dump(&mut writer, &instance.name());
126-
}
127-
}
128-
}
129-
13089
/// Structure that represents the source location of a definition.
13190
/// TODO: Use `InternedString` once we move it out of the cprover_bindings.
13291
/// <https://github.com/model-checking/kani/issues/2435>

0 commit comments

Comments
 (0)