Patch kani 0.49.1

cprover_bindings/src/goto_program/expr.rs

@@ -389,6 +389,7 @@ impl Expr {
             source.is_integer() || source.is_pointer() || source.is_bool()
         } else if target.is_integer() {
             source.is_c_bool()
+                || source.is_bool()
                 || source.is_integer()
                 || source.is_floating_point()
                 || source.is_pointer()

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

@@ -292,6 +292,11 @@ impl<'tcx> GotocCtx<'tcx> {
                             "element of {parent_ty:?} is not accessed via field projection"
                         )
                     }
+                    TyKind::RigidTy(RigidTy::Pat(..)) => {
+                        // See https://github.com/rust-lang/types-team/issues/126
+                        // for what is currently supported.
+                        unreachable!("projection inside a pattern is not supported, only transmute")
+                    }
                 }
             }
             // if we fall here, then we are handling an enum

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

@@ -20,6 +20,7 @@ use num::bigint::BigInt;
 use rustc_middle::ty::{TyCtxt, VtblEntry};
 use rustc_smir::rustc_internal;
 use rustc_target::abi::{FieldsShape, TagEncoding, Variants};
+use stable_mir::abi::{Primitive, Scalar, ValueAbi};
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
     AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp,
@@ -32,9 +33,11 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand, e2: &Operand) -> Expr {
         let left_op = self.codegen_operand_stable(e1);
         let right_op = self.codegen_operand_stable(e2);
-        let is_float =
-            matches!(self.operand_ty_stable(e1).kind(), TyKind::RigidTy(RigidTy::Float(..)));
-        comparison_expr(op, left_op, right_op, is_float)
+        let left_ty = self.operand_ty_stable(e1);
+        let right_ty = self.operand_ty_stable(e2);
+        let res_ty = op.ty(left_ty, right_ty);
+        let is_float = matches!(left_ty.kind(), TyKind::RigidTy(RigidTy::Float(..)));
+        self.comparison_expr(op, left_op, right_op, res_ty, is_float)
     }
 
     /// This function codegen comparison for fat pointers.
