Skip to content

Commit 9d01f97

Browse files
ouz-aouz-a
authored
Make codegen_span stable (rust-lang#2882)
Follow up pr to model-checking/kani#2871 as `stable_mir::ty::Span` have ability to `get_filename` and `get_lineinfo` we could start adopting it.
1 parent aeafbd8 commit 9d01f97

File tree

3 files changed

+129
-120
lines changed

3 files changed

+129
-120
lines changed

‎kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,16 +3,21 @@
33

44
//! MIR Span related functions
55
6-
use crate::{codegen_cprover_gotoc::GotocCtx, kani_middle::SourceLocation};
6+
use crate::codegen_cprover_gotoc::GotocCtx;
77
use cbmc::goto_program::Location;
88
use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents};
9+
use rustc_smir::rustc_internal;
910
use rustc_span::Span;
1011

1112
impl<'tcx> GotocCtx<'tcx> {
1213
pub fn codegen_span(&self, sp: &Span) -> Location {
13-
let loc = SourceLocation::new(self.tcx, sp);
14+
self.stable_codegen_span(&rustc_internal::stable(sp))
15+
}
16+
17+
pub fn stable_codegen_span(&self, sp: &stable_mir::ty::Span) -> Location {
18+
let loc = sp.get_lines();
1419
Location::new(
15-
loc.filename,
20+
sp.get_filename().to_string(),
1621
self.current_fn.as_ref().map(|x| x.readable_name().to_string()),
1722
loc.start_line,
1823
Some(loc.start_col),

‎kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

Lines changed: 103 additions & 92 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,7 @@ use rustc_session::config::{CrateType, OutputFilenames, OutputType};
4343
use rustc_session::cstore::MetadataLoaderDyn;
4444
use rustc_session::output::out_filename;
4545
use rustc_session::Session;
46+
use rustc_smir::rustc_internal;
4647
use rustc_target::abi::Endian;
4748
use rustc_target::spec::PanicStrategy;
4849
use std::any::Any;
@@ -208,105 +209,115 @@ impl CodegenBackend for GotocCodegenBackend {
208209
rustc_metadata: EncodedMetadata,
209210
_need_metadata_module: bool,
210211
) -> Box<dyn Any> {
211-
super::utils::init();
212-
213-
// Queries shouldn't change today once codegen starts.
214-
let queries = self.queries.lock().unwrap().clone();
215-
check_target(tcx.sess);
216-
check_options(tcx.sess);
217-
218-
// Codegen all items that need to be processed according to the selected reachability mode:
219-
//
220-
// - Harnesses: Generate one model per local harnesses (marked with `kani::proof` attribute).
221-
// - Tests: Generate one model per test harnesses.
222-
// - PubFns: Generate code for all reachable logic starting from the local public functions.
223-
// - None: Don't generate code. This is used to compile dependencies.
224-
let base_filename = tcx.output_filenames(()).output_path(OutputType::Object);
225-
let reachability = queries.args().reachability_analysis;
226-
let mut results = GotoCodegenResults::new(tcx, reachability);
227-
match reachability {
228-
ReachabilityType::Harnesses => {
229-
// Cross-crate collecting of all items that are reachable from the crate harnesses.
230-
let harnesses = queries.target_harnesses();
231-
let mut items: HashSet<DefPathHash> = HashSet::with_capacity(harnesses.len());
232-
items.extend(harnesses);
233-
let harnesses =
234-
filter_crate_items(tcx, |_, def_id| items.contains(&tcx.def_path_hash(def_id)));
235-
for harness in harnesses {
236-
let model_path =
237-
queries.harness_model_path(&tcx.def_path_hash(harness.def_id())).unwrap();
212+
let ret_val = rustc_internal::run(tcx, || {
213+
super::utils::init();
214+
215+
// Queries shouldn't change today once codegen starts.
216+
let queries = self.queries.lock().unwrap().clone();
217+
check_target(tcx.sess);
218+
check_options(tcx.sess);
219+
220+
// Codegen all items that need to be processed according to the selected reachability mode:
221+
//
222+
// - Harnesses: Generate one model per local harnesses (marked with `kani::proof` attribute).
223+
// - Tests: Generate one model per test harnesses.
224+
// - PubFns: Generate code for all reachable logic starting from the local public functions.
225+
// - None: Don't generate code. This is used to compile dependencies.
226+
let base_filename = tcx.output_filenames(()).output_path(OutputType::Object);
227+
let reachability = queries.args().reachability_analysis;
228+
let mut results = GotoCodegenResults::new(tcx, reachability);
229+
match reachability {
230+
ReachabilityType::Harnesses => {
231+
// Cross-crate collecting of all items that are reachable from the crate harnesses.
232+
let harnesses = queries.target_harnesses();
233+
let mut items: HashSet<DefPathHash> = HashSet::with_capacity(harnesses.len());
234+
items.extend(harnesses);
235+
let harnesses = filter_crate_items(tcx, |_, def_id| {
236+
items.contains(&tcx.def_path_hash(def_id))
237+
});
238+
for harness in harnesses {
239+
let model_path = queries
240+
.harness_model_path(&tcx.def_path_hash(harness.def_id()))
241+
.unwrap();
242+
let (gcx, items) =
243+
self.codegen_items(tcx, &[harness], model_path, &results.machine_model);
244+
results.extend(gcx, items, None);
245+
}
246+
}
247+
ReachabilityType::Tests => {
248+
// We're iterating over crate items here, so what we have to codegen is the "test description" containing the
249+
// test closure that we want to execute
250+
// TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match.
251+
let mut descriptions = vec![];
252+
let harnesses = filter_const_crate_items(tcx, |_, def_id| {
253+
if is_test_harness_description(tcx, def_id) {
254+
descriptions.push(def_id);
255+
true
256+
} else {
257+
false
258+
}
259+
});
260+
// Codegen still takes a considerable amount, thus, we only generate one model for
261+
// all harnesses and copy them for each harness.
262+
// We will be able to remove this once we optimize all calls to CBMC utilities.
263+
// https://github.com/model-checking/kani/issues/1971
264+
let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
238265
let (gcx, items) =
239-
self.codegen_items(tcx, &[harness], model_path, &results.machine_model);
266+
self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model);
240267
results.extend(gcx, items, None);
241-
}
242-
}
243-
ReachabilityType::Tests => {
244-
// We're iterating over crate items here, so what we have to codegen is the "test description" containing the
245-
// test closure that we want to execute
246-
// TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match.
247-
let mut descriptions = vec![];
248-
let harnesses = filter_const_crate_items(tcx, |_, def_id| {
249-
if is_test_harness_description(tcx, def_id) {
250-
descriptions.push(def_id);
251-
true
252-
} else {
253-
false
268+
269+
for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) {
270+
let instance =
271+
if let MonoItem::Fn(instance) = test_fn { instance } else { continue };
272+
let metadata =
273+
gen_test_metadata(tcx, *test_desc, *instance, &base_filename);
274+
let test_model_path = &metadata.goto_file.as_ref().unwrap();
275+
std::fs::copy(&model_path, test_model_path).expect(&format!(
276+
"Failed to copy {} to {}",
277+
model_path.display(),
278+
test_model_path.display()
279+
));
280+
results.harnesses.push(metadata);
254281
}
255-
});
256-
// Codegen still takes a considerable amount, thus, we only generate one model for
257-
// all harnesses and copy them for each harness.
258-
// We will be able to remove this once we optimize all calls to CBMC utilities.
259-
// https://github.com/model-checking/kani/issues/1971
260-
let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
261-
let (gcx, items) =
262-
self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model);
263-
results.extend(gcx, items, None);
264-
265-
for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) {
266-
let instance =
267-
if let MonoItem::Fn(instance) = test_fn { instance } else { continue };
268-
let metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename);
269-
let test_model_path = &metadata.goto_file.as_ref().unwrap();
270-
std::fs::copy(&model_path, test_model_path).expect(&format!(
271-
"Failed to copy {} to {}",
272-
model_path.display(),
273-
test_model_path.display()
274-
));
275-
results.harnesses.push(metadata);
282+
}
283+
ReachabilityType::None => {}
284+
ReachabilityType::PubFns => {
285+
let entry_fn = tcx.entry_fn(()).map(|(id, _)| id);
286+
let local_reachable = filter_crate_items(tcx, |_, def_id| {
287+
(tcx.is_reachable_non_generic(def_id) && tcx.def_kind(def_id).is_fn_like())
288+
|| entry_fn == Some(def_id)
289+
});
290+
let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
291+
let (gcx, items) = self.codegen_items(
292+
tcx,
293+
&local_reachable,
294+
&model_path,
295+
&results.machine_model,
296+
);
297+
results.extend(gcx, items, None);
276298
}
277299
}
278-
ReachabilityType::None => {}
279-
ReachabilityType::PubFns => {
280-
let entry_fn = tcx.entry_fn(()).map(|(id, _)| id);
281-
let local_reachable = filter_crate_items(tcx, |_, def_id| {
282-
(tcx.is_reachable_non_generic(def_id) && tcx.def_kind(def_id).is_fn_like())
283-
|| entry_fn == Some(def_id)
284-
});
285-
let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
286-
let (gcx, items) =
287-
self.codegen_items(tcx, &local_reachable, &model_path, &results.machine_model);
288-
results.extend(gcx, items, None);
289-
}
290-
}
291300

292-
if reachability != ReachabilityType::None {
293-
// Print compilation report.
294-
results.print_report(tcx);
295-
296-
if reachability != ReachabilityType::Harnesses {
297-
// In a workspace, cargo seems to be using the same file prefix to build a crate that is
298-
// a package lib and also a dependency of another package.
299-
// To avoid overriding the metadata for its verification, we skip this step when
300-
// reachability is None, even because there is nothing to record.
301-
write_file(
302-
&base_filename,
303-
ArtifactType::Metadata,
304-
&results.generate_metadata(),
305-
queries.args().output_pretty_json,
306-
);
301+
if reachability != ReachabilityType::None {
302+
// Print compilation report.
303+
results.print_report(tcx);
304+
305+
if reachability != ReachabilityType::Harnesses {
306+
// In a workspace, cargo seems to be using the same file prefix to build a crate that is
307+
// a package lib and also a dependency of another package.
308+
// To avoid overriding the metadata for its verification, we skip this step when
309+
// reachability is None, even because there is nothing to record.
310+
write_file(
311+
&base_filename,
312+
ArtifactType::Metadata,
313+
&results.generate_metadata(),
314+
queries.args().output_pretty_json,
315+
);
316+
}
307317
}
308-
}
309-
codegen_results(tcx, rustc_metadata, &results.machine_model)
318+
codegen_results(tcx, rustc_metadata, &results.machine_model)
319+
});
320+
ret_val.unwrap()
310321
}
311322

312323
fn join_codegen(

‎kani-compiler/src/kani_middle/analysis.rs

Lines changed: 18 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -23,31 +23,24 @@ use std::fmt::Display;
2323
/// - Number of items per type (Function / Constant / Shims)
2424
/// - Number of instructions per type.
2525
/// - Total number of MIR instructions.
26-
pub fn print_stats<'tcx>(tcx: TyCtxt<'tcx>, items: &[InternalMonoItem<'tcx>]) {
27-
rustc_internal::run(tcx, || {
28-
let items: Vec<MonoItem> = items.iter().map(rustc_internal::stable).collect();
29-
let item_types = items.iter().collect::<Counter>();
30-
let visitor = items
31-
.iter()
32-
.filter_map(
33-
|mono| {
34-
if let MonoItem::Fn(instance) = mono { Some(instance) } else { None }
35-
},
36-
)
37-
.fold(StatsVisitor::default(), |mut visitor, body| {
38-
visitor.visit_body(&body.body().unwrap());
39-
visitor
40-
});
41-
eprintln!("====== Reachability Analysis Result =======");
42-
eprintln!("Total # items: {}", item_types.total());
43-
eprintln!("Total # statements: {}", visitor.stmts.total());
44-
eprintln!("Total # expressions: {}", visitor.exprs.total());
45-
eprintln!("\nReachable Items:\n{item_types}");
46-
eprintln!("Statements:\n{}", visitor.stmts);
47-
eprintln!("Expressions:\n{}", visitor.exprs);
48-
eprintln!("-------------------------------------------")
49-
})
50-
.unwrap();
26+
pub fn print_stats<'tcx>(_tcx: TyCtxt<'tcx>, items: &[InternalMonoItem<'tcx>]) {
27+
let items: Vec<MonoItem> = items.iter().map(rustc_internal::stable).collect();
28+
let item_types = items.iter().collect::<Counter>();
29+
let visitor = items
30+
.iter()
31+
.filter_map(|mono| if let MonoItem::Fn(instance) = mono { Some(instance) } else { None })
32+
.fold(StatsVisitor::default(), |mut visitor, body| {
33+
visitor.visit_body(&body.body().unwrap());
34+
visitor
35+
});
36+
eprintln!("====== Reachability Analysis Result =======");
37+
eprintln!("Total # items: {}", item_types.total());
38+
eprintln!("Total # statements: {}", visitor.stmts.total());
39+
eprintln!("Total # expressions: {}", visitor.exprs.total());
40+
eprintln!("\nReachable Items:\n{item_types}");
41+
eprintln!("Statements:\n{}", visitor.stmts);
42+
eprintln!("Expressions:\n{}", visitor.exprs);
43+
eprintln!("-------------------------------------------")
5144
}
5245

5346
#[derive(Default)]

0 commit comments

Comments
 (0)