Merge branch 'main' into contract-harness-errors

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

@@ -23,10 +23,12 @@ use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
 use rustc_middle::mir::coverage::SourceRegion;
 use stable_mir::mir::{Place, ProjectionElem};
-use stable_mir::ty::{Span as SpanStable, TypeAndMut};
+use stable_mir::ty::{Span as SpanStable, Ty};
 use strum_macros::{AsRefStr, EnumString};
 use tracing::debug;
 
+use super::intrinsic::SizeAlign;
+
 /// Classifies the type of CBMC `assert`, as different assertions can have different semantics (e.g. cover)
 ///
 /// Each property class should justify its existence with a note about the special handling it recieves.
@@ -333,8 +335,10 @@ impl<'tcx> GotocCtx<'tcx> {
  pub fn codegen_raw_ptr_deref_validity_check(
  &mut self,
  place: &Place,
+ place_ref: Expr,
+ place_ref_ty: Ty,
  loc: &Location,
- ) -> Option<Stmt> {
+ ) -> Option<(Stmt, Stmt)> {
  if let Some(ProjectionElem::Deref) = place.projection.last() {
  // Create a place without the topmost dereference projection.ß
  let ptr_place = {
@@ -346,41 +350,42 @@ impl<'tcx> GotocCtx<'tcx> {
  let ptr_place_ty = self.place_ty_stable(&ptr_place);
  if ptr_place_ty.kind().is_raw_ptr() {
  // Extract the size of the pointee.
- let pointee_size = {
- let TypeAndMut { ty: pointee_ty, .. } =
- ptr_place_ty.kind().builtin_deref(true).unwrap();
- let pointee_ty_layout = pointee_ty.layout().unwrap();
- pointee_ty_layout.shape().size.bytes()
+ let SizeAlign { size: sz, align } =
+ self.size_and_align_of_dst(place_ref_ty, place_ref);
+
+ // Encode __CPROVER_r_ok(ptr, size).
+ // First, generate a CBMC expression representing the pointer.
+ let ptr = {
+ let ptr_projection = self.codegen_place_stable(&ptr_place, *loc).unwrap();
+ let place_ty = self.place_ty_stable(place);
+ if self.use_thin_pointer_stable(place_ty) {
+ ptr_projection.goto_expr().clone()
+ } else {
+ ptr_projection.goto_expr().clone().member("data", &self.symbol_table)
+ }
  };
+ // Then generate an alignment check
+ let align_ok =
+ ptr.clone().cast_to(Type::size_t()).rem(align).eq(Type::size_t().zero());
+ let align_check = self.codegen_assert_assume(align_ok, PropertyClass::SafetyCheck,
+ "misaligned pointer to reference cast: address must be a multiple of its type's \
+ alignment", *loc);
 
+ // Then, generate a __CPROVER_r_ok check.
+ let raw_ptr_read_ok_expr =
+ Expr::read_ok(ptr.cast_to(Type::void_pointer()), sz.clone())
+ .cast_to(Type::Bool);
  // __CPROVER_r_ok fails if size == 0, so need to explicitly avoid the check.
- if pointee_size != 0 {
- // Encode __CPROVER_r_ok(ptr, size).
- // First, generate a CBMC expression representing the pointer.
- let ptr = {
- let ptr_projection = self.codegen_place_stable(&ptr_place, *loc).unwrap();
- let place_ty = self.place_ty_stable(place);
- if self.use_thin_pointer_stable(place_ty) {
- ptr_projection.goto_expr().clone()
- } else {
- ptr_projection.goto_expr().clone().member("data", &self.symbol_table)
- }
- };
- // Then, generate a __CPROVER_r_ok check.
- let raw_ptr_read_ok_expr = Expr::read_ok(
- ptr.cast_to(Type::void_pointer()),
- Expr::int_constant(pointee_size, Type::size_t()),
- )
- .cast_to(Type::Bool);
- // Finally, assert that the pointer points to a valid memory location.
- let raw_ptr_read_ok = self.codegen_assert(
- raw_ptr_read_ok_expr,
- PropertyClass::SafetyCheck,
- "dereference failure: pointer invalid",
- *loc,
- );
- return Some(raw_ptr_read_ok);
- }
+ let sz_typ = sz.typ().clone();
+ let raw_ptr_read_ok_expr = sz.eq(sz_typ.zero()).or(raw_ptr_read_ok_expr);
+ // Finally, assert that the pointer points to a valid memory location.
+ let raw_ptr_read_ok = self.codegen_assert(
+ raw_ptr_read_ok_expr,
+ PropertyClass::SafetyCheck,
+ "dereference failure: pointer invalid",
+ *loc,
+ );
+ return Some((align_check, raw_ptr_read_ok));
  }
  }
  None

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

@@ -18,9 +18,9 @@ use stable_mir::mir::{BasicBlockIdx, Operand, Place};
 use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
 use tracing::debug;
 
-struct SizeAlign {
- size: Expr,
- align: Expr,
+pub struct SizeAlign {
+ pub size: Expr,
+ pub align: Expr,
 }
 
 enum VTableInfo {
@@ -1291,7 +1291,7 @@ 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(&mut self, ty: Ty, arg: Expr) -> SizeAlign {
+ pub fn size_and_align_of_dst(&mut self, ty: Ty, arg: Expr) -> SizeAlign {
  let layout = self.layout_of_stable(ty);
  let usizet = Type::size_t();
  if !layout.is_unsized() {

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

@@ -738,12 +738,23 @@ impl<'tcx> GotocCtx<'tcx> {
  Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => {
  let place_ref = self.codegen_place_ref_stable(&p, loc);
  let place_ref_type = place_ref.typ().clone();
- match self.codegen_raw_ptr_deref_validity_check(&p, &loc) {
- Some(ptr_validity_check_expr) => Expr::statement_expression(
- vec![ptr_validity_check_expr, place_ref.as_stmt(loc)],
- place_ref_type,
- loc,
- ),
+ match self.codegen_raw_ptr_deref_validity_check(
+ &p,
+ place_ref.clone(),
+ self.place_ty_stable(p),
+ &loc,
+ ) {
+ Some((ptr_alignment_check_expr, ptr_validity_check_expr)) => {
+ Expr::statement_expression(
+ vec![
+ ptr_alignment_check_expr,
+ ptr_validity_check_expr,
+ place_ref.as_stmt(loc),
+ ],
+ place_ref_type,
+ loc,
+ )
+ }
  None => place_ref,
  }
  }

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-09-11"
+channel = "nightly-2024-09-12"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/intrinsics/simd-arith-overflows/main.rs

@@ -8,14 +8,14 @@ use std::intrinsics::simd::{simd_add, simd_mul, simd_sub};
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq, Debug)]
-pub struct i8x2(i8, i8);
+pub struct i8x2([i8; 2]);
 
 #[kani::proof]
 fn main() {
  let a = kani::any();
  let b = kani::any();
- let simd_a = i8x2(a, a);
- let simd_b = i8x2(b, b);
+ let simd_a = i8x2([a, a]);
+ let simd_b = i8x2([b, b]);
 
  unsafe {
  let _ = simd_add(simd_a, simd_b);

tests/expected/intrinsics/simd-cmp-result-type-is-diff-size/main.rs

@@ -9,26 +9,26 @@ use std::intrinsics::simd::simd_eq;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u64x2(u64, u64);
+pub struct u64x2([u64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u32x4(u32, u32, u32, u32);
+pub struct u32x4([u32; 4]);
 
 #[kani::proof]
 fn main() {
- let x = u64x2(0, 0);
- let y = u64x2(0, 1);
+ let x = u64x2([0, 0]);
+ let y = u64x2([0, 1]);
 
  unsafe {
  let invalid_simd: u32x4 = simd_eq(x, y);
- assert!(invalid_simd == u32x4(u32::MAX, u32::MAX, 0, 0));
+ assert!(invalid_simd == u32x4([u32::MAX, u32::MAX, 0, 0]));
  // ^^^^ The code above fails to type-check in Rust with the error:
  // ```
  // error[E0511]: invalid monomorphization of `simd_eq` intrinsic: expected

tests/expected/intrinsics/simd-div-div-zero/main.rs

@@ -8,13 +8,13 @@ use std::intrinsics::simd::simd_div;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[kani::proof]
 fn test_simd_div() {
  let dividend = kani::any();
- let dividends = i32x2(dividend, dividend);
+ let dividends = i32x2([dividend, dividend]);
  let divisor = 0;
- let divisors = i32x2(divisor, divisor);
+ let divisors = i32x2([divisor, divisor]);
  let _ = unsafe { simd_div(dividends, divisors) };
 }

tests/expected/intrinsics/simd-div-rem-overflow/expected

@@ -1,8 +1,8 @@
 FAILURE\
 attempt to compute simd_div which would overflow
 UNREACHABLE\
-assertion failed: quotients.0 == quotients.1
+assertion failed: quotients.0[0] == quotients.0[1]
 FAILURE\
 attempt to compute simd_rem which would overflow
 UNREACHABLE\
-assertion failed: remainders.0 == remainders.1
+assertion failed: remainders.0[0] == remainders.0[1]

tests/expected/intrinsics/simd-div-rem-overflow/main.rs

@@ -8,7 +8,7 @@ use std::intrinsics::simd::{simd_div, simd_rem};
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 unsafe fn do_simd_div(dividends: i32x2, divisors: i32x2) -> i32x2 {
  simd_div(dividends, divisors)
@@ -21,19 +21,19 @@ unsafe fn do_simd_rem(dividends: i32x2, divisors: i32x2) -> i32x2 {
 #[kani::proof]
 fn test_simd_div_overflow() {
  let dividend = i32::MIN;
- let dividends = i32x2(dividend, dividend);
+ let dividends = i32x2([dividend, dividend]);
  let divisor = -1;
- let divisors = i32x2(divisor, divisor);
+ let divisors = i32x2([divisor, divisor]);
  let quotients = unsafe { do_simd_div(dividends, divisors) };
- assert_eq!(quotients.0, quotients.1);
+ assert_eq!(quotients.0[0], quotients.0[1]);
 }
 
 #[kani::proof]
 fn test_simd_rem_overflow() {
  let dividend = i32::MIN;
- let dividends = i32x2(dividend, dividend);
+ let dividends = i32x2([dividend, dividend]);
  let divisor = -1;
- let divisors = i32x2(divisor, divisor);
+ let divisors = i32x2([divisor, divisor]);
  let remainders = unsafe { do_simd_rem(dividends, divisors) };
- assert_eq!(remainders.0, remainders.1);
+ assert_eq!(remainders.0[0], remainders.0[1]);
 }

tests/expected/intrinsics/simd-extract-wrong-type/main.rs

@@ -10,11 +10,11 @@ use std::intrinsics::simd::simd_extract;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[kani::proof]
 fn main() {
- let y = i64x2(0, 1);
+ let y = i64x2([0, 1]);
  let res: i32 = unsafe { simd_extract(y, 1) };
  // ^^^^ The code above fails to type-check in Rust with the error:
  // ```

tests/expected/intrinsics/simd-insert-wrong-type/main.rs

@@ -10,11 +10,11 @@ use std::intrinsics::simd::simd_insert;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[kani::proof]
 fn main() {
- let y = i64x2(0, 1);
+ let y = i64x2([0, 1]);
  let _ = unsafe { simd_insert(y, 0, 1) };
  // ^^^^ The code above fails to type-check in Rust with the error:
  // ```

tests/expected/intrinsics/simd-rem-div-zero/main.rs

@@ -8,13 +8,13 @@ use std::intrinsics::simd::simd_rem;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[kani::proof]
 fn test_simd_rem() {
  let dividend = kani::any();
- let dividends = i32x2(dividend, dividend);
+ let dividends = i32x2([dividend, dividend]);
  let divisor = 0;
- let divisors = i32x2(divisor, divisor);
+ let divisors = i32x2([divisor, divisor]);
  let _ = unsafe { simd_rem(dividends, divisors) };
 }

tests/expected/intrinsics/simd-result-type-is-float/main.rs

@@ -9,31 +9,31 @@ use std::intrinsics::simd::simd_eq;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i64x2(i64, i64);
+pub struct i64x2([i64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u64x2(u64, u64);
+pub struct u64x2([u64; 2]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct u32x4(u32, u32, u32, u32);
+pub struct u32x4([u32; 4]);
 
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq)]
-pub struct f32x2(f32, f32);
+pub struct f32x2([f32; 2]);
 
 #[kani::proof]
 fn main() {
- let x = u64x2(0, 0);
- let y = u64x2(0, 1);
+ let x = u64x2([0, 0]);
+ let y = u64x2([0, 1]);
 
  unsafe {
  let invalid_simd: f32x2 = simd_eq(x, y);
- assert!(invalid_simd == f32x2(0.0, -1.0));
+ assert!(invalid_simd == f32x2([0.0, -1.0]));
  // ^^^^ The code above fails to type-check in Rust with the error:
  // ```
  // error[E0511]: invalid monomorphization of `simd_eq` intrinsic: expected return type with integer elements, found `f32x2` with non-integer `f32`

tests/expected/intrinsics/simd-shl-shift-negative/main.rs

@@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shl;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[kani::proof]
 fn test_simd_shl() {
  let value = kani::any();
- let values = i32x2(value, value);
+ let values = i32x2([value, value]);
  let shift = kani::any();
  kani::assume(shift < 32);
- let shifts = i32x2(shift, shift);
+ let shifts = i32x2([shift, shift]);
  let _result = unsafe { simd_shl(values, shifts) };
 }

tests/expected/intrinsics/simd-shl-shift-too-large/main.rs

@@ -8,14 +8,14 @@ use std::intrinsics::simd::simd_shl;
 #[repr(simd)]
 #[allow(non_camel_case_types)]
 #[derive(Clone, Copy, PartialEq, Eq)]
-pub struct i32x2(i32, i32);
+pub struct i32x2([i32; 2]);
 
 #[kani::proof]
 fn test_simd_shl() {
  let value = kani::any();
- let values = i32x2(value, value);
+ let values = i32x2([value, value]);
  let shift = kani::any();
  kani::assume(shift >= 0);
- let shifts = i32x2(shift, shift);
+ let shifts = i32x2([shift, shift]);
  let _result = unsafe { simd_shl(values, shifts) };
 }