diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index f5760bd4d829..4c54ad33b53d 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/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, + kani_havoc: Option, + stubbed: HashSet, + target_fn: Option, +} + +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::>()) + } 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) + } +} diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 8d5c61f55c92..b6ea0f582e69 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/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 }); diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs index b35a74c29343..d09a86ad804f 100644 --- a/library/kani/src/internal.rs +++ b/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::()); - } } -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::()); - } } -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::()); - } } -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::()); - } } /// A way to break the ownerhip rules. Only used by contracts where we can diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index acf1e08e0441..00c5a944e24b 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -180,6 +180,20 @@ pub fn any_modifies() -> 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(_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. diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 07c4e06ffbd1..b2c08f902224 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/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 )