Upgrade the toolchain to nightly-2023-04-16 (#2406)

Update the toolchain to use nightly-2023-04-16. Changes were related to the following changes to the toolchain: - rust-lang/rust#108944 - rust-lang/rust#108148 - rust-lang/rust#108471 - rust-lang/rust#109358 - rust-lang/rust#109849 - rust-lang/rust#109819 - rust-lang/rust#109718 - rust-lang/rust#109092 - rust-lang/rust#108856 - rust-lang/rust#105613 - rust-lang/rust#103042 - rust-lang/rust#109716 - rust-lang/rust#108340 - rust-lang/rust#102906 - rust-lang/rust#98112 - rust-lang/rust#108080
model-checking · May 16, 2023 · 6f7aa65 · 6f7aa65
1 parent 2a09d79
commit 6f7aa65
Show file tree

Hide file tree

Showing 37 changed files with 181 additions and 131 deletions.
diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
@@ -851,6 +851,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();

diff --git 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/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -51,7 +51,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/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -9,7 +9,7 @@ use cbmc::goto_program::{
     Location, Stmt, 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;
@@ -753,7 +753,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,
@@ -781,7 +781,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,
@@ -790,8 +793,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
@@ -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),
             },
         }
     }
@@ -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
@@ -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
@@ -17,6 +17,8 @@ use cbmc::goto_program::{
 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;
@@ -321,7 +323,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,
@@ -341,7 +347,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     if idx == *discriminant_field {
                         Expr::int_constant(0, self.codegen_ty(field_ty))
                     } else {
-                        self.codegen_operand(&operands[idx])
+                        self.codegen_operand(&operands[idx.into()])
                     }
                 })
                 .collect(),
@@ -358,7 +364,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 {
@@ -400,7 +406,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,
             );
@@ -419,7 +425,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 {
@@ -449,8 +455,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,
                 )
             }
@@ -464,7 +470,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 {
@@ -487,7 +493,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,
                 )
@@ -537,6 +543,10 @@ impl<'tcx> GotocCtx<'tcx> {
                 let t = self.monomorphize(*t);
                 self.codegen_pointer_cast(k, e, t, loc)
             }
+            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)
             }
@@ -636,7 +646,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
@@ -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",
             ),
@@ -165,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()
@@ -187,9 +192,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 => {
@@ -232,19 +235,23 @@ 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 {
                         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);
                         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(_))
                         {
@@ -548,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(..)
@@ -562,6 +570,7 @@ impl<'tcx> GotocCtx<'tcx> {
                                 .with_location(loc),
                         ]
                     }
+                    InstanceDef::ThreadLocalShim(_) => todo!(),
                 };
                 stmts.push(self.codegen_end_call(target.as_ref(), loc));
                 Stmt::block(stmts, loc)