Upgrade toolchain to nightly-2022-09-13

.cargo/config.toml

@@ -28,4 +28,8 @@ rustflags = [ # Global lints/warnings. Need to use underscore instead of -.
  "-Aclippy::expect_fun_call",
  "-Aclippy::or_fun_call",
  "-Aclippy::new_without_default",
+
+ # New lints that we are not compliant yet
+ "-Aclippy::needless-borrow",
+ "-Aclippy::bool-to-int-with-if",
 ]

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

@@ -313,13 +313,6 @@ impl<'tcx> GotocCtx<'tcx> {
  ($f:ident) => {{ codegen_intrinsic_binop!($f) }};
  }
 
- // Intrinsics which encode a pointer comparison (e.g., `ptr_guaranteed_eq`).
- // These behave as regular pointer comparison at runtime:
- // https://doc.rust-lang.org/beta/std/primitive.pointer.html#method.guaranteed_eq
- macro_rules! codegen_ptr_guaranteed_cmp {
- ($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b).cast_to(Type::c_bool())) }};
- }
-
  // Intrinsics which encode a simple binary operation
  macro_rules! codegen_intrinsic_binop {
  ($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b)) }};
@@ -596,8 +589,7 @@ impl<'tcx> GotocCtx<'tcx> {
  "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)),
  "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)),
  "pref_align_of" => codegen_intrinsic_const!(),
- "ptr_guaranteed_eq" => codegen_ptr_guaranteed_cmp!(eq),
- "ptr_guaranteed_ne" => codegen_ptr_guaranteed_cmp!(neq),
+ "ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, p),
  "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, p, loc),
  "ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, p, loc),
  "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, p, loc),
@@ -1012,6 +1004,26 @@ impl<'tcx> GotocCtx<'tcx> {
  Stmt::block(vec![src_align_check, dst_align_check, overflow_check, copy_expr], loc)
  }
 
+ // In some contexts (e.g., compilation-time evaluation),
+ // `ptr_guaranteed_cmp` compares two pointers and returns:
+ // * 2 if the result is unknown.
+ // * 1 if they are guaranteed to be equal.
+ // * 0 if they are guaranteed to be not equal.
+ // But at runtime, this intrinsic behaves as a regular pointer comparison.
+ // Therefore, we return 1 if the pointers are equal and 0 otherwise.
+ //
+ // This intrinsic replaces `ptr_guaranteed_eq` and `ptr_guaranteed_ne`:
+ // https://doc.rust-lang.org/beta/std/primitive.pointer.html#method.guaranteed_eq
+ fn codegen_ptr_guaranteed_cmp(&mut self, mut fargs: Vec<Expr>, p: &Place<'tcx>) -> Stmt {
+ let a = fargs.remove(0);
+ let b = fargs.remove(0);
+ let place_type = self.place_ty(p);
+ let res_type = self.codegen_ty(place_type);
+ let eq_expr = a.eq(b);
+ let cmp_expr = eq_expr.ternary(res_type.one(), res_type.zero());
+ self.codegen_expr_to_place(p, cmp_expr)
+ }
+
  /// Computes the offset from a pointer.
  ///
  /// Note that this function handles code generation for:

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

@@ -466,12 +466,12 @@ impl<'tcx> GotocCtx<'tcx> {
  }
 
  fn codegen_allocation_data(&mut self, alloc: &'tcx Allocation) -> Vec<AllocData<'tcx>> {
- let mut alloc_vals = Vec::with_capacity(alloc.relocations().len() + 1);
+ let mut alloc_vals = Vec::with_capacity(alloc.provenance().len() + 1);
  let pointer_size =
  Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes());
 
  let mut next_offset = Size::ZERO;
- for &(offset, alloc_id) in alloc.relocations().iter() {
+ for &(offset, alloc_id) in alloc.provenance().iter() {
  if offset > next_offset {
  let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(
  next_offset.bytes_usize()..offset.bytes_usize(),

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

@@ -504,7 +504,7 @@ impl<'tcx> GotocCtx<'tcx> {
  TagEncoding::Direct => {
  self.codegen_discriminant_field(e, ty).cast_to(self.codegen_ty(res_ty))
  }
- TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
+ TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
  // This code follows the logic in the ssa codegen backend:
  // https:/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247
  // See also the cranelift backend:
@@ -550,7 +550,7 @@ impl<'tcx> GotocCtx<'tcx> {
  };
  is_niche.ternary(
  niche_discr,
- Expr::int_constant(dataful_variant.as_u32(), result_type),
+ Expr::int_constant(untagged_variant.as_u32(), result_type),
  )
  }
  },

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

@@ -11,8 +11,8 @@ use kani_queries::UserInput;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
 use rustc_middle::mir::{
- AssertKind, BasicBlock, Operand, Place, Statement, StatementKind, SwitchTargets, Terminator,
- TerminatorKind,
+ AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind,
+ SwitchTargets, Terminator, TerminatorKind,
 };
 use rustc_middle::ty;
 use rustc_middle::ty::layout::LayoutOf;
@@ -89,8 +89,8 @@ impl<'tcx> GotocCtx<'tcx> {
  self.codegen_discriminant_field(place_goto_expr, pt)
  .assign(discr, location)
  }
- TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
- if dataful_variant != variant_index {
+ TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
+ if untagged_variant != variant_index {
  let offset = match &layout.fields {
  FieldsShape::Arbitrary { offsets, .. } => offsets[0],
  _ => unreachable!("niche encoding must have arbitrary fields"),
@@ -122,11 +122,9 @@ impl<'tcx> GotocCtx<'tcx> {
  }
  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,
- ref count,
- }) => {
+ StatementKind::Intrinsic(box NonDivergingIntrinsic::CopyNonOverlapping(
+ mir::CopyNonOverlapping { ref src, ref dst, ref count },
+ )) => {
  // Pack the operands and their types, then call `codegen_copy`
  let fargs = vec![
  self.codegen_operand(src),
@@ -137,6 +135,15 @@ impl<'tcx> GotocCtx<'tcx> {
  &[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)];
  self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location)
  }
+ StatementKind::Intrinsic(box NonDivergingIntrinsic::Assume(ref op)) => {
+ let cond = self.codegen_operand(op).cast_to(Type::bool());
+ self.codegen_assert_assume(
+ cond,
+ PropertyClass::Assume,
+ "assumption failed",
+ location,
+ )
+ }
  StatementKind::FakeRead(_)
  | StatementKind::Retag(_, _)
  | StatementKind::AscribeUserType(_, _)

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

@@ -1418,32 +1418,34 @@ impl<'tcx> GotocCtx<'tcx> {
  subst: &'tcx InternalSubsts<'tcx>,
  ) -> Type {
  let pretty_name = self.ty_pretty_name(ty);
- self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |ctx, name| {
-  // variants appearing in source code (in source code order)
-  let source_variants = &adtdef.variants();
-  let layout = ctx.layout_of(ty);
-  // variants appearing in mir code
- match &layout.variants {
- Variants::Single { index } => {
+ // variants appearing in source code (in source code order)
+ let source_variants = &adtdef.variants();
+ let layout = self.layout_of(ty);
+ // variants appearing in mir code
+ match &layout.variants {
+ Variants::Single { index } => {
+ self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, _| {
  match source_variants.get(*index) {
  None => {
  // an empty enum with no variants (its value cannot be instantiated)
  vec![]
  }
  Some(variant) => {
  // a single enum is pretty much like a struct
- let layout = ctx.layout_of(ty).layout;
- ctx.codegen_variant_struct_fields(variant, subst, &layout, Size::ZERO)
+ let layout = gcx.layout_of(ty).layout;
+ gcx.codegen_variant_struct_fields(variant, subst, &layout, Size::ZERO)
  }
  }
- }
- Variants::Multiple { tag_encoding, variants, tag_field, .. } => {
- // Contrary to generators, currently enums have only one field (the discriminant), the rest are in the variants:
- assert!(layout.fields.count() <= 1);
- // Contrary to generators, the discriminant is the first (and only) field for enums:
- assert_eq!(*tag_field, 0);
- match tag_encoding {
- TagEncoding::Direct => {
+ })
+ }
+ Variants::Multiple { tag_encoding, variants, tag_field, .. } => {
+ // Contrary to generators, currently enums have only one field (the discriminant), the rest are in the variants:
+ assert!(layout.fields.count() <= 1);
+ // Contrary to generators, the discriminant is the first (and only) field for enums:
+ assert_eq!(*tag_field, 0);
+ match tag_encoding {
+ TagEncoding::Direct => {
+ self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |gcx, name| {
  // For direct encoding of tags, we generate a type with two fields:
  // ```
  // struct tag-<> { // enum type
@@ -1455,22 +1457,22 @@ impl<'tcx> GotocCtx<'tcx> {
  // (`#[repr]`) and it represents which variant is being used.
  // The `cases` field is a union of all variant types where the name
  // of each union field is the name of the corresponding discriminant.
- let discr_t = ctx.codegen_enum_discr_typ(ty);
- let int = ctx.codegen_ty(discr_t);
- let discr_offset = ctx.layout_of(discr_t).size;
+ let discr_t = gcx.codegen_enum_discr_typ(ty);
+ let int = gcx.codegen_ty(discr_t);
+ let discr_offset = gcx.layout_of(discr_t).size;
  let initial_offset =
- ctx.variant_min_offset(variants).unwrap_or(discr_offset);
+ gcx.variant_min_offset(variants).unwrap_or(discr_offset);
  let mut fields = vec![DatatypeComponent::field("case", int)];
  if let Some(padding) =
- ctx.codegen_struct_padding(discr_offset, initial_offset, 0)
+ gcx.codegen_struct_padding(discr_offset, initial_offset, 0)
  {
  fields.push(padding);
  }
  let union_name = format!("{}-union", name);
  let union_pretty_name = format!("{}-union", pretty_name);
  fields.push(DatatypeComponent::field(
  "cases",
- ctx.ensure_union(&union_name, &union_pretty_name, |ctx, name| {
+ gcx.ensure_union(&union_name, &union_pretty_name, |ctx, name| {
  ctx.codegen_enum_cases(
  name,
  pretty_name,
@@ -1482,45 +1484,56 @@ impl<'tcx> GotocCtx<'tcx> {
  }),
  ));
  fields
- }
- TagEncoding::Niche { dataful_variant, .. } => {
- // Enumerations with multiple variants and niche encoding have a
- // specific format that can be used to optimize its layout and reduce
- // memory consumption.
- //
- // These enumerations have one and only one variant with non-ZST
- // fields which is referred to by the `dataful_variant` index. Their
- // final size and alignment is equal to the one from the
- // `dataful_variant`. All other variants either don't have any field
- // or all fields types are ZST.
- //
- // Because of that, we can represent these enums as simple structures
- // where each field represent one variant. This allows them to be
- // referred to correctly.
- //
- // Note: I tried using a union instead but it had a significant runtime
- // penalty.
- tracing::trace!(
- ?name,
- ?variants,
- ?dataful_variant,
- ?tag_encoding,
- ?subst,
- "codegen_enum: Niche"
- );
- ctx.codegen_enum_cases(
- name,
- pretty_name,
- adtdef,
- subst,
- variants,
- Size::ZERO,
- )
- }
+ })
+ }
+ TagEncoding::Niche { .. } => {
+ self.codegen_enum_niche(ty, adtdef, subst, variants)
  }
  }
  }
- })
+ }
+ }
+
+ /// Codegen an enumeration that is encoded using niche optimization.
+ ///
+ /// Enumerations with multiple variants and niche encoding have a
+ /// specific format that can be used to optimize its layout and reduce
+ /// memory consumption.
+ ///
+ /// The niche is a location in the entire type where some bit pattern
+ /// isn't valid. The compiler uses the `untagged_variant` index to
+ /// access this field.
+ /// The final size and alignment is also equal to the one from the
+ /// `untagged_variant`. All other variants either don't have any field,
+ /// or their size is smaller than the `untagged_variant`.
+ /// See <https:/rust-lang/rust/issues/46213> for more details.
+ ///
+ /// Because of that, we usually represent these enums as simple unions
+ /// where each field represent one variant. This allows them to be
+ /// referred to correctly.
+ ///
+ /// The one exception is the case where only one variant has data.
+ /// We use a struct instead because it is more performant.
+ fn codegen_enum_niche(
+ &mut self,
+ ty: Ty<'tcx>,
+ adtdef: &'tcx AdtDef,
+ subst: &'tcx InternalSubsts<'tcx>,
+ variants: &IndexVec<VariantIdx, Layout>,
+ ) -> Type {
+ let non_zst_count = variants.iter().filter(|layout| layout.size().bytes() > 0).count();
+ let mangled_name = self.ty_mangled_name(ty);
+ let pretty_name = self.ty_pretty_name(ty);
+ tracing::trace!(?pretty_name, ?variants, ?subst, ?non_zst_count, "codegen_enum: Niche");
+ if non_zst_count > 1 {
+ self.ensure_union(mangled_name, pretty_name, |gcx, name| {
+ gcx.codegen_enum_cases(name, pretty_name, adtdef, subst, variants, Size::ZERO)
+ })
+ } else {
+ self.ensure_struct(mangled_name, pretty_name, |gcx, name| {
+ gcx.codegen_enum_cases(name, pretty_name, adtdef, subst, variants, Size::ZERO)
+ })
+ }
  }
 
  pub(crate) fn variant_min_offset(

kani-compiler/src/codegen_cprover_gotoc/reachability.rs

@@ -96,7 +96,7 @@ impl<'tcx> MonoItemsCollector<'tcx> {
 
  // Collect initialization.
  let alloc = self.tcx.eval_static_initializer(def_id).unwrap();
- for &id in alloc.inner().relocations().values() {
+ for &id in alloc.inner().provenance().values() {
  self.queue.extend(collect_alloc_items(self.tcx, id).iter());
  }
  }
@@ -202,7 +202,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
  }
  ConstValue::Slice { data: alloc, start: _, end: _ }
  | ConstValue::ByRef { alloc, .. } => {
- for &id in alloc.inner().relocations().values() {
+ for &id in alloc.inner().provenance().values() {
  self.collected.extend(collect_alloc_items(self.tcx, id).iter())
  }
  }
@@ -542,7 +542,7 @@ fn collect_alloc_items<'tcx>(tcx: TyCtxt<'tcx>, alloc_id: AllocId) -> Vec<MonoIt
  GlobalAlloc::Memory(alloc) => {
  trace!(?alloc_id, "global_alloc memory");
  items.extend(
- alloc.inner().relocations().values().flat_map(|id| collect_alloc_items(tcx, *id)),
+ alloc.inner().provenance().values().flat_map(|id| collect_alloc_items(tcx, *id)),
  );
  }
  GlobalAlloc::VTable(ty, trait_ref) => {

kani-compiler/src/main.rs

@@ -12,6 +12,7 @@
 #![feature(box_patterns)]
 #![feature(once_cell)]
 #![feature(rustc_private)]
+#![feature(more_qualified_paths)]
 extern crate rustc_ast;
 extern crate rustc_codegen_ssa;
 extern crate rustc_data_structures;

kani-driver/src/main.rs

@@ -1,5 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(let_chains)]
 
 use anyhow::Result;
 use args_toml::join_args;

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2022-08-30"
+channel = "nightly-2022-09-13"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

src/lib.rs

@@ -12,8 +12,6 @@
 //! binaries will download the appropriate Kani release bundle and invoke
 //! the "real" `kani` and `cargo-kani` binaries.
 
-#![warn(clippy::all, clippy::cargo)]
-
 mod cmd;
 mod os_hacks;
 mod setup;