Skip to content

Commit

Permalink
Make codegen_span stable (#2882)
Browse files Browse the repository at this point in the history 
Follow up pr to #2871 as
`stable_mir::ty::Span` have ability to `get_filename` and `get_lineinfo`
we could start adopting it.
  • Loading branch information
@ouz-a
ouz-a authored Nov 29, 2023
1 parent aeafbd8 commit 9d01f97
Show file tree
Hide file tree
Showing 3 changed files with 129 additions and 120 deletions.
11 changes: 8 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,16 +3,21 @@

//! MIR Span related functions

use crate::{codegen_cprover_gotoc::GotocCtx, kani_middle::SourceLocation};
use crate::codegen_cprover_gotoc::GotocCtx;
use cbmc::goto_program::Location;
use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents};
use rustc_smir::rustc_internal;
use rustc_span::Span;

impl<'tcx> GotocCtx<'tcx> {
pub fn codegen_span(&self, sp: &Span) -> Location {
let loc = SourceLocation::new(self.tcx, sp);
self.stable_codegen_span(&rustc_internal::stable(sp))
}

pub fn stable_codegen_span(&self, sp: &stable_mir::ty::Span) -> Location {
let loc = sp.get_lines();
Location::new(
loc.filename,
sp.get_filename().to_string(),
self.current_fn.as_ref().map(|x| x.readable_name().to_string()),
loc.start_line,
Some(loc.start_col),
Expand Down
195 changes: 103 additions & 92 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ use rustc_session::config::{CrateType, OutputFilenames, OutputType};
use rustc_session::cstore::MetadataLoaderDyn;
use rustc_session::output::out_filename;
use rustc_session::Session;
use rustc_smir::rustc_internal;
use rustc_target::abi::Endian;
use rustc_target::spec::PanicStrategy;
use std::any::Any;
Expand Down Expand Up @@ -208,105 +209,115 @@ impl CodegenBackend for GotocCodegenBackend {
rustc_metadata: EncodedMetadata,
_need_metadata_module: bool,
) -> Box<dyn Any> {
super::utils::init();

// Queries shouldn't change today once codegen starts.
let queries = self.queries.lock().unwrap().clone();
check_target(tcx.sess);
check_options(tcx.sess);

// Codegen all items that need to be processed according to the selected reachability mode:
//
// - Harnesses: Generate one model per local harnesses (marked with `kani::proof` attribute).
// - Tests: Generate one model per test harnesses.
// - PubFns: Generate code for all reachable logic starting from the local public functions.
// - None: Don't generate code. This is used to compile dependencies.
let base_filename = tcx.output_filenames(()).output_path(OutputType::Object);
let reachability = queries.args().reachability_analysis;
let mut results = GotoCodegenResults::new(tcx, reachability);
match reachability {
ReachabilityType::Harnesses => {
// Cross-crate collecting of all items that are reachable from the crate harnesses.
let harnesses = queries.target_harnesses();
let mut items: HashSet<DefPathHash> = HashSet::with_capacity(harnesses.len());
items.extend(harnesses);
let harnesses =
filter_crate_items(tcx, |_, def_id| items.contains(&tcx.def_path_hash(def_id)));
for harness in harnesses {
let model_path =
queries.harness_model_path(&tcx.def_path_hash(harness.def_id())).unwrap();
let ret_val = rustc_internal::run(tcx, || {
super::utils::init();

// Queries shouldn't change today once codegen starts.
let queries = self.queries.lock().unwrap().clone();
check_target(tcx.sess);
check_options(tcx.sess);

// Codegen all items that need to be processed according to the selected reachability mode:
//
// - Harnesses: Generate one model per local harnesses (marked with `kani::proof` attribute).
// - Tests: Generate one model per test harnesses.
// - PubFns: Generate code for all reachable logic starting from the local public functions.
// - None: Don't generate code. This is used to compile dependencies.
let base_filename = tcx.output_filenames(()).output_path(OutputType::Object);
let reachability = queries.args().reachability_analysis;
let mut results = GotoCodegenResults::new(tcx, reachability);
match reachability {
ReachabilityType::Harnesses => {
// Cross-crate collecting of all items that are reachable from the crate harnesses.
let harnesses = queries.target_harnesses();
let mut items: HashSet<DefPathHash> = HashSet::with_capacity(harnesses.len());
items.extend(harnesses);
let harnesses = filter_crate_items(tcx, |_, def_id| {
items.contains(&tcx.def_path_hash(def_id))
});
for harness in harnesses {
let model_path = queries
.harness_model_path(&tcx.def_path_hash(harness.def_id()))
.unwrap();
let (gcx, items) =
self.codegen_items(tcx, &[harness], model_path, &results.machine_model);
results.extend(gcx, items, None);
}
}
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
// TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match.
let mut descriptions = vec![];
let harnesses = filter_const_crate_items(tcx, |_, def_id| {
if is_test_harness_description(tcx, def_id) {
descriptions.push(def_id);
true
} else {
false
}
});
// Codegen still takes a considerable amount, thus, we only generate one model for
// all harnesses and copy them for each harness.
// We will be able to remove this once we optimize all calls to CBMC utilities.
// https://github.com/model-checking/kani/issues/1971
let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
let (gcx, items) =
self.codegen_items(tcx, &[harness], model_path, &results.machine_model);
self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model);
results.extend(gcx, items, None);
}
}
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
// TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match.
let mut descriptions = vec![];
let harnesses = filter_const_crate_items(tcx, |_, def_id| {
if is_test_harness_description(tcx, def_id) {
descriptions.push(def_id);
true
} else {
false

for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) {
let instance =
if let MonoItem::Fn(instance) = test_fn { instance } else { continue };
let metadata =
gen_test_metadata(tcx, *test_desc, *instance, &base_filename);
let test_model_path = &metadata.goto_file.as_ref().unwrap();
std::fs::copy(&model_path, test_model_path).expect(&format!(
"Failed to copy {} to {}",
model_path.display(),
test_model_path.display()
));
results.harnesses.push(metadata);
}
});
// Codegen still takes a considerable amount, thus, we only generate one model for
// all harnesses and copy them for each harness.
// We will be able to remove this once we optimize all calls to CBMC utilities.
// https://github.com/model-checking/kani/issues/1971
let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
let (gcx, items) =
self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model);
results.extend(gcx, items, None);

for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) {
let instance =
if let MonoItem::Fn(instance) = test_fn { instance } else { continue };
let metadata = gen_test_metadata(tcx, *test_desc, *instance, &base_filename);
let test_model_path = &metadata.goto_file.as_ref().unwrap();
std::fs::copy(&model_path, test_model_path).expect(&format!(
"Failed to copy {} to {}",
model_path.display(),
test_model_path.display()
));
results.harnesses.push(metadata);
}
ReachabilityType::None => {}
ReachabilityType::PubFns => {
let entry_fn = tcx.entry_fn(()).map(|(id, _)| id);
let local_reachable = filter_crate_items(tcx, |_, def_id| {
(tcx.is_reachable_non_generic(def_id) && tcx.def_kind(def_id).is_fn_like())
|| entry_fn == Some(def_id)
});
let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
let (gcx, items) = self.codegen_items(
tcx,
&local_reachable,
&model_path,
&results.machine_model,
);
results.extend(gcx, items, None);
}
}
ReachabilityType::None => {}
ReachabilityType::PubFns => {
let entry_fn = tcx.entry_fn(()).map(|(id, _)| id);
let local_reachable = filter_crate_items(tcx, |_, def_id| {
(tcx.is_reachable_non_generic(def_id) && tcx.def_kind(def_id).is_fn_like())
|| entry_fn == Some(def_id)
});
let model_path = base_filename.with_extension(ArtifactType::SymTabGoto);
let (gcx, items) =
self.codegen_items(tcx, &local_reachable, &model_path, &results.machine_model);
results.extend(gcx, items, None);
}
}

if reachability != ReachabilityType::None {
// Print compilation report.
results.print_report(tcx);

if reachability != ReachabilityType::Harnesses {
// In a workspace, cargo seems to be using the same file prefix to build a crate that is
// a package lib and also a dependency of another package.
// To avoid overriding the metadata for its verification, we skip this step when
// reachability is None, even because there is nothing to record.
write_file(
&base_filename,
ArtifactType::Metadata,
&results.generate_metadata(),
queries.args().output_pretty_json,
);
if reachability != ReachabilityType::None {
// Print compilation report.
results.print_report(tcx);

if reachability != ReachabilityType::Harnesses {
// In a workspace, cargo seems to be using the same file prefix to build a crate that is
// a package lib and also a dependency of another package.
// To avoid overriding the metadata for its verification, we skip this step when
// reachability is None, even because there is nothing to record.
write_file(
&base_filename,
ArtifactType::Metadata,
&results.generate_metadata(),
queries.args().output_pretty_json,
);
}
}
}
codegen_results(tcx, rustc_metadata, &results.machine_model)
codegen_results(tcx, rustc_metadata, &results.machine_model)
});
ret_val.unwrap()
}

fn join_codegen(
Expand Down
43 changes: 18 additions & 25 deletions kani-compiler/src/kani_middle/analysis.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,31 +23,24 @@ use std::fmt::Display;
/// - Number of items per type (Function / Constant / Shims)
/// - Number of instructions per type.
/// - Total number of MIR instructions.
pub fn print_stats<'tcx>(tcx: TyCtxt<'tcx>, items: &[InternalMonoItem<'tcx>]) {
rustc_internal::run(tcx, || {
let items: Vec<MonoItem> = items.iter().map(rustc_internal::stable).collect();
let item_types = items.iter().collect::<Counter>();
let visitor = items
.iter()
.filter_map(
|mono| {
if let MonoItem::Fn(instance) = mono { Some(instance) } else { None }
},
)
.fold(StatsVisitor::default(), |mut visitor, body| {
visitor.visit_body(&body.body().unwrap());
visitor
});
eprintln!("====== Reachability Analysis Result =======");
eprintln!("Total # items: {}", item_types.total());
eprintln!("Total # statements: {}", visitor.stmts.total());
eprintln!("Total # expressions: {}", visitor.exprs.total());
eprintln!("\nReachable Items:\n{item_types}");
eprintln!("Statements:\n{}", visitor.stmts);
eprintln!("Expressions:\n{}", visitor.exprs);
eprintln!("-------------------------------------------")
})
.unwrap();
pub fn print_stats<'tcx>(_tcx: TyCtxt<'tcx>, items: &[InternalMonoItem<'tcx>]) {
let items: Vec<MonoItem> = items.iter().map(rustc_internal::stable).collect();
let item_types = items.iter().collect::<Counter>();
let visitor = items
.iter()
.filter_map(|mono| if let MonoItem::Fn(instance) = mono { Some(instance) } else { None })
.fold(StatsVisitor::default(), |mut visitor, body| {
visitor.visit_body(&body.body().unwrap());
visitor
});
eprintln!("====== Reachability Analysis Result =======");
eprintln!("Total # items: {}", item_types.total());
eprintln!("Total # statements: {}", visitor.stmts.total());
eprintln!("Total # expressions: {}", visitor.exprs.total());
eprintln!("\nReachable Items:\n{item_types}");
eprintln!("Statements:\n{}", visitor.stmts);
eprintln!("Expressions:\n{}", visitor.exprs);
eprintln!("-------------------------------------------")
}

#[derive(Default)]
Expand Down

0 comments on commit 9d01f97

Please sign in to comment.