diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index 4d6bab5ca2a3..b210b2c9333e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -17,8 +17,8 @@ impl<'tcx> GotocCtx<'tcx> { /// 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. + /// 1. Gets the `#[kanitool::modifies_wrapper = "..."]` target, then resolves exactly one + /// instance of it. Panics if there are more or less than one instance. /// 2. The additional arguments for the inner checks are locations that may be modified. /// Add them to the list of CBMC's assigns. /// 3. Returns the mangled name of the symbol it attached the contract to. @@ -107,13 +107,13 @@ impl<'tcx> GotocCtx<'tcx> { None }) }; - let outside_check = if contract_attrs.has_recursion { - find_closure(instance, contract_attrs.recursion_check.as_str())? + let check_instance = if contract_attrs.has_recursion { + let recursion_check = find_closure(instance, contract_attrs.recursion_check.as_str())?; + find_closure(recursion_check, contract_attrs.checked_with.as_str())? } else { - instance + find_closure(instance, contract_attrs.checked_with.as_str())? }; - let check = find_closure(outside_check, contract_attrs.checked_with.as_str())?; - find_closure(check, contract_attrs.inner_check.as_str()) + find_closure(check_instance, contract_attrs.modifies_wrapper.as_str()) } /// Convert the Kani level contract into a CBMC level contract by creating a diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 6a1af75f3643..19cbba59cb83 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -54,12 +54,12 @@ enum KaniAttributeKind { /// Attribute on a function that was auto-generated from expanding a /// function contract. IsContractGenerated, - /// A function used as the inner code of a contract check. + /// A function with contract expanded to include the write set as arguments. /// /// 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, + ModifiesWrapper, /// Attribute used to mark contracts for functions with recursion. /// We use this attribute to properly instantiate `kani::any_modifies` in /// cases when recursion is present given our contracts instrumentation. @@ -92,7 +92,7 @@ impl KaniAttributeKind { | KaniAttributeKind::ReplacedWith | KaniAttributeKind::RecursionCheck | KaniAttributeKind::CheckedWith - | KaniAttributeKind::InnerCheck + | KaniAttributeKind::ModifiesWrapper | KaniAttributeKind::IsContractGenerated | KaniAttributeKind::DisableChecks => false, } @@ -134,7 +134,7 @@ pub struct ContractAttributes { /// The name of the contract replacement. pub replaced_with: Symbol, /// The name of the inner check used to modify clauses. - pub inner_check: Symbol, + pub modifies_wrapper: Symbol, } impl<'tcx> std::fmt::Debug for KaniAttributes<'tcx> { @@ -262,13 +262,13 @@ impl<'tcx> KaniAttributes<'tcx> { let recursion_check = self.attribute_value(KaniAttributeKind::RecursionCheck); let checked_with = self.attribute_value(KaniAttributeKind::CheckedWith); let replace_with = self.attribute_value(KaniAttributeKind::ReplacedWith); - let inner_check = self.attribute_value(KaniAttributeKind::InnerCheck); + let modifies_wrapper = self.attribute_value(KaniAttributeKind::ModifiesWrapper); let total = recursion_check .iter() .chain(&checked_with) .chain(&replace_with) - .chain(&inner_check) + .chain(&modifies_wrapper) .count(); if total != 0 && total != 4 { self.tcx.sess.dcx().err(format!( @@ -282,7 +282,7 @@ impl<'tcx> KaniAttributes<'tcx> { recursion_check: recursion_check?, checked_with: checked_with?, replaced_with: replace_with?, - inner_check: inner_check?, + modifies_wrapper: modifies_wrapper?, }) } @@ -373,7 +373,7 @@ impl<'tcx> KaniAttributes<'tcx> { } KaniAttributeKind::FnMarker | KaniAttributeKind::CheckedWith - | KaniAttributeKind::InnerCheck + | KaniAttributeKind::ModifiesWrapper | KaniAttributeKind::RecursionCheck | KaniAttributeKind::ReplacedWith => { self.attribute_value(kind); @@ -505,7 +505,7 @@ impl<'tcx> KaniAttributes<'tcx> { } KaniAttributeKind::CheckedWith | KaniAttributeKind::IsContractGenerated - | KaniAttributeKind::InnerCheck + | KaniAttributeKind::ModifiesWrapper | KaniAttributeKind::RecursionCheck | KaniAttributeKind::RecursionTracker | KaniAttributeKind::ReplacedWith => { diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 2d1a34d49a2f..71e06f5c49cd 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -78,31 +78,12 @@ impl TransformPass for AnyModifiesPass { impl AnyModifiesPass { /// Build the pass with non-extern function stubs. pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> AnyModifiesPass { - let item_fn_def = |item| { - let TyKind::RigidTy(RigidTy::FnDef(def, _)) = - rustc_internal::stable(tcx.type_of(item)).value.kind() - else { - unreachable!("Expected function, but found `{:?}`", tcx.def_path_str(item)) - }; - def - }; - let kani_any = - tcx.get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAny")).map(item_fn_def); - let kani_any_modifies = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies")) - .map(item_fn_def); - let kani_write_any = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAny")) - .map(item_fn_def); - let kani_write_any_slim = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnySlim")) - .map(item_fn_def); - let kani_write_any_slice = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnySlice")) - .map(item_fn_def); - let kani_write_any_str = tcx - .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniWriteAnyStr")) - .map(item_fn_def); + let kani_any = find_fn_def(tcx, "KaniAny"); + let kani_any_modifies = find_fn_def(tcx, "KaniAnyModifies"); + let kani_write_any = find_fn_def(tcx, "KaniWriteAny"); + let kani_write_any_slim = find_fn_def(tcx, "KaniWriteAnySlim"); + let kani_write_any_slice = find_fn_def(tcx, "KaniWriteAnySlice"); + let kani_write_any_str = find_fn_def(tcx, "KaniWriteAnyStr"); let target_fn = if let Some(harness) = unit.harnesses.first() { let attributes = KaniAttributes::for_instance(tcx, *harness); let target_fn = @@ -242,7 +223,7 @@ impl AnyModifiesPass { /// #[kanitool::recursion_check = "__kani_recursion_check_modify"] /// #[kanitool::checked_with = "__kani_check_modify"] /// #[kanitool::replaced_with = "__kani_replace_modify"] -/// #[kanitool::inner_check = "__kani_modifies_modify"] +/// #[kanitool::modifies_wrapper = "__kani_modifies_modify"] /// fn name_fn(ptr: &mut u32) { /// #[kanitool::fn_marker = "kani_register_contract"] /// pub const fn kani_register_contract T>(f: F) -> T { @@ -289,6 +270,8 @@ pub struct FunctionWithContractPass { /// are not to be used in this harness. /// In order to avoid bringing unnecessary logic, we clear their body. unused_closures: HashSet, + /// Cache KaniRunContract function used to implement contracts. + run_contract_fn: Option, } impl TransformPass for FunctionWithContractPass { @@ -318,8 +301,7 @@ impl TransformPass for FunctionWithContractPass { } else if KaniAttributes::for_instance(tcx, instance).fn_marker() == Some(Symbol::intern("kani_register_contract")) { - let run = Instance::resolve(find_fn_def(tcx, "KaniRunContract").unwrap(), args) - .unwrap(); + let run = Instance::resolve(self.run_contract_fn.unwrap(), args).unwrap(); (true, run.body().unwrap()) } else { // Not a contract annotated function @@ -357,9 +339,17 @@ impl FunctionWithContractPass { .iter() .map(|(_, def_id, _)| *def_id) .collect(); - FunctionWithContractPass { check_fn, replace_fns, unused_closures: Default::default() } + let run_contract_fn = find_fn_def(tcx, "KaniRunContract"); + assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function"); + FunctionWithContractPass { + check_fn, + replace_fns, + unused_closures: Default::default(), + run_contract_fn, + } } else { - // Building the model for tests or public functions. + // If reachability mode is PubFns or Tests, we just remove any contract logic. + // Note that in this path there is no proof harness. FunctionWithContractPass::default() } } diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index 56eddc657eb3..68b15316b4c1 100644 --- a/library/kani/src/internal.rs +++ b/library/kani/src/internal.rs @@ -49,7 +49,7 @@ impl Pointer for *mut T { /// A way to break the ownerhip rules. Only used by contracts where we can /// guarantee it is done safely. /// TODO: Remove this! This is not safe. Users should be able to use `ptr::read` and `old` if -/// they really need to. +/// they really need to. See . #[inline(never)] #[doc(hidden)] #[rustc_diagnostic_item = "KaniUntrackedDeref"] diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index f7f150570ae3..8ad21e8a9c6b 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -41,7 +41,7 @@ impl<'a> ContractConditionsHandler<'a> { #[kanitool::recursion_check = #recursion_name] #[kanitool::checked_with = #check_name] #[kanitool::replaced_with = #replace_name] - #[kanitool::inner_check = #modifies_name] + #[kanitool::modifies_wrapper = #modifies_name] #vis #sig { // Dummy function used to force the compiler to capture the environment. // We cannot call closures inside constant functions. diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index ef7b88dc87d1..c7c7a4bb1598 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -10,7 +10,7 @@ //! implements a state machine in order to be able to handle multiple attributes //! on the same function correctly. //! -//! ## How the handling for `requires` and `ensures` works. +//! ## How the handling for `requires`, `modifies`, and `ensures` works. //! //! Our aim is to generate a "check" function that can be used to verify the //! validity of the contract and a "replace" function that can be used as a @@ -31,49 +31,20 @@ //! addition, we also want to make sure to support non-contract attributes on //! functions with contracts. //! -//! To this end we use a state machine with two states. The initial state is an "untouched" -//! function with possibly multiple contract attributes, none of which have been -//! expanded. When we expand the first (outermost) contract -//! attribute on such a function we re-emit the function with a few closures defined -//! in their body, which correspond to the "check", "recursive" and "replace" that enforce the -//! condition carried by the attribute currently being expanded. -//! -//! We also add new marker attributes to the original function to -//! advance the state machine. The re-emitted original meanwhile is decorated with -//! `kanitool::checked_with(name_of_generated_check_variable)` and an analogous -//! `kanittool::replaced_with` attribute also. -//! Each closure gets a `kanitool::is_contract_generated()` attributes. -//! The next contract attribute that -//! is expanded will detect the presence of these markers in the attributes of -//! the item and be able to determine their position in the state machine this -//! way. -//! -//! Subsequent run, will expand the existing definitions with the condition being processed. +//! To this end we generate attributes in a two-phase approach: initial and subsequent expansions. +//! +//! The initial expansion modifies the original function to contains all necessary instrumentation +//! contracts need to be analyzed. It will do the following: +//! 1. Annotate the function with extra `kanitool` attributes +//! 2. Generate closures for each contract processing scenario (recursive check, simple check, +//! replacement, and regular execution). +//! +//! Subsequent expansions will detect the existence of the extra `kanitool` attributes, +//! and they will only expand the body of the closures generated in the initial phase. //! //! Note: We place marker attributes at the bottom of the attribute stack (innermost), //! otherwise they would not be visible to the future macro expansions. //! -//! Below you can see a graphical rendering where boxes are states and each -//! arrow represents the expansion of a `requires` or `ensures` macro. -//! -//! ```plain -//! │ Start -//! ▼ -//! ┌───────────┐ -//! │ Untouched │ -//! │ Function │ -//! └─────┬─────┘ -//! │ -//! │ Annotate original + generate closures -//! │ -//! ▼ -//! ┌──────────┐ -//! │ Original │◄─┐ -//! └──┬───────┘ │ -//! │ │ Expand -//! └──────────┘ closures -//! ``` -//! //! ## Check closure //! //! Generates a `__kani__check` closure that assumes preconditions @@ -160,7 +131,7 @@ //! #[kanitool::recursion_check = "__kani_recursion_check_div"] //! #[kanitool::checked_with = "__kani_check_div"] //! #[kanitool::replaced_with = "__kani_replace_div"] -//! #[kanitool::inner_check = "__kani_modifies_div"] +//! #[kanitool::modifies_wrapper = "__kani_modifies_div"] //! fn div(dividend: u32, divisor: u32) -> u32 { //! #[inline(never)] //! #[kanitool::fn_marker = "kani_register_contract"] @@ -293,7 +264,7 @@ //! #[kanitool::recursion_check = "__kani_recursion_check_modify"] //! #[kanitool::checked_with = "__kani_check_modify"] //! #[kanitool::replaced_with = "__kani_replace_modify"] -//! #[kanitool::inner_check = "__kani_modifies_modify"] +//! #[kanitool::modifies_wrapper = "__kani_modifies_modify"] //! fn modify(ptr: &mut u32) { //! #[inline(never)] //! #[kanitool::fn_marker = "kani_register_contract"]