hack

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

@@ -11,7 +11,7 @@ use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Body, ConstOperand, Operand, TerminatorKind};
-use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
+use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind, TypeAndMut};
 use stable_mir::{CrateDef, DefId};
 use std::collections::HashSet;
 use std::fmt::Debug;
@@ -25,6 +25,10 @@ use tracing::{debug, trace};
 pub struct AnyModifiesPass {
     kani_any: Option<FnDef>,
     kani_any_modifies: Option<FnDef>,
+    kani_havoc: Option<FnDef>,
+    kani_havoc_slim: Option<FnDef>,
+    kani_havoc_slice: Option<FnDef>,
+    kani_havoc_str: Option<FnDef>,
     stubbed: HashSet<DefId>,
     target_fn: Option<InternedString>,
 }
@@ -78,6 +82,18 @@ impl AnyModifiesPass {
         let kani_any_modifies = tcx
             .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniAnyModifies"))
             .map(item_fn_def);
+        let kani_havoc = tcx
+            .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavoc"))
+            .map(item_fn_def);
+        let kani_havoc_slim = tcx
+            .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavocSlim"))
+            .map(item_fn_def);
+        let kani_havoc_slice = tcx
+            .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavocSlice"))
+            .map(item_fn_def);
+        let kani_havoc_str = tcx
+            .get_diagnostic_item(rustc_span::symbol::Symbol::intern("KaniHavocStr"))
+            .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 =
@@ -86,7 +102,16 @@ impl AnyModifiesPass {
         } else {
             (None, HashSet::new())
         };
-        AnyModifiesPass { kani_any, kani_any_modifies, target_fn, stubbed }
+        AnyModifiesPass {
+            kani_any,
+            kani_any_modifies,
+            kani_havoc,
+            kani_havoc_slim,
+            kani_havoc_slice,
+            kani_havoc_str,
+            target_fn,
+            stubbed,
+        }
     }
 
     /// If we apply `transform_any_modifies` in all contract-generated items,
@@ -105,7 +130,7 @@ impl AnyModifiesPass {
         let mut changed = false;
         let locals = body.locals().to_vec();
         for bb in body.blocks.iter_mut() {
-            let TerminatorKind::Call { func, .. } = &mut bb.terminator.kind else { continue };
+            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_any_modifies
@@ -117,6 +142,39 @@ impl AnyModifiesPass {
                 *func = Operand::Constant(new_func);
                 changed = true;
             }
+
+            if let TyKind::RigidTy(RigidTy::FnDef(def, instance_args)) =
+                func.ty(&locals).unwrap().kind()
+                && Some(def) == self.kani_havoc
+                && args.len() == 1
+                && let Some(fn_sig) = func.ty(&locals).unwrap().kind().fn_sig()
+                && let Some(TypeAndMut { ty: internal_type, mutability: _ }) =
+                    fn_sig.skip_binder().inputs()[0].kind().builtin_deref(true)
+            {
+                if let TyKind::RigidTy(RigidTy::Slice(_)) = internal_type.kind() {
+                    let instance =
+                        Instance::resolve(self.kani_havoc_slice.unwrap(), &instance_args).unwrap();
+                    let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
+                    let span = bb.terminator.span;
+                    let new_func = ConstOperand { span, user_ty: None, const_: literal };
+                    *func = Operand::Constant(new_func);
+                } else if let TyKind::RigidTy(RigidTy::Str) = internal_type.kind() {
+                    let instance =
+                        Instance::resolve(self.kani_havoc_str.unwrap(), &instance_args).unwrap();
+                    let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
+                    let span = bb.terminator.span;
+                    let new_func = ConstOperand { span, user_ty: None, const_: literal };
+                    *func = Operand::Constant(new_func);
+                } else {
+                    let instance =
+                        Instance::resolve(self.kani_havoc_slim.unwrap(), &instance_args).unwrap();
+                    let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
+                    let span = bb.terminator.span;
+                    let new_func = ConstOperand { span, user_ty: None, const_: literal };
+                    *func = Operand::Constant(new_func);
+                }
+                changed = true;
+            }
         }
         (changed, body)
     }
