new compilation phase

kani-compiler/src/kani_middle/transform/contracts.rs

@@ -166,3 +166,94 @@ impl AnyModifiesPass {
  }
  }
 }
+
+/// Check if we can replace calls to havoc.
+///
+/// This pass will replace the entire body, and it should only be applied to stubs
+/// that have a body.
+#[derive(Debug)]
+pub struct HavocPass {
+ kani_any_modifies: Option<FnDef>,
+ kani_havoc: Option<FnDef>,
+ stubbed: HashSet<DefId>,
+ target_fn: Option<InternedString>,
+}
+
+impl TransformPass for HavocPass {
+ fn transformation_type() -> TransformationType
+ where
+ Self: Sized,
+ {
+ TransformationType::Stubbing
+ }
+
+ fn is_enabled(&self, query_db: &QueryDb) -> bool
+ where
+ Self: Sized,
+ {
+ // TODO: Check if this is the harness has proof_for_contract
+ query_db.args().unstable_features.contains(&"function-contracts".to_string())
+ }
+
+ /// Transform the function body by replacing it with the stub body.
+ fn transform(&self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+ trace!(function=?instance.name(), "HavocPass::transform");
+
+ if self.should_apply(tcx, instance) { self.replace_havoc(body) } else { (false, body) }
+ }
+}
+
+impl HavocPass {
+ /// Build the pass with non-extern function stubs.
+ pub fn new(tcx: TyCtxt, unit: &CodegenUnit) -> HavocPass {
+ 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_havoc = tcx
+ .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavoc"))
+ .map(item_fn_def);
+ let kani_any_modifies = tcx
+ .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies"))
+ .map(item_fn_def);
+ let (target_fn, stubbed) = if let Some(harness) = unit.harnesses.first() {
+ let attributes = KaniAttributes::for_instance(tcx, *harness);
+ let target_fn =
+ attributes.proof_for_contract().map(|symbol| symbol.unwrap().as_str().intern());
+ (target_fn, unit.stubs.keys().map(|from| from.def_id()).collect::<HashSet<_>>())
+ } else {
+ (None, HashSet::new())
+ };
+ HavocPass { kani_any_modifies, kani_havoc, target_fn, stubbed }
+ }
+
+ fn should_apply(&self, tcx: TyCtxt, instance: Instance) -> bool {
+ let item_attributes =
+ KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, instance.def.def_id()));
+ self.stubbed.contains(&instance.def.def_id()) || item_attributes.has_recursion()
+ }
+
+ /// Replace calls to `any_modifies` by calls to `any`.
+ fn replace_havoc(&self, mut body: Body) -> (bool, Body) {
+ let mut changed = false;
+ let locals = body.locals().to_vec();
+ for bb in body.blocks.iter_mut() {
+ let TerminatorKind::Call { func, args, .. } = &mut bb.terminator.kind else { continue };
+ if let TyKind::RigidTy(RigidTy::FnDef(def, instance_args)) =
+ func.ty(&locals).unwrap().kind()
+ && Some(def) == self.kani_havoc
+ {
+ if args.len() != 1 {
+ panic!("kani::havoc should have exactly one arg")
+ }
+ // TODO: create an MIR bb to replace bb with the proper stuff
+ // changed = true;
+ }
+ }
+ (changed, body)
+ }
+}

kani-compiler/src/kani_middle/transform/mod.rs

@@ -19,7 +19,7 @@
 use crate::kani_middle::codegen_units::CodegenUnit;
 use crate::kani_middle::transform::body::CheckType;
 use crate::kani_middle::transform::check_values::ValidValuePass;
-use crate::kani_middle::transform::contracts::AnyModifiesPass;
+use crate::kani_middle::transform::contracts::{AnyModifiesPass, HavocPass};
 use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass;
 use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass};
 use crate::kani_queries::QueryDb;
@@ -62,6 +62,7 @@ impl BodyTransformation {
  transformer.add_pass(queries, FnStubPass::new(&unit.stubs));
  transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs));
  // This has to come after stubs since we want this to replace the stubbed body.
+ transformer.add_pass(queries, HavocPass::new(tcx, &unit));
  transformer.add_pass(queries, AnyModifiesPass::new(tcx, &unit));
  transformer.add_pass(queries, ValidValuePass { check_type: check_type.clone() });
  transformer.add_pass(queries, IntrinsicGeneratorPass { check_type });

library/kani/src/internal.rs

@@ -14,108 +14,66 @@ pub trait Pointer<'a> {
  /// 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 fill_any(self);
 }
 
-impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b T {
+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 fill_any(self) {
- *std::mem::transmute::<*const T, &mut T>(self as *const T) = crate::any();
- }
 }
 
-impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b mut 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 fill_any(self) {
- *std::mem::transmute::<&mut T, &mut T>(self) = crate::any();
- }
 }
 
-impl<'a, T: crate::Arbitrary> Pointer<'a> for *const T {
+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 fill_any(self) {
- *std::mem::transmute::<*const T, &mut T>(self) = crate::any();
- }
 }
 
-impl<'a, T: crate::Arbitrary> Pointer<'a> for *mut T {
+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 fill_any(self) {
- *std::mem::transmute::<*mut T, &mut T>(self) = crate::any();
- }
 }
 
-impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b [T] {
+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 fill_any(self) {
- std::mem::transmute::<*const [T], &mut [T]>(self as *const [T])
- .fill_with(|| crate::any::<T>());
- }
 }
 
-impl<'a, 'b, T: crate::Arbitrary> Pointer<'a> for &'b mut [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 fill_any(self) {
- std::mem::transmute::<&mut [T], &mut [T]>(self).fill_with(|| crate::any::<T>());
- }
 }
 
-impl<'a, T: crate::Arbitrary> Pointer<'a> for *const [T] {
+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 fill_any(self) {
- std::mem::transmute::<*const [T], &mut [T]>(self).fill_with(|| crate::any::<T>());
- }
 }
 
-impl<'a, T: crate::Arbitrary> Pointer<'a> for *mut [T] {
+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 fill_any(self) {
- std::mem::transmute::<*mut [T], &mut [T]>(self).fill_with(|| crate::any::<T>());
- }
 }
 
 /// A way to break the ownerhip rules. Only used by contracts where we can

library/kani/src/lib.rs

@@ -180,6 +180,20 @@ pub fn any_modifies<T>() -> T {
  unreachable!()
 }
 
+/// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object.
+/// Only for use within function contracts and will not be replaced if the recursive or function stub
+/// replace contracts are not used.
+#[rustc_diagnostic_item = "KaniHavoc"]
+#[inline(never)]
+#[doc(hidden)]
+pub fn havoc<T>(_pointer: &T) {
+ // This function should not be reacheable.
+ // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
+ // otherwise, this might not be properly instantiate. We mark this as unreachable to make
+ // sure Kani doesn't report any false positives.
+ unreachable!()
+}
+
 /// This creates a symbolic *valid* value of type `T`.
 /// The value is constrained to be a value accepted by the predicate passed to the filter.
 /// You can assign the return value of this function to a variable that you want to make symbolic.

library/kani_macros/src/sysroot/contracts/replace.rs

@@ -94,7 +94,7 @@ impl<'a> ContractConditionsHandler<'a> {
  let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
  quote!(
  #(#before)*
- #(unsafe {kani::internal::Pointer::fill_any(kani::internal::untracked_deref(&#attr))};)*
+ #(kani::havoc(&#attr);)*
  #(#after)*
  #result
  )