Clean up codegen_niche_literal (#1486)

model-checking · Aug 11, 2022 · de71c09 · de71c09
1 parent 88aace3
commit de71c09
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 41 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -14,7 +14,7 @@ use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{self, Const, ConstKind, FloatTy, Instance, IntTy, Ty, Uint, UintTy};
 use rustc_span::def_id::DefId;
 use rustc_span::Span;
-use rustc_target::abi::{FieldsShape, Size, TagEncoding, Variants};
+use rustc_target::abi::{Size, TagEncoding, Variants};
 use tracing::{debug, trace};
 
 enum AllocData<'a> {
@@ -271,15 +271,24 @@ impl<'tcx> GotocCtx<'tcx> {
                                 _ => unreachable!(),
                             }
                         }
-                        Variants::Multiple { tag_encoding, .. } => match tag_encoding {
+                        Variants::Multiple { tag_encoding, tag_field, .. } => match tag_encoding {
                             TagEncoding::Niche { .. } => {
-                                let offset = match &layout.fields {
-                                    FieldsShape::Arbitrary { offsets, .. } => offsets[0],
-                                    _ => unreachable!("niche encoding must have arbitrary fields"),
-                                };
+                                let niche_offset = layout.fields.offset(*tag_field);
+                                assert_eq!(
+                                    niche_offset,
+                                    Size::ZERO,
+                                    "nonzero offset for niche in scalar"
+                                );
                                 let discr_ty = self.codegen_enum_discr_typ(ty);
                                 let niche_val = self.codegen_scalar(s, discr_ty, span);
-                                self.codegen_niche_literal(ty, offset, niche_val)
+                                let result_type = self.codegen_ty(ty);
+                                let niche_type = niche_val.typ().clone();
+                                assert_eq!(
+                                    niche_type.sizeof_in_bits(&self.symbol_table),
+                                    result_type.sizeof_in_bits(&self.symbol_table),
+                                    "niche type and enum have different size in scalar"
+                                );
+                                niche_val.transmute_to(result_type, &self.symbol_table)
                             }
 
                             TagEncoding::Direct => {
@@ -589,11 +598,6 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    fn codegen_niche_init_name(&self, ty: Ty<'tcx>) -> String {
-        let name = self.ty_mangled_name(ty);
-        format!("gen-{}:niche", name)
-    }
-
     /// fetch the niche value (as both left and right value)
     pub fn codegen_get_niche(&self, v: Expr, offset: Size, niche_ty: Type) -> Expr {
         v // t: T
@@ -604,31 +608,6 @@ impl<'tcx> GotocCtx<'tcx> {
             .dereference() // *(N *)(((u8 *)&t) + offset): N
     }
 
-    fn codegen_niche_literal(&mut self, ty: Ty<'tcx>, offset: Size, init: Expr) -> Expr {
-        let cgt = self.codegen_ty(ty);
-        let fname = self.codegen_niche_init_name(ty);
-        let pretty_name = format!("init_niche<{}>", self.ty_pretty_name(ty));
-        self.ensure(&fname, |tcx, _| {
-            let target_ty = init.typ().clone(); // N
-            let param = tcx.gen_function_parameter(1, &fname, target_ty.clone());
-            let var = tcx.gen_function_local_variable(2, &fname, cgt.clone()).to_expr();
-            let body = vec![
-                Stmt::decl(var.clone(), None, Location::none()),
-                tcx.codegen_get_niche(var.clone(), offset, target_ty)
-                    .assign(param.to_expr(), Location::none()),
-                var.ret(Location::none()),
-            ];
-            Symbol::function(
-                &fname,
-                Type::code(vec![param.to_function_parameter()], cgt),
-                Some(Stmt::block(body, Location::none())),
-                pretty_name,
-                Location::none(),
-            )
-        });
-        self.find_function(&fname).unwrap().call(vec![init])
-    }
-
     /// Ensure that the given instance is in the symbol table, returning the symbol.
     ///
     /// FIXME: The function should not have to return the type of the function symbol as well

diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -271,10 +271,6 @@ impl<'tcx> GotocCtx<'tcx> {
         Type::union_tag(union_name)
     }
 
-    pub fn find_function<T: Into<InternedString>>(&mut self, fname: T) -> Option<Expr> {
-        self.symbol_table.lookup(fname).map(|s| s.to_expr())
-    }
-
     /// Makes a __attribute__((constructor)) fnname() {body} initalizer function
     pub fn register_initializer(&mut self, var_name: &str, body: Stmt) -> &Symbol {
         let fn_name = Self::initializer_fn_name(var_name);