Merge branch 'main' into features/loop-contracts-annotation

Cargo.lock

@@ -75,9 +75,9 @@ dependencies = [
 
 [[package]]
 name = "anyhow"
-version = "1.0.87"
+version = "1.0.89"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "10f00e1f6e58a40e807377c75c6a7f97bf9044fab57816f2414e6f5f4499d7b8"
+checksum = "86fdf8605db99b54d3cd748a44c6d04df638eb5dafb219b135d0149bd0db01f6"
 
 [[package]]
 name = "autocfg"
@@ -892,9 +892,9 @@ dependencies = [
 
 [[package]]
 name = "redox_syscall"
-version = "0.5.3"
+version = "0.5.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2a908a6e00f1fdd0dfd9c0eb08ce85126f6d8bbda50017e74bc4a4b7d4a926a4"
+checksum = "0884ad60e090bf1345b93da0a5de8923c93884cd03f40dfcfddd3b4bee661853"
 dependencies = [
  "bitflags",
 ]
@@ -951,9 +951,9 @@ checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f"
 
 [[package]]
 name = "rustix"
-version = "0.38.36"
+version = "0.38.37"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3f55e80d50763938498dd5ebb18647174e0c76dc38c5505294bb224624f30f36"
+checksum = "8acb788b847c24f28525660c4d7758620a7210875711f79e7f663cc152726811"
 dependencies = [
  "bitflags",
  "errno",
@@ -1345,9 +1345,9 @@ dependencies = [
 
 [[package]]
 name = "unicode-ident"
-version = "1.0.12"
+version = "1.0.13"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
+checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe"
 
 [[package]]
 name = "unicode-width"

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,
                 }
             }

kani-compiler/src/kani_middle/attributes.rs

@@ -358,7 +358,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                         );
                     }
                     expect_single(self.tcx, kind, &attrs);
-                    attrs.iter().for_each(|attr| self.check_proof_attribute(attr))
+                    attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr))
                 }
                 KaniAttributeKind::Unstable => attrs.iter().for_each(|attr| {
                     let _ = UnstableAttribute::try_from(*attr).map_err(|err| err.report(self.tcx));
@@ -370,6 +370,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                         );
                     }
                     expect_single(self.tcx, kind, &attrs);
+                    attrs.iter().for_each(|attr| self.check_proof_attribute(kind, attr))
                 }
                 KaniAttributeKind::StubVerified => {
                     expect_single(self.tcx, kind, &attrs);
@@ -583,15 +584,29 @@ impl<'tcx> KaniAttributes<'tcx> {
     }
 
     /// Check that if this item is tagged with a proof_attribute, it is a valid harness.
-    fn check_proof_attribute(&self, proof_attribute: &Attribute) {
+    fn check_proof_attribute(&self, kind: KaniAttributeKind, proof_attribute: &Attribute) {
         let span = proof_attribute.span;
         let tcx = self.tcx;
-        expect_no_args(tcx, KaniAttributeKind::Proof, proof_attribute);
+        if let KaniAttributeKind::Proof = kind {
+            expect_no_args(tcx, kind, proof_attribute);
+        }
+
         if tcx.def_kind(self.item) != DefKind::Fn {
-            tcx.dcx().span_err(span, "the `proof` attribute can only be applied to functions");
+            tcx.dcx().span_err(
+                span,
+                format!(
+                    "the '#[kani::{}]' attribute can only be applied to functions",
+                    kind.as_ref()
+                ),
+            );
         } else if tcx.generics_of(self.item).requires_monomorphization(tcx) {
-            tcx.dcx()
-                .span_err(span, "the `proof` attribute cannot be applied to generic functions");
+            tcx.dcx().span_err(
+                span,
+                format!(
+                    "the '#[kani::{}]' attribute cannot be applied to generic functions",
+                    kind.as_ref()
+                ),
+            );
         } else {
             let instance = Instance::mono(tcx, self.item);
             if !super::fn_abi(tcx, instance).args.is_empty() {

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-09-08"
+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:
     // ```