Address PR comments:

 - Improve comments.
 - Remove wrong cast to i64.
 - Fix statement location.
 - Create util function to create unsigned type.

cprover_bindings/src/goto_program/typ.rs

@@ -973,6 +973,19 @@ impl Type {
         Pointer { typ: Box::new(self) }
     }
 
+    /// Convert type to its unsigned counterpart if possible.
+    /// For types that are already unsigned, this will return self.
+    /// Note: This will expand any typedef.
+    pub fn to_unsigned(&self) -> Option<Self> {
+        let concrete = self.unwrap_typedef();
+        match concrete {
+            CInteger(CIntType::SSizeT) => Some(CInteger(CIntType::SizeT)),
+            Signedbv { ref width } => Some(Unsignedbv { width: *width }),
+            Unsignedbv { .. } => Some(self.clone()),
+            _ => None,
+        }
+    }
+
     pub fn signed_int<T>(w: T) -> Self
     where
         T: TryInto<u64>,

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

@@ -475,9 +475,11 @@ impl<'tcx> GotocCtx<'tcx> {
 
                     // Compute relative discriminant value (`niche_val - niche_start`).
                     //
-                    // We remap `niche_start..=niche_start + n` (which may wrap around) to (non-wrap-around)
-                    // `0..=n`, to be able to check whether the discriminant corresponds to a niche variant with
-                    // one comparison.
+                    // "We remap `niche_start..=niche_start + n` (which may wrap around) to
+                    // (non-wrap-around) `0..=n`, to be able to check whether the discriminant
+                    // corresponds to a niche variant with one comparison."
+                    // https://github.com/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247
+                    //
                     // Note: niche_variants can only represent values that fit in a u32.
                     let discr_mir_ty = self.codegen_enum_discr_typ(ty);
                     let discr_type = self.codegen_ty(discr_mir_ty);
@@ -1271,8 +1273,8 @@ fn wrapping_sub(expr: &Expr, constant: u64) -> Expr {
         // No need to subtract.
         expr.clone()
     } else {
-        let unsigned = Type::unsigned_int(expr.typ().width().unwrap());
-        let constant = Expr::int_constant(constant as i64, unsigned.clone());
+        let unsigned = expr.typ().to_unsigned().unwrap();
+        let constant = Expr::int_constant(constant, unsigned.clone());
         expr.clone().cast_to(unsigned).sub(constant)
     }
 }

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

