From e1502e7b76a6992e689db06abbafeb6451a0b1e7 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 18 Dec 2023 05:11:04 +0000 Subject: [PATCH 1/8] Start migrating foreign function --- .../codegen/foreign_function.rs | 43 ++++++++----------- .../src/codegen_cprover_gotoc/utils/names.rs | 31 ++----------- 2 files changed, 22 insertions(+), 52 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 22546be18909..b09da9f35abf 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -15,10 +15,10 @@ use crate::kani_middle; use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type}; use cbmc::{InternString, InternedString}; use lazy_static::lazy_static; -use rustc_middle::ty::Instance; use rustc_smir::rustc_internal; use rustc_target::abi::call::Conv; -use stable_mir::mir::mono::Instance as InstanceStable; +use stable_mir::mir::mono::Instance; +use stable_mir::CrateDef; use tracing::{debug, trace}; lazy_static! { @@ -46,15 +46,16 @@ impl<'tcx> GotocCtx<'tcx> { /// /// For other foreign items, we declare a shim and add to the list of foreign shims to be /// handled later. - pub fn codegen_foreign_fn(&mut self, instance: InstanceStable) -> &Symbol { + pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol { debug!(?instance, "codegen_foreign_function"); - let instance = rustc_internal::internal(instance); - let fn_name = self.symbol_name(instance).intern(); + let internal_instance = rustc_internal::internal(instance); + let fn_name = self.symbol_name_stable(instance).intern(); if self.symbol_table.contains(fn_name) { // Symbol has been added (either a built-in CBMC function or a Rust allocation function). self.symbol_table.lookup(fn_name).unwrap() } else if RUST_ALLOC_FNS.contains(&fn_name) - || (self.is_cffi_enabled() && kani_middle::fn_abi(self.tcx, instance).conv == Conv::C) + || (self.is_cffi_enabled() + && kani_middle::fn_abi(self.tcx, internal_instance).conv == Conv::C) { // Add a Rust alloc lib function as is declared by core. // When C-FFI feature is enabled, we just trust the rust declaration. @@ -63,14 +64,8 @@ impl<'tcx> GotocCtx<'tcx> { // https://github.com/model-checking/kani/issues/2426 self.ensure(fn_name, |gcx, _| { let typ = gcx.codegen_ffi_type(instance); - Symbol::function( - fn_name, - typ, - None, - gcx.readable_instance_name(instance), - Location::none(), - ) - .with_is_extern(true) + Symbol::function(fn_name, typ, None, instance.name(), Location::none()) + .with_is_extern(true) }) } else { let shim_name = format!("{fn_name}_ffi_shim"); @@ -82,7 +77,7 @@ impl<'tcx> GotocCtx<'tcx> { &shim_name, typ, Some(gcx.codegen_ffi_shim(shim_name.as_str().into(), instance)), - gcx.readable_instance_name(instance), + instance.name(), Location::none(), ) }) @@ -96,19 +91,19 @@ impl<'tcx> GotocCtx<'tcx> { } /// Generate code for a foreign function shim. - fn codegen_ffi_shim(&mut self, shim_name: InternedString, instance: Instance<'tcx>) -> Stmt { + fn codegen_ffi_shim(&mut self, shim_name: InternedString, instance: Instance) -> Stmt { debug!(?shim_name, ?instance, sym=?self.symbol_table.lookup(shim_name), "generate_foreign_shim"); - let loc = self.codegen_span(&self.tcx.def_span(instance.def_id())); + let loc = self.codegen_span_stable(instance.def.span()); let unsupported_check = self.codegen_ffi_unsupported(instance, loc); Stmt::block(vec![unsupported_check], loc) } /// Generate type for the given foreign instance. - fn codegen_ffi_type(&mut self, instance: Instance<'tcx>) -> Type { - let fn_name = self.symbol_name(instance); - let fn_abi = kani_middle::fn_abi(self.tcx, instance); - let loc = self.codegen_span(&self.tcx.def_span(instance.def_id())); + fn codegen_ffi_type(&mut self, instance: Instance) -> Type { + let fn_name = self.symbol_name_stable(instance); + let fn_abi = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance)); + let loc = self.codegen_span_stable(instance.def.span()); let params = fn_abi .args .iter() @@ -137,15 +132,15 @@ impl<'tcx> GotocCtx<'tcx> { /// /// This will behave like `codegen_unimplemented_stmt` but print a message that includes /// the name of the function not supported and the calling convention. - fn codegen_ffi_unsupported(&mut self, instance: Instance<'tcx>, loc: Location) -> Stmt { - let fn_name = &self.symbol_name(instance); + fn codegen_ffi_unsupported(&mut self, instance: Instance, loc: Location) -> Stmt { + let fn_name = &self.symbol_name_stable(instance); debug!(?fn_name, ?loc, "codegen_ffi_unsupported"); // Save this occurrence so we can emit a warning in the compilation report. let entry = self.unsupported_constructs.entry("foreign function".into()).or_default(); entry.push(loc); - let call_conv = kani_middle::fn_abi(self.tcx, instance).conv; + let call_conv = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance)).conv; let msg = format!("call to foreign \"{call_conv:?}\" function `{fn_name}`"); let url = if call_conv == Conv::C { "https://github.com/model-checking/kani/issues/2423" diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index 1b6d3da65cbd..e75182f99afb 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -7,11 +7,9 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::InternedString; use rustc_hir::def_id::LOCAL_CRATE; use rustc_middle::mir::mono::CodegenUnitNameBuilder; -use rustc_middle::ty::print::with_no_trimmed_paths; -use rustc_middle::ty::{Instance, TyCtxt}; -use stable_mir::mir::mono::Instance as InstanceStable; +use rustc_middle::ty::TyCtxt; +use stable_mir::mir::mono::Instance; use stable_mir::mir::Local; -use tracing::debug; impl<'tcx> GotocCtx<'tcx> { /// The full crate name including versioning info @@ -52,34 +50,11 @@ impl<'tcx> GotocCtx<'tcx> { format!("{var_name}_init") } - /// A human readable name in Rust for reference, should not be used as a key. - pub fn readable_instance_name(&self, instance: Instance<'tcx>) -> String { - with_no_trimmed_paths!(self.tcx.def_path_str_with_args(instance.def_id(), instance.args)) - } - - /// The actual function name used in the symbol table - pub fn symbol_name(&self, instance: Instance<'tcx>) -> String { - let llvm_mangled = self.tcx.symbol_name(instance).name.to_string(); - debug!( - "finding function name for instance: {}, debug: {:?}, name: {}, symbol: {}", - instance, - instance, - self.readable_instance_name(instance), - llvm_mangled, - ); - - let pretty = self.readable_instance_name(instance); - - // Make main function a special case in order to support `--function main` - // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129 - if pretty == "main" { pretty } else { llvm_mangled } - } - /// Return the mangled name to be used in the symbol table. /// /// We special case main function in order to support `--function main`. // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129 - pub fn symbol_name_stable(&self, instance: InstanceStable) -> String { + pub fn symbol_name_stable(&self, instance: Instance) -> String { let pretty = instance.name(); if pretty == "main" { pretty } else { instance.mangled_name() } } From 3b3c43e7e29b12ac1a960639684d070d3f391228 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 18 Dec 2023 20:21:55 +0000 Subject: [PATCH 2/8] Migrate compiler interface to use StableMIR --- .../codegen/intrinsic.rs | 2 +- .../compiler_interface.rs | 74 +++++++----------- kani-compiler/src/kani_compiler.rs | 12 +-- kani-compiler/src/kani_middle/analysis.rs | 6 +- kani-compiler/src/kani_middle/attributes.rs | 16 +++- kani-compiler/src/kani_middle/metadata.rs | 41 +++++----- kani-compiler/src/kani_middle/mod.rs | 78 +++++++++++-------- kani-compiler/src/kani_middle/provide.rs | 7 +- kani-compiler/src/kani_middle/reachability.rs | 39 ++++------ kani-compiler/src/kani_middle/stubbing/mod.rs | 6 +- kani-compiler/src/kani_queries/mod.rs | 10 +-- 11 files changed, 140 insertions(+), 151 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index fa23b85c18f1..e70662d4ff2a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1331,7 +1331,7 @@ impl<'tcx> GotocCtx<'tcx> { TyKind::RigidTy(RigidTy::Slice(_)) | TyKind::RigidTy(RigidTy::Str) => { let unit_t = match ty.kind() { TyKind::RigidTy(RigidTy::Slice(et)) => et, - TyKind::RigidTy(RigidTy::Str) => rustc_internal::stable(self.tcx.types.u8), + TyKind::RigidTy(RigidTy::Str) => Ty::unsigned_ty(UintTy::U8), _ => unreachable!(), }; let unit = self.layout_of_stable(unit_t); diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 21dea6160536..82e4a761845d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -16,7 +16,7 @@ use crate::kani_middle::{check_reachable_items, dump_mir_items}; use crate::kani_queries::QueryDb; use cbmc::goto_program::Location; use cbmc::irep::goto_binary_serde::write_goto_binary_file; -use cbmc::RoundingMode; +use cbmc::{InternString, RoundingMode}; use cbmc::{InternedString, MachineModel}; use kani_metadata::artifact::convert_type; use kani_metadata::CompilerArtifactStub; @@ -32,12 +32,10 @@ use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; use rustc_data_structures::temp_dir::MaybeTempDir; use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; use rustc_hir::def_id::LOCAL_CRATE; -use rustc_hir::definitions::DefPathHash; use rustc_metadata::creader::MetadataLoaderDyn; use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; -use rustc_middle::mir::mono::MonoItem; use rustc_middle::ty::TyCtxt; use rustc_middle::util::Providers; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; @@ -46,7 +44,7 @@ use rustc_session::Session; use rustc_smir::rustc_internal; use rustc_target::abi::Endian; use rustc_target::spec::PanicStrategy; -use stable_mir::mir::mono::MonoItem as MonoItemStable; +use stable_mir::mir::mono::MonoItem; use stable_mir::CrateDef; use std::any::Any; use std::collections::BTreeMap; @@ -82,10 +80,10 @@ impl GotocCodegenBackend { fn codegen_items<'tcx>( &self, tcx: TyCtxt<'tcx>, - starting_items: &[MonoItem<'tcx>], + starting_items: &[MonoItem], symtab_goto: &Path, machine_model: &MachineModel, - ) -> (GotocCtx<'tcx>, Vec>) { + ) -> (GotocCtx<'tcx>, Vec) { let items = with_timer( || collect_reachable_items(tcx, starting_items), "codegen reachability analysis", @@ -103,17 +101,13 @@ impl GotocCodegenBackend { for item in &items { match *item { MonoItem::Fn(instance) => { - let instance = rustc_internal::stable(instance); gcx.call_with_panic_debug_info( |ctx| ctx.declare_function(instance), format!("declare_function: {}", instance.name()), instance.def, ); } - MonoItem::Static(_) => { - let MonoItemStable::Static(def) = rustc_internal::stable(item) else { - unreachable!() - }; + MonoItem::Static(def) => { gcx.call_with_panic_debug_info( |ctx| ctx.declare_static(def), format!("declare_static: {}", def.name()), @@ -128,7 +122,6 @@ impl GotocCodegenBackend { for item in &items { match *item { MonoItem::Fn(instance) => { - let instance = rustc_internal::stable(instance); gcx.call_with_panic_debug_info( |ctx| ctx.codegen_function(instance), format!( @@ -139,10 +132,7 @@ impl GotocCodegenBackend { instance.def, ); } - MonoItem::Static(_) => { - let MonoItemStable::Static(def) = rustc_internal::stable(item) else { - unreachable!() - }; + MonoItem::Static(def) => { gcx.call_with_panic_debug_info( |ctx| ctx.codegen_static(def), format!("codegen_static: {}", def.name()), @@ -237,18 +227,20 @@ impl CodegenBackend for GotocCodegenBackend { 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()); + 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)) + let harnesses = filter_crate_items(tcx, |_, instance| { + items.contains(&instance.name().intern()) }); 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); + let model_path = queries.harness_model_path(&harness.name()).unwrap(); + let (gcx, mono_items) = self.codegen_items( + tcx, + &[MonoItem::Fn(harness)], + model_path, + &results.machine_model, + ); + results.extend(gcx, mono_items, None); } } ReachabilityType::Tests => { @@ -256,9 +248,9 @@ impl CodegenBackend for GotocCodegenBackend { // 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); + let harnesses = filter_const_crate_items(tcx, |_, item| { + if is_test_harness_description(tcx, item.def) { + descriptions.push(item.def); true } else { false @@ -289,11 +281,10 @@ impl CodegenBackend for GotocCodegenBackend { } 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 local_reachable = filter_crate_items(tcx, |_, _| true) + .into_iter() + .map(MonoItem::Fn) + .collect::>(); let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); let (gcx, items) = self.codegen_items( tcx, @@ -527,17 +518,17 @@ where } } -struct GotoCodegenResults<'tcx> { +struct GotoCodegenResults { reachability: ReachabilityType, harnesses: Vec, unsupported_constructs: UnsupportedConstructs, concurrent_constructs: UnsupportedConstructs, - items: Vec>, + items: Vec, crate_name: InternedString, machine_model: MachineModel, } -impl<'tcx> GotoCodegenResults<'tcx> { +impl GotoCodegenResults { pub fn new(tcx: TyCtxt, reachability: ReachabilityType) -> Self { GotoCodegenResults { reachability, @@ -585,12 +576,7 @@ impl<'tcx> GotoCodegenResults<'tcx> { } } - fn extend( - &mut self, - gcx: GotocCtx, - items: Vec>, - metadata: Option, - ) { + fn extend(&mut self, gcx: GotocCtx, items: Vec, metadata: Option) { let mut items = items; self.harnesses.extend(metadata); self.concurrent_constructs.extend(gcx.concurrent_constructs); @@ -599,7 +585,7 @@ impl<'tcx> GotoCodegenResults<'tcx> { } /// Prints a report at the end of the compilation. - fn print_report(&self, tcx: TyCtxt<'tcx>) { + fn print_report(&self, tcx: TyCtxt) { // Print all unsupported constructs. if !self.unsupported_constructs.is_empty() { // Sort alphabetically. @@ -631,7 +617,7 @@ impl<'tcx> GotoCodegenResults<'tcx> { // Print some compilation stats. if tracing::enabled!(tracing::Level::INFO) { - analysis::print_stats(tcx, &self.items); + analysis::print_stats(&self.items); } } } diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index fc04b68ec747..2042dc717652 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -25,6 +25,7 @@ use crate::kani_middle::reachability::filter_crate_items; use crate::kani_middle::stubbing::{self, harness_stub_map}; use crate::kani_queries::QueryDb; use crate::session::init_session; +use cbmc::{InternString, InternedString}; use clap::Parser; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; use rustc_codegen_ssa::traits::CodegenBackend; @@ -68,7 +69,7 @@ fn backend(queries: Arc>) -> Box { } /// A stable (across compilation sessions) identifier for the harness function. -type HarnessId = DefPathHash; +type HarnessId = InternedString; /// A set of stubs. type Stubs = BTreeMap; @@ -280,14 +281,13 @@ impl KaniCompiler { if self.queries.lock().unwrap().args().reachability_analysis == ReachabilityType::Harnesses { let base_filename = tcx.output_filenames(()).output_path(OutputType::Object); - let harnesses = filter_crate_items(tcx, |_, def_id| is_proof_harness(tcx, def_id)); + let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance)); let all_harnesses = harnesses .into_iter() .map(|harness| { - let def_id = harness.def_id(); - let def_path = tcx.def_path_hash(def_id); - let metadata = gen_proof_metadata(tcx, def_id, &base_filename); - let stub_map = harness_stub_map(tcx, def_id, &metadata); + let def_path = harness.name().intern(); + let metadata = gen_proof_metadata(tcx, harness, &base_filename); + let stub_map = harness_stub_map(tcx, harness, &metadata); (def_path, HarnessInfo { metadata, stub_map }) }) .collect::>(); diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs index b23fb99f83ff..0adee0e52cca 100644 --- a/kani-compiler/src/kani_middle/analysis.rs +++ b/kani-compiler/src/kani_middle/analysis.rs @@ -7,9 +7,6 @@ //! This module will perform all the analyses requested. Callers are responsible for selecting //! when the cost of these analyses are worth it. -use rustc_middle::mir::mono::MonoItem as InternalMonoItem; -use rustc_middle::ty::TyCtxt; -use rustc_smir::rustc_internal; use stable_mir::mir::mono::MonoItem; use stable_mir::mir::{ visit::Location, MirVisitor, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, @@ -23,8 +20,7 @@ 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>]) { - let items: Vec = items.iter().map(rustc_internal::stable).collect(); +pub fn print_stats(items: &[MonoItem]) { let item_types = items.iter().collect::(); let visitor = items .iter() diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 2c9c6d7ee54c..6fee2f110ae4 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -13,7 +13,10 @@ use rustc_errors::ErrorGuaranteed; use rustc_hir::{def::DefKind, def_id::DefId}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_session::Session; +use rustc_smir::rustc_internal; use rustc_span::{Span, Symbol}; +use stable_mir::mir::mono::Instance as InstanceStable; +use stable_mir::CrateDef; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; @@ -111,6 +114,10 @@ impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> { impl<'tcx> KaniAttributes<'tcx> { /// Perform preliminary parsing and checking for the attributes on this /// function + pub fn for_instance(tcx: TyCtxt<'tcx>, instance: InstanceStable) -> Self { + KaniAttributes::for_item(tcx, rustc_internal::internal(instance.def.def_id())) + } + pub fn for_item(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self { let all_attributes = tcx.get_attrs_unchecked(def_id); let map = all_attributes.iter().fold( @@ -511,20 +518,23 @@ pub fn is_function_contract_generated(tcx: TyCtxt, def_id: DefId) -> bool { /// Same as [`KaniAttributes::is_harness`] but more efficient because less /// attribute parsing is performed. -pub fn is_proof_harness(tcx: TyCtxt, def_id: DefId) -> bool { +pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool { + let def_id = rustc_internal::internal(instance.def.def_id()); has_kani_attribute(tcx, def_id, |a| { matches!(a, KaniAttributeKind::Proof | KaniAttributeKind::ProofForContract) }) } /// Does this `def_id` have `#[rustc_test_marker]`? -pub fn is_test_harness_description(tcx: TyCtxt, def_id: DefId) -> bool { +pub fn is_test_harness_description(tcx: TyCtxt, item: impl CrateDef) -> bool { + let def_id = rustc_internal::internal(item.def_id()); let attrs = tcx.get_attrs_unchecked(def_id); attr::contains_name(attrs, rustc_span::symbol::sym::rustc_test_marker) } /// Extract the test harness name from the `#[rustc_test_maker]` -pub fn test_harness_name(tcx: TyCtxt, def_id: DefId) -> String { +pub fn test_harness_name(tcx: TyCtxt, def: &impl CrateDef) -> String { + let def_id = rustc_internal::internal(def.def_id()); let attrs = tcx.get_attrs_unchecked(def_id); let marker = attr::find_by_name(attrs, rustc_span::symbol::sym::rustc_test_marker).unwrap(); parse_str_value(&marker).unwrap() diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index fbf69c2d4fa4..32549fe056b4 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -7,32 +7,30 @@ 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, InstanceDef, TyCtxt}; +use rustc_middle::ty::TyCtxt; +use stable_mir::mir::mono::Instance; +use stable_mir::CrateDef; use super::{attributes::KaniAttributes, 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 = KaniAttributes::for_item(tcx, def_id).harness_attributes(); - let pretty_name = tcx.def_path_str(def_id); +pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata { + let def = instance.def; + let attributes = KaniAttributes::for_instance(tcx, instance).harness_attributes(); + let pretty_name = instance.name(); // 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 mangled_name = + if pretty_name == "main" { pretty_name.clone() } else { instance.mangled_name() }; - let body = tcx.instance_mir(InstanceDef::Item(def_id)); - let loc = SourceLocation::new(tcx, &body.span); + let loc = SourceLocation::new(&instance.def.span()); 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(), + crate_name: def.krate().name, original_file: loc.filename, original_start_line: loc.start_line, original_end_line: loc.end_line, @@ -44,23 +42,22 @@ pub fn gen_proof_metadata(tcx: TyCtxt, def_id: DefId, base_name: &Path) -> Harne /// 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>, +pub fn gen_test_metadata( + tcx: TyCtxt, + test_desc: impl CrateDef, + test_fn: Instance, base_name: &Path, ) -> HarnessMetadata { - let pretty_name = test_harness_name(tcx, test_desc); - let mangled_name = tcx.symbol_name(test_fn).to_string(); - let body = tcx.instance_mir(InstanceDef::Item(test_desc)); - let loc = SourceLocation::new(tcx, &body.span); + let pretty_name = test_harness_name(tcx, &test_desc); + let mangled_name = test_fn.mangled_name(); + let loc = SourceLocation::new(&test_desc.span()); 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(), + crate_name: test_desc.krate().name, original_file: loc.filename, original_start_line: loc.start_line, original_end_line: loc.end_line, diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index c63b8303de17..eaf9a366ddeb 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -7,20 +7,23 @@ use std::collections::HashSet; use std::path::Path; use crate::kani_queries::QueryDb; -use rustc_hir::{def::DefKind, def_id::DefId, def_id::LOCAL_CRATE}; -use rustc_middle::mir::mono::MonoItem; +use rustc_hir::{def::DefKind, def_id::LOCAL_CRATE}; use rustc_middle::mir::write_mir_pretty; use rustc_middle::span_bug; use rustc_middle::ty::layout::{ FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers, TyAndLayout, }; -use rustc_middle::ty::{self, Instance, InstanceDef, ParamEnv, Ty, TyCtxt}; +use rustc_middle::ty::{self, Instance as InstanceInternal, Ty, TyCtxt}; use rustc_session::config::OutputType; +use rustc_smir::rustc_internal; use rustc_span::source_map::respan; use rustc_span::Span; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; +use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem}; +use stable_mir::ty::{BoundVariableKind, Span as SpanStable}; +use stable_mir::{CrateDef, DefId}; use std::fs::File; use std::io::BufWriter; use std::io::Write; @@ -66,14 +69,20 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { /// Check that all given 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. -pub fn check_reachable_items<'tcx>(tcx: TyCtxt<'tcx>, queries: &QueryDb, items: &[MonoItem<'tcx>]) { +pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) { // Avoid printing the same error multiple times for different instantiations of the same item. let mut def_ids = HashSet::new(); for item in items.iter().filter(|i| matches!(i, MonoItem::Fn(..) | MonoItem::Static(..))) { - let def_id = item.def_id(); + let def_id = match item { + MonoItem::Fn(instance) => instance.def.def_id(), + MonoItem::Static(def) => def.def_id(), + MonoItem::GlobalAsm(_) => { + unreachable!() + } + }; if !def_ids.contains(&def_id) { // Check if any unstable attribute was reached. - KaniAttributes::for_item(tcx, def_id) + KaniAttributes::for_item(tcx, rustc_internal::internal(def_id)) .check_unstable_features(&queries.args().unstable_features); def_ids.insert(def_id); } @@ -81,7 +90,7 @@ pub fn check_reachable_items<'tcx>(tcx: TyCtxt<'tcx>, queries: &QueryDb, items: // We don't short circuit here since this is a type check and can shake // out differently depending on generic parameters. if let MonoItem::Fn(instance) = item { - if attributes::is_function_contract_generated(tcx, instance.def_id()) { + if attributes::is_function_contract_generated(tcx, rustc_internal::internal(def_id)) { check_is_contract_safe(tcx, *instance); } } @@ -94,7 +103,7 @@ pub fn check_reachable_items<'tcx>(tcx: TyCtxt<'tcx>, queries: &QueryDb, items: /// /// This is a temporary safety measure because contracts cannot yet reason /// about the heap. -fn check_is_contract_safe<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) { +fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) { use ty::TypeVisitor; struct NoMutPtr<'tcx> { tcx: TyCtxt<'tcx>, @@ -112,7 +121,9 @@ fn check_is_contract_safe<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) { use ty::TypeSuperVisitable; if (self.is_prohibited)(t) { // TODO make this more user friendly - self.tcx.sess.err(format!("{} contains a {}pointer ({t:?}). This is prohibited for functions with contracts, as they cannot yet reason about the pointer behavior.", self.r#where, self.what)); + self.tcx.sess.err(format!( + "{} contains a {}pointer ({t:?}). This is prohibited for functions with contracts, \ + as they cannot yet reason about the pointer behavior.", self.r#where, self.what)); } // Rust's type visitor only recurses into type arguments, (e.g. @@ -147,12 +158,14 @@ fn check_is_contract_safe<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) { matches!(t.kind(), ty::TyKind::RawPtr(tmut) if tmut.mutbl == rustc_ast::Mutability::Mut) } - let bound_fn_sig = instance.ty(tcx, ParamEnv::reveal_all()).fn_sig(tcx); + // TODO: Replace this with fn_abi. + // https://github.com/model-checking/kani/issues/1365 + let bound_fn_sig = instance.ty().kind().fn_sig().unwrap(); - for v in bound_fn_sig.bound_vars() { - if let ty::BoundVariableKind::Ty(t) = v { + for var in &bound_fn_sig.bound_vars { + if let BoundVariableKind::Ty(t) = var { tcx.sess.span_err( - tcx.def_span(instance.def_id()), + rustc_internal::internal(instance.def.span()), format!("Found a bound type variable {t:?} after monomorphization"), ); } @@ -168,7 +181,7 @@ fn check_is_contract_safe<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) { .chain([(fn_typ.output(), (ty::Ty::is_unsafe_ptr as fn(_) -> _, "The return", ""))]) { let mut v = NoMutPtr { tcx, is_prohibited, r#where, what }; - v.visit_ty(typ); + v.visit_ty(rustc_internal::internal(typ)); } } @@ -176,14 +189,14 @@ fn check_is_contract_safe<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) { pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) { /// Convert MonoItem into a DefId. /// Skip stuff that we cannot generate the MIR items. - fn visible_item<'tcx>(item: &MonoItem<'tcx>) -> Option<(MonoItem<'tcx>, DefId)> { + fn visible_item(item: &MonoItem) -> Option<(MonoItem, DefId)> { match item { // Exclude FnShims and others that cannot be dumped. - MonoItem::Fn(instance) if matches!(instance.def, InstanceDef::Item(..)) => { - Some((*item, instance.def_id())) + MonoItem::Fn(instance) if matches!(instance.kind, InstanceKind::Item) => { + Some((item.clone(), instance.def.def_id())) } MonoItem::Fn(..) => None, - MonoItem::Static(def_id) => Some((*item, *def_id)), + MonoItem::Static(def) => Some((item.clone(), def.def_id())), MonoItem::GlobalAsm(_) => None, } } @@ -196,7 +209,7 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) { // For each def_id, dump their MIR for (item, def_id) in items.iter().filter_map(visible_item) { writeln!(writer, "// Item: {item:?}").unwrap(); - write_mir_pretty(tcx, Some(def_id), &mut writer).unwrap(); + write_mir_pretty(tcx, Some(rustc_internal::internal(def_id)), &mut writer).unwrap(); } } } @@ -213,27 +226,24 @@ pub struct SourceLocation { } 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, - }; + pub fn new(span: &SpanStable) -> Self { + let loc = span.get_lines(); + let filename = span.get_filename().to_string(); + let start_line = loc.start_line; + let start_col = loc.start_col; + let end_line = loc.end_line; + let end_col = loc.end_col; SourceLocation { filename, start_line, start_col, end_line, end_col } } } /// Get the FnAbi of a given instance with no extra variadic arguments. -/// TODO: Get rid of this. Use instance.fn_sig() instead. +/// TODO: Get rid of this. Use instance.fn_abi() instead. /// -pub fn fn_abi<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> &'tcx FnAbi<'tcx, Ty<'tcx>> { +pub fn fn_abi<'tcx>( + tcx: TyCtxt<'tcx>, + instance: InstanceInternal<'tcx>, +) -> &'tcx FnAbi<'tcx, Ty<'tcx>> { let helper = CompilerHelpers { tcx }; helper.fn_abi_of_instance(instance, ty::List::empty()) } diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index 3c7664d076d6..70e046d6f9d6 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -13,6 +13,7 @@ use rustc_hir::def_id::{DefId, LocalDefId}; use rustc_interface; use rustc_middle::util::Providers; use rustc_middle::{mir::Body, query::queries, ty::TyCtxt}; +use stable_mir::mir::mono::MonoItem; /// Sets up rustc's query mechanism to apply Kani's custom queries to code from /// a crate. @@ -77,10 +78,8 @@ fn collect_and_partition_mono_items( key: (), ) -> queries::collect_and_partition_mono_items::ProvidedValue { rustc_smir::rustc_internal::run(tcx, || { - 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) || entry_fn == Some(def_id) - }); + let local_reachable = + filter_crate_items(tcx, |_, _| true).into_iter().map(MonoItem::Fn).collect::>(); // We do not actually need the value returned here. collect_reachable_items(tcx, &local_reachable); }) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 2a6bfbe8fc6b..71696a769e6c 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -21,8 +21,6 @@ use tracing::{debug, debug_span, trace}; use rustc_data_structures::fingerprint::Fingerprint; use rustc_data_structures::fx::FxHashSet; use rustc_data_structures::stable_hasher::{HashStable, StableHasher}; -use rustc_hir::def_id::DefId; -use rustc_middle::mir::mono::MonoItem as InternalMonoItem; use rustc_middle::ty::{TyCtxt, VtblEntry}; use rustc_smir::rustc_internal; use stable_mir::mir::alloc::{AllocId, GlobalAlloc}; @@ -41,15 +39,12 @@ use crate::kani_middle::coercion::CoercionBase; use crate::kani_middle::stubbing::{get_stub, validate_instance}; /// Collect all reachable items starting from the given starting points. -pub fn collect_reachable_items<'tcx>( - tcx: TyCtxt<'tcx>, - starting_points: &[InternalMonoItem<'tcx>], -) -> Vec> { +pub fn collect_reachable_items(tcx: TyCtxt, starting_points: &[MonoItem]) -> Vec { // For each harness, collect items using the same collector. // I.e.: This will return any item that is reachable from one or more of the starting points. let mut collector = MonoItemsCollector::new(tcx); for item in starting_points { - collector.collect(rustc_internal::stable(item)); + collector.collect(item.clone()); } #[cfg(debug_assertions)] @@ -62,17 +57,16 @@ pub fn collect_reachable_items<'tcx>( // Sort the result so code generation follows deterministic order. // This helps us to debug the code, but it also provides the user a good experience since the // order of the errors and warnings is stable. - let mut sorted_items: Vec<_> = - collector.collected.iter().map(rustc_internal::internal).collect(); + let mut sorted_items: Vec<_> = collector.collected.into_iter().collect(); sorted_items.sort_by_cached_key(|item| to_fingerprint(tcx, item)); sorted_items } /// Collect all (top-level) items in the crate that matches the given predicate. -/// An item can only be a root if they are: non-generic Fn / Static / GlobalASM -pub fn filter_crate_items(tcx: TyCtxt, predicate: F) -> Vec +/// An item can only be a root if they are a non-generic function. +pub fn filter_crate_items(tcx: TyCtxt, predicate: F) -> Vec where - F: Fn(TyCtxt, DefId) -> bool, + F: Fn(TyCtxt, Instance) -> bool, { let crate_items = stable_mir::all_local_items(); // Filter regular items. @@ -80,11 +74,9 @@ where .iter() .filter_map(|item| { // Only collect monomorphic items. - Instance::try_from(*item).ok().and_then(|instance| { - let def_id = rustc_internal::internal(item); - predicate(tcx, def_id) - .then_some(InternalMonoItem::Fn(rustc_internal::internal(&instance))) - }) + Instance::try_from(*item) + .ok() + .and_then(|instance| predicate(tcx, instance).then_some(instance)) }) .collect::>() } @@ -93,9 +85,9 @@ where /// /// Probably only specifically useful with a predicate to find `TestDescAndFn` const declarations from /// tests and extract the closures from them. -pub fn filter_const_crate_items(tcx: TyCtxt, mut predicate: F) -> Vec +pub fn filter_const_crate_items(tcx: TyCtxt, mut predicate: F) -> Vec where - F: FnMut(TyCtxt, DefId) -> bool, + F: FnMut(TyCtxt, Instance) -> bool, { let crate_items = stable_mir::all_local_items(); let mut roots = Vec::new(); @@ -103,8 +95,7 @@ where for item in crate_items { // Only collect monomorphic items. if let Ok(instance) = Instance::try_from(item) { - let def_id = rustc_internal::internal(&item); - if predicate(tcx, def_id) { + if predicate(tcx, instance) { let body = instance.body().unwrap(); let mut collector = MonoItemsFnCollector { tcx, @@ -113,7 +104,7 @@ where instance: &instance, }; collector.visit_body(&body); - roots.extend(collector.collected.iter().map(rustc_internal::internal)); + roots.extend(collector.collected.into_iter()); } } } @@ -475,10 +466,10 @@ fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty) /// Convert a `MonoItem` into a stable `Fingerprint` which can be used as a stable hash across /// compilation sessions. This allow us to provide a stable deterministic order to codegen. -fn to_fingerprint(tcx: TyCtxt, item: &InternalMonoItem) -> Fingerprint { +fn to_fingerprint(tcx: TyCtxt, item: &MonoItem) -> Fingerprint { tcx.with_stable_hashing_context(|mut hcx| { let mut hasher = StableHasher::new(); - item.hash_stable(&mut hcx, &mut hasher); + rustc_internal::internal(item).hash_stable(&mut hcx, &mut hasher); hasher.finish() }) } diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 6af0b442c8d4..9b83ae2f2415 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -10,7 +10,6 @@ use tracing::{debug, trace}; pub use self::transform::*; use kani_metadata::HarnessMetadata; -use rustc_hir::def_id::DefId; use rustc_hir::definitions::DefPathHash; use rustc_middle::mir::Const; use rustc_middle::ty::{self, EarlyBinder, ParamEnv, TyCtxt, TypeFoldable}; @@ -25,13 +24,14 @@ use self::annotations::update_stub_mapping; /// Collects the stubs from the harnesses in a crate. pub fn harness_stub_map( tcx: TyCtxt, - harness: DefId, + harness: Instance, metadata: &HarnessMetadata, ) -> BTreeMap { + let def_id = rustc_internal::internal(harness.def.def_id()); let attrs = &metadata.attributes; let mut stub_pairs = BTreeMap::default(); for stubs in &attrs.stubs { - update_stub_mapping(tcx, harness.expect_local(), stubs, &mut stub_pairs); + update_stub_mapping(tcx, def_id.expect_local(), stubs, &mut stub_pairs); } stub_pairs } diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index 7c716a5f38a5..6bda0a20bd2f 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Define the communication between KaniCompiler and the codegen implementation. -use rustc_hir::definitions::DefPathHash; +use cbmc::{InternString, InternedString}; use std::{ collections::HashMap, path::PathBuf, @@ -16,7 +16,7 @@ use crate::args::Arguments; pub struct QueryDb { args: Option, /// Information about all target harnesses. - pub harnesses_info: HashMap, + pub harnesses_info: HashMap, } impl QueryDb { @@ -25,13 +25,13 @@ impl QueryDb { } /// Get the definition hash for all harnesses that are being compiled in this compilation stage. - pub fn target_harnesses(&self) -> Vec { + pub fn target_harnesses(&self) -> Vec { self.harnesses_info.keys().cloned().collect() } /// Get the model path for a given harness. - pub fn harness_model_path(&self, harness: &DefPathHash) -> Option<&PathBuf> { - self.harnesses_info.get(harness) + pub fn harness_model_path(&self, harness: &String) -> Option<&PathBuf> { + self.harnesses_info.get(&harness.intern()) } pub fn set_args(&mut self, args: Arguments) { From b672e9b94b04ab56be4dd048c649faef20b95158 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 19 Dec 2023 16:00:23 -0800 Subject: [PATCH 3/8] Finish migration of compiler-interface --- kani-compiler/src/kani_compiler.rs | 27 +++++---- kani-compiler/src/kani_middle/metadata.rs | 6 +- kani-compiler/src/kani_middle/mod.rs | 60 ++++++++++--------- kani-compiler/src/kani_middle/reachability.rs | 17 ++++-- .../assess-workspace-artifacts/expected | 6 +- 5 files changed, 68 insertions(+), 48 deletions(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 2042dc717652..e9fbd6ba05ac 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -446,7 +446,14 @@ mod tests { use rustc_hir::definitions::DefPathHash; use std::collections::HashMap; - fn mock_next_id() -> HarnessId { + fn mock_next_harness() -> HarnessId { + static mut COUNTER: u64 = 0; + unsafe { COUNTER += 1 }; + let id = unsafe { COUNTER }; + format!("mod::harness-{id}").intern() + } + + fn mock_next_stub() -> DefPathHash { static mut COUNTER: u64 = 0; unsafe { COUNTER += 1 }; let id = unsafe { COUNTER }; @@ -473,15 +480,15 @@ mod tests { #[test] fn test_group_by_stubs_works() { // Set up the inputs - let harness_1 = mock_next_id(); - let harness_2 = mock_next_id(); - let harness_3 = mock_next_id(); + let harness_1 = mock_next_harness(); + let harness_2 = mock_next_harness(); + let harness_3 = mock_next_harness(); let harnesses = vec![harness_1, harness_2, harness_3]; - let stub_1 = (mock_next_id(), mock_next_id()); - let stub_2 = (mock_next_id(), mock_next_id()); - let stub_3 = (mock_next_id(), mock_next_id()); - let stub_4 = (stub_3.0, mock_next_id()); + let stub_1 = (mock_next_stub(), mock_next_stub()); + let stub_2 = (mock_next_stub(), mock_next_stub()); + let stub_3 = (mock_next_stub(), mock_next_stub()); + let stub_4 = (stub_3.0, mock_next_stub()); let set_1 = Stubs::from([stub_1, stub_2, stub_3]); let set_2 = Stubs::from([stub_1, stub_2, stub_4]); @@ -516,7 +523,7 @@ mod tests { let mut info = mock_info_with_stubs(Stubs::default()); info.metadata.attributes.proof = true; - let id = mock_next_id(); + let id = mock_next_harness(); let all_harnesses = HashMap::from([(id, info.clone())]); // Call generate metadata. @@ -553,7 +560,7 @@ mod tests { let infos = harnesses.map(|harness| { let mut metadata = mock_metadata(harness.to_string(), krate.clone()); metadata.attributes.proof = true; - (mock_next_id(), HarnessInfo { stub_map: Stubs::default(), metadata }) + (mock_next_harness(), HarnessInfo { stub_map: Stubs::default(), metadata }) }); let all_harnesses = HashMap::from(infos.clone()); diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 32549fe056b4..43eed5ecac3a 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -23,7 +23,9 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> let mangled_name = if pretty_name == "main" { pretty_name.clone() } else { instance.mangled_name() }; - let loc = SourceLocation::new(&instance.def.span()); + // We get the body span to include the entire function definition. + // This is required for concrete playback to properly position the generated test. + let loc = SourceLocation::new(instance.body().unwrap().span); 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); @@ -50,7 +52,7 @@ pub fn gen_test_metadata( ) -> HarnessMetadata { let pretty_name = test_harness_name(tcx, &test_desc); let mangled_name = test_fn.mangled_name(); - let loc = SourceLocation::new(&test_desc.span()); + let loc = SourceLocation::new(test_desc.span()); 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); diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index eaf9a366ddeb..5d1b148b963f 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -14,7 +14,7 @@ use rustc_middle::ty::layout::{ FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers, TyAndLayout, }; -use rustc_middle::ty::{self, Instance as InstanceInternal, Ty, TyCtxt}; +use rustc_middle::ty::{self, Instance as InstanceInternal, Ty as TyInternal, TyCtxt}; use rustc_session::config::OutputType; use rustc_smir::rustc_internal; use rustc_span::source_map::respan; @@ -22,7 +22,9 @@ use rustc_span::Span; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem}; -use stable_mir::ty::{BoundVariableKind, Span as SpanStable}; +use stable_mir::mir::pretty::pretty_ty; +use stable_mir::ty::{BoundVariableKind, RigidTy, Span as SpanStable, Ty, TyKind}; +use stable_mir::visitor::{Visitable, Visitor as TypeVisitor}; use stable_mir::{CrateDef, DefId}; use std::fs::File; use std::io::BufWriter; @@ -104,10 +106,9 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) /// This is a temporary safety measure because contracts cannot yet reason /// about the heap. fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) { - use ty::TypeVisitor; struct NoMutPtr<'tcx> { tcx: TyCtxt<'tcx>, - is_prohibited: fn(ty::Ty<'tcx>) -> bool, + is_prohibited: fn(Ty) -> bool, /// Where (top level) did the type we're analyzing come from. Used for /// composing error messages. r#where: &'static str, @@ -116,14 +117,15 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) { what: &'static str, } - impl<'tcx> TypeVisitor> for NoMutPtr<'tcx> { - fn visit_ty(&mut self, t: ty::Ty<'tcx>) -> std::ops::ControlFlow { - use ty::TypeSuperVisitable; - if (self.is_prohibited)(t) { + impl<'tcx> TypeVisitor for NoMutPtr<'tcx> { + type Break = (); + fn visit_ty(&mut self, ty: &Ty) -> std::ops::ControlFlow { + if (self.is_prohibited)(*ty) { // TODO make this more user friendly self.tcx.sess.err(format!( - "{} contains a {}pointer ({t:?}). This is prohibited for functions with contracts, \ - as they cannot yet reason about the pointer behavior.", self.r#where, self.what)); + "{} contains a {}pointer ({}). This is prohibited for functions with contracts, \ + as they cannot yet reason about the pointer behavior.", self.r#where, self.what, + pretty_ty(ty.kind()))); } // Rust's type visitor only recurses into type arguments, (e.g. @@ -134,28 +136,28 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) { // Since the field types also must contain in some form all the type // arguments the visitor will see them as it inspects the fields and // we don't need to call back to `super`. - if let ty::TyKind::Adt(adt_def, generics) = t.kind() { + if let TyKind::RigidTy(RigidTy::Adt(adt_def, generics)) = ty.kind() { for variant in adt_def.variants() { - for field in &variant.fields { - let ctrl = self.visit_ty(field.ty(self.tcx, generics)); - if ctrl.is_break() { - // Technically we can just ignore this because we - // know this case will never happen, but just to be - // safe. - return ctrl; - } + for field in &variant.fields() { + self.visit_ty(&field.ty_with_args(&generics))?; } } std::ops::ControlFlow::Continue(()) } else { // For every other type. - t.super_visit_with(self) + ty.super_visit(self) } } } - fn is_raw_mutable_ptr(t: ty::Ty) -> bool { - matches!(t.kind(), ty::TyKind::RawPtr(tmut) if tmut.mutbl == rustc_ast::Mutability::Mut) + fn is_raw_mutable_ptr(ty: Ty) -> bool { + let kind = ty.kind(); + kind.is_raw_ptr() && kind.is_mutable_ptr() + } + + fn is_raw_ptr(ty: Ty) -> bool { + let kind = ty.kind(); + kind.is_raw_ptr() } // TODO: Replace this with fn_abi. @@ -173,15 +175,15 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) { let fn_typ = bound_fn_sig.skip_binder(); - for (typ, (is_prohibited, r#where, what)) in fn_typ + for (input_ty, (is_prohibited, r#where, what)) in fn_typ .inputs() .iter() .copied() .zip(std::iter::repeat((is_raw_mutable_ptr as fn(_) -> _, "This argument", "mutable "))) - .chain([(fn_typ.output(), (ty::Ty::is_unsafe_ptr as fn(_) -> _, "The return", ""))]) + .chain([(fn_typ.output(), (is_raw_ptr as fn(_) -> _, "The return", ""))]) { let mut v = NoMutPtr { tcx, is_prohibited, r#where, what }; - v.visit_ty(rustc_internal::internal(typ)); + v.visit_ty(&input_ty); } } @@ -226,7 +228,7 @@ pub struct SourceLocation { } impl SourceLocation { - pub fn new(span: &SpanStable) -> Self { + pub fn new(span: SpanStable) -> Self { let loc = span.get_lines(); let filename = span.get_filename().to_string(); let start_line = loc.start_line; @@ -243,7 +245,7 @@ impl SourceLocation { pub fn fn_abi<'tcx>( tcx: TyCtxt<'tcx>, instance: InstanceInternal<'tcx>, -) -> &'tcx FnAbi<'tcx, Ty<'tcx>> { +) -> &'tcx FnAbi<'tcx, TyInternal<'tcx>> { let helper = CompilerHelpers { tcx }; helper.fn_abi_of_instance(instance, ty::List::empty()) } @@ -274,14 +276,14 @@ impl<'tcx> LayoutOfHelpers<'tcx> for CompilerHelpers<'tcx> { type LayoutOfResult = TyAndLayout<'tcx>; #[inline] - fn handle_layout_err(&self, err: LayoutError<'tcx>, span: Span, ty: Ty<'tcx>) -> ! { + fn handle_layout_err(&self, err: LayoutError<'tcx>, span: Span, ty: TyInternal<'tcx>) -> ! { span_bug!(span, "failed to get layout for `{}`: {}", ty, err) } } /// Implement error handling for extracting function ABI information. impl<'tcx> FnAbiOfHelpers<'tcx> for CompilerHelpers<'tcx> { - type FnAbiOfResult = &'tcx FnAbi<'tcx, Ty<'tcx>>; + type FnAbiOfResult = &'tcx FnAbi<'tcx, TyInternal<'tcx>>; #[inline] fn handle_fn_abi_err( diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 71696a769e6c..bc1dd6935043 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -31,8 +31,8 @@ use stable_mir::mir::{ TerminatorKind, }; use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind}; -use stable_mir::CrateDef; use stable_mir::{self, CrateItem}; +use stable_mir::{CrateDef, ItemKind}; use crate::kani_middle::coercion; use crate::kani_middle::coercion::CoercionBase; @@ -73,10 +73,19 @@ where crate_items .iter() .filter_map(|item| { + tracing::warn!(?item, name = item.name(), "crate_item"); + tracing::warn!(body=?item.body().blocks.len(), "crate_item"); // Only collect monomorphic items. - Instance::try_from(*item) - .ok() - .and_then(|instance| predicate(tcx, instance).then_some(instance)) + // TODO: Remove the def_kind check once https://github.com/rust-lang/rust/pull/119135 has been released. + let def_id = rustc_internal::internal(item.def_id()); + (matches!(tcx.def_kind(def_id), rustc_hir::def::DefKind::Ctor(..)) + || matches!(item.kind(), ItemKind::Fn)) + .then(|| { + Instance::try_from(*item) + .ok() + .and_then(|instance| predicate(tcx, instance).then_some(instance)) + }) + .flatten() }) .collect::>() } diff --git a/tests/cargo-kani/assess-workspace-artifacts/expected b/tests/cargo-kani/assess-workspace-artifacts/expected index 21d964340630..4e9a26f89c27 100644 --- a/tests/cargo-kani/assess-workspace-artifacts/expected +++ b/tests/cargo-kani/assess-workspace-artifacts/expected @@ -11,10 +11,10 @@ Analyzed 2 packages unsupported_construct | 3 none (success) | 3 ========================================= -======================================================================================================================= +================================================= Candidate for proof harness | Location ---------------------------------------+-------------------------------------------------------------------------------- +--------------------------------------+---------- a_supported_test_from_tests | a_supported_test_from_the_lib | a_supported_test_from_the_subpackage | -======================================================================================================================= +================================================== From 9afc460b8ce0b348c7cca07c9ca1f3949ef763d0 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 19 Dec 2023 20:26:11 -0800 Subject: [PATCH 4/8] Fix regression tests and remove debug --- .../codegen_cprover_gotoc/compiler_interface.rs | 15 ++++++++++----- kani-compiler/src/kani_middle/reachability.rs | 2 -- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 82e4a761845d..a3dbbfda37ac 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -44,7 +44,7 @@ use rustc_session::Session; use rustc_smir::rustc_internal; use rustc_target::abi::Endian; use rustc_target::spec::PanicStrategy; -use stable_mir::mir::mono::MonoItem; +use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::CrateDef; use std::any::Any; use std::collections::BTreeMap; @@ -281,10 +281,15 @@ impl CodegenBackend for GotocCodegenBackend { } ReachabilityType::None => {} ReachabilityType::PubFns => { - let local_reachable = filter_crate_items(tcx, |_, _| true) - .into_iter() - .map(MonoItem::Fn) - .collect::>(); + let main_instance = + stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap()); + let local_reachable = filter_crate_items(tcx, |_, instance| { + let def_id = rustc_internal::internal(instance.def.def_id()); + Some(instance) == main_instance || tcx.is_reachable_non_generic(def_id) + }) + .into_iter() + .map(MonoItem::Fn) + .collect::>(); let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); let (gcx, items) = self.codegen_items( tcx, diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index bc1dd6935043..024434f6ac2f 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -73,8 +73,6 @@ where crate_items .iter() .filter_map(|item| { - tracing::warn!(?item, name = item.name(), "crate_item"); - tracing::warn!(body=?item.body().blocks.len(), "crate_item"); // Only collect monomorphic items. // TODO: Remove the def_kind check once https://github.com/rust-lang/rust/pull/119135 has been released. let def_id = rustc_internal::internal(item.def_id()); From f7e2d82d0aef7f24c02099fd9769da73e220540e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 19 Dec 2023 16:00:01 -0800 Subject: [PATCH 5/8] Update the rust-toolchain --- kani-compiler/src/session.rs | 4 ++-- rust-toolchain.toml | 2 +- tools/bookrunner/librustdoc/doctest.rs | 8 ++++---- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index 87d25f1e8fc3..a1c3af20bb06 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -9,7 +9,7 @@ use rustc_errors::{ ColorConfig, Diagnostic, TerminalUrl, }; use rustc_session::config::ErrorOutputType; -use rustc_session::EarlyErrorHandler; +use rustc_session::EarlyDiagCtxt; use std::io::IsTerminal; use std::panic; use std::sync::LazyLock; @@ -71,7 +71,7 @@ pub fn init_session(args: &Arguments, json_hook: bool) { // Initialize the rustc logger using value from RUSTC_LOG. We keep the log control separate // because we cannot control the RUSTC log format unless if we match the exact tracing // version used by RUSTC. - let handler = EarlyErrorHandler::new(ErrorOutputType::default()); + let handler = EarlyDiagCtxt::new(ErrorOutputType::default()); rustc_driver::init_rustc_env_logger(&handler); // Install Kani panic hook. diff --git a/rust-toolchain.toml b/rust-toolchain.toml index af9f0d238cc5..fe2513be9b06 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-12-18" +channel = "nightly-2023-12-20" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tools/bookrunner/librustdoc/doctest.rs b/tools/bookrunner/librustdoc/doctest.rs index 734dacd093a6..01fc395046f2 100644 --- a/tools/bookrunner/librustdoc/doctest.rs +++ b/tools/bookrunner/librustdoc/doctest.rs @@ -66,7 +66,7 @@ pub fn make_test( let result = rustc_driver::catch_fatal_errors(|| { rustc_span::create_session_if_not_set_then(edition, |_| { use rustc_errors::emitter::{Emitter, EmitterWriter}; - use rustc_errors::Handler; + use rustc_errors::DiagCtxt; use rustc_parse::maybe_new_parser_from_source_str; use rustc_parse::parser::ForceCollect; use rustc_session::parse::ParseSess; @@ -88,8 +88,8 @@ pub fn make_test( let emitter = EmitterWriter::new(Box::new(io::sink()), fallback_bundle); // FIXME(misdreavus): pass `-Z treat-err-as-bug` to the doctest parser - let handler = Handler::with_emitter(Box::new(emitter)); - let sess = ParseSess::with_span_handler(handler, sm); + let handler = DiagCtxt::with_emitter(Box::new(emitter)); + let sess = ParseSess::with_dcx(handler, sm); let mut found_main = false; let mut found_extern_crate = crate_name.is_none(); @@ -152,7 +152,7 @@ pub fn make_test( // handler. Any errors in the tests will be reported when the test file is compiled, // Note that we still need to cancel the errors above otherwise `DiagnosticBuilder` // will panic on drop. - sess.span_diagnostic.reset_err_count(); + sess.dcx.reset_err_count(); (found_main, found_extern_crate, found_macro) }) From 2474b8ba31b21a601cb6890f578c38c79789fda4 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 19 Dec 2023 21:38:26 -0800 Subject: [PATCH 6/8] Fix perfomance regression --- .../src/codegen_cprover_gotoc/compiler_interface.rs | 5 +++-- kani-compiler/src/kani_compiler.rs | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index a3dbbfda37ac..129143937105 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -230,10 +230,11 @@ impl CodegenBackend for GotocCodegenBackend { let mut items: HashSet<_> = HashSet::with_capacity(harnesses.len()); items.extend(harnesses); let harnesses = filter_crate_items(tcx, |_, instance| { - items.contains(&instance.name().intern()) + items.contains(&instance.mangled_name().intern()) }); for harness in harnesses { - let model_path = queries.harness_model_path(&harness.name()).unwrap(); + let model_path = + queries.harness_model_path(&harness.mangled_name()).unwrap(); let (gcx, mono_items) = self.codegen_items( tcx, &[MonoItem::Fn(harness)], diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index e9fbd6ba05ac..df95d5c30ae8 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -285,7 +285,7 @@ impl KaniCompiler { let all_harnesses = harnesses .into_iter() .map(|harness| { - let def_path = harness.name().intern(); + let def_path = harness.mangled_name().intern(); let metadata = gen_proof_metadata(tcx, harness, &base_filename); let stub_map = harness_stub_map(tcx, harness, &metadata); (def_path, HarnessInfo { metadata, stub_map }) From 038e316a5c139b363d1779a659c83bc0ee55ec23 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 20 Dec 2023 10:34:59 -0800 Subject: [PATCH 7/8] Apply suggestions from code review Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- .../src/codegen_cprover_gotoc/codegen/foreign_function.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index b09da9f35abf..2eb1610ab4d8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -48,14 +48,14 @@ impl<'tcx> GotocCtx<'tcx> { /// handled later. pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol { debug!(?instance, "codegen_foreign_function"); - let internal_instance = rustc_internal::internal(instance); + let instance_internal = rustc_internal::internal(instance); let fn_name = self.symbol_name_stable(instance).intern(); if self.symbol_table.contains(fn_name) { // Symbol has been added (either a built-in CBMC function or a Rust allocation function). self.symbol_table.lookup(fn_name).unwrap() } else if RUST_ALLOC_FNS.contains(&fn_name) || (self.is_cffi_enabled() - && kani_middle::fn_abi(self.tcx, internal_instance).conv == Conv::C) + && kani_middle::fn_abi(self.tcx, instance_internal).conv == Conv::C) { // Add a Rust alloc lib function as is declared by core. // When C-FFI feature is enabled, we just trust the rust declaration. From 31af32bb6b903a788e759ecdd5301e3afb69ce8d Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 20 Dec 2023 10:47:10 -0800 Subject: [PATCH 8/8] Rename mock functions --- kani-compiler/src/kani_compiler.rs | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index df95d5c30ae8..57280c5b332b 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -446,14 +446,14 @@ mod tests { use rustc_hir::definitions::DefPathHash; use std::collections::HashMap; - fn mock_next_harness() -> HarnessId { + fn mock_next_harness_id() -> HarnessId { static mut COUNTER: u64 = 0; unsafe { COUNTER += 1 }; let id = unsafe { COUNTER }; format!("mod::harness-{id}").intern() } - fn mock_next_stub() -> DefPathHash { + fn mock_next_stub_id() -> DefPathHash { static mut COUNTER: u64 = 0; unsafe { COUNTER += 1 }; let id = unsafe { COUNTER }; @@ -480,15 +480,15 @@ mod tests { #[test] fn test_group_by_stubs_works() { // Set up the inputs - let harness_1 = mock_next_harness(); - let harness_2 = mock_next_harness(); - let harness_3 = mock_next_harness(); + let harness_1 = mock_next_harness_id(); + let harness_2 = mock_next_harness_id(); + let harness_3 = mock_next_harness_id(); let harnesses = vec![harness_1, harness_2, harness_3]; - let stub_1 = (mock_next_stub(), mock_next_stub()); - let stub_2 = (mock_next_stub(), mock_next_stub()); - let stub_3 = (mock_next_stub(), mock_next_stub()); - let stub_4 = (stub_3.0, mock_next_stub()); + let stub_1 = (mock_next_stub_id(), mock_next_stub_id()); + let stub_2 = (mock_next_stub_id(), mock_next_stub_id()); + let stub_3 = (mock_next_stub_id(), mock_next_stub_id()); + let stub_4 = (stub_3.0, mock_next_stub_id()); let set_1 = Stubs::from([stub_1, stub_2, stub_3]); let set_2 = Stubs::from([stub_1, stub_2, stub_4]); @@ -523,7 +523,7 @@ mod tests { let mut info = mock_info_with_stubs(Stubs::default()); info.metadata.attributes.proof = true; - let id = mock_next_harness(); + let id = mock_next_harness_id(); let all_harnesses = HashMap::from([(id, info.clone())]); // Call generate metadata. @@ -560,7 +560,7 @@ mod tests { let infos = harnesses.map(|harness| { let mut metadata = mock_metadata(harness.to_string(), krate.clone()); metadata.attributes.proof = true; - (mock_next_harness(), HarnessInfo { stub_map: Stubs::default(), metadata }) + (mock_next_harness_id(), HarnessInfo { stub_map: Stubs::default(), metadata }) }); let all_harnesses = HashMap::from(infos.clone());