Upgrade toolchain to 2023-02-05 (#2347)

tautschnig · celinval · web-flow · commit 22b14f400edf · 2023-04-14T22:43:15.000Z
Co-authored-by: Celina G. Val &lt;celinval@amazon.com&gt;
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -624,6 +624,17 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// Given a projection, generate an lvalue that represents the given variant index.
+    pub fn codegen_variant_lvalue(
+        &mut self,
+        initial_projection: ProjectedPlace<'tcx>,
+        variant_idx: VariantIdx,
+    ) -> ProjectedPlace<'tcx> {
+        debug!(?initial_projection, ?variant_idx, "codegen_variant_lvalue");
+        let downcast = ProjectionElem::Downcast(None, variant_idx);
+        self.codegen_projection(Ok(initial_projection), downcast).unwrap()
+    }
+
     // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.ProjectionElem.html
     // ConstantIndex
     // [−]
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -2,6 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use super::typ::pointee_type;
+use crate::codegen_cprover_gotoc::codegen::place::{ProjectedPlace, TypeOrVariant};
 use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
@@ -17,9 +18,9 @@ use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place,
 use rustc_middle::ty::adjustment::PointerCast;
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry};
-use rustc_target::abi::{FieldsShape, Size, TagEncoding, Variants};
+use rustc_target::abi::{FieldsShape, Size, TagEncoding, VariantIdx, Variants};
 use std::collections::BTreeMap;