@@ -72,16 +75,18 @@ impl<'tcx> GotocCtx<'tcx> {
             Expr::statement_expression(body, ret_type).with_location(loc)
         } else {
             // Compare data pointer.
+            let res_ty = op.ty(left_typ, right_typ);
             let left_ptr = self.codegen_operand_stable(left_op);
             let left_data = left_ptr.clone().member("data", &self.symbol_table);
             let right_ptr = self.codegen_operand_stable(right_op);
             let right_data = right_ptr.clone().member("data", &self.symbol_table);
-            let data_cmp = comparison_expr(op, left_data.clone(), right_data.clone(), false);
+            let data_cmp =
+                self.comparison_expr(op, left_data.clone(), right_data.clone(), res_ty, false);
 
             // Compare the slice metadata (this logic could be adapted to compare vtable if needed).
             let left_len = left_ptr.member("len", &self.symbol_table);
             let right_len = right_ptr.member("len", &self.symbol_table);
-            let metadata_cmp = comparison_expr(op, left_len, right_len, false);
+            let metadata_cmp = self.comparison_expr(op, left_len, right_len, res_ty, false);
 
             // Join the results.
             // https://github.com/rust-lang/rust/pull/29781
@@ -93,10 +98,20 @@ impl<'tcx> GotocCtx<'tcx> {
                 // If data is different, only compare data.
                 // If data is equal, apply operator to metadata.
                 BinOp::Lt | BinOp::Le | BinOp::Ge | BinOp::Gt => {
-                    let data_eq =
-                        comparison_expr(&BinOp::Eq, left_data.clone(), right_data.clone(), false);
-                    let data_strict_comp =
-                        comparison_expr(&get_strict_operator(op), left_data, right_data, false);
+                    let data_eq = self.comparison_expr(
+                        &BinOp::Eq,
+                        left_data.clone(),
+                        right_data.clone(),
+                        res_ty,
+                        false,
+                    );
+                    let data_strict_comp = self.comparison_expr(
+                        &get_strict_operator(op),
+                        left_data,
+                        right_data,
+                        res_ty,
+                        false,
+                    );
                     data_strict_comp.or(data_eq.and(metadata_cmp))
                 }
                 _ => unreachable!("Unexpected operator {:?}", op),
@@ -376,7 +391,7 @@ impl<'tcx> GotocCtx<'tcx> {
             BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => {
                 self.codegen_unchecked_scalar_binop(op, e1, e2)
             }
-            BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => {
+            BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt | BinOp::Cmp => {
                 let op_ty = self.operand_ty_stable(e1);
                 if self.is_fat_pointer_stable(op_ty) {
                     self.codegen_comparison_fat_ptr(op, e1, e2, loc)
@@ -681,7 +696,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 | CastKind::FnPtrToPtr
                 | CastKind::PtrToPtr
                 | CastKind::PointerExposeAddress
-                | CastKind::PointerFromExposedAddress,
+                | CastKind::PointerWithExposedProvenance,
                 e,
                 t,
             ) => self.codegen_misc_cast(e, *t),
@@ -1260,7 +1275,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn check_vtable_size(&mut self, operand_type: Ty, vt_size: Expr) -> Stmt {
         // Check against the size we get from the layout from the what we
         // get constructing a value of that type
-        let ty: Type = self.codegen_ty_stable(operand_type);
+        let ty = self.codegen_ty_stable(operand_type);
         let codegen_size = ty.sizeof(&self.symbol_table);
         assert_eq!(vt_size.int_constant_value().unwrap(), BigInt::from(codegen_size));
 
@@ -1423,6 +1438,65 @@ impl<'tcx> GotocCtx<'tcx> {
             }
         }
     }
+
+    fn comparison_expr(
+        &mut self,
+        op: &BinOp,
+        left: Expr,
+        right: Expr,
+        res_ty: Ty,
+        is_float: bool,
+    ) -> Expr {
+        match op {
+            BinOp::Eq => {
+                if is_float {
+                    left.feq(right)
+                } else {
+                    left.eq(right)
+                }
+            }
+            BinOp::Lt => left.lt(right),
+            BinOp::Le => left.le(right),
+            BinOp::Ne => {
+                if is_float {
+                    left.fneq(right)
+                } else {
+                    left.neq(right)
+                }
+            }
+            BinOp::Ge => left.ge(right),
+            BinOp::Gt => left.gt(right),
+            BinOp::Cmp => {
+                // Implement https://doc.rust-lang.org/core/cmp/trait.Ord.html as done in cranelift,
+                // i.e., (left > right) - (left < right)
+                // Return value is the Ordering enumeration:
+                // ```
+                // #[repr(i8)]
+                // pub enum Ordering {
+                //     Less = -1,
+                //     Equal = 0,
+                //     Greater = 1,
+                // }
+                // ```
+                let res_typ = self.codegen_ty_stable(res_ty);
+                let ValueAbi::Scalar(Scalar::Initialized { value, valid_range }) =
+                    res_ty.layout().unwrap().shape().abi
+                else {
+                    unreachable!("Unexpected layout")
+                };
+                assert_eq!(valid_range.start, -1i8 as u8 as u128);
+                assert_eq!(valid_range.end, 1);
+                let Primitive::Int { length, signed: true } = value else { unreachable!() };
+                let scalar_typ = Type::signed_int(length.bits());
+                left.clone()
+                    .gt(right.clone())
+                    .cast_to(scalar_typ.clone())
+                    .sub(left.lt(right).cast_to(scalar_typ))
+                    .transmute_to(res_typ, &self.symbol_table)
+            }
+            _ => unreachable!(),
+        }
+    }
 }
 
 /// Perform a wrapping subtraction of an Expr with a constant "expr - constant"
@@ -1445,30 +1519,6 @@ fn wrapping_sub(expr: &Expr, constant: u64) -> Expr {
     }
 }
 
-fn comparison_expr(op: &BinOp, left: Expr, right: Expr, is_float: bool) -> Expr {
-    match op {
-        BinOp::Eq => {
-            if is_float {
-                left.feq(right)
-            } else {
-                left.eq(right)
-            }
-        }
-        BinOp::Lt => left.lt(right),
-        BinOp::Le => left.le(right),
-        BinOp::Ne => {
-            if is_float {
-                left.fneq(right)
-            } else {
-                left.neq(right)
-            }
-        }
-        BinOp::Ge => left.ge(right),
-        BinOp::Gt => left.gt(right),
-        _ => unreachable!(),
-    }
-}
-
 /// Remove the equality from an operator. Translates `<=` to `<` and `>=` to `>`
 fn get_strict_operator(op: &BinOp) -> BinOp {
     match op {

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

@@ -595,6 +595,13 @@ impl<'tcx> GotocCtx<'tcx> {
                     )
                 }
             }
+            // This object has the same layout as base. For now, translate this into `(base)`.
+            // The only difference is the niche.
+            ty::Pat(base_ty, ..) => {
+                self.ensure_struct(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |tcx, _| {
+                    tcx.codegen_ty_tuple_like(ty, vec![*base_ty])
+                })
+            }
             ty::Alias(..) => {
                 unreachable!("Type should've been normalized already")
             }
@@ -995,6 +1002,7 @@ impl<'tcx> GotocCtx<'tcx> {
             | ty::Int(_)
             | ty::RawPtr(_, _)
             | ty::Ref(..)
+            | ty::Pat(..)
             | ty::Tuple(_)
             | ty::Uint(_) => self.codegen_ty(pointee_type).to_pointer(),
 

kani-compiler/src/kani_middle/stubbing/annotations.rs

@@ -56,7 +56,7 @@ pub fn update_stub_mapping(
                         "duplicate stub mapping: {} mapped to {} and {}",
                         tcx.def_path_str(orig_id),
                         tcx.def_path_str(stub_id),
-                        tcx.def_path_str(tcx.def_path_hash_to_def_id(other, &mut || panic!()))
+                        tcx.def_path_str(tcx.def_path_hash_to_def_id(other, &()))
                     ),
                 );
             }

kani-compiler/src/kani_middle/stubbing/transform.rs

@@ -234,7 +234,7 @@ fn deserialize_mapping(tcx: TyCtxt, val: &str) -> HashMap<DefId, DefId> {
     type Item = (u64, u64);
     let item_to_def_id = |item: Item| -> DefId {
         let hash = DefPathHash(Fingerprint::new(item.0, item.1));
-        tcx.def_path_hash_to_def_id(hash, &mut || panic!())
+        tcx.def_path_hash_to_def_id(hash, &())
     };
     let pairs: Vec<(Item, Item)> = serde_json::from_str(val).unwrap();
     let mut m = HashMap::default();

kani-compiler/src/kani_middle/transform/check_values.rs

@@ -612,7 +612,7 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> {
                     ty: (rvalue.ty(self.locals).unwrap()),
                 }),
                 CastKind::PointerExposeAddress
-                | CastKind::PointerFromExposedAddress
+                | CastKind::PointerWithExposedProvenance
                 | CastKind::PointerCoercion(_)
                 | CastKind::IntToInt
                 | CastKind::FloatToInt
@@ -879,6 +879,12 @@ fn ty_validity_per_offset(
                         }
                     }
                 }
+                RigidTy::Pat(base_ty, ..) => {
+                    // This is similar to a structure with one field and with niche defined.
+                    let mut pat_validity = ty_req();
+                    pat_validity.append(&mut ty_validity_per_offset(machine_info, *base_ty, 0)?);
+                    Ok(pat_validity)
+                }
                 RigidTy::Tuple(tys) => {
                     let mut tuple_validity = vec![];
                     for idx in layout.fields.fields_by_offset_order() {

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-03-29"
+channel = "nightly-2024-04-15"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tests/kani/ValidValues/write_invalid_fixme.rs → tests/kani/ValidValues/write_invalid.rs

@@ -6,9 +6,6 @@
 //! Writing invalid bytes is not UB as long as the incorrect value is not read.
 //! However, we over-approximate for sake of simplicity and performance.
 
-// Note: We're getting an unexpected compilation error because the type returned
-// from StableMIR is `Alias`: https://github.com/model-checking/kani/issues/3113
-
 use std::num::NonZeroU8;
 
 #[kani::proof]