From 9d01f97978c9295feebb2c1e26d26dbe736f9e9d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=C4=9Fuz=20A=C4=9Fcayaz=C4=B1?= Date: Wed, 29 Nov 2023 22:02:08 +0300 Subject: [PATCH] Make `codegen_span` stable (#2882) Follow up pr to https://github.com/model-checking/kani/pull/2871 as `stable_mir::ty::Span` have ability to `get_filename` and `get_lineinfo` we could start adopting it. --- .../src/codegen_cprover_gotoc/codegen/span.rs | 11 +- .../compiler_interface.rs | 195 +++++++++--------- kani-compiler/src/kani_middle/analysis.rs | 43 ++-- 3 files changed, 129 insertions(+), 120 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 27f47ed457c9..9f88bbbe7b55 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -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), diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index f0021c14e9d7..df472518c9a3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -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; @@ -208,105 +209,115 @@ impl CodegenBackend for GotocCodegenBackend { rustc_metadata: EncodedMetadata, _need_metadata_module: bool, ) -> Box { - 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 = 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 = 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( diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index 61d0b4c9acfe..011907c14ea4 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -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 = items.iter().map(rustc_internal::stable).collect(); - let item_types = items.iter().collect::(); - 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 = items.iter().map(rustc_internal::stable).collect(); + let item_types = items.iter().collect::(); + 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)]