Add initial implementation of the reachability algorithm #1683
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -3,16 +3,18 @@ | |
|
|
||
| //! This file contains the code necessary to interface with the compiler backend | ||
|
|
||
| use crate::codegen_cprover_gotoc::reachability::{collect_reachable_items, filter_crate_items}; | ||
| use crate::codegen_cprover_gotoc::GotocCtx; | ||
| use bitflags::_core::any::Any; | ||
| use cbmc::goto_program::{symtab_transformer, Location}; | ||
| use cbmc::{InternedString, MachineModel}; | ||
| use kani_metadata::KaniMetadata; | ||
| use kani_queries::{QueryDb, ReachabilityType, UserInput}; | ||
| use rustc_codegen_ssa::traits::CodegenBackend; | ||
| use rustc_codegen_ssa::{CodegenResults, CrateInfo}; | ||
| use rustc_data_structures::fx::FxHashMap; | ||
| use rustc_errors::ErrorGuaranteed; | ||
| use rustc_hir::def::DefKind; | ||
| use rustc_metadata::EncodedMetadata; | ||
| use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; | ||
| use rustc_middle::mir::mono::{CodegenUnit, MonoItem}; | ||
|
|
@@ -51,104 +53,92 @@ impl CodegenBackend for GotocCodegenBackend { | |
|
|
||
| fn provide_extern(&self, _providers: &mut ty::query::ExternProviders) {} | ||
|
|
||
| fn codegen_crate( | ||
| &self, | ||
| tcx: TyCtxt, | ||
| rustc_metadata: EncodedMetadata, | ||
| need_metadata_module: bool, | ||
| ) -> Box<dyn Any> { | ||
| super::utils::init(); | ||
|
|
||
| // Follow rustc naming convention (cx is abbrev for context). | ||
| // https://rustc-dev-guide.rust-lang.org/conventions.html#naming-conventions | ||
| let mut gcx = GotocCtx::new(tcx, self.queries.clone()); | ||
celinval marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| check_target(tcx.sess); | ||
| check_options(tcx.sess, need_metadata_module); | ||
| check_crate_items(&gcx); | ||
|
|
||
| let items = collect_codegen_items(&gcx); | ||
| if items.is_empty() { | ||
| // There's nothing to do. | ||
| return codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model()); | ||
| } | ||
|
|
||
| // we first declare all functions | ||
|
|
||
| for item in &items { | ||
| match *item { | ||
| MonoItem::Fn(instance) => { | ||
| gcx.call_with_panic_debug_info( | ||
| |ctx| ctx.declare_function(instance), | ||
| format!("declare_function: {}", gcx.readable_instance_name(instance)), | ||
| instance.def_id(), | ||
| ); | ||
| } | ||
| MonoItem::Static(def_id) => { | ||
| gcx.call_with_panic_debug_info( | ||
| |ctx| ctx.declare_static(def_id, *item), | ||
| format!("declare_static: {:?}", def_id), | ||
| def_id, | ||
| ); | ||
| } | ||
| MonoItem::GlobalAsm(_) => {} // Ignore this. We have already warned about it. | ||
| } | ||
| } | ||
|
|
||
| // then we move on to codegen | ||
| for item in items { | ||
| match item { | ||
| MonoItem::Fn(instance) => { | ||
| gcx.call_with_panic_debug_info( | ||
| |ctx| ctx.codegen_function(instance), | ||
| format!( | ||
| "codegen_function: {}\n{}", | ||
| gcx.readable_instance_name(instance), | ||
| gcx.symbol_name(instance) | ||
| ), | ||
| instance.def_id(), | ||
| ); | ||
| } | ||
| MonoItem::Static(def_id) => { | ||
| gcx.call_with_panic_debug_info( | ||
| |ctx| ctx.codegen_static(def_id, item), | ||
| format!("codegen_static: {:?}", def_id), | ||
| def_id, | ||
| ); | ||
| } | ||
| MonoItem::GlobalAsm(_) => {} // We have already warned above | ||
| } | ||
| } | ||
|
|
||
| // Print compilation report. | ||
| print_report(&gcx, tcx); | ||
|
|
||
| // perform post-processing symbol table passes | ||
| let passes = self.queries.get_symbol_table_passes(); | ||
| let symtab = symtab_transformer::do_passes(gcx.symbol_table, &passes); | ||
|
|
||
| // Map MIR types to GotoC types | ||
| let type_map: BTreeMap<InternedString, InternedString> = | ||
| BTreeMap::from_iter(gcx.type_map.into_iter().map(|(k, v)| (k, v.to_string().into()))); | ||
|
|
||
| // Get the vtable function pointer restrictions if requested | ||
| let vtable_restrictions = if gcx.vtable_ctx.emit_vtable_restrictions { | ||
| Some(gcx.vtable_ctx.get_virtual_function_restrictions()) | ||
| } else { | ||
| None | ||
| }; | ||
|
|
||
| let metadata = KaniMetadata { proof_harnesses: gcx.proof_harnesses }; | ||
|
|
||
| // No output should be generated if user selected no_codegen. | ||
| if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { | ||
|
|
@@ -163,18 +153,7 @@ impl CodegenBackend for GotocCodegenBackend { | |
| write_file(&base_filename, "restrictions.json", &restrictions, pretty); | ||
| } | ||
| } | ||
| codegen_results(tcx, rustc_metadata, symtab.machine_model()) | ||
| } | ||
|
|
||
| fn join_codegen( | ||
|
|
@@ -246,7 +225,7 @@ fn check_target(session: &Session) { | |
| session.abort_if_errors(); | ||
| } | ||
|
|
||
| fn check_options(session: &Session, need_metadata_module: bool) { | ||
| // The requirements for `min_global_align` and `endian` are needed to build | ||
| // a valid CBMC machine model in function `machine_model_from_session` from | ||
| // src/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs | ||
|
|
@@ -281,17 +260,37 @@ fn check_options(session: &Session, need_metadata_module: bool, queries: Rc<Quer | |
| session.err("Kani cannot generate metadata module."); | ||
| } | ||
|
|
||
| session.abort_if_errors(); | ||
| } | ||
|
|
||
| /// Check that all crate items are supported and there's no misconfiguration. | ||
| /// This method will exhaustively print any error / warning and it will abort at the end if any | ||
| /// error was found. | ||
| fn check_crate_items(gcx: &GotocCtx) { | ||
| let tcx = gcx.tcx; | ||
| for item in tcx.hir_crate_items(()).items() { | ||
| let def_id = item.def_id.to_def_id(); | ||
| gcx.check_attributes(def_id); | ||
| if tcx.def_kind(def_id) == DefKind::GlobalAsm { | ||
| if !gcx.queries.get_ignore_global_asm() { | ||
| let error_msg = format!( | ||
| "Crate {} contains global ASM, which is not supported by Kani. Rerun with \ | ||
| `--enable-unstable --ignore-global-asm` to suppress this error \ | ||
| (**Verification results may be impacted**).", | ||
| gcx.short_crate_name() | ||
| ); | ||
| tcx.sess.err(&error_msg); | ||
| } else { | ||
| warn!( | ||
| "Ignoring global ASM in crate {}. Verification results may be impacted.", | ||
| gcx.short_crate_name() | ||
| ); | ||
| } | ||
| } | ||
| } | ||
| tcx.sess.abort_if_errors(); | ||
| } | ||
|
|
||
| fn write_file<T>(base_filename: &Path, extension: &str, source: &T, pretty: bool) | ||
| where | ||
| T: serde::Serialize, | ||
|
|
@@ -327,3 +326,56 @@ fn print_report<'tcx>(ctx: &GotocCtx, tcx: TyCtxt<'tcx>) { | |
| tcx.sess.warn(&msg); | ||
| } | ||
| } | ||
|
|
||
| /// Return a struct that contains information about the codegen results as expected by `rustc`. | ||
| fn codegen_results( | ||
celinval marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| tcx: TyCtxt, | ||
| rustc_metadata: EncodedMetadata, | ||
| machine: &MachineModel, | ||
| ) -> Box<dyn Any> { | ||
| let work_products = FxHashMap::<WorkProductId, WorkProduct>::default(); | ||
| Box::new(( | ||
| CodegenResults { | ||
| modules: vec![], | ||
| allocator_module: None, | ||
| metadata_module: None, | ||
| metadata: rustc_metadata, | ||
| crate_info: CrateInfo::new(tcx, machine.architecture.clone()), | ||
| }, | ||
| work_products, | ||
| )) | ||
| } | ||
|
|
||
| /// Retrieve all items that need to be processed. | ||
| fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec<MonoItem<'tcx>> { | ||
| let tcx = gcx.tcx; | ||
| let reach = gcx.queries.get_reachability_analysis(); | ||
| debug!(?reach, "starting_points"); | ||
| match reach { | ||
| ReachabilityType::Legacy => { | ||
|
There was a problem hiding this comment. Well.. this slice on the public items and it is not cross crate. |
||
| // Use rustc monomorphizer to retrieve items to codegen. | ||
| let codegen_units: &'tcx [CodegenUnit<'_>] = tcx.collect_and_partition_mono_items(()).1; | ||
| codegen_units | ||
| .iter() | ||
| .flat_map(|cgu| cgu.items_in_deterministic_order(tcx)) | ||
| .map(|(item, _)| item) | ||
|
There was a problem hiding this comment. Do we want to run There was a problem hiding this comment. From our offline conversation, I'll use uniq here and remove this code: kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs Lines 93 to 94 in a2ecd4b There was a problem hiding this comment. I couldn't find any |
||
| .collect() | ||
| } | ||
| ReachabilityType::Harnesses => { | ||
| // Cross-crate collecting of all items that are reachable from the crate harnesses. | ||
| let harnesses = filter_crate_items(tcx, |_, def_id| gcx.is_proof_harness(def_id)); | ||
| collect_reachable_items(tcx, &harnesses).into_iter().collect() | ||
| } | ||
| ReachabilityType::None => Vec::new(), | ||
|
There was a problem hiding this comment. Nope... this is needed to build dependencies. You can see more details here: https://model-checking.github.io/kani/rfc/rfcs/0001-mir-linker.html#cross-crate-reachability-analysis |
||
| ReachabilityType::PubFns => { | ||
| // TODO: https://github.com/model-checking/kani/issues/1674 | ||
| let err_msg = format!( | ||
| "Using {} reachability mode is still unsupported.", | ||
| ReachabilityType::PubFns.as_ref() | ||
| ); | ||
| tcx.sess.err(&err_msg); | ||
celinval marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| tcx.sess.abort_if_errors(); | ||
| unreachable!("Session should've been aborted") | ||
| } | ||
| } | ||
| } | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.