Add size_of annotation to help CBMC's allocator (model-checking#2395)

cprover_bindings/src/goto_program/expr.rs

@@ -19,7 +19,17 @@ use std::fmt::Debug;
 ///////////////////////////////////////////////////////////////////////////////////////////////
 
 /// An `Expr` represents an expression type: i.e. a computation that returns a value.
-/// Every expression has a type, a value, and a location (which may be `None`).
+/// Every expression has a type, a value, and a location (which may be `None`). An expression may
+/// also include a type annotation (`size_of_annotation`), which states that the expression is the
+/// result of computing `size_of(type)`.
+///
+/// The `size_of_annotation` is eventually picked up by CBMC's symbolic execution when simulating
+/// heap allocations: for a requested allocation of N bytes, CBMC can either create a byte array of
+/// size N, or, when a type T is annotated and N is a multiple of the size of T, an array of
+/// N/size_of(T) elements. The latter will facilitate updates using member operations (when T is an
+/// aggregate type), and pointer-typed members can be tracked more precisely. Note that this is
+/// merely a hint: failing to provide such an annotation may hamper performance, but will never
+/// affect correctness.
 ///
 /// The fields of `Expr` are kept private, and there are no getters that return mutable references.
 /// This means that the only way to create and update `Expr`s is using the constructors and setters.
@@ -41,6 +51,7 @@ pub struct Expr {
     value: Box<ExprValue>,
     typ: Type,
     location: Location,
+    size_of_annotation: Option<Type>,
 }
 
 /// The different kinds of values an expression can have.
@@ -293,6 +304,10 @@ impl Expr {
         &self.value
     }
 
+    pub fn size_of_annotation(&self) -> Option<&Type> {
+        self.size_of_annotation.as_ref()
+    }
+
     /// If the expression is an Int constant type, return its value
     pub fn int_constant_value(&self) -> Option<BigInt> {
         match &*self.value {
@@ -404,12 +419,19 @@ impl Expr {
     }
 }
 
+impl Expr {
+    pub fn with_size_of_annotation(mut self, ty: Type) -> Self {
+        self.size_of_annotation = Some(ty);
+        self
+    }
+}
+
 /// Private constructor. Making this a macro allows multiple reference to self in the same call.
 macro_rules! expr {
     ( $value:expr,  $typ:expr) => {{
         let typ = $typ;
         let value = Box::new($value);
-        Expr { value, typ, location: Location::none() }
+        Expr { value, typ, location: Location::none(), size_of_annotation: None }
     }};
 }
 

cprover_bindings/src/irep/to_irep.rs

@@ -162,6 +162,10 @@ impl ToIrep for Expr {
         } else {
             self.value().to_irep(mm).with_location(self.location(), mm).with_type(self.typ(), mm)
         }
+        .with_named_sub_option(
+            IrepId::CCSizeofType,
+            self.size_of_annotation().map(|ty| ty.to_irep(mm)),
+        )
     }
 }
 

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

@@ -288,7 +288,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }};
         }
 