@@ -166,94 +224,3 @@ 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, HavocPass};
+use crate::kani_middle::transform::contracts::AnyModifiesPass;
 use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass;
 use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass};
 use crate::kani_queries::QueryDb;
@@ -62,7 +62,6 @@ 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,65 +14,56 @@ 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;
+
+    unsafe fn assignable(self) -> &'a mut Self::Inner;
 }
 
-impl<'a, 'b, T> Pointer<'a> for &'b T {
+impl<'a, 'b, T: ?Sized> 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 {
+impl<'a, 'b, T: ?Sized> 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)
     }
-}
 
-impl<'a, T> Pointer<'a> for *const T {
-    type Inner = T;
-    unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-        &**self as &'a T
+    unsafe fn assignable(self) -> &'a mut Self::Inner {
+        std::mem::transmute(self)
     }
 }
 
-impl<'a, T> Pointer<'a> for *mut T {
+impl<'a, T: ?Sized> Pointer<'a> for *const T {
     type Inner = T;
     unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
         &**self as &'a 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)
-    }
-}
-
-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];
+impl<'a, T: ?Sized> Pointer<'a> for *mut T {
+    type Inner = T;
     unsafe fn decouple_lifetime(&self) -> &'a Self::Inner {
-        &**self as &'a [T]
+        &**self as &'a 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 assignable(self) -> &'a mut Self::Inner {
+        std::mem::transmute(self)
     }
 }
 

library/kani/src/lib.rs

@@ -186,14 +186,32 @@ pub fn any_modifies<T>() -> T {
 #[rustc_diagnostic_item = "KaniHavoc"]
 #[inline(never)]
 #[doc(hidden)]
-pub fn havoc<T>(_pointer: &T) {
+pub fn havoc<T: ?Sized>(_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!()
 }
 
+#[rustc_diagnostic_item = "KaniHavocSlice"]
+#[inline(always)]
+pub fn havoc_slice<T: Arbitrary>(slice: &mut [T]) {
+    slice.fill_with(|| T::any())
+}
+
+#[rustc_diagnostic_item = "KaniHavocSlim"]
+#[inline(always)]
+pub fn havoc_slim<T: Arbitrary>(pointer: &mut T) {
+    *pointer = T::any()
+}
+
+#[rustc_diagnostic_item = "KaniHavocStr"]
+#[inline(always)]
+pub fn havoc_str(s: &mut str) {
+    todo!()
+}
+
 /// 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)*
-                    #(kani::havoc(&#attr);)*
+                    #(kani::havoc(unsafe{kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr))});)*
                     #(#after)*
                     #result
                 )

tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.expected

@@ -1,5 +1,5 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\
+- Description: "|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\
 
 VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/modifies_fat_pointer/nondeterministic_size.rs

@@ -5,7 +5,7 @@
 // Test that modifies a slice of nondeterministic size
 
 #[kani::modifies(x)]
-#[kani::ensures(|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b))]
+#[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))]
 fn zero(x: &mut [u8]) {
     x.fill(0)
 }

tests/expected/function-contract/modifies_fat_pointer/u32slice.expected

@@ -1,5 +1,5 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\
+- Description: "|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\
 
 VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/modifies_fat_pointer/u32slice.rs

@@ -5,7 +5,7 @@
 // Test that modifies a slice containing bytesize data
 
 #[kani::modifies(x)]
-#[kani::ensures(|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b))]
+#[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))]
 fn zero(x: &mut [u32]) {
     x.fill(0)
 }

tests/expected/function-contract/modifies_fat_pointer/u8slice.expected

@@ -1,5 +1,5 @@
 assertion\
 - Status: SUCCESS\
-- Description: "|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\
+- Description: "|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b)"\
 
 VERIFICATION:- SUCCESSFUL

tests/expected/function-contract/modifies_fat_pointer/u8slice.rs

@@ -5,7 +5,7 @@
 // Test that modifies a slice containing bytesize data
 
 #[kani::modifies(x)]
-#[kani::ensures(|_| x.into_iter().map(|v| *v == 0).fold(true,|a,b|a&b))]
+#[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))]
 fn zero(x: &mut [u8]) {
     x.fill(0)
 }