initial working for bytesize

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;
@@ -121,11 +121,44 @@ 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)) {
+                    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),
+                        ]),
+                    )
+                } else {
+                    Lambda::as_contract_for(
+                        &goto_annotated_fn_typ,
+                        None,
+                        self.codegen_place_stable(&local.into(), loc)
+                            .unwrap()
+                            .goto_expr
+                            .dereference(),
+                    )
+                }
             })
             .collect();
 

library/kani/src/internal.rs

@@ -7,7 +7,7 @@
 #[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.
     ///
@@ -16,7 +16,7 @@ pub trait Pointer<'a> {
     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 fill_any(self);
 }
 
 impl<'a, 'b, T> Pointer<'a> for &'b T {
@@ -26,8 +26,8 @@ impl<'a, 'b, T> Pointer<'a> for &'b T {
     }
 
     #[allow(clippy::transmute_ptr_to_ref)]
-    unsafe fn assignable(self) -> &'a mut Self::Inner {
-        std::mem::transmute(self as *const T)
+    unsafe fn fill_any(self) {
+        *std::mem::transmute::<*const T, &mut T>(self as *const T) = crate::any_modifies();
     }
 }
 
@@ -39,8 +39,8 @@ impl<'a, 'b, T> Pointer<'a> for &'b mut T {
         std::mem::transmute::<_, &&'a T>(self)
     }
 
-    unsafe fn assignable(self) -> &'a mut Self::Inner {
-        std::mem::transmute(self)
+    unsafe fn fill_any(self) {
+        *std::mem::transmute::<&mut T, &mut T>(self) = crate::any_modifies();
     }
 }
 
@@ -51,8 +51,8 @@ impl<'a, T> Pointer<'a> for *const T {
     }
 
     #[allow(clippy::transmute_ptr_to_ref)]
-    unsafe fn assignable(self) -> &'a mut Self::Inner {
-        std::mem::transmute(self)
+    unsafe fn fill_any(self) {
+        *std::mem::transmute::<*const T, &mut T>(self) = crate::any_modifies();
     }
 }
 
@@ -63,8 +63,58 @@ impl<'a, T> Pointer<'a> for *mut T {
     }
 
     #[allow(clippy::transmute_ptr_to_ref)]
-    unsafe fn assignable(self) -> &'a mut Self::Inner {
-        std::mem::transmute(self)
+    unsafe fn fill_any(self) {
+        *std::mem::transmute::<*mut T, &mut T>(self) = crate::any_modifies();
+    }
+}
+
+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_modifies::<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_modifies::<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_modifies::<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_modifies::<T>());
     }
 }
 

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::Pointer::fill_any(kani::internal::untracked_deref(&#attr))};)*
                     #(#after)*
                     #result
                 )