-use tracing::{debug, warn};
+use tracing::{debug, trace, warn};
 
 impl<'tcx> GotocCtx<'tcx> {
     fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand<'tcx>, e2: &Operand<'tcx>) -> Expr {
@@ -279,13 +280,112 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// Create an initializer for a generator struct.
+    fn codegen_rvalue_generator(&mut self, operands: &[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,
+            _ => unreachable!(
+                "Expected generators to have multiple variants and direct encoding, but found: {layout:?}"
+            ),
+        };
+        let overall_t = self.codegen_ty(ty);
+        let direct_fields = overall_t.lookup_field("direct_fields", &self.symbol_table).unwrap();
+        let mut operands_iter = operands.iter();
+        let direct_fields_expr = Expr::struct_expr_from_values(
+            direct_fields.typ(),
+            layout
+                .fields
+                .index_by_increasing_offset()
+                .map(|idx| {
+                    let field_ty = layout.field(self, idx).ty;
+                    if idx == *discriminant_field {
+                        Expr::int_constant(0, self.codegen_ty(field_ty))
+                    } else {
+                        self.codegen_operand(operands_iter.next().unwrap())
+                    }
+                })
+                .collect(),
+            &self.symbol_table,
+        );
+        assert!(operands_iter.next().is_none());
+        Expr::union_expr(overall_t, "direct_fields", direct_fields_expr, &self.symbol_table)
+    }
+
+    /// This code will generate an expression that initializes an enumeration.
+    ///
+    /// It will first create a temporary variant with the same enum type.
+    /// Initialize the case structure and set its discriminant.
+    /// Finally, it will return the temporary value.
+    fn codegen_rvalue_enum_aggregate(
+        &mut self,
+        variant_index: VariantIdx,
+        operands: &[Operand<'tcx>],
+        res_ty: Ty<'tcx>,
+        loc: Location,
+    ) -> Expr {
+        let mut stmts = vec![];
+        let typ = self.codegen_ty(res_ty);
+        // 1- Create a temporary value of the enum type.
+        tracing::debug!(?typ, ?res_ty, "aggregate_enum");
+        let (temp_var, decl) = self.decl_temp_variable(typ.clone(), None, loc);
+        stmts.push(decl);
+        if !operands.is_empty() {
+            // 2- Initialize the members of the temporary variant.
+            let initial_projection = ProjectedPlace::try_new(
+                temp_var.clone(),
+                TypeOrVariant::Type(res_ty),
+                None,
+                None,
+                self,
+            )
+            .unwrap();
+            let variant_proj = self.codegen_variant_lvalue(initial_projection, variant_index);
+            let variant_expr = variant_proj.goto_expr.clone();
+            let layout = self.layout_of(res_ty);
+            let fields = match &layout.variants {
+                Variants::Single { index } => {
+                    if *index != variant_index {
+                        // This may occur if all variants except for the one pointed by
+                        // index can never be constructed. Generic code might still try
+                        // to initialize the non-existing invariant.
+                        trace!(?res_ty, ?variant_index, "Unreachable invariant");
+                        return Expr::nondet(typ);
+                    }
+                    &layout.fields
+                }
+                Variants::Multiple { variants, .. } => &variants[variant_index].fields,
+            };
+
+            trace!(?variant_expr, ?fields, ?operands, "codegen_aggregate enum");
+            let init_struct = Expr::struct_expr_from_values(
+                variant_expr.typ().clone(),
+                fields
+                    .index_by_increasing_offset()
+                    .map(|idx| self.codegen_operand(&operands[idx]))
+                    .collect(),
+                &self.symbol_table,
+            );
+            let assign_case = variant_proj.goto_expr.assign(init_struct, loc);
+            stmts.push(assign_case);
+        }
+        // 3- Set discriminant.
+        let set_discriminant =
+            self.codegen_set_discriminant(res_ty, temp_var.clone(), variant_index, loc);
+        stmts.push(set_discriminant);
+        // 4- Return temporary variable.
+        stmts.push(temp_var.as_stmt(loc));
+        Expr::statement_expression(stmts, typ)
+    }
+
     fn codegen_rvalue_aggregate(
         &mut self,
-        k: &AggregateKind<'tcx>,
+        aggregate: &AggregateKind<'tcx>,
         operands: &[Operand<'tcx>],
         res_ty: Ty<'tcx>,
+        loc: Location,
     ) -> Expr {
-        match *k {
+        match *aggregate {
             AggregateKind::Array(et) => {
                 if et.is_unit() {
                     Expr::struct_expr_from_values(
@@ -304,7 +404,44 @@ impl<'tcx> GotocCtx<'tcx> {
                     )
                 }
             }
-            AggregateKind::Tuple => {
+            AggregateKind::Adt(_, _, _, _, Some(active_field_index)) => {
+                assert!(res_ty.is_union());
+                assert_eq!(operands.len(), 1);
+                let typ = self.codegen_ty(res_ty);
+                let components = typ.lookup_components(&self.symbol_table).unwrap();
+                Expr::union_expr(
+                    typ,
+                    components[active_field_index].name(),
+                    self.codegen_operand(&operands[0]),
+                    &self.symbol_table,
+                )
+            }
+            AggregateKind::Adt(_, _, _, _, _) if res_ty.is_simd() => {
+                let typ = self.codegen_ty(res_ty);
+                let layout = self.layout_of(res_ty);
+                let vector_element_type = typ.base_type().unwrap().clone();
+                Expr::vector_expr(
+                    typ,
+                    layout
+                        .fields
+                        .index_by_increasing_offset()
+                        .map(|idx| {
+                            let cgo = self.codegen_operand(&operands[idx]);
+                            // The input operand might actually be a one-element array, as seen
+                            // when running assess on firecracker.
+                            if *cgo.typ() == vector_element_type {
+                                cgo
+                            } else {
+                                cgo.transmute_to(vector_element_type.clone(), &self.symbol_table)
+                            }
+                        })
+                        .collect(),
+                )
+            }
+            AggregateKind::Adt(_, variant_index, ..) if res_ty.is_enum() => {
+                self.codegen_rvalue_enum_aggregate(variant_index, operands, res_ty, loc)
+            }
+            AggregateKind::Adt(..) | AggregateKind::Closure(..) | AggregateKind::Tuple => {
                 let typ = self.codegen_ty(res_ty);
                 let layout = self.layout_of(res_ty);
                 Expr::struct_expr_from_values(
@@ -317,9 +454,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     &self.symbol_table,
                 )
             }
-            AggregateKind::Adt(_, _, _, _, _) => unimplemented!(),
-            AggregateKind::Closure(_, _) => unimplemented!(),
-            AggregateKind::Generator(_, _, _) => unimplemented!(),
+            AggregateKind::Generator(_, _, _) => self.codegen_rvalue_generator(&operands, res_ty),
         }
     }
 
@@ -406,7 +541,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_get_discriminant(place, pt, res_ty)
             }
             Rvalue::Aggregate(ref k, operands) => {
-                self.codegen_rvalue_aggregate(k, operands, res_ty)
+                self.codegen_rvalue_aggregate(k, operands, res_ty, loc)
             }
             Rvalue::ThreadLocalRef(def_id) => {
                 // Since Kani is single-threaded, we treat a thread local like a static variable:
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -16,6 +16,7 @@ use rustc_middle::ty;
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{Instance, InstanceDef, Ty};
 use rustc_span::Span;
+use rustc_target::abi::VariantIdx;
 use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
 use tracing::{debug, debug_span, trace};
 
@@ -55,68 +56,11 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             StatementKind::Deinit(place) => self.codegen_deinit(place, location),
             StatementKind::SetDiscriminant { place, variant_index } => {
-                // this requires place points to an enum type.
-                let pt = self.place_ty(place);
-                let layout = self.layout_of(pt);
-                match &layout.variants {
-                    Variants::Single { .. } => Stmt::skip(location),
-                    Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
-                        TagEncoding::Direct => {
-                            let discr =
-                                pt.discriminant_for_variant(self.tcx, *variant_index).unwrap();
-                            let discr_t = self.codegen_enum_discr_typ(pt);
-                            // The constant created below may not fit into the type.
-                            // https://github.com/model-checking/kani/issues/996
-                            //
-                            // It doesn't matter if the type comes from `self.codegen_enum_discr_typ(pt)`
-                            // or `discr.ty`. It looks like something is wrong with `discriminat_for_variant`
-                            // because when it tries to codegen `std::cmp::Ordering` (which should produce
-                            // discriminant values -1, 0 and 1) it produces values 255, 0 and 1 with i8 types:
-                            //
-                            // debug!("DISCRIMINANT - val:{:?} ty:{:?}", discr.val, discr.ty);
-                            // 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));
-                            let place_goto_expr = unwrap_or_return_codegen_unimplemented_stmt!(
-                                self,
-                                self.codegen_place(place)
-                            )
-                            .goto_expr;
-                            self.codegen_discriminant_field(place_goto_expr, pt)
-                                .assign(discr, location)
-                        }
-                        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"),
-                                };
-                                let discr_ty = self.codegen_enum_discr_typ(pt);
-                                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);
-                                let value = if niche_value == 0
-                                    && matches!(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)
-                            } else {
-                                Stmt::skip(location)
-                            }
-                        }
-                    },
-                }
+                let dest_ty = self.place_ty(place);
+                let dest_expr =
+                    unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
+                        .goto_expr;
+                self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location)
             }
             StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me
             StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me