-        // Intrinsics which encode a value known during compilation (e.g., `size_of`)
+        // Intrinsics which encode a value known during compilation
         macro_rules! codegen_intrinsic_const {
             () => {{
                 let value = self
@@ -611,7 +611,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 loc,
             ),
             "simd_xor" => codegen_intrinsic_binop!(bitxor),
-            "size_of" => codegen_intrinsic_const!(),
+            "size_of" => unreachable!(),
             "size_of_val" => codegen_size_align!(size),
             "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)),
             "sqrtf64" => unstable_codegen!(codegen_simple_intrinsic!(Sqrt)),
@@ -1183,7 +1183,8 @@ impl<'tcx> GotocCtx<'tcx> {
         let dst = fargs.remove(0).cast_to(Type::void_pointer());
         let val = fargs.remove(0).cast_to(Type::void_pointer());
         let layout = self.layout_of(ty);
-        let sz = Expr::int_constant(layout.size.bytes(), Type::size_t());
+        let sz = Expr::int_constant(layout.size.bytes(), Type::size_t())
+            .with_size_of_annotation(self.codegen_ty(ty));
         let e = BuiltinFn::Memcmp
             .call(vec![dst, val, sz], loc)
             .eq(Type::c_int().zero())
@@ -1267,11 +1268,12 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This function computes the size and alignment of a dynamically-sized type.
     /// The implementations follows closely the SSA implementation found in
     /// `rustc_codegen_ssa::glue::size_and_align_of_dst`.
-    fn size_and_align_of_dst(&self, t: Ty<'tcx>, arg: Expr) -> SizeAlign {
+    fn size_and_align_of_dst(&mut self, t: Ty<'tcx>, arg: Expr) -> SizeAlign {
         let layout = self.layout_of(t);
         let usizet = Type::size_t();
         if !layout.is_unsized() {
-            let size = Expr::int_constant(layout.size.bytes_usize(), Type::size_t());
+            let size = Expr::int_constant(layout.size.bytes_usize(), Type::size_t())
+                .with_size_of_annotation(self.codegen_ty(t));
             let align = Expr::int_constant(layout.align.abi.bytes(), usizet);
             return SizeAlign { size, align };
         }
@@ -1294,6 +1296,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // The info in this case is the length of the str, so the size is that
                 // times the unit size.
                 let size = Expr::int_constant(unit.size.bytes_usize(), Type::size_t())
+                    .with_size_of_annotation(self.codegen_ty(*unit_t))
                     .mul(arg.member("len", &self.symbol_table));
                 let align = Expr::int_constant(layout.align.abi.bytes(), usizet);
                 SizeAlign { size, align }
@@ -1316,7 +1319,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 // FIXME: We assume they are aligned according to the machine-preferred alignment given by layout abi.
                 let n = layout.fields.count() - 1;
                 let sized_size =
-                    Expr::int_constant(layout.fields.offset(n).bytes(), Type::size_t());
+                    Expr::int_constant(layout.fields.offset(n).bytes(), Type::size_t())
+                        .with_size_of_annotation(self.codegen_ty(t));
                 let sized_align = Expr::int_constant(layout.align.abi.bytes(), Type::size_t());
 
                 // Call this function recursively to compute the size and align for the last field.
@@ -1724,7 +1728,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ///  * The result expression of the computation.
     ///  * An assertion statement to ensure the operation has not overflowed.
     fn count_in_bytes(
-        &self,
+        &mut self,
         count: Expr,
         ty: Ty<'tcx>,
         res_ty: Type,
@@ -1733,7 +1737,8 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> (Expr, Stmt) {
         assert!(res_ty.is_integer());
         let layout = self.layout_of(ty);
-        let size_of_elem = Expr::int_constant(layout.size.bytes(), res_ty);
+        let size_of_elem = Expr::int_constant(layout.size.bytes(), res_ty)
+            .with_size_of_annotation(self.codegen_ty(ty));
         let size_of_count_elems = count.mul_overflow(size_of_elem);
         let message =
             format!("{intrinsic}: attempt to compute number in bytes which would overflow");

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

@@ -509,7 +509,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 let t = self.monomorphize(*t);
                 let layout = self.layout_of(t);
                 match k {
-                    NullOp::SizeOf => Expr::int_constant(layout.size.bytes_usize(), Type::size_t()),
+                    NullOp::SizeOf => Expr::int_constant(layout.size.bytes_usize(), Type::size_t())
+                        .with_size_of_annotation(self.codegen_ty(t)),
                     NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()),
                 }
             }
@@ -1053,11 +1054,12 @@ impl<'tcx> GotocCtx<'tcx> {
     /// When we get the size and align of a ty::Ref, the TyCtxt::layout_of
     /// returns the correct size to match rustc vtable values. Checked via
     /// Kani-compile-time and CBMC assertions in check_vtable_size.
-    fn codegen_vtable_size_and_align(&self, operand_type: Ty<'tcx>) -> (Expr, Expr) {
+    fn codegen_vtable_size_and_align(&mut self, operand_type: Ty<'tcx>) -> (Expr, Expr) {
         debug!("vtable_size_and_align {:?}", operand_type.kind());
         let vtable_layout = self.layout_of(operand_type);
         assert!(!vtable_layout.is_unsized(), "Can't create a vtable for an unsized type");
-        let vt_size = Expr::int_constant(vtable_layout.size.bytes(), Type::size_t());
+        let vt_size = Expr::int_constant(vtable_layout.size.bytes(), Type::size_t())
+            .with_size_of_annotation(self.codegen_ty(operand_type));
         let vt_align = Expr::int_constant(vtable_layout.align.abi.bytes(), Type::size_t());
 
         (vt_size, vt_align)

tests/kani/Drop/drop_after_moving_across_channel.rs

@@ -3,8 +3,6 @@
 
 //! This test checks whether dropping objects passed through
 //! std::sync::mpsc::channel is handled.
-//! This test only passes on MacOS today, so we duplicate the test for now.
-#![cfg(target_os = "macos")]
 
 use std::sync::mpsc::*;