From 7fd65462e35881ee5d86b241c4ddd2f18ce78d6c Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 10 Jun 2024 12:15:16 -0700 Subject: [PATCH] Refactor stubbing so Kani compiler only invoke rustc once per crate (#3245) Using stubs or function contracts as part of the `verify-std` sub-command does not work with multiple rustc executions as previous implementation. This happens because we now enable verifying dependencies, and cargo crashes due to a race condition. As soon as the first rustc invocation succeeds, cargo starts the compilation of the dependents crate. However, new executions can override files. Instead, we moved the stub logic to the new transformation framework, which is done on the top of the StableMIR body, and doesn't affect the Rust compiler session. We are now able to apply stub without restarting the compiler. This is a much better user experience as well, since multiple calls to the compiler can print the same warnings multiple times. Resolves #3072 Towards #3152 Co-authored-by: Felipe R. Monteiro --- .../compiler_interface.rs | 58 +- kani-compiler/src/kani_compiler.rs | 530 +----------------- kani-compiler/src/kani_middle/attributes.rs | 9 +- .../src/kani_middle/codegen_units.rs | 213 +++++++ kani-compiler/src/kani_middle/metadata.rs | 4 +- kani-compiler/src/kani_middle/mod.rs | 1 + kani-compiler/src/kani_middle/provide.rs | 48 +- kani-compiler/src/kani_middle/reachability.rs | 90 +-- .../src/kani_middle/stubbing/annotations.rs | 13 +- kani-compiler/src/kani_middle/stubbing/mod.rs | 101 +++- .../src/kani_middle/stubbing/transform.rs | 261 --------- .../src/kani_middle/transform/body.rs | 141 ++++- .../src/kani_middle/transform/check_values.rs | 3 +- .../src/kani_middle/transform/contracts.rs | 168 ++++++ .../src/kani_middle/transform/mod.rs | 43 +- .../src/kani_middle/transform/stubs.rs | 222 ++++++++ kani-compiler/src/kani_queries/mod.rs | 43 +- .../harness/expected | 3 +- .../modifies/check_invalid_modifies.expected | 10 +- tests/expected/issue-2589/issue_2589.expected | 2 +- .../stubbing-different-sets/stubbing.expected | 19 + .../stubbing-different-sets}/stubbing.rs | 6 +- .../check_compiler_sessions.expected | 3 - .../check_compiler_sessions.sh | 27 - .../stubbing_compiler_sessions/config.yml | 4 - .../verify_std_cmd/verify_std.expected | 5 +- .../verify_std_cmd/verify_std.sh | 17 +- .../stubbing-type-validation/expected | 17 +- 28 files changed, 987 insertions(+), 1074 deletions(-) create mode 100644 kani-compiler/src/kani_middle/codegen_units.rs delete mode 100644 kani-compiler/src/kani_middle/stubbing/transform.rs create mode 100644 kani-compiler/src/kani_middle/transform/contracts.rs create mode 100644 kani-compiler/src/kani_middle/transform/stubs.rs create mode 100644 tests/expected/stubbing-different-sets/stubbing.expected rename tests/{script-based-pre/stubbing_compiler_sessions => expected/stubbing-different-sets}/stubbing.rs (88%) delete mode 100644 tests/script-based-pre/stubbing_compiler_sessions/check_compiler_sessions.expected delete mode 100755 tests/script-based-pre/stubbing_compiler_sessions/check_compiler_sessions.sh delete mode 100644 tests/script-based-pre/stubbing_compiler_sessions/config.yml 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/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/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/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