Skip to content

Commit de71c09

Browse files
authored
Clean up codegen_niche_literal (#1486)
1 parent 88aace3 commit de71c09

File tree

2 files changed

+16
-41
lines changed

2 files changed

+16
-41
lines changed

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

Lines changed: 16 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ use rustc_middle::ty::layout::LayoutOf;
1414
use rustc_middle::ty::{self, Const, ConstKind, FloatTy, Instance, IntTy, Ty, Uint, UintTy};
1515
use rustc_span::def_id::DefId;
1616
use rustc_span::Span;
17-
use rustc_target::abi::{FieldsShape, Size, TagEncoding, Variants};
17+
use rustc_target::abi::{Size, TagEncoding, Variants};
1818
use tracing::{debug, trace};
1919

2020
enum AllocData<'a> {
@@ -271,15 +271,24 @@ impl<'tcx> GotocCtx<'tcx> {
271271
_ => unreachable!(),
272272
}
273273
}
274-
Variants::Multiple { tag_encoding, .. } => match tag_encoding {
274+
Variants::Multiple { tag_encoding, tag_field, .. } => match tag_encoding {
275275
TagEncoding::Niche { .. } => {
276-
let offset = match &layout.fields {
277-
FieldsShape::Arbitrary { offsets, .. } => offsets[0],
278-
_ => unreachable!("niche encoding must have arbitrary fields"),
279-
};
276+
let niche_offset = layout.fields.offset(*tag_field);
277+
assert_eq!(
278+
niche_offset,
279+
Size::ZERO,
280+
"nonzero offset for niche in scalar"
281+
);
280282
let discr_ty = self.codegen_enum_discr_typ(ty);
281283
let niche_val = self.codegen_scalar(s, discr_ty, span);
282-
self.codegen_niche_literal(ty, offset, niche_val)
284+
let result_type = self.codegen_ty(ty);
285+
let niche_type = niche_val.typ().clone();
286+
assert_eq!(
287+
niche_type.sizeof_in_bits(&self.symbol_table),
288+
result_type.sizeof_in_bits(&self.symbol_table),
289+
"niche type and enum have different size in scalar"
290+
);
291+
niche_val.transmute_to(result_type, &self.symbol_table)
283292
}
284293

285294
TagEncoding::Direct => {
@@ -589,11 +598,6 @@ impl<'tcx> GotocCtx<'tcx> {
589598
}
590599
}
591600

592-
fn codegen_niche_init_name(&self, ty: Ty<'tcx>) -> String {
593-
let name = self.ty_mangled_name(ty);
594-
format!("gen-{}:niche", name)
595-
}
596-
597601
/// fetch the niche value (as both left and right value)
598602
pub fn codegen_get_niche(&self, v: Expr, offset: Size, niche_ty: Type) -> Expr {
599603
v // t: T
@@ -604,31 +608,6 @@ impl<'tcx> GotocCtx<'tcx> {
604608
.dereference() // *(N *)(((u8 *)&t) + offset): N
605609
}
606610

607-
fn codegen_niche_literal(&mut self, ty: Ty<'tcx>, offset: Size, init: Expr) -> Expr {
608-
let cgt = self.codegen_ty(ty);
609-
let fname = self.codegen_niche_init_name(ty);
610-
let pretty_name = format!("init_niche<{}>", self.ty_pretty_name(ty));
611-
self.ensure(&fname, |tcx, _| {
612-
let target_ty = init.typ().clone(); // N
613-
let param = tcx.gen_function_parameter(1, &fname, target_ty.clone());
614-
let var = tcx.gen_function_local_variable(2, &fname, cgt.clone()).to_expr();
615-
let body = vec![
616-
Stmt::decl(var.clone(), None, Location::none()),
617-
tcx.codegen_get_niche(var.clone(), offset, target_ty)
618-
.assign(param.to_expr(), Location::none()),
619-
var.ret(Location::none()),
620-
];
621-
Symbol::function(
622-
&fname,
623-
Type::code(vec![param.to_function_parameter()], cgt),
624-
Some(Stmt::block(body, Location::none())),
625-
pretty_name,
626-
Location::none(),
627-
)
628-
});
629-
self.find_function(&fname).unwrap().call(vec![init])
630-
}
631-
632611
/// Ensure that the given instance is in the symbol table, returning the symbol.
633612
///
634613
/// FIXME: The function should not have to return the type of the function symbol as well

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -271,10 +271,6 @@ impl<'tcx> GotocCtx<'tcx> {
271271
Type::union_tag(union_name)
272272
}
273273

274-
pub fn find_function<T: Into<InternedString>>(&mut self, fname: T) -> Option<Expr> {
275-
self.symbol_table.lookup(fname).map(|s| s.to_expr())
276-
}
277-
278274
/// Makes a __attribute__((constructor)) fnname() {body} initalizer function
279275
pub fn register_initializer(&mut self, var_name: &str, body: Stmt) -> &Symbol {
280276
let fn_name = Self::initializer_fn_name(var_name);

0 commit comments

Comments
 (0)