@@ -603,6 +603,7 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt {
         let _trace_span = info_span!("CodegenStatement", statement = ?stmt).entered();
         debug!("handling statement {:?}", stmt);
+        let location = self.codegen_span(&stmt.source_info.span);
         match &stmt.kind {
             StatementKind::Assign(box (l, r)) => {
                 let lty = self.place_ty(l);
@@ -617,15 +618,15 @@ impl<'tcx> GotocCtx<'tcx> {
                     // where the reference is implicit.
                     unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
                         .goto_expr
-                        .assign(self.codegen_rvalue(r).address_of(), Location::none())
+                        .assign(self.codegen_rvalue(r).address_of(), location)
                 } else if rty.is_bool() {
                     unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
                         .goto_expr
-                        .assign(self.codegen_rvalue(r).cast_to(Type::c_bool()), Location::none())
+                        .assign(self.codegen_rvalue(r).cast_to(Type::c_bool()), location)
                 } else {
                     unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
                         .goto_expr
-                        .assign(self.codegen_rvalue(r), Location::none())
+                        .assign(self.codegen_rvalue(r), location)
                 }
             }
             StatementKind::Deinit(place) => {
@@ -634,15 +635,15 @@ impl<'tcx> GotocCtx<'tcx> {
                 let dst_mir_ty = self.place_ty(place);
                 let dst_type = self.codegen_ty(dst_mir_ty);
                 let layout = self.layout_of(dst_mir_ty);
-                if layout.is_zst() || self.ignore_var_ty(dst_mir_ty) {
+                if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 {
                     // We ignore assignment for all zero size types
                     // Ignore generators too for now:
                     // https://github.com/model-checking/kani/issues/416
-                    Stmt::skip(Location::none())
+                    Stmt::skip(location)
                 } else {
                     unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
                         .goto_expr
-                        .assign(dst_type.nondet(), Location::none())
+                        .assign(dst_type.nondet(), location)
                 }
             }
             StatementKind::SetDiscriminant { place, variant_index } => {
@@ -655,16 +656,16 @@ impl<'tcx> GotocCtx<'tcx> {
                             .codegen_unimplemented(
                                 "ty::Generator",
                                 Type::code(vec![], Type::empty()),
-                                Location::none(),
+                                location.clone(),
                                 "https://github.com/model-checking/kani/issues/416",
                             )
-                            .as_stmt(Location::none());
+                            .as_stmt(location);
                     }
                     _ => unreachable!(),
                 };
                 let layout = self.layout_of(pt);
                 match &layout.variants {
-                    Variants::Single { .. } => Stmt::skip(Location::none()),
+                    Variants::Single { .. } => Stmt::skip(location),
                     Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
                         TagEncoding::Direct => {
                             let discr = def.discriminant_for_variant(self.tcx, *variant_index);
@@ -688,7 +689,7 @@ impl<'tcx> GotocCtx<'tcx> {
                             )
                             .goto_expr
                             .member("case", &self.symbol_table)
-                            .assign(discr, Location::none())
+                            .assign(discr, location)
                         }
                         TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
                             if dataful_variant != variant_index {
@@ -715,16 +716,16 @@ impl<'tcx> GotocCtx<'tcx> {
                                 )
                                 .goto_expr;
                                 self.codegen_get_niche(place, offset, discr_ty)
-                                    .assign(value, Location::none())
+                                    .assign(value, location)
                             } else {
-                                Stmt::skip(Location::none())
+                                Stmt::skip(location)
                             }
                         }
                     },
                 }
             }
-            StatementKind::StorageLive(_) => Stmt::skip(Location::none()), // TODO: fix me
-            StatementKind::StorageDead(_) => Stmt::skip(Location::none()), // TODO: fix me
+            StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me
+            StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me
             StatementKind::CopyNonOverlapping(box mir::CopyNonOverlapping {
                 ref src,
                 ref dst,
@@ -737,26 +738,21 @@ impl<'tcx> GotocCtx<'tcx> {
                 let sz = Expr::int_constant(sz, Type::size_t());
                 let n = sz.mul(count);
                 let dst = dst.cast_to(Type::void_pointer());
-                let e = BuiltinFn::Memcpy.call(vec![dst, src, n.clone()], Location::none());
+                let e = BuiltinFn::Memcpy.call(vec![dst, src, n.clone()], location.clone());
 
                 // The C implementation of memcpy does not allow an invalid pointer for
                 // the src/dst, but the LLVM implementation specifies that a copy with
                 // length zero is a no-op. This comes up specifically when handling
                 // the empty string; CBMC will fail on passing a reference to empty
                 // string unless we codegen this zero check.
                 // https://llvm.org/docs/LangRef.html#llvm-memcpy-intrinsic
-                Stmt::if_then_else(
-                    n.is_zero().not(),
-                    e.as_stmt(Location::none()),
-                    None,
-                    Location::none(),
-                )
+                Stmt::if_then_else(n.is_zero().not(), e.as_stmt(location.clone()), None, location)
             }
             StatementKind::FakeRead(_)
             | StatementKind::Retag(_, _)
             | StatementKind::AscribeUserType(_, _)
             | StatementKind::Nop
-            | StatementKind::Coverage { .. } => Stmt::skip(Location::none()),
+            | StatementKind::Coverage { .. } => Stmt::skip(location),
         }
         .with_location(self.codegen_span(&stmt.source_info.span))
     }

kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs

@@ -114,32 +114,10 @@ impl<'tcx> GotocCtx<'tcx> {
     /// If either of those change, this will almost certainly stop working.
     pub fn deref_box(&self, box_expr: Expr) -> Expr {
         // Internally, a Boxed type is stored as a chain of structs.
-        // In particular:
-        // `Box<T>` is an owning reference to an allocation of type T on the heap.
-        // It has a pointer of type `ptr::Unique<T>` and an allocator of type `alloc::Global`
-        // Unique<T> is an owning raw pointer to a location in memory.
-        // So given a Box<T>, we can follow the chain to get the desired pointer.
-        // If either rustc or Kani changes how boxed types are represented, this will need to be
-        // updated.
         //
-        // The following C code is the result of running `kani --gen-c` on rust with boxed types:
-        // Given a boxed type (note that Rust can reorder fields to improve struct packing):
-        // ```
-        // struct std::boxed::Box<[u8]>
-        // {
-        //   struct std::alloc::Global 1;
-        //   struct std::ptr::Unique<[u8]> 0;
-        // };
-        // ```
-        // We follow the Unique pointer:
-        // ```
-        // struct std::ptr::Unique<[u8]>
-        // {
-        //   struct std::marker::PhantomData<[u8]> _marker;
-        //   struct &[u8] pointer;
-        // };
-        // ```
-        // And notice that its `.pointer` field is exactly what we want.
+        // This code has to match the exact structure from the std library version that is
+        // supported to access the raw pointer. If either rustc or Kani changes how boxed types are
+        // represented, this will need to be updated.
         self.assert_is_rust_box_like(box_expr.typ());
         RAW_PTR_FROM_BOX.iter().fold(box_expr, |expr, name| expr.member(name, &self.symbol_table))
     }

tests/kani/Enum/discriminant_128bits.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// Check niche optimization for mix of option, tuple and nonnull.
+// Check niche optimization for an object that is 128 bits long.
 
 use std::mem::{discriminant, size_of_val};
 use std::num::NonZeroU128;