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",
 ]

cprover_bindings/src/goto_program/expr.rs

@@ -544,6 +544,13 @@ impl Expr {
         Self::double_constant(c)
     }
 
+    /// `if (c) { t } else { e }`
+    pub fn if_then_else_expr(c: Expr, t: Expr, e: Expr) -> Self {
+        assert!(c.typ().is_bool());
+        assert!(t.typ() == e.typ());
+        expr!(If { c, t, e }, t.typ().clone())
+    }
+
     pub fn empty_union(typ: Type, st: &SymbolTable) -> Self {
         assert!(typ.is_union() || typ.is_union_tag());
         assert!(typ.lookup_components(st).unwrap().is_empty());

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 = Expr::if_then_else_expr(eq_expr, 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://github.com/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,
-            }) => {
+            mir::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://github.com/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;