Skip to content
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

Jump to bottom

Make codegen_span stable #2882

Merged
merged 3 commits into from
Nov 29, 2023
Merged

Make codegen_span stable #2882

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
f6c4ba4
Make codegen_span stable
ouz-a Nov 16, 2023
042615e
move init to `codegen_crate`
ouz-a Nov 29, 2023
dae87f2
Merge branch 'main' into stable_codegen_span
celinval Nov 29, 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
11 changes: 8 additions & 3 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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