From b5c116d342f4319e5bb5fd146f8bc88d654ea635 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 25 Apr 2023 14:02:57 +0200 Subject: [PATCH] Add size_of annotation to help CBMC's allocator (#2395) --- cprover_bindings/src/goto_program/expr.rs | 26 ++++++++++- cprover_bindings/src/irep/to_irep.rs | 4 ++ .../codegen/intrinsic.rs | 21 +++++---- .../codegen_cprover_gotoc/codegen/rvalue.rs | 8 ++-- .../Drop/drop_after_moving_across_channel.rs | 2 - .../fixme_drop_after_moving_across_channel.rs | 46 ------------------- 6 files changed, 46 insertions(+), 61 deletions(-) delete mode 100644 tests/kani/Drop/fixme_drop_after_moving_across_channel.rs diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 7aae03f1538a..f0bd945d63ce 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/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, typ: Type, location: Location, + size_of_annotation: Option, } /// 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 { 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 } }}; } diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 3ba02e3bd97f..70810e403c54 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/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)), + ) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index d657de37c601..6e63f2dfe70a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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"); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 29d636cc4150..e47b0984d440 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/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) diff --git a/tests/kani/Drop/drop_after_moving_across_channel.rs b/tests/kani/Drop/drop_after_moving_across_channel.rs index f06f7b3fa1e7..1c59e2e404e9 100644 --- a/tests/kani/Drop/drop_after_moving_across_channel.rs +++ b/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::*; diff --git a/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs b/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs deleted file mode 100644 index a66d7df7cf36..000000000000 --- a/tests/kani/Drop/fixme_drop_after_moving_across_channel.rs +++ /dev/null @@ -1,46 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This test checks whether dropping objects passed through -//! std::sync::mpsc::channel is handled. -// -// This test case fails to resolve in a reasonable amount of -// time. Settign kani::unwind(1) is insufficient for verification, but -// kani::unwind(2) takes longer than 10m on a M1 Mac. For details, -// please see: https://github.com/model-checking/kani/issues/1286 - -#[cfg(target_os = "linux")] -mod fixme_harness { - use std::sync::mpsc::*; - - static mut CELL: i32 = 0; - - struct DropSetCELLToOne {} - - impl Drop for DropSetCELLToOne { - fn drop(&mut self) { - unsafe { - CELL = 1; - } - } - } - - #[kani::unwind(1)] - #[kani::proof] - fn main() { - { - let (send, recv) = channel::(); - send.send(DropSetCELLToOne {}).unwrap(); - let _to_drop: DropSetCELLToOne = recv.recv().unwrap(); - } - assert_eq!(unsafe { CELL }, 1, "Drop should be called"); - } -} - -#[cfg(target_os = "macos")] -mod forced_failure { - #[kani::proof] - fn just_panic() { - panic!("This test only fails on linux"); - } -}