From 4a6a4f47c56ddf6667483f197014f6682dbc97b6 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 18 Apr 2023 13:41:50 -0700
Subject: [PATCH 1/9] Upgrade the toolchain to nightly-2023-04-16

 - Fixed compilation errors but not runtime.
 - There are a few new variants that still need to be implemented.
---
 .../codegen_cprover_gotoc/codegen/assert.rs   |  4 +--
 .../codegen/intrinsic.rs                      | 19 +++++++++----
 .../codegen_cprover_gotoc/codegen/operand.rs  |  4 +--
 .../codegen_cprover_gotoc/codegen/place.rs    | 11 ++++----
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 25 +++++++++++------
 .../codegen/statement.rs                      | 12 ++++----
 .../src/codegen_cprover_gotoc/codegen/typ.rs  | 27 +++++++++---------
 .../compiler_interface.rs                     |  7 ++++-
 .../codegen_cprover_gotoc/context/goto_ctx.rs | 19 -------------
 kani-compiler/src/kani_middle/attributes.rs   |  4 +--
 kani-compiler/src/kani_middle/coercion.rs     |  2 +-
 kani-compiler/src/kani_middle/provide.rs      | 28 ++++++++++---------
 kani-compiler/src/kani_middle/reachability.rs |  8 +++---
 kani-compiler/src/main.rs                     |  3 +-
 kani-compiler/src/session.rs                  |  7 ++---
 rust-toolchain.toml                           |  2 +-
 .../rustc-generator-tests/yield-in-box.rs     |  8 +++---
 tools/bookrunner/librustdoc/doctest.rs        |  7 +++--
 tools/bookrunner/librustdoc/lib.rs            |  2 --
 tools/compiletest/src/header.rs               |  6 ++++
 20 files changed, 107 insertions(+), 98 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index 8dfb31af85cc..1003681bce80 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -154,11 +154,11 @@ impl<'tcx> GotocCtx<'tcx> {
         if self.queries.get_check_assertion_reachability() {
             // Generate a unique ID for the assert
             let assert_id = self.next_check_id();
-            // Generate a message for the reachability check that includes the unique ID
-            let reach_msg = assert_id.clone();
             // Also add the unique ID as a prefix to the assert message so that it can be
             // easily paired with the reachability check
             let msg = GotocCtx::add_prefix_to_msg(&msg, &assert_id);
+            // Generate a message for the reachability check that includes the unique ID
+            let reach_msg = assert_id;
             // inject a reachability check, which is a (non-blocking)
             // assert(false) whose failure indicates that this line is reachable.
             // The property class (`PropertyClass:ReachabilityCheck`) is used by
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index d657de37c601..081ab52adbe1 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -9,7 +9,7 @@ use cbmc::goto_program::{
     Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
 };
 use rustc_middle::mir::{BasicBlock, Operand, Place};
-use rustc_middle::ty::layout::LayoutOf;
+use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement};
 use rustc_middle::ty::{self, Ty};
 use rustc_middle::ty::{Instance, InstanceDef};
 use rustc_span::Span;
@@ -760,7 +760,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// layout is invalid so we get a message that mentions the offending type.
     ///
     /// <https://doc.rust-lang.org/std/intrinsics/fn.assert_inhabited.html>
-    /// <https://doc.rust-lang.org/std/intrinsics/fn.assert_uninit_valid.html>
+    /// <https://doc.rust-lang.org/std/intrinsics/fn.assert_mem_uninitialized_valid.html>
     /// <https://doc.rust-lang.org/std/intrinsics/fn.assert_zero_valid.html>
     fn codegen_assert_intrinsic(
         &mut self,
@@ -788,7 +788,10 @@ impl<'tcx> GotocCtx<'tcx> {
         // Then we check if the type allows "raw" initialization for the cases
         // where memory is zero-initialized or entirely uninitialized
         if intrinsic == "assert_zero_valid"
-            && !self.tcx.permits_zero_init(param_env_and_type).ok().unwrap()
+            && !self
+                .tcx
+                .check_validity_requirement((ValidityRequirement::Zero, param_env_and_type))
+                .unwrap()
         {
             return self.codegen_fatal_error(
                 PropertyClass::SafetyCheck,
@@ -797,8 +800,14 @@ impl<'tcx> GotocCtx<'tcx> {
             );
         }
 
-        if intrinsic == "assert_uninit_valid"
-            && !self.tcx.permits_uninit_init(param_env_and_type).ok().unwrap()
+        if intrinsic == "assert_mem_uninitialized_valid"
+            && !self
+                .tcx
+                .check_validity_requirement((
+                    ValidityRequirement::UninitMitigated0x01Fill,
+                    param_env_and_type,
+                ))
+                .unwrap()
         {
             return self.codegen_fatal_error(
                 PropertyClass::SafetyCheck,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index f33a454ee79d..ed46655f9a37 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -310,7 +310,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         }
                     } else {
                         // otherwise, there is just one field, which is stored as the scalar data
-                        let field = &variant.fields[0];
+                        let field = &variant.fields[0usize.into()];
                         let fty = field.ty(self.tcx, subst);
 
                         let overall_t = self.codegen_ty(ty);
@@ -336,7 +336,7 @@ impl<'tcx> GotocCtx<'tcx> {
                                     &self.symbol_table,
                                 ),
                                 1 => {
-                                    let fty = variant.fields[0].ty(self.tcx, subst);
+                                    let fty = variant.fields[0usize.into()].ty(self.tcx, subst);
                                     self.codegen_single_variant_single_field(
                                         s, span, overall_t, fty,
                                     )
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index dc6938f780f1..f3310498f842 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -11,10 +11,11 @@ use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{Expr, Location, Type};
+use rustc_abi::FieldIdx;
 use rustc_hir::Mutability;
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::{
-    mir::{Field, Local, Place, ProjectionElem},
+    mir::{Local, Place, ProjectionElem},
     ty::{self, Ty, TypeAndMut, VariantDef},
 };
 use rustc_target::abi::{TagEncoding, VariantIdx, Variants};
@@ -238,7 +239,7 @@ impl<'tcx> GotocCtx<'tcx> {
         &mut self,
         res: Expr,
         t: TypeOrVariant<'tcx>,
-        f: &Field,
+        f: &FieldIdx,
     ) -> Result<Expr, UnimplementedData> {
         match t {
             TypeOrVariant::Type(t) => {
@@ -278,12 +279,12 @@ impl<'tcx> GotocCtx<'tcx> {
                     }
                     // if we fall here, then we are handling either a struct or a union
                     ty::Adt(def, _) => {
-                        let field = &def.variants().raw[0].fields[f.index()];
+                        let field = &def.variants().raw[0].fields[*f];
                         Ok(res.member(&field.name.to_string(), &self.symbol_table))
                     }
                     ty::Closure(..) => Ok(res.member(&f.index().to_string(), &self.symbol_table)),
                     ty::Generator(..) => {
-                        let field_name = self.generator_field_name(f.index());
+                        let field_name = self.generator_field_name(f.as_usize());
                         Ok(res
                             .member("direct_fields", &self.symbol_table)
                             .member(field_name, &self.symbol_table))
@@ -293,7 +294,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             // if we fall here, then we are handling an enum
             TypeOrVariant::Variant(v) => {
-                let field = &v.fields[f.index()];
+                let field = &v.fields[*f];
                 Ok(res.member(&field.name.to_string(), &self.symbol_table))
             }
             TypeOrVariant::GeneratorVariant(_var_idx) => {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 29d636cc4150..d9fedc3e507f 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -14,6 +14,8 @@ use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use cbmc::MachineModel;
 use cbmc::{btree_string_map, InternString, InternedString};
 use num::bigint::BigInt;
+use rustc_abi::FieldIdx;
+use rustc_index::vec::IndexVec;
 use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
 use rustc_middle::ty::adjustment::PointerCast;
 use rustc_middle::ty::layout::LayoutOf;
@@ -281,7 +283,11 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Create an initializer for a generator struct.
-    fn codegen_rvalue_generator(&mut self, operands: &[Operand<'tcx>], ty: Ty<'tcx>) -> Expr {
+    fn codegen_rvalue_generator(
+        &mut self,
+        operands: &IndexVec<FieldIdx, Operand<'tcx>>,
+        ty: Ty<'tcx>,
+    ) -> Expr {
         let layout = self.layout_of(ty);
         let discriminant_field = match &layout.variants {
             Variants::Multiple { tag_encoding: TagEncoding::Direct, tag_field, .. } => tag_field,
@@ -320,7 +326,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_rvalue_enum_aggregate(
         &mut self,
         variant_index: VariantIdx,
-        operands: &[Operand<'tcx>],
+        operands: &IndexVec<FieldIdx, Operand<'tcx>>,
         res_ty: Ty<'tcx>,
         loc: Location,
     ) -> Expr {
@@ -362,7 +368,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 variant_expr.typ().clone(),
                 fields
                     .index_by_increasing_offset()
-                    .map(|idx| self.codegen_operand(&operands[idx]))
+                    .map(|idx| self.codegen_operand(&operands[idx.into()]))
                     .collect(),
                 &self.symbol_table,
             );
@@ -381,7 +387,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_rvalue_aggregate(
         &mut self,
         aggregate: &AggregateKind<'tcx>,
-        operands: &[Operand<'tcx>],
+        operands: &IndexVec<FieldIdx, Operand<'tcx>>,
         res_ty: Ty<'tcx>,
         loc: Location,
     ) -> Expr {
@@ -411,8 +417,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 let components = typ.lookup_components(&self.symbol_table).unwrap();
                 Expr::union_expr(
                     typ,
-                    components[active_field_index].name(),
-                    self.codegen_operand(&operands[0]),
+                    components[active_field_index.as_usize()].name(),
+                    self.codegen_operand(&operands[0usize.into()]),
                     &self.symbol_table,
                 )
             }
@@ -426,7 +432,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         .fields
                         .index_by_increasing_offset()
                         .map(|idx| {
-                            let cgo = self.codegen_operand(&operands[idx]);
+                            let cgo = self.codegen_operand(&operands[idx.into()]);
                             // The input operand might actually be a one-element array, as seen
                             // when running assess on firecracker.
                             if *cgo.typ() == vector_element_type {
@@ -449,7 +455,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     layout
                         .fields
                         .index_by_increasing_offset()
-                        .map(|idx| self.codegen_operand(&operands[idx]))
+                        .map(|idx| self.codegen_operand(&operands[idx.into()]))
                         .collect(),
                     &self.symbol_table,
                 )
@@ -499,6 +505,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let t = self.monomorphize(*t);
                 self.codegen_pointer_cast(k, e, t, loc)
             }
+            Rvalue::Cast(rustc_middle::mir::CastKind::Transmute, _, _) => todo!(),
             Rvalue::BinaryOp(op, box (ref e1, ref e2)) => {
                 self.codegen_rvalue_binary_op(op, e1, e2, loc)
             }
@@ -597,7 +604,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     // See also the cranelift backend:
                     // https://github.com/rust-lang/rust/blob/05d22212e89588e7c443cc6b9bc0e4e02fdfbc8d/compiler/rustc_codegen_cranelift/src/discriminant.rs#L116
                     let offset = match &layout.fields {
-                        FieldsShape::Arbitrary { offsets, .. } => offsets[0],
+                        FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()],
                         _ => unreachable!("niche encoding must have arbitrary fields"),
                     };
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 4892ed988e39..38d2018ca0cf 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -86,6 +86,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     location,
                 )
             }
+            StatementKind::PlaceMention(_) => todo!(),
             StatementKind::FakeRead(_)
             | StatementKind::Retag(_, _)
             | StatementKind::AscribeUserType(_, _)
@@ -122,8 +123,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 loc,
                 "https://github.com/model-checking/kani/issues/692",
             ),
-            TerminatorKind::Abort => self.codegen_mimic_unimplemented(
-                "TerminatorKind::Abort",
+            TerminatorKind::Terminate => self.codegen_mimic_unimplemented(
+                "TerminatorKind::Terminate",
                 loc,
                 "https://github.com/model-checking/kani/issues/692",
             ),
@@ -187,9 +188,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     loc,
                 )
             }
-            TerminatorKind::DropAndReplace { .. }
-            | TerminatorKind::FalseEdge { .. }
-            | TerminatorKind::FalseUnwind { .. } => {
+            TerminatorKind::FalseEdge { .. } | TerminatorKind::FalseUnwind { .. } => {
                 unreachable!("drop elaboration removes these TerminatorKind")
             }
             TerminatorKind::Yield { .. } | TerminatorKind::GeneratorDrop => {
@@ -238,7 +237,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
                     if *untagged_variant != variant_index {
                         let offset = match &layout.fields {
-                            FieldsShape::Arbitrary { offsets, .. } => offsets[0],
+                            FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()],
                             _ => unreachable!("niche encoding must have arbitrary fields"),
                         };
                         let discr_ty = self.codegen_enum_discr_typ(dest_ty);
@@ -562,6 +561,7 @@ impl<'tcx> GotocCtx<'tcx> {
                                 .with_location(loc),
                         ]
                     }
+                    InstanceDef::ThreadLocalShim(_) | InstanceDef::FnPtrAddrShim(_, _) => todo!(),
                 };
                 stmts.push(self.codegen_end_call(target.as_ref(), loc));
                 Stmt::block(stmts, loc)
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 6520b330af03..8459c2581381 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -297,7 +297,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         // In addition to `def_id` and `substs`, we need to provide the kind of region `env_region`
         // in `closure_env_ty`, which we can build from the bound variables as follows
-        let bound_vars = self.tcx.mk_bound_variable_kinds(
+        let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
             sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
         );
         let br = ty::BoundRegion {
@@ -314,7 +314,7 @@ impl<'tcx> GotocCtx<'tcx> {
         //  * the rest of attributes are obtained from `sig`
         let sig = ty::Binder::bind_with_vars(
             self.tcx.mk_fn_sig(
-                iter::once(env_ty).chain(iter::once(sig.inputs()[0])),
+                [env_ty, sig.inputs()[0]],
                 sig.output(),
                 sig.c_variadic,
                 sig.unsafety,
@@ -338,7 +338,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ) -> ty::PolyFnSig<'tcx> {
         let sig = substs.as_generator().poly_sig();
 
-        let bound_vars = self.tcx.mk_bound_variable_kinds(
+        let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
             sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
         );
         let br = ty::BoundRegion {
@@ -346,11 +346,11 @@ impl<'tcx> GotocCtx<'tcx> {
             kind: ty::BoundRegionKind::BrEnv,
         };
         let env_region = ty::ReLateBound(ty::INNERMOST, br);
-        let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region(env_region), ty);
+        let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region_from_kind(env_region), ty);
 
         let pin_did = self.tcx.require_lang_item(LangItem::Pin, None);
         let pin_adt_ref = self.tcx.adt_def(pin_did);
-        let pin_substs = self.tcx.intern_substs(&[env_ty.into()]);
+        let pin_substs = self.tcx.mk_substs(&[env_ty.into()]);
         let env_ty = self.tcx.mk_adt(pin_adt_ref, pin_substs);
 
         let sig = sig.skip_binder();
@@ -363,7 +363,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // The signature should be `Future::poll(_, &mut Context<'_>) -> Poll<Output>`
             let poll_did = tcx.require_lang_item(LangItem::Poll, None);
             let poll_adt_ref = tcx.adt_def(poll_did);
-            let poll_substs = tcx.intern_substs(&[sig.return_ty.into()]);
+            let poll_substs = tcx.mk_substs(&[sig.return_ty.into()]);
             let ret_ty = tcx.mk_adt(poll_adt_ref, poll_substs);
 
             // We have to replace the `ResumeTy` that is used for type and borrow checking
@@ -384,7 +384,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // The signature should be `Generator::resume(_, Resume) -> GeneratorState<Yield, Return>`
             let state_did = tcx.require_lang_item(LangItem::GeneratorState, None);
             let state_adt_ref = tcx.adt_def(state_did);
-            let state_substs = tcx.intern_substs(&[sig.yield_ty.into(), sig.return_ty.into()]);
+            let state_substs = tcx.mk_substs(&[sig.yield_ty.into(), sig.return_ty.into()]);
             let ret_ty = tcx.mk_adt(state_adt_ref, state_substs);
 
             (sig.resume_ty, ret_ty)
@@ -392,8 +392,8 @@ impl<'tcx> GotocCtx<'tcx> {
 
         ty::Binder::bind_with_vars(
             tcx.mk_fn_sig(
-                [env_ty, resume_ty].iter(),
-                &ret_ty,
+                [env_ty, resume_ty],
+                ret_ty,
                 false,
                 Unsafety::Normal,
                 rustc_target::spec::abi::Abi::Rust,
@@ -423,7 +423,7 @@ impl<'tcx> GotocCtx<'tcx> {
 impl<'tcx> GotocCtx<'tcx> {
     pub fn monomorphize<T>(&self, value: T) -> T
     where
-        T: TypeFoldable<'tcx>,
+        T: TypeFoldable<TyCtxt<'tcx>>,
     {
         // Instance is Some(..) only when current codegen unit is a function.
         if let Some(current_fn) = &self.current_fn {
@@ -937,7 +937,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let mut final_fields = Vec::with_capacity(flds.len());
                 let mut offset = initial_offset;
                 for idx in layout.fields.index_by_increasing_offset() {
-                    let fld_offset = offsets[idx];
+                    let fld_offset = offsets[idx.into()];
                     let (fld_name, fld_ty) = &flds[idx];
                     if let Some(padding) =
                         self.codegen_struct_padding(offset, fld_offset, final_fields.len())
@@ -1804,6 +1804,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     let components = fields_shape
                         .index_by_increasing_offset()
                         .map(|idx| {
+                            let idx = idx.into();
                             let name = fields[idx].name.to_string().intern();
                             let field_ty = fields[idx].ty(ctx.tcx, adt_substs);
                             let typ = if !ctx.is_zst(field_ty) {
@@ -1839,8 +1840,8 @@ impl<'tcx> GotocCtx<'tcx> {
         while let ty::Adt(adt_def, adt_substs) = typ.kind() {
             assert_eq!(adt_def.variants().len(), 1, "Expected a single-variant ADT. Found {typ:?}");
             let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields;
-            let last_field = fields.last().expect("Trait should be the last element.");
-            typ = last_field.ty(self.tcx, adt_substs);
+            let last_field = fields.last_index().expect("Trait should be the last element.");
+            typ = fields[last_field].ty(self.tcx, adt_substs);
         }
         if typ.is_trait() { Some(typ) } else { None }
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 100fba0ef281..c86b0cd1bc47 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -23,7 +23,7 @@ use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_codegen_ssa::{CodegenResults, CrateInfo};
 use rustc_data_structures::fx::FxHashMap;
 use rustc_data_structures::temp_dir::MaybeTempDir;
-use rustc_errors::ErrorGuaranteed;
+use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
 use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
@@ -86,6 +86,11 @@ impl CodegenBackend for GotocCodegenBackend {
         println!("Kani-goto version: {}", env!("CARGO_PKG_VERSION"));
     }
 
+    fn locale_resource(&self) -> &'static str {
+        // We don't currently support multiple languages.
+        DEFAULT_LOCALE_RESOURCE
+    }
+
     fn codegen_crate(
         &self,
         tcx: TyCtxt,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 1d9d2fbaa403..cfcaaaae8fb9 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -24,9 +24,6 @@ use cbmc::{MachineModel, RoundingMode};
 use kani_metadata::{HarnessMetadata, UnsupportedFeature};
 use kani_queries::{QueryDb, UserInput};
 use rustc_data_structures::fx::FxHashMap;
-use rustc_data_structures::owning_ref::OwningRef;
-use rustc_data_structures::rustc_erase_owner;
-use rustc_data_structures::sync::MetadataRef;
 use rustc_middle::mir::interpret::Allocation;
 use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
@@ -34,14 +31,11 @@ use rustc_middle::ty::layout::{
     TyAndLayout,
 };
 use rustc_middle::ty::{self, Instance, Ty, TyCtxt};
-use rustc_session::cstore::MetadataLoader;
 use rustc_session::Session;
 use rustc_span::source_map::{respan, Span};
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::Endian;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
-use rustc_target::spec::Target;
-use std::path::Path;
 
 pub struct GotocCtx<'tcx> {
     /// the typing context
@@ -422,19 +416,6 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> {
     }
 }
 
-pub struct GotocMetadataLoader();
-impl MetadataLoader for GotocMetadataLoader {
-    fn get_rlib_metadata(&self, _: &Target, _filename: &Path) -> Result<MetadataRef, String> {
-        let buf = vec![];
-        let buf: OwningRef<Vec<u8>, [u8]> = OwningRef::new(buf);
-        Ok(rustc_erase_owner!(buf.map_owner_box()))
-    }
-
-    fn get_dylib_metadata(&self, target: &Target, filename: &Path) -> Result<MetadataRef, String> {
-        self.get_rlib_metadata(target, filename)
-    }
-}
-
 /// Builds a machine model which is required by CBMC
 fn machine_model_from_session(sess: &Session) -> MachineModel {
     // The model assumes a `x86_64-unknown-linux-gnu`, `x86_64-apple-darwin`
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 0b69b856940a..86757ea3ad11 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -5,7 +5,7 @@
 use std::collections::BTreeMap;
 
 use kani_metadata::{CbmcSolver, HarnessAttributes, Stub};
-use rustc_ast::{AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem};
+use rustc_ast::{attr, AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem};
 use rustc_hir::{def::DefKind, def_id::DefId};
 use rustc_middle::ty::{self, Instance, TyCtxt};
 use rustc_span::Span;
@@ -58,7 +58,7 @@ pub fn is_proof_harness(tcx: TyCtxt, def_id: DefId) -> bool {
 /// Does this `def_id` have `#[rustc_test_marker]`?
 pub fn is_test_harness_description(tcx: TyCtxt, def_id: DefId) -> bool {
     let attrs = tcx.get_attrs_unchecked(def_id);
-    tcx.sess.contains_name(attrs, rustc_span::symbol::sym::rustc_test_marker)
+    attr::contains_name(attrs, rustc_span::symbol::sym::rustc_test_marker)
 }
 
 /// Is this the closure inside of a test description const (i.e. macro expanded from a `#[test]`)?
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 71ddd457e075..3c87a8173b3f 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -184,7 +184,7 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
 
                 let CustomCoerceUnsized::Struct(coerce_index) =
                     custom_coerce_unsize_info(self.tcx, src_ty, dst_ty);
-                assert!(coerce_index < src_fields.len());
+                assert!(coerce_index.as_usize() < src_fields.len());
 
                 self.src_ty = Some(src_fields[coerce_index].ty(self.tcx, src_substs));
                 self.dst_ty = Some(dst_fields[coerce_index].ty(self.tcx, dst_substs));
diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs
index 03cf5bd5d9f6..aaef3037ad7b 100644
--- a/kani-compiler/src/kani_middle/provide.rs
+++ b/kani-compiler/src/kani_middle/provide.rs
@@ -8,7 +8,7 @@ use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_ite
 use crate::kani_middle::stubbing;
 use crate::kani_middle::ty::query::query_provided::collect_and_partition_mono_items;
 use kani_queries::{QueryDb, UserInput};
-use rustc_hir::def_id::DefId;
+use rustc_hir::def_id::{DefId, LocalDefId};
 use rustc_interface;
 use rustc_middle::{
     mir::Body,
@@ -18,7 +18,7 @@ use rustc_middle::{
 /// Sets up rustc's query mechanism to apply Kani's custom queries to code from
 /// the present crate.
 pub fn provide(providers: &mut Providers, queries: &QueryDb) {
-    providers.optimized_mir = run_mir_passes::<false>;
+    providers.optimized_mir = run_mir_passes;
     if queries.get_stubbing_enabled() {
         providers.collect_and_partition_mono_items = collect_and_partition_mono_items;
     }
@@ -27,23 +27,25 @@ pub fn provide(providers: &mut Providers, queries: &QueryDb) {
 /// Sets up rustc's query mechanism to apply Kani's custom queries to code from
 /// external crates.
 pub fn provide_extern(providers: &mut ExternProviders) {
-    providers.optimized_mir = run_mir_passes::<true>;
+    providers.optimized_mir = run_mir_passes_extern;
 }
 
-/// Returns the optimized code for the function associated with `def_id` by
+/// Returns the optimized code for the external function associated with `def_id` by
 /// running rustc's optimization passes followed by Kani-specific passes.
-fn run_mir_passes<const EXTERN: bool>(tcx: TyCtxt, def_id: DefId) -> &Body {
-    tracing::debug!(?def_id, "Run rustc transformation passes");
-    let optimized_mir = if EXTERN {
-        rustc_interface::DEFAULT_EXTERN_QUERY_PROVIDERS.optimized_mir
-    } else {
-        rustc_interface::DEFAULT_QUERY_PROVIDERS.optimized_mir
-    };
-    let body = optimized_mir(tcx, def_id);
-
+fn run_mir_passes_extern(tcx: TyCtxt, def_id: DefId) -> &Body {
+    tracing::debug!(?def_id, "run_mir_passes_extern");
+    let body = (rustc_interface::DEFAULT_EXTERN_QUERY_PROVIDERS.optimized_mir)(tcx, def_id);
     run_kani_mir_passes(tcx, def_id, body)
 }
 
+/// Returns the optimized code for the local function associated with `def_id` by
+/// running rustc's optimization passes followed by Kani-specific passes.
+fn run_mir_passes(tcx: TyCtxt, def_id: LocalDefId) -> &Body {
+    tracing::debug!(?def_id, "run_mir_passes");
+    let body = (rustc_interface::DEFAULT_QUERY_PROVIDERS.optimized_mir)(tcx, def_id);
+    run_kani_mir_passes(tcx, def_id.to_def_id(), body)
+}
+
 /// Returns the optimized code for the function associated with `def_id` by
 /// running Kani-specific passes. The argument `body` should be the optimized
 /// code rustc generates for this function.
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index 7845f4bab4ca..14fea7d11022 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -215,7 +215,7 @@ struct MonoItemsFnCollector<'a, 'tcx> {
 impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
     fn monomorphize<T>(&self, value: T) -> T
     where
-        T: TypeFoldable<'tcx>,
+        T: TypeFoldable<TyCtxt<'tcx>>,
     {
         trace!(instance=?self.instance, ?value, "monomorphize");
         self.instance.subst_mir_and_normalize_erasing_regions(
@@ -283,6 +283,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
             | InstanceDef::Item(..)
             | InstanceDef::ReifyShim(..)
             | InstanceDef::VTableShim(..) => true,
+            InstanceDef::ThreadLocalShim(_) | InstanceDef::FnPtrAddrShim(_, _) => todo!(),
         };
         if should_collect && should_codegen_locally(self.tcx, &instance) {
             trace!(?instance, "collect_instance");
@@ -487,8 +488,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
                     );
                 }
             }
-            TerminatorKind::Drop { ref place, .. }
-            | TerminatorKind::DropAndReplace { ref place, .. } => {
+            TerminatorKind::Drop { ref place, .. } => {
                 let place_ty = place.ty(self.body, self.tcx).ty;
                 let place_mono_ty = self.monomorphize(place_ty);
                 let instance = Instance::resolve_drop_in_place(self.tcx, place_mono_ty);
@@ -498,7 +498,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
                 // We don't support inline assembly. This shall be replaced by an unsupported
                 // construct during codegen.
             }
-            TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => {
+            TerminatorKind::Terminate { .. } | TerminatorKind::Assert { .. } => {
                 // We generate code for this without invoking any lang item.
             }
             TerminatorKind::Goto { .. }
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index d89521719dd7..f532ca49d66e 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -10,10 +10,11 @@
 #![feature(extern_types)]
 #![recursion_limit = "256"]
 #![feature(box_patterns)]
-#![feature(once_cell)]
 #![feature(rustc_private)]
+#![feature(lazy_cell)]
 #![feature(more_qualified_paths)]
 #![feature(iter_intersperse)]
+extern crate rustc_abi;
 extern crate rustc_ast;
 extern crate rustc_codegen_ssa;
 extern crate rustc_data_structures;
diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs
index 99d7b7239d05..3900aba5e82f 100644
--- a/kani-compiler/src/session.rs
+++ b/kani-compiler/src/session.rs
@@ -48,7 +48,7 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send
             // Print stack trace.
             let msg = format!("Kani unexpectedly panicked at {info}.",);
             let fallback_bundle =
-                fallback_fluent_bundle(rustc_errors::DEFAULT_LOCALE_RESOURCES, false);
+                fallback_fluent_bundle(rustc_driver::DEFAULT_LOCALE_RESOURCES.to_vec(), false);
             let mut emitter = JsonEmitter::basic(
                 false,
                 HumanReadableErrorType::Default(ColorConfig::Never),
@@ -71,10 +71,7 @@ pub fn init_session(args: &ArgMatches, json_hook: bool) {
     // Initialize the rustc logger using value from RUSTC_LOG. We keep the log control separate
     // because we cannot control the RUSTC log format unless if we match the exact tracing
     // version used by RUSTC.
-    // TODO: Enable rustc log when we upgrade the toolchain.
-    // <https://github.com/model-checking/kani/issues/2283>
-    //
-    // rustc_driver::init_rustc_env_logger();
+    rustc_driver::init_rustc_env_logger();
 
     // Install Kani panic hook.
     if json_hook {
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 5ce9d4ff0e42..968c1e04951e 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-02-18"
+channel = "nightly-2023-04-16"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs
index 2178159bbaf1..17db46389576 100644
--- a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs
+++ b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs
@@ -9,7 +9,7 @@
 // run-pass
 // Test that box-statements with yields in them work.
 
-#![feature(generators, box_syntax, generator_trait)]
+#![feature(generators, generator_trait)]
 use std::ops::Generator;
 use std::ops::GeneratorState;
 use std::pin::Pin;
@@ -22,14 +22,14 @@ fn main() {
         //~ WARN unused generator that must be used
         let y = 2u32;
         {
-            let _t = box (&x, yield 0, &y);
+            let _t = Box::new(&x, yield 0, &y);
         }
-        match box (&x, yield 0, &y) {
+        match Box::new(&x, yield 0, &y) {
             _t => {}
         }
     };
 
-    let mut g = |_| box yield;
+    let mut g = |_| Box::new(yield);
     assert_eq!(Pin::new(&mut g).resume(1), GeneratorState::Yielded(()));
     assert_eq!(Pin::new(&mut g).resume(2), GeneratorState::Complete(box 2));
 }
diff --git a/tools/bookrunner/librustdoc/doctest.rs b/tools/bookrunner/librustdoc/doctest.rs
index 58f6ea8d1b18..5d11ea7ec55b 100644
--- a/tools/bookrunner/librustdoc/doctest.rs
+++ b/tools/bookrunner/librustdoc/doctest.rs
@@ -4,6 +4,7 @@
 // See GitHub history for details.
 use rustc_ast as ast;
 use rustc_data_structures::sync::Lrc;
+use rustc_driver::DEFAULT_LOCALE_RESOURCES;
 use rustc_errors::{ColorConfig, TerminalUrl};
 use rustc_span::edition::Edition;
 use rustc_span::source_map::SourceMap;
@@ -79,7 +80,7 @@ pub fn make_test(
             let sm = Lrc::new(SourceMap::new(FilePathMapping::empty()));
 
             let fallback_bundle =
-                rustc_errors::fallback_fluent_bundle(rustc_errors::DEFAULT_LOCALE_RESOURCES, false);
+                rustc_errors::fallback_fluent_bundle(DEFAULT_LOCALE_RESOURCES.to_vec(), false);
             supports_color = EmitterWriter::stderr(
                 ColorConfig::Auto,
                 None,
@@ -95,7 +96,7 @@ pub fn make_test(
             .supports_color();
 
             let emitter = EmitterWriter::new(
-                box io::sink(),
+                Box::new(io::sink()),
                 None,
                 None,
                 fallback_bundle,
@@ -109,7 +110,7 @@ pub fn make_test(
             );
 
             // FIXME(misdreavus): pass `-Z treat-err-as-bug` to the doctest parser
-            let handler = Handler::with_emitter(false, None, box emitter);
+            let handler = Handler::with_emitter(false, None, Box::new(emitter));
             let sess = ParseSess::with_span_handler(handler, sm);
 
             let mut found_main = false;
diff --git a/tools/bookrunner/librustdoc/lib.rs b/tools/bookrunner/librustdoc/lib.rs
index 57ae24335c2a..9046478cf502 100644
--- a/tools/bookrunner/librustdoc/lib.rs
+++ b/tools/bookrunner/librustdoc/lib.rs
@@ -11,10 +11,8 @@
 #![feature(assert_matches)]
 #![feature(box_patterns)]
 #![feature(control_flow_enum)]
-#![feature(box_syntax)]
 #![feature(test)]
 #![feature(never_type)]
-#![feature(once_cell)]
 #![feature(type_ascription)]
 #![feature(iter_intersperse)]
 #![recursion_limit = "256"]
diff --git a/tools/compiletest/src/header.rs b/tools/compiletest/src/header.rs
index afb9057ad451..89e3603a8510 100644
--- a/tools/compiletest/src/header.rs
+++ b/tools/compiletest/src/header.rs
@@ -233,5 +233,11 @@ pub fn make_test_description<R: Read>(
         compile_fail: false,
         no_run: false,
         test_type: test::TestType::Unknown,
+        // Enter dummy values since the test doesn't have a line per-se.
+        source_file: "unknown_file",
+        start_line: 0,
+        start_col: 0,
+        end_line: 0,
+        end_col: 0,
     }
 }

From befb8ddf77a49c891b49943c4bd1da9046f548fd Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 19 Apr 2023 16:33:51 -0700
Subject: [PATCH 2/9] Fix runtime issues

  - Discriminant calculation
  - Implement Cast transmute
  - Misaligned assertion check error message
  - Codegen ZST constant
  - Is user variable detection
---
 cprover_bindings/src/goto_program/expr.rs     | 25 +++++++++++++------
 .../codegen_cprover_gotoc/codegen/function.rs |  2 +-
 .../codegen_cprover_gotoc/codegen/operand.rs  |  2 +-
 .../codegen_cprover_gotoc/codegen/rvalue.rs   |  5 +++-
 .../codegen/statement.rs                      | 12 +++++++--
 .../src/codegen_cprover_gotoc/utils/names.rs  |  4 +++
 ...doesnt_call_crate_with_global_asm.expected |  1 -
 7 files changed, 38 insertions(+), 13 deletions(-)

diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 7aae03f1538a..8fb5f4d6a28b 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -131,7 +131,7 @@ pub enum ExprValue {
     StringConstant {
         s: InternedString,
     },
-    /// Struct initializer  
+    /// Struct initializer
     /// `struct foo the_foo = >>> {field1, field2, ... } <<<`
     Struct {
         values: Vec<Expr>,
@@ -142,7 +142,7 @@ pub enum ExprValue {
     },
     /// `(typ) self`. Target type is in the outer `Expr` struct.
     Typecast(Expr),
-    /// Union initializer  
+    /// Union initializer
     /// `union foo the_foo = >>> {.field = value } <<<`
     Union {
         value: Expr,
@@ -681,7 +681,7 @@ impl Expr {
         expr!(StatementExpression { statements: ops }, typ)
     }
 
-    /// Internal helper function for Struct initalizer  
+    /// Internal helper function for Struct initalizer
     /// `struct foo the_foo = >>> {.field1 = val1, .field2 = val2, ... } <<<`
     /// ALL fields must be given, including padding
     fn struct_expr_with_explicit_padding(
@@ -698,7 +698,7 @@ impl Expr {
         expr!(Struct { values }, typ)
     }
 
-    /// Struct initializer  
+    /// Struct initializer
     /// `struct foo the_foo = >>> {.field1 = val1, .field2 = val2, ... } <<<`
     /// Note that only the NON padding fields should be explicitly given.
     /// Padding fields are automatically inserted using the type from the `SymbolTable`
@@ -764,7 +764,7 @@ impl Expr {
         Expr::struct_expr_from_values(typ, values, symbol_table)
     }
 
-    /// Struct initializer  
+    /// Struct initializer
     /// `struct foo the_foo = >>> {field1, field2, ... } <<<`
     /// Note that only the NON padding fields should be explicitly given.
     /// Padding fields are automatically inserted using the type from the `SymbolTable`
@@ -800,7 +800,7 @@ impl Expr {
         Expr::struct_expr_with_explicit_padding(typ, fields, values)
     }
 
-    /// Struct initializer  
+    /// Struct initializer
     /// `struct foo the_foo = >>> {field1, padding2, field3, ... } <<<`
     /// Note that padding fields should be explicitly given.
     /// This would be used when the values and padding have already been combined,
@@ -829,6 +829,17 @@ impl Expr {
         Expr::struct_expr_with_explicit_padding(typ, fields, values)
     }
 
+    /// Initializer for a zero sized type (ZST).
+    /// Since this is a ZST, we call nondet to simplify everything.
+    pub fn init_unit(typ: Type, symbol_table: &SymbolTable) -> Self {
+        assert!(
+            typ.is_struct_tag(),
+            "Zero sized types should be represented as struct: but found: {typ:?}"
+        );
+        assert_eq!(typ.sizeof_in_bits(symbol_table), 0);
+        Expr::nondet(typ)
+    }
+
     /// `identifier`
     pub fn symbol_expression<T: Into<InternedString>>(identifier: T, typ: Type) -> Self {
         let identifier = identifier.into();
@@ -859,7 +870,7 @@ impl Expr {
         self.transmute_to(t, st)
     }
 
-    /// Union initializer  
+    /// Union initializer
     /// `union foo the_foo = >>> {.field = value } <<<`
     pub fn union_expr<T: Into<InternedString>>(
         typ: Type,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
index b7c98a4a2314..5e7a591396fd 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -53,7 +53,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 var_type,
                 self.codegen_span(&ldata.source_info.span),
             )
-            .with_is_hidden(!ldata.is_user_variable())
+            .with_is_hidden(!self.is_user_variable(&lc))
             .with_is_parameter((idx > 0 && idx <= num_args) && !self.is_zst(var_ty));
             let sym_e = sym.to_expr();
             self.symbol_table.insert(sym);
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index ed46655f9a37..b4236a034594 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -141,7 +141,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ConstValue::ZeroSized => match lit_ty.kind() {
                 // Rust "function items" (not closures, not function pointers, see `codegen_fndef`)
                 ty::FnDef(d, substs) => self.codegen_fndef(*d, substs, span),
-                _ => unimplemented!(),
+                _ => Expr::init_unit(self.codegen_ty(lit_ty), &self.symbol_table),
             },
         }
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index d9fedc3e507f..04a86b7ff29a 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -505,7 +505,10 @@ impl<'tcx> GotocCtx<'tcx> {
                 let t = self.monomorphize(*t);
                 self.codegen_pointer_cast(k, e, t, loc)
             }
-            Rvalue::Cast(rustc_middle::mir::CastKind::Transmute, _, _) => todo!(),
+            Rvalue::Cast(CastKind::Transmute, operand, ty) => {
+                let goto_typ = self.codegen_ty(self.monomorphize(*ty));
+                self.codegen_operand(operand).transmute_to(goto_typ, &self.symbol_table)
+            }
             Rvalue::BinaryOp(op, box (ref e1, ref e2)) => {
                 self.codegen_rvalue_binary_op(op, e1, e2, loc)
             }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 38d2018ca0cf..8e96272a08c5 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -166,6 +166,10 @@ impl<'tcx> GotocCtx<'tcx> {
                     // "index out of bounds: the length is {len} but the index is {index}",
                     // but CBMC only accepts static messages so we don't add values to the message.
                     "index out of bounds: the length is less than or equal to the given index"
+                } else if let AssertKind::MisalignedPointerDereference { .. } = msg {
+                    // Misaligned pointer dereference check messages is also a runtime messages.
+                    // Generate a generic one here.
+                    "misaligned pointer dereference: address must be a multiple of its type's alignment"
                 } else {
                     // For all other assert kind we can get the static message.
                     msg.description()
@@ -231,8 +235,11 @@ impl<'tcx> GotocCtx<'tcx> {
                     // DISCRIMINANT - val:255 ty:i8
                     // DISCRIMINANT - val:0 ty:i8
                     // DISCRIMINANT - val:1 ty:i8
-                    let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t));
-                    self.codegen_discriminant_field(dest_expr, dest_ty).assign(discr, location)
+                    trace!(?discr, ?discr_t, ?dest_ty, "codegen_set_discriminant direct");
+                    // The discr.ty doesn't always match the tag type. Explicitly cast if needed.
+                    let discr_expr = Expr::int_constant(discr.val, self.codegen_ty(discr.ty))
+                        .cast_to(self.codegen_ty(discr_t));
+                    self.codegen_discriminant_field(dest_expr, dest_ty).assign(discr_expr, location)
                 }
                 TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
                     if *untagged_variant != variant_index {
@@ -244,6 +251,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         let discr_ty = self.codegen_ty(discr_ty);
                         let niche_value = variant_index.as_u32() - niche_variants.start().as_u32();
                         let niche_value = (niche_value as u128).wrapping_add(*niche_start);
+                        trace!(val=?niche_value, typ=?discr_ty, "codegen_set_discriminant niche");
                         let value = if niche_value == 0
                             && matches!(tag.primitive(), Primitive::Pointer(_))
                         {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
index b2c4345109f1..8eaf537f2e31 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
@@ -34,6 +34,10 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    pub fn is_user_variable(&self, var: &Local) -> bool {
+        self.find_debug_info(var).is_some()
+    }
+
     // Special naming conventions for parameters that are spread from a tuple
     // into its individual components at the LLVM level, see comment at
     // compiler/rustc_codegen_llvm/src/gotoc/mod.rs:codegen_function_prelude
diff --git a/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected b/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected
index 59aa1503d9a4..961b5f960b0b 100644
--- a/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected
+++ b/tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected
@@ -1,2 +1 @@
 error: Crate crate_with_global_asm contains global ASM, which is not supported by Kani. Rerun with `--enable-unstable --ignore-global-asm` to suppress this error (**Verification results may be impacted**).
-error: could not compile `crate_with_global_asm` due to 2 previous errors

From 00d3fba7cfa2a12b7ca54faf9d0e6fe2eb6142a8 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 20 Apr 2023 00:13:04 -0700
Subject: [PATCH 3/9] Define different function for concrete playback

It looks like the `if cfg!()` is no longer being propagated and the
concrete playback code is increasing the logic that the compiler detects
as reachable.
---
 library/kani/src/lib.rs | 41 ++++++++++++++++++++++++++++-------------
 1 file changed, 28 insertions(+), 13 deletions(-)

diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index e82b57d35457..7807a4068beb 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -48,10 +48,16 @@ pub use futures::block_on;
 /// ```
 #[inline(never)]
 #[rustc_diagnostic_item = "KaniAssume"]
-pub fn assume(_cond: bool) {
-    if cfg!(feature = "concrete_playback") {
-        assert!(_cond, "kani::assume should always hold");
-    }
+#[cfg(not(feature = "concrete_playback"))]
+pub fn assume(cond: bool) {
+    let _ = cond;
+}
+
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniAssume"]
+#[cfg(feature = "concrete_playback")]
+pub fn assume(cond: bool) {
+    assert!(cond, "kani::assume should always hold");
 }
 
 /// Creates an assertion of the specified condition and message.
@@ -63,12 +69,19 @@ pub fn assume(_cond: bool) {
 /// let y = !x;
 /// kani::assert(x || y, "ORing a boolean variable with its negation must be true")
 /// ```
+#[cfg(not(feature = "concrete_playback"))]
+#[inline(never)]
+#[rustc_diagnostic_item = "KaniAssert"]
+pub const fn assert(cond: bool, msg: &'static str) {
+    let _ = cond;
+    let _ = msg;
+}
+
+#[cfg(feature = "concrete_playback")]
 #[inline(never)]
 #[rustc_diagnostic_item = "KaniAssert"]
-pub const fn assert(_cond: bool, _msg: &'static str) {
-    if cfg!(feature = "concrete_playback") {
-        assert!(_cond, "{}", _msg);
-    }
+pub const fn assert(cond: bool, msg: &'static str) {
+    assert!(cond, "{}", msg);
 }
 
 /// Creates a cover property with the specified condition and message.
@@ -153,15 +166,17 @@ pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T {
 ///
 /// Note that SIZE_T must be equal the size of type T in bytes.
 #[inline(never)]
+#[cfg(not(feature = "concrete_playback"))]
 pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
-    #[cfg(feature = "concrete_playback")]
-    return concrete_playback::any_raw_internal::<T, SIZE_T>();
-
-    #[cfg(not(feature = "concrete_playback"))]
-    #[allow(unreachable_code)]
     any_raw_inner::<T>()
 }
 
+#[inline(never)]
+#[cfg(feature = "concrete_playback")]
+pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
+    return concrete_playback::any_raw_internal::<T, SIZE_T>();
+}
+
 /// This low-level function returns nondet bytes of size T.
 #[rustc_diagnostic_item = "KaniAnyRaw"]
 #[inline(never)]

From aee643bf77dc7752e804e79a938d6f9ba0856f22 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 20 Apr 2023 10:18:52 +0200
Subject: [PATCH 4/9] Update yield-in-box.rs

Fix parenthesis
---
 tests/kani/Generator/rustc-generator-tests/yield-in-box.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs
index 17db46389576..c320c2c16418 100644
--- a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs
+++ b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs
@@ -22,14 +22,14 @@ fn main() {
         //~ WARN unused generator that must be used
         let y = 2u32;
         {
-            let _t = Box::new(&x, yield 0, &y);
+            let _t = Box::new((&x, yield 0, &y));
         }
-        match Box::new(&x, yield 0, &y) {
+        match Box::new((&x, yield 0, &y)) {
             _t => {}
         }
     };
 
     let mut g = |_| Box::new(yield);
     assert_eq!(Pin::new(&mut g).resume(1), GeneratorState::Yielded(()));
-    assert_eq!(Pin::new(&mut g).resume(2), GeneratorState::Complete(box 2));
+    assert_eq!(Pin::new(&mut g).resume(2), GeneratorState::Complete(Box::new(2)));
 }

From 725f586ea07677fa4da1be9432bebd00425b8064 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 25 Apr 2023 18:02:05 -0700
Subject: [PATCH 5/9] Fix performance issue due to checked operation use

---
 cprover_bindings/src/goto_program/expr.rs     | 13 +++-
 .../codegen/intrinsic.rs                      | 67 ++++++++---------
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 72 ++++++++++++++-----
 tests/ui/cbmc_checks/signed-overflow/expected |  9 +--
 .../ui/cbmc_checks/unsigned-overflow/expected | 10 +--
 5 files changed, 103 insertions(+), 68 deletions(-)

diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 8fb5f4d6a28b..70c9f97c24fe 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -1392,9 +1392,9 @@ impl Expr {
         ArithmeticOverflowResult { result, overflowed }
     }
 
-    /// Uses CBMC's add-with-overflow operation that performs a single addition
+    /// Uses CBMC's [binop]-with-overflow operation that performs a single addition
     /// operation
-    /// `struct (T, bool) overflow(+, self, e)` where `T` is the type of `self`
+    /// `struct (T, bool) overflow(binop, self, e)` where `T` is the type of `self`
     /// Pseudocode:
     /// ```
     /// struct overflow_result_t {
@@ -1406,6 +1406,14 @@ impl Expr {
     /// overflow_result.overflowed = raw_result > maximum value of T;
     /// return overflow_result;
     /// ```
+    pub fn overflow_op(self, op: BinaryOperator, e: Expr) -> Expr {
+        assert!(
+            matches!(op, OverflowResultMinus | OverflowResultMult | OverflowResultPlus),
+            "Expected an overflow operation, but found: `{op:?}`"
+        );
+        self.binop(op, e)
+    }
+
     pub fn add_overflow_result(self, e: Expr) -> Expr {
         self.binop(OverflowResultPlus, e)
     }
@@ -1437,6 +1445,7 @@ impl Expr {
 
     /// `ArithmeticOverflowResult r; >>>r.overflowed = builtin_sub_overflow(self, e, &r.result)<<<`
     pub fn mul_overflow(self, e: Expr) -> ArithmeticOverflowResult {
+        // TODO: Should we always use the one below?
         let result = self.clone().mul(e.clone());
         let overflowed = self.mul_overflow_p(e);
         ArithmeticOverflowResult { result, overflowed }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 081ab52adbe1..0ded815c53f0 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -5,8 +5,8 @@ use super::typ::{self, pointee_type};
 use super::PropertyClass;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{
-    arithmetic_overflow_result_type, ArithmeticOverflowResult, BuiltinFn, Expr, Location, Stmt,
-    Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
+    arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr,
+    Location, Stmt, Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
 };
 use rustc_middle::mir::{BasicBlock, Operand, Place};
 use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement};
@@ -172,38 +172,6 @@ impl<'tcx> GotocCtx<'tcx> {
             }};
         }
 
-        // Intrinsics of the form *_with_overflow
-        macro_rules! codegen_op_with_overflow {
-            ($f:ident) => {{
-                let pt = self.place_ty(p);
-                let t = self.codegen_ty(pt);
-                let a = fargs.remove(0);
-                let b = fargs.remove(0);
-                let op_type = a.typ().clone();
-                let res = a.$f(b);
-                // add to symbol table
-                let struct_tag = self.codegen_arithmetic_overflow_result_type(op_type.clone());
-                assert_eq!(*res.typ(), struct_tag);
-
-                // store the result in a temporary variable
-                let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc);
-                // cast into result type
-                let e = Expr::struct_expr_from_values(
-                    t.clone(),
-                    vec![
-                        var.clone().member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table),
-                        var.member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table)
-                            .cast_to(Type::c_bool()),
-                    ],
-                    &self.symbol_table,
-                );
-                self.codegen_expr_to_place(
-                    p,
-                    Expr::statement_expression(vec![decl, e.as_stmt(loc)], t),
-                )
-            }};
-        }
-
         // Intrinsics which encode a simple arithmetic operation with overflow check
         macro_rules! codegen_op_with_overflow_check {
             ($f:ident) => {{
@@ -362,7 +330,9 @@ impl<'tcx> GotocCtx<'tcx> {
         }
 
         match intrinsic {
-            "add_with_overflow" => codegen_op_with_overflow!(add_overflow_result),
+            "add_with_overflow" => {
+                self.codegen_op_with_overflow(BinaryOperator::OverflowResultPlus, fargs, p, loc)
+            }
             "arith_offset" => self.codegen_offset(intrinsic, instance, fargs, p, loc),
             "assert_inhabited" => self.codegen_assert_intrinsic(instance, intrinsic, span),
             "assert_mem_uninitialized_valid" => {
@@ -528,7 +498,9 @@ impl<'tcx> GotocCtx<'tcx> {
             "min_align_of_val" => codegen_size_align!(align),
             "minnumf32" => codegen_simple_intrinsic!(Fminf),
             "minnumf64" => codegen_simple_intrinsic!(Fmin),
-            "mul_with_overflow" => codegen_op_with_overflow!(mul_overflow_result),
+            "mul_with_overflow" => {
+                self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, p, loc)
+            }
             "nearbyintf32" => codegen_simple_intrinsic!(Nearbyintf),
             "nearbyintf64" => codegen_simple_intrinsic!(Nearbyint),
             "needs_drop" => codegen_intrinsic_const!(),
@@ -615,7 +587,9 @@ impl<'tcx> GotocCtx<'tcx> {
             "size_of_val" => codegen_size_align!(size),
             "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)),
             "sqrtf64" => unstable_codegen!(codegen_simple_intrinsic!(Sqrt)),
-            "sub_with_overflow" => codegen_op_with_overflow!(sub_overflow_result),
+            "sub_with_overflow" => {
+                self.codegen_op_with_overflow(BinaryOperator::OverflowResultMinus, fargs, p, loc)
+            }
             "transmute" => self.codegen_intrinsic_transmute(fargs, ret_ty, p),
             "truncf32" => codegen_simple_intrinsic!(Truncf),
             "truncf64" => codegen_simple_intrinsic!(Trunc),
@@ -719,6 +693,25 @@ impl<'tcx> GotocCtx<'tcx> {
         dividend_is_int_min.and(divisor_is_minus_one).not()
     }
 
+    /// Intrinsics of the form *_with_overflow
+    fn codegen_op_with_overflow(
+        &mut self,
+        binop: BinaryOperator,
+        mut fargs: Vec<Expr>,
+        place: &Place<'tcx>,
+        loc: Location,
+    ) -> Stmt {
+        let place_ty = self.place_ty(place);
+        let result_type = self.codegen_ty(place_ty);
+        let left = fargs.remove(0);
+        let right = fargs.remove(0);
+        let res = self.binop_with_overflow(binop, left, right, result_type.clone(), loc);
+        self.codegen_expr_to_place(
+            place,
+            Expr::statement_expression(vec![res.as_stmt(loc)], result_type),
+        )
+    }
+
     fn codegen_exact_div(&mut self, mut fargs: Vec<Expr>, p: &Place<'tcx>, loc: Location) -> Stmt {
         // Check for undefined behavior conditions defined in
         // https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 04a86b7ff29a..37505c5360b9 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -10,7 +10,10 @@ use crate::kani_middle::coercion::{
     extract_unsize_casting, CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBase,
 };
 use crate::unwrap_or_return_codegen_unimplemented;
-use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
+use cbmc::goto_program::{
+    arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Symbol, Type,
+    ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD,
+};
 use cbmc::MachineModel;
 use cbmc::{btree_string_map, InternString, InternedString};
 use num::bigint::BigInt;
@@ -167,6 +170,37 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// Generate code for a binary operation with an overflow and returns a tuple (res, overflow).
+    pub fn binop_with_overflow(
+        &mut self,
+        bin_op: BinaryOperator,
+        left: Expr,
+        right: Expr,
+        expected_typ: Type,
+        loc: Location,
+    ) -> Expr {
+        // Create CBMC result type and add to the symbol table.
+        let res_type = arithmetic_overflow_result_type(left.typ().clone());
+        let tag = res_type.tag().unwrap();
+        let struct_tag =
+            self.ensure_struct(tag, tag, |_, _| res_type.components().unwrap().clone());
+        let res = left.overflow_op(bin_op, right);
+        // store the result in a temporary variable
+        let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc);
+        // cast into result type
+        let cast = Expr::struct_expr_from_values(
+            expected_typ.clone(),
+            vec![
+                var.clone().member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table),
+                var.member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table)
+                    .cast_to(Type::c_bool()),
+            ],
+            &self.symbol_table,
+        );
+        Expr::statement_expression(vec![decl, cast.as_stmt(loc)], expected_typ)
+    }
+
+    /// Generate code for a binary arithmetic operation with UB / overflow checks in place.
     fn codegen_rvalue_checked_binary_op(
         &mut self,
         op: &BinOp,
@@ -201,27 +235,33 @@ impl<'tcx> GotocCtx<'tcx> {
 
         match op {
             BinOp::Add => {
-                let res = ce1.add_overflow(ce2);
-                Expr::struct_expr_from_values(
-                    self.codegen_ty(res_ty),
-                    vec![res.result, res.overflowed.cast_to(Type::c_bool())],
-                    &self.symbol_table,
+                let res_type = self.codegen_ty(res_ty);
+                self.binop_with_overflow(
+                    BinaryOperator::OverflowResultPlus,
+                    ce1,
+                    ce2,
+                    res_type,
+                    Location::None,
                 )
             }
             BinOp::Sub => {
-                let res = ce1.sub_overflow(ce2);
-                Expr::struct_expr_from_values(
-                    self.codegen_ty(res_ty),
-                    vec![res.result, res.overflowed.cast_to(Type::c_bool())],
-                    &self.symbol_table,
+                let res_type = self.codegen_ty(res_ty);
+                self.binop_with_overflow(
+                    BinaryOperator::OverflowResultMinus,
+                    ce1,
+                    ce2,
+                    res_type,
+                    Location::None,
                 )
             }
             BinOp::Mul => {
-                let res = ce1.mul_overflow(ce2);
-                Expr::struct_expr_from_values(
-                    self.codegen_ty(res_ty),
-                    vec![res.result, res.overflowed.cast_to(Type::c_bool())],
-                    &self.symbol_table,
+                let res_type = self.codegen_ty(res_ty);
+                self.binop_with_overflow(
+                    BinaryOperator::OverflowResultMult,
+                    ce1,
+                    ce2,
+                    res_type,
+                    Location::None,
                 )
             }
             BinOp::Shl => {
diff --git a/tests/ui/cbmc_checks/signed-overflow/expected b/tests/ui/cbmc_checks/signed-overflow/expected
index 2922f224a5d1..143dd683f76f 100644
--- a/tests/ui/cbmc_checks/signed-overflow/expected
+++ b/tests/ui/cbmc_checks/signed-overflow/expected
@@ -7,12 +7,5 @@ Failed Checks: attempt to calculate the remainder with a divisor of zero
 Failed Checks: attempt to calculate the remainder with overflow
 Failed Checks: attempt to shift left with overflow
 Failed Checks: attempt to shift right with overflow
-Failed Checks: arithmetic overflow on signed addition
-Failed Checks: arithmetic overflow on signed subtraction
-Failed Checks: arithmetic overflow on signed multiplication
-Failed Checks: shift distance is negative
-Failed Checks: shift distance too large
-Failed Checks: shift operand is negative
 Failed Checks: arithmetic overflow on signed shl
-Failed Checks: shift distance is negative
-Failed Checks: shift distance too large
+Failed Checks: shift operand is negative
diff --git a/tests/ui/cbmc_checks/unsigned-overflow/expected b/tests/ui/cbmc_checks/unsigned-overflow/expected
index b9cde3bb478b..fd6e760da3c8 100644
--- a/tests/ui/cbmc_checks/unsigned-overflow/expected
+++ b/tests/ui/cbmc_checks/unsigned-overflow/expected
@@ -1,7 +1,7 @@
 Failed Checks: attempt to divide by zero
 Failed Checks: attempt to calculate the remainder with a divisor of zero
-Failed Checks: arithmetic overflow on unsigned addition
-Failed Checks: arithmetic overflow on unsigned subtraction
-Failed Checks: arithmetic overflow on unsigned multiplication
-Failed Checks: shift distance too large
-Failed Checks: shift distance too large
+Failed Checks: attempt to add with overflow
+Failed Checks: attempt to subtract with overflow
+Failed Checks: attempt to multiply with overflow
+Failed Checks: attempt to shift right with overflow
+Failed Checks: attempt to shift left with overflow

From 095e38e31f1f2bf375185d6a6c70fe11cef14f12 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 25 Apr 2023 18:04:54 -0700
Subject: [PATCH 6/9] Finish fixing the regression

---
 .../src/codegen_cprover_gotoc/codegen/statement.rs       | 3 ++-
 tests/expected/array/main.rs                             | 8 +++++++-
 .../PhantomData/{phantom_fixme.rs => phantom_data.rs}    | 0
 tests/ui/cbmc_checks/pointer/expected                    | 7 ++-----
 tests/ui/code-location/expected                          | 2 +-
 tests/ui/should-panic-attribute/no-panics/expected       | 7 ++++---
 .../should-panic-attribute/unexpected-failures/expected  | 9 +++++----
 .../should-panic-attribute/unexpected-failures/test.rs   | 3 ++-
 8 files changed, 23 insertions(+), 16 deletions(-)
 rename tests/kani/PhantomData/{phantom_fixme.rs => phantom_data.rs} (100%)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 8e96272a08c5..18f510dc7a56 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -555,6 +555,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     // Normal, non-virtual function calls
                     InstanceDef::Item(..)
                     | InstanceDef::DropGlue(_, Some(_))
+                    | InstanceDef::FnPtrAddrShim(_, _)
                     | InstanceDef::Intrinsic(..)
                     | InstanceDef::FnPtrShim(..)
                     | InstanceDef::VTableShim(..)
@@ -569,7 +570,7 @@ impl<'tcx> GotocCtx<'tcx> {
                                 .with_location(loc),
                         ]
                     }
-                    InstanceDef::ThreadLocalShim(_) | InstanceDef::FnPtrAddrShim(_, _) => todo!(),
+                    InstanceDef::ThreadLocalShim(_) => todo!(),
                 };
                 stmts.push(self.codegen_end_call(target.as_ref(), loc));
                 Stmt::block(stmts, loc)
diff --git a/tests/expected/array/main.rs b/tests/expected/array/main.rs
index 1f2e04ed0b5a..d01f326b8bb7 100644
--- a/tests/expected/array/main.rs
+++ b/tests/expected/array/main.rs
@@ -6,11 +6,17 @@ fn foo(x: [i32; 5]) -> [i32; 2] {
     [x[0], x[1]]
 }
 
+/// Generate an out-of-bound index with the given length.
+/// We use a function so the constant propagation
+fn oob_index(len: usize) -> usize {
+    len
+}
+
 #[kani::proof]
 fn main() {
     let x = [1, 2, 3, 4, 5];
     let y = foo(x);
-    let z = 2;
+    let z = oob_index(y.len());
     assert!(y[0] == 1);
     assert!(y[1] == 2);
     assert!(y[z] == 3);
diff --git a/tests/kani/PhantomData/phantom_fixme.rs b/tests/kani/PhantomData/phantom_data.rs
similarity index 100%
rename from tests/kani/PhantomData/phantom_fixme.rs
rename to tests/kani/PhantomData/phantom_data.rs
diff --git a/tests/ui/cbmc_checks/pointer/expected b/tests/ui/cbmc_checks/pointer/expected
index 5c002065b37f..5a1d87cf2e3d 100644
--- a/tests/ui/cbmc_checks/pointer/expected
+++ b/tests/ui/cbmc_checks/pointer/expected
@@ -1,5 +1,2 @@
-Failed Checks: dereference failure: pointer NULL
-Failed Checks: dereference failure: deallocated dynamic object
-Failed Checks: dereference failure: dead object
-Failed Checks: dereference failure: pointer outside object bounds
-Failed Checks: dereference failure: invalid integer address
+Failed Checks: misaligned pointer dereference: address must be a multiple of its type's alignment
+Failed Checks: assertion failed: unsafe { *p1 != 0 }
diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected
index 79e1ac6cb30e..cced065e9f1a 100644
--- a/tests/ui/code-location/expected
+++ b/tests/ui/code-location/expected
@@ -1,6 +1,6 @@
 module/mod.rs:10:5 in function module::not_empty
 main.rs:13:5 in function same_file
 /toolchains/
-alloc/src/vec/mod.rs:3030:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
+alloc/src/vec/mod.rs:3018:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tests/ui/should-panic-attribute/no-panics/expected b/tests/ui/should-panic-attribute/no-panics/expected
index 37cd42b86d22..be42df7fb7f6 100644
--- a/tests/ui/should-panic-attribute/no-panics/expected
+++ b/tests/ui/should-panic-attribute/no-panics/expected
@@ -1,4 +1,5 @@
-- Status: SUCCESS\
-- Description: "assertion failed: 1 + 1 == 2"
- ** 0 of 1 failed
+check.assertion\
+SUCCESS\
+assertion failed: 1 + 1 == 2
+
 VERIFICATION:- FAILED (encountered no panics, but at least one was expected)
diff --git a/tests/ui/should-panic-attribute/unexpected-failures/expected b/tests/ui/should-panic-attribute/unexpected-failures/expected
index 513744fa06fb..6cd10b4bafd5 100644
--- a/tests/ui/should-panic-attribute/unexpected-failures/expected
+++ b/tests/ui/should-panic-attribute/unexpected-failures/expected
@@ -1,8 +1,9 @@
-overflow.undefined-shift.1\
-- Status: FAILURE\
-- Description: "shift distance too large"
-Failed Checks: attempt to shift left with overflow
+undefined-shift\
+Status: FAILURE\
+Description: "shift distance too large"
+
 Failed Checks: panicked on the `1` arm!
 Failed Checks: panicked on the `0` arm!
 Failed Checks: shift distance too large
+
 VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
diff --git a/tests/ui/should-panic-attribute/unexpected-failures/test.rs b/tests/ui/should-panic-attribute/unexpected-failures/test.rs
index 776bc87d3b62..625a15c89683 100644
--- a/tests/ui/should-panic-attribute/unexpected-failures/test.rs
+++ b/tests/ui/should-panic-attribute/unexpected-failures/test.rs
@@ -3,10 +3,11 @@
 
 //! Checks that verfication fails when `#[kani::should_panic]` is used but not
 //! all failures encountered are panics.
+#![feature(unchecked_math)]
 
 fn trigger_overflow() {
     let x: u32 = kani::any();
-    let _ = 42 << x;
+    let _ = unsafe { 42u32.unchecked_shl(x) };
 }
 
 #[kani::proof]

From 0033a60f2bac04db7a55e48a3cdf820b3705917a Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 1 May 2023 13:00:08 -0700
Subject: [PATCH 7/9] Change tests expectations

Remove CBMC failure expectations that are now caught by the rust
overflow check. This was due to the following Rust compiler change:
- https://github.com/rust-lang/rust/pull/108282
---
 tests/ui/cbmc_checks/signed-overflow/expected   | 2 --
 tests/ui/cbmc_checks/unsigned-overflow/expected | 1 -
 2 files changed, 3 deletions(-)

diff --git a/tests/ui/cbmc_checks/signed-overflow/expected b/tests/ui/cbmc_checks/signed-overflow/expected
index 745ff831a41c..143dd683f76f 100644
--- a/tests/ui/cbmc_checks/signed-overflow/expected
+++ b/tests/ui/cbmc_checks/signed-overflow/expected
@@ -9,5 +9,3 @@ Failed Checks: attempt to shift left with overflow
 Failed Checks: attempt to shift right with overflow
 Failed Checks: arithmetic overflow on signed shl
 Failed Checks: shift operand is negative
-Failed Checks: shift distance is negative
-Failed Checks: shift distance too large
diff --git a/tests/ui/cbmc_checks/unsigned-overflow/expected b/tests/ui/cbmc_checks/unsigned-overflow/expected
index ef0f06506b36..fd6e760da3c8 100644
--- a/tests/ui/cbmc_checks/unsigned-overflow/expected
+++ b/tests/ui/cbmc_checks/unsigned-overflow/expected
@@ -5,4 +5,3 @@ Failed Checks: attempt to subtract with overflow
 Failed Checks: attempt to multiply with overflow
 Failed Checks: attempt to shift right with overflow
 Failed Checks: attempt to shift left with overflow
-Failed Checks: shift distance too large

From 623420d254701443ab0d3b6a78c23c4da8869f89 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 2 May 2023 09:45:18 -0700
Subject: [PATCH 8/9] Fix comment in the test file `main.rs`

---
 tests/expected/array/main.rs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tests/expected/array/main.rs b/tests/expected/array/main.rs
index d01f326b8bb7..44c9ca376a07 100644
--- a/tests/expected/array/main.rs
+++ b/tests/expected/array/main.rs
@@ -7,7 +7,9 @@ fn foo(x: [i32; 5]) -> [i32; 2] {
 }
 
 /// Generate an out-of-bound index with the given length.
-/// We use a function so the constant propagation
+///
+/// We use a function to prevent constant progragation, so the out-of-bounds
+/// error is not detected at compilation time.
 fn oob_index(len: usize) -> usize {
     len
 }

From fe800fe03c3f9ab7956465bae697a0551fd2f56b Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Thu, 4 May 2023 11:26:30 -0700
Subject: [PATCH 9/9] Fix the merge

   - Support all instance types as part of the rechability analysis.
   - Skip assembly and closures for attribute checking due to rustc
     limitation.
   - Fix mir changes to the stats collector.
---
 kani-compiler/src/kani_middle/analysis.rs       | 4 ++--
 kani-compiler/src/kani_middle/attributes.rs     | 7 ++++++-
 kani-compiler/src/kani_middle/mod.rs            | 2 +-
 kani-compiler/src/kani_middle/reachability.rs   | 2 +-
 tests/cargo-ui/unstable-attr/invalid/expected   | 6 +++---
 tests/cargo-ui/unstable-attr/invalid/src/lib.rs | 5 +++++
 6 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs
index e618d8ec2163..ee0b8e769bc7 100644
--- a/kani-compiler/src/kani_middle/analysis.rs
+++ b/kani-compiler/src/kani_middle/analysis.rs
@@ -138,6 +138,7 @@ impl<'tcx> From<&Statement<'tcx>> for Key {
             | StatementKind::ConstEvalCounter
             | StatementKind::FakeRead(_)
             | StatementKind::Nop
+            | StatementKind::PlaceMention(_)
             | StatementKind::Retag(_, _)
             | StatementKind::StorageLive(_)
             | StatementKind::StorageDead(_) => Key("Ignored"),
@@ -148,11 +149,9 @@ impl<'tcx> From<&Statement<'tcx>> for Key {
 impl<'tcx> From<&Terminator<'tcx>> for Key {
     fn from(value: &Terminator<'tcx>) -> Self {
         match value.kind {
-            TerminatorKind::Abort => Key("Abort"),
             TerminatorKind::Assert { .. } => Key("Assert"),
             TerminatorKind::Call { .. } => Key("Call"),
             TerminatorKind::Drop { .. } => Key("Drop"),
-            TerminatorKind::DropAndReplace { .. } => Key("DropAndReplace"),
             TerminatorKind::GeneratorDrop => Key("GeneratorDrop"),
             TerminatorKind::Goto { .. } => Key("Goto"),
             TerminatorKind::FalseEdge { .. } => Key("FalseEdge"),
@@ -161,6 +160,7 @@ impl<'tcx> From<&Terminator<'tcx>> for Key {
             TerminatorKind::Resume => Key("Resume"),
             TerminatorKind::Return => Key("Return"),
             TerminatorKind::SwitchInt { .. } => Key("SwitchInt"),
+            TerminatorKind::Terminate => Key("Terminate"),
             TerminatorKind::Unreachable => Key("Unreachable"),
             TerminatorKind::Yield { .. } => Key("Yield"),
         }
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 8bb298dbd810..8e0691182215 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -8,7 +8,7 @@ use kani_metadata::{CbmcSolver, HarnessAttributes, Stub};
 use rustc_ast::{attr, AttrKind, Attribute, LitKind, MetaItem, MetaItemKind, NestedMetaItem};
 use rustc_errors::ErrorGuaranteed;
 use rustc_hir::{def::DefKind, def_id::DefId};
-use rustc_middle::ty::{self, Instance, TyCtxt};
+use rustc_middle::ty::{self, Instance, TyCtxt, TyKind};
 use rustc_span::Span;
 use std::str::FromStr;
 use strum_macros::{AsRefStr, EnumString};
@@ -155,6 +155,11 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option<HarnessA
 ///
 /// TODO: Improve error message by printing the span of the callee instead of the definition.
 pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: DefId) {
+    if !matches!(tcx.type_of(def_id).0.kind(), TyKind::FnDef(..)) {
+        // skip closures due to an issue with rustc.
+        // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862
+        return;
+    }
     let attributes = extract_kani_attributes(tcx, def_id);
     if let Some(unstable_attrs) = attributes.get(&KaniAttributeKind::Unstable) {
         for attr in unstable_attrs {
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index dc5a8986c409..82c519c48967 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -61,7 +61,7 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
 pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) {
     // Avoid printing the same error multiple times for different instantiations of the same item.
     let mut def_ids = HashSet::new();
-    for item in items {
+    for item in items.iter().filter(|i| matches!(i, MonoItem::Fn(..) | MonoItem::Static(..))) {
         let def_id = item.def_id();
         if !def_ids.contains(&def_id) {
             // Check if any unstable attribute was reached.
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index 14fea7d11022..a322007485a4 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -283,7 +283,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
             | InstanceDef::Item(..)
             | InstanceDef::ReifyShim(..)
             | InstanceDef::VTableShim(..) => true,
-            InstanceDef::ThreadLocalShim(_) | InstanceDef::FnPtrAddrShim(_, _) => todo!(),
+            InstanceDef::ThreadLocalShim(_) | InstanceDef::FnPtrAddrShim(_, _) => true,
         };
         if should_collect && should_codegen_locally(self.tcx, &instance) {
             trace!(?instance, "collect_instance");
diff --git a/tests/cargo-ui/unstable-attr/invalid/expected b/tests/cargo-ui/unstable-attr/invalid/expected
index 66d0c5271668..b3acac173184 100644
--- a/tests/cargo-ui/unstable-attr/invalid/expected
+++ b/tests/cargo-ui/unstable-attr/invalid/expected
@@ -1,8 +1,8 @@
-error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found `feature("invalid_args")`\
+error: failed to parse `#[kani::unstable]`: expected "key = value" pair, but found\
 src/lib.rs\
 |\
-| #[kani::unstable(feature("invalid_args"))]\
-| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\
+| #[kani::unstable(\
+| ^^^^^^^^^^^^^^^^^^\
 |\
 = note: expected format: #[kani::unstable(feature="<IDENTIFIER>", issue="<ISSUE>", reason="<DESCRIPTION>")]\
 = note: this error originates in the attribute macro `kani::unstable` (in Nightly builds, run with -Z macro-backtrace for more info)
diff --git a/tests/cargo-ui/unstable-attr/invalid/src/lib.rs b/tests/cargo-ui/unstable-attr/invalid/src/lib.rs
index f6f55bc112ef..5fbfc768c883 100644
--- a/tests/cargo-ui/unstable-attr/invalid/src/lib.rs
+++ b/tests/cargo-ui/unstable-attr/invalid/src/lib.rs
@@ -1,6 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+//! All the unstable definitions below should fail.
+//! The expected file only contains a generic check since we trigger an ICE for debug builds and
+//! we don't guarantee the order that these will be evaluated.
+//! TODO: We should break down this test to ensure all of these fail.
+
 #[kani::unstable(reason = "just checking", issue = "<link>")]
 pub fn missing_feature() {
     todo!()