From 194ff21d2e53832751d7fbb5f5d7bd016c6ba273 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 7 Jun 2024 19:47:22 -0700 Subject: [PATCH 01/11] Start refactoring stubbing 1. Change KaniCompiler to only run rustc once. 2. Move harness grouping to new codegen_units module. 3. Iterate over the codegen units. Verification of code without stubbing now works. Next step is to move the transformation to the new framework. --- .../compiler_interface.rs | 50 +- kani-compiler/src/kani_compiler.rs | 515 +----------------- .../src/kani_middle/codegen_units.rs | 164 ++++++ kani-compiler/src/kani_middle/mod.rs | 1 + .../src/kani_middle/stubbing/annotations.rs | 13 +- kani-compiler/src/kani_middle/stubbing/mod.rs | 8 +- .../src/kani_middle/stubbing/transform.rs | 90 +-- .../src/kani_middle/transform/mod.rs | 6 +- kani-compiler/src/kani_queries/mod.rs | 12 - 9 files changed, 268 insertions(+), 591 deletions(-) create mode 100644 kani-compiler/src/kani_middle/codegen_units.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 039c50eefe18..3b642f3262a7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -7,6 +7,7 @@ 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::codegen_units::CodegenUnits; use crate::kani_middle::metadata::{canonical_mangled_name, gen_test_metadata}; use crate::kani_middle::provide; use crate::kani_middle::reachability::{ @@ -231,43 +232,41 @@ 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 units = CodegenUnits::new(&queries, tcx); // 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 harnesses in units.iter() { + let mut transformer = BodyTransformation::new(&queries, tcx); + for harness in 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 { + self.queries.lock().unwrap().register_assigns_contract( + canonical_mangled_name(*harness).intern(), + assigns_contract, + ); + } } } + units.store_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 mut transformer = BodyTransformation::new(&queries, tcx); let mut descriptions = vec![]; let harnesses = filter_const_crate_items(tcx, &mut transformer, |_, item| { if is_test_harness_description(tcx, item.def) { @@ -310,6 +309,7 @@ impl CodegenBackend for GotocCodegenBackend { } ReachabilityType::None => {} ReachabilityType::PubFns => { + let mut transformer = BodyTransformation::new(&queries, tcx); 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..6fcd2a910080 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -25,17 +25,15 @@ 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}; @@ -69,537 +67,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 misusage 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/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs new file mode 100644 index 000000000000..4aef17668c99 --- /dev/null +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -0,0 +1,164 @@ +// 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. + +// TODO: Move this out of CBMC crate. +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::harness_stub_map; +use crate::kani_queries::QueryDb; +use cbmc::{InternString, InternedString}; +use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; +use rustc_hir::def_id::{DefId, DefPathHash}; +use rustc_middle::ty::TyCtxt; +use rustc_session::config::OutputType; +use stable_mir::mir::mono::Instance; +use std::collections::{BTreeMap, HashMap}; +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. +type Stubs = HashMap; + +#[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, +} + +/// We group the harnesses that have the same stubs. +pub struct CodegenUnits { + units: Vec>, + all_harnesses: HashMap, + crate_info: CrateInfo, +} + +impl CodegenUnits { + pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self { + let crate_info = CrateInfo { + name: stable_mir::local_crate().name.as_str().into(), + output_path: metadata_output_path(tcx), + }; + 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); + let stub_map = harness_stub_map(tcx, harness, &metadata); + (harness, HarnessInfo { metadata, stub_map }) + }) + .collect::>(); + + let (no_stubs, with_stubs): (Vec<_>, Vec<_>) = if queries.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. + let mut units = vec![no_stubs]; + units.extend(group_by_stubs(tcx, with_stubs, &all_harnesses)); + CodegenUnits { units, all_harnesses, crate_info } + } else { + // Leave other reachability type handling as is for now. + CodegenUnits { units: vec![], all_harnesses: HashMap::default(), crate_info } + } + } + + pub fn iter(&self) -> impl Iterator> { + self.units.iter() + } + + pub fn store_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.all_harnesses[&harness].metadata.goto_file.as_ref() + } + + /// Generate [KaniMetadata] for the target crate. + fn generate_metadata(&self) -> KaniMetadata { + let (proof_harnesses, test_harnesses) = self + .all_harnesses + .values() + .map(|info| &info.metadata) + .cloned() + .partition(|md| md.attributes.proof); + KaniMetadata { + crate_name: self.crate_info.name.clone(), + proof_harnesses, + unsupported_features: vec![], + test_harnesses, + } + } +} + +/// Group the harnesses by their stubs. +fn group_by_stubs( + tcx: TyCtxt, + harnesses: Vec, + all_harnesses: &HashMap, +) -> Vec> { + let mut per_stubs: HashMap, Vec> = + HashMap::default(); + for harness in harnesses { + let stub_map = all_harnesses[&harness] + .stub_map + .iter() + .map(|(k, v)| (tcx.def_path_hash(*k), tcx.def_path_hash(*v))) + .collect::>(); + per_stubs.entry(stub_map).or_default().push(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(); + } +} 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/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..0f5bf3c9dab4 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -6,12 +6,12 @@ mod annotations; mod transform; 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; @@ -27,10 +27,10 @@ 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); } diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs index f101a6009907..690bc45e79c2 100644 --- a/kani-compiler/src/kani_middle/stubbing/transform.rs +++ b/kani-compiler/src/kani_middle/stubbing/transform.rs @@ -10,8 +10,7 @@ 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_hir::def_id::DefId; use rustc_index::IndexVec; use rustc_middle::mir::{ visit::MutVisitor, Body, Const, ConstValue, Local, LocalDecl, Location, Operand, @@ -209,53 +208,56 @@ fn check_compatibility<'a, 'tcx>( 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()) +/// Retrieves the stub mapping from the compiler configuration. +fn get_stub_mapping(_tcx: TyCtxt) -> Option> { + None } -/// 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, &()) +#[cfg(new_stub)] +mod new_stub { + use crate::kani_middle::attributes::matches_diagnostic; + use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruction}; + use crate::kani_middle::transform::{TransformPass, TransformationType}; + use crate::kani_queries::QueryDb; + use rustc_middle::ty::TyCtxt; + use stable_mir::mir::mono::Instance; + use stable_mir::mir::{ + BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL, }; - 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 -} + use stable_mir::target::MachineInfo; + use stable_mir::ty::{Const, RigidTy, TyKind}; + use std::fmt::Debug; + use strum_macros::AsRefStr; + use tracing::trace; -/// 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(); + /// Generate the body for a few Kani intrinsics. + #[derive(Debug)] + pub struct FnStubPass { + pub check_type: CheckType, } - 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())); + + impl TransformPass for FnStubPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Instrumentation + } + + fn is_enabled(&self, _query_db: &QueryDb) -> bool + where + Self: Sized, + { + true + } + + /// Transform the function body by inserting checks one-by-one. + /// For every unsafe dereference or a transmute operation, we check all values are valid. + fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + trace!(function=?instance.name(), "transform"); + body } } - None + + impl FnStubPass {} } diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index d4e06a785fb3..23b3a52def77 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -26,7 +26,7 @@ use stable_mir::mir::Body; use std::collections::HashMap; use std::fmt::Debug; -mod body; +pub(crate) mod body; mod check_values; mod kani_intrinsics; @@ -108,7 +108,7 @@ 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. @@ -117,7 +117,7 @@ enum TransformationType { } /// 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_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index d6b37a35f9cb..7e5d90428ee8 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -16,8 +16,6 @@ use crate::args::Arguments; #[derive(Debug, Default, Clone)] pub struct QueryDb { args: Option, - /// Information about all target harnesses. - pub harnesses_info: HashMap, modifies_contracts: HashMap, } @@ -26,16 +24,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); } From 7695405a7e499716d2b1fcc195611f7c0af57eff Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 7 Jun 2024 23:49:34 -0700 Subject: [PATCH 02/11] Initial stub implementation Still missing some validation and foreign function support --- .../compiler_interface.rs | 16 ++-- .../src/kani_middle/codegen_units.rs | 86 ++++++++++--------- kani-compiler/src/kani_middle/provide.rs | 26 ------ kani-compiler/src/kani_middle/reachability.rs | 22 ++--- .../src/kani_middle/stubbing/transform.rs | 49 ----------- .../src/kani_middle/transform/mod.rs | 29 ++++--- .../src/kani_middle/transform/stubs.rs | 61 +++++++++++++ kani-compiler/src/kani_queries/mod.rs | 3 +- 8 files changed, 142 insertions(+), 150 deletions(-) create mode 100644 kani-compiler/src/kani_middle/transform/stubs.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 3b642f3262a7..ed6e2feeb89e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -7,7 +7,7 @@ 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::codegen_units::CodegenUnits; +use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits}; use crate::kani_middle::metadata::{canonical_mangled_name, gen_test_metadata}; use crate::kani_middle::provide; use crate::kani_middle::reachability::{ @@ -237,9 +237,11 @@ impl CodegenBackend for GotocCodegenBackend { ReachabilityType::Harnesses => { let units = CodegenUnits::new(&queries, tcx); // Cross-crate collecting of all items that are reachable from the crate harnesses. - for harnesses in units.iter() { - let mut transformer = BodyTransformation::new(&queries, tcx); - for harness in harnesses { + 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(); @@ -266,7 +268,8 @@ impl CodegenBackend for GotocCodegenBackend { // We're iterating over crate items here, so what we have to codegen is the "test description" containing the // test closure that we want to execute // TODO: Refactor this code so we can guarantee that the pair (test_fn, test_desc) actually match. - let mut transformer = BodyTransformation::new(&queries, tcx); + 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) { @@ -309,7 +312,8 @@ impl CodegenBackend for GotocCodegenBackend { } ReachabilityType::None => {} ReachabilityType::PubFns => { - let mut transformer = BodyTransformation::new(&queries, tcx); + 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_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 4aef17668c99..2061c2004954 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -19,7 +19,9 @@ use kani_metadata::{ArtifactType, 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 std::collections::{BTreeMap, HashMap}; use std::fs::File; use std::io::BufWriter; @@ -30,13 +32,7 @@ use tracing::debug; type Harness = Instance; /// A set of stubs. -type Stubs = HashMap; - -#[derive(Clone, Debug)] -struct HarnessInfo { - pub metadata: HarnessMetadata, - pub stub_map: Stubs, -} +pub type Stubs = HashMap; /// Store some relevant information about the crate compilation. #[derive(Clone, Debug)] @@ -49,11 +45,17 @@ struct CrateInfo { /// We group the harnesses that have the same stubs. pub struct CodegenUnits { - units: Vec>, - all_harnesses: HashMap, + 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 { @@ -68,33 +70,20 @@ impl CodegenUnits { .into_iter() .map(|harness| { let metadata = gen_proof_metadata(tcx, harness, &base_filename); - let stub_map = harness_stub_map(tcx, harness, &metadata); - (harness, HarnessInfo { metadata, stub_map }) + (harness, metadata) }) .collect::>(); - let (no_stubs, with_stubs): (Vec<_>, Vec<_>) = if queries.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. - let mut units = vec![no_stubs]; - units.extend(group_by_stubs(tcx, with_stubs, &all_harnesses)); - CodegenUnits { units, all_harnesses, crate_info } + let units = group_by_stubs(tcx, &all_harnesses); + CodegenUnits { units, harness_info: all_harnesses, crate_info } } else { // Leave other reachability type handling as is for now. - CodegenUnits { units: vec![], all_harnesses: HashMap::default(), crate_info } + CodegenUnits { units: vec![], harness_info: HashMap::default(), crate_info } } } - pub fn iter(&self) -> impl Iterator> { + pub fn iter(&self) -> impl Iterator { self.units.iter() } @@ -105,17 +94,13 @@ impl CodegenUnits { } pub fn harness_model_path(&self, harness: Harness) -> Option<&PathBuf> { - self.all_harnesses[&harness].metadata.goto_file.as_ref() + 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 - .all_harnesses - .values() - .map(|info| &info.metadata) - .cloned() - .partition(|md| md.attributes.proof); + 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, @@ -125,21 +110,38 @@ impl CodegenUnits { } } +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, but found: {ty}") + } +} + /// Group the harnesses by their stubs. fn group_by_stubs( tcx: TyCtxt, - harnesses: Vec, - all_harnesses: &HashMap, -) -> Vec> { - let mut per_stubs: HashMap, Vec> = + all_harnesses: &HashMap, +) -> Vec { + let mut per_stubs: HashMap, CodegenUnit> = HashMap::default(); - for harness in harnesses { - let stub_map = all_harnesses[&harness] - .stub_map + 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::>(); - per_stubs.entry(stub_map).or_default().push(harness) + 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::>(); + per_stubs.insert(stub_map, CodegenUnit { stubs, harnesses: vec![*harness] }); + } } per_stubs.into_values().collect() } diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index d9197493f4db..c22da858952c 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -25,10 +25,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; - } } } @@ -78,25 +74,3 @@ fn run_kani_mir_passes<'tcx>( 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..1d5920715dae 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -185,19 +185,15 @@ 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, + instance: &instance, + }; + collector.visit_body(&body); + collector.collected.into_iter().collect() } /// Visit a static object and collect drop / initialization functions. diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs index 690bc45e79c2..687d7c27661f 100644 --- a/kani-compiler/src/kani_middle/stubbing/transform.rs +++ b/kani-compiler/src/kani_middle/stubbing/transform.rs @@ -212,52 +212,3 @@ fn check_compatibility<'a, 'tcx>( fn get_stub_mapping(_tcx: TyCtxt) -> Option> { None } - -#[cfg(new_stub)] -mod new_stub { - use crate::kani_middle::attributes::matches_diagnostic; - use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruction}; - use crate::kani_middle::transform::{TransformPass, TransformationType}; - use crate::kani_queries::QueryDb; - use rustc_middle::ty::TyCtxt; - use stable_mir::mir::mono::Instance; - use stable_mir::mir::{ - BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL, - }; - use stable_mir::target::MachineInfo; - use stable_mir::ty::{Const, RigidTy, TyKind}; - use std::fmt::Debug; - use strum_macros::AsRefStr; - use tracing::trace; - - /// Generate the body for a few Kani intrinsics. - #[derive(Debug)] - pub struct FnStubPass { - pub check_type: CheckType, - } - - impl TransformPass for FnStubPass { - fn transformation_type() -> TransformationType - where - Self: Sized, - { - TransformationType::Instrumentation - } - - fn is_enabled(&self, _query_db: &QueryDb) -> bool - where - Self: Sized, - { - true - } - - /// Transform the function body by inserting checks one-by-one. - /// For every unsafe dereference or a transmute operation, we check all values are valid. - fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { - trace!(function=?instance.name(), "transform"); - body - } - } - - impl FnStubPass {} -} diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 23b3a52def77..d1ec4a8014c4 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -16,9 +16,11 @@ //! //! 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, CodegenUnits}; use crate::kani_middle::transform::body::CheckType; use crate::kani_middle::transform::check_values::ValidValuePass; use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; +use crate::kani_middle::transform::stubs::FnStubPass; use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; @@ -29,6 +31,7 @@ use std::fmt::Debug; pub(crate) mod body; mod check_values; 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 +40,9 @@ mod kani_intrinsics; /// after. #[derive(Debug)] pub struct BodyTransformation { - /// The passes that may optimize the function body. + /// The passes that may change the function body according to harness configuration. /// We store them separately from the instrumentation passes because we run the in specific order. - opt_passes: Vec>, + user_mod_passes: Vec>, /// The passes that may add safety checks to the function body. inst_passes: Vec>, /// Cache transformation results. @@ -47,13 +50,14 @@ 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![], + user_mod_passes: vec![], inst_passes: vec![], cache: Default::default(), }; let check_type = CheckType::new(tcx); + transformer.add_pass(queries, FnStubPass { stubs: unit.stubs.clone() }); transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() }); transformer.add_pass(queries, IntrinsicGeneratorPass { check_type }); transformer @@ -63,7 +67,11 @@ impl BodyTransformation { /// 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() } + BodyTransformation { + user_mod_passes: vec![], + inst_passes: vec![], + cache: Default::default(), + } } /// Retrieve the body of an instance. @@ -77,7 +85,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.user_mod_passes.iter().chain(self.inst_passes.iter()) { let result = pass.transform(tcx, body, instance); modified |= result.0; body = result.1; @@ -98,9 +106,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::UserTransformation => self.user_mod_passes.push(Box::new(pass)), } } } @@ -111,9 +117,8 @@ impl BodyTransformation { 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 user requested transformation. + UserTransformation, } /// A trait to represent transformation passes that can be used to modify the body of a function. 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..0c0fb3020303 --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -0,0 +1,61 @@ +// 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::attributes::matches_diagnostic; +use crate::kani_middle::codegen_units::Stubs; +use crate::kani_middle::stubbing::validate_instance; +use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruction}; +use crate::kani_middle::transform::{TransformPass, TransformationType}; +use crate::kani_queries::QueryDb; +use rustc_middle::ty::TyCtxt; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{ + BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL, +}; +use stable_mir::target::MachineInfo; +use stable_mir::ty::{Const, RigidTy, TyKind}; +use std::fmt::Debug; +use strum_macros::AsRefStr; +use tracing::trace; + +/// Replace the body of a function that is stubbed by the other. +#[derive(Debug)] +pub struct FnStubPass { + pub stubs: Stubs, +} + +impl TransformPass for FnStubPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::UserTransformation + } + + fn is_enabled(&self, _query_db: &QueryDb) -> bool + where + Self: Sized, + { + true + } + + /// 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(); + let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = ty.kind() else { + unreachable!("Expected stub function, but found: {ty}") + }; + + if let Some(replace) = self.stubs.get(&fn_def) { + let new_instance = Instance::resolve(*replace, &args).unwrap(); + if validate_instance(tcx, new_instance) { + return (true, new_instance.body().unwrap()); + } + } + (false, body) + } +} + +impl FnStubPass {} diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index 7e5d90428ee8..1b1f6311aa11 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -2,11 +2,10 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Define the communication between KaniCompiler and the codegen implementation. -use cbmc::{InternString, InternedString}; +use cbmc::InternedString; use kani_metadata::AssignsContract; use std::{ collections::HashMap, - path::PathBuf, sync::{Arc, Mutex}, }; From 3fb4f534383acbecbba059bceaa24172624b9fcb Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Sat, 8 Jun 2024 14:17:11 -0700 Subject: [PATCH 03/11] Add basic support for stubs --- kani-compiler/src/kani_middle/codegen_units.rs | 3 ++- kani-compiler/src/kani_middle/transform/stubs.rs | 14 ++++++-------- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 2061c2004954..878090ab77e6 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -76,6 +76,7 @@ impl CodegenUnits { // Even if no_stubs is empty we still need to store rustc metadata. let units = group_by_stubs(tcx, &all_harnesses); + debug!(?units, "CodegenUnits::new"); CodegenUnits { units, harness_info: all_harnesses, crate_info } } else { // Leave other reachability type handling as is for now. @@ -116,7 +117,7 @@ fn stub_def(tcx: TyCtxt, def_id: DefId) -> FnDef { if let TyKind::RigidTy(RigidTy::FnDef(def, _)) = ty.kind() { def } else { - unreachable!("Expected stub function, but found: {ty}") + unreachable!("Expected stub function for `{:?}`, but found: {ty}", tcx.def_path(def_id)) } } diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index 0c0fb3020303..3cd1216aae30 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -44,14 +44,12 @@ impl TransformPass for FnStubPass { fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { trace!(function=?instance.name(), "transform"); let ty = instance.ty(); - let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = ty.kind() else { - unreachable!("Expected stub function, but found: {ty}") - }; - - if let Some(replace) = self.stubs.get(&fn_def) { - let new_instance = Instance::resolve(*replace, &args).unwrap(); - if validate_instance(tcx, new_instance) { - return (true, new_instance.body().unwrap()); + 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(); + if validate_instance(tcx, new_instance) { + return (true, new_instance.body().unwrap()); + } } } (false, body) From 6d9556c28aa43be2f43ad661ac3e905d35c5dcb4 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Sat, 8 Jun 2024 21:16:23 -0700 Subject: [PATCH 04/11] Add ForeignFnStubPass and stub validation --- .../src/kani_middle/codegen_units.rs | 15 +- kani-compiler/src/kani_middle/provide.rs | 3 +- kani-compiler/src/kani_middle/reachability.rs | 2 +- kani-compiler/src/kani_middle/stubbing/mod.rs | 90 ++++++++++-- .../src/kani_middle/stubbing/transform.rs | 136 +----------------- .../src/kani_middle/transform/check_values.rs | 3 +- .../src/kani_middle/transform/mod.rs | 26 ++-- .../src/kani_middle/transform/stubs.rs | 105 ++++++++++++-- 8 files changed, 206 insertions(+), 174 deletions(-) diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 878090ab77e6..a38410194bdf 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -12,7 +12,7 @@ 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::harness_stub_map; +use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; use crate::kani_queries::QueryDb; use cbmc::{InternString, InternedString}; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; @@ -22,6 +22,7 @@ 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}; use std::fs::File; use std::io::BufWriter; @@ -76,6 +77,7 @@ impl CodegenUnits { // 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 { @@ -165,3 +167,14 @@ fn store_metadata(queries: &QueryDb, metadata: &KaniMetadata, filename: &Path) { serde_json::to_writer(writer, &metadata).unwrap(); } } + +fn validate_units(tcx: TyCtxt, units: &[CodegenUnit]) { + for unit in units { + for (from, to) in &unit.stubs { + 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(); +} diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index c22da858952c..1b176850c60a 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -57,8 +57,7 @@ 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 mut transformed_body = body.clone(); 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 diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 1d5920715dae..e2a5ef348d08 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -36,7 +36,7 @@ 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::stubbing::{get_stub, validate_stub}; use crate::kani_middle::transform::BodyTransformation; /// Collect all reachable items starting from the given starting points. diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 0f5bf3c9dab4..a96722467225 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -5,6 +5,7 @@ mod annotations; mod transform; +use itertools::Itertools; use rustc_span::DUMMY_SP; use std::collections::HashMap; use tracing::{debug, trace}; @@ -18,6 +19,7 @@ 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; @@ -37,6 +39,78 @@ pub fn harness_stub_map( 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> { + 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_ty = rustc_internal::stable(tcx.type_of(old_def_id)).value; + let new_ty = rustc_internal::stable(tcx.type_of(new_def_id)).value; + let old_sig = old_ty.kind().fn_sig().unwrap().skip_binder(); + let new_sig = new_ty.kind().fn_sig().unwrap().skip_binder(); + // Check whether the arities match. + if old_sig.inputs_and_output.len() != new_sig.inputs_and_output.len() { + let msg = format!( + "arity mismatch: original function/method `{}` takes {} argument(s), stub `{}` takes {}", + old_def.name(), + old_sig.inputs_and_output.len() - 1, + new_def.name(), + new_sig.inputs_and_output.len() - 1, + ); + return Err(msg); + } + // 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(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_sig.output(); + let new_ret_ty = new_sig.output(); + 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_ty, new_arg_ty)) in + old_sig.inputs().iter().zip(new_sig.inputs().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 +118,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(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 index 687d7c27661f..710418534ebc 100644 --- a/kani-compiler/src/kani_middle/stubbing/transform.rs +++ b/kani-compiler/src/kani_middle/stubbing/transform.rs @@ -17,6 +17,7 @@ use rustc_middle::mir::{ }; use rustc_middle::ty::{self, TyCtxt}; +use crate::kani_middle::stubbing::check_compatibility; use tracing::debug; /// Returns the `DefId` of the stub for the function/method identified by the @@ -31,35 +32,6 @@ pub fn get_stub_key(tcx: TyCtxt, def_id: DefId) -> Option { 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. @@ -102,112 +74,6 @@ impl<'tcx> MutVisitor<'tcx> for AnyModifiesTransformer<'tcx> { } } -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 -} - /// Retrieves the stub mapping from the compiler configuration. fn get_stub_mapping(_tcx: TyCtxt) -> Option> { None 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/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index d1ec4a8014c4..8b65b852b7fc 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -20,7 +20,7 @@ use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits}; use crate::kani_middle::transform::body::CheckType; use crate::kani_middle::transform::check_values::ValidValuePass; use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; -use crate::kani_middle::transform::stubs::FnStubPass; +use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; @@ -30,6 +30,7 @@ use std::fmt::Debug; pub(crate) mod body; mod check_values; +mod contracts; mod kani_intrinsics; mod stubs; @@ -41,8 +42,8 @@ mod stubs; #[derive(Debug)] pub struct BodyTransformation { /// The passes that may change the function body according to harness configuration. - /// We store them separately from the instrumentation passes because we run the in specific order. - user_mod_passes: Vec>, + /// 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. @@ -52,12 +53,13 @@ pub struct BodyTransformation { impl BodyTransformation { pub fn new(queries: &QueryDb, tcx: TyCtxt, unit: &CodegenUnit) -> Self { let mut transformer = BodyTransformation { - user_mod_passes: vec![], + stub_passes: vec![], inst_passes: vec![], cache: Default::default(), }; let check_type = CheckType::new(tcx); - transformer.add_pass(queries, FnStubPass { stubs: unit.stubs.clone() }); + transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); + transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() }); transformer.add_pass(queries, IntrinsicGeneratorPass { check_type }); transformer @@ -67,11 +69,7 @@ impl BodyTransformation { /// 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 { - user_mod_passes: vec![], - inst_passes: vec![], - cache: Default::default(), - } + BodyTransformation { stub_passes: vec![], inst_passes: vec![], cache: Default::default() } } /// Retrieve the body of an instance. @@ -85,7 +83,7 @@ impl BodyTransformation { None => { let mut body = instance.body().unwrap(); let mut modified = false; - for pass in self.user_mod_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; @@ -106,7 +104,7 @@ impl BodyTransformation { if pass.is_enabled(&query_db) { match P::transformation_type() { TransformationType::Instrumentation => self.inst_passes.push(Box::new(pass)), - TransformationType::UserTransformation => self.user_mod_passes.push(Box::new(pass)), + TransformationType::Stubbing => self.stub_passes.push(Box::new(pass)), } } } @@ -117,8 +115,8 @@ impl BodyTransformation { pub(crate) enum TransformationType { /// Should only add assertion checks to ensure the program is correct. Instrumentation, - /// Apply some user requested transformation. - UserTransformation, + /// Apply some sort of stubbing. + Stubbing, } /// A trait to represent transformation passes that can be used to modify the body of a function. diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index 3cd1216aae30..c6c72f6d3bc6 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -4,25 +4,32 @@ //! stubbing of functions and methods. use crate::kani_middle::attributes::matches_diagnostic; use crate::kani_middle::codegen_units::Stubs; -use crate::kani_middle::stubbing::validate_instance; +use crate::kani_middle::stubbing::validate_stub; use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruction}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; +use itertools::Itertools; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ - BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL, + BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, TerminatorKind, + RETURN_LOCAL, }; use stable_mir::target::MachineInfo; -use stable_mir::ty::{Const, RigidTy, TyKind}; +use stable_mir::ty::{Abi, Const as MirConst, FnDef, RigidTy, TyKind}; +use stable_mir::CrateDef; +use std::collections::HashMap; use std::fmt::Debug; use strum_macros::AsRefStr; -use tracing::trace; +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 { - pub stubs: Stubs, + stubs: Stubs, } impl TransformPass for FnStubPass { @@ -30,14 +37,14 @@ impl TransformPass for FnStubPass { where Self: Sized, { - TransformationType::UserTransformation + TransformationType::Stubbing } - fn is_enabled(&self, _query_db: &QueryDb) -> bool + fn is_enabled(&self, query_db: &QueryDb) -> bool where Self: Sized, { - true + query_db.args().stubbing_enabled && !self.stubs.is_empty() } /// Transform the function body by replacing it with the stub body. @@ -47,7 +54,8 @@ impl TransformPass for FnStubPass { 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(); - if validate_instance(tcx, new_instance) { + if validate_stub(tcx, new_instance) { + debug!(from=?instance.name(), to=?new_instance.name(), "FnStubPass::transform"); return (true, new_instance.body().unwrap()); } } @@ -56,4 +64,81 @@ impl TransformPass for FnStubPass { } } -impl FnStubPass {} +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. + fn transform(&self, tcx: TyCtxt, mut body: Body, instance: Instance) -> (bool, Body) { + trace!(function=?instance.name(), "transform"); + 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, args)) = func.ty(&locals).unwrap().kind() { + if let Some(replace) = self.stubs.get(&def) { + debug!(func=?instance.name(), orig=?def.name(), replace=?replace.name(), + "ExternFnStubPass::transform"); + tracing::error!(func=?instance.name(), orig=?def.name(), replace=?replace + .name(), + "ExternFnStubPass::transform"); + let instance = Instance::resolve(*replace, &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) + } +} + +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() +} From 58943f9ee61deef31286d7330eb50241d7b7ddb8 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Sun, 9 Jun 2024 01:08:07 -0700 Subject: [PATCH 05/11] Get contracts to work now Need to adjust tests --- .../compiler_interface.rs | 13 +- kani-compiler/src/kani_middle/attributes.rs | 5 + .../src/kani_middle/codegen_units.rs | 12 +- kani-compiler/src/kani_middle/metadata.rs | 4 +- kani-compiler/src/kani_middle/provide.rs | 11 -- kani-compiler/src/kani_middle/reachability.rs | 63 +------ kani-compiler/src/kani_middle/stubbing/mod.rs | 35 ++-- .../src/kani_middle/stubbing/transform.rs | 80 -------- .../src/kani_middle/transform/contracts.rs | 178 ++++++++++++++++++ .../src/kani_middle/transform/mod.rs | 3 + .../src/kani_middle/transform/stubs.rs | 3 - kani-compiler/src/kani_queries/mod.rs | 6 - .../modifies/check_invalid_modifies.expected | 10 +- 13 files changed, 231 insertions(+), 192 deletions(-) delete mode 100644 kani-compiler/src/kani_middle/stubbing/transform.rs create mode 100644 kani-compiler/src/kani_middle/transform/contracts.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index ed6e2feeb89e..7811cbc90bb2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -49,8 +49,8 @@ use rustc_target::spec::PanicStrategy; 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::collections::{BTreeMap, HashMap}; use std::ffi::OsString; use std::fmt::Write; use std::fs::File; @@ -235,7 +235,8 @@ impl CodegenBackend for GotocCodegenBackend { let mut results = GotoCodegenResults::new(tcx, reachability); match reachability { ReachabilityType::Harnesses => { - let units = CodegenUnits::new(&queries, tcx); + 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. for unit in units.iter() { // We reset the body cache for now because each codegen unit has different @@ -255,14 +256,12 @@ impl CodegenBackend for GotocCodegenBackend { ); 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, - ); + modifies_instances.push((*harness, assigns_contract)); } } } - units.store_metadata(&queries, tcx); + 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 diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 4f9dce49af95..986681f4ac46 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -238,6 +238,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 index a38410194bdf..1e006d089ce3 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -15,7 +15,7 @@ use crate::kani_middle::reachability::filter_crate_items; use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; use crate::kani_queries::QueryDb; use cbmc::{InternString, InternedString}; -use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; +use kani_metadata::{ArtifactType, AssignsContract, HarnessMetadata, KaniMetadata}; use rustc_hir::def_id::{DefId, DefPathHash}; use rustc_middle::ty::TyCtxt; use rustc_session::config::OutputType; @@ -90,7 +90,15 @@ impl CodegenUnits { self.units.iter() } - pub fn store_metadata(&self, queries: &QueryDb, tcx: TyCtxt) { + /// 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); 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/provide.rs b/kani-compiler/src/kani_middle/provide.rs index 1b176850c60a..852f17b1b2b7 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -58,17 +58,6 @@ fn run_kani_mir_passes<'tcx>( ) -> &'tcx Body<'tcx> { tracing::debug!(?def_id, "Run Kani transformation passes"); let mut transformed_body = body.clone(); - 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); - } // This should be applied after stubbing so user stubs take precedence. ModelIntrinsics::run_pass(tcx, &mut transformed_body); tcx.arena.alloc(transformed_body) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index e2a5ef348d08..b5a3762d1287 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -36,7 +36,7 @@ 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_stub}; +use crate::kani_middle::stubbing::validate_stub; use crate::kani_middle::transform::BodyTransformation; /// Collect all reachable items starting from the given starting points. @@ -399,65 +399,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/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index a96722467225..10cde2243c45 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -3,14 +3,12 @@ //! This module contains code for implementing stubbing. mod annotations; -mod transform; use itertools::Itertools; use rustc_span::DUMMY_SP; use std::collections::HashMap; use tracing::{debug, trace}; -pub use self::transform::*; use kani_metadata::HarnessMetadata; use rustc_hir::def_id::DefId; use rustc_middle::mir::Const; @@ -44,24 +42,25 @@ pub fn harness_stub_map( /// 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> { - 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_ty = rustc_internal::stable(tcx.type_of(old_def_id)).value; - let new_ty = rustc_internal::stable(tcx.type_of(new_def_id)).value; - let old_sig = old_ty.kind().fn_sig().unwrap().skip_binder(); - let new_sig = new_ty.kind().fn_sig().unwrap().skip_binder(); + // 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_sig.inputs_and_output.len() != new_sig.inputs_and_output.len() { + 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_sig.inputs_and_output.len() - 1, + old_body.arg_locals().len(), new_def.name(), - new_sig.inputs_and_output.len() - 1, + 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 { @@ -81,21 +80,21 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul // instead, we should be checking for the equivalence of types up to the // renaming of generic parameters. // - let old_ret_ty = old_sig.output(); - let new_ret_ty = new_sig.output(); + 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_ty, new_arg_ty)) in - old_sig.inputs().iter().zip(new_sig.inputs().iter()).enumerate() + 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 { + if old_arg.ty != new_arg.ty { diff.push(format!( "Expected type `{}` for parameter {}, but found `{}`", - old_arg_ty, + old_arg.ty, i + 1, - new_arg_ty + new_arg.ty )); } } 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 710418534ebc..000000000000 --- a/kani-compiler/src/kani_middle/stubbing/transform.rs +++ /dev/null @@ -1,80 +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_hir::def_id::DefId; -use rustc_index::IndexVec; -use rustc_middle::mir::{ - visit::MutVisitor, Body, Const, ConstValue, Local, LocalDecl, Location, Operand, -}; -use rustc_middle::ty::{self, TyCtxt}; - -use crate::kani_middle::stubbing::check_compatibility; -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 }) -} - -/// 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), - ); - } - } - } -} - -/// Retrieves the stub mapping from the compiler configuration. -fn get_stub_mapping(_tcx: TyCtxt) -> Option> { - None -} 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..228d148cf7d4 --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -0,0 +1,178 @@ +// 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::{matches_diagnostic, KaniAttributes}; +use crate::kani_middle::codegen_units::{CodegenUnit, Stubs}; +use crate::kani_middle::stubbing; +use crate::kani_middle::stubbing::validate_stub; +use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruction}; +use crate::kani_middle::transform::{TransformPass, TransformationType}; +use crate::kani_queries::QueryDb; +use cbmc::{InternString, InternedString}; +use itertools::Itertools; +use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{ + BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, TerminatorKind, + RETURN_LOCAL, +}; +use stable_mir::target::MachineInfo; +use stable_mir::ty::{Abi, Const as MirConst, FnDef, RigidTy, TyKind}; +use stable_mir::{CrateDef, DefId}; +use std::collections::{HashMap, HashSet}; +use std::fmt::Debug; +use strum_macros::AsRefStr; +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, mut 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(tcx, 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.iter().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())); + let result = + self.stubbed.contains(&instance.def.def_id()) || item_attributes.has_recursion(); + result + } + + /// Replace calls to `any_modifies` by calls to `any`. + fn replace_any_modifies(&self, tcx: TyCtxt, 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, args, .. } = &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 let Some(target_fn) = self.target_fn { + 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 8b65b852b7fc..5013aaf0d254 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -19,6 +19,7 @@ use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits}; 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; @@ -60,6 +61,8 @@ impl BodyTransformation { 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 diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index c6c72f6d3bc6..902019040297 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -110,9 +110,6 @@ impl TransformPass for ExternFnStubPass { if let Some(replace) = self.stubs.get(&def) { debug!(func=?instance.name(), orig=?def.name(), replace=?replace.name(), "ExternFnStubPass::transform"); - tracing::error!(func=?instance.name(), orig=?def.name(), replace=?replace - .name(), - "ExternFnStubPass::transform"); let instance = Instance::resolve(*replace, &args).unwrap(); let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap(); let span = bb.terminator.span; diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index 1b1f6311aa11..0b6478bb2dea 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -44,10 +44,4 @@ impl QueryDb { "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/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. From 5ec460547d7ab117449e7138c7eebc1eee602ef0 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Sun, 9 Jun 2024 02:24:01 -0700 Subject: [PATCH 06/11] Handle function pointer stubs --- .../src/kani_middle/transform/body.rs | 139 +++++++++++++++++- .../src/kani_middle/transform/stubs.rs | 79 +++++++--- 2 files changed, 192 insertions(+), 26 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 9402835c2ff2..b7f0c9954a3f 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,136 @@ 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 a 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/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index 902019040297..b81700f1d7b8 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -5,15 +5,18 @@ use crate::kani_middle::attributes::matches_diagnostic; use crate::kani_middle::codegen_units::Stubs; use crate::kani_middle::stubbing::validate_stub; -use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruction}; +use crate::kani_middle::transform::body::{ + CheckType, MutMirVisitor, MutableBody, SourceInstruction, +}; +use crate::kani_middle::transform::check_values::{ty_validity_per_offset, ValidValueReq}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use itertools::Itertools; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ - BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, TerminatorKind, - RETURN_LOCAL, + BinOp, Body, Constant, LocalDecl, Operand, Place, Rvalue, Statement, StatementKind, Terminator, + TerminatorKind, RETURN_LOCAL, }; use stable_mir::target::MachineInfo; use stable_mir::ty::{Abi, Const as MirConst, FnDef, RigidTy, TyKind}; @@ -100,26 +103,17 @@ impl TransformPass for ExternFnStubPass { } /// Search for calls to extern functions that should be stubbed. - fn transform(&self, tcx: TyCtxt, mut body: Body, instance: Instance) -> (bool, Body) { + /// + /// 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 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, args)) = func.ty(&locals).unwrap().kind() { - if let Some(replace) = self.stubs.get(&def) { - debug!(func=?instance.name(), orig=?def.name(), replace=?replace.name(), - "ExternFnStubPass::transform"); - let instance = Instance::resolve(*replace, &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) + 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()) } } @@ -139,3 +133,46 @@ impl ExternFnStubPass { fn has_body(def: FnDef) -> bool { def.body().is_some() } + +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; + } + } + } +} From 2b8d2686bbf25461650359405ee45d89fbd1566b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Sun, 9 Jun 2024 02:33:09 -0700 Subject: [PATCH 07/11] Clean up all warnings --- .../compiler_interface.rs | 7 ++-- kani-compiler/src/kani_compiler.rs | 15 +------- kani-compiler/src/kani_middle/attributes.rs | 4 --- .../src/kani_middle/codegen_units.rs | 8 +---- kani-compiler/src/kani_middle/provide.rs | 8 +---- kani-compiler/src/kani_middle/reachability.rs | 19 +++------- .../src/kani_middle/transform/body.rs | 2 +- .../src/kani_middle/transform/contracts.rs | 36 +++++++------------ .../src/kani_middle/transform/mod.rs | 9 +---- .../src/kani_middle/transform/stubs.rs | 21 +++-------- kani-compiler/src/kani_queries/mod.rs | 24 ++----------- 11 files changed, 33 insertions(+), 120 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 7811cbc90bb2..ca66e1c0e165 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -8,7 +8,7 @@ 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::codegen_units::{CodegenUnit, CodegenUnits}; -use crate::kani_middle::metadata::{canonical_mangled_name, gen_test_metadata}; +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, @@ -18,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,8 +49,7 @@ use rustc_target::spec::PanicStrategy; use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::{CrateDef, DefId}; use std::any::Any; -use std::collections::HashSet; -use std::collections::{BTreeMap, HashMap}; +use std::collections::BTreeMap; use std::ffi::OsString; use std::fmt::Write; use std::fs::File; diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 6fcd2a910080..4c60df7f14dd 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -15,32 +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 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_interface::Config; -use rustc_middle::ty::TyCtxt; 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; diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 986681f4ac46..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) } diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 1e006d089ce3..18823770d254 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -14,7 +14,6 @@ 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 cbmc::{InternString, InternedString}; use kani_metadata::{ArtifactType, AssignsContract, HarnessMetadata, KaniMetadata}; use rustc_hir::def_id::{DefId, DefPathHash}; use rustc_middle::ty::TyCtxt; @@ -40,8 +39,6 @@ pub type Stubs = HashMap; 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, } /// We group the harnesses that have the same stubs. @@ -59,10 +56,7 @@ pub struct CodegenUnit { impl CodegenUnits { pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self { - let crate_info = CrateInfo { - name: stable_mir::local_crate().name.as_str().into(), - output_path: metadata_output_path(tcx), - }; + 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(); diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index 852f17b1b2b7..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. diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index b5a3762d1287..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::validate_stub; 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()); } @@ -186,12 +180,8 @@ impl<'tcx, 'a> MonoItemsCollector<'tcx, 'a> { fn visit_fn(&mut self, instance: Instance) -> Vec { let _guard = debug_span!("visit_fn", function=?instance).entered(); let body = self.transformer.body(self.tcx, instance); - let mut collector = MonoItemsFnCollector { - tcx: self.tcx, - collected: FxHashSet::default(), - body: &body, - instance: &instance, - }; + let mut collector = + MonoItemsFnCollector { tcx: self.tcx, collected: FxHashSet::default(), body: &body }; collector.visit_body(&body); collector.collected.into_iter().collect() } @@ -225,7 +215,6 @@ struct MonoItemsFnCollector<'a, 'tcx> { tcx: TyCtxt<'tcx>, collected: FxHashSet, body: &'a Body, - instance: &'a Instance, } impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index b7f0c9954a3f..7120abd8ec55 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -313,7 +313,7 @@ pub trait MutMirVisitor { self.super_rvalue(rvalue) } - fn visit_operand(&mut self, operand: &mut Operand) {} + fn visit_operand(&mut self, _operand: &mut Operand) {} fn super_body(&mut self, body: &mut MutableBody) { for bb in body.blocks.iter_mut() { diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 228d148cf7d4..c99874cc42a8 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -1,28 +1,20 @@ // 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::{matches_diagnostic, KaniAttributes}; -use crate::kani_middle::codegen_units::{CodegenUnit, Stubs}; -use crate::kani_middle::stubbing; -use crate::kani_middle::stubbing::validate_stub; -use crate::kani_middle::transform::body::{CheckType, MutableBody, SourceInstruction}; +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 itertools::Itertools; use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; -use stable_mir::mir::{ - BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, TerminatorKind, - RETURN_LOCAL, -}; -use stable_mir::target::MachineInfo; -use stable_mir::ty::{Abi, Const as MirConst, FnDef, RigidTy, TyKind}; +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::{HashMap, HashSet}; +use std::collections::HashSet; use std::fmt::Debug; -use strum_macros::AsRefStr; use tracing::{debug, trace}; /// Check if we can replace calls to any_modifies. @@ -55,7 +47,7 @@ impl TransformPass for AnyModifiesPass { } /// Transform the function body by replacing it with the stub body. - fn transform(&self, tcx: TyCtxt, mut body: Body, instance: Instance) -> (bool, 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() { @@ -63,7 +55,7 @@ impl TransformPass for AnyModifiesPass { self.any_body(tcx, body) } else if self.should_apply(tcx, instance) { // Replace any modifies occurrences. - self.replace_any_modifies(tcx, body) + self.replace_any_modifies(body) } else { (false, body) } @@ -90,7 +82,7 @@ impl AnyModifiesPass { 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.iter().map(|(from, _)| from.def_id()).collect::>()) + (target_fn, unit.stubs.keys().map(|from| from.def_id()).collect::>()) } else { (None, HashSet::new()) }; @@ -105,17 +97,15 @@ impl AnyModifiesPass { fn should_apply(&self, tcx: TyCtxt, instance: Instance) -> bool { let item_attributes = KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, instance.def.def_id())); - let result = - self.stubbed.contains(&instance.def.def_id()) || item_attributes.has_recursion(); - result + 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, tcx: TyCtxt, mut body: Body) -> (bool, Body) { + 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, args, .. } = &mut bb.terminator.kind else { continue }; + 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 @@ -146,7 +136,7 @@ impl AnyModifiesPass { valid = false; debug!(?e, "AnyModifiesPass::any_body failed"); let receiver_ty = args.0[0].expect_ty(); - let msg = if let Some(target_fn) = self.target_fn { + let msg = if self.target_fn.is_some() { format!( "`{receiver_ty}` doesn't implement `kani::Arbitrary`.\ Please, check `{}` contract.", diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 5013aaf0d254..8d5c61f55c92 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -16,7 +16,7 @@ //! //! 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, CodegenUnits}; +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; @@ -68,13 +68,6 @@ impl BodyTransformation { 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 { stub_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 diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index b81700f1d7b8..b024adb0f28e 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -2,28 +2,17 @@ // 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::attributes::matches_diagnostic; use crate::kani_middle::codegen_units::Stubs; use crate::kani_middle::stubbing::validate_stub; -use crate::kani_middle::transform::body::{ - CheckType, MutMirVisitor, MutableBody, SourceInstruction, -}; -use crate::kani_middle::transform::check_values::{ty_validity_per_offset, ValidValueReq}; +use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; -use itertools::Itertools; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; -use stable_mir::mir::{ - BinOp, Body, Constant, LocalDecl, Operand, Place, Rvalue, Statement, StatementKind, Terminator, - TerminatorKind, RETURN_LOCAL, -}; -use stable_mir::target::MachineInfo; -use stable_mir::ty::{Abi, Const as MirConst, FnDef, RigidTy, TyKind}; -use stable_mir::CrateDef; +use stable_mir::mir::{Body, Constant, LocalDecl, Operand, Terminator, TerminatorKind}; +use stable_mir::ty::{Const as MirConst, FnDef, RigidTy, TyKind}; use std::collections::HashMap; use std::fmt::Debug; -use strum_macros::AsRefStr; use tracing::{debug, trace}; /// Replace the body of a function that is stubbed by the other. @@ -106,10 +95,10 @@ impl TransformPass for ExternFnStubPass { /// /// 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) { + fn transform(&self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { trace!(function=?instance.name(), "transform"); let mut new_body = MutableBody::from(body); - let mut changed = false; + 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); diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index 0b6478bb2dea..bb28237248d3 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -2,20 +2,16 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Define the communication between KaniCompiler and the codegen implementation. -use cbmc::InternedString; -use kani_metadata::AssignsContract; -use std::{ - collections::HashMap, - 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, - modifies_contracts: HashMap, } impl QueryDb { @@ -30,18 +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}", - ) - } } From 9bfe5a8a9a8bc30f5382b628bf0b474f3aa67b6c Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Sun, 9 Jun 2024 13:00:12 -0700 Subject: [PATCH 08/11] Add a few more validation checks for stubbing --- .../src/kani_middle/codegen_units.rs | 34 +++++++++- kani-compiler/src/kani_middle/stubbing/mod.rs | 2 +- .../src/kani_middle/transform/stubs.rs | 63 +++++++++++++++++-- .../harness/expected | 3 +- tests/expected/issue-2589/issue_2589.expected | 2 +- .../stubbing-type-validation/expected | 17 ++--- 6 files changed, 106 insertions(+), 15 deletions(-) diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 18823770d254..39a5863f7202 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -22,7 +22,7 @@ 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}; +use std::collections::{BTreeMap, HashMap, HashSet}; use std::fs::File; use std::io::BufWriter; use std::path::{Path, PathBuf}; @@ -145,6 +145,7 @@ fn group_by_stubs( .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] }); } } @@ -170,9 +171,11 @@ fn store_metadata(queries: &QueryDb, metadata: &KaniMetadata, filename: &Path) { } } +/// 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); @@ -180,3 +183,32 @@ fn validate_units(tcx: TyCtxt, units: &[CodegenUnit]) { } 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/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs index 10cde2243c45..1abcc0ec4f80 100644 --- a/kani-compiler/src/kani_middle/stubbing/mod.rs +++ b/kani-compiler/src/kani_middle/stubbing/mod.rs @@ -117,7 +117,7 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul /// /// 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_stub(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); diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index b024adb0f28e..6d8849a9f1fe 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -3,14 +3,17 @@ //! 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; +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}; @@ -46,9 +49,10 @@ impl TransformPass for FnStubPass { 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(); - if validate_stub(tcx, new_instance) { - debug!(from=?instance.name(), to=?new_instance.name(), "FnStubPass::transform"); - return (true, new_instance.body().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); } } } @@ -123,6 +127,57 @@ 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, 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/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/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 From 6dad69f6bcceab87313497d5258a8e2e48655313 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Sun, 9 Jun 2024 13:23:35 -0700 Subject: [PATCH 09/11] Adjust a few more tests --- .../check_compiler_sessions.expected | 3 - .../check_compiler_sessions.sh | 27 -------- .../stubbing_compiler_sessions/config.yml | 4 -- .../stubbing_compiler_sessions/stubbing.rs | 64 ------------------- .../verify_std_cmd/verify_std.expected | 5 +- .../verify_std_cmd/verify_std.sh | 17 ++++- 6 files changed, 20 insertions(+), 100 deletions(-) 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 delete mode 100644 tests/script-based-pre/stubbing_compiler_sessions/stubbing.rs 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/stubbing_compiler_sessions/stubbing.rs b/tests/script-based-pre/stubbing_compiler_sessions/stubbing.rs deleted file mode 100644 index cde1902c3558..000000000000 --- a/tests/script-based-pre/stubbing_compiler_sessions/stubbing.rs +++ /dev/null @@ -1,64 +0,0 @@ -// 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. - -fn identity(i: i8) -> i8 { - i -} - -fn decrement(i: i8) -> i8 { - i.wrapping_sub(1) -} - -fn increment(i: i8) -> i8 { - i.wrapping_add(1) -} - -#[kani::proof] -fn check_identity() { - let n = kani::any(); - assert_eq!(identity(n), n); -} - -#[kani::proof] -fn check_decrement() { - let n = kani::any(); - kani::assume(n > i8::MIN); - assert_eq!(decrement(n), n - 1); -} - -#[kani::proof] -#[kani::stub(decrement, increment)] -fn check_decrement_is_increment() { - let n = kani::any(); - kani::assume(n < i8::MAX); - assert_eq!(decrement(n), n + 1); -} - -#[kani::proof] -#[kani::stub(increment, identity)] -#[kani::stub(decrement, identity)] -fn check_all_identity() { - let n = kani::any(); - assert_eq!(decrement(n), increment(n)); -} - -#[kani::proof] -#[kani::stub(decrement, identity)] -#[kani::stub(increment, identity)] -fn check_all_identity_2() { - let n = kani::any(); - assert_eq!(decrement(n), n); - assert_eq!(increment(n), n); -} - -#[kani::proof] -#[kani::stub(decrement, increment)] -#[kani::stub(increment, identity)] -fn check_indirect_all_identity() { - let n = kani::any(); - assert_eq!(decrement(n), n); - assert_eq!(increment(n), n); -} 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} From 40c244570a2842f326da25d5be5bcfc4ee77bb79 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 10 Jun 2024 11:09:10 -0700 Subject: [PATCH 10/11] Apply suggestions from code review Co-authored-by: Felipe R. Monteiro --- kani-compiler/src/kani_compiler.rs | 2 +- kani-compiler/src/kani_middle/transform/body.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 4c60df7f14dd..58c22f940352 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -100,7 +100,7 @@ impl Callbacks for KaniCompiler { debug!(?queries, "config end"); } - /// After analysis, we check the crate items for Kani API misusage or configuration issues. + /// 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, diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 7120abd8ec55..5c321f06b61c 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -287,7 +287,7 @@ fn find_instance(tcx: TyCtxt, diagnostic: &str) -> Option { /// Basic mutable body visitor. /// -/// We removed a many methods for simplicity. +/// We removed many methods for simplicity. /// /// TODO: Contribute this to stable_mir. /// This code was based on the existing MirVisitor: From cf2c5b22d3a584feae6095118227c22319573547 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 10 Jun 2024 11:43:02 -0700 Subject: [PATCH 11/11] Re-add test and improve TODO comments --- .../src/kani_middle/codegen_units.rs | 1 - .../src/kani_middle/transform/body.rs | 2 + .../stubbing-different-sets/stubbing.expected | 19 ++++++ .../stubbing-different-sets/stubbing.rs | 64 +++++++++++++++++++ 4 files changed, 85 insertions(+), 1 deletion(-) create mode 100644 tests/expected/stubbing-different-sets/stubbing.expected create mode 100644 tests/expected/stubbing-different-sets/stubbing.rs diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 39a5863f7202..260b363a868a 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -7,7 +7,6 @@ //! Today, only stub / contracts can affect the harness codegen. Thus, we group the harnesses //! according to their stub configuration. -// TODO: Move this out of CBMC crate. use crate::args::ReachabilityType; use crate::kani_middle::attributes::is_proof_harness; use crate::kani_middle::metadata::gen_proof_metadata; diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 5c321f06b61c..bd6c9be6581a 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -290,6 +290,8 @@ fn find_instance(tcx: TyCtxt, diagnostic: &str) -> Option { /// We removed many methods for simplicity. /// /// TODO: Contribute this to stable_mir. +/// +/// /// This code was based on the existing MirVisitor: /// pub trait MutMirVisitor { 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/expected/stubbing-different-sets/stubbing.rs b/tests/expected/stubbing-different-sets/stubbing.rs new file mode 100644 index 000000000000..90905baa5bb6 --- /dev/null +++ b/tests/expected/stubbing-different-sets/stubbing.rs @@ -0,0 +1,64 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// 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 +} + +fn decrement(i: i8) -> i8 { + i.wrapping_sub(1) +} + +fn increment(i: i8) -> i8 { + i.wrapping_add(1) +} + +#[kani::proof] +fn check_identity() { + let n = kani::any(); + assert_eq!(identity(n), n); +} + +#[kani::proof] +fn check_decrement() { + let n = kani::any(); + kani::assume(n > i8::MIN); + assert_eq!(decrement(n), n - 1); +} + +#[kani::proof] +#[kani::stub(decrement, increment)] +fn check_decrement_is_increment() { + let n = kani::any(); + kani::assume(n < i8::MAX); + assert_eq!(decrement(n), n + 1); +} + +#[kani::proof] +#[kani::stub(increment, identity)] +#[kani::stub(decrement, identity)] +fn check_all_identity() { + let n = kani::any(); + assert_eq!(decrement(n), increment(n)); +} + +#[kani::proof] +#[kani::stub(decrement, identity)] +#[kani::stub(increment, identity)] +fn check_all_identity_2() { + let n = kani::any(); + assert_eq!(decrement(n), n); + assert_eq!(increment(n), n); +} + +#[kani::proof] +#[kani::stub(decrement, increment)] +#[kani::stub(increment, identity)] +fn check_indirect_all_identity() { + let n = kani::any(); + assert_eq!(decrement(n), n); + assert_eq!(increment(n), n); +}