diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs index c9e34b36257c..4eb1a0720f22 100644 --- a/cprover_bindings/src/irep/goto_binary_serde.rs +++ b/cprover_bindings/src/irep/goto_binary_serde.rs @@ -9,7 +9,7 @@ use std::fs::File; use std::hash::Hash; use std::io::{self, BufReader}; use std::io::{BufWriter, Bytes, Error, ErrorKind, Read, Write}; -use std::path::PathBuf; +use std::path::Path; /// Writes a symbol table to a file in goto binary format in version 5. /// @@ -18,7 +18,7 @@ use std::path::PathBuf; /// - src/util/irep_serialization.h /// - src/util/irep_hash_container.h /// - src/util/irep_hash.h -pub fn write_goto_binary_file(filename: &PathBuf, source: &crate::goto_program::SymbolTable) { +pub fn write_goto_binary_file(filename: &Path, source: &crate::goto_program::SymbolTable) { let out_file = File::create(filename).unwrap(); let mut writer = BufWriter::new(out_file); let mut serializer = GotoBinarySerializer::new(&mut writer); @@ -33,7 +33,7 @@ pub fn write_goto_binary_file(filename: &PathBuf, source: &crate::goto_program:: /// - src/util/irep_serialization.h /// - src/util/irep_hash_container.h /// - src/util/irep_hash.h -pub fn read_goto_binary_file(filename: &PathBuf) -> io::Result<()> { +pub fn read_goto_binary_file(filename: &Path) -> io::Result<()> { let file = File::open(filename)?; let reader = BufReader::new(file); let mut deserializer = GotoBinaryDeserializer::new(reader); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index b7c98a4a2314..cdab6d58251f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -4,10 +4,8 @@ //! This file contains functions related to codegenning MIR functions into gotoc use crate::codegen_cprover_gotoc::GotocCtx; -use crate::kani_middle::attributes::{extract_harness_attributes, is_test_harness_closure}; use cbmc::goto_program::{Expr, Stmt, Symbol}; use cbmc::InternString; -use kani_metadata::{HarnessAttributes, HarnessMetadata}; use rustc_middle::mir::traversal::reverse_postorder; use rustc_middle::mir::{Body, HasLocalDecls, Local}; use rustc_middle::ty::{self, Instance}; @@ -89,9 +87,6 @@ impl<'tcx> GotocCtx<'tcx> { let stmts = self.current_fn_mut().extract_block(); let body = Stmt::block(stmts, loc); self.symbol_table.update_fn_declaration_with_definition(&name, body); - - self.record_kani_attributes(); - self.record_test_harness_metadata(); } self.reset_current_fn(); } @@ -244,50 +239,4 @@ impl<'tcx> GotocCtx<'tcx> { }); self.reset_current_fn(); } - - /// We record test harness information in kani-metadata, just like we record - /// proof harness information. This is used to support e.g. cargo-kani assess. - /// - /// Note that we do not actually spot the function that was annotated by `#[test]` - /// but instead the closure that gets put into the "test description" that macro - /// expands into. (See comment below) This ends up being preferrable, actually, - /// as it add asserts for tests that return `Result` types. - fn record_test_harness_metadata(&mut self) { - let def_id = self.current_fn().instance().def_id(); - if is_test_harness_closure(self.tcx, def_id) { - self.test_harnesses.push(self.generate_metadata(None)) - } - } - - /// This updates the goto context with any information that should be accumulated from a function's - /// attributes. - /// - /// Handle all attributes i.e. `#[kani::x]` (which kani_macros translates to `#[kanitool::x]` for us to handle here) - fn record_kani_attributes(&mut self) { - let def_id = self.current_fn().instance().def_id(); - let attributes = extract_harness_attributes(self.tcx, def_id); - if attributes.is_some() { - self.proof_harnesses.push(self.generate_metadata(attributes)); - } - } - - /// Create the default proof harness for the current function - fn generate_metadata(&self, attributes: Option) -> HarnessMetadata { - let current_fn = self.current_fn(); - let pretty_name = current_fn.readable_name().to_owned(); - let mangled_name = current_fn.name(); - let loc = self.codegen_span(¤t_fn.mir().span); - - HarnessMetadata { - pretty_name, - mangled_name, - crate_name: current_fn.krate(), - original_file: loc.filename().unwrap(), - original_start_line: loc.start_line().unwrap() as usize, - original_end_line: loc.end_line().unwrap() as usize, - attributes: attributes.unwrap_or_default(), - // We record the actual path after codegen before we dump the metadata into a file. - goto_file: None, - } - } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 2c333daf89eb..72c9e258c14d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -3,32 +3,21 @@ //! MIR Span related functions -use crate::codegen_cprover_gotoc::GotocCtx; +use crate::{codegen_cprover_gotoc::GotocCtx, kani_middle::SourceLocation}; use cbmc::goto_program::Location; use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents}; use rustc_span::Span; impl<'tcx> GotocCtx<'tcx> { pub fn codegen_span(&self, sp: &Span) -> Location { - let smap = self.tcx.sess.source_map(); - let lo = smap.lookup_char_pos(sp.lo()); - let start_line = lo.line; - let start_col = 1 + lo.col_display; - let hi = smap.lookup_char_pos(sp.hi()); - let end_line = hi.line; - let end_col = 1 + hi.col_display; - let filename0 = lo.file.name.prefer_local().to_string_lossy().to_string(); - let filename1 = match std::fs::canonicalize(filename0.clone()) { - Ok(pathbuf) => pathbuf.to_str().unwrap().to_string(), - Err(_) => filename0, - }; + let loc = SourceLocation::new(self.tcx, sp); Location::new( - filename1, + loc.filename, self.current_fn.as_ref().map(|x| x.readable_name().to_string()), - start_line, - Some(start_col), - end_line, - Some(end_col), + loc.start_line, + Some(loc.start_col), + loc.end_line, + Some(loc.end_col), ) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 9df0797d9d51..fbd8b583a820 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -10,14 +10,18 @@ use crate::kani_middle::attributes::is_proof_harness; use crate::kani_middle::attributes::is_test_harness_description; use crate::kani_middle::check_crate_items; use crate::kani_middle::check_reachable_items; +use crate::kani_middle::metadata::{gen_proof_metadata, gen_test_metadata}; use crate::kani_middle::provide; use crate::kani_middle::reachability::{ collect_reachable_items, filter_const_crate_items, filter_crate_items, }; use cbmc::goto_program::Location; use cbmc::irep::goto_binary_serde::write_goto_binary_file; +use cbmc::RoundingMode; use cbmc::{InternedString, MachineModel}; +use kani_metadata::artifact::convert_type; use kani_metadata::CompilerArtifactStub; +use kani_metadata::UnsupportedFeature; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; use kani_queries::{QueryDb, ReachabilityType, UserInput}; use rustc_codegen_ssa::back::metadata::create_wrapper_file; @@ -56,6 +60,7 @@ use std::time::Instant; use tempfile::Builder as TempFileBuilder; use tracing::{debug, error, info}; +pub type UnsupportedConstructs = FxHashMap>; #[derive(Clone)] pub struct GotocCodegenBackend { /// The query is shared with `KaniCompiler` and it is initialized as part of `rustc` @@ -69,46 +74,24 @@ impl GotocCodegenBackend { pub fn new(queries: Arc>) -> Self { GotocCodegenBackend { queries } } -} - -impl CodegenBackend for GotocCodegenBackend { - fn metadata_loader(&self) -> Box { - Box::new(rustc_codegen_ssa::back::metadata::DefaultMetadataLoader) - } - - fn provide(&self, providers: &mut Providers) { - provide::provide(providers, &self.queries.lock().unwrap()); - } - - fn provide_extern(&self, providers: &mut ty::query::ExternProviders) { - provide::provide_extern(providers); - } - - fn print_version(&self) { - println!("Kani-goto version: {}", env!("CARGO_PKG_VERSION")); - } - fn codegen_crate( + /// Generate code that is reachable from the given starting points. + fn codegen_items<'tcx>( &self, - tcx: TyCtxt, - rustc_metadata: EncodedMetadata, - _need_metadata_module: bool, - ) -> Box { - super::utils::init(); + tcx: TyCtxt<'tcx>, + starting_items: &[MonoItem<'tcx>], + symtab_goto: &Path, + machine_model: &MachineModel, + ) -> (GotocCtx<'tcx>, Vec>) { + let items = with_timer( + || collect_reachable_items(tcx, starting_items), + "codegen reachability analysis", + ); + dump_mir_items(tcx, &items); // 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.lock().unwrap()).clone()); - check_target(tcx.sess); - check_options(tcx.sess); - check_crate_items(gcx.tcx, gcx.queries.get_ignore_global_asm()); - - let items = with_timer(|| collect_codegen_items(&gcx), "codegen reachability analysis"); - if items.is_empty() { - // There's nothing to do. - return codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model()); - } - dump_mir_items(tcx, &items); + let mut gcx = GotocCtx::new(tcx, (*self.queries.lock().unwrap()).clone(), machine_model); check_reachable_items(gcx.tcx, &gcx.queries, &items); with_timer( @@ -165,12 +148,6 @@ impl CodegenBackend for GotocCodegenBackend { "codegen", ); - // Print compilation report. - print_report(&gcx, tcx); - - // Print some compilation stats. - print_stats(&gcx, tcx, &items); - // Map from name to prettyName for all symbols let pretty_name_map: BTreeMap> = BTreeMap::from_iter(gcx.symbol_table.iter().map(|(k, s)| (*k, s.pretty_name))); @@ -186,31 +163,132 @@ impl CodegenBackend for GotocCodegenBackend { None }; - let metadata = generate_metadata(&gcx, tcx); - // 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() { - let outputs = tcx.output_filenames(()); - let base_filename = outputs.output_path(OutputType::Object); let pretty = self.queries.lock().unwrap().get_output_pretty_json(); - write_file(&base_filename, ArtifactType::PrettyNameMap, &pretty_name_map, pretty); + write_file(&symtab_goto, ArtifactType::PrettyNameMap, &pretty_name_map, pretty); if gcx.queries.get_write_json_symtab() { - write_file(&base_filename, ArtifactType::SymTab, &gcx.symbol_table, pretty); - symbol_table_to_gotoc(&tcx, &base_filename); + write_file(&symtab_goto, ArtifactType::SymTab, &gcx.symbol_table, pretty); + symbol_table_to_gotoc(&tcx, &symtab_goto); } else { - write_goto_binary_file( - &base_filename.with_extension(ArtifactType::SymTabGoto), - &gcx.symbol_table, - ); + write_goto_binary_file(symtab_goto, &gcx.symbol_table); } - write_file(&base_filename, ArtifactType::TypeMap, &type_map, pretty); - write_file(&base_filename, ArtifactType::Metadata, &metadata, pretty); + write_file(&symtab_goto, ArtifactType::TypeMap, &type_map, pretty); // If they exist, write out vtable virtual call function pointer restrictions if let Some(restrictions) = vtable_restrictions { - write_file(&base_filename, ArtifactType::VTableRestriction, &restrictions, pretty); + write_file(&symtab_goto, ArtifactType::VTableRestriction, &restrictions, pretty); + } + } + + (gcx, items) + } +} + +impl CodegenBackend for GotocCodegenBackend { + fn metadata_loader(&self) -> Box { + Box::new(rustc_codegen_ssa::back::metadata::DefaultMetadataLoader) + } + + fn provide(&self, providers: &mut Providers) { + provide::provide(providers, &self.queries.lock().unwrap()); + } + + fn provide_extern(&self, providers: &mut ty::query::ExternProviders) { + provide::provide_extern(providers); + } + + fn print_version(&self) { + println!("Kani-goto version: {}", env!("CARGO_PKG_VERSION")); + } + + fn codegen_crate( + &self, + tcx: TyCtxt, + 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); + check_crate_items(tcx, queries.get_ignore_global_asm()); + + // 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.get_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 = filter_crate_items(tcx, |_, def_id| is_proof_harness(tcx, def_id)); + for harness in harnesses { + let metadata = gen_proof_metadata(tcx, harness.def_id(), &base_filename); + let model_path = &metadata.goto_file.as_ref().unwrap(); + let (gcx, items) = + self.codegen_items(tcx, &[harness], model_path, &results.machine_model); + results.extend(gcx, items, Some(metadata)); + } + } + 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 model_path = &metadata.goto_file.as_ref().unwrap(); + let (gcx, items) = + self.codegen_items(tcx, &[*test_fn], model_path, &results.machine_model); + results.extend(gcx, items, Some(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); } } - codegen_results(tcx, rustc_metadata, gcx.symbol_table.machine_model()) + + if reachability != ReachabilityType::None { + // Print compilation report. + results.print_report(tcx); + + // 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.get_output_pretty_json(), + ); + } + codegen_results(tcx, rustc_metadata, &results.machine_model) } fn join_codegen( @@ -336,38 +414,6 @@ fn check_options(session: &Session) { session.abort_if_errors(); } -/// Prints a report at the end of the compilation. -fn print_report(ctx: &GotocCtx, tcx: TyCtxt) { - // Print all unsupported constructs. - if !ctx.unsupported_constructs.is_empty() { - // Sort alphabetically. - let unsupported: BTreeMap> = ctx - .unsupported_constructs - .iter() - .map(|(key, val)| (key.map(|s| String::from(s)), val)) - .collect(); - let mut msg = String::from("Found the following unsupported constructs:\n"); - unsupported.iter().for_each(|(construct, locations)| { - writeln!(&mut msg, " - {construct} ({})", locations.len()).unwrap(); - }); - msg += "\nVerification will fail if one or more of these constructs is reachable."; - msg += "\nSee https://model-checking.github.io/kani/rust-feature-support.html for more \ - details."; - tcx.sess.warn(&msg); - } - - if !ctx.concurrent_constructs.is_empty() { - let mut msg = String::from( - "Kani currently does not support concurrency. The following constructs will be treated \ - as sequential operations:\n", - ); - for (construct, locations) in ctx.concurrent_constructs.iter() { - writeln!(&mut msg, " - {construct} ({})", locations.len()).unwrap(); - } - tcx.sess.warn(&msg); - } -} - /// Return a struct that contains information about the codegen results as expected by `rustc`. fn codegen_results( tcx: TyCtxt, @@ -387,47 +433,9 @@ fn codegen_results( )) } -/// Retrieve all items that need to be processed according to the selected reachability mode: -/// -/// - Harnesses: Cross-crate collection of all reachable items starting from local harnesses. -/// - None: Skip collection and codegen all together. This is used to compile dependencies. -/// - Legacy: Use regular compiler collection that will collect local items, and a few cross -/// crate items (such as generic functions and functions candidate to be inlined). -/// - PubFns: Cross-crate reachability analysis that use the local public fns as starting point. -/// - Tests: Cross-crate collection of all reachable items starting from test harnesses. -fn collect_codegen_items<'tcx>(gcx: &GotocCtx<'tcx>) -> Vec> { - let tcx = gcx.tcx; - let reach = gcx.queries.get_reachability_analysis(); - debug!(?reach, "collect_codegen_items"); - match reach { - ReachabilityType::Harnesses => { - // Cross-crate collecting of all items that are reachable from the crate harnesses. - let harnesses = filter_crate_items(tcx, |_, def_id| is_proof_harness(gcx.tcx, def_id)); - collect_reachable_items(tcx, &harnesses).into_iter().collect() - } - 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 - let harnesses = filter_const_crate_items(tcx, |_, def_id| { - is_test_harness_description(gcx.tcx, def_id) - }); - collect_reachable_items(tcx, &harnesses).into_iter().collect() - } - ReachabilityType::None => Vec::new(), - 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) - }); - collect_reachable_items(tcx, &local_reachable).into_iter().collect() - } - } -} - -fn symbol_table_to_gotoc(tcx: &TyCtxt, file: &Path) -> PathBuf { - let output_filename = file.with_extension(ArtifactType::SymTabGoto); - let input_filename = file.with_extension(ArtifactType::SymTab); +fn symbol_table_to_gotoc(tcx: &TyCtxt, base_path: &Path) -> PathBuf { + let output_filename = base_path.to_path_buf(); + let input_filename = convert_type(base_path, ArtifactType::SymTabGoto, ArtifactType::SymTab); let args = vec![ input_filename.clone().into_os_string(), @@ -490,40 +498,11 @@ fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem]) { } } -/// Print statistics about the MIR used as input to code generation as well as the emitted goto. -/// TODO: Print stats for the goto. -fn print_stats<'tcx>(_ctx: &GotocCtx, tcx: TyCtxt<'tcx>, items: &[MonoItem<'tcx>]) { - if tracing::enabled!(tracing::Level::INFO) { - analysis::print_stats(tcx, items); - } -} - -/// Method that generates `KaniMetadata` from the given compilation context. -/// This is a temporary method used until we generate a model per-harness. -/// See for more details. -fn generate_metadata(gcx: &GotocCtx, tcx: TyCtxt) -> KaniMetadata { - let outputs = tcx.output_filenames(()); - let model_file = - outputs.output_path(OutputType::Object).with_extension(ArtifactType::SymTabGoto); - let extend_harnesses = |mut harnesses: Vec| { - for harness in harnesses.iter_mut() { - harness.goto_file = Some(model_file.clone()); - } - harnesses - }; - KaniMetadata { - crate_name: tcx.crate_name(LOCAL_CRATE).to_string(), - proof_harnesses: extend_harnesses(gcx.proof_harnesses.clone()), - unsupported_features: gcx.unsupported_metadata(), - test_harnesses: extend_harnesses(gcx.test_harnesses.clone()), - } -} - pub fn write_file(base_path: &Path, file_type: ArtifactType, source: &T, pretty: bool) where T: serde::Serialize, { - let filename = base_path.with_extension(file_type); + let filename = convert_type(base_path, ArtifactType::SymTabGoto, file_type); debug!(?filename, "write_json"); let out_file = File::create(&filename).unwrap(); let writer = BufWriter::new(out_file); @@ -534,6 +513,228 @@ where } } +struct GotoCodegenResults<'tcx> { + reachability: ReachabilityType, + harnesses: Vec, + unsupported_constructs: UnsupportedConstructs, + concurrent_constructs: UnsupportedConstructs, + items: Vec>, + crate_name: InternedString, + machine_model: MachineModel, +} + +impl<'tcx> GotoCodegenResults<'tcx> { + pub fn new(tcx: TyCtxt, reachability: ReachabilityType) -> Self { + GotoCodegenResults { + reachability, + harnesses: vec![], + unsupported_constructs: UnsupportedConstructs::default(), + concurrent_constructs: UnsupportedConstructs::default(), + items: vec![], + crate_name: tcx.crate_name(LOCAL_CRATE).as_str().into(), + machine_model: new_machine_model(tcx.sess), + } + } + /// Method that generates `KaniMetadata` from the given compilation results. + pub fn generate_metadata(&self) -> KaniMetadata { + // Maps the goto-context "unsupported features" data into the KaniMetadata "unsupported features" format. + // TODO: Do we really need different formats?? + let unsupported_features = self + .unsupported_constructs + .iter() + .map(|(construct, location)| UnsupportedFeature { + feature: construct.to_string(), + locations: location + .iter() + .map(|l| { + // We likely (and should) have no instances of + // calling `codegen_unimplemented` without file/line. + // So while we map out of `Option` here, we expect them to always be `Some` + kani_metadata::Location { + filename: l.filename().unwrap_or_default(), + start_line: l.start_line().unwrap_or_default(), + } + }) + .collect(), + }) + .collect(); + let (proofs, tests) = if self.reachability == ReachabilityType::Harnesses { + (self.harnesses.clone(), vec![]) + } else { + (vec![], self.harnesses.clone()) + }; + KaniMetadata { + crate_name: self.crate_name.to_string(), + proof_harnesses: proofs, + unsupported_features, + test_harnesses: tests, + } + } + + fn extend( + &mut self, + gcx: GotocCtx, + items: Vec>, + metadata: Option, + ) { + let mut items = items; + self.harnesses.extend(metadata.into_iter()); + self.concurrent_constructs.extend(gcx.concurrent_constructs.into_iter()); + self.unsupported_constructs.extend(gcx.unsupported_constructs.into_iter()); + self.items.append(&mut items); + } + + /// Prints a report at the end of the compilation. + fn print_report(&self, tcx: TyCtxt<'tcx>) { + // Print all unsupported constructs. + if !self.unsupported_constructs.is_empty() { + // Sort alphabetically. + let unsupported: BTreeMap> = self + .unsupported_constructs + .iter() + .map(|(key, val)| (key.map(|s| String::from(s)), val)) + .collect(); + let mut msg = String::from("Found the following unsupported constructs:\n"); + unsupported.iter().for_each(|(construct, locations)| { + writeln!(&mut msg, " - {construct} ({})", locations.len()).unwrap(); + }); + msg += "\nVerification will fail if one or more of these constructs is reachable."; + msg += "\nSee https://model-checking.github.io/kani/rust-feature-support.html for more \ + details."; + tcx.sess.warn(&msg); + } + + if !self.concurrent_constructs.is_empty() { + let mut msg = String::from( + "Kani currently does not support concurrency. The following constructs will be treated \ + as sequential operations:\n", + ); + for (construct, locations) in self.concurrent_constructs.iter() { + writeln!(&mut msg, " - {construct} ({})", locations.len()).unwrap(); + } + tcx.sess.warn(&msg); + } + + // Print some compilation stats. + if tracing::enabled!(tracing::Level::INFO) { + analysis::print_stats(tcx, &self.items); + } + } +} + +/// Builds a machine model which is required by CBMC +fn new_machine_model(sess: &Session) -> MachineModel { + // The model assumes a `x86_64-unknown-linux-gnu`, `x86_64-apple-darwin` + // or `aarch64-apple-darwin` platform. We check the target platform in function + // `check_target` from src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs + // and error if it is not any of the ones we expect. + let architecture = &sess.target.arch; + let pointer_width = sess.target.pointer_width.into(); + + // The model assumes the following values for session options: + // * `min_global_align`: 1 + // * `endian`: `Endian::Little` + // + // We check these options in function `check_options` from + // src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs + // and error if their values are not the ones we expect. + let alignment = sess.target.options.min_global_align.unwrap_or(1); + let is_big_endian = match sess.target.options.endian { + Endian::Little => false, + Endian::Big => true, + }; + + // The values below cannot be obtained from the session so they are + // hardcoded using standard ones for the supported platforms + // see /tools/sizeofs/main.cpp. + // For reference, the definition in CBMC: + //https://github.com/diffblue/cbmc/blob/develop/src/util/config.cpp + match architecture.as_ref() { + "x86_64" => { + let bool_width = 8; + let char_is_unsigned = false; + let char_width = 8; + let double_width = 64; + let float_width = 32; + let int_width = 32; + let long_double_width = 128; + let long_int_width = 64; + let long_long_int_width = 64; + let short_int_width = 16; + let single_width = 32; + let wchar_t_is_unsigned = false; + let wchar_t_width = 32; + + MachineModel { + architecture: architecture.to_string(), + alignment, + bool_width, + char_is_unsigned, + char_width, + double_width, + float_width, + int_width, + is_big_endian, + long_double_width, + long_int_width, + long_long_int_width, + memory_operand_size: int_width / 8, + null_is_zero: true, + pointer_width, + rounding_mode: RoundingMode::ToNearest, + short_int_width, + single_width, + wchar_t_is_unsigned, + wchar_t_width, + word_size: int_width, + } + } + "aarch64" => { + let bool_width = 8; + let char_is_unsigned = true; + let char_width = 8; + let double_width = 64; + let float_width = 32; + let int_width = 32; + let long_double_width = 64; + let long_int_width = 64; + let long_long_int_width = 64; + let short_int_width = 16; + let single_width = 32; + let wchar_t_is_unsigned = false; + let wchar_t_width = 32; + + MachineModel { + // CBMC calls it arm64, not aarch64 + architecture: "arm64".to_string(), + alignment, + bool_width, + char_is_unsigned, + char_width, + double_width, + float_width, + int_width, + is_big_endian, + long_double_width, + long_int_width, + long_long_int_width, + memory_operand_size: int_width / 8, + null_is_zero: true, + pointer_width, + rounding_mode: RoundingMode::ToNearest, + short_int_width, + single_width, + wchar_t_is_unsigned, + wchar_t_width, + word_size: int_width, + } + } + _ => { + panic!("Unsupported architecture: {architecture}"); + } + } +} + /// Execute the provided function and measure the clock time it took for its execution. /// Log the time with the given description. pub fn with_timer(func: F, description: &str) -> T diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 1d9d2fbaa403..b260df32f881 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -17,11 +17,11 @@ use super::current_fn::CurrentFnCtx; use super::vtable_ctx::VtableCtx; use crate::codegen_cprover_gotoc::overrides::{fn_hooks, GotocHooks}; use crate::codegen_cprover_gotoc::utils::full_crate_name; +use crate::codegen_cprover_gotoc::UnsupportedConstructs; use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type}; use cbmc::utils::aggr_tag; -use cbmc::InternedString; -use cbmc::{MachineModel, RoundingMode}; -use kani_metadata::{HarnessMetadata, UnsupportedFeature}; +use cbmc::{InternedString, MachineModel}; +use kani_metadata::HarnessMetadata; use kani_queries::{QueryDb, UserInput}; use rustc_data_structures::fx::FxHashMap; use rustc_data_structures::owning_ref::OwningRef; @@ -35,10 +35,8 @@ use rustc_middle::ty::layout::{ }; use rustc_middle::ty::{self, Instance, Ty, TyCtxt}; use rustc_session::cstore::MetadataLoader; -use rustc_session::Session; use rustc_span::source_map::{respan, Span}; use rustc_target::abi::call::FnAbi; -use rustc_target::abi::Endian; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; use rustc_target::spec::Target; use std::path::Path; @@ -70,19 +68,22 @@ pub struct GotocCtx<'tcx> { /// a global counter for generating unique IDs for checks pub global_checks_count: u64, /// A map of unsupported constructs that were found while codegen - pub unsupported_constructs: FxHashMap>, + pub unsupported_constructs: UnsupportedConstructs, /// A map of concurrency constructs that are treated sequentially. /// We collect them and print one warning at the end if not empty instead of printing one /// warning at each occurrence. - pub concurrent_constructs: FxHashMap>, + pub concurrent_constructs: UnsupportedConstructs, } /// Constructor impl<'tcx> GotocCtx<'tcx> { - pub fn new(tcx: TyCtxt<'tcx>, queries: QueryDb) -> GotocCtx<'tcx> { + pub fn new( + tcx: TyCtxt<'tcx>, + queries: QueryDb, + machine_model: &MachineModel, + ) -> GotocCtx<'tcx> { let fhks = fn_hooks(); - let mm = machine_model_from_session(tcx.sess); - let symbol_table = SymbolTable::new(mm); + let symbol_table = SymbolTable::new(machine_model.clone()); let emit_vtable_restrictions = queries.get_emit_vtable_restrictions(); GotocCtx { tcx, @@ -114,32 +115,6 @@ impl<'tcx> GotocCtx<'tcx> { pub fn current_fn_mut(&mut self) -> &mut CurrentFnCtx<'tcx> { self.current_fn.as_mut().unwrap() } - - /// Maps the goto-context "unsupported features" data into the - /// KaniMetadata "unsupported features" format. - /// - /// These are different because the KaniMetadata is a flat serializable list, - /// while we need a more richly structured HashMap in the goto context. - pub(crate) fn unsupported_metadata(&self) -> Vec { - self.unsupported_constructs - .iter() - .map(|(construct, location)| UnsupportedFeature { - feature: construct.to_string(), - locations: location - .iter() - .map(|l| { - // We likely (and should) have no instances of - // calling `codegen_unimplemented` without file/line. - // So while we map out of `Option` here, we expect them to always be `Some` - kani_metadata::Location { - filename: l.filename().unwrap_or_default(), - start_line: l.start_line().unwrap_or_default(), - } - }) - .collect(), - }) - .collect() - } } /// Generate variables @@ -434,116 +409,3 @@ impl MetadataLoader for GotocMetadataLoader { self.get_rlib_metadata(target, filename) } } - -/// Builds a machine model which is required by CBMC -fn machine_model_from_session(sess: &Session) -> MachineModel { - // The model assumes a `x86_64-unknown-linux-gnu`, `x86_64-apple-darwin` - // or `aarch64-apple-darwin` platform. We check the target platform in function - // `check_target` from src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs - // and error if it is not any of the ones we expect. - let architecture = &sess.target.arch; - let pointer_width = sess.target.pointer_width.into(); - - // The model assumes the following values for session options: - // * `min_global_align`: 1 - // * `endian`: `Endian::Little` - // - // We check these options in function `check_options` from - // src/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs - // and error if their values are not the ones we expect. - let alignment = sess.target.options.min_global_align.unwrap_or(1); - let is_big_endian = match sess.target.options.endian { - Endian::Little => false, - Endian::Big => true, - }; - - // The values below cannot be obtained from the session so they are - // hardcoded using standard ones for the supported platforms - // see /tools/sizeofs/main.cpp. - // For reference, the definition in CBMC: - //https://github.com/diffblue/cbmc/blob/develop/src/util/config.cpp - match architecture.as_ref() { - "x86_64" => { - let bool_width = 8; - let char_is_unsigned = false; - let char_width = 8; - let double_width = 64; - let float_width = 32; - let int_width = 32; - let long_double_width = 128; - let long_int_width = 64; - let long_long_int_width = 64; - let short_int_width = 16; - let single_width = 32; - let wchar_t_is_unsigned = false; - let wchar_t_width = 32; - - MachineModel { - architecture: architecture.to_string(), - alignment, - bool_width, - char_is_unsigned, - char_width, - double_width, - float_width, - int_width, - is_big_endian, - long_double_width, - long_int_width, - long_long_int_width, - memory_operand_size: int_width / 8, - null_is_zero: true, - pointer_width, - rounding_mode: RoundingMode::ToNearest, - short_int_width, - single_width, - wchar_t_is_unsigned, - wchar_t_width, - word_size: int_width, - } - } - "aarch64" => { - let bool_width = 8; - let char_is_unsigned = true; - let char_width = 8; - let double_width = 64; - let float_width = 32; - let int_width = 32; - let long_double_width = 64; - let long_int_width = 64; - let long_long_int_width = 64; - let short_int_width = 16; - let single_width = 32; - let wchar_t_is_unsigned = false; - let wchar_t_width = 32; - - MachineModel { - // CBMC calls it arm64, not aarch64 - architecture: "arm64".to_string(), - alignment, - bool_width, - char_is_unsigned, - char_width, - double_width, - float_width, - int_width, - is_big_endian, - long_double_width, - long_int_width, - long_long_int_width, - memory_operand_size: int_width / 8, - null_is_zero: true, - pointer_width, - rounding_mode: RoundingMode::ToNearest, - short_int_width, - single_width, - wchar_t_is_unsigned, - wchar_t_width, - word_size: int_width, - } - } - _ => { - panic!("Unsupported architecture: {architecture}"); - } - } -} diff --git a/kani-compiler/src/codegen_cprover_gotoc/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/mod.rs index 46bcc8aa33ce..da98c9f07030 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/mod.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/mod.rs @@ -7,6 +7,6 @@ mod context; mod overrides; mod utils; -pub use compiler_interface::GotocCodegenBackend; +pub use compiler_interface::{GotocCodegenBackend, UnsupportedConstructs}; pub use context::GotocCtx; pub use context::VtableCtx; diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 6d6f98cf300b..0a4f5a4c4e8b 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -78,30 +78,11 @@ pub fn is_test_harness_description(tcx: TyCtxt, def_id: DefId) -> bool { tcx.sess.contains_name(attrs, rustc_span::symbol::sym::rustc_test_marker) } -/// Is this the closure inside of a test description const (i.e. macro expanded from a `#[test]`)? -/// -/// We're trying to detect the closure (`||`) inside code like: -/// -/// ```ignore -/// #[rustc_test_marker] -/// pub const check_2: test::TestDescAndFn = test::TestDescAndFn { -/// desc: ..., -/// testfn: test::StaticTestFn(|| test::assert_test_result(check_2())), -/// }; -/// ``` -pub fn is_test_harness_closure(tcx: TyCtxt, def_id: DefId) -> bool { - if !def_id.is_local() { - return false; - } - - let local_def_id = def_id.expect_local(); - let hir_id = tcx.hir().local_def_id_to_hir_id(local_def_id); - - // The parent item of the closure appears to reliably be the `const` declaration item. - let parent_id = tcx.hir().get_parent_item(hir_id); - let parent_def_id = parent_id.to_def_id(); - - is_test_harness_description(tcx, parent_def_id) +/// Extract the test harness name from the `#[rustc_test_maker]` +pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String { + let attrs = tcx.get_attrs_unchecked(def_id); + let marker = tcx.sess.find_by_name(attrs, rustc_span::symbol::sym::rustc_test_marker).unwrap(); + parse_str_value(&marker).unwrap() } /// Extract all Kani attributes for a given `def_id` if any exists. @@ -492,6 +473,16 @@ fn parse_key_values(attr: &Attribute) -> Result, String .collect() } +/// Extracts the string value argument from the attribute provided. +/// +/// For attributes with the following format, this will return a string that represents "VALUE". +/// - `#[attribute = "VALUE"]` +fn parse_str_value(attr: &Attribute) -> Option { + // Vector of meta items , that contain the arguments given the attribute + let value = attr.value_str(); + value.map(|sym| sym.to_string()) +} + /// If the attribute is named `kanitool::name`, this extracts `name` fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { match &attr.kind { diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs new file mode 100644 index 000000000000..de3667c6e6a8 --- /dev/null +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -0,0 +1,69 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module handles Kani metadata generation. For example, generating HarnessMetadata for a +//! given function. + +use std::path::Path; + +use crate::kani_middle::attributes::test_harness_name; +use kani_metadata::{ArtifactType, HarnessAttributes, HarnessMetadata}; +use rustc_hir::def_id::DefId; +use rustc_middle::ty::{Instance, TyCtxt}; + +use super::{attributes::extract_harness_attributes, SourceLocation}; + +/// Create the harness metadata for a proof harness for a given function. +pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> HarnessMetadata { + let attributes = extract_harness_attributes(tcx, def_id); + let pretty_name = tcx.def_path_str(def_id); + // Main function a special case in order to support `--function main` + // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129 + let mangled_name = if pretty_name == "main" { + pretty_name.clone() + } else { + tcx.symbol_name(Instance::mono(tcx, def_id)).to_string() + }; + + let loc = SourceLocation::def_id_loc(tcx, def_id); + let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap()); + let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto); + + HarnessMetadata { + pretty_name, + mangled_name, + crate_name: tcx.crate_name(def_id.krate).to_string(), + original_file: loc.filename, + original_start_line: loc.start_line, + original_end_line: loc.end_line, + attributes: attributes.unwrap_or_default(), + // TODO: This no longer needs to be an Option. + goto_file: Some(model_file), + } +} + +/// Create the harness metadata for a test description. +#[allow(dead_code)] +pub fn gen_test_metadata<'tcx>( + tcx: TyCtxt<'tcx>, + test_desc: DefId, + test_fn: Instance<'tcx>, + base_name: &Path, +) -> HarnessMetadata { + let pretty_name = test_harness_name(tcx, test_desc); + let mangled_name = tcx.symbol_name(test_fn).to_string(); + let loc = SourceLocation::def_id_loc(tcx, test_desc); + let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap()); + let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto); + + HarnessMetadata { + pretty_name, + mangled_name, + crate_name: tcx.crate_name(test_desc.krate).to_string(), + original_file: loc.filename, + original_start_line: loc.start_line, + original_end_line: loc.end_line, + attributes: HarnessAttributes::default(), + // TODO: This no longer needs to be an Option. + goto_file: Some(model_file), + } +} diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index fba7094a3cc4..5405da3ef1b2 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -6,7 +6,10 @@ use std::collections::HashSet; use kani_queries::{QueryDb, UserInput}; -use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE}; +use rustc_hir::{ + def::DefKind, + def_id::{DefId, LOCAL_CRATE}, +}; use rustc_middle::mir::mono::MonoItem; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ @@ -24,6 +27,7 @@ use self::attributes::{check_attributes, check_unstable_features}; pub mod analysis; pub mod attributes; pub mod coercion; +pub mod metadata; pub mod provide; pub mod reachability; pub mod resolve; @@ -72,6 +76,40 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) tcx.sess.abort_if_errors(); } +/// Structure that represents the source location of a definition. +/// TODO: Use `InternedString` once we move it out of the cprover_bindings. +/// +pub struct SourceLocation { + pub filename: String, + pub start_line: usize, + pub start_col: usize, + pub end_line: usize, + pub end_col: usize, +} + +impl SourceLocation { + pub fn new(tcx: TyCtxt, span: &Span) -> Self { + let smap = tcx.sess.source_map(); + let lo = smap.lookup_char_pos(span.lo()); + let start_line = lo.line; + let start_col = 1 + lo.col_display; + let hi = smap.lookup_char_pos(span.hi()); + let end_line = hi.line; + let end_col = 1 + hi.col_display; + let local_filename = lo.file.name.prefer_local().to_string_lossy().to_string(); + let filename = match std::fs::canonicalize(local_filename.clone()) { + Ok(pathbuf) => pathbuf.to_str().unwrap().to_string(), + Err(_) => local_filename, + }; + SourceLocation { filename, start_line, start_col, end_line, end_col } + } + + pub fn def_id_loc(tcx: TyCtxt, def_id: DefId) -> Self { + let span = tcx.def_span(def_id); + Self::new(tcx, &span) + } +} + /// Get the FnAbi of a given instance with no extra variadic arguments. pub fn fn_abi<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> &'tcx FnAbi<'tcx, Ty<'tcx>> { let helper = CompilerHelpers { tcx }; diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 4eb7e9010eeb..df55537b40a3 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -400,8 +400,8 @@ mod tests { let args_both = ["kani", "x.rs", "--default-unwind", "2", "--unwind", "1", "--harness", "check_one"]; - let harness_none = mock_proof_harness("check_one", None, None); - let harness_some = mock_proof_harness("check_one", Some(3), None); + let harness_none = mock_proof_harness("check_one", None, None, None); + let harness_some = mock_proof_harness("check_one", Some(3), None, None); fn resolve(args: &[&str], harness: &HarnessMetadata) -> Option { resolve_unwind_value( diff --git a/kani-driver/src/call_cbmc_viewer.rs b/kani-driver/src/call_cbmc_viewer.rs index 3643b9eda93e..7a352c72dc16 100644 --- a/kani-driver/src/call_cbmc_viewer.rs +++ b/kani-driver/src/call_cbmc_viewer.rs @@ -22,7 +22,8 @@ impl KaniSession { let results_filename = alter_extension(file, "results.xml"); let property_filename = alter_extension(file, "property.xml"); - self.record_temporary_files(&[&results_filename, &property_filename]); + self.record_temporary_file(&results_filename); + self.record_temporary_file(&property_filename); self.cbmc_variant(file, &["--xml-ui", "--trace"], &results_filename, harness_metadata)?; self.cbmc_variant( diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 58096f1953e4..a3565e479a94 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -71,7 +71,7 @@ impl KaniSession { /// Apply --restrict-vtable to a goto binary. pub fn apply_vtable_restrictions(&self, goto_file: &Path, restrictions: &Path) -> Result<()> { let linked_restrictions = alter_extension(goto_file, "linked-restrictions.json"); - self.record_temporary_files(&[&linked_restrictions]); + self.record_temporary_file(&linked_restrictions); collect_and_link_function_pointer_restrictions(restrictions, &linked_restrictions)?; let args: Vec = vec![ diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 82d58bcd63c9..2580d0675bf2 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -57,7 +57,7 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> { let goto_file = self.project.get_harness_artifact(&harness, ArtifactType::Goto).unwrap(); let specialized_obj = specialized_harness_name(goto_file, &harness_filename); - self.sess.record_temporary_files(&[&specialized_obj]); + self.sess.record_temporary_file(&specialized_obj); self.sess.instrument_model( goto_file, &specialized_obj, diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 0e10a3077880..613129d8188c 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use anyhow::Result; -use std::path::Path; +use std::path::{Path, PathBuf}; use tracing::{debug, trace}; use kani_metadata::{ @@ -149,6 +149,7 @@ pub fn mock_proof_harness( name: &str, unwind_value: Option, krate: Option<&str>, + model_file: Option, ) -> HarnessMetadata { HarnessMetadata { pretty_name: name.into(), @@ -158,7 +159,7 @@ pub fn mock_proof_harness( original_start_line: 0, original_end_line: 0, attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() }, - goto_file: None, + goto_file: model_file, } } @@ -192,9 +193,9 @@ mod tests { #[test] fn check_find_proof_harness() { let harnesses = vec![ - mock_proof_harness("check_one", None, None), - mock_proof_harness("module::check_two", None, None), - mock_proof_harness("module::not_check_three", None, None), + mock_proof_harness("check_one", None, None, None), + mock_proof_harness("module::check_two", None, None, None), + mock_proof_harness("module::not_check_three", None, None, None), ]; let ref_harnesses = harnesses.iter().collect::>(); assert_eq!( diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index c7bc6ec32803..adf88c1ba580 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -19,11 +19,10 @@ use crate::metadata::{from_json, merge_kani_metadata, mock_proof_harness}; use crate::session::KaniSession; use crate::util::{crate_name, guess_rlib_name}; -use anyhow::Result; +use anyhow::{Context, Result}; use kani_metadata::{ artifact::convert_type, ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata, }; -use std::collections::HashMap; use std::fs::File; use std::io::BufWriter; use std::ops::Deref; @@ -51,7 +50,7 @@ pub struct Project { /// A flag that indicated whether all artifacts have been merged or not. /// /// This allow us to provide a consistent behavior for `--function`. - /// For these this option, we still merge all the artifacts together, so the + /// For this option, we still merge all the artifacts together, so the /// `merged_artifacts` flag will be set to `true`. /// When this flag is `true`, there should only be up to one artifact of any given type. /// When this flag is `false`, there may be multiple artifacts for any given type. However, @@ -100,6 +99,56 @@ impl Project { && expected_path.as_ref().map_or(true, |goto_file| *goto_file == artifact.path) }) } + + /// Try to build a new project from the build result metadata. + /// + /// This method will parse the metadata in order to gather all artifacts generated by the + /// compiler. + fn try_new( + session: &KaniSession, + outdir: PathBuf, + metadata: Vec, + cargo_metadata: Option, + failed_targets: Option>, + ) -> Result { + // For each harness (test or proof) from each metadata, read the path for the goto + // SymTabGoto file. Use that path to find all the other artifacts. + let mut artifacts = vec![]; + for crate_metadata in &metadata { + for harness_metadata in + crate_metadata.test_harnesses.iter().chain(crate_metadata.proof_harnesses.iter()) + { + let symtab_out = Artifact::try_new( + harness_metadata.goto_file.as_ref().expect("Expected a model file"), + SymTabGoto, + )?; + let goto_path = convert_type(&symtab_out.path, symtab_out.typ, Goto); + + // Link + session.link_goto_binary(&[symtab_out.to_path_buf()], &goto_path)?; + let goto = Artifact::try_new(&goto_path, Goto)?; + + // All other harness artifacts that may have been generated as part of the build. + artifacts.extend([TypeMap, VTableRestriction, PrettyNameMap].iter().filter_map( + |typ| { + let artifact = Artifact::try_from(&symtab_out, *typ).ok()?; + Some(artifact) + }, + )); + artifacts.push(symtab_out); + artifacts.push(goto); + } + } + + Ok(Project { + outdir, + metadata, + artifacts, + merged_artifacts: false, + cargo_metadata, + failed_targets, + }) + } } /// Information about a build artifact. @@ -127,19 +176,26 @@ impl Deref for Artifact { impl Artifact { /// Create a new artifact if the given path exists. pub fn try_new(path: &Path, typ: ArtifactType) -> Result { - Ok(Artifact { path: path.canonicalize()?, typ }) + Ok(Artifact { + path: path.canonicalize().context(format!("Failed to process {}", path.display()))?, + typ, + }) } /// Check if this artifact has the given type. pub fn has_type(&self, typ: ArtifactType) -> bool { self.typ == typ } -} -/// Generate the expected path to a cargo artifact and return it if the artifact actually exists. -fn cargo_artifact(metadata: &Path, typ: ArtifactType) -> Option { - let path = convert_type(metadata, Metadata, typ); - if path.exists() { Artifact::try_new(&path, typ).ok() } else { None } + /// Try to derive an artifact based on a different artifact of a different type. + /// For example: + /// ```no_run + /// let artifact = Artifact::try_new(&"/tmp/file.kani_metadata.json", Metadata).unwrap(); + /// let goto = Artifact::try_from(artifact, Goto); // Will try to create "/tmp/file.goto" + /// ``` + pub fn try_from(artifact: &Artifact, typ: ArtifactType) -> Result { + Self::try_new(&convert_type(&artifact.path, artifact.typ, typ), typ) + } } /// Store the KaniMetadata into a file. @@ -154,32 +210,37 @@ fn dump_metadata(metadata: &KaniMetadata, path: &Path) { /// be collected from the project. pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result { let outputs = session.cargo_build(keep_going)?; - let mut artifacts = vec![]; let outdir = outputs.outdir.canonicalize()?; if session.args.function.is_some() { + let mut artifacts = vec![]; // For the `--function` support, we still use a glob to link everything. // Yes, this is broken, but it has been broken for quite some time. :( // Merge goto files. + // https://github.com/model-checking/kani/issues/2129 let joined_name = "cbmc-linked"; let base_name = outdir.join(joined_name); let goto = base_name.with_extension(Goto); let all_gotos = outputs .metadata .iter() - .map(|artifact| { - convert_type(&artifact, ArtifactType::Metadata, ArtifactType::SymTabGoto) - }) + .map(|artifact| convert_type(&artifact, Metadata, SymTabGoto)) .collect::>(); session.link_goto_binary(&all_gotos, &goto)?; - artifacts.push(Artifact::try_new(&goto, Goto)?); + let goto_artifact = Artifact::try_new(&goto, Goto)?; // Merge metadata files. let per_crate: Vec<_> = outputs.metadata.iter().filter_map(|f| from_json::(f).ok()).collect(); let merged_metadata = merge_kani_metadata(per_crate); - let metadata = metadata_with_function(session, joined_name, merged_metadata); + let metadata = metadata_with_function( + session, + joined_name, + merged_metadata, + goto_artifact.with_extension(SymTabGoto), + ); let metadata_file = base_name.with_extension(Metadata); dump_metadata(&metadata, &metadata_file); + artifacts.push(goto_artifact); artifacts.push(Artifact::try_new(&metadata_file, Metadata)?); Ok(Project { @@ -191,33 +252,19 @@ pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result failed_targets: outputs.failed_targets, }) } else { - // For the MIR Linker we know there is only one artifact per verification target. Use - // that in our favor. - let mut metadata = vec![]; - for meta_file in outputs.metadata { - // Link the artifact. - let canonical_metafile = meta_file.canonicalize()?; - let symtab_out = convert_type(&canonical_metafile, Metadata, SymTabGoto); - let goto = convert_type(&canonical_metafile, Metadata, Goto); - session.link_goto_binary(&[symtab_out], &goto)?; - - // Store project information. - let crate_metadata: KaniMetadata = from_json(&meta_file)?; - let crate_name = &crate_metadata.crate_name; - artifacts.extend( - BUILD_ARTIFACTS.iter().filter_map(|typ| cargo_artifact(&canonical_metafile, *typ)), - ); - debug!(?crate_name, ?crate_metadata, "cargo_project"); - metadata.push(crate_metadata); - } - Ok(Project { + // For the MIR Linker we know there is only one metadata per crate. Use that in our favor. + let metadata = outputs + .metadata + .iter() + .map(|md_file| from_json(md_file)) + .collect::>>()?; + Project::try_new( + session, outdir, - artifacts, metadata, - merged_artifacts: false, - cargo_metadata: Some(outputs.cargo_metadata), - failed_targets: outputs.failed_targets, - }) + Some(outputs.cargo_metadata), + outputs.failed_targets, + ) } } @@ -230,8 +277,8 @@ pub fn standalone_project(input: &Path, session: &KaniSession) -> Result { /// The directory where all outputs should be directed to. outdir: PathBuf, - /// The collection of artifacts that may be generated. - artifacts: HashMap, + /// The metadata file for the target crate. + metadata: Artifact, /// The input file. input: PathBuf, /// The crate name. @@ -240,10 +287,6 @@ struct StandaloneProjectBuilder<'a> { session: &'a KaniSession, } -/// All the type of artifacts that may be generated as part of the build. -const BUILD_ARTIFACTS: [ArtifactType; 7] = - [Metadata, Goto, SymTab, SymTabGoto, TypeMap, VTableRestriction, PrettyNameMap]; - impl<'a> StandaloneProjectBuilder<'a> { /// Create a `StandaloneProjectBuilder` from the given input and session. /// This will perform a few validations before the build. @@ -256,11 +299,10 @@ impl<'a> StandaloneProjectBuilder<'a> { input.canonicalize().unwrap().parent().unwrap().to_path_buf() }; let crate_name = crate_name(&input); - let artifacts = - BUILD_ARTIFACTS.map(|typ| (typ, standalone_artifact(&outdir, &crate_name, typ))); + let metadata = standalone_artifact(&outdir, &crate_name, Metadata); Ok(StandaloneProjectBuilder { outdir, - artifacts: HashMap::from(artifacts), + metadata, input: input.to_path_buf(), crate_name, session, @@ -271,50 +313,30 @@ impl<'a> StandaloneProjectBuilder<'a> { fn build(self) -> Result { // Register artifacts that may be generated by the compiler / linker for future deletion. let rlib_path = guess_rlib_name(&self.outdir.join(self.input.file_name().unwrap())); - self.session.record_temporary_files(&[&rlib_path]); - self.session.record_temporary_files(&self.artifacts.values().collect::>()); + self.session.record_temporary_file(&rlib_path); + self.session.record_temporary_file(&self.metadata.path); // Build and link the artifacts. debug!(krate=?self.crate_name, input=?self.input, ?rlib_path, "build compile"); self.session.compile_single_rust_file(&self.input, &self.crate_name, &self.outdir)?; - let symtab_out = self.artifact(SymTabGoto); - let goto = self.artifact(Goto); - - if symtab_out.exists() { - debug!(?symtab_out, "build link"); - self.session.link_goto_binary(&[symtab_out.to_path_buf()], goto)?; - } - // Create the project with the artifacts built by the compiler. - let metadata_path = self.artifact(Metadata); - let metadata = if metadata_path.exists() { - metadata_with_function(self.session, &self.crate_name, from_json(metadata_path)?) + let metadata = if let Ok(goto_model) = Artifact::try_from(&self.metadata, SymTabGoto) { + metadata_with_function( + self.session, + &self.crate_name, + from_json(&self.metadata)?, + goto_model.path, + ) } else { - // TODO: The compiler should still produce a metadata file even when no harness exists. - KaniMetadata { - crate_name: self.crate_name, - proof_harnesses: vec![], - unsupported_features: vec![], - test_harnesses: vec![], - } + from_json(&self.metadata)? }; - Ok(Project { - outdir: self.outdir, - metadata: vec![metadata], - artifacts: self - .artifacts - .into_values() - .filter(|artifact| artifact.path.exists()) - .collect(), - merged_artifacts: false, - cargo_metadata: None, - failed_targets: None, - }) - } - - fn artifact(&self, typ: ArtifactType) -> &Path { - &self.artifacts.get(&typ).unwrap().path + // Create the project with the artifacts built by the compiler. + let result = Project::try_new(self.session, self.outdir, vec![metadata], None, None); + if let Ok(project) = &result { + self.session.record_temporary_files(&project.artifacts); + } + result } } @@ -324,10 +346,16 @@ fn metadata_with_function( session: &KaniSession, crate_name: &str, mut metadata: KaniMetadata, + model_file: PathBuf, ) -> KaniMetadata { if let Some(name) = &session.args.function { // --function is untranslated, create a mock harness - metadata.proof_harnesses.push(mock_proof_harness(name, None, Some(crate_name))); + metadata.proof_harnesses.push(mock_proof_harness( + name, + None, + Some(crate_name), + Some(model_file), + )); } metadata } diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index a5ed9d4c36a7..866181b7d877 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -65,7 +65,15 @@ impl KaniSession { }) } - pub fn record_temporary_files>(&self, temps: &[&T]) { + /// Record a temporary file so we can cleanup after ourselves at the end. + /// Note that there will be no failure if the file does not exist. + pub fn record_temporary_file>(&self, temp: &T) { + self.record_temporary_files(&[temp]) + } + + /// Record temporary files so we can cleanup after ourselves at the end. + /// Note that there will be no failure if the file does not exist. + pub fn record_temporary_files>(&self, temps: &[T]) { // unwrap safety: will panic this thread if another thread panicked *while holding the lock.* // This is vanishingly unlikely, and even then probably the right thing to do let mut t = self.temporaries.lock().unwrap(); diff --git a/tests/expected/per-harness/drop.rs b/tests/expected/per-harness/drop.rs new file mode 100644 index 000000000000..1172ca2e7539 --- /dev/null +++ b/tests/expected/per-harness/drop.rs @@ -0,0 +1,49 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: --harness check_drop_foo + +//! Test that Kani reachability analysis remove other unrelated drop implementations when using +//! fat pointers. +//! For each harness, there should be 1 of 1 cover satisfied. + +use std::any::Any; +use std::fmt::Debug; +use std::ptr::drop_in_place; + +#[derive(Debug)] +struct Foo {} + +#[derive(Debug)] +struct Bar {} + +impl Drop for Foo { + fn drop(&mut self) { + kani::cover!(true, "DropFoo"); + } +} + +impl Drop for Bar { + fn drop(&mut self) { + // This cover should be excluded from the result since there is no CFG path that connects + // the harness `check_drop_foo` with this function call. + kani::cover!(true, "DropBar"); + } +} + +#[kani::proof] +fn check_drop_foo() { + let boxed: Box = Box::new(Foo {}); + unsafe { drop_in_place(Box::into_raw(boxed)) }; +} + +#[kani::proof] +fn check_drop_bar() { + let boxed: Box = Box::new(Bar {}); + unsafe { drop_in_place(Box::into_raw(boxed)) }; +} + +#[kani::proof] +fn check_drop_bar_debug() { + let boxed: Box = Box::new(Bar {}); + unsafe { drop_in_place(Box::into_raw(boxed)) }; +} diff --git a/tests/expected/per-harness/expected b/tests/expected/per-harness/expected new file mode 100644 index 000000000000..e8d57d0d727b --- /dev/null +++ b/tests/expected/per-harness/expected @@ -0,0 +1,6 @@ +Checking harness check_drop_foo... + +Status: SATISFIED\ +Description: "DropFoo" + +1 of 1 cover properties satisfied diff --git a/tests/script-based-pre/check-output/check-output.sh b/tests/script-based-pre/check-output/check-output.sh index 429bd49ac042..45cb3b166669 100755 --- a/tests/script-based-pre/check-output/check-output.sh +++ b/tests/script-based-pre/check-output/check-output.sh @@ -34,15 +34,15 @@ rm -rf *.c kani --gen-c --enable-unstable singlefile.rs >& kani.log || \ { ret=$?; echo "== Failed to run Kani"; cat kani.log; rm kani.log; exit 1; } rm -f kani.log -if ! [ -e singlefile.for-main.c ] +if ! [ -e singlefile_main.for-main.c ] then - echo "Error: no GotoC file generated. Expected: singlefile.for-main.c" + echo "Error: no GotoC file generated. Expected: singlefile_main.for-main.c" exit 1 fi -if ! [ -e singlefile.for-main.demangled.c ] +if ! [ -e singlefile_main.for-main.demangled.c ] then - echo "Error: no demangled GotoC file generated. Expected singlefile.for-main.demangled.c." + echo "Error: no demangled GotoC file generated. Expected singlefile_main.for-main.demangled.c." exit 1 fi @@ -57,9 +57,9 @@ declare -a PATTERNS=( ) for val in "${PATTERNS[@]}"; do - if ! grep -Fq "$val" singlefile.for-main.demangled.c; + if ! grep -Fq "$val" singlefile_main.for-main.demangled.c; then - echo "Error: demangled file singlefile.for-main.demangled.c did not contain expected pattern '$val'." + echo "Error: demangled file singlefile_main.for-main.demangled.c did not contain expected pattern '$val'." exit 1 fi done