diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs index 15c0282f9a40..8b61722344fb 100644 --- a/cprover_bindings/src/goto_program/mod.rs +++ b/cprover_bindings/src/goto_program/mod.rs @@ -22,6 +22,6 @@ pub use expr::{ }; pub use location::Location; pub use stmt::{Stmt, StmtBody, SwitchCase}; -pub use symbol::{Symbol, SymbolValues}; +pub use symbol::{FunctionContract, Lambda, Symbol, SymbolValues}; pub use symbol_table::SymbolTable; pub use typ::{CIntType, DatatypeComponent, Parameter, Type}; diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs index 7f74abaa9816..b1082a8f1f80 100644 --- a/cprover_bindings/src/goto_program/symbol.rs +++ b/cprover_bindings/src/goto_program/symbol.rs @@ -13,6 +13,8 @@ pub struct Symbol { pub location: Location, pub typ: Type, pub value: SymbolValues, + /// Contracts to be enforced (only supported for functions) + pub contract: Option>, /// Optional debugging information @@ -44,6 +46,57 @@ pub struct Symbol { pub is_weak: bool, } +/// The equivalent of a "mathematical function" in CBMC. Semantically this is an +/// anonymous function object, similar to a closure, but without closing over an +/// environment. +/// +/// This is only valid for use as a function contract. It may not perform side +/// effects, a property that is enforced on the CBMC side. +/// +/// The precise nomenclature is that in CBMC a contract value has *type* +/// `mathematical_function` and values of that type are `lambda`s. Since this +/// struct represents such values it is named `Lambda`. +#[derive(Debug, Clone)] +pub struct Lambda { + pub arguments: Vec, + pub body: Expr, +} + +impl Lambda { + pub fn as_contract_for( + fn_ty: &Type, + return_var_name: Option, + body: Expr, + ) -> Self { + let arguments = match fn_ty { + Type::Code { parameters, return_type } => { + [Parameter::new(None, return_var_name, (**return_type).clone())] + .into_iter() + .chain(parameters.iter().cloned()) + .collect() + } + _ => panic!( + "Contract lambdas can only be generated for `Code` types, received {fn_ty:?}" + ), + }; + Self { arguments, body } + } +} + +/// The CBMC representation of a function contract. Represents +/// https://diffblue.github.io/cbmc/contracts-user.html but currently only assigns clauses are +/// supported. +#[derive(Clone, Debug)] +pub struct FunctionContract { + pub(crate) assigns: Vec, +} + +impl FunctionContract { + pub fn new(assigns: Vec) -> Self { + Self { assigns } + } +} + /// Currently, only C is understood by CBMC. // TODO: #[derive(Clone, Debug)] @@ -84,6 +137,7 @@ impl Symbol { base_name, pretty_name, + contract: None, module: None, mode: SymbolModes::C, // global properties @@ -107,6 +161,18 @@ impl Symbol { } } + /// Add this contract to the symbol (symbol must be a function) or fold the + /// conditions into an existing contract. + pub fn attach_contract(&mut self, contract: FunctionContract) { + assert!(self.typ.is_code()); + match self.contract { + Some(ref mut prior) => { + prior.assigns.extend(contract.assigns); + } + None => self.contract = Some(Box::new(contract)), + } + } + /// The symbol that defines the type of the struct or union. /// For a struct foo this is the symbol "tag-foo" that maps to the type struct foo. pub fn aggr_ty>(t: Type, pretty_name: T) -> Symbol { @@ -319,6 +385,12 @@ impl Symbol { self.is_auxiliary = hidden; self } + + /// Set `is_property`. + pub fn with_is_property(mut self, v: bool) -> Self { + self.is_property = v; + self + } } /// Predicates diff --git a/cprover_bindings/src/goto_program/symbol_table.rs b/cprover_bindings/src/goto_program/symbol_table.rs index 1e635ec925da..8125c8df3cd9 100644 --- a/cprover_bindings/src/goto_program/symbol_table.rs +++ b/cprover_bindings/src/goto_program/symbol_table.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT use super::super::{env, MachineModel}; -use super::{BuiltinFn, Stmt, Symbol}; +use super::{BuiltinFn, FunctionContract, Stmt, Symbol}; use crate::InternedString; use std::collections::BTreeMap; /// This is a typesafe implementation of the CBMC symbol table, based on the CBMC code at: @@ -79,6 +79,17 @@ impl SymbolTable { let name = name.into(); self.symbol_table.get_mut(&name).unwrap().update_fn_declaration_with_definition(body); } + + /// Attach a contract to the symbol identified by `name`. If a prior + /// contract exists it is extended with additional clauses. + pub fn attach_contract>( + &mut self, + name: T, + contract: FunctionContract, + ) { + let sym = self.symbol_table.get_mut(&name.into()).unwrap(); + sym.attach_contract(contract); + } } /// Getters diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index 9d1649b99cd1..dd07c150bb3f 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/cprover_bindings/src/goto_program/typ.rs @@ -228,6 +228,17 @@ impl Parameter { } } +/// Constructor +impl Parameter { + pub fn new>( + base_name: Option, + identifier: Option, + typ: Type, + ) -> Self { + Self { base_name: base_name.map(Into::into), identifier: identifier.map(Into::into), typ } + } +} + impl CIntType { pub fn sizeof_in_bits(&self, st: &SymbolTable) -> u64 { match self { diff --git a/cprover_bindings/src/irep/irep.rs b/cprover_bindings/src/irep/irep.rs index 68e094000884..0d0c6dc4ace7 100644 --- a/cprover_bindings/src/irep/irep.rs +++ b/cprover_bindings/src/irep/irep.rs @@ -6,6 +6,7 @@ use super::super::goto_program::{Location, Type}; use super::super::MachineModel; use super::{IrepId, ToIrep}; use crate::cbmc_string::InternedString; +use crate::linear_map; use linear_map::LinearMap; use num::BigInt; use std::fmt::Debug; @@ -141,4 +142,12 @@ impl Irep { pub fn zero() -> Irep { Irep::just_id(IrepId::Id0) } + + pub fn tuple(sub: Vec) -> Self { + Irep { + id: IrepId::Tuple, + sub, + named_sub: linear_map![(IrepId::Type, Irep::just_id(IrepId::Tuple))], + } + } } diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index 3ad8f71a7e86..cad6eb563bf4 100644 --- a/cprover_bindings/src/irep/irep_id.rs +++ b/cprover_bindings/src/irep/irep_id.rs @@ -593,6 +593,7 @@ pub enum IrepId { CSpecLoopInvariant, CSpecRequires, CSpecEnsures, + CSpecAssigns, VirtualFunction, ElementType, WorkingDirectory, @@ -1462,6 +1463,7 @@ impl ToString for IrepId { IrepId::CSpecLoopInvariant => "#spec_loop_invariant", IrepId::CSpecRequires => "#spec_requires", IrepId::CSpecEnsures => "#spec_ensures", + IrepId::CSpecAssigns => "#spec_assigns", IrepId::VirtualFunction => "virtual_function", IrepId::ElementType => "element_type", IrepId::WorkingDirectory => "working_directory", diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 41c501896cd1..16b8b69c8fe7 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/cprover_bindings/src/irep/to_irep.rs @@ -6,8 +6,9 @@ use super::super::goto_program; use super::super::MachineModel; use super::{Irep, IrepId}; use crate::linear_map; +use crate::InternedString; use goto_program::{ - BinaryOperator, CIntType, DatatypeComponent, Expr, ExprValue, Location, Parameter, + BinaryOperator, CIntType, DatatypeComponent, Expr, ExprValue, Lambda, Location, Parameter, SelfOperator, Stmt, StmtBody, SwitchCase, SymbolValues, Type, UnaryOperator, }; @@ -16,10 +17,10 @@ pub trait ToIrep { } /// Utility functions -fn arguments_irep(arguments: &[Expr], mm: &MachineModel) -> Irep { +fn arguments_irep<'a>(arguments: impl Iterator, mm: &MachineModel) -> Irep { Irep { id: IrepId::Arguments, - sub: arguments.iter().map(|x| x.to_irep(mm)).collect(), + sub: arguments.map(|x| x.to_irep(mm)).collect(), named_sub: linear_map![], } } @@ -169,6 +170,16 @@ impl ToIrep for Expr { } } +impl Irep { + pub fn symbol(identifier: InternedString) -> Self { + Irep { + id: IrepId::Symbol, + sub: vec![], + named_sub: linear_map![(IrepId::Identifier, Irep::just_string_id(identifier))], + } + } +} + impl ToIrep for ExprValue { fn to_irep(&self, mm: &MachineModel) -> Irep { match self { @@ -245,7 +256,7 @@ impl ToIrep for ExprValue { } ExprValue::FunctionCall { function, arguments } => side_effect_irep( IrepId::FunctionCall, - vec![function.to_irep(mm), arguments_irep(arguments, mm)], + vec![function.to_irep(mm), arguments_irep(arguments.iter(), mm)], ), ExprValue::If { c, t, e } => Irep { id: IrepId::If, @@ -297,14 +308,7 @@ impl ToIrep for ExprValue { sub: values.iter().map(|x| x.to_irep(mm)).collect(), named_sub: linear_map![], }, - ExprValue::Symbol { identifier } => Irep { - id: IrepId::Symbol, - sub: vec![], - named_sub: linear_map![( - IrepId::Identifier, - Irep::just_string_id(identifier.to_string()), - )], - }, + ExprValue::Symbol { identifier } => Irep::symbol(*identifier), ExprValue::Typecast(e) => { Irep { id: IrepId::Typecast, sub: vec![e.to_irep(mm)], named_sub: linear_map![] } } @@ -456,7 +460,7 @@ impl ToIrep for StmtBody { vec![ lhs.as_ref().map_or(Irep::nil(), |x| x.to_irep(mm)), function.to_irep(mm), - arguments_irep(arguments, mm), + arguments_irep(arguments.iter(), mm), ], ), StmtBody::Goto(dest) => code_irep(IrepId::Goto, vec![]) @@ -499,10 +503,50 @@ impl ToIrep for SwitchCase { } } +impl ToIrep for Lambda { + /// At the moment this function assumes that this lambda is used for a + /// `modifies` contract. It should work for any other lambda body, but + /// the parameter names use "modifies" in their generated names. + fn to_irep(&self, mm: &MachineModel) -> Irep { + let (ops_ireps, types) = self + .arguments + .iter() + .enumerate() + .map(|(index, param)| { + let ty_rep = param.typ().to_irep(mm); + ( + Irep::symbol( + param.identifier().unwrap_or_else(|| format!("_modifies_{index}").into()), + ) + .with_named_sub(IrepId::Type, ty_rep.clone()), + ty_rep, + ) + }) + .unzip(); + let typ = Irep { + id: IrepId::MathematicalFunction, + sub: vec![Irep::just_sub(types), self.body.typ().to_irep(mm)], + named_sub: Default::default(), + }; + Irep { + id: IrepId::Lambda, + sub: vec![Irep::tuple(ops_ireps), self.body.to_irep(mm)], + named_sub: linear_map!((IrepId::Type, typ)), + } + } +} + impl goto_program::Symbol { pub fn to_irep(&self, mm: &MachineModel) -> super::Symbol { + let mut typ = self.typ.to_irep(mm); + if let Some(contract) = &self.contract { + typ = typ.with_named_sub( + IrepId::CSpecAssigns, + Irep::just_sub(contract.assigns.iter().map(|req| req.to_irep(mm)).collect()), + ); + } super::Symbol { - typ: self.typ.to_irep(mm), + typ, value: match &self.value { SymbolValues::Expr(e) => e.to_irep(mm), SymbolValues::Stmt(s) => s.to_irep(mm), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs new file mode 100644 index 000000000000..964286984fc6 --- /dev/null +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -0,0 +1,119 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +use crate::codegen_cprover_gotoc::GotocCtx; +use crate::kani_middle::attributes::KaniAttributes; +use cbmc::goto_program::FunctionContract; +use cbmc::goto_program::Lambda; +use kani_metadata::AssignsContract; +use rustc_hir::def_id::DefId as InternalDefId; +use rustc_smir::rustc_internal; +use stable_mir::mir::mono::{Instance, MonoItem}; +use stable_mir::mir::Local; +use stable_mir::CrateDef; +use tracing::debug; + +impl<'tcx> GotocCtx<'tcx> { + /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`, + /// find or create the `AssignsContract` that needs to be enforced and attach it to the symbol + /// for which it needs to be enforced. + /// + /// 1. Gets the `#[kanitool::inner_check = "..."]` target, then resolves exactly one instance + /// of it. Panics if there are more or less than one instance. + /// 2. Expects that a `#[kanitool::modifies(...)]` is placed on the `inner_check` function, + /// turns it into a CBMC contract and attaches it to the symbol for the previously resolved + /// instance. + /// 3. Returns the mangled name of the symbol it attached the contract to. + /// 4. Resolves the `#[kanitool::checked_with = "..."]` target from `function_under_contract` + /// which has `static mut REENTRY : bool` declared inside. + /// 5. Returns the full path to this constant that `--nondet-static-exclude` expects which is + /// comprised of the file path that `checked_with` is located in, the name of the + /// `checked_with` function and the name of the constant (`REENTRY`). + pub fn handle_check_contract( + &mut self, + function_under_contract: InternalDefId, + items: &[MonoItem], + ) -> AssignsContract { + let tcx = self.tcx; + let function_under_contract_attrs = KaniAttributes::for_item(tcx, function_under_contract); + let wrapped_fn = function_under_contract_attrs.inner_check().unwrap().unwrap(); + + let mut instance_under_contract = items.iter().filter_map(|i| match i { + MonoItem::Fn(instance @ Instance { def, .. }) + if wrapped_fn == rustc_internal::internal(def.def_id()) => + { + Some(*instance) + } + _ => None, + }); + let instance_of_check = instance_under_contract.next().unwrap(); + assert!( + instance_under_contract.next().is_none(), + "Only one instance of a checked function may be in scope" + ); + let attrs_of_wrapped_fn = KaniAttributes::for_item(tcx, wrapped_fn); + let assigns_contract = attrs_of_wrapped_fn.modifies_contract().unwrap_or_else(|| { + debug!(?instance_of_check, "had no assigns contract specified"); + vec![] + }); + self.attach_modifies_contract(instance_of_check, assigns_contract); + + let wrapper_name = self.symbol_name_stable(instance_of_check); + + let recursion_wrapper_id = + function_under_contract_attrs.checked_with_id().unwrap().unwrap(); + let span_of_recursion_wrapper = tcx.def_span(recursion_wrapper_id); + let location_of_recursion_wrapper = self.codegen_span(&span_of_recursion_wrapper); + + let full_name = format!( + "{}:{}::REENTRY", + location_of_recursion_wrapper + .filename() + .expect("recursion location wrapper should have a file name"), + tcx.item_name(recursion_wrapper_id), + ); + + AssignsContract { recursion_tracker: full_name, contracted_function_name: wrapper_name } + } + + /// Convert the Kani level contract into a CBMC level contract by creating a + /// CBMC lambda. + fn codegen_modifies_contract(&mut self, modified_places: Vec) -> FunctionContract { + let goto_annotated_fn_name = self.current_fn().name(); + let goto_annotated_fn_typ = self + .symbol_table + .lookup(&goto_annotated_fn_name) + .unwrap_or_else(|| panic!("Function '{goto_annotated_fn_name}' is not declared")) + .typ + .clone(); + + let assigns = modified_places + .into_iter() + .map(|local| { + Lambda::as_contract_for( + &goto_annotated_fn_typ, + None, + self.codegen_place_stable(&local.into()).unwrap().goto_expr.dereference(), + ) + }) + .collect(); + + FunctionContract::new(assigns) + } + + /// Convert the contract to a CBMC contract, then attach it to `instance`. + /// `instance` must have previously been declared. + /// + /// This merges with any previously attached contracts. + pub fn attach_modifies_contract(&mut self, instance: Instance, modified_places: Vec) { + // This should be safe, since the contract is pretty much evaluated as + // though it was the first (or last) assertion in the function. + assert!(self.current_fn.is_none()); + let body = instance.body().unwrap(); + self.set_current_fn(instance, &body); + let goto_contract = self.codegen_modifies_contract(modified_places); + let name = self.current_fn().name(); + + self.symbol_table.attach_contract(name, goto_contract); + self.reset_current_fn() + } +} diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs index 938a784765e0..238bdb27b069 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs @@ -17,6 +17,7 @@ mod statement; mod static_var; // Visible for all codegen module. +pub mod contract; mod ty_stable; pub(super) mod typ; diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 8b21093f4667..1cfff307f856 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -6,8 +6,8 @@ use crate::args::ReachabilityType; use crate::codegen_cprover_gotoc::GotocCtx; use crate::kani_middle::analysis; -use crate::kani_middle::attributes::is_test_harness_description; -use crate::kani_middle::metadata::gen_test_metadata; +use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes}; +use crate::kani_middle::metadata::{canonical_mangled_name, gen_test_metadata}; use crate::kani_middle::provide; use crate::kani_middle::reachability::{ collect_reachable_items, filter_const_crate_items, filter_crate_items, @@ -19,9 +19,9 @@ use cbmc::irep::goto_binary_serde::write_goto_binary_file; use cbmc::{InternString, RoundingMode}; use cbmc::{InternedString, MachineModel}; use kani_metadata::artifact::convert_type; -use kani_metadata::CompilerArtifactStub; use kani_metadata::UnsupportedFeature; use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; +use kani_metadata::{AssignsContract, CompilerArtifactStub}; use rustc_codegen_ssa::back::archive::{ get_native_object_symbols, ArArchiveBuilder, ArchiveBuilder, }; @@ -31,7 +31,7 @@ use rustc_codegen_ssa::{CodegenResults, CrateInfo}; use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; use rustc_data_structures::temp_dir::MaybeTempDir; use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; -use rustc_hir::def_id::LOCAL_CRATE; +use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; use rustc_metadata::creader::MetadataLoaderDyn; use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; use rustc_metadata::EncodedMetadata; @@ -45,7 +45,7 @@ use rustc_smir::rustc_internal; use rustc_target::abi::Endian; use rustc_target::spec::PanicStrategy; use stable_mir::mir::mono::{Instance, MonoItem}; -use stable_mir::CrateDef; +use stable_mir::{CrateDef, DefId}; use std::any::Any; use std::collections::BTreeMap; use std::collections::HashSet; @@ -62,6 +62,7 @@ use tempfile::Builder as TempFileBuilder; use tracing::{debug, error, info}; pub type UnsupportedConstructs = FxHashMap>; + #[derive(Clone)] pub struct GotocCodegenBackend { /// The query is shared with `KaniCompiler` and it is initialized as part of `rustc` @@ -77,13 +78,16 @@ impl GotocCodegenBackend { } /// Generate code that is reachable from the given starting points. + /// + /// Invariant: iff `check_contract.is_some()` then `return.2.is_some()` fn codegen_items<'tcx>( &self, tcx: TyCtxt<'tcx>, starting_items: &[MonoItem], symtab_goto: &Path, machine_model: &MachineModel, - ) -> (GotocCtx<'tcx>, Vec) { + check_contract: Option, + ) -> (GotocCtx<'tcx>, Vec, Option) { let items = with_timer( || collect_reachable_items(tcx, starting_items), "codegen reachability analysis", @@ -95,7 +99,7 @@ impl GotocCodegenBackend { let mut gcx = GotocCtx::new(tcx, (*self.queries.lock().unwrap()).clone(), machine_model); check_reachable_items(gcx.tcx, &gcx.queries, &items); - with_timer( + let contract_info = with_timer( || { // we first declare all items for item in &items { @@ -142,6 +146,8 @@ impl GotocCodegenBackend { MonoItem::GlobalAsm(_) => {} // We have already warned above } } + + check_contract.map(|check_id| gcx.handle_check_contract(check_id, &items)) }, "codegen", ); @@ -178,7 +184,7 @@ impl GotocCodegenBackend { } } - (gcx, items) + (gcx, items, contract_info) } } @@ -235,13 +241,22 @@ impl CodegenBackend for GotocCodegenBackend { for harness in harnesses { let model_path = queries.harness_model_path(&harness.mangled_name()).unwrap(); - let (gcx, mono_items) = self.codegen_items( + 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, ); - results.extend(gcx, mono_items, None); + 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, + ); + } } } ReachabilityType::Tests => { @@ -262,10 +277,17 @@ impl CodegenBackend for GotocCodegenBackend { // We will be able to remove this once we optimize all calls to CBMC utilities. // https://github.com/model-checking/kani/issues/1971 let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); - let (gcx, items) = - self.codegen_items(tcx, &harnesses, &model_path, &results.machine_model); + let (gcx, items, contract_info) = self.codegen_items( + tcx, + &harnesses, + &model_path, + &results.machine_model, + Default::default(), + ); results.extend(gcx, items, None); + assert!(contract_info.is_none()); + for (test_fn, test_desc) in harnesses.iter().zip(descriptions.iter()) { let instance = if let MonoItem::Fn(instance) = test_fn { instance } else { continue }; @@ -292,12 +314,14 @@ impl CodegenBackend for GotocCodegenBackend { .map(MonoItem::Fn) .collect::>(); let model_path = base_filename.with_extension(ArtifactType::SymTabGoto); - let (gcx, items) = self.codegen_items( + let (gcx, items, contract_info) = self.codegen_items( tcx, &local_reachable, &model_path, &results.machine_model, + Default::default(), ); + assert!(contract_info.is_none()); results.extend(gcx, items, None); } } @@ -394,6 +418,14 @@ impl CodegenBackend for GotocCodegenBackend { } } +fn contract_metadata_for_harness( + tcx: TyCtxt, + def_id: DefId, +) -> Result, ErrorGuaranteed> { + let attrs = KaniAttributes::for_def_id(tcx, def_id); + Ok(attrs.interpret_the_for_contract_attribute().transpose()?.map(|(_, id, _)| id)) +} + fn check_target(session: &Session) { // The requirement below is needed to build a valid CBMC machine model // in function `machine_model_from_session` from diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 57280c5b332b..118821f5995f 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -29,6 +29,7 @@ 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; @@ -184,21 +185,43 @@ impl KaniCompiler { pub fn run(&mut self, orig_args: Vec) -> Result<(), ErrorGuaranteed> { loop { debug!(next=?self.stage, "run"); - match &self.stage { - CompilationStage::Init => { - self.run_compilation_session(&orig_args)?; + // 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 = &target_harnesses[0]; - let extra_arg = - stubbing::mk_rustc_arg(&all_harnesses[&target_harness].stub_map); + 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)?; + self.run_compilation_session(&args)? } CompilationStage::Done { metadata: Some((kani_metadata, crate_info)) } => { // Only store metadata for harnesses for now. @@ -251,7 +274,7 @@ impl KaniCompiler { } else { CompilationStage::Done { metadata: Some(( - generate_metadata(&crate_info, all_harnesses), + generate_metadata(&crate_info, &all_harnesses), crate_info.clone(), )), } @@ -269,7 +292,8 @@ impl KaniCompiler { let queries = self.queries.clone(); let mut compiler = RunCompiler::new(args, self); compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| backend(queries)))); - compiler.run() + compiler.run()?; + Ok(()) } /// Gather and process all harnesses from this crate that shall be compiled. @@ -470,6 +494,7 @@ mod tests { original_end_line: 20, goto_file: None, attributes: HarnessAttributes::default(), + contract: Default::default(), } } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index bfc36360270e..e9edbedfcd82 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -6,17 +6,25 @@ use std::collections::BTreeMap; use kani_metadata::{CbmcSolver, HarnessAttributes, Stub}; use rustc_ast::{ - attr, AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, + attr, + token::Token, + token::TokenKind, + tokenstream::{TokenStream, TokenTree}, + AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, NestedMetaItem, }; use rustc_errors::ErrorGuaranteed; -use rustc_hir::{def::DefKind, def_id::DefId}; +use rustc_hir::{ + def::DefKind, + def_id::{DefId, LocalDefId}, +}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_session::Session; use rustc_smir::rustc_internal; use rustc_span::{Span, Symbol}; use stable_mir::mir::mono::Instance as InstanceStable; -use stable_mir::CrateDef; +use stable_mir::mir::Local; +use stable_mir::{CrateDef, DefId as StableDefId}; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; @@ -51,6 +59,17 @@ enum KaniAttributeKind { /// Attribute on a function that was auto-generated from expanding a /// function contract. IsContractGenerated, + /// Identifies a set of pointer arguments that should be added to the write + /// set when checking a function contract. Placed on the inner check function. + /// + /// Emitted by the expansion of a `modifies` function contract clause. + Modifies, + /// A function used as the inner code of a contract check. + /// + /// Contains the original body of the contracted function. The signature is + /// expanded with additional pointer arguments that are not used in the function + /// but referenced by the `modifies` annotation. + InnerCheck, } impl KaniAttributeKind { @@ -67,6 +86,8 @@ impl KaniAttributeKind { KaniAttributeKind::Unstable | KaniAttributeKind::ReplacedWith | KaniAttributeKind::CheckedWith + | KaniAttributeKind::Modifies + | KaniAttributeKind::InnerCheck | KaniAttributeKind::IsContractGenerated => false, } } @@ -115,7 +136,12 @@ impl<'tcx> KaniAttributes<'tcx> { /// Perform preliminary parsing and checking for the attributes on this /// function pub fn for_instance(tcx: TyCtxt<'tcx>, instance: InstanceStable) -> Self { - KaniAttributes::for_item(tcx, rustc_internal::internal(instance.def.def_id())) + KaniAttributes::for_def_id(tcx, instance.def.def_id()) + } + + /// Look up the attributes by a stable MIR DefID + pub fn for_def_id(tcx: TyCtxt<'tcx>, def_id: StableDefId) -> Self { + KaniAttributes::for_item(tcx, rustc_internal::internal(def_id)) } pub fn for_item(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self { @@ -177,7 +203,7 @@ impl<'tcx> KaniAttributes<'tcx> { /// Parse and extract the `proof_for_contract(TARGET)` attribute. The /// returned symbol and DefId are respectively the name and id of `TARGET`, /// the span in the span for the attribute (contents). - fn interpret_the_for_contract_attribute( + pub(crate) fn interpret_the_for_contract_attribute( &self, ) -> Option> { self.expect_maybe_one(KaniAttributeKind::ProofForContract).map(|target| { @@ -206,18 +232,60 @@ impl<'tcx> KaniAttributes<'tcx> { .map(|target| expect_key_string_value(self.tcx.sess, target)) } - /// Extract the name of the sibling function this function's contract is - /// stubbed as (if any). - /// - /// `None` indicates this function does not use a contract, `Some(Err(_))` - /// indicates a contract does exist but an error occurred during resolution. + pub fn inner_check(&self) -> Option> { + self.eval_sibling_attribute(KaniAttributeKind::InnerCheck) + } + pub fn replaced_with(&self) -> Option> { self.expect_maybe_one(KaniAttributeKind::ReplacedWith) .map(|target| expect_key_string_value(self.tcx.sess, target)) } - /// Resolve a function that is known to reside in the same module as the one - /// these attributes belong to (`self.item`). + /// Retrieves the global, static recursion tracker variable. + pub fn checked_with_id(&self) -> Option> { + self.eval_sibling_attribute(KaniAttributeKind::CheckedWith) + } + + /// Find the `mod` that `self.item` is defined in, then search in the items defined in this + /// `mod` for an item that is named after the `name` in the `#[kanitool:: = ""]` + /// annotation on `self.item`. + /// + /// This is similar to [`resolve_fn`] but more efficient since it only looks inside one `mod`. + fn eval_sibling_attribute( + &self, + kind: KaniAttributeKind, + ) -> Option> { + use rustc_hir::{Item, ItemKind, Mod, Node}; + self.expect_maybe_one(kind).map(|target| { + let name = expect_key_string_value(self.tcx.sess, target)?; + let hir_map = self.tcx.hir(); + let hir_id = self.tcx.local_def_id_to_hir_id(self.item.expect_local()); + let find_in_mod = |md: &Mod<'_>| { + md.item_ids + .iter() + .find(|it| hir_map.item(**it).ident.name == name) + .unwrap() + .hir_id() + }; + + let result = match hir_map.get_parent(hir_id) { + Node::Item(Item { kind, .. }) => match kind { + ItemKind::Mod(m) => find_in_mod(m), + ItemKind::Impl(imp) => { + imp.items.iter().find(|it| it.ident.name == name).unwrap().id.hir_id() + } + other => panic!("Odd parent item kind {other:?}"), + }, + Node::Crate(m) => find_in_mod(m), + other => panic!("Odd parent node type {other:?}"), + } + .expect_owner() + .def_id + .to_def_id(); + Ok(result) + }) + } + fn resolve_sibling(&self, path_str: &str) -> Result> { resolve_fn( self.tcx, @@ -295,6 +363,12 @@ impl<'tcx> KaniAttributes<'tcx> { // to communicate with one another. So by the time it gets // here we don't care if it's valid or not. } + KaniAttributeKind::Modifies => { + self.modifies_contract(); + } + KaniAttributeKind::InnerCheck => { + self.inner_check(); + } } } } @@ -396,6 +470,8 @@ impl<'tcx> KaniAttributes<'tcx> { } KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated + | KaniAttributeKind::Modifies + | KaniAttributeKind::InnerCheck | KaniAttributeKind::ReplacedWith => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref())); } @@ -451,7 +527,7 @@ impl<'tcx> KaniAttributes<'tcx> { .with_span_note( self.tcx.def_span(def_id), format!( - "Try adding a contract to this function or use the unsound `{}` attribute instead.", + "Try adding a contract to this function or use the unsound `{}` attribute instead.", KaniAttributeKind::Stub.as_ref(), ) ) @@ -498,6 +574,81 @@ impl<'tcx> KaniAttributes<'tcx> { resolve::resolve_fn(self.tcx, current_module.to_local_def_id(), &replacement).unwrap(); Stub { original: original_str.to_string(), replacement } } + + /// Parse and interpret the `kanitool::modifies(var1, var2, ...)` annotation into the vector + /// `[var1, var2, ...]`. + pub fn modifies_contract(&self) -> Option> { + let local_def_id = self.item.expect_local(); + self.map.get(&KaniAttributeKind::Modifies).map(|attr| { + attr.iter() + .flat_map(|clause| match &clause.get_normal_item().args { + AttrArgs::Delimited(lvals) => { + parse_modify_values(self.tcx, local_def_id, &lvals.tokens) + } + _ => unreachable!(), + }) + .collect() + }) + } +} + +/// Pattern macro for the comma token used in attributes. +macro_rules! comma_tok { + () => { + TokenTree::Token(Token { kind: TokenKind::Comma, .. }, _) + }; +} + +/// Parse the token stream inside an attribute (like `kanitool::modifies`) as a comma separated +/// sequence of function parameter names on `local_def_id` (must refer to a function). Then +/// translates the names into [`Local`]s. +fn parse_modify_values<'a>( + tcx: TyCtxt<'a>, + local_def_id: LocalDefId, + t: &'a TokenStream, +) -> impl Iterator + 'a { + let mir = tcx.optimized_mir(local_def_id); + let mut iter = t.trees(); + std::iter::from_fn(move || { + let tree = iter.next()?; + let wrong_token_err = || { + tcx.sess.parse_sess.dcx.span_err(tree.span(), "Unexpected token. Expected identifier.") + }; + let result = match tree { + TokenTree::Token(token, _) => { + if let TokenKind::Ident(id, _) = &token.kind { + let hir = tcx.hir(); + let bid = hir.body_owned_by(local_def_id); + Some( + hir.body_param_names(bid) + .zip(mir.args_iter()) + .find(|(name, _decl)| name.name == *id) + .unwrap() + .1 + .as_usize(), + ) + } else { + wrong_token_err(); + None + } + } + _ => { + wrong_token_err(); + None + } + }; + match iter.next() { + None | Some(comma_tok!()) => (), + Some(not_comma) => { + tcx.sess.parse_sess.dcx.span_err( + not_comma.span(), + "Unexpected token, expected end of attribute or comma", + ); + iter.by_ref().skip_while(|t| !matches!(t, comma_tok!())).count(); + } + } + result + }) } /// An efficient check for the existence for a particular [`KaniAttributeKind`]. diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 43eed5ecac3a..02f5da107556 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -3,6 +3,7 @@ //! This module handles Kani metadata generation. For example, generating HarnessMetadata for a //! given function. +use std::default::Default; use std::path::Path; use crate::kani_middle::attributes::test_harness_name; @@ -13,15 +14,19 @@ use stable_mir::CrateDef; use super::{attributes::KaniAttributes, SourceLocation}; +pub fn canonical_mangled_name(instance: Instance) -> String { + let pretty_name = instance.name(); + // Main function a special case in order to support `--function main` + // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129 + if pretty_name == "main" { pretty_name } else { instance.mangled_name() } +} + /// 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 pretty_name = instance.name(); - // Main function a special case in order to support `--function main` - // TODO: Get rid of this: https://github.com/model-checking/kani/issues/2129 - let mangled_name = - if pretty_name == "main" { pretty_name.clone() } else { instance.mangled_name() }; + let mangled_name = canonical_mangled_name(instance); // We get the body span to include the entire function definition. // This is required for concrete playback to properly position the generated test. @@ -39,6 +44,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> attributes, // TODO: This no longer needs to be an Option. goto_file: Some(model_file), + contract: Default::default(), } } @@ -66,5 +72,6 @@ pub fn gen_test_metadata( attributes: HarnessAttributes::default(), // TODO: This no longer needs to be an Option. goto_file: Some(model_file), + contract: Default::default(), } } diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 4ccac4f485fe..66fb2ca0aa33 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -84,7 +84,7 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) }; if !def_ids.contains(&def_id) { // Check if any unstable attribute was reached. - KaniAttributes::for_item(tcx, rustc_internal::internal(def_id)) + KaniAttributes::for_def_id(tcx, def_id) .check_unstable_features(&queries.args().unstable_features); def_ids.insert(def_id); } diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 1d3b1a2c2f06..e88485ebc6d7 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -52,7 +52,7 @@ pub fn resolve_fn<'tcx>( /// paths. /// /// Note: This function was written to be generic, however, it has only been tested for functions. -fn resolve_path<'tcx>( +pub(crate) fn resolve_path<'tcx>( tcx: TyCtxt<'tcx>, current_module: LocalDefId, path_str: &str, diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index 6bda0a20bd2f..e918bf1b8a73 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -3,6 +3,8 @@ //! Define the communication between KaniCompiler and the codegen implementation. use cbmc::{InternString, InternedString}; +use kani_metadata::AssignsContract; +use std::fmt::{Display, Formatter, Write}; use std::{ collections::HashMap, path::PathBuf, @@ -17,6 +19,7 @@ pub struct QueryDb { args: Option, /// Information about all target harnesses. pub harnesses_info: HashMap, + modifies_contracts: HashMap, } impl QueryDb { @@ -41,4 +44,41 @@ impl QueryDb { pub fn args(&self) -> &Arguments { self.args.as_ref().expect("Arguments have not been initialized") } + + /// Register that a CBMC-level `assigns` contract for a function that is + /// called from this harness. + pub fn register_assigns_contract( + &mut self, + harness_name: InternedString, + contract: AssignsContract, + ) { + let replaced = self.modifies_contracts.insert(harness_name, contract); + assert!( + replaced.is_none(), + "Invariant broken, tried adding second modifies contracts to: {harness_name}", + ) + } + + /// Lookup all CBMC-level `assigns` contract were registered with + /// [`Self::add_assigns_contract`]. + pub fn assigns_contracts(&self) -> impl Iterator { + self.modifies_contracts.iter() + } +} + +struct PrintList(I); + +impl + Clone> Display for PrintList { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + f.write_char('[')?; + let mut is_first = true; + for e in self.0.clone() { + if is_first { + f.write_str(", ")?; + is_first = false; + } + e.fmt(f)?; + } + f.write_char(']') + } } diff --git a/kani-driver/src/call_goto_instrument.rs b/kani-driver/src/call_goto_instrument.rs index 8a97d9e15747..83744eddabfd 100644 --- a/kani-driver/src/call_goto_instrument.rs +++ b/kani-driver/src/call_goto_instrument.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use anyhow::Result; -use std::ffi::OsString; +use std::ffi::{OsStr, OsString}; use std::fs::File; use std::io::BufReader; use std::path::Path; @@ -37,6 +37,8 @@ impl KaniSession { self.goto_sanity_check(output)?; } + self.instrument_contracts(harness, output)?; + if self.args.checks.undefined_function_on() { self.add_library(output)?; self.undefined_functions(output)?; @@ -160,6 +162,23 @@ impl KaniSession { self.call_goto_instrument(args) } + /// Make CBMC enforce a function contract. + pub fn instrument_contracts(&self, harness: &HarnessMetadata, file: &Path) -> Result<()> { + let Some(assigns) = harness.contract.as_ref() else { return Ok(()) }; + + let args: &[std::ffi::OsString] = &[ + "--dfcc".into(), + (&harness.mangled_name).into(), + "--enforce-contract".into(), + assigns.contracted_function_name.as_str().into(), + "--nondet-static-exclude".into(), + assigns.recursion_tracker.as_str().into(), + file.into(), + file.into(), + ]; + self.call_goto_instrument(args) + } + /// Generate a .demangled.c file from the .c file using the `prettyName`s from the symbol table /// /// Currently, only top-level function names and (most) type names are demangled. @@ -189,7 +208,10 @@ impl KaniSession { } /// Non-public helper function to actually do the run of goto-instrument - fn call_goto_instrument(&self, args: Vec) -> Result<()> { + fn call_goto_instrument>( + &self, + args: impl IntoIterator, + ) -> Result<()> { // TODO get goto-instrument path from self let mut cmd = Command::new("goto-instrument"); cmd.args(args); diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 2cd8bb7cbd70..f0a7def68d32 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -57,6 +57,7 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> { let report_dir = self.project.outdir.join(format!("report-{harness_filename}")); let goto_file = self.project.get_harness_artifact(&harness, ArtifactType::Goto).unwrap(); + self.sess.instrument_model(goto_file, goto_file, &self.project, &harness)?; if self.sess.args.synthesize_loop_contracts { diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 871be621c6b0..fabf5dacf3e8 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -184,6 +184,7 @@ pub fn mock_proof_harness( original_end_line: 0, attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() }, goto_file: model_file, + contract: Default::default(), } } diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index df85ca151077..b99a7e9aff07 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -225,6 +225,7 @@ pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result .iter() .map(|artifact| convert_type(&artifact, Metadata, SymTabGoto)) .collect::>(); + session.link_goto_binary(&all_gotos, &goto)?; let goto_artifact = Artifact::try_new(&goto, Goto)?; diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 2356f9bdf42f..3dd6c82ebd39 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -5,6 +5,15 @@ use crate::CbmcSolver; use serde::{Deserialize, Serialize}; use std::path::PathBuf; +/// A CBMC-level `assigns` contract that needs to be enforced on a function. +#[derive(Clone, Debug, Serialize, Deserialize, PartialEq)] +pub struct AssignsContract { + /// The target of the contract + pub contracted_function_name: String, + /// A static global variable used to track recursion that must not be havocked. + pub recursion_tracker: String, +} + /// We emit this structure for each annotated proof harness (`#[kani::proof]`) we find. #[derive(Debug, Clone, Serialize, Deserialize, PartialEq)] pub struct HarnessMetadata { @@ -24,6 +33,8 @@ pub struct HarnessMetadata { pub goto_file: Option, /// The `#[kani::<>]` attributes added to a harness. pub attributes: HarnessAttributes, + /// A CBMC-level assigns contract that should be enforced when running this harness. + pub contract: Option, } /// The attributes added by the user to control how a harness is executed. diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index a211a8ba905c..4f963038cab9 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -118,14 +118,22 @@ //! //! ## Specification Attributes Overview //! -//! There are currently two specification attributes available for describing -//! function behavior: [`requires`][macro@requires] for preconditions and +//! The basic two specification attributes available for describing +//! function behavior are [`requires`][macro@requires] for preconditions and //! [`ensures`][macro@ensures] for postconditions. Both admit arbitrary Rust //! expressions as their bodies which may also reference the function arguments //! but must not mutate memory or perform I/O. The postcondition may //! additionally reference the return value of the function as the variable //! `result`. //! +//! In addition Kani provides the [`modifies`](macro@modifies) attribute. This +//! works a bit different in that it does not contain conditions but a comma +//! separated sequence of expressions that evaluate to pointers. This attribute +//! constrains to which memory locations the function is allowed to write. Each +//! expression can contain arbitrary Rust syntax, though it may not perform side +//! effects and it is also currently unsound if the expression can panic. For more +//! information see the [write sets](#write-sets) section. +//! //! During verified stubbing the return value of a function with a contract is //! replaced by a call to `kani::any`. As such the return value must implement //! the `kani::Arbitrary` trait. @@ -189,4 +197,32 @@ //! If you feel strongly about this issue you can join the discussion on issue //! [#2823](https://github.com/model-checking/kani/issues/2823) to enable //! opt-out of inductive verification. -pub use super::{ensures, proof_for_contract, requires, stub_verified}; +//! +//! ## Write Sets +//! +//! The [`modifies`](macro@modifies) attribute is used to describe which +//! locations in memory a function may assign to. The attribute contains a comma +//! separated series of expressions that reference the function arguments. +//! Syntactically any expression is permissible, though it may not perform side +//! effects (I/O, mutation) or panic. As an example consider this super simple +//! function: +//! +//! ``` +//! #[kani::modifies(ptr, my_box.as_ref())] +//! fn a_function(ptr: &mut u32, my_box: &mut Box) { +//! *ptr = 80; +//! *my_box.as_mut() = 90; +//! } +//! ``` +//! +//! Because the function performs an observable side-effect (setting both the +//! value behind the pointer and the value pointed-to by the box) we need to +//! provide a `modifies` attribute. Otherwise Kani will reject a contract on +//! this function. +//! +//! An expression used in a `modifies` clause must return a pointer to the +//! location that you would like to allow to be modified. This can be any basic +//! Rust pointer type (`&T`, `&mut T`, `*const T` or `*mut T`). In addition `T` +//! must implement [`Arbitrary`](super::Arbitrary). This is used to assign +//! `kani::any()` to the location when the function is used in a `stub_verified`. +pub use super::{ensures, modifies, proof_for_contract, requires, stub_verified}; diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs new file mode 100644 index 000000000000..d2f2970d1c05 --- /dev/null +++ b/library/kani/src/internal.rs @@ -0,0 +1,78 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +/// Helper trait for code generation for `modifies` contracts. +/// +/// We allow the user to provide us with a pointer-like object that we convert as needed. +#[doc(hidden)] +pub trait Pointer<'a> { + /// Type of the pointed-to data + type Inner; + + /// Used for checking assigns contracts where we pass immutable references to the function. + /// + /// We're using a reference to self here, because the user can use just a plain function + /// argument, for instance one of type `&mut _`, in the `modifies` clause which would move it. + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner; + + /// used for havocking on replecement of a `modifies` clause. + unsafe fn assignable(self) -> &'a mut Self::Inner; +} + +impl<'a, 'b, T> Pointer<'a> for &'b T { + type Inner = T; + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + std::mem::transmute(*self) + } + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn assignable(self) -> &'a mut Self::Inner { + std::mem::transmute(self as *const T) + } +} + +impl<'a, 'b, T> Pointer<'a> for &'b mut T { + type Inner = T; + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + std::mem::transmute::<_, &&'a T>(self) + } + + unsafe fn assignable(self) -> &'a mut Self::Inner { + std::mem::transmute(self) + } +} + +impl<'a, T> Pointer<'a> for *const T { + type Inner = T; + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + &**self as &'a T + } + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn assignable(self) -> &'a mut Self::Inner { + std::mem::transmute(self) + } +} + +impl<'a, T> Pointer<'a> for *mut T { + type Inner = T; + unsafe fn decouple_lifetime(&self) -> &'a Self::Inner { + &**self as &'a T + } + + #[allow(clippy::transmute_ptr_to_ref)] + unsafe fn assignable(self) -> &'a mut Self::Inner { + std::mem::transmute(self) + } +} + +/// A way to break the ownerhip rules. Only used by contracts where we can +/// guarantee it is done safely. +#[inline(never)] +#[doc(hidden)] +#[rustc_diagnostic_item = "KaniUntrackedDeref"] +pub fn untracked_deref(_: &T) -> T { + todo!() +} diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index d2959e548417..865344df4d4b 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -25,6 +25,9 @@ pub mod slice; pub mod tuple; pub mod vec; +#[doc(hidden)] +pub mod internal; + mod models; pub use arbitrary::Arbitrary; @@ -92,15 +95,6 @@ macro_rules! implies { }; } -/// A way to break the ownerhip rules. Only used by contracts where we can -/// guarantee it is done safely. -#[inline(never)] -#[doc(hidden)] -#[rustc_diagnostic_item = "KaniUntrackedDeref"] -pub fn untracked_deref(_: &T) -> T { - todo!() -} - /// Creates an assertion of the specified condition and message. /// /// # Example: diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 89482a6266ca..32bd44d2ea38 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -167,6 +167,27 @@ pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::stub_verified(attr, item) } +/// Declaration of an explicit write-set for the annotated function. +/// +/// This is part of the function contract API, for more general information see +/// the [module-level documentation](../kani/contracts/index.html). +/// +/// The contents of the attribute is a series of comma-separated expressions referencing the +/// arguments of the function. Each expression is expected to return a pointer type, i.e. `*const T`, +/// `*mut T`, `&T` or `&mut T`. The pointed-to type must implement +/// [`Arbitrary`](../kani/arbitrary/trait.Arbitrary.html). +/// +/// All Rust syntax is supported, even calling other functions, but the computations must be side +/// effect free, e.g. it cannot perform I/O or use mutable memory. +/// +/// Kani requires each function that uses a contract to have at least one designated +/// [`proof_for_contract`][macro@proof_for_contract] harness for checking the +/// contract. +#[proc_macro_attribute] +pub fn modifies(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::modifies(attr, item) +} + /// This module implements Kani attributes in a way that only Kani's compiler can understand. /// This code should only be activated when pre-building Kani's sysroot. #[cfg(kani_sysroot)] @@ -175,7 +196,7 @@ mod sysroot { mod contracts; - pub use contracts::{ensures, proof_for_contract, requires, stub_verified}; + pub use contracts::{ensures, modifies, proof_for_contract, requires, stub_verified}; use super::*; @@ -348,6 +369,7 @@ mod regular { no_op!(unwind); no_op!(requires); no_op!(ensures); + no_op!(modifies); no_op!(proof_for_contract); no_op!(stub_verified); } diff --git a/library/kani_macros/src/sysroot/contracts.rs b/library/kani_macros/src/sysroot/contracts.rs index a497e0ca8cee..3aeb8c1788d9 100644 --- a/library/kani_macros/src/sysroot/contracts.rs +++ b/library/kani_macros/src/sysroot/contracts.rs @@ -88,7 +88,7 @@ //! ``` //! //! All named arguments of the annotated function are unsafely shallow-copied -//! with the `kani::untracked_deref` function to circumvent the borrow checker +//! with the `kani::internal::untracked_deref` function to circumvent the borrow checker //! for postconditions. The case where this is relevant is if you want to return //! a mutable borrow from the function which means any immutable borrow in the //! postcondition would be illegal. We must ensure that those copies are not @@ -190,8 +190,8 @@ //! #[allow(unused_variables)] //! #[kanitool::is_contract_generated(check)] //! fn div_check_965916(dividend: u32, divisor: u32) -> u32 { -//! let dividend_renamed = kani::untracked_deref(÷nd); -//! let divisor_renamed = kani::untracked_deref(&divisor); +//! let dividend_renamed = kani::internal::untracked_deref(÷nd); +//! let divisor_renamed = kani::internal::untracked_deref(&divisor); //! let result = { kani::assume(divisor != 0); { dividend / divisor } }; //! kani::assert(result <= dividend_renamed, "result <= dividend"); //! std::mem::forget(dividend_renamed); @@ -204,8 +204,8 @@ //! #[kanitool::is_contract_generated(replace)] //! fn div_replace_965916(dividend: u32, divisor: u32) -> u32 { //! kani::assert(divisor != 0, "divisor != 0"); -//! let dividend_renamed = kani::untracked_deref(÷nd); -//! let divisor_renamed = kani::untracked_deref(&divisor); +//! let dividend_renamed = kani::internal::untracked_deref(÷nd); +//! let divisor_renamed = kani::internal::untracked_deref(&divisor); //! let result = kani::any(); //! kani::assume(result <= dividend_renamed, "result <= dividend"); //! std::mem::forget(dividend_renamed); @@ -238,115 +238,63 @@ use std::{ collections::{HashMap, HashSet}, }; use syn::{ - parse_macro_input, spanned::Spanned, visit::Visit, visit_mut::VisitMut, Attribute, Expr, - ItemFn, PredicateType, ReturnType, Signature, TraitBound, TypeParamBound, WhereClause, + parse_macro_input, spanned::Spanned, visit::Visit, visit_mut::VisitMut, Attribute, Expr, FnArg, + ItemFn, PredicateType, ReturnType, Signature, Token, TraitBound, TypeParamBound, WhereClause, }; -/// Create a unique hash for a token stream (basically a [`std::hash::Hash`] -/// impl for `proc_macro2::TokenStream`). -fn hash_of_token_stream(hasher: &mut H, stream: proc_macro2::TokenStream) { - use proc_macro2::TokenTree; - use std::hash::Hash; - for token in stream { - match token { - TokenTree::Ident(i) => i.hash(hasher), - TokenTree::Punct(p) => p.as_char().hash(hasher), - TokenTree::Group(g) => { - std::mem::discriminant(&g.delimiter()).hash(hasher); - hash_of_token_stream(hasher, g.stream()); - } - TokenTree::Literal(lit) => lit.to_string().hash(hasher), - } - } -} - -/// Hash this `TokenStream` and return an integer that is at most digits -/// long when hex formatted. -fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 { - use std::hash::Hasher; - let mut hasher = std::collections::hash_map::DefaultHasher::default(); - hash_of_token_stream(&mut hasher, proc_macro2::TokenStream::from(stream.clone())); - let long_hash = hasher.finish(); - long_hash % 0x1_000_000 // six hex digits -} - -/// Makes consistent names for a generated function which was created for -/// `purpose`, from an attribute that decorates `related_function` with the -/// hash `hash`. -fn identifier_for_generated_function(related_function: &ItemFn, purpose: &str, hash: u64) -> Ident { - let identifier = format!("{}_{purpose}_{hash:x}", related_function.sig.ident); - Ident::new(&identifier, proc_macro2::Span::mixed_site()) -} - +#[allow(dead_code)] pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { - requires_ensures_main(attr, item, true) + requires_ensures_main(attr, item, ContractConditionsType::Requires) } +#[allow(dead_code)] pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { - requires_ensures_main(attr, item, false) + requires_ensures_main(attr, item, ContractConditionsType::Ensures) } -/// Collect all named identifiers used in the argument patterns of a function. -struct ArgumentIdentCollector(HashSet); - -impl ArgumentIdentCollector { - fn new() -> Self { - Self(HashSet::new()) - } +#[allow(dead_code)] +pub fn modifies(attr: TokenStream, item: TokenStream) -> TokenStream { + requires_ensures_main(attr, item, ContractConditionsType::Modifies) } -impl<'ast> Visit<'ast> for ArgumentIdentCollector { - fn visit_pat_ident(&mut self, i: &'ast syn::PatIdent) { - self.0.insert(i.ident.clone()); - syn::visit::visit_pat_ident(self, i) - } - fn visit_receiver(&mut self, _: &'ast syn::Receiver) { - self.0.insert(Ident::new("self", proc_macro2::Span::call_site())); +/// This is very similar to the kani_attribute macro, but it instead creates +/// key-value style attributes which I find a little easier to parse. +macro_rules! passthrough { + ($name:ident, $allow_dead_code:ident) => { + pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { + let args = proc_macro2::TokenStream::from(attr); + let fn_item = proc_macro2::TokenStream::from(item); + let name = Ident::new(stringify!($name), proc_macro2::Span::call_site()); + let extra_attrs = if $allow_dead_code { + quote!(#[allow(dead_code)]) + } else { + quote!() + }; + quote!( + #extra_attrs + #[kanitool::#name = stringify!(#args)] + #fn_item + ) + .into() + } } } -/// Applies the contained renaming (key renamed to value) to every ident pattern -/// and ident expr visited. -struct Renamer<'a>(&'a HashMap); - -impl<'a> VisitMut for Renamer<'a> { - fn visit_expr_path_mut(&mut self, i: &mut syn::ExprPath) { - if i.path.segments.len() == 1 { - i.path - .segments - .first_mut() - .and_then(|p| self.0.get(&p.ident).map(|new| p.ident = new.clone())); - } - } +passthrough!(stub_verified, false); - /// This restores shadowing. Without this we would rename all ident - /// occurrences, but not rebinding location. This is because our - /// [`Self::visit_expr_path_mut`] is scope-unaware. - fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) { - if let Some(new) = self.0.get(&i.ident) { - i.ident = new.clone(); +pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream { + let args = proc_macro2::TokenStream::from(attr); + let ItemFn { attrs, vis, sig, block } = parse_macro_input!(item as ItemFn); + quote!( + #[allow(dead_code)] + #[kanitool::proof_for_contract = stringify!(#args)] + #(#attrs)* + #vis #sig { + let _ = std::boxed::Box::new(0_usize); + #block } - } -} - -/// Does the provided path have the same chain of identifiers as `mtch` (match) -/// and no arguments anywhere? -/// -/// So for instance (using some pseudo-syntax for the [`syn::Path`]s) -/// `matches_path(std::vec::Vec, &["std", "vec", "Vec"]) == true` but -/// `matches_path(std::Vec::::contains, &["std", "Vec", "contains"]) != -/// true`. -/// -/// This is intended to be used to match the internal `kanitool` family of -/// attributes which we know to have a regular structure and no arguments. -fn matches_path(path: &syn::Path, mtch: &[E]) -> bool -where - Ident: std::cmp::PartialEq, -{ - path.segments.len() == mtch.len() - && path.segments.iter().all(|s| s.arguments.is_empty()) - && path.leading_colon.is_none() - && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) + ) + .into() } /// Classifies the state a function is in in the contract handling pipeline. @@ -363,6 +311,7 @@ enum ContractFunctionState { /// This is a replace function that was generated from a previous evaluation /// of a contract attribute. Replace, + ModifiesWrapper, } impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState { @@ -379,6 +328,7 @@ impl<'a> TryFrom<&'a syn::Attribute> for ContractFunctionState { return match ident_str.as_str() { "check" => Ok(Self::Check), "replace" => Ok(Self::Replace), + "wrapper" => Ok(Self::ModifiesWrapper), _ => { Err(Some(lst.span().unwrap().error("Expected `check` or `replace` ident"))) } @@ -419,154 +369,128 @@ impl ContractFunctionState { } } -/// A visitor which injects a copy of the token stream it holds before every -/// `return` expression. -/// -/// This is intended to be used with postconditions and for that purpose it also -/// performs a rewrite where the return value is first bound to `result` so the -/// postconditions can access it. -/// -/// # Example -/// -/// The expression `return x;` turns into -/// -/// ```rs -/// { // Always opens a new block -/// let result = x; -/// -/// return result; -/// } -/// ``` -struct PostconditionInjector(TokenStream2); - -impl VisitMut for PostconditionInjector { - /// We leave this empty to stop the recursion here. We don't want to look - /// inside the closure, because the return statements contained within are - /// for a different function. - fn visit_expr_closure_mut(&mut self, _: &mut syn::ExprClosure) {} - - fn visit_expr_mut(&mut self, i: &mut Expr) { - if let syn::Expr::Return(r) = i { - let tokens = self.0.clone(); - let mut output = TokenStream2::new(); - if let Some(expr) = &mut r.expr { - // In theory the return expression can contain itself a `return` - // so we need to recurse here. - self.visit_expr_mut(expr); - output.extend(quote!(let result = #expr;)); - *expr = Box::new(Expr::Verbatim(quote!(result))); - } - *i = syn::Expr::Verbatim(quote!({ - #output - #tokens - #i - })) - } else { - syn::visit_mut::visit_expr_mut(self, i) - } - } -} - -/// A supporting function for creating shallow, unsafe copies of the arguments -/// for the postconditions. -/// -/// This function: -/// - Collects all [`Ident`]s found in the argument patterns; -/// - Creates new names for them; -/// - Replaces all occurrences of those idents in `attrs` with the new names and; -/// - Returns the mapping of old names to new names. -fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap { - let mut arg_ident_collector = ArgumentIdentCollector::new(); - arg_ident_collector.visit_signature(&sig); - - let mk_new_ident_for = |id: &Ident| Ident::new(&format!("{}_renamed", id), Span::mixed_site()); - let arg_idents = arg_ident_collector - .0 - .into_iter() - .map(|i| { - let new = mk_new_ident_for(&i); - (i, new) - }) - .collect::>(); - - let mut ident_rewriter = Renamer(&arg_idents); - ident_rewriter.visit_expr_mut(attr); - arg_idents -} - /// The information needed to generate the bodies of check and replacement /// functions that integrate the conditions from this contract attribute. struct ContractConditionsHandler<'a> { function_state: ContractFunctionState, /// Information specific to the type of contract attribute we're expanding. - condition_type: ContractConditionsType, - /// The contents of the attribute. - attr: Expr, + condition_type: ContractConditionsData, /// Body of the function this attribute was found on. - annotated_fn: &'a ItemFn, + annotated_fn: &'a mut ItemFn, /// An unparsed, unmodified copy of `attr`, used in the error messages. attr_copy: TokenStream2, /// The stream to which we should write the generated code. output: &'a mut TokenStream2, + hash: Option, } -/// Information needed for generating check and replace handlers for different -/// contract attributes. +/// Which kind of contract attribute are we dealing with? +/// +/// Pre-parsing version of [`ContractConditionsData`]. +#[derive(Copy, Clone, Eq, PartialEq)] enum ContractConditionsType { Requires, + Ensures, + Modifies, +} + +/// Clause-specific information mostly generated by parsing the attribute. +/// +/// [`ContractConditionsType`] is the corresponding pre-parse version. +enum ContractConditionsData { + Requires { + /// The contents of the attribute. + attr: Expr, + }, Ensures { /// Translation map from original argument names to names of the copies /// we will be emitting. argument_names: HashMap, + /// The contents of the attribute. + attr: Expr, + }, + Modifies { + attr: Vec, }, } -impl ContractConditionsType { +impl ContractConditionsData { /// Constructs a [`Self::Ensures`] from the signature of the decorated /// function and the contents of the decorating attribute. /// /// Renames the [`Ident`]s used in `attr` and stores the translation map in /// `argument_names`. - fn new_ensures(sig: &Signature, attr: &mut Expr) -> Self { - let argument_names = rename_argument_occurrences(sig, attr); - ContractConditionsType::Ensures { argument_names } + fn new_ensures(sig: &Signature, mut attr: Expr) -> Self { + let argument_names = rename_argument_occurrences(sig, &mut attr); + ContractConditionsData::Ensures { argument_names, attr } + } + + /// Constructs a [`Self::Modifies`] from the contents of the decorating attribute. + /// + /// Responsible for parsing the attribute. + fn new_modifies(attr: TokenStream, output: &mut TokenStream2) -> Self { + let attr = chunks_by(TokenStream2::from(attr), is_token_stream_2_comma) + .map(syn::parse2) + .filter_map(|expr| match expr { + Err(e) => { + output.extend(e.into_compile_error()); + None + } + Ok(expr) => Some(expr), + }) + .collect(); + + ContractConditionsData::Modifies { attr } } } impl<'a> ContractConditionsHandler<'a> { + fn is_first_emit(&self) -> bool { + matches!(self.function_state, ContractFunctionState::Untouched) + } + /// Initialize the handler. Constructs the required /// [`ContractConditionsType`] depending on `is_requires`. fn new( function_state: ContractFunctionState, - is_requires: bool, - mut attr: Expr, - annotated_fn: &'a ItemFn, + is_requires: ContractConditionsType, + attr: TokenStream, + annotated_fn: &'a mut ItemFn, attr_copy: TokenStream2, output: &'a mut TokenStream2, - ) -> Self { - let condition_type = if is_requires { - ContractConditionsType::Requires - } else { - ContractConditionsType::new_ensures(&annotated_fn.sig, &mut attr) + hash: Option, + ) -> Result { + let condition_type = match is_requires { + ContractConditionsType::Requires => { + ContractConditionsData::Requires { attr: syn::parse(attr)? } + } + ContractConditionsType::Ensures => { + ContractConditionsData::new_ensures(&annotated_fn.sig, syn::parse(attr)?) + } + ContractConditionsType::Modifies => ContractConditionsData::new_modifies(attr, output), }; - Self { function_state, condition_type, attr, annotated_fn, attr_copy, output } + Ok(Self { function_state, condition_type, annotated_fn, attr_copy, output, hash }) } /// Create the body of a check function. /// /// Wraps the conditions from this attribute around `self.body`. - fn make_check_body(&self) -> TokenStream2 { - let Self { attr, attr_copy, .. } = self; - let ItemFn { sig, block, .. } = self.annotated_fn; - let return_type = return_type_to_type(&sig.output); + /// + /// Mutable because a `modifies` clause may need to extend the inner call to + /// the wrapper with new arguments. + fn make_check_body(&mut self) -> TokenStream2 { + let mut inner = self.ensure_bootstrapped_check_body(); + let Self { attr_copy, .. } = self; match &self.condition_type { - ContractConditionsType::Requires => quote!( - kani::assume(#attr); - #block - ), - ContractConditionsType::Ensures { argument_names } => { + ContractConditionsData::Requires { attr } => { + quote!( + kani::assume(#attr); + #(#inner)* + ) + } + ContractConditionsData::Ensures { argument_names, attr } => { let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); // The code that enforces the postconditions and cleans up the shallow @@ -576,21 +500,120 @@ impl<'a> ContractConditionsHandler<'a> { #copy_clean ); - // We make a copy here because we'll modify it. Technically not - // necessary but could lead to weird results if - // `make_replace_body` were called after this if we modified in - // place. - let mut call = block.clone(); - let mut inject_conditions = PostconditionInjector(exec_postconditions.clone()); - inject_conditions.visit_block_mut(&mut call); + assert!(matches!( + inner.pop(), + Some(syn::Stmt::Expr(syn::Expr::Path(pexpr), None)) + if pexpr.path.get_ident().map_or(false, |id| id == "result") + )); quote!( #arg_copies - let result : #return_type = #call; + #(#inner)* #exec_postconditions result ) } + ContractConditionsData::Modifies { attr } => { + let wrapper_name = self.make_wrapper_name().to_string(); + + let wrapper_args = if let Some(wrapper_call_args) = + inner.iter_mut().find_map(|stmt| try_as_wrapper_call_args(stmt, &wrapper_name)) + { + let wrapper_args = make_wrapper_args(wrapper_call_args.len(), attr.len()); + wrapper_call_args + .extend(wrapper_args.clone().map(|a| Expr::Verbatim(quote!(#a)))); + wrapper_args + } else { + unreachable!( + "Invariant broken, check function did not contain a call to the wrapper function" + ) + }; + + quote!( + #(let #wrapper_args = unsafe { kani::internal::Pointer::decouple_lifetime(&#attr) };)* + #(#inner)* + ) + } + } + } + + /// Create a new name for the assigns wrapper function *or* get the name of + /// the wrapper we must have already generated. This is so that we can + /// recognize a call to that wrapper inside the check function. + fn make_wrapper_name(&self) -> Ident { + if let Some(hash) = self.hash { + identifier_for_generated_function(&self.annotated_fn.sig.ident, "wrapper", hash) + } else { + let str_name = self.annotated_fn.sig.ident.to_string(); + let splits = str_name.rsplitn(3, '_').collect::>(); + let [hash, _, base] = splits.as_slice() else { + unreachable!("Odd name for function {str_name}, splits were {}", splits.len()); + }; + + Ident::new(&format!("{base}_wrapper_{hash}"), Span::call_site()) + } + } + + /// Get the sequence of statements of the previous check body or create the default one. + fn ensure_bootstrapped_check_body(&self) -> Vec { + let wrapper_name = self.make_wrapper_name(); + let return_type = return_type_to_type(&self.annotated_fn.sig.output); + if self.is_first_emit() { + let args = exprs_for_args(&self.annotated_fn.sig.inputs); + let wrapper_call = if is_probably_impl_fn(self.annotated_fn) { + quote!(Self::#wrapper_name) + } else { + quote!(#wrapper_name) + }; + syn::parse_quote!( + let result : #return_type = #wrapper_call(#(#args),*); + result + ) + } else { + self.annotated_fn.block.stmts.clone() + } + } + + /// Split an existing replace body of the form + /// + /// ```ignore + /// // multiple preconditions and argument copies like like + /// kani::assert(.. precondition); + /// let arg_name = kani::internal::untracked_deref(&arg_value); + /// // single result havoc + /// let result : ResultType = kani::any(); + /// + /// // multiple argument havockings + /// *unsafe { kani::internal::Pointer::assignable(argument) } = kani::any(); + /// // multiple postconditions + /// kani::assume(postcond); + /// // multiple argument copy (used in postconditions) cleanups + /// std::mem::forget(arg_name); + /// // single return + /// result + /// ``` + /// + /// Such that the first vector contains everything up to and including the single result havoc + /// and the second one the rest, excluding the return. + /// + /// If this is the first time we're emitting replace we create the return havoc and nothing else. + fn ensure_bootstrapped_replace_body(&self) -> (Vec, Vec) { + if self.is_first_emit() { + let return_type = return_type_to_type(&self.annotated_fn.sig.output); + (vec![syn::parse_quote!(let result : #return_type = kani::any();)], vec![]) + } else { + let stmts = &self.annotated_fn.block.stmts; + let idx = stmts + .iter() + .enumerate() + .find_map(|(i, elem)| is_replace_return_havoc(elem).then_some(i)) + .unwrap_or_else(|| { + panic!("ICE: Could not find result let binding in statement sequence") + }); + // We want the result assign statement to end up as the last statement in the first + // vector, hence the `+1`. + let (before, after) = stmts.split_at(idx + 1); + (before.to_vec(), after.split_last().unwrap().1.to_vec()) } } @@ -602,28 +625,38 @@ impl<'a> ContractConditionsHandler<'a> { /// /// `use_nondet_result` will only be true if this is the first time we are /// generating a replace function. - fn make_replace_body(&self, use_nondet_result: bool) -> TokenStream2 { - let Self { attr, attr_copy, .. } = self; - let ItemFn { sig, block, .. } = self.annotated_fn; - let call_to_prior = - if use_nondet_result { quote!(kani::any()) } else { block.to_token_stream() }; - let return_type = return_type_to_type(&sig.output); + fn make_replace_body(&self) -> TokenStream2 { + let (before, after) = self.ensure_bootstrapped_replace_body(); match &self.condition_type { - ContractConditionsType::Requires => quote!( - kani::assert(#attr, stringify!(#attr_copy)); - #call_to_prior - ), - ContractConditionsType::Ensures { argument_names } => { + ContractConditionsData::Requires { attr } => { + let Self { attr_copy, .. } = self; + quote!( + kani::assert(#attr, stringify!(#attr_copy)); + #(#before)* + #(#after)* + result + ) + } + ContractConditionsData::Ensures { attr, argument_names } => { let (arg_copies, copy_clean) = make_unsafe_argument_copies(&argument_names); quote!( #arg_copies - let result: #return_type = #call_to_prior; + #(#before)* + #(#after)* kani::assume(#attr); #copy_clean result ) } + ContractConditionsData::Modifies { attr } => { + quote!( + #(#before)* + #(*unsafe { kani::internal::Pointer::assignable(#attr) } = kani::any();)* + #(#after)* + result + ) + } } } @@ -653,7 +686,7 @@ impl<'a> ContractConditionsHandler<'a> { /// /// See [`Self::make_replace_body`] for the most interesting parts of this /// function. - fn emit_replace_function(&mut self, replace_function_ident: Ident, is_first_emit: bool) { + fn emit_replace_function(&mut self, replace_function_ident: Ident) { self.emit_common_header(); if self.function_state.emit_tag_attr() { @@ -662,10 +695,10 @@ impl<'a> ContractConditionsHandler<'a> { self.output.extend(quote!(#[kanitool::is_contract_generated(replace)])); } let mut sig = self.annotated_fn.sig.clone(); - if is_first_emit { + if self.is_first_emit() { attach_require_kani_any(&mut sig); } - let body = self.make_replace_body(is_first_emit); + let body = self.make_replace_body(); sig.ident = replace_function_ident; // Finally emit the check function itself. @@ -686,6 +719,253 @@ impl<'a> ContractConditionsHandler<'a> { } self.output.extend(self.annotated_fn.attrs.iter().flat_map(Attribute::to_token_stream)); } + + /// Emit a modifies wrapper, possibly augmenting a prior, existing one. + /// + /// We only augment if this clause is a `modifies` clause. In that case we + /// expand its signature with one new argument of type `&impl Arbitrary` for + /// each expression in the clause. + fn emit_augmented_modifies_wrapper(&mut self) { + if let ContractConditionsData::Modifies { attr } = &self.condition_type { + let wrapper_args = make_wrapper_args(self.annotated_fn.sig.inputs.len(), attr.len()); + let sig = &mut self.annotated_fn.sig; + for arg in wrapper_args.clone() { + let lifetime = syn::Lifetime { apostrophe: Span::call_site(), ident: arg.clone() }; + sig.inputs.push(FnArg::Typed(syn::PatType { + attrs: vec![], + colon_token: Token![:](Span::call_site()), + pat: Box::new(syn::Pat::Verbatim(quote!(#arg))), + ty: Box::new(syn::Type::Verbatim(quote!(&#lifetime impl kani::Arbitrary))), + })); + sig.generics.params.push(syn::GenericParam::Lifetime(syn::LifetimeParam { + lifetime, + colon_token: None, + bounds: Default::default(), + attrs: vec![], + })); + } + self.output.extend(quote!(#[kanitool::modifies(#(#wrapper_args),*)])) + } + self.emit_common_header(); + + if self.function_state.emit_tag_attr() { + // If it's the first time we also emit this marker. Again, order is + // important so this happens as the last emitted attribute. + self.output.extend(quote!(#[kanitool::is_contract_generated(wrapper)])); + } + + let name = self.make_wrapper_name(); + let ItemFn { vis, sig, block, .. } = self.annotated_fn; + + let mut sig = sig.clone(); + sig.ident = name; + self.output.extend(quote!( + #vis #sig #block + )); + } +} + +/// Used as the "single source of truth" for [`try_as_result_assign`] and [`try_as_result_assign_mut`] +/// since we can't abstract over mutability. Input is the object to match on and the name of the +/// function used to convert an `Option` into the result type (e.g. `as_ref` and `as_mut` +/// respectively). +/// +/// We start with a `match` as a top-level here, since if we made this a pattern macro (the "clean" +/// thing to do) then we cant use the `if` inside there which we need because box patterns are +/// unstable. +macro_rules! try_as_result_assign_pat { + ($input:expr, $convert:ident) => { + match $input { + syn::Stmt::Local(syn::Local { + pat: syn::Pat::Type(syn::PatType { + pat: inner_pat, + attrs, + .. + }), + init, + .. + }) if attrs.is_empty() + && matches!( + inner_pat.as_ref(), + syn::Pat::Ident(syn::PatIdent { + by_ref: None, + mutability: None, + ident: result_ident, + subpat: None, + .. + }) if result_ident == "result" + ) => init.$convert(), + _ => None, + } + }; +} + +/// Try to parse this statement as `let result : <...> = ;` and return `init`. +/// +/// This is the shape of statement we create in replace functions to havoc (with `init` being +/// `kani::any()`) and we need to recognize it for when we edit the replace function and integrate +/// additional conditions. +/// +/// It's a thin wrapper around [`try_as_result_assign_pat!`] to create an immutable match. +fn try_as_result_assign(stmt: &syn::Stmt) -> Option<&syn::LocalInit> { + try_as_result_assign_pat!(stmt, as_ref) +} + +/// Try to parse this statement as `let result : <...> = ;` and return a mutable reference to +/// `init`. +/// +/// This is the shape of statement we create in check functions (with `init` being a call to check +/// function with additional pointer arguments for the `modifies` clause) and we need to recognize +/// it to then edit this call if we find another `modifies` clause and add its additional arguments. +/// additional conditions. +/// +/// It's a thin wrapper around [`try_as_result_assign_pat!`] to create a mutable match. +fn try_as_result_assign_mut(stmt: &mut syn::Stmt) -> Option<&mut syn::LocalInit> { + try_as_result_assign_pat!(stmt, as_mut) +} + +/// Is this statement `let result : <...> = kani::any();`. +fn is_replace_return_havoc(stmt: &syn::Stmt) -> bool { + let Some(syn::LocalInit { diverge: None, expr: e, .. }) = try_as_result_assign(stmt) else { + return false; + }; + + matches!( + e.as_ref(), + Expr::Call(syn::ExprCall { + func, + args, + .. + }) + if args.is_empty() + && matches!( + func.as_ref(), + Expr::Path(syn::ExprPath { + qself: None, + path, + attrs, + }) + if path.segments.len() == 2 + && path.segments[0].ident == "kani" + && path.segments[1].ident == "any" + && attrs.is_empty() + ) + ) +} + +/// For each argument create an expression that passes this argument along unmodified. +/// +/// Reconstructs structs that may have been deconstructed with patterns. +fn exprs_for_args( + args: &syn::punctuated::Punctuated, +) -> impl Iterator + Clone + '_ { + args.iter().map(|arg| match arg { + FnArg::Receiver(_) => Expr::Verbatim(quote!(self)), + FnArg::Typed(typed) => pat_to_expr(&typed.pat), + }) +} + +/// Create an expression that reconstructs a struct that was matched in a pattern. +/// +/// Does not support enums, wildcards, pattern alternatives (`|`), range patterns, or verbatim. +fn pat_to_expr(pat: &syn::Pat) -> Expr { + use syn::Pat; + let mk_err = |typ| { + pat.span() + .unwrap() + .error(format!("`{typ}` patterns are not supported for functions with contracts")) + .emit(); + unreachable!() + }; + match pat { + Pat::Const(c) => Expr::Const(c.clone()), + Pat::Ident(id) => Expr::Verbatim(id.ident.to_token_stream()), + Pat::Lit(lit) => Expr::Lit(lit.clone()), + Pat::Reference(rf) => Expr::Reference(syn::ExprReference { + attrs: vec![], + and_token: rf.and_token, + mutability: rf.mutability, + expr: Box::new(pat_to_expr(&rf.pat)), + }), + Pat::Tuple(tup) => Expr::Tuple(syn::ExprTuple { + attrs: vec![], + paren_token: tup.paren_token, + elems: tup.elems.iter().map(pat_to_expr).collect(), + }), + Pat::Slice(slice) => Expr::Reference(syn::ExprReference { + attrs: vec![], + and_token: syn::Token!(&)(Span::call_site()), + mutability: None, + expr: Box::new(Expr::Array(syn::ExprArray { + attrs: vec![], + bracket_token: slice.bracket_token, + elems: slice.elems.iter().map(pat_to_expr).collect(), + })), + }), + Pat::Path(pth) => Expr::Path(pth.clone()), + Pat::Or(_) => mk_err("or"), + Pat::Rest(_) => mk_err("rest"), + Pat::Wild(_) => mk_err("wildcard"), + Pat::Paren(inner) => pat_to_expr(&inner.pat), + Pat::Range(_) => mk_err("range"), + Pat::Struct(strct) => { + if strct.rest.is_some() { + mk_err(".."); + } + Expr::Struct(syn::ExprStruct { + attrs: vec![], + path: strct.path.clone(), + brace_token: strct.brace_token, + dot2_token: None, + rest: None, + qself: strct.qself.clone(), + fields: strct + .fields + .iter() + .map(|field_pat| syn::FieldValue { + attrs: vec![], + member: field_pat.member.clone(), + colon_token: field_pat.colon_token, + expr: pat_to_expr(&field_pat.pat), + }) + .collect(), + }) + } + Pat::Verbatim(_) => mk_err("verbatim"), + Pat::Type(pt) => pat_to_expr(pt.pat.as_ref()), + Pat::TupleStruct(_) => mk_err("tuple struct"), + _ => mk_err("unknown"), + } +} + +/// Try to interpret this statement as `let result : <...> = (args ...);` and +/// return a mutable reference to the parameter list. +fn try_as_wrapper_call_args<'a>( + stmt: &'a mut syn::Stmt, + wrapper_fn_name: &str, +) -> Option<&'a mut syn::punctuated::Punctuated> { + let syn::LocalInit { diverge: None, expr: init_expr, .. } = try_as_result_assign_mut(stmt)? + else { + return None; + }; + + match init_expr.as_mut() { + Expr::Call(syn::ExprCall { func: box_func, args, .. }) => match box_func.as_ref() { + syn::Expr::Path(syn::ExprPath { qself: None, path, .. }) + if path.get_ident().map_or(false, |id| id == wrapper_fn_name) => + { + Some(args) + } + _ => None, + }, + _ => None, + } +} + +/// Make `num` [`Ident`]s with the names `_wrapper_arg_{i}` with `i` starting at `low` and +/// increasing by one each time. +fn make_wrapper_args(low: usize, num: usize) -> impl Iterator + Clone { + (low..).map(|i| Ident::new(&format!("_wrapper_arg_{i}"), Span::mixed_site())).take(num) } /// If an explicit return type was provided it is returned, otherwise `()`. @@ -762,7 +1042,7 @@ fn make_unsafe_argument_copies( let also_arg_names = renaming_map.values(); let arg_values = renaming_map.keys(); ( - quote!(#(let #arg_names = kani::untracked_deref(&#arg_values);)*), + quote!(#(let #arg_names = kani::internal::untracked_deref(&#arg_values);)*), quote!(#(std::mem::forget(#also_arg_names);)*), ) } @@ -771,13 +1051,16 @@ fn make_unsafe_argument_copies( /// /// See the [module level documentation][self] for a description of how the code /// generation works. -fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool) -> TokenStream { +fn requires_ensures_main( + attr: TokenStream, + item: TokenStream, + is_requires: ContractConditionsType, +) -> TokenStream { let attr_copy = TokenStream2::from(attr.clone()); - let attr = parse_macro_input!(attr as Expr); let mut output = proc_macro2::TokenStream::new(); let item_stream_clone = item.clone(); - let item_fn = parse_macro_input!(item as ItemFn); + let mut item_fn = parse_macro_input!(item as ItemFn); let function_state = ContractFunctionState::from_attributes(&item_fn.attrs); @@ -793,16 +1076,26 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool return item_fn.into_token_stream().into(); } - let mut handler = ContractConditionsHandler::new( + let hash = matches!(function_state, ContractFunctionState::Untouched) + .then(|| short_hash_of_token_stream(&item_stream_clone)); + + let original_function_name = item_fn.sig.ident.clone(); + + let mut handler = match ContractConditionsHandler::new( function_state, is_requires, attr, - &item_fn, + &mut item_fn, attr_copy, &mut output, - ); + hash, + ) { + Ok(handler) => handler, + Err(e) => return e.into_compile_error().into(), + }; match function_state { + ContractFunctionState::ModifiesWrapper => handler.emit_augmented_modifies_wrapper(), ContractFunctionState::Check => { // The easy cases first: If we are on a check or replace function // emit them again but with additional conditions layered on. @@ -810,11 +1103,11 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool // Since we are already on the check function, it will have an // appropriate, unique generated name which we are just going to // pass on. - handler.emit_check_function(item_fn.sig.ident.clone()); + handler.emit_check_function(original_function_name); } ContractFunctionState::Replace => { // Analogous to above - handler.emit_replace_function(item_fn.sig.ident.clone(), false); + handler.emit_replace_function(original_function_name); } ContractFunctionState::Original => { unreachable!("Impossible: This is handled via short circuiting earlier.") @@ -832,12 +1125,17 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool // We'll be using this to postfix the generated names for the "check" // and "replace" functions. - let item_hash = short_hash_of_token_stream(&item_stream_clone); - - let check_fn_name = identifier_for_generated_function(&item_fn, "check", item_hash); - let replace_fn_name = identifier_for_generated_function(&item_fn, "replace", item_hash); - let recursion_wrapper_name = - identifier_for_generated_function(&item_fn, "recursion_wrapper", item_hash); + let item_hash = hash.unwrap(); + + let check_fn_name = + identifier_for_generated_function(&original_function_name, "check", item_hash); + let replace_fn_name = + identifier_for_generated_function(&original_function_name, "replace", item_hash); + let recursion_wrapper_name = identifier_for_generated_function( + &original_function_name, + "recursion_wrapper", + item_hash, + ); // Constructing string literals explicitly here, because `stringify!` // doesn't work. Let's say we have an identifier `check_fn` and we were @@ -847,6 +1145,8 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool // instead the *expression* `stringify!(check_fn)`. let replace_fn_name_str = syn::LitStr::new(&replace_fn_name.to_string(), Span::call_site()); + let wrapper_fn_name_str = + syn::LitStr::new(&handler.make_wrapper_name().to_string(), Span::call_site()); let recursion_wrapper_name_str = syn::LitStr::new(&recursion_wrapper_name.to_string(), Span::call_site()); @@ -858,12 +1158,13 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool // // The same care is taken when we emit check and replace functions. // emit the check function. - let is_impl_fn = is_probably_impl_fn(&item_fn); - let ItemFn { attrs, vis, sig, block } = &item_fn; + let is_impl_fn = is_probably_impl_fn(&handler.annotated_fn); + let ItemFn { attrs, vis, sig, block } = &handler.annotated_fn; handler.output.extend(quote!( #(#attrs)* #[kanitool::checked_with = #recursion_wrapper_name_str] #[kanitool::replaced_with = #replace_fn_name_str] + #[kanitool::inner_check = #wrapper_fn_name_str] #vis #sig { #block } @@ -898,7 +1199,8 @@ fn requires_ensures_main(attr: TokenStream, item: TokenStream, is_requires: bool )); handler.emit_check_function(check_fn_name); - handler.emit_replace_function(replace_fn_name, true); + handler.emit_replace_function(replace_fn_name); + handler.emit_augmented_modifies_wrapper(); } } @@ -996,31 +1298,160 @@ fn is_probably_impl_fn(fun: &ItemFn) -> bool { self_detector.0 } -/// This is very similar to the kani_attribute macro, but it instead creates -/// key-value style attributes which I find a little easier to parse. -macro_rules! passthrough { - ($name:ident, $allow_dead_code:ident) => { - pub fn $name(attr: TokenStream, item: TokenStream) -> TokenStream { - let args = proc_macro2::TokenStream::from(attr); - let fn_item = proc_macro2::TokenStream::from(item); - let name = Ident::new(stringify!($name), proc_macro2::Span::call_site()); - let extra_attrs = if $allow_dead_code { - quote!(#[allow(dead_code)]) +/// Create a unique hash for a token stream (basically a [`std::hash::Hash`] +/// impl for `proc_macro2::TokenStream`). +fn hash_of_token_stream(hasher: &mut H, stream: proc_macro2::TokenStream) { + use proc_macro2::TokenTree; + use std::hash::Hash; + for token in stream { + match token { + TokenTree::Ident(i) => i.hash(hasher), + TokenTree::Punct(p) => p.as_char().hash(hasher), + TokenTree::Group(g) => { + std::mem::discriminant(&g.delimiter()).hash(hasher); + hash_of_token_stream(hasher, g.stream()); + } + TokenTree::Literal(lit) => lit.to_string().hash(hasher), + } + } +} + +/// Hash this `TokenStream` and return an integer that is at most digits +/// long when hex formatted. +fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 { + const SIX_HEX_DIGITS_MASK: u64 = 0x1_000_000; + use std::hash::Hasher; + let mut hasher = std::collections::hash_map::DefaultHasher::default(); + hash_of_token_stream(&mut hasher, proc_macro2::TokenStream::from(stream.clone())); + let long_hash = hasher.finish(); + long_hash % SIX_HEX_DIGITS_MASK +} + +/// Makes consistent names for a generated function which was created for +/// `purpose`, from an attribute that decorates `related_function` with the +/// hash `hash`. +fn identifier_for_generated_function( + related_function_name: &Ident, + purpose: &str, + hash: u64, +) -> Ident { + let identifier = format!("{}_{purpose}_{hash:x}", related_function_name); + Ident::new(&identifier, proc_macro2::Span::mixed_site()) +} + +fn is_token_stream_2_comma(t: &proc_macro2::TokenTree) -> bool { + matches!(t, proc_macro2::TokenTree::Punct(p) if p.as_char() == ',') +} + +fn chunks_by<'a, T, C: Default + Extend>( + i: impl IntoIterator + 'a, + mut pred: impl FnMut(&T) -> bool + 'a, +) -> impl Iterator + 'a { + let mut iter = i.into_iter(); + std::iter::from_fn(move || { + let mut new = C::default(); + let mut empty = true; + for tok in iter.by_ref() { + empty = false; + if pred(&tok) { + break; } else { - quote!() - }; - quote!( - #extra_attrs - #[kanitool::#name = stringify!(#args)] - #fn_item - ) - .into() + new.extend([tok]) + } } + (!empty).then_some(new) + }) +} + +/// Collect all named identifiers used in the argument patterns of a function. +struct ArgumentIdentCollector(HashSet); + +impl ArgumentIdentCollector { + fn new() -> Self { + Self(HashSet::new()) } } -passthrough!(stub_verified, false); -passthrough!(proof_for_contract, true); +impl<'ast> Visit<'ast> for ArgumentIdentCollector { + fn visit_pat_ident(&mut self, i: &'ast syn::PatIdent) { + self.0.insert(i.ident.clone()); + syn::visit::visit_pat_ident(self, i) + } + fn visit_receiver(&mut self, _: &'ast syn::Receiver) { + self.0.insert(Ident::new("self", proc_macro2::Span::call_site())); + } +} + +/// Applies the contained renaming (key renamed to value) to every ident pattern +/// and ident expr visited. +struct Renamer<'a>(&'a HashMap); + +impl<'a> VisitMut for Renamer<'a> { + fn visit_expr_path_mut(&mut self, i: &mut syn::ExprPath) { + if i.path.segments.len() == 1 { + i.path + .segments + .first_mut() + .and_then(|p| self.0.get(&p.ident).map(|new| p.ident = new.clone())); + } + } + + /// This restores shadowing. Without this we would rename all ident + /// occurrences, but not rebinding location. This is because our + /// [`Self::visit_expr_path_mut`] is scope-unaware. + fn visit_pat_ident_mut(&mut self, i: &mut syn::PatIdent) { + if let Some(new) = self.0.get(&i.ident) { + i.ident = new.clone(); + } + } +} + +/// A supporting function for creating shallow, unsafe copies of the arguments +/// for the postconditions. +/// +/// This function: +/// - Collects all [`Ident`]s found in the argument patterns; +/// - Creates new names for them; +/// - Replaces all occurrences of those idents in `attrs` with the new names and; +/// - Returns the mapping of old names to new names. +fn rename_argument_occurrences(sig: &syn::Signature, attr: &mut Expr) -> HashMap { + let mut arg_ident_collector = ArgumentIdentCollector::new(); + arg_ident_collector.visit_signature(&sig); + + let mk_new_ident_for = |id: &Ident| Ident::new(&format!("{}_renamed", id), Span::mixed_site()); + let arg_idents = arg_ident_collector + .0 + .into_iter() + .map(|i| { + let new = mk_new_ident_for(&i); + (i, new) + }) + .collect::>(); + + let mut ident_rewriter = Renamer(&arg_idents); + ident_rewriter.visit_expr_mut(attr); + arg_idents +} + +/// Does the provided path have the same chain of identifiers as `mtch` (match) +/// and no arguments anywhere? +/// +/// So for instance (using some pseudo-syntax for the [`syn::Path`]s) +/// `matches_path(std::vec::Vec, &["std", "vec", "Vec"]) == true` but +/// `matches_path(std::Vec::::contains, &["std", "Vec", "contains"]) != +/// true`. +/// +/// This is intended to be used to match the internal `kanitool` family of +/// attributes which we know to have a regular structure and no arguments. +fn matches_path(path: &syn::Path, mtch: &[E]) -> bool +where + Ident: std::cmp::PartialEq, +{ + path.segments.len() == mtch.len() + && path.segments.iter().all(|s| s.arguments.is_empty()) + && path.leading_colon.is_none() + && path.segments.iter().zip(mtch).all(|(actual, expected)| actual.ident == *expected) +} #[cfg(test)] mod test { diff --git a/tests/expected/function-contract/modifies/expr_pass.expected b/tests/expected/function-contract/modifies/expr_pass.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/modifies/expr_pass.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/expr_pass.rs b/tests/expected/function-contract/modifies/expr_pass.rs new file mode 100644 index 000000000000..65e561df48a2 --- /dev/null +++ b/tests/expected/function-contract/modifies/expr_pass.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Test that a modifies clause works when a (function call) +// expression is provided + +#[kani::requires(**ptr < 100)] +#[kani::modifies(ptr.as_ref())] +#[kani::ensures(**ptr < 101)] +fn modify(ptr: &mut Box) { + *ptr.as_mut() += 1; +} + +#[kani::proof_for_contract(modify)] +fn main() { + let mut i = Box::new(kani::any()); + modify(&mut i); +} diff --git a/tests/expected/function-contract/modifies/expr_replace_fail.expected b/tests/expected/function-contract/modifies/expr_replace_fail.expected new file mode 100644 index 000000000000..f8019df2927c --- /dev/null +++ b/tests/expected/function-contract/modifies/expr_replace_fail.expected @@ -0,0 +1,7 @@ +main.assertion\ +- Status: FAILURE\ +- Description: ""Increment"" + +Failed Checks: "Increment" + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/expr_replace_fail.rs b/tests/expected/function-contract/modifies/expr_replace_fail.rs new file mode 100644 index 000000000000..09fa840d8696 --- /dev/null +++ b/tests/expected/function-contract/modifies/expr_replace_fail.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Tests that providing the "modifies" clause havocks the pointer such +// that the increment can no longer be observed (in the absence of an +// "ensures" clause) + +#[kani::requires(**ptr < 100)] +#[kani::modifies(ptr.as_ref())] +fn modify(ptr: &mut Box) { + *ptr.as_mut() += 1; +} + +#[kani::proof] +#[kani::stub_verified(modify)] +fn main() { + let val = kani::any_where(|i| *i < 100); + let mut i = Box::new(val); + modify(&mut i); + assert!(*i == val + 1, "Increment"); +} diff --git a/tests/expected/function-contract/modifies/expr_replace_pass.expected b/tests/expected/function-contract/modifies/expr_replace_pass.expected new file mode 100644 index 000000000000..405875334763 --- /dev/null +++ b/tests/expected/function-contract/modifies/expr_replace_pass.expected @@ -0,0 +1,5 @@ +main.assertion\ +- Status: SUCCESS\ +- Description: "Increment"\ + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/expr_replace_pass.rs b/tests/expected/function-contract/modifies/expr_replace_pass.rs new file mode 100644 index 000000000000..8be1ef2cbaee --- /dev/null +++ b/tests/expected/function-contract/modifies/expr_replace_pass.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::requires(**ptr < 100)] +#[kani::modifies(ptr.as_ref())] +#[kani::ensures(**ptr == prior + 1)] +fn modify(ptr: &mut Box, prior: u32) { + *ptr.as_mut() += 1; +} + +#[kani::proof] +#[kani::stub_verified(modify)] +fn main() { + let val = kani::any_where(|i| *i < 100); + let mut i = Box::new(val); + modify(&mut i, val); + kani::assert(*i == val + 1, "Increment"); +} diff --git a/tests/expected/function-contract/modifies/field_pass.expected b/tests/expected/function-contract/modifies/field_pass.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/modifies/field_pass.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/field_pass.rs b/tests/expected/function-contract/modifies/field_pass.rs new file mode 100644 index 000000000000..997f67474350 --- /dev/null +++ b/tests/expected/function-contract/modifies/field_pass.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +struct S<'a> { + distraction: usize, + target: &'a mut u32, +} +#[kani::requires(*s.target < 100)] +#[kani::modifies(s.target)] +fn modify(s: S) { + *s.target += 1; +} + +#[kani::proof_for_contract(modify)] +fn main() { + let mut i = kani::any(); + let s = S { distraction: 0, target: &mut i }; + modify(s); +} diff --git a/tests/expected/function-contract/modifies/field_replace_fail.expected b/tests/expected/function-contract/modifies/field_replace_fail.expected new file mode 100644 index 000000000000..91643c68b3c5 --- /dev/null +++ b/tests/expected/function-contract/modifies/field_replace_fail.expected @@ -0,0 +1,7 @@ +main.assertion\ +- Status: FAILURE\ +- Description: "Increment havocked" + +Failed Checks: Increment havocked + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/field_replace_fail.rs b/tests/expected/function-contract/modifies/field_replace_fail.rs new file mode 100644 index 000000000000..261e4ebd4974 --- /dev/null +++ b/tests/expected/function-contract/modifies/field_replace_fail.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +struct S<'a> { + distraction: usize, + target: &'a mut u32, +} +#[kani::requires(*s.target < 100)] +#[kani::modifies(s.target)] +fn modify(s: S) { + *s.target += 1; +} + +#[kani::proof] +#[kani::stub_verified(modify)] +fn main() { + let mut i = kani::any_where(|i| *i < 100); + let i_copy = i; + let s = S { distraction: 0, target: &mut i }; + modify(s); + kani::assert(i == i_copy + 1, "Increment havocked"); +} diff --git a/tests/expected/function-contract/modifies/field_replace_pass.expected b/tests/expected/function-contract/modifies/field_replace_pass.expected new file mode 100644 index 000000000000..64dedf3f511a --- /dev/null +++ b/tests/expected/function-contract/modifies/field_replace_pass.expected @@ -0,0 +1,9 @@ +main.assertion\ +- Status: SUCCESS\ +- Description: "Increment"\ + +main.assertion\ +- Status: SUCCESS\ +- Description: "Unchanged" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/field_replace_pass.rs b/tests/expected/function-contract/modifies/field_replace_pass.rs new file mode 100644 index 000000000000..a6ae4ea4a7e0 --- /dev/null +++ b/tests/expected/function-contract/modifies/field_replace_pass.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +struct S<'a> { + distraction: &'a mut u32, + target: &'a mut u32, +} +#[kani::requires(*s.target < 100)] +#[kani::modifies(s.target)] +#[kani::ensures(*s.target == prior + 1)] +fn modify(s: S, prior: u32) { + *s.target += 1; +} + +#[kani::proof] +#[kani::stub_verified(modify)] +fn main() { + let mut i = kani::any_where(|i| *i < 100); + let i_copy = i; + let mut distraction = kani::any(); + let distraction_copy = distraction; + let s = S { distraction: &mut distraction, target: &mut i }; + modify(s, i_copy); + kani::assert(i == i_copy + 1, "Increment"); + kani::assert(distraction == distraction_copy, "Unchanged"); +} diff --git a/tests/expected/function-contract/modifies/global_fail.expected b/tests/expected/function-contract/modifies/global_fail.expected new file mode 100644 index 000000000000..04e0359ad8a4 --- /dev/null +++ b/tests/expected/function-contract/modifies/global_fail.expected @@ -0,0 +1,9 @@ +assigns\ +- Status: FAILURE\ +- Description: "Check that *var_1 is assignable"\ +in function modify_wrapper + +Failed Checks: Check that *var_1 is assignable\ +in modify_wrapper + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/global_fail.rs b/tests/expected/function-contract/modifies/global_fail.rs new file mode 100644 index 000000000000..48c095a4964e --- /dev/null +++ b/tests/expected/function-contract/modifies/global_fail.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +static mut PTR: u32 = 0; + +#[kani::requires(PTR < 100)] +unsafe fn modify() { + PTR += 1; +} + +#[kani::proof_for_contract(modify)] +fn main() { + unsafe { + modify(); + } +} diff --git a/tests/expected/function-contract/modifies/global_pass.expected b/tests/expected/function-contract/modifies/global_pass.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/modifies/global_pass.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/global_pass.rs b/tests/expected/function-contract/modifies/global_pass.rs new file mode 100644 index 000000000000..f4579c0b5e29 --- /dev/null +++ b/tests/expected/function-contract/modifies/global_pass.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +static mut PTR: u32 = 0; + +#[kani::requires(PTR < 100)] +#[kani::modifies(&mut PTR)] +unsafe fn modify() { + PTR += 1; +} + +#[kani::proof_for_contract(modify)] +fn main() { + unsafe { + modify(); + } +} diff --git a/tests/expected/function-contract/modifies/global_replace_fail.expected b/tests/expected/function-contract/modifies/global_replace_fail.expected new file mode 100644 index 000000000000..8c0761731a4b --- /dev/null +++ b/tests/expected/function-contract/modifies/global_replace_fail.expected @@ -0,0 +1,8 @@ +main.assertion\ +- Status: FAILURE\ +- Description: "not havocked"\ +in function main + +Failed Checks: not havocked + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/global_replace_fail.rs b/tests/expected/function-contract/modifies/global_replace_fail.rs new file mode 100644 index 000000000000..25169918b120 --- /dev/null +++ b/tests/expected/function-contract/modifies/global_replace_fail.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +static mut PTR: u32 = 0; + +#[kani::requires(PTR < 100)] +#[kani::modifies(&mut PTR)] +unsafe fn modify() { + PTR += 1; +} + +#[kani::proof] +#[kani::stub_verified(modify)] +fn main() { + unsafe { + PTR = kani::any_where(|i| *i < 100); + let compare = PTR; + modify(); + kani::assert(compare + 1 == PTR, "not havocked"); + } +} diff --git a/tests/expected/function-contract/modifies/global_replace_pass.expected b/tests/expected/function-contract/modifies/global_replace_pass.expected new file mode 100644 index 000000000000..164f00c88d22 --- /dev/null +++ b/tests/expected/function-contract/modifies/global_replace_pass.expected @@ -0,0 +1,6 @@ +main.assertion\ +- Status: SUCCESS\ +- Description: "replaced"\ +in function main + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/global_replace_pass.rs b/tests/expected/function-contract/modifies/global_replace_pass.rs new file mode 100644 index 000000000000..333348f25ce4 --- /dev/null +++ b/tests/expected/function-contract/modifies/global_replace_pass.rs @@ -0,0 +1,22 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +static mut PTR: u32 = 0; + +#[kani::modifies(&mut PTR)] +#[kani::ensures(PTR == src)] +unsafe fn modify(src: u32) { + PTR = src; +} + +#[kani::proof] +#[kani::stub_verified(modify)] +fn main() { + unsafe { + PTR = kani::any(); + let new = kani::any(); + modify(new); + kani::assert(new == PTR, "replaced"); + } +} diff --git a/tests/expected/function-contract/modifies/havoc_pass.expected b/tests/expected/function-contract/modifies/havoc_pass.expected new file mode 100644 index 000000000000..02ce972ef370 --- /dev/null +++ b/tests/expected/function-contract/modifies/havoc_pass.expected @@ -0,0 +1,38 @@ +copy_replace.assertion\ +- Status: SUCCESS\ +- Description: "equality"\ +in function copy_replace + +VERIFICATION:- SUCCESSFUL + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that var_4 is assignable"\ +in function copy + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that var_3 is assignable"\ +in function copy\ + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that var_5 is assignable"\ +in function copy + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that *var_5 is assignable"\ +in function copy\ + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that var_7 is assignable"\ +in function copy + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that *var_7 is assignable"\ +in function copy + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/havoc_pass.rs b/tests/expected/function-contract/modifies/havoc_pass.rs new file mode 100644 index 000000000000..aa5bcada1a26 --- /dev/null +++ b/tests/expected/function-contract/modifies/havoc_pass.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::modifies(dst)] +#[kani::ensures(*dst == src)] +fn copy(src: u32, dst: &mut u32) { + *dst = src; +} + +#[kani::proof_for_contract(copy)] +fn copy_harness() { + copy(kani::any(), &mut kani::any()); +} + +#[kani::proof] +#[kani::stub_verified(copy)] +fn copy_replace() { + let src = kani::any(); + let mut dst = kani::any(); + copy(src, &mut dst); + kani::assert(src == dst, "equality"); +} diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.expected b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected new file mode 100644 index 000000000000..02ce972ef370 --- /dev/null +++ b/tests/expected/function-contract/modifies/havoc_pass_reordered.expected @@ -0,0 +1,38 @@ +copy_replace.assertion\ +- Status: SUCCESS\ +- Description: "equality"\ +in function copy_replace + +VERIFICATION:- SUCCESSFUL + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that var_4 is assignable"\ +in function copy + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that var_3 is assignable"\ +in function copy\ + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that var_5 is assignable"\ +in function copy + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that *var_5 is assignable"\ +in function copy\ + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that var_7 is assignable"\ +in function copy + +copy.assigns\ +- Status: SUCCESS\ +- Description: "Check that *var_7 is assignable"\ +in function copy + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/havoc_pass_reordered.rs b/tests/expected/function-contract/modifies/havoc_pass_reordered.rs new file mode 100644 index 000000000000..dc5f370179e5 --- /dev/null +++ b/tests/expected/function-contract/modifies/havoc_pass_reordered.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// These two are reordered in comparison to `havoc_pass` and we expect the test case to pass still +#[kani::ensures(*dst == src)] +#[kani::modifies(dst)] +fn copy(src: u32, dst: &mut u32) { + *dst = src; +} + +#[kani::proof_for_contract(copy)] +fn copy_harness() { + copy(kani::any(), &mut kani::any()); +} + +#[kani::proof] +#[kani::stub_verified(copy)] +fn copy_replace() { + let src = kani::any(); + let mut dst = kani::any(); + copy(src, &mut dst); + kani::assert(src == dst, "equality"); +} diff --git a/tests/expected/function-contract/modifies/refcell_fixme.rs b/tests/expected/function-contract/modifies/refcell_fixme.rs new file mode 100644 index 000000000000..8ae9cb390eb7 --- /dev/null +++ b/tests/expected/function-contract/modifies/refcell_fixme.rs @@ -0,0 +1,13 @@ +use std::cell::RefCell; +use std::ops::Deref; + +#[kani::modifies(cell.borrow().deref())] +fn modifies_ref_cell(cell: &RefCell) { + *cell.borrow_mut() = 100; +} + +#[kani::proof_for_contract(modifies_ref_cell)] +fn check_harness() { + let rc = RefCell::new(0); + modifies_ref_cell(&rc); +} diff --git a/tests/expected/function-contract/modifies/simple_fail.expected b/tests/expected/function-contract/modifies/simple_fail.expected new file mode 100644 index 000000000000..ffaee2293931 --- /dev/null +++ b/tests/expected/function-contract/modifies/simple_fail.expected @@ -0,0 +1,7 @@ +assigns\ +- Status: FAILURE\ +- Description: "Check that *ptr is assignable" + +Failed Checks: Check that *ptr is assignable + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/modifies/simple_fail.rs b/tests/expected/function-contract/modifies/simple_fail.rs new file mode 100644 index 000000000000..8d1b16e9a976 --- /dev/null +++ b/tests/expected/function-contract/modifies/simple_fail.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::requires(*ptr < 100)] +fn modify(ptr: &mut u32) { + *ptr += 1; +} + +#[kani::proof_for_contract(modify)] +fn main() { + let mut i = kani::any(); + modify(&mut i); +} diff --git a/tests/expected/function-contract/modifies/simple_pass.expected b/tests/expected/function-contract/modifies/simple_pass.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/modifies/simple_pass.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/simple_pass.rs b/tests/expected/function-contract/modifies/simple_pass.rs new file mode 100644 index 000000000000..3c90ef8c789f --- /dev/null +++ b/tests/expected/function-contract/modifies/simple_pass.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::requires(*ptr < 100)] +#[kani::modifies(ptr)] +fn modify(ptr: &mut u32) { + *ptr += 1; +} + +#[kani::proof_for_contract(modify)] +fn main() { + let mut i = kani::any(); + modify(&mut i); +} diff --git a/tests/expected/function-contract/modifies/stmt_expr.expected b/tests/expected/function-contract/modifies/stmt_expr.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/modifies/stmt_expr.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/stmt_expr.rs b/tests/expected/function-contract/modifies/stmt_expr.rs new file mode 100644 index 000000000000..f8e7f9e4a836 --- /dev/null +++ b/tests/expected/function-contract/modifies/stmt_expr.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::requires(**ptr < 100)] +#[kani::modifies({ + let r = ptr.as_ref(); + r +})] +fn modify(ptr: &mut Box) { + *ptr.as_mut() += 1; +} + +#[kani::proof_for_contract(modify)] +fn main() { + let mut i = Box::new(kani::any()); + modify(&mut i); +} diff --git a/tests/expected/function-contract/modifies/unique_arguments.expected b/tests/expected/function-contract/modifies/unique_arguments.expected new file mode 100644 index 000000000000..d84097d648e9 --- /dev/null +++ b/tests/expected/function-contract/modifies/unique_arguments.expected @@ -0,0 +1,9 @@ +test_stubbing.assertion\ +- Status: SUCCESS\ +- Description: "a is 1" + +test_stubbing.assertion\ +- Status: SUCCESS\ +- Description: "b is 2" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/unique_arguments.rs b/tests/expected/function-contract/modifies/unique_arguments.rs new file mode 100644 index 000000000000..396ba4c5b036 --- /dev/null +++ b/tests/expected/function-contract/modifies/unique_arguments.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::modifies(a)] +#[kani::modifies(b)] +#[kani::ensures(*a == 1)] +#[kani::ensures(*b == 2)] +fn two_pointers(a: &mut u32, b: &mut u32) { + *a = 1; + *b = 2; +} + +#[kani::proof_for_contract(two_pointers)] +fn test_contract() { + two_pointers(&mut kani::any(), &mut kani::any()); +} + +#[kani::proof] +#[kani::stub_verified(two_pointers)] +fn test_stubbing() { + let mut a = kani::any(); + let mut b = kani::any(); + + two_pointers(&mut a, &mut b); + + kani::assert(a == 1, "a is 1"); + kani::assert(b == 2, "b is 2"); +} diff --git a/tests/expected/function-contract/modifies/unsafe_rc_fixme.rs b/tests/expected/function-contract/modifies/unsafe_rc_fixme.rs new file mode 100644 index 000000000000..81cc65ce9957 --- /dev/null +++ b/tests/expected/function-contract/modifies/unsafe_rc_fixme.rs @@ -0,0 +1,33 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +use std::ops::Deref; +/// Illustrates the problem from https://github.com/model-checking/kani/issues/2907 +use std::rc::Rc; + +#[kani::modifies({ + let intref : &u32 = ptr.deref().deref(); + intref +})] +fn modify(ptr: Rc<&mut u32>) { + unsafe { + **(Rc::as_ptr(&ptr) as *mut &mut u32) = 1; + } +} + +#[kani::proof_for_contract(modify)] +fn main() { + let mut i: u32 = kani::any(); + let ptr = Rc::new(&mut i); + modify(ptr.clone()); +} + +#[kani::proof] +#[kani::stub_verified(modify)] +fn replace_modify() { + let begin = kani::any_where(|i| *i < 100); + let i = Rc::new(RefCell::new(begin)); + modify(i.clone()); + kani::assert(*i.borrow() == begin + 1, "end"); +} diff --git a/tests/expected/function-contract/modifies/vec_pass.expected b/tests/expected/function-contract/modifies/vec_pass.expected new file mode 100644 index 000000000000..d31486f2dcc6 --- /dev/null +++ b/tests/expected/function-contract/modifies/vec_pass.expected @@ -0,0 +1,20 @@ +modify.assertion\ +- Status: SUCCESS\ +- Description: "v.len() > 0"\ +in function modify + +modify_replace.assertion\ +- Status: SUCCESS\ +- Description: "element set"\ +in function modify_replace + +modify_replace.assertion\ +- Status: SUCCESS\ +- Description: "vector tail equality"\ +in function modify_replace + +assertion\ +- Status: SUCCESS\ +- Description: "v[0] == src" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/vec_pass.rs b/tests/expected/function-contract/modifies/vec_pass.rs new file mode 100644 index 000000000000..1e40a2a08eb7 --- /dev/null +++ b/tests/expected/function-contract/modifies/vec_pass.rs @@ -0,0 +1,34 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +#[kani::requires(v.len() > 0)] +#[kani::modifies(&v[0])] +#[kani::ensures(v[0] == src)] +fn modify(v: &mut Vec, src: u32) { + v[0] = src +} + +#[kani::unwind(10)] +#[kani::proof_for_contract(modify)] +fn main() { + let v_len = kani::any_where(|i| *i < 4); + let mut v: Vec = vec![kani::any()]; + for _ in 0..v_len { + v.push(kani::any()); + } + modify(&mut v, kani::any()); +} + +#[kani::unwind(10)] +#[kani::proof] +#[kani::stub_verified(modify)] +fn modify_replace() { + let v_len = kani::any_where(|i| *i < 4 && *i > 0); + let mut v: Vec = vec![kani::any(); v_len].to_vec(); + let compare = v[1..].to_vec(); + let src = kani::any(); + modify(&mut v, src); + kani::assert(v[0] == src, "element set"); + kani::assert(compare == v[1..v_len], "vector tail equality"); +}