@@ -259,6 +203,64 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
+    /// Create a statement that sets the variable discriminant to the value that corresponds to the
+    /// variant index.
+    pub fn codegen_set_discriminant(
+        &mut self,
+        dest_ty: Ty<'tcx>,
+        dest_expr: Expr,
+        variant_index: VariantIdx,
+        location: Location,
+    ) -> Stmt {
+        // this requires place points to an enum type.
+        let layout = self.layout_of(dest_ty);
+        match &layout.variants {
+            Variants::Single { .. } => Stmt::skip(location),
+            Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
+                TagEncoding::Direct => {
+                    let discr = dest_ty.discriminant_for_variant(self.tcx, variant_index).unwrap();
+                    let discr_t = self.codegen_enum_discr_typ(dest_ty);
+                    // The constant created below may not fit into the type.
+                    // https://github.com/model-checking/kani/issues/996
+                    //
+                    // It doesn't matter if the type comes from `self.codegen_enum_discr_typ(pt)`
+                    // or `discr.ty`. It looks like something is wrong with `discriminat_for_variant`
+                    // because when it tries to codegen `std::cmp::Ordering` (which should produce
+                    // discriminant values -1, 0 and 1) it produces values 255, 0 and 1 with i8 types:
+                    //
+                    // debug!("DISCRIMINANT - val:{:?} ty:{:?}", discr.val, discr.ty);
+                    // 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)
+                }
+                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"),
+                        };
+                        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);
+                        let value = if niche_value == 0
+                            && matches!(tag.primitive(), Primitive::Pointer(_))
+                        {
+                            discr_ty.null()
+                        } else {
+                            Expr::int_constant(niche_value, discr_ty.clone())
+                        };
+                        self.codegen_get_niche(dest_expr, offset, discr_ty).assign(value, location)
+                    } else {
+                        Stmt::skip(location)
+                    }
+                }
+            },
+        }
+    }
+
     /// From rustc doc: "This writes `uninit` bytes to the entire place."
     /// Our model of GotoC has a similar statement, which is later lowered
     /// to assigning a Nondet in CBMC, with a comment specifying that it
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-02-04"
+channel = "nightly-2023-02-05"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/kani/Enum/multiple_never.rs b/tests/kani/Enum/multiple_never.rs
diff --git a/tests/kani/Enum/one_two.rs b/tests/kani/Enum/one_two.rs
