Address PR comments

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

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 => {

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: FnOnce() -> 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<ClosureDef>,
+ /// Cache KaniRunContract function used to implement contracts.
+ run_contract_fn: Option<FnDef>,
 }
 
 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()
  }
  }

library/kani/src/internal.rs

@@ -49,7 +49,7 @@ impl<T: ?Sized> 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 <https://github.com/model-checking/kani/issues/3293>.
 #[inline(never)]
 #[doc(hidden)]
 #[rustc_diagnostic_item = "KaniUntrackedDeref"]

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.

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(<KIND>)` 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_<fn_name>_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"]