diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 039c50eefe18..ca66e1c0e165 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -7,7 +7,8 @@ use crate::args::ReachabilityType; use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::analysis; use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes}; -use crate::kani_middle::metadata::{canonical_mangled_name, gen_test_metadata}; +use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits}; +use crate::kani_middle::metadata::gen_test_metadata; use crate::kani_middle::provide; use crate::kani_middle::reachability::{ collect_reachable_items, filter_const_crate_items, filter_crate_items, @@ -17,7 +18,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::{InternString, RoundingMode}; +use cbmc::RoundingMode; use cbmc::{InternedString, MachineModel}; use kani_metadata::artifact::convert_type; use kani_metadata::UnsupportedFeature; @@ -49,7 +50,6 @@ use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::{CrateDef, DefId}; use std::any::Any; use std::collections::BTreeMap; -use std::collections::HashSet; use std::ffi::OsString; use std::fmt::Write; use std::fs::File; @@ -231,43 +231,43 @@ impl CodegenBackend for GotocCodegenBackend { let base_filepath = tcx.output_filenames(()).path(OutputType::Object); let base_filename = base_filepath.as_path(); let reachability = queries.args().reachability_analysis; - let mut transformer = BodyTransformation::new(&queries, tcx); let mut results = GotoCodegenResults::new(tcx, reachability); match reachability { ReachabilityType::Harnesses => { + let mut units = CodegenUnits::new(&queries, tcx); + let mut modifies_instances = vec![]; // Cross-crate collecting of all items that are reachable from the crate harnesses. - let harnesses = queries.target_harnesses(); - let mut items: HashSet<_> = HashSet::with_capacity(harnesses.len()); - items.extend(harnesses); - let harnesses = filter_crate_items(tcx, |_, instance| { - items.contains(&instance.mangled_name().intern()) - }); - for harness in harnesses { - let model_path = - queries.harness_model_path(&harness.mangled_name()).unwrap(); - let contract_metadata = - contract_metadata_for_harness(tcx, harness.def.def_id()).unwrap(); - let (gcx, items, contract_info) = self.codegen_items( - tcx, - &[MonoItem::Fn(harness)], - model_path, - &results.machine_model, - contract_metadata, - transformer, - ); - transformer = results.extend(gcx, items, None); - if let Some(assigns_contract) = contract_info { - self.queries.lock().unwrap().register_assigns_contract( - canonical_mangled_name(harness).intern(), - assigns_contract, + for unit in units.iter() { + // We reset the body cache for now because each codegen unit has different + // configurations that affect how we transform the instance body. + let mut transformer = BodyTransformation::new(&queries, tcx, &unit); + for harness in &unit.harnesses { + let model_path = units.harness_model_path(*harness).unwrap(); + let contract_metadata = + contract_metadata_for_harness(tcx, harness.def.def_id()).unwrap(); + let (gcx, items, contract_info) = self.codegen_items( + tcx, + &[MonoItem::Fn(*harness)], + model_path, + &results.machine_model, + contract_metadata, + transformer, ); + transformer = results.extend(gcx, items, None); + if let Some(assigns_contract) = contract_info { + modifies_instances.push((*harness, assigns_contract)); + } } } + units.store_modifies(&modifies_instances); + units.write_metadata(&queries, tcx); } 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 unit = CodegenUnit::default(); + let mut transformer = BodyTransformation::new(&queries, tcx, &unit); let mut descriptions = vec![]; let harnesses = filter_const_crate_items(tcx, &mut transformer, |_, item| { if is_test_harness_description(tcx, item.def) { @@ -310,6 +310,8 @@ impl CodegenBackend for GotocCodegenBackend { } ReachabilityType::None => {} ReachabilityType::PubFns => { + let unit = CodegenUnit::default(); + let transformer = BodyTransformation::new(&queries, tcx, &unit); let main_instance = stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap()); let local_reachable = filter_crate_items(tcx, |_, instance| { diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 1793165bdf81..58c22f940352 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -15,34 +15,19 @@ //! in order to apply the stubs. For the subsequent runs, we add the stub configuration to //! `-C llvm-args`. -use crate::args::{Arguments, ReachabilityType}; +use crate::args::Arguments; #[cfg(feature = "cprover")] use crate::codegen_cprover_gotoc::GotocCodegenBackend; -use crate::kani_middle::attributes::is_proof_harness; use crate::kani_middle::check_crate_items; -use crate::kani_middle::metadata::gen_proof_metadata; -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; -use rustc_data_structures::fx::FxHashMap; use rustc_driver::{Callbacks, Compilation, RunCompiler}; -use rustc_hir::def_id::LOCAL_CRATE; -use rustc_hir::definitions::DefPathHash; use rustc_interface::Config; -use rustc_middle::ty::TyCtxt; -use rustc_session::config::{ErrorOutputType, OutputType}; +use rustc_session::config::ErrorOutputType; use rustc_smir::rustc_internal; use rustc_span::ErrorGuaranteed; -use std::collections::{BTreeMap, HashMap}; -use std::fs::File; -use std::io::BufWriter; -use std::mem; -use std::path::{Path, PathBuf}; use std::process::ExitCode; use std::sync::{Arc, Mutex}; use tracing::debug; @@ -69,537 +54,64 @@ fn backend(queries: Arc>) -> Box { compile_error!("No backend is available. Only supported value today is `cprover`"); } -/// A stable (across compilation sessions) identifier for the harness function. -type HarnessId = InternedString; - -/// A set of stubs. -type Stubs = BTreeMap; - -#[derive(Clone, Debug)] -struct HarnessInfo { - pub metadata: HarnessMetadata, - pub stub_map: Stubs, -} - -/// Store some relevant information about the crate compilation. -#[derive(Clone, Debug)] -struct CrateInfo { - /// The name of the crate being compiled. - pub name: String, - /// The metadata output path that shall be generated as part of the crate compilation. - pub output_path: PathBuf, -} - -/// Represents the current compilation stage. -/// -/// The Kani compiler may run the Rust compiler multiple times since stubbing has to be applied -/// to the entire Rust compiler session. -/// -/// - We always start in the [CompilationStage::Init]. -/// - After [CompilationStage::Init] we transition to either -/// - [CompilationStage::CodegenNoStubs] on a regular crate compilation, this will follow Init. -/// - [CompilationStage::CompilationSkipped], running the compiler to gather information, such as -/// `--version` will skip code generation completely, and there is no work to be done. -/// - After the [CompilationStage::CodegenNoStubs], we transition to either -/// - [CompilationStage::CodegenWithStubs] when there is at least one harness with stubs. -/// - [CompilationStage::Done] where there is no harness left to process. -/// - The [CompilationStage::CodegenWithStubs] can last multiple Rust compiler runs. Once there is -/// no harness left, we move to [CompilationStage::Done]. -/// - The final stages are either [CompilationStage::Done] or [CompilationStage::CompilationSkipped]. -/// - [CompilationStage::Done] represents the final state of the compiler after a successful -/// compilation. The crate metadata is stored here (even if no codegen was actually performed). -/// - [CompilationStage::CompilationSkipped] no compilation was actually performed. -/// No work needs to be done. -/// -/// Note: In a scenario where the compilation fails, the compiler will exit immediately, -/// independent on the stage. Any artifact produced shouldn't be used. I.e.: -/// -/// ```dot -/// graph CompilationStage { -/// Init -> {CodegenNoStubs, CompilationSkipped} -/// CodegenNoStubs -> {CodegenStubs, Done} -/// // Loop up to N harnesses times. -/// CodegenStubs -> {CodegenStubs, Done} -/// CompilationSkipped -/// Done -/// } -/// ``` -#[allow(dead_code)] -#[derive(Debug)] -enum CompilationStage { - /// Initial state that the compiler is always instantiated with. - /// In this stage, we initialize the Query and collect all harnesses. - Init, - /// State where the compiler ran but didn't actually compile anything (e.g.: --version). - CompilationSkipped, - /// Stage where the compiler will perform codegen of all harnesses that don't use stub. - CodegenNoStubs { - target_harnesses: Vec, - next_harnesses: Vec>, - all_harnesses: HashMap, - crate_info: CrateInfo, - }, - /// Stage where the compiler will codegen harnesses that use stub, one group at a time. - /// The harnesses at this stage are grouped according to the stubs they are using. For now, - /// we ensure they have the exact same set of stubs. - CodegenWithStubs { - target_harnesses: Vec, - next_harnesses: Vec>, - all_harnesses: HashMap, - crate_info: CrateInfo, - }, - Done { - metadata: Option<(KaniMetadata, CrateInfo)>, - }, -} - -impl CompilationStage { - pub fn is_init(&self) -> bool { - matches!(self, CompilationStage::Init) - } -} - /// This object controls the compiler behavior. /// /// It is responsible for initializing the query database, as well as controlling the compiler -/// state machine. For stubbing, we may require multiple iterations of the rustc driver, which is -/// controlled and configured via KaniCompiler. +/// state machine. struct KaniCompiler { - /// Store the queries database. The queries should be initialized as part of `config` when the + /// Store the query database. The queries should be initialized as part of `config` when the /// compiler state is Init. /// Note that we need to share the queries with the backend before `config` is called. pub queries: Arc>, - /// The state which the compiler is at. - stage: CompilationStage, } impl KaniCompiler { /// Create a new [KaniCompiler] instance. pub fn new() -> KaniCompiler { - KaniCompiler { queries: QueryDb::new(), stage: CompilationStage::Init } + KaniCompiler { queries: QueryDb::new() } } /// Compile the current crate with the given arguments. /// /// Since harnesses may have different attributes that affect compilation, Kani compiler can /// actually invoke the rust compiler multiple times. - pub fn run(&mut self, orig_args: Vec) -> Result<(), ErrorGuaranteed> { - loop { - debug!(next=?self.stage, "run"); - // Because this modifies `self.stage` we need to run this before - // borrowing `&self.stage` immutably - if let CompilationStage::Done { metadata: Some((metadata, _)), .. } = &mut self.stage { - let mut contracts = self - .queries - .lock() - .unwrap() - .assigns_contracts() - .map(|(k, v)| (*k, v.clone())) - .collect::>(); - for harness in - metadata.proof_harnesses.iter_mut().chain(metadata.test_harnesses.iter_mut()) - { - if let Some(modifies_contract) = - contracts.remove(&(&harness.mangled_name).intern()) - { - harness.contract = modifies_contract.into(); - } - } - assert!( - contracts.is_empty(), - "Invariant broken: not all contracts have been handled." - ) - } - match &self.stage { - CompilationStage::Init => self.run_compilation_session(&orig_args)?, - CompilationStage::CodegenNoStubs { .. } => { - unreachable!("This stage should always run in the same session as Init"); - } - CompilationStage::CodegenWithStubs { target_harnesses, all_harnesses, .. } => { - assert!(!target_harnesses.is_empty(), "expected at least one target harness"); - let target_harness_name = &target_harnesses[0]; - let target_harness = &all_harnesses[target_harness_name]; - let extra_arg = stubbing::mk_rustc_arg(&target_harness.stub_map); - let mut args = orig_args.clone(); - args.push(extra_arg); - self.run_compilation_session(&args)? - } - CompilationStage::Done { metadata: Some((kani_metadata, crate_info)) } => { - // Only store metadata for harnesses for now. - // TODO: This should only skip None. - // https://github.com/model-checking/kani/issues/2493 - if self.queries.lock().unwrap().args().reachability_analysis - == ReachabilityType::Harnesses - { - // Store metadata file. - // We delay storing the metadata so we can include information collected - // during codegen. - self.store_metadata(&kani_metadata, &crate_info.output_path); - } - return Ok(()); - } - CompilationStage::Done { metadata: None } - | CompilationStage::CompilationSkipped => { - return Ok(()); - } - }; - - self.next_stage(); - } - } - - /// Set up the next compilation stage after a `rustc` run. - fn next_stage(&mut self) { - self.stage = match &mut self.stage { - CompilationStage::Init => { - // This may occur when user passes arguments like --version or --help. - CompilationStage::Done { metadata: None } - } - CompilationStage::CodegenNoStubs { - next_harnesses, all_harnesses, crate_info, .. - } - | CompilationStage::CodegenWithStubs { - next_harnesses, - all_harnesses, - crate_info, - .. - } => { - if let Some(target_harnesses) = next_harnesses.pop() { - assert!(!target_harnesses.is_empty(), "expected at least one target harness"); - CompilationStage::CodegenWithStubs { - target_harnesses, - next_harnesses: mem::take(next_harnesses), - all_harnesses: mem::take(all_harnesses), - crate_info: crate_info.clone(), - } - } else { - CompilationStage::Done { - metadata: Some(( - generate_metadata(&crate_info, &all_harnesses), - crate_info.clone(), - )), - } - } - } - CompilationStage::Done { .. } | CompilationStage::CompilationSkipped => { - unreachable!() - } - }; - } - - /// Run the Rust compiler with the given arguments and pass `&mut self` to handle callbacks. - fn run_compilation_session(&mut self, args: &[String]) -> Result<(), ErrorGuaranteed> { + pub fn run(&mut self, args: Vec) -> Result<(), ErrorGuaranteed> { debug!(?args, "run_compilation_session"); let queries = self.queries.clone(); - let mut compiler = RunCompiler::new(args, self); + let mut compiler = RunCompiler::new(&args, self); compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| backend(queries)))); compiler.run()?; Ok(()) } - - /// Gather and process all harnesses from this crate that shall be compiled. - fn process_harnesses(&self, tcx: TyCtxt) -> CompilationStage { - let crate_info = CrateInfo { - name: tcx.crate_name(LOCAL_CRATE).as_str().into(), - output_path: metadata_output_path(tcx), - }; - if self.queries.lock().unwrap().args().reachability_analysis == ReachabilityType::Harnesses - { - let base_filepath = tcx.output_filenames(()).path(OutputType::Object); - let base_filename = base_filepath.as_path(); - let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance)); - let all_harnesses = harnesses - .into_iter() - .map(|harness| { - 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 }) - }) - .collect::>(); - - let (no_stubs, with_stubs): (Vec<_>, Vec<_>) = - if self.queries.lock().unwrap().args().stubbing_enabled { - // Partition harnesses that don't have stub with the ones with stub. - all_harnesses - .keys() - .cloned() - .partition(|harness| all_harnesses[harness].stub_map.is_empty()) - } else { - // Generate code without stubs. - (all_harnesses.keys().cloned().collect(), vec![]) - }; - - // Even if no_stubs is empty we still need to store rustc metadata. - CompilationStage::CodegenNoStubs { - target_harnesses: no_stubs, - next_harnesses: group_by_stubs(with_stubs, &all_harnesses), - all_harnesses, - crate_info, - } - } else { - // Leave other reachability type handling as is for now. - CompilationStage::CodegenNoStubs { - target_harnesses: vec![], - next_harnesses: vec![], - all_harnesses: HashMap::default(), - crate_info, - } - } - } - - /// Prepare the query for the next codegen stage. - fn prepare_codegen(&mut self) -> Compilation { - debug!(stage=?self.stage, "prepare_codegen"); - match &self.stage { - CompilationStage::CodegenNoStubs { target_harnesses, all_harnesses, .. } - | CompilationStage::CodegenWithStubs { target_harnesses, all_harnesses, .. } => { - debug!( - harnesses=?target_harnesses - .iter() - .map(|h| &all_harnesses[h].metadata.pretty_name) - .collect::>(), - "prepare_codegen" - ); - let queries = &mut (*self.queries.lock().unwrap()); - queries.harnesses_info = target_harnesses - .iter() - .map(|harness| { - (*harness, all_harnesses[harness].metadata.goto_file.clone().unwrap()) - }) - .collect(); - Compilation::Continue - } - CompilationStage::Init - | CompilationStage::Done { .. } - | CompilationStage::CompilationSkipped => unreachable!(), - } - } - - /// Write the metadata to a file - fn store_metadata(&self, metadata: &KaniMetadata, filename: &Path) { - debug!(?filename, "store_metadata"); - let out_file = File::create(filename).unwrap(); - let writer = BufWriter::new(out_file); - if self.queries.lock().unwrap().args().output_pretty_json { - serde_json::to_writer_pretty(writer, &metadata).unwrap(); - } else { - serde_json::to_writer(writer, &metadata).unwrap(); - } - } -} - -/// Group the harnesses by their stubs. -fn group_by_stubs( - harnesses: Vec, - all_harnesses: &HashMap, -) -> Vec> { - let mut per_stubs: BTreeMap<&Stubs, Vec> = BTreeMap::default(); - for harness in harnesses { - per_stubs.entry(&all_harnesses[&harness].stub_map).or_default().push(harness) - } - per_stubs.into_values().collect() } /// Use default function implementations. impl Callbacks for KaniCompiler { /// Configure the [KaniCompiler] `self` object during the [CompilationStage::Init]. fn config(&mut self, config: &mut Config) { - if self.stage.is_init() { - let mut args = vec!["kani-compiler".to_string()]; - args.extend(config.opts.cg.llvm_args.iter().cloned()); - let args = Arguments::parse_from(args); - init_session(&args, matches!(config.opts.error_format, ErrorOutputType::Json { .. })); - // Configure queries. - let queries = &mut (*self.queries.lock().unwrap()); + let mut args = vec!["kani-compiler".to_string()]; + args.extend(config.opts.cg.llvm_args.iter().cloned()); + let args = Arguments::parse_from(args); + init_session(&args, matches!(config.opts.error_format, ErrorOutputType::Json { .. })); - queries.set_args(args); - - debug!(?queries, "config end"); - } + // Configure queries. + let queries = &mut (*self.queries.lock().unwrap()); + queries.set_args(args); + debug!(?queries, "config end"); } - /// During the initialization state, we collect the crate harnesses and prepare for codegen. + /// After analysis, we check the crate items for Kani API misuse or configuration issues. fn after_analysis<'tcx>( &mut self, _compiler: &rustc_interface::interface::Compiler, rustc_queries: &'tcx rustc_interface::Queries<'tcx>, ) -> Compilation { - if self.stage.is_init() { - self.stage = rustc_queries.global_ctxt().unwrap().enter(|tcx| { - rustc_internal::run(tcx, || { - check_crate_items(tcx, self.queries.lock().unwrap().args().ignore_global_asm); - self.process_harnesses(tcx) - }) - .unwrap() + rustc_queries.global_ctxt().unwrap().enter(|tcx| { + rustc_internal::run(tcx, || { + check_crate_items(tcx, self.queries.lock().unwrap().args().ignore_global_asm); }) - } - - self.prepare_codegen() - } -} - -/// Generate [KaniMetadata] for the target crate. -fn generate_metadata( - crate_info: &CrateInfo, - all_harnesses: &HashMap, -) -> KaniMetadata { - let (proof_harnesses, test_harnesses) = all_harnesses - .values() - .map(|info| &info.metadata) - .cloned() - .partition(|md| md.attributes.proof); - KaniMetadata { - crate_name: crate_info.name.clone(), - proof_harnesses, - unsupported_features: vec![], - test_harnesses, - } -} - -/// Extract the filename for the metadata file. -fn metadata_output_path(tcx: TyCtxt) -> PathBuf { - let filepath = tcx.output_filenames(()).path(OutputType::Object); - let filename = filepath.as_path(); - filename.with_extension(ArtifactType::Metadata).to_path_buf() -} - -#[cfg(test)] -mod tests { - use super::*; - use kani_metadata::HarnessAttributes; - use rustc_data_structures::fingerprint::Fingerprint; - - 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_id() -> DefPathHash { - static mut COUNTER: u64 = 0; - unsafe { COUNTER += 1 }; - let id = unsafe { COUNTER }; - DefPathHash(Fingerprint::new(id, 0)) - } - - fn mock_metadata(name: String, krate: String) -> HarnessMetadata { - HarnessMetadata { - pretty_name: name.clone(), - mangled_name: name.clone(), - original_file: format!("{}.rs", krate), - crate_name: krate, - original_start_line: 10, - original_end_line: 20, - goto_file: None, - attributes: HarnessAttributes::default(), - contract: Default::default(), - } - } - - fn mock_info_with_stubs(stub_map: Stubs) -> HarnessInfo { - HarnessInfo { metadata: mock_metadata("dummy".to_string(), "crate".to_string()), stub_map } - } - - #[test] - fn test_group_by_stubs_works() { - // Set up the inputs - 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_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]); - let set_3 = Stubs::from([stub_1, stub_3, stub_2]); - assert_eq!(set_1, set_3); - assert_ne!(set_1, set_2); - - let harnesses_info = HashMap::from([ - (harness_1, mock_info_with_stubs(set_1)), - (harness_2, mock_info_with_stubs(set_2)), - (harness_3, mock_info_with_stubs(set_3)), - ]); - assert_eq!(harnesses_info.len(), 3); - - // Run the function under test. - let grouped = group_by_stubs(harnesses, &harnesses_info); - - // Verify output. - assert_eq!(grouped.len(), 2); - assert!( - grouped.contains(&vec![harness_1, harness_3]) - || grouped.contains(&vec![harness_3, harness_1]) - ); - assert!(grouped.contains(&vec![harness_2])); - } - - #[test] - fn test_generate_metadata() { - // Mock inputs. - let name = "my_crate".to_string(); - let crate_info = CrateInfo { name: name.clone(), output_path: PathBuf::default() }; - - let mut info = mock_info_with_stubs(Stubs::default()); - info.metadata.attributes.proof = true; - let id = mock_next_harness_id(); - let all_harnesses = HashMap::from([(id, info.clone())]); - - // Call generate metadata. - let metadata = generate_metadata(&crate_info, &all_harnesses); - - // Check output. - assert_eq!(metadata.crate_name, name); - assert_eq!(metadata.proof_harnesses.len(), 1); - assert_eq!(*metadata.proof_harnesses.first().unwrap(), info.metadata); - } - - #[test] - fn test_generate_empty_metadata() { - // Mock inputs. - let name = "my_crate".to_string(); - let crate_info = CrateInfo { name: name.clone(), output_path: PathBuf::default() }; - let all_harnesses = HashMap::new(); - - // Call generate metadata. - let metadata = generate_metadata(&crate_info, &all_harnesses); - - // Check output. - assert_eq!(metadata.crate_name, name); - assert_eq!(metadata.proof_harnesses.len(), 0); - } - - #[test] - fn test_generate_metadata_with_multiple_harness() { - // Mock inputs. - let krate = "my_crate".to_string(); - let crate_info = CrateInfo { name: krate.clone(), output_path: PathBuf::default() }; - - let harnesses = ["h1", "h2", "h3"]; - let infos = harnesses.map(|harness| { - let mut metadata = mock_metadata(harness.to_string(), krate.clone()); - metadata.attributes.proof = true; - (mock_next_harness_id(), HarnessInfo { stub_map: Stubs::default(), metadata }) + .unwrap() }); - let all_harnesses = HashMap::from(infos.clone()); - - // Call generate metadata. - let metadata = generate_metadata(&crate_info, &all_harnesses); - - // Check output. - assert_eq!(metadata.crate_name, krate); - assert_eq!(metadata.proof_harnesses.len(), infos.len()); - assert!( - metadata - .proof_harnesses - .iter() - .all(|harness| harnesses.contains(&&*harness.pretty_name)) - ); + Compilation::Continue } } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 4f9dce49af95..e2617739e461 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -198,10 +198,6 @@ impl<'tcx> KaniAttributes<'tcx> { .collect() } - pub(crate) fn is_contract_generated(&self) -> bool { - self.map.contains_key(&KaniAttributeKind::IsContractGenerated) - } - pub(crate) fn has_recursion(&self) -> bool { self.map.contains_key(&KaniAttributeKind::Recursion) } @@ -238,6 +234,11 @@ impl<'tcx> KaniAttributes<'tcx> { .map(|target| expect_key_string_value(self.tcx.sess, target)) } + pub fn proof_for_contract(&self) -> Option> { + self.expect_maybe_one(KaniAttributeKind::ProofForContract) + .map(|target| expect_key_string_value(self.tcx.sess, target)) + } + pub fn inner_check(&self) -> Option> { self.eval_sibling_attribute(KaniAttributeKind::InnerCheck) } diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs new file mode 100644 index 000000000000..260b363a868a --- /dev/null +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -0,0 +1,213 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module is responsible for extracting grouping harnesses that can be processed together +//! by codegen. +//! +//! Today, only stub / contracts can affect the harness codegen. Thus, we group the harnesses +//! according to their stub configuration. + +use crate::args::ReachabilityType; +use crate::kani_middle::attributes::is_proof_harness; +use crate::kani_middle::metadata::gen_proof_metadata; +use crate::kani_middle::reachability::filter_crate_items; +use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; +use crate::kani_queries::QueryDb; +use kani_metadata::{ArtifactType, AssignsContract, HarnessMetadata, KaniMetadata}; +use rustc_hir::def_id::{DefId, DefPathHash}; +use rustc_middle::ty::TyCtxt; +use rustc_session::config::OutputType; +use rustc_smir::rustc_internal; +use stable_mir::mir::mono::Instance; +use stable_mir::ty::{FnDef, RigidTy, TyKind}; +use stable_mir::CrateDef; +use std::collections::{BTreeMap, HashMap, HashSet}; +use std::fs::File; +use std::io::BufWriter; +use std::path::{Path, PathBuf}; +use tracing::debug; + +/// A stable (across compilation sessions) identifier for the harness function. +type Harness = Instance; + +/// A set of stubs. +pub type Stubs = HashMap; + +/// Store some relevant information about the crate compilation. +#[derive(Clone, Debug)] +struct CrateInfo { + /// The name of the crate being compiled. + pub name: String, +} + +/// We group the harnesses that have the same stubs. +pub struct CodegenUnits { + units: Vec, + harness_info: HashMap, + crate_info: CrateInfo, +} + +#[derive(Clone, Default, Debug)] +pub struct CodegenUnit { + pub harnesses: Vec, + pub stubs: Stubs, +} + +impl CodegenUnits { + pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self { + let crate_info = CrateInfo { name: stable_mir::local_crate().name.as_str().into() }; + if queries.args().reachability_analysis == ReachabilityType::Harnesses { + let base_filepath = tcx.output_filenames(()).path(OutputType::Object); + let base_filename = base_filepath.as_path(); + let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance)); + let all_harnesses = harnesses + .into_iter() + .map(|harness| { + let metadata = gen_proof_metadata(tcx, harness, &base_filename); + (harness, metadata) + }) + .collect::>(); + + // Even if no_stubs is empty we still need to store rustc metadata. + let units = group_by_stubs(tcx, &all_harnesses); + validate_units(tcx, &units); + debug!(?units, "CodegenUnits::new"); + CodegenUnits { units, harness_info: all_harnesses, crate_info } + } else { + // Leave other reachability type handling as is for now. + CodegenUnits { units: vec![], harness_info: HashMap::default(), crate_info } + } + } + + pub fn iter(&self) -> impl Iterator { + self.units.iter() + } + + /// We store which instance of modifies was generated. + pub fn store_modifies(&mut self, harness_modifies: &[(Harness, AssignsContract)]) { + for (harness, modifies) in harness_modifies { + self.harness_info.get_mut(harness).unwrap().contract = Some(modifies.clone()); + } + } + + /// Write compilation metadata into a file. + pub fn write_metadata(&self, queries: &QueryDb, tcx: TyCtxt) { + let metadata = self.generate_metadata(); + let outpath = metadata_output_path(tcx); + store_metadata(queries, &metadata, &outpath); + } + + pub fn harness_model_path(&self, harness: Harness) -> Option<&PathBuf> { + self.harness_info[&harness].goto_file.as_ref() + } + + /// Generate [KaniMetadata] for the target crate. + fn generate_metadata(&self) -> KaniMetadata { + let (proof_harnesses, test_harnesses) = + self.harness_info.values().cloned().partition(|md| md.attributes.proof); + KaniMetadata { + crate_name: self.crate_info.name.clone(), + proof_harnesses, + unsupported_features: vec![], + test_harnesses, + } + } +} + +fn stub_def(tcx: TyCtxt, def_id: DefId) -> FnDef { + let ty_internal = tcx.type_of(def_id).instantiate_identity(); + let ty = rustc_internal::stable(ty_internal); + if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = ty.kind() { + def + } else { + unreachable!("Expected stub function for `{:?}`, but found: {ty}", tcx.def_path(def_id)) + } +} + +/// Group the harnesses by their stubs. +fn group_by_stubs( + tcx: TyCtxt, + all_harnesses: &HashMap, +) -> Vec { + let mut per_stubs: HashMap, CodegenUnit> = + HashMap::default(); + for (harness, metadata) in all_harnesses { + let stub_ids = harness_stub_map(tcx, *harness, metadata); + let stub_map = stub_ids + .iter() + .map(|(k, v)| (tcx.def_path_hash(*k), tcx.def_path_hash(*v))) + .collect::>(); + if let Some(unit) = per_stubs.get_mut(&stub_map) { + unit.harnesses.push(*harness); + } else { + let stubs = stub_ids + .iter() + .map(|(from, to)| (stub_def(tcx, *from), stub_def(tcx, *to))) + .collect::>(); + let stubs = apply_transitivity(tcx, *harness, stubs); + per_stubs.insert(stub_map, CodegenUnit { stubs, harnesses: vec![*harness] }); + } + } + per_stubs.into_values().collect() +} + +/// Extract the filename for the metadata file. +fn metadata_output_path(tcx: TyCtxt) -> PathBuf { + let filepath = tcx.output_filenames(()).path(OutputType::Object); + let filename = filepath.as_path(); + filename.with_extension(ArtifactType::Metadata).to_path_buf() +} + +/// Write the metadata to a file +fn store_metadata(queries: &QueryDb, metadata: &KaniMetadata, filename: &Path) { + debug!(?filename, "store_metadata"); + let out_file = File::create(filename).unwrap(); + let writer = BufWriter::new(out_file); + if queries.args().output_pretty_json { + serde_json::to_writer_pretty(writer, &metadata).unwrap(); + } else { + serde_json::to_writer(writer, &metadata).unwrap(); + } +} + +/// Validate the unit configuration. +fn validate_units(tcx: TyCtxt, units: &[CodegenUnit]) { + for unit in units { + for (from, to) in &unit.stubs { + // We use harness span since we don't keep the attribute span. + let Err(msg) = check_compatibility(tcx, *from, *to) else { continue }; + let span = unit.harnesses.first().unwrap().def.span(); + tcx.dcx().span_err(rustc_internal::internal(tcx, span), msg); + } + } + tcx.dcx().abort_if_errors(); +} + +/// Apply stub transitivity operations. +/// +/// If `fn1` is stubbed by `fn2`, and `fn2` is stubbed by `fn3`, `f1` is in fact stubbed by `fn3`. +fn apply_transitivity(tcx: TyCtxt, harness: Harness, stubs: Stubs) -> Stubs { + let mut new_stubs = Stubs::with_capacity(stubs.len()); + for (orig, new) in stubs.iter() { + let mut new_fn = *new; + let mut visited = HashSet::new(); + while let Some(stub) = stubs.get(&new_fn) { + if !visited.insert(stub) { + // Visiting the same stub, i.e. found cycle. + let span = harness.def.span(); + tcx.dcx().span_err( + rustc_internal::internal(tcx, span), + format!( + "Cannot stub `{}`. Stub configuration for harness `{}` has a cycle", + orig.name(), + harness.def.name(), + ), + ); + break; + } + new_fn = *stub; + } + new_stubs.insert(*orig, new_fn); + } + new_stubs +} diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 9236de48308f..2bf1531a2a1a 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -23,7 +23,7 @@ pub fn canonical_mangled_name(instance: Instance) -> String { /// Create the harness metadata for a proof harness for a given function. 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 kani_attributes = KaniAttributes::for_instance(tcx, instance); let pretty_name = instance.name(); let mangled_name = canonical_mangled_name(instance); @@ -40,7 +40,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> original_file: loc.filename, original_start_line: loc.start_line, original_end_line: loc.end_line, - attributes, + attributes: kani_attributes.harness_attributes(), // TODO: This no longer needs to be an Option. goto_file: Some(model_file), contract: Default::default(), diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 17992953d5c7..257d337cd576 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -32,6 +32,7 @@ use self::attributes::KaniAttributes; pub mod analysis; pub mod attributes; +pub mod codegen_units; pub mod coercion; mod intrinsics; pub mod metadata; diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index d9197493f4db..91b830a2349b 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -6,16 +6,10 @@ use crate::args::{Arguments, ReachabilityType}; use crate::kani_middle::intrinsics::ModelIntrinsics; -use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items}; -use crate::kani_middle::stubbing; -use crate::kani_middle::transform::BodyTransformation; use crate::kani_queries::QueryDb; use rustc_hir::def_id::{DefId, LocalDefId}; use rustc_middle::util::Providers; -use rustc_middle::{mir::Body, query::queries, ty::TyCtxt}; -use stable_mir::mir::mono::MonoItem; - -use crate::kani_middle::KaniAttributes; +use rustc_middle::{mir::Body, ty::TyCtxt}; /// Sets up rustc's query mechanism to apply Kani's custom queries to code from /// a crate. @@ -25,10 +19,6 @@ pub fn provide(providers: &mut Providers, queries: &QueryDb) { // Don't override queries if we are only compiling our dependencies. providers.optimized_mir = run_mir_passes; providers.extern_queries.optimized_mir = run_mir_passes_extern; - if args.stubbing_enabled { - // TODO: Check if there's at least one stub being applied. - providers.collect_and_partition_mono_items = collect_and_partition_mono_items; - } } } @@ -61,42 +51,8 @@ fn run_kani_mir_passes<'tcx>( body: &'tcx Body<'tcx>, ) -> &'tcx Body<'tcx> { tracing::debug!(?def_id, "Run Kani transformation passes"); - let mut transformed_body = stubbing::transform(tcx, def_id, body); - stubbing::transform_foreign_functions(tcx, &mut transformed_body); - let item_attributes = KaniAttributes::for_item(tcx, def_id); - // If we apply `transform_any_modifies` in all contract-generated items, - // we will ended up instantiating `kani::any_modifies` for the replace function - // every time, even if we are only checking the contract, because the function - // is always included during contract instrumentation. Thus, we must only apply - // the transformation if we are using a verified stub or in the presence of recursion. - if item_attributes.is_contract_generated() - && (stubbing::get_stub_key(tcx, def_id).is_some() || item_attributes.has_recursion()) - { - stubbing::transform_any_modifies(tcx, &mut transformed_body); - } + let mut transformed_body = body.clone(); // This should be applied after stubbing so user stubs take precedence. ModelIntrinsics::run_pass(tcx, &mut transformed_body); tcx.arena.alloc(transformed_body) } - -/// Runs a reachability analysis before running the default -/// `collect_and_partition_mono_items` query. The reachability analysis finds -/// trait mismatches introduced by stubbing and performs a graceful exit in -/// these cases. Left to its own devices, the default query panics. -/// This is an issue when compiling a library, since the crate metadata is -/// generated (using this query) before code generation begins (which is -/// when we normally run the reachability analysis). -fn collect_and_partition_mono_items( - tcx: TyCtxt, - key: (), -) -> queries::collect_and_partition_mono_items::ProvidedValue { - rustc_smir::rustc_internal::run(tcx, || { - 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, &mut BodyTransformation::dummy(), &local_reachable); - }) - .unwrap(); - (rustc_interface::DEFAULT_QUERY_PROVIDERS.collect_and_partition_mono_items)(tcx, key) -} diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 71eb4931aad4..186bd65a7840 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -33,10 +33,8 @@ use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind} use stable_mir::CrateItem; use stable_mir::{CrateDef, ItemKind}; -use crate::kani_middle::attributes::matches_diagnostic as matches_function; use crate::kani_middle::coercion; use crate::kani_middle::coercion::CoercionBase; -use crate::kani_middle::stubbing::{get_stub, validate_instance}; use crate::kani_middle::transform::BodyTransformation; /// Collect all reachable items starting from the given starting points. @@ -113,12 +111,8 @@ where if let Ok(instance) = Instance::try_from(item) { if predicate(tcx, instance) { let body = transformer.body(tcx, instance); - let mut collector = MonoItemsFnCollector { - tcx, - body: &body, - collected: FxHashSet::default(), - instance: &instance, - }; + let mut collector = + MonoItemsFnCollector { tcx, body: &body, collected: FxHashSet::default() }; collector.visit_body(&body); roots.extend(collector.collected.into_iter()); } @@ -185,19 +179,11 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> { /// Visit a function and collect all mono-items reachable from its instructions. fn visit_fn(&mut self, instance: Instance) -> Vec { let _guard = debug_span!("visit_fn", function=?instance).entered(); - if validate_instance(self.tcx, instance) { - let body = self.transformer.body(self.tcx, instance); - let mut collector = MonoItemsFnCollector { - tcx: self.tcx, - collected: FxHashSet::default(), - body: &body, - instance: &instance, - }; - collector.visit_body(&body); - collector.collected.into_iter().collect() - } else { - vec![] - } + let body = self.transformer.body(self.tcx, instance); + let mut collector = + MonoItemsFnCollector { tcx: self.tcx, collected: FxHashSet::default(), body: &body }; + collector.visit_body(&body); + collector.collected.into_iter().collect() } /// Visit a static object and collect drop / initialization functions. @@ -229,7 +215,6 @@ struct MonoItemsFnCollector<'a, 'tcx> { tcx: TyCtxt<'tcx>, collected: FxHashSet, body: &'a Body, - instance: &'a Instance, } impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { @@ -403,65 +388,8 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> { TerminatorKind::Call { ref func, .. } => { let fn_ty = func.ty(self.body.locals()).unwrap(); if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = fn_ty.kind() { - let instance_opt = Instance::resolve(fn_def, &args).ok(); - match instance_opt { - None => { - let caller = CrateItem::try_from(*self.instance).unwrap().name(); - let callee = fn_def.name(); - // Check if the current function has been stubbed. - if let Some(stub) = get_stub( - self.tcx, - rustc_internal::internal(self.tcx, self.instance).def_id(), - ) { - // During the MIR stubbing transformation, we do not - // force type variables in the stub's signature to - // implement the same traits as those in the - // original function/method. A trait mismatch shows - // up here, when we try to resolve a trait method - - // FIXME: This assumes the type resolving the - // trait is the first argument, but that isn't - // necessarily true. It could be any argument or - // even the return type, for instance for a - // trait like `FromIterator`. - let receiver_ty = args.0[0].expect_ty(); - let sep = callee.rfind("::").unwrap(); - let trait_ = &callee[..sep]; - self.tcx.dcx().span_err( - rustc_internal::internal(self.tcx, terminator.span), - format!( - "`{}` doesn't implement \ - `{}`. The function `{}` \ - cannot be stubbed by `{}` due to \ - generic bounds not being met. Callee: {}", - receiver_ty, - trait_, - caller, - self.tcx.def_path_str(stub), - callee, - ), - ); - } else if matches_function(self.tcx, self.instance.def, "KaniAny") { - let receiver_ty = args.0[0].expect_ty(); - let sep = callee.rfind("::").unwrap(); - let trait_ = &callee[..sep]; - self.tcx.dcx().span_err( - rustc_internal::internal(self.tcx, terminator.span), - format!( - "`{}` doesn't implement \ - `{}`. Callee: `{}`\nPlease, check whether the type of all \ - objects in the modifies clause (including return types) \ - implement `{}`.\nThis is a strict condition to use \ - function contracts as verified stubs.", - receiver_ty, trait_, callee, trait_, - ), - ); - } else { - panic!("unable to resolve call to `{callee}` in `{caller}`") - } - } - Some(instance) => self.collect_instance(instance, true), - }; + let instance = Instance::resolve(fn_def, &args).unwrap(); + self.collect_instance(instance, true); } else { assert!( matches!(fn_ty.kind().rigid(), Some(RigidTy::FnPtr(..))), diff --git a/kani-compiler/src/kani_middle/stubbing/annotations.rs b/kani-compiler/src/kani_middle/stubbing/annotations.rs index 26e508707207..9fc7be491d85 100644 --- a/kani-compiler/src/kani_middle/stubbing/annotations.rs +++ b/kani-compiler/src/kani_middle/stubbing/annotations.rs @@ -2,11 +2,10 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! This file contains code for extracting stubbing-related attributes. -use std::collections::BTreeMap; +use std::collections::HashMap; use kani_metadata::Stub; use rustc_hir::def_id::{DefId, LocalDefId}; -use rustc_hir::definitions::DefPathHash; use rustc_middle::ty::TyCtxt; use crate::kani_middle::resolve::resolve_fn; @@ -42,21 +41,19 @@ pub fn update_stub_mapping( tcx: TyCtxt, harness: LocalDefId, stub: &Stub, - stub_pairs: &mut BTreeMap, + stub_pairs: &mut HashMap, ) { if let Some((orig_id, stub_id)) = stub_def_ids(tcx, harness, stub) { - let orig_hash = tcx.def_path_hash(orig_id); - let stub_hash = tcx.def_path_hash(stub_id); - let other_opt = stub_pairs.insert(orig_hash, stub_hash); + let other_opt = stub_pairs.insert(orig_id, stub_id); if let Some(other) = other_opt { - if other != stub_hash { + if other != stub_id { tcx.dcx().span_err( tcx.def_span(harness), format!( "duplicate stub mapping: {} mapped to {} and {}", tcx.def_path_str(orig_id), tcx.def_path_str(stub_id), - tcx.def_path_str(tcx.def_path_hash_to_def_id(other, &())) + tcx.def_path_str(other) ), ); } diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 37426bfe0b77..1abcc0ec4f80 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -3,21 +3,21 @@ //! This module contains code for implementing stubbing. mod annotations; -mod transform; +use itertools::Itertools; use rustc_span::DUMMY_SP; -use std::collections::BTreeMap; +use std::collections::HashMap; use tracing::{debug, trace}; -pub use self::transform::*; use kani_metadata::HarnessMetadata; -use rustc_hir::definitions::DefPathHash; +use rustc_hir::def_id::DefId; use rustc_middle::mir::Const; use rustc_middle::ty::{self, EarlyBinder, ParamEnv, TyCtxt, TypeFoldable}; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::visit::{Location, MirVisitor}; use stable_mir::mir::Constant; +use stable_mir::ty::FnDef; use stable_mir::{CrateDef, CrateItem}; use self::annotations::update_stub_mapping; @@ -27,16 +27,89 @@ pub fn harness_stub_map( tcx: TyCtxt, harness: Instance, metadata: &HarnessMetadata, -) -> BTreeMap { +) -> HashMap { let def_id = rustc_internal::internal(tcx, harness.def.def_id()); let attrs = &metadata.attributes; - let mut stub_pairs = BTreeMap::default(); + let mut stub_pairs = HashMap::default(); for stubs in &attrs.stubs { update_stub_mapping(tcx, def_id.expect_local(), stubs, &mut stub_pairs); } stub_pairs } +/// Checks whether the stub is compatible with the original function/method: do +/// the arities and types (of the parameters and return values) match up? This +/// does **NOT** check whether the type variables are constrained to implement +/// the same traits; trait mismatches are checked during monomorphization. +pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Result<(), String> { + // TODO: Validate stubs that do not have body. + // We could potentially look at the function signature to see if they match. + // However, they will include region information which can make types different. + let Some(old_body) = old_def.body() else { return Ok(()) }; + let Some(new_body) = new_def.body() else { return Ok(()) }; + // Check whether the arities match. + if old_body.arg_locals().len() != new_body.arg_locals().len() { + let msg = format!( + "arity mismatch: original function/method `{}` takes {} argument(s), stub `{}` takes {}", + old_def.name(), + old_body.arg_locals().len(), + new_def.name(), + new_body.arg_locals().len(), + ); + return Err(msg); + } + // Check whether the numbers of generic parameters match. + let old_def_id = rustc_internal::internal(tcx, old_def.def_id()); + let new_def_id = rustc_internal::internal(tcx, new_def.def_id()); + let old_num_generics = tcx.generics_of(old_def_id).count(); + let stub_num_generics = tcx.generics_of(new_def_id).count(); + if old_num_generics != stub_num_generics { + let msg = format!( + "mismatch in the number of generic parameters: original function/method `{}` takes {} generic parameters(s), stub `{}` takes {}", + old_def.name(), + old_num_generics, + new_def.name(), + stub_num_generics + ); + return Err(msg); + } + // Check whether the types match. Index 0 refers to the returned value, + // indices [1, `arg_count`] refer to the parameters. + // TODO: We currently force generic parameters in the stub to have exactly + // the same names as their counterparts in the original function/method; + // instead, we should be checking for the equivalence of types up to the + // renaming of generic parameters. + // + let old_ret_ty = old_body.ret_local().ty; + let new_ret_ty = new_body.ret_local().ty; + let mut diff = vec![]; + if old_ret_ty != new_ret_ty { + diff.push(format!("Expected return type `{old_ret_ty}`, but found `{new_ret_ty}`")); + } + for (i, (old_arg, new_arg)) in + old_body.arg_locals().iter().zip(new_body.arg_locals().iter()).enumerate() + { + if old_arg.ty != new_arg.ty { + diff.push(format!( + "Expected type `{}` for parameter {}, but found `{}`", + old_arg.ty, + i + 1, + new_arg.ty + )); + } + } + if !diff.is_empty() { + Err(format!( + "Cannot stub `{}` by `{}`.\n - {}", + old_def.name(), + new_def.name(), + diff.iter().join("\n - ") + )) + } else { + Ok(()) + } +} + /// Validate that an instance body can be instantiated. /// /// Stubbing may cause an instance to not be correctly instantiated since we delay checking its @@ -44,17 +117,13 @@ pub fn harness_stub_map( /// /// In stable MIR, trying to retrieve an `Instance::body()` will ICE if we cannot evaluate a /// constant as expected. For now, use internal APIs to anticipate this issue. -pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool { +pub fn validate_stub_const(tcx: TyCtxt, instance: Instance) -> bool { + debug!(?instance, "validate_instance"); + let item = CrateItem::try_from(instance).unwrap(); let internal_instance = rustc_internal::internal(tcx, instance); - if get_stub(tcx, internal_instance.def_id()).is_some() { - debug!(?instance, "validate_instance"); - let item = CrateItem::try_from(instance).unwrap(); - let mut checker = StubConstChecker::new(tcx, internal_instance, item); - checker.visit_body(&item.body()); - checker.is_valid() - } else { - true - } + let mut checker = StubConstChecker::new(tcx, internal_instance, item); + checker.visit_body(&item.body()); + checker.is_valid() } struct StubConstChecker<'tcx> { diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs deleted file mode 100644 index f101a6009907..000000000000 --- a/kani-compiler/src/kani_middle/stubbing/transform.rs +++ /dev/null @@ -1,261 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module contains code related to the MIR-to-MIR pass that performs the -//! stubbing of functions and methods. The primary function of the module is -//! `transform`, which takes the `DefId` of a function/method and returns the -//! body of its stub, if appropriate. The stub mapping it uses is set via rustc -//! arguments. - -use std::collections::{BTreeMap, HashMap}; - -use lazy_static::lazy_static; -use regex::Regex; -use rustc_data_structures::fingerprint::Fingerprint; -use rustc_hir::{def_id::DefId, definitions::DefPathHash}; -use rustc_index::IndexVec; -use rustc_middle::mir::{ - visit::MutVisitor, Body, Const, ConstValue, Local, LocalDecl, Location, Operand, -}; -use rustc_middle::ty::{self, TyCtxt}; - -use tracing::debug; - -/// Returns the `DefId` of the stub for the function/method identified by the -/// parameter `def_id`, and `None` if the function/method is not stubbed. -pub fn get_stub(tcx: TyCtxt, def_id: DefId) -> Option { - let stub_map = get_stub_mapping(tcx)?; - stub_map.get(&def_id).copied() -} - -pub fn get_stub_key(tcx: TyCtxt, def_id: DefId) -> Option { - let stub_map = get_stub_mapping(tcx)?; - stub_map.iter().find_map(|(&key, &val)| if val == def_id { Some(key) } else { None }) -} - -/// Returns the new body of a function/method if it has been stubbed out; -/// otherwise, returns the old body. -pub fn transform<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, old_body: &'tcx Body<'tcx>) -> Body<'tcx> { - if let Some(replacement) = get_stub(tcx, def_id) { - debug!( - original = tcx.def_path_debug_str(def_id), - replaced = tcx.def_path_debug_str(replacement), - "transform" - ); - let new_body = tcx.optimized_mir(replacement).clone(); - if check_compatibility(tcx, def_id, old_body, replacement, &new_body) { - return new_body; - } - } - old_body.clone() -} - -/// Traverse `body` searching for calls to foreing functions and, whevever there is -/// a stub available, replace the call to the foreign function with a call -/// to its correspondent stub. This happens as a separate step because there is no -/// body available to foreign functions at this stage. -pub fn transform_foreign_functions<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) { - if let Some(stub_map) = get_stub_mapping(tcx) { - let mut visitor = - ForeignFunctionTransformer { tcx, local_decls: body.clone().local_decls, stub_map }; - visitor.visit_body(body); - } -} - -/// Traverse `body` searching for calls to `kani::any_modifies` and replace these calls -/// with calls to `kani::any`. This happens as a separate step as it is only necessary -/// for contract-generated functions. -pub fn transform_any_modifies<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) { - let mut visitor = AnyModifiesTransformer { tcx, local_decls: body.clone().local_decls }; - visitor.visit_body(body); -} - -struct AnyModifiesTransformer<'tcx> { - /// The compiler context. - tcx: TyCtxt<'tcx>, - /// Local declarations of the callee function. Kani searches here for foreign functions. - local_decls: IndexVec>, -} - -impl<'tcx> MutVisitor<'tcx> for AnyModifiesTransformer<'tcx> { - fn tcx(&self) -> TyCtxt<'tcx> { - self.tcx - } - - fn visit_operand(&mut self, operand: &mut Operand<'tcx>, _location: Location) { - let func_ty = operand.ty(&self.local_decls, self.tcx); - if let ty::FnDef(reachable_function, arguments) = *func_ty.kind() { - if let Some(any_modifies) = self.tcx.get_diagnostic_name(reachable_function) - && any_modifies.as_str() == "KaniAnyModifies" - { - let Operand::Constant(function_definition) = operand else { - return; - }; - let kani_any_symbol = self - .tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAny")) - .expect("We should have a `kani::any()` definition at this point."); - function_definition.const_ = Const::from_value( - ConstValue::ZeroSized, - self.tcx.type_of(kani_any_symbol).instantiate(self.tcx, arguments), - ); - } - } - } -} - -struct ForeignFunctionTransformer<'tcx> { - /// The compiler context. - tcx: TyCtxt<'tcx>, - /// Local declarations of the callee function. Kani searches here for foreign functions. - local_decls: IndexVec>, - /// Map of functions/methods to their correspondent stubs. - stub_map: HashMap, -} - -impl<'tcx> MutVisitor<'tcx> for ForeignFunctionTransformer<'tcx> { - fn tcx(&self) -> TyCtxt<'tcx> { - self.tcx - } - - fn visit_operand(&mut self, operand: &mut Operand<'tcx>, _location: Location) { - let func_ty = operand.ty(&self.local_decls, self.tcx); - if let ty::FnDef(reachable_function, arguments) = *func_ty.kind() { - if self.tcx.is_foreign_item(reachable_function) { - if let Some(stub) = self.stub_map.get(&reachable_function) { - let Operand::Constant(function_definition) = operand else { - return; - }; - function_definition.const_ = Const::from_value( - ConstValue::ZeroSized, - self.tcx.type_of(stub).instantiate(self.tcx, arguments), - ); - } - } - } - } -} - -/// Checks whether the stub is compatible with the original function/method: do -/// the arities and types (of the parameters and return values) match up? This -/// does **NOT** check whether the type variables are constrained to implement -/// the same traits; trait mismatches are checked during monomorphization. -fn check_compatibility<'a, 'tcx>( - tcx: TyCtxt, - old_def_id: DefId, - old_body: &'a Body<'tcx>, - stub_def_id: DefId, - stub_body: &'a Body<'tcx>, -) -> bool { - // Check whether the arities match. - if old_body.arg_count != stub_body.arg_count { - tcx.dcx().span_err( - tcx.def_span(stub_def_id), - format!( - "arity mismatch: original function/method `{}` takes {} argument(s), stub `{}` takes {}", - tcx.def_path_str(old_def_id), - old_body.arg_count, - tcx.def_path_str(stub_def_id), - stub_body.arg_count - ), - ); - return false; - } - // Check whether the numbers of generic parameters match. - let old_num_generics = tcx.generics_of(old_def_id).count(); - let stub_num_generics = tcx.generics_of(stub_def_id).count(); - if old_num_generics != stub_num_generics { - tcx.dcx().span_err( - tcx.def_span(stub_def_id), - format!( - "mismatch in the number of generic parameters: original function/method `{}` takes {} generic parameters(s), stub `{}` takes {}", - tcx.def_path_str(old_def_id), - old_num_generics, - tcx.def_path_str(stub_def_id), - stub_num_generics - ), - ); - return false; - } - // Check whether the types match. Index 0 refers to the returned value, - // indices [1, `arg_count`] refer to the parameters. - // TODO: We currently force generic parameters in the stub to have exactly - // the same names as their counterparts in the original function/method; - // instead, we should be checking for the equivalence of types up to the - // renaming of generic parameters. - // - let mut matches = true; - for i in 0..=old_body.arg_count { - let old_arg = old_body.local_decls.get(i.into()).unwrap(); - let new_arg = stub_body.local_decls.get(i.into()).unwrap(); - if old_arg.ty != new_arg.ty { - let prefix = if i == 0 { - "return type differs".to_string() - } else { - format!("type of parameter {} differs", i - 1) - }; - tcx.dcx().span_err( - new_arg.source_info.span, - format!( - "{prefix}: stub `{}` has type `{}` where original function/method `{}` has type `{}`", - tcx.def_path_str(stub_def_id), - new_arg.ty, - tcx.def_path_str(old_def_id), - old_arg.ty - ), - ); - matches = false; - } - } - matches -} - -/// The prefix we will use when serializing the stub mapping as a rustc argument. -const RUSTC_ARG_PREFIX: &str = "kani_stubs="; - -/// Serializes the stub mapping into a rustc argument. -pub fn mk_rustc_arg(stub_mapping: &BTreeMap) -> String { - // Serialize each `DefPathHash` as a pair of `u64`s, and the whole mapping - // as an association list. - let mut pairs = Vec::new(); - for (k, v) in stub_mapping { - let (k_a, k_b) = k.0.split(); - let kparts = (k_a.as_u64(), k_b.as_u64()); - let (v_a, v_b) = v.0.split(); - let vparts = (v_a.as_u64(), v_b.as_u64()); - pairs.push((kparts, vparts)); - } - // Store our serialized mapping as a fake LLVM argument (safe to do since - // LLVM will never see them). - format!("-Cllvm-args='{RUSTC_ARG_PREFIX}{}'", serde_json::to_string(&pairs).unwrap()) -} - -/// Deserializes the stub mapping from the rustc argument value. -fn deserialize_mapping(tcx: TyCtxt, val: &str) -> HashMap { - type Item = (u64, u64); - let item_to_def_id = |item: Item| -> DefId { - let hash = DefPathHash(Fingerprint::new(item.0, item.1)); - tcx.def_path_hash_to_def_id(hash, &()) - }; - let pairs: Vec<(Item, Item)> = serde_json::from_str(val).unwrap(); - let mut m = HashMap::default(); - for (k, v) in pairs { - let kid = item_to_def_id(k); - let vid = item_to_def_id(v); - m.insert(kid, vid); - } - m -} - -/// Retrieves the stub mapping from the compiler configuration. -fn get_stub_mapping(tcx: TyCtxt) -> Option> { - // Use a static so that we compile the regex only once. - lazy_static! { - static ref RE: Regex = Regex::new(&format!("'{RUSTC_ARG_PREFIX}(.*)'")).unwrap(); - } - for arg in &tcx.sess.opts.cg.llvm_args { - if let Some(captures) = RE.captures(arg) { - return Some(deserialize_mapping(tcx, captures.get(1).unwrap().as_str())); - } - } - None -} diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 9402835c2ff2..bd6c9be6581a 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -6,11 +6,7 @@ use crate::kani_middle::find_fn_def; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; -use stable_mir::mir::{ - BasicBlock, BasicBlockIdx, BinOp, Body, CastKind, Constant, Local, LocalDecl, Mutability, - Operand, Place, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, - VarDebugInfo, -}; +use stable_mir::mir::*; use stable_mir::ty::{Const, GenericArgs, Span, Ty, UintTy}; use std::fmt::Debug; use std::mem; @@ -288,3 +284,138 @@ impl SourceInstruction { fn find_instance(tcx: TyCtxt, diagnostic: &str) -> Option { Instance::resolve(find_fn_def(tcx, diagnostic)?, &GenericArgs(vec![])).ok() } + +/// Basic mutable body visitor. +/// +/// We removed many methods for simplicity. +/// +/// TODO: Contribute this to stable_mir. +/// +/// +/// This code was based on the existing MirVisitor: +/// +pub trait MutMirVisitor { + fn visit_body(&mut self, body: &mut MutableBody) { + self.super_body(body) + } + + fn visit_basic_block(&mut self, bb: &mut BasicBlock) { + self.super_basic_block(bb) + } + + fn visit_statement(&mut self, stmt: &mut Statement) { + self.super_statement(stmt) + } + + fn visit_terminator(&mut self, term: &mut Terminator) { + self.super_terminator(term) + } + + fn visit_rvalue(&mut self, rvalue: &mut Rvalue) { + self.super_rvalue(rvalue) + } + + fn visit_operand(&mut self, _operand: &mut Operand) {} + + fn super_body(&mut self, body: &mut MutableBody) { + for bb in body.blocks.iter_mut() { + self.visit_basic_block(bb); + } + } + + fn super_basic_block(&mut self, bb: &mut BasicBlock) { + for stmt in &mut bb.statements { + self.visit_statement(stmt); + } + self.visit_terminator(&mut bb.terminator); + } + + fn super_statement(&mut self, stmt: &mut Statement) { + match &mut stmt.kind { + StatementKind::Assign(_, rvalue) => { + self.visit_rvalue(rvalue); + } + StatementKind::Intrinsic(intrisic) => match intrisic { + NonDivergingIntrinsic::Assume(operand) => { + self.visit_operand(operand); + } + NonDivergingIntrinsic::CopyNonOverlapping(CopyNonOverlapping { + src, + dst, + count, + }) => { + self.visit_operand(src); + self.visit_operand(dst); + self.visit_operand(count); + } + }, + StatementKind::FakeRead(_, _) + | StatementKind::SetDiscriminant { .. } + | StatementKind::Deinit(_) + | StatementKind::StorageLive(_) + | StatementKind::StorageDead(_) + | StatementKind::Retag(_, _) + | StatementKind::PlaceMention(_) + | StatementKind::AscribeUserType { .. } + | StatementKind::Coverage(_) + | StatementKind::ConstEvalCounter + | StatementKind::Nop => {} + } + } + + fn super_terminator(&mut self, term: &mut Terminator) { + let Terminator { kind, .. } = term; + match kind { + TerminatorKind::Assert { cond, .. } => { + self.visit_operand(cond); + } + TerminatorKind::Call { func, args, .. } => { + self.visit_operand(func); + for arg in args { + self.visit_operand(arg); + } + } + TerminatorKind::SwitchInt { discr, .. } => { + self.visit_operand(discr); + } + TerminatorKind::InlineAsm { .. } => { + // we don't support inline assembly. + } + TerminatorKind::Return + | TerminatorKind::Goto { .. } + | TerminatorKind::Resume + | TerminatorKind::Abort + | TerminatorKind::Drop { .. } + | TerminatorKind::Unreachable => {} + } + } + + fn super_rvalue(&mut self, rvalue: &mut Rvalue) { + match rvalue { + Rvalue::Aggregate(_, operands) => { + for op in operands { + self.visit_operand(op); + } + } + Rvalue::BinaryOp(_, lhs, rhs) | Rvalue::CheckedBinaryOp(_, lhs, rhs) => { + self.visit_operand(lhs); + self.visit_operand(rhs); + } + Rvalue::Cast(_, op, _) => { + self.visit_operand(op); + } + Rvalue::Repeat(op, _) => { + self.visit_operand(op); + } + Rvalue::ShallowInitBox(op, _) => self.visit_operand(op), + Rvalue::UnaryOp(_, op) | Rvalue::Use(op) => { + self.visit_operand(op); + } + Rvalue::AddressOf(..) => {} + Rvalue::CopyForDeref(_) | Rvalue::Discriminant(_) | Rvalue::Len(_) => {} + Rvalue::Ref(..) => {} + Rvalue::ThreadLocalRef(_) => {} + Rvalue::NullaryOp(..) => {} + } + } +} diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 2c05c07be7f2..893b2244f2ca 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -730,7 +730,8 @@ fn expect_instance(locals: &[LocalDecl], func: &Operand) -> Instance { let ty = func.ty(locals).unwrap(); match ty.kind() { TyKind::RigidTy(RigidTy::FnDef(def, args)) => Instance::resolve(def, &args).unwrap(), - _ => unreachable!(), + TyKind::RigidTy(RigidTy::FnPtr(sig)) => todo!("Add support to FnPtr: {sig:?}"), + _ => unreachable!("Found: {func:?}"), } } diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs new file mode 100644 index 000000000000..c99874cc42a8 --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -0,0 +1,168 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains code related to the MIR-to-MIR pass to enable contracts. +use crate::kani_middle::attributes::KaniAttributes; +use crate::kani_middle::codegen_units::CodegenUnit; +use crate::kani_middle::transform::body::MutableBody; +use crate::kani_middle::transform::{TransformPass, TransformationType}; +use crate::kani_queries::QueryDb; +use cbmc::{InternString, InternedString}; +use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{Body, Constant, Operand, TerminatorKind}; +use stable_mir::ty::{Const as MirConst, FnDef, RigidTy, TyKind}; +use stable_mir::{CrateDef, DefId}; +use std::collections::HashSet; +use std::fmt::Debug; +use tracing::{debug, trace}; + +/// Check if we can replace calls to any_modifies. +/// +/// This pass will replace the entire body, and it should only be applied to stubs +/// that have a body. +#[derive(Debug)] +pub struct AnyModifiesPass { + kani_any: Option, + kani_any_modifies: Option, + stubbed: HashSet, + target_fn: Option, +} + +impl TransformPass for AnyModifiesPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Stubbing + } + + fn is_enabled(&self, query_db: &QueryDb) -> bool + where + Self: Sized, + { + // TODO: Check if this is the harness has proof_for_contract + query_db.args().unstable_features.contains(&"function-contracts".to_string()) + && self.kani_any.is_some() + } + + /// Transform the function body by replacing it with the stub body. + fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + trace!(function=?instance.name(), "AnyModifiesPass::transform"); + + if instance.def.def_id() == self.kani_any.unwrap().def_id() { + // Ensure kani::any is valid. + self.any_body(tcx, body) + } else if self.should_apply(tcx, instance) { + // Replace any modifies occurrences. + self.replace_any_modifies(body) + } else { + (false, body) + } + } +} + +impl AnyModifiesPass { + /// Build the pass with non-extern function stubs. + pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> AnyModifiesPass { + let item_fn_def = |item| { + let TyKind::RigidTy(RigidTy::FnDef(def, _)) = + rustc_internal::stable(tcx.type_of(item)).value.kind() + else { + unreachable!("Expected function, but found `{:?}`", tcx.def_path_str(item)) + }; + def + }; + let kani_any = + tcx.get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAny")).map(item_fn_def); + let kani_any_modifies = tcx + .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies")) + .map(item_fn_def); + let (target_fn, stubbed) = if let Some(harness) = unit.harnesses.first() { + let attributes = KaniAttributes::for_instance(tcx, *harness); + let target_fn = + attributes.proof_for_contract().map(|symbol| symbol.unwrap().as_str().intern()); + (target_fn, unit.stubs.keys().map(|from| from.def_id()).collect::>()) + } else { + (None, HashSet::new()) + }; + AnyModifiesPass { kani_any, kani_any_modifies, target_fn, stubbed } + } + + /// If we apply `transform_any_modifies` in all contract-generated items, + /// we will end up instantiating `kani::any_modifies` for the replace function + /// every time, even if we are only checking the contract, because the function + /// is always included during contract instrumentation. Thus, we must only apply + /// the transformation if we are using a verified stub or in the presence of recursion. + fn should_apply(&self, tcx: TyCtxt, instance: Instance) -> bool { + let item_attributes = + KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, instance.def.def_id())); + self.stubbed.contains(&instance.def.def_id()) || item_attributes.has_recursion() + } + + /// Replace calls to `any_modifies` by calls to `any`. + fn replace_any_modifies(&self, mut body: Body) -> (bool, Body) { + let mut changed = false; + let locals = body.locals().to_vec(); + for bb in body.blocks.iter_mut() { + let TerminatorKind::Call { func, .. } = &mut bb.terminator.kind else { continue }; + if let TyKind::RigidTy(RigidTy::FnDef(def, instance_args)) = + func.ty(&locals).unwrap().kind() + && Some(def) == self.kani_any_modifies + { + let instance = Instance::resolve(self.kani_any.unwrap(), &instance_args).unwrap(); + let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); + let span = bb.terminator.span; + let new_func = Constant { span, user_ty: None, literal }; + *func = Operand::Constant(new_func); + changed = true; + } + } + (changed, body) + } + + /// Check if T::Arbitrary requirement for `kani::any()` is met after replacement. + /// + /// If it T does not implement arbitrary, generate error and delete body to interrupt analysis. + fn any_body(&self, tcx: TyCtxt, mut body: Body) -> (bool, Body) { + let mut valid = true; + let locals = body.locals().to_vec(); + for bb in body.blocks.iter_mut() { + let TerminatorKind::Call { func, .. } = &mut bb.terminator.kind else { continue }; + if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = func.ty(&locals).unwrap().kind() { + match Instance::resolve(def, &args) { + Ok(_) => {} + Err(e) => { + valid = false; + debug!(?e, "AnyModifiesPass::any_body failed"); + let receiver_ty = args.0[0].expect_ty(); + let msg = if self.target_fn.is_some() { + format!( + "`{receiver_ty}` doesn't implement `kani::Arbitrary`.\ + Please, check `{}` contract.", + self.target_fn.unwrap(), + ) + } else { + format!("`{receiver_ty}` doesn't implement `kani::Arbitrary`.") + }; + tcx.dcx() + .struct_span_err(rustc_internal::internal(tcx, bb.terminator.span), msg) + .with_help( + "All objects in the modifies clause must implement the Arbitrary. \ + The return type must also implement the Arbitrary trait if you \ + are checking recursion or using verified stub.", + ) + .emit(); + } + } + } + } + if valid { + (true, body) + } else { + let mut new_body = MutableBody::from(body); + new_body.clear_body(); + (false, new_body.into()) + } + } +} diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index d4e06a785fb3..8d5c61f55c92 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -16,9 +16,12 @@ //! //! For all instrumentation passes, always use exhaustive matches to ensure soundness in case a new //! case is added. +use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::transform::body::CheckType; use crate::kani_middle::transform::check_values::ValidValuePass; +use crate::kani_middle::transform::contracts::AnyModifiesPass; use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; +use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; @@ -26,9 +29,11 @@ use stable_mir::mir::Body; use std::collections::HashMap; use std::fmt::Debug; -mod body; +pub(crate) mod body; mod check_values; +mod contracts; mod kani_intrinsics; +mod stubs; /// Object used to retrieve a transformed instance body. /// The transformations to be applied may be controlled by user options. @@ -37,9 +42,9 @@ mod kani_intrinsics; /// after. #[derive(Debug)] pub struct BodyTransformation { - /// The passes that may optimize the function body. - /// We store them separately from the instrumentation passes because we run the in specific order. - opt_passes: Vec>, + /// The passes that may change the function body according to harness configuration. + /// The stubbing passes should be applied before so user stubs take precedence. + stub_passes: Vec>, /// The passes that may add safety checks to the function body. inst_passes: Vec>, /// Cache transformation results. @@ -47,25 +52,22 @@ pub struct BodyTransformation { } impl BodyTransformation { - pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self { + pub fn new(queries: &QueryDb, tcx: TyCtxt, unit: &CodegenUnit) -> Self { let mut transformer = BodyTransformation { - opt_passes: vec![], + stub_passes: vec![], inst_passes: vec![], cache: Default::default(), }; let check_type = CheckType::new(tcx); + transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); + transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); + // This has to come after stubs since we want this to replace the stubbed body. + transformer.add_pass(queries, AnyModifiesPass::new(tcx, &unit)); transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() }); transformer.add_pass(queries, IntrinsicGeneratorPass { check_type }); transformer } - /// Allow the creation of a dummy transformer that doesn't apply any transformation due to - /// the stubbing validation hack (see `collect_and_partition_mono_items` override. - /// Once we move the stubbing logic to a [TransformPass], we should be able to remove this. - pub fn dummy() -> Self { - BodyTransformation { opt_passes: vec![], inst_passes: vec![], cache: Default::default() } - } - /// Retrieve the body of an instance. /// /// Note that this assumes that the instance does have a body since existing consumers already @@ -77,7 +79,7 @@ impl BodyTransformation { None => { let mut body = instance.body().unwrap(); let mut modified = false; - for pass in self.opt_passes.iter().chain(self.inst_passes.iter()) { + for pass in self.stub_passes.iter().chain(self.inst_passes.iter()) { let result = pass.transform(tcx, body, instance); modified |= result.0; body = result.1; @@ -98,9 +100,7 @@ impl BodyTransformation { if pass.is_enabled(&query_db) { match P::transformation_type() { TransformationType::Instrumentation => self.inst_passes.push(Box::new(pass)), - TransformationType::Optimization => { - unreachable!() - } + TransformationType::Stubbing => self.stub_passes.push(Box::new(pass)), } } } @@ -108,16 +108,15 @@ impl BodyTransformation { /// The type of transformation that a pass may perform. #[derive(Copy, Clone, Debug, Eq, PartialEq, Hash)] -enum TransformationType { +pub(crate) enum TransformationType { /// Should only add assertion checks to ensure the program is correct. Instrumentation, - /// May replace inefficient code with more performant but equivalent code. - #[allow(dead_code)] - Optimization, + /// Apply some sort of stubbing. + Stubbing, } /// A trait to represent transformation passes that can be used to modify the body of a function. -trait TransformPass: Debug { +pub(crate) trait TransformPass: Debug { /// The type of transformation that this pass implements. fn transformation_type() -> TransformationType where diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs new file mode 100644 index 000000000000..6d8849a9f1fe --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -0,0 +1,222 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains code related to the MIR-to-MIR pass that performs the +//! stubbing of functions and methods. +use crate::kani_middle::codegen_units::Stubs; +use crate::kani_middle::stubbing::validate_stub_const; +use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody}; +use crate::kani_middle::transform::{TransformPass, TransformationType}; +use crate::kani_queries::QueryDb; +use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::visit::{Location, MirVisitor}; +use stable_mir::mir::{Body, Constant, LocalDecl, Operand, Terminator, TerminatorKind}; +use stable_mir::ty::{Const as MirConst, FnDef, RigidTy, TyKind}; +use stable_mir::CrateDef; +use std::collections::HashMap; +use std::fmt::Debug; +use tracing::{debug, trace}; + +/// Replace the body of a function that is stubbed by the other. +/// +/// This pass will replace the entire body, and it should only be applied to stubs +/// that have a body. +#[derive(Debug)] +pub struct FnStubPass { + stubs: Stubs, +} + +impl TransformPass for FnStubPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Stubbing + } + + fn is_enabled(&self, query_db: &QueryDb) -> bool + where + Self: Sized, + { + query_db.args().stubbing_enabled && !self.stubs.is_empty() + } + + /// Transform the function body by replacing it with the stub body. + fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + trace!(function=?instance.name(), "transform"); + let ty = instance.ty(); + if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = ty.kind() { + if let Some(replace) = self.stubs.get(&fn_def) { + let new_instance = Instance::resolve(*replace, &args).unwrap(); + debug!(from=?instance.name(), to=?new_instance.name(), "FnStubPass::transform"); + if let Some(body) = FnStubValidator::validate(tcx, (fn_def, *replace), new_instance) + { + return (true, body); + } + } + } + (false, body) + } +} + +impl FnStubPass { + /// Build the pass with non-extern function stubs. + pub fn new(all_stubs: &Stubs) -> FnStubPass { + let stubs = all_stubs + .iter() + .filter_map(|(from, to)| (has_body(*from) && has_body(*to)).then_some((*from, *to))) + .collect::>(); + FnStubPass { stubs } + } +} + +/// Replace the body of a function that is stubbed by the other. +/// +/// This pass will replace the function call, since one of the functions do not have a body to +/// replace. +#[derive(Debug)] +pub struct ExternFnStubPass { + pub stubs: Stubs, +} + +impl TransformPass for ExternFnStubPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Stubbing + } + + fn is_enabled(&self, query_db: &QueryDb) -> bool + where + Self: Sized, + { + query_db.args().stubbing_enabled && !self.stubs.is_empty() + } + + /// Search for calls to extern functions that should be stubbed. + /// + /// We need to find function calls and function pointers. + /// We should replace this with a visitor once StableMIR includes a mutable one. + fn transform(&self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + trace!(function=?instance.name(), "transform"); + let mut new_body = MutableBody::from(body); + let changed = false; + let locals = new_body.locals().to_vec(); + let mut visitor = ExternFnStubVisitor { changed, locals, stubs: &self.stubs }; + visitor.visit_body(&mut new_body); + (visitor.changed, new_body.into()) + } +} + +impl ExternFnStubPass { + /// Build the pass with the extern function stubs. + /// + /// This will cover any case where the stub doesn't have a body. + pub fn new(all_stubs: &Stubs) -> ExternFnStubPass { + let stubs = all_stubs + .iter() + .filter_map(|(from, to)| (!has_body(*from) || !has_body(*to)).then_some((*from, *to))) + .collect::>(); + ExternFnStubPass { stubs } + } +} + +fn has_body(def: FnDef) -> bool { + def.body().is_some() +} + +/// Validate that the body of the stub is valid for the given instantiation +struct FnStubValidator<'a, 'tcx> { + stub: (FnDef, FnDef), + tcx: TyCtxt<'tcx>, + locals: &'a [LocalDecl], + is_valid: bool, +} + +impl<'a, 'tcx> FnStubValidator<'a, 'tcx> { + fn validate(tcx: TyCtxt, stub: (FnDef, FnDef), new_instance: Instance) -> Option { + if validate_stub_const(tcx, new_instance) { + let body = new_instance.body().unwrap(); + let mut validator = + FnStubValidator { stub, tcx, locals: body.locals(), is_valid: true }; + validator.visit_body(&body); + validator.is_valid.then_some(body) + } else { + None + } + } +} + +impl<'a, 'tcx> MirVisitor for FnStubValidator<'a, 'tcx> { + fn visit_operand(&mut self, op: &Operand, loc: Location) { + let op_ty = op.ty(self.locals).unwrap(); + if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = op_ty.kind() { + if Instance::resolve(def, &args).is_err() { + self.is_valid = false; + let callee = def.name(); + let receiver_ty = args.0[0].expect_ty(); + let sep = callee.rfind("::").unwrap(); + let trait_ = &callee[..sep]; + self.tcx.dcx().span_err( + rustc_internal::internal(self.tcx, loc.span()), + format!( + "`{}` doesn't implement \ + `{}`. The function `{}` \ + cannot be stubbed by `{}` due to \ + generic bounds not being met. Callee: {}", + receiver_ty, + trait_, + self.stub.0.name(), + self.stub.1.name(), + callee, + ), + ); + } + } + } +} + +struct ExternFnStubVisitor<'a> { + changed: bool, + locals: Vec, + stubs: &'a Stubs, +} + +impl<'a> MutMirVisitor for ExternFnStubVisitor<'a> { + fn visit_terminator(&mut self, term: &mut Terminator) { + // Replace direct calls + if let TerminatorKind::Call { func, .. } = &mut term.kind { + if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = + func.ty(&self.locals).unwrap().kind() + { + if let Some(new_def) = self.stubs.get(&def) { + let instance = Instance::resolve(*new_def, &args).unwrap(); + let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); + let span = term.span; + let new_func = Constant { span, user_ty: None, literal }; + *func = Operand::Constant(new_func); + self.changed = true; + } + } + } + self.super_terminator(term); + } + + fn visit_operand(&mut self, operand: &mut Operand) { + let func_ty = operand.ty(&self.locals).unwrap(); + if let TyKind::RigidTy(RigidTy::FnDef(orig_def, args)) = func_ty.kind() { + if let Some(new_def) = self.stubs.get(&orig_def) { + let Operand::Constant(Constant { span, .. }) = operand else { + unreachable!(); + }; + let instance = Instance::resolve_for_fn_ptr(*new_def, &args).unwrap(); + let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); + let new_func = Constant { span: *span, user_ty: None, literal }; + *operand = Operand::Constant(new_func); + self.changed = true; + } + } + } +} diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index d6b37a35f9cb..bb28237248d3 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -2,23 +2,16 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Define the communication between KaniCompiler and the codegen implementation. -use cbmc::{InternString, InternedString}; -use kani_metadata::AssignsContract; -use std::{ - collections::HashMap, - path::PathBuf, - sync::{Arc, Mutex}, -}; +use std::sync::{Arc, Mutex}; use crate::args::Arguments; /// This structure should only be used behind a synchronized reference or a snapshot. +/// +/// TODO: Merge this with arguments #[derive(Debug, Default, Clone)] pub struct QueryDb { args: Option, - /// Information about all target harnesses. - pub harnesses_info: HashMap, - modifies_contracts: HashMap, } impl QueryDb { @@ -26,16 +19,6 @@ impl QueryDb { Arc::new(Mutex::new(QueryDb::default())) } - /// Get the definition hash for all harnesses that are being compiled in this compilation stage. - 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: &String) -> Option<&PathBuf> { - self.harnesses_info.get(&harness.intern()) - } - pub fn set_args(&mut self, args: Arguments) { self.args = Some(args); } @@ -43,24 +26,4 @@ impl QueryDb { pub fn args(&self) -> &Arguments { self.args.as_ref().expect("Arguments have not been initialized") } - - /// Register that a CBMC-level `assigns` contract for a function that is - /// called from this harness. - pub fn register_assigns_contract( - &mut self, - harness_name: InternedString, - contract: AssignsContract, - ) { - let replaced = self.modifies_contracts.insert(harness_name, contract); - assert!( - replaced.is_none(), - "Invariant broken, tried adding second modifies contracts to: {harness_name}", - ) - } - - /// Lookup all CBMC-level `assigns` contract were registered with - /// [`Self::add_assigns_contract`]. - pub fn assigns_contracts(&self) -> impl Iterator { - self.modifies_contracts.iter() - } } diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 7c35cc469254..6a48bab08070 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -85,7 +85,7 @@ impl<'a> ContractConditionsHandler<'a> { let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); self.output.extend(quote!( - #[allow(dead_code, unused_variables)] + #[allow(dead_code, unused_variables, unused_mut)] #[kanitool::is_contract_generated(recursion_wrapper)] #wrapper_sig { static mut REENTRY: bool = false; diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index b0f5804824ad..b0d323b12ca3 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -50,7 +50,7 @@ impl<'a> ContractConditionsHandler<'a> { pub fn emit_common_header(&mut self) { if self.function_state.emit_tag_attr() { self.output.extend(quote!( - #[allow(dead_code, unused_variables)] + #[allow(dead_code, unused_variables, unused_mut)] )); } self.output.extend(self.annotated_fn.attrs.iter().flat_map(Attribute::to_token_stream)); diff --git a/tests/cargo-kani/stubbing-double-extern-path/harness/expected b/tests/cargo-kani/stubbing-double-extern-path/harness/expected index adbbf31d49bd..dbca159f92d5 100644 --- a/tests/cargo-kani/stubbing-double-extern-path/harness/expected +++ b/tests/cargo-kani/stubbing-double-extern-path/harness/expected @@ -1 +1,2 @@ -error[E0391]: cycle detected when optimizing MIR for `crate_b::assert_false` +error: Cannot stub `crate_b::assert_false`. Stub configuration for harness `check_inverted` has a cycle +error: Cannot stub `crate_b::assert_true`. Stub configuration for harness `check_inverted` has a cycle diff --git a/tests/expected/function-contract/gcd_success.rs b/tests/expected/function-contract/gcd_success.rs index 3b983a230b60..61d8fea8ec80 100644 --- a/tests/expected/function-contract/gcd_success.rs +++ b/tests/expected/function-contract/gcd_success.rs @@ -1,28 +1,22 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts +#![deny(warnings)] type T = u8; /// Euclid's algorithm for calculating the GCD of two numbers #[kani::requires(x != 0 && y != 0)] #[kani::ensures(|result : &T| *result != 0 && x % *result == 0 && y % *result == 0)] -fn gcd(x: T, y: T) -> T { - let mut max = x; - let mut min = y; - if min > max { - let val = max; - max = min; - min = val; - } - +fn gcd(mut x: T, mut y: T) -> T { + (x, y) = (if x > y { x } else { y }, if x > y { y } else { x }); loop { - let res = max % min; + let res = x % y; if res == 0 { - return min; + return y; } - max = min; - min = res; + x = y; + y = res; } } diff --git a/tests/expected/function-contract/modifies/check_invalid_modifies.expected b/tests/expected/function-contract/modifies/check_invalid_modifies.expected index fa1d96f1fe3f..660430705aa2 100644 --- a/tests/expected/function-contract/modifies/check_invalid_modifies.expected +++ b/tests/expected/function-contract/modifies/check_invalid_modifies.expected @@ -1,3 +1,7 @@ -error: `&str` doesn't implement `kani::Arbitrary`. Callee: `kani::Arbitrary::any` \ - Please, check whether the type of all objects in the modifies clause (including return types) implement `kani::Arbitrary`. \ - This is a strict condition to use function contracts as verified stubs. +error: `&str` doesn't implement `kani::Arbitrary`\ + -->\ +| +| T::any() +| ^^^^^^^^ +| += help: All objects in the modifies clause must implement the Arbitrary. The return type must also implement the Arbitrary trait if you are checking recursion or using verified stub. diff --git a/tests/expected/issue-2589/issue_2589.expected b/tests/expected/issue-2589/issue_2589.expected index 0352a8933b6d..a753bc7390a0 100644 --- a/tests/expected/issue-2589/issue_2589.expected +++ b/tests/expected/issue-2589/issue_2589.expected @@ -1 +1 @@ -error: Type `std::string::String` does not implement trait `Dummy`. This is likely because `original` is used as a stub but its generic bounds are not being met. +error: Type `std::string::String` does not implement trait `Dummy`. This is likely because `stub` is used as a stub but its generic bounds are not being met. diff --git a/tests/expected/stubbing-different-sets/stubbing.expected b/tests/expected/stubbing-different-sets/stubbing.expected new file mode 100644 index 000000000000..cf362d974f2e --- /dev/null +++ b/tests/expected/stubbing-different-sets/stubbing.expected @@ -0,0 +1,19 @@ +Checking harness check_indirect_all_identity... +VERIFICATION:- SUCCESSFUL + +Checking harness check_all_identity_2... +VERIFICATION:- SUCCESSFUL + +Checking harness check_all_identity... +VERIFICATION:- SUCCESSFUL + +Checking harness check_decrement_is_increment... +VERIFICATION:- SUCCESSFUL + +Checking harness check_decrement... +VERIFICATION:- SUCCESSFUL + +Checking harness check_identity... +VERIFICATION:- SUCCESSFUL + +Complete - 6 successfully verified harnesses, 0 failures, 6 total. diff --git a/tests/script-based-pre/stubbing_compiler_sessions/stubbing.rs b/tests/expected/stubbing-different-sets/stubbing.rs similarity index 88% rename from tests/script-based-pre/stubbing_compiler_sessions/stubbing.rs rename to tests/expected/stubbing-different-sets/stubbing.rs index cde1902c3558..90905baa5bb6 100644 --- a/tests/script-based-pre/stubbing_compiler_sessions/stubbing.rs +++ b/tests/expected/stubbing-different-sets/stubbing.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// -// Check that Kani handles different sets of stubbing correctly. -// I.e., not correctly replacing the stubs will cause a harness to fail. +// kani-flags: -Z stubbing +//! Check that Kani handles different sets of stubbing correctly. +//! I.e., not correctly replacing the stubs will cause a harness to fail. fn identity(i: i8) -> i8 { i diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index d90729de3f6d..59ef366af76e 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit d90729de3f6d1fdc76ddff734591cfc2d8e61e80 +Subproject commit 59ef366af76edfb4f89bd39137865db2a1ad041d diff --git a/tests/script-based-pre/stubbing_compiler_sessions/check_compiler_sessions.expected b/tests/script-based-pre/stubbing_compiler_sessions/check_compiler_sessions.expected deleted file mode 100644 index 9c6b0f53778f..000000000000 --- a/tests/script-based-pre/stubbing_compiler_sessions/check_compiler_sessions.expected +++ /dev/null @@ -1,3 +0,0 @@ -Complete - 6 successfully verified harnesses, 0 failures, 6 total. - -Rust compiler sessions: 4 diff --git a/tests/script-based-pre/stubbing_compiler_sessions/check_compiler_sessions.sh b/tests/script-based-pre/stubbing_compiler_sessions/check_compiler_sessions.sh deleted file mode 100755 index 9e4afff0b09c..000000000000 --- a/tests/script-based-pre/stubbing_compiler_sessions/check_compiler_sessions.sh +++ /dev/null @@ -1,27 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -# -# Checks that the Kani compiler can encode harnesses with the same set of stubs -# in one rustc session. - -set +e - -log_file=output.log - -kani stubbing.rs --enable-unstable --enable-stubbing --verbose >& ${log_file} - -echo "------- Raw output ---------" -cat $log_file -echo "----------------------------" - -# We print the reachability analysis results once for each session. -# This is the only reliable way to get the number of sessions from the compiler. -# The other option would be to use debug comments. -# Ideally, the compiler should only print one set of statistics at the end of its run. -# In that case, we should include number of sessions to those stats. -runs=$(grep -c "Reachability Analysis Result" ${log_file}) -echo "Rust compiler sessions: ${runs}" - -# Cleanup -rm ${log_file} diff --git a/tests/script-based-pre/stubbing_compiler_sessions/config.yml b/tests/script-based-pre/stubbing_compiler_sessions/config.yml deleted file mode 100644 index b1e83ed011c7..000000000000 --- a/tests/script-based-pre/stubbing_compiler_sessions/config.yml +++ /dev/null @@ -1,4 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -script: check_compiler_sessions.sh -expected: check_compiler_sessions.expected diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected index aa965f50cdf2..028e8949815f 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_std.expected +++ b/tests/script-based-pre/verify_std_cmd/verify_std.expected @@ -1,4 +1,7 @@ [TEST] Run kani verify-std +Checking harness kani::check_stub... +VERIFICATION:- SUCCESSFUL + Checking harness kani::check_success... VERIFICATION:- SUCCESSFUL @@ -8,4 +11,4 @@ VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) Checking harness num::verify::check_non_zero... VERIFICATION:- SUCCESSFUL -Complete - 3 successfully verified harnesses, 0 failures, 3 total. +Complete - 4 successfully verified harnesses, 0 failures, 4 total. diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index 9e18ed72ca2a..cc960ee2bfaf 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -54,6 +54,21 @@ pub mod kani { let new = mid as u8; assert!(orig == new, "Conversion round trip works"); } + + pub fn assert_true(cond: bool) { + assert!(cond) + } + + pub fn assert_false(cond: bool) { + assert!(!cond) + } + + #[kani_core::proof] + #[kani_core::stub(assert_true, assert_false)] + fn check_stub() { + // Check this is in fact asserting false. + assert_true(false) + } } ' @@ -85,7 +100,7 @@ cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs echo "[TEST] Run kani verify-std" export RUST_BACKTRACE=1 -kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" +kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z stubbing # Cleanup rm -r ${TMP_DIR} diff --git a/tests/ui/stubbing/stubbing-type-validation/expected b/tests/ui/stubbing/stubbing-type-validation/expected index 5c56ad015a79..177375b4f4ba 100644 --- a/tests/ui/stubbing/stubbing-type-validation/expected +++ b/tests/ui/stubbing/stubbing-type-validation/expected @@ -1,8 +1,11 @@ -error: arity mismatch: original function/method `f1` takes 1 argument(s), stub `f2` takes 0 -error: return type differs: stub `g2` has type `i32` where original function/method `g1` has type `bool` -error: type of parameter 1 differs: stub `g2` has type `u32` where original function/method `g1` has type `i32` -error: type of parameter 2 differs: stub `g2` has type `&mut bool` where original function/method `g1` has type `&bool` error: mismatch in the number of generic parameters: original function/method `h1` takes 1 generic parameters(s), stub `h2` takes 2 -error: return type differs: stub `i2` has type `Y` where original function/method `i1` has type `X` -error: type of parameter 1 differs: stub `j2` has type `&X` where original function/method `j1` has type `&Y` -error: aborting due to 7 previous errors \ No newline at end of file + +error: Cannot stub `g1` by `g2`.\ + - Expected return type `bool`, but found `i32`\ + - Expected type `i32` for parameter 2, but found `u32`\ + - Expected type `&bool` for parameter 3, but found `&mut bool`\ + +error: Cannot stub `i1` by `i2`.\ + - Expected return type `X`, but found `Y` + +error: arity mismatch: original function/method `f1` takes 1 argument(s), stub `f2` takes 0