Function Contracts: Modify Slices

kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs

@@ -3,7 +3,7 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::attributes::KaniAttributes;
 use cbmc::goto_program::FunctionContract;
-use cbmc::goto_program::{Lambda, Location};
+use cbmc::goto_program::{Expr, Lambda, Location, Type};
 use kani_metadata::AssignsContract;
 use rustc_hir::def_id::DefId as InternalDefId;
 use rustc_smir::rustc_internal;
@@ -12,6 +12,8 @@ use stable_mir::mir::Local;
 use stable_mir::CrateDef;
 use tracing::debug;
 
+use stable_mir::ty::{RigidTy, TyKind};
+
 impl<'tcx> GotocCtx<'tcx> {
     /// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
     /// find or create the `AssignsContract` that needs to be enforced and attach it to the symbol
@@ -142,11 +144,63 @@ impl<'tcx> GotocCtx<'tcx> {
         let assigns = modified_places
             .into_iter()
             .map(|local| {
-                Lambda::as_contract_for(
-                    &goto_annotated_fn_typ,
-                    None,
-                    self.codegen_place_stable(&local.into(), loc).unwrap().goto_expr.dereference(),
-                )
+                if self.is_fat_pointer_stable(self.local_ty_stable(local)) {
+                    let unref = match self.local_ty_stable(local).kind() {
+                        TyKind::RigidTy(RigidTy::Ref(_, ty, _)) => ty,
+                        kind => unreachable!("{:?} is not a reference", kind),
+                    };
+                    let size = match unref.kind() {
+                        TyKind::RigidTy(RigidTy::Slice(elt_type)) => {
+                            elt_type.layout().unwrap().shape().size.bytes()
+                        }
+                        TyKind::RigidTy(RigidTy::Str) => 8,
+                        // For adt, see https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp
+                        TyKind::RigidTy(RigidTy::Adt(..)) => {
+                            todo!("Adt fat pointers not implemented")
+                        }
+                        kind => unreachable!("Generating a slice fat pointer to {:?}", kind),
+                    };
+                    Lambda::as_contract_for(
+                        &goto_annotated_fn_typ,
+                        None,
+                        Expr::symbol_expression(
+                            "__CPROVER_object_upto",
+                            Type::code(
+                                vec![
+                                    Type::empty()
+                                        .to_pointer()
+                                        .as_parameter(None, Some("ptr".into())),
+                                    Type::size_t().as_parameter(None, Some("size".into())),
+                                ],
+                                Type::empty(),
+                            ),
+                        )
+                        .call(vec![
+                            self.codegen_place_stable(&local.into(), loc)
+                                .unwrap()
+                                .goto_expr
+                                .member("data", &self.symbol_table)
+                                .cast_to(Type::empty().to_pointer()),
+                            self.codegen_place_stable(&local.into(), loc)
+                                .unwrap()
+                                .goto_expr
+                                .member("len", &self.symbol_table)
+                                .mul(Expr::size_constant(
+                                    size.try_into().unwrap(),
+                                    &self.symbol_table,
+                                )),
+                        ]),
+                    )
+                } else {
+                    Lambda::as_contract_for(
+                        &goto_annotated_fn_typ,
+                        None,
+                        self.codegen_place_stable(&local.into(), loc)
+                            .unwrap()
+                            .goto_expr
+                            .dereference(),
+                    )
+                }
             })
             .chain(shadow_memory_assign)
             .collect();

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)
     }

library/kani/src/internal.rs

@@ -7,19 +7,18 @@
 #[doc(hidden)]
 pub trait Pointer<'a> {
     /// Type of the pointed-to data
-    type Inner;
+    type Inner: ?Sized;
 
     /// Used for checking assigns contracts where we pass immutable references to the function.
     ///
     /// 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 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)
@@ -31,7 +30,7 @@ impl<'a, 'b, T> Pointer<'a> for &'b 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)]
@@ -44,7 +43,7 @@ impl<'a, 'b, T> Pointer<'a> for &'b mut T {
     }
 }
 
-impl<'a, T> Pointer<'a> for *const 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
@@ -56,7 +55,7 @@ impl<'a, T> Pointer<'a> for *const T {
     }
 }
 
-impl<'a, T> Pointer<'a> for *mut 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

library/kani/src/lib.rs

@@ -183,6 +183,39 @@ 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: ?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) {
+    unsafe { s.as_bytes_mut() }.fill_with(u8::any)
+    //TODO: String validation
+}
+
 /// 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/check.rs

@@ -156,11 +156,19 @@ impl<'a> ContractConditionsHandler<'a> {
             let sig = &mut self.annotated_fn.sig;
             for (arg, arg_type) in wrapper_args.clone().zip(type_params) {
                 // Add the type parameter to the function signature's generic parameters list
+                let mut bounds: syn::punctuated::Punctuated<syn::TypeParamBound, syn::token::Plus> =
+                    syn::punctuated::Punctuated::new();
+                bounds.push(syn::TypeParamBound::Trait(syn::TraitBound {
+                    paren_token: None,
+                    modifier: syn::TraitBoundModifier::Maybe(Token![?](Span::call_site())),
+                    lifetimes: None,
+                    path: syn::Ident::new("Sized", Span::call_site()).into(),
+                }));
                 sig.generics.params.push(syn::GenericParam::Type(syn::TypeParam {
                     attrs: vec![],
                     ident: arg_type.clone(),
-                    colon_token: None,
-                    bounds: Default::default(),
+                    colon_token: Some(Token![:](Span::call_site())),
+                    bounds: bounds,
                     eq_token: None,
                     default: None,
                 }));

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::assignable(kani::internal::untracked_deref(&(#attr))) } = kani::any_modifies();)*
+                    #(kani::havoc(unsafe{kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr))});)*
                     #(#after)*
                     #result
                 )

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

@@ -0,0 +1,5 @@
+assertion\
+- Status: SUCCESS\
+- 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

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Test that modifies a slice of nondeterministic size
+
+#[kani::modifies(x)]
+#[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))]
+fn zero(x: &mut [u8]) {
+    x.fill(0)
+}
+
+#[kani::proof_for_contract(zero)]
+fn harness() {
+    let mut x = [0..kani::any()].map(|_| kani::any());
+    zero(&mut x);
+}

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

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

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

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Test that modifies a slice containing bytesize data
+
+#[kani::modifies(x)]
+#[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))]
+fn zero(x: &mut [u32]) {
+    x.fill(0)
+}
+
+#[kani::proof_for_contract(zero)]
+fn harness() {
+    let mut x = [kani::any(), kani::any(), kani::any()];
+    zero(&mut x);
+}

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

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

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

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Test that modifies a slice containing bytesize data
+
+#[kani::modifies(x)]
+#[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))]
+fn zero(x: &mut [u8]) {
+    x.fill(0)
+}
+
+#[kani::proof_for_contract(zero)]
+fn harness() {
+    let mut x = [kani::any(), kani::any(), kani::any()];
+    zero(&mut x);
+}