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) => 1,
+                        // 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,20 +11,29 @@ 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;
 use tracing::{debug, trace};
 
-/// Check if we can replace calls to any_modifies.
+/// Check if we can replace calls to any_modifies or write_any.
 ///
 /// This pass will replace the entire body, and it should only be applied to stubs
 /// that have a body.
+///
+/// write_any is replaced with one of write_any_slim, write_any_slice, or write_any_str
+/// depending on what the type of the input it
+///
+/// any_modifies is replaced with any
 #[derive(Debug)]
 pub struct AnyModifiesPass {
     kani_any: Option<FnDef>,
     kani_any_modifies: Option<FnDef>,
+    kani_write_any: Option<FnDef>,
+    kani_write_any_slim: Option<FnDef>,
+    kani_write_any_slice: Option<FnDef>,
+    kani_write_any_str: Option<FnDef>,
     stubbed: HashSet<DefId>,
     target_fn: Option<InternedString>,
 }
@@ -78,6 +87,18 @@ impl AnyModifiesPass {
         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 (target_fn, stubbed) = if let Some(harness) = unit.harnesses.first() {
             let attributes = KaniAttributes::for_instance(tcx, *harness);
             let target_fn =
@@ -86,7 +107,16 @@ impl AnyModifiesPass {
         } else {
             (None, HashSet::new())
         };
-        AnyModifiesPass { kani_any, kani_any_modifies, target_fn, stubbed }
+        AnyModifiesPass {
+            kani_any,
+            kani_any_modifies,
+            kani_write_any,
+            kani_write_any_slim,
+            kani_write_any_slice,
+            kani_write_any_str,
+            target_fn,
+            stubbed,
+        }
     }
 
     /// If we apply `transform_any_modifies` in all contract-generated items,
@@ -105,7 +135,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 +147,47 @@ impl AnyModifiesPass {
                 *func = Operand::Constant(new_func);
                 changed = true;
             }
+
+            // if this is a valid kani::write_any function
+            if let TyKind::RigidTy(RigidTy::FnDef(def, instance_args)) =
+                func.ty(&locals).unwrap().kind()
+                && Some(def) == self.kani_write_any
+                && 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)
+            {
+                // case on the type of the input
+                if let TyKind::RigidTy(RigidTy::Slice(_)) = internal_type.kind() {
+                    //if the input is a slice, use write_any_slice
+                    let instance =
+                        Instance::resolve(self.kani_write_any_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() {
+                    //if the input is a str, use write_any_str
+                    let instance =
+                        Instance::resolve(self.kani_write_any_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 {
+                    //otherwise, use write_any_slim
+                    let instance =
+                        Instance::resolve(self.kani_write_any_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

@@ -1,70 +1,69 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+use crate::arbitrary::Arbitrary;
+use std::ptr;
+
 /// Helper trait for code generation for `modifies` contracts.
 ///
 /// We allow the user to provide us with a pointer-like object that we convert as needed.
 #[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;
+    unsafe fn assignable(self) -> *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 {
+    unsafe fn assignable(self) -> *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)
     }
 
-    unsafe fn assignable(self) -> &'a mut Self::Inner {
-        std::mem::transmute(self)
+    unsafe fn assignable(self) -> *mut Self::Inner {
+        self as *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
     }
 
-    #[allow(clippy::transmute_ptr_to_ref)]
-    unsafe fn assignable(self) -> &'a mut Self::Inner {
+    unsafe fn assignable(self) -> *mut Self::Inner {
         std::mem::transmute(self)
     }
 }
 
-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
     }
 
-    #[allow(clippy::transmute_ptr_to_ref)]
-    unsafe fn assignable(self) -> &'a mut Self::Inner {
-        std::mem::transmute(self)
+    unsafe fn assignable(self) -> *mut Self::Inner {
+        self
     }
 }
 
@@ -97,3 +96,49 @@ pub fn init_contracts() {}
 pub fn apply_closure<T, U: Fn(&T) -> bool>(f: U, x: &T) -> bool {
     f(x)
 }
+
+/// 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.
+#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
+#[rustc_diagnostic_item = "KaniWriteAny"]
+#[inline(never)]
+#[doc(hidden)]
+pub unsafe fn write_any<T: ?Sized>(_pointer: *mut 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!()
+}
+
+/// Fill in a slice with kani::any.
+/// Intended as a post compilation replacement for write_any
+#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
+#[rustc_diagnostic_item = "KaniWriteAnySlice"]
+#[inline(always)]
+pub unsafe fn write_any_slice<T: Arbitrary>(slice: *mut [T]) {
+    (*slice).fill_with(T::any)
+}
+
+/// Fill in a pointer with kani::any.
+/// Intended as a post compilation replacement for write_any
+#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
+#[rustc_diagnostic_item = "KaniWriteAnySlim"]
+#[inline(always)]
+pub unsafe fn write_any_slim<T: Arbitrary>(pointer: *mut T) {
+    ptr::write(pointer, T::any())
+}
+
+/// Fill in a str with kani::any.
+/// Intended as a post compilation replacement for write_any.
+/// Not yet implemented
+#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
+#[rustc_diagnostic_item = "KaniWriteAnyStr"]
+#[inline(always)]
+pub unsafe fn write_any_str(_s: *mut str) {
+    //TODO: strings introduce new UB
+    //(*s).as_bytes_mut().fill_with(u8::any)
+    //TODO: String validation
+    unimplemented!("Kani does not support creating arbitrary `str`")
+}

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();)*
+                    #(unsafe{kani::internal::write_any(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