Update the rust toolchain to nightly-2022-05-03 (#1181)

* Update rust toolchain to nightly-2022-05-03

This compiles but regression is failing due to unimplemented statement.

* Handle change to Box<T> structure

Box<T> now users NonNull<T> instead of raw pointer.

* Handle new statement kind Deinit

We codegen an assignment to non-det value per documentation. See more
information here:
 - rust-lang/rust#95125

* Fix discriminant computation

After the merge, the previous wrapping sub logic was triggering a panic
due to u128 -> i64 conversion. There were also other overflow issues
when trying to convert the `niche_value` to unsigned.

For now, I'm disabling the coversion check which I believe is too
strict. We should consider implementing a more flexible check later that
can be controlled by the user without affecting the internal compiler
codegen.

* Address PR comments:

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

Author: celinval

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

@@ -472,19 +472,27 @@ impl<'tcx> GotocCtx<'tcx> {
                         FieldsShape::Arbitrary { offsets, .. } => offsets[0].bytes_usize(),
                         _ => unreachable!("niche encoding must have arbitrary fields"),
                     };
-                    let discr_ty = self.codegen_enum_discr_typ(ty);
-                    let discr_ty = self.codegen_ty(discr_ty);
-                    let niche_val = self.codegen_get_niche(e, offset, discr_ty.clone());
-                    let relative_discr = if *niche_start == 0 {
-                        niche_val
-                    } else {
-                        wrapping_sub(&niche_val, *niche_start)
-                    };
+
+                    // 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."
+                    // 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);
+                    let niche_val = self.codegen_get_niche(e, offset, discr_type.clone());
+                    let relative_discr =
+                        wrapping_sub(&niche_val, u64::try_from(*niche_start).unwrap());
                     let relative_max =
                         niche_variants.end().as_u32() - niche_variants.start().as_u32();
-                    let is_niche = if tag.value == Primitive::Pointer {
-                        discr_ty.null().eq(relative_discr.clone())
+                    let is_niche = if tag.primitive() == Primitive::Pointer {
+                        tracing::trace!(?tag, "Primitive::Pointer");
+                        discr_type.null().eq(relative_discr.clone())
                     } else {
+                        tracing::trace!(?tag, "Not Primitive::Pointer");
                         relative_discr
                             .clone()
                             .le(Expr::int_constant(relative_max, relative_discr.typ().clone()))
@@ -1260,26 +1268,13 @@ impl<'tcx> GotocCtx<'tcx> {
 /// Perform a wrapping subtraction of an Expr with a constant "expr - constant"
 /// where "-" is wrapping subtraction, i.e., the result should be interpreted as
 /// an unsigned value (2's complement).
-fn wrapping_sub(expr: &Expr, constant: u128) -> Expr {
-    // While the wrapping subtraction can be done through a regular subtraction
-    // and then casting the result to an unsigned, doing so may result in CBMC
-    // flagging the operation with a signed to unsigned overflow failure (see
-    // https://github.com/model-checking/kani/issues/356).
-    // To avoid those overflow failures, the wrapping subtraction operation is
-    // computed as:
-    //   if expr >= constant {
-    //       // result is positive, so overflow may not occur
-    //       expr - constant
-    //   } else {
-    //       // compute the 2's complement to avoid overflow
-    //       expr - constant + 2^32
-    //   }
-    let s64 = Type::signed_int(64);
-    let expr = expr.clone().cast_to(s64.clone());
-    let twos_complement: i64 = u32::MAX as i64 + 1 - i64::try_from(constant).unwrap();
-    let constant = Expr::int_constant(constant, s64.clone());
-    expr.clone().ge(constant.clone()).ternary(
-        expr.clone().sub(constant),
-        expr.plus(Expr::int_constant(twos_complement, s64.clone())),
-    )
+fn wrapping_sub(expr: &Expr, constant: u64) -> Expr {
+    if constant == 0 {
+        // No need to subtract.
+        expr.clone()
+    } else {
+        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,32 @@ 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) => {
+                // From rustc doc: "This writes `uninit` bytes to the entire place."
+                // Thus, we assign nondet() value to the entire place.
+                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() || 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)
+                } else {
+                    unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
+                        .goto_expr
+                        .assign(dst_type.nondet(), location)
                 }
             }
             StatementKind::SetDiscriminant { place, variant_index } => {
@@ -638,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);
@@ -671,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 {
@@ -686,27 +704,28 @@ impl<'tcx> GotocCtx<'tcx> {
                                 let niche_value =
                                     variant_index.as_u32() - niche_variants.start().as_u32();
                                 let niche_value = (niche_value as u128).wrapping_add(*niche_start);
-                                let value = if niche_value == 0 && tag.value == Primitive::Pointer {
-                                    discr_ty.null()
-                                } else {
-                                    Expr::int_constant(niche_value, discr_ty.clone())
-                                };
+                                let value =
+                                    if niche_value == 0 && tag.primitive() == Primitive::Pointer {
+                                        discr_ty.null()
+                                    } else {
+                                        Expr::int_constant(niche_value, discr_ty.clone())
+                                    };
                                 let place = unwrap_or_return_codegen_unimplemented_stmt!(
                                     self,
                                     self.codegen_place(place)
                                 )
                                 .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,
@@ -719,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/codegen/typ.rs

@@ -1206,7 +1206,7 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_enum_discr_typ(&self, ty: Ty<'tcx>) -> Ty<'tcx> {
         let layout = self.layout_of(ty);
         match &layout.variants {
-            Variants::Multiple { tag, .. } => self.codegen_prim_typ(tag.value),
+            Variants::Multiple { tag, .. } => self.codegen_prim_typ(tag.primitive()),
             _ => unreachable!("only enum has discriminant"),
         }
     }
@@ -1263,7 +1263,7 @@ impl<'tcx> GotocCtx<'tcx> {
             _ => unreachable!(),
         };
 
-        let rustc_target::abi::Scalar { value: prim_type, .. } = element;
+        let prim_type = element.primitive();
         let rust_type = self.codegen_prim_typ(prim_type);
         let cbmc_type = self.codegen_ty(rust_type);