Skip to content

Commit 02ebd42

Browse files
fzaiserfzaiser
authored
Refactor: use Size type for offsets and sizes (rust-lang#1418)
1 parent 4a7f298 commit 02ebd42

File tree

4 files changed

+48
-55
lines changed

4 files changed

+48
-55
lines changed

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

+13-14
Original file line numberDiff line numberDiff line change
@@ -273,9 +273,7 @@ impl<'tcx> GotocCtx<'tcx> {
273273
Variants::Multiple { tag_encoding, .. } => match tag_encoding {
274274
TagEncoding::Niche { .. } => {
275275
let offset = match &layout.fields {
276-
FieldsShape::Arbitrary { offsets, .. } => {
277-
offsets[0].bytes_usize()
278-
}
276+
FieldsShape::Arbitrary { offsets, .. } => offsets[0],
279277
_ => unreachable!("niche encoding must have arbitrary fields"),
280278
};
281279
let discr_ty = self.codegen_enum_discr_typ(ty);
@@ -454,19 +452,20 @@ impl<'tcx> GotocCtx<'tcx> {
454452

455453
fn codegen_allocation_data(&mut self, alloc: &'tcx Allocation) -> Vec<AllocData<'tcx>> {
456454
let mut alloc_vals = Vec::with_capacity(alloc.relocations().len() + 1);
457-
let pointer_size = self.symbol_table.machine_model().pointer_width_in_bytes();
455+
let pointer_size =
456+
Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes());
458457

459-
let mut next_offset = 0;
458+
let mut next_offset = Size::ZERO;
460459
for &(offset, alloc_id) in alloc.relocations().iter() {
461-
let offset = offset.bytes_usize();
462460
if offset > next_offset {
463-
let bytes =
464-
alloc.inspect_with_uninit_and_ptr_outside_interpreter(next_offset..offset);
461+
let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(
462+
next_offset.bytes_usize()..offset.bytes_usize(),
463+
);
465464
alloc_vals.push(AllocData::Bytes(bytes));
466465
}
467466
let ptr_offset = {
468467
let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(
469-
offset..(offset + pointer_size),
468+
offset.bytes_usize()..(offset + pointer_size).bytes_usize(),
470469
);
471470
read_target_uint(self.tcx.sess.target.options.endian, bytes)
472471
}
@@ -480,8 +479,8 @@ impl<'tcx> GotocCtx<'tcx> {
480479

481480
next_offset = offset + pointer_size;
482481
}
483-
if alloc.len() >= next_offset {
484-
let range = next_offset..alloc.len();
482+
if alloc.len() >= next_offset.bytes_usize() {
483+
let range = next_offset.bytes_usize()..alloc.len();
485484
let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(range);
486485
alloc_vals.push(AllocData::Bytes(bytes));
487486
}
@@ -598,16 +597,16 @@ impl<'tcx> GotocCtx<'tcx> {
598597
}
599598

600599
/// fetch the niche value (as both left and right value)
601-
pub fn codegen_get_niche(&self, v: Expr, offset: usize, niche_ty: Type) -> Expr {
600+
pub fn codegen_get_niche(&self, v: Expr, offset: Size, niche_ty: Type) -> Expr {
602601
v // t: T
603602
.address_of() // &t: T*
604603
.cast_to(Type::unsigned_int(8).to_pointer()) // (u8 *)&t: u8 *
605-
.plus(Expr::int_constant(offset, Type::size_t())) // ((u8 *)&t) + offset: u8 *
604+
.plus(Expr::int_constant(offset.bytes_usize(), Type::size_t())) // ((u8 *)&t) + offset: u8 *
606605
.cast_to(niche_ty.to_pointer()) // (N *)(((u8 *)&t) + offset): N *
607606
.dereference() // *(N *)(((u8 *)&t) + offset): N
608607
}
609608

610-
fn codegen_niche_literal(&mut self, ty: Ty<'tcx>, offset: usize, init: Expr) -> Expr {
609+
fn codegen_niche_literal(&mut self, ty: Ty<'tcx>, offset: Size, init: Expr) -> Expr {
611610
let cgt = self.codegen_ty(ty);
612611
let fname = self.codegen_niche_init_name(ty);
613612
let pretty_name = format!("init_niche<{}>", self.ty_pretty_name(ty));

‎kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -541,7 +541,7 @@ impl<'tcx> GotocCtx<'tcx> {
541541
// This code follows the logic in the cranelift codegen backend:
542542
// https://github.com/rust-lang/rust/blob/05d22212e89588e7c443cc6b9bc0e4e02fdfbc8d/compiler/rustc_codegen_cranelift/src/discriminant.rs#L116
543543
let offset = match &layout.fields {
544-
FieldsShape::Arbitrary { offsets, .. } => offsets[0].bytes_usize(),
544+
FieldsShape::Arbitrary { offsets, .. } => offsets[0],
545545
_ => unreachable!("niche encoding must have arbitrary fields"),
546546
};
547547

‎kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

+1-3
Original file line numberDiff line numberDiff line change
@@ -107,9 +107,7 @@ impl<'tcx> GotocCtx<'tcx> {
107107
TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => {
108108
if dataful_variant != variant_index {
109109
let offset = match &layout.fields {
110-
FieldsShape::Arbitrary { offsets, .. } => {
111-
offsets[0].bytes_usize()
112-
}
110+
FieldsShape::Arbitrary { offsets, .. } => offsets[0],
113111
_ => unreachable!("niche encoding must have arbitrary fields"),
114112
};
115113
let discr_ty = self.codegen_enum_discr_typ(pt);

‎kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

+33-37
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,6 @@ use rustc_target::abi::{
2525
};
2626
use rustc_target::spec::abi::Abi;
2727
use std::collections::BTreeMap;
28-
use std::convert::TryInto;
29-
use std::fmt::Debug;
3028
use std::iter;
3129
use std::iter::FromIterator;
3230
use tracing::{debug, trace, warn};
@@ -717,24 +715,18 @@ impl<'tcx> GotocCtx<'tcx> {
717715
self.codegen_ty_tuple_like(t, tys.to_vec())
718716
}
719717

720-
fn codegen_struct_padding<T>(
718+
fn codegen_struct_padding(
721719
&self,
722-
current_offset_in_bits: T,
723-
next_offset_in_bits: T,
720+
current_offset: Size,
721+
next_offset: Size,
724722
idx: usize,
725-
) -> Option<DatatypeComponent>
726-
where
727-
T: TryInto<u64>,
728-
T::Error: Debug,
729-
{
730-
let current_offset: u64 = current_offset_in_bits.try_into().unwrap();
731-
let next_offset: u64 = next_offset_in_bits.try_into().unwrap();
723+
) -> Option<DatatypeComponent> {
732724
assert!(current_offset <= next_offset);
733725
if current_offset < next_offset {
734726
// We need to pad to the next offset
735-
let bits = next_offset - current_offset;
727+
let padding_size = next_offset - current_offset;
736728
let name = format!("$pad{}", idx);
737-
Some(DatatypeComponent::padding(&name, bits))
729+
Some(DatatypeComponent::padding(&name, padding_size.bits()))
738730
} else {
739731
None
740732
}
@@ -747,10 +739,10 @@ impl<'tcx> GotocCtx<'tcx> {
747739
layout: &Layout,
748740
idx: usize,
749741
) -> Option<DatatypeComponent> {
750-
let align = layout.align().abi.bits();
751-
let overhang = size.bits() % align;
752-
if overhang != 0 {
753-
self.codegen_struct_padding(size.bits(), size.bits() + align - overhang, idx)
742+
let align = Size::from_bits(layout.align().abi.bits());
743+
let overhang = Size::from_bits(size.bits() % align.bits());
744+
if overhang != Size::ZERO {
745+
self.codegen_struct_padding(size, size + align - overhang, idx)
754746
} else {
755747
None
756748
}
@@ -770,16 +762,16 @@ impl<'tcx> GotocCtx<'tcx> {
770762
&mut self,
771763
flds: Vec<(String, Ty<'tcx>)>,
772764
layout: &Layout,
773-
initial_offset: usize,
765+
initial_offset: Size,
774766
) -> Vec<DatatypeComponent> {
775767
match &layout.fields() {
776768
FieldsShape::Arbitrary { offsets, memory_index } => {
777769
assert_eq!(flds.len(), offsets.len());
778770
assert_eq!(offsets.len(), memory_index.len());
779771
let mut final_fields = Vec::with_capacity(flds.len());
780-
let mut offset: u64 = initial_offset.try_into().unwrap();
772+
let mut offset = initial_offset;
781773
for idx in layout.fields().index_by_increasing_offset() {
782-
let fld_offset = offsets[idx].bits();
774+
let fld_offset = offsets[idx];
783775
let (fld_name, fld_ty) = &flds[idx];
784776
if let Some(padding) =
785777
self.codegen_struct_padding(offset, fld_offset, final_fields.len())
@@ -790,10 +782,10 @@ impl<'tcx> GotocCtx<'tcx> {
790782
final_fields.push(DatatypeComponent::field(fld_name, self.codegen_ty(*fld_ty)));
791783
let layout = self.layout_of(*fld_ty);
792784
// we compute the overall offset of the end of the current struct
793-
offset = fld_offset + layout.size.bits();
785+
offset = fld_offset + layout.size;
794786
}
795787
final_fields.extend(self.codegen_alignment_padding(
796-
Size::from_bits(offset),
788+
offset,
797789
&layout,
798790
final_fields.len(),
799791
));
@@ -810,7 +802,7 @@ impl<'tcx> GotocCtx<'tcx> {
810802
let flds: Vec<_> =
811803
tys.iter().enumerate().map(|(i, t)| (GotocCtx::tuple_fld_name(i), *t)).collect();
812804
// tuple cannot have other initial offset
813-
self.codegen_struct_fields(flds, &layout.layout, 0)
805+
self.codegen_struct_fields(flds, &layout.layout, Size::ZERO)
814806
}
815807

816808
/// A closure in Rust MIR takes two arguments:
@@ -1004,9 +996,7 @@ impl<'tcx> GotocCtx<'tcx> {
1004996
let field_ty = type_and_layout.field(ctx, idx).ty;
1005997
let field_offset = type_and_layout.fields.offset(idx);
1006998
let field_size = type_and_layout.field(ctx, idx).size;
1007-
if let Some(padding) =
1008-
ctx.codegen_struct_padding(offset.bits(), field_offset.bits(), idx)
1009-
{
999+
if let Some(padding) = ctx.codegen_struct_padding(offset, field_offset, idx) {
10101000
fields.push(padding);
10111001
}
10121002
fields.push(DatatypeComponent::Field {
@@ -1215,7 +1205,7 @@ impl<'tcx> GotocCtx<'tcx> {
12151205
self.ensure_struct(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |ctx, _| {
12161206
let variant = &def.variants().raw[0];
12171207
let layout = ctx.layout_of(ty);
1218-
ctx.codegen_variant_struct_fields(variant, subst, &layout.layout, 0)
1208+
ctx.codegen_variant_struct_fields(variant, subst, &layout.layout, Size::ZERO)
12191209
})
12201210
}
12211211

@@ -1225,7 +1215,7 @@ impl<'tcx> GotocCtx<'tcx> {
12251215
variant: &VariantDef,
12261216
subst: &'tcx InternalSubsts<'tcx>,
12271217
layout: &Layout,
1228-
initial_offset: usize,
1218+
initial_offset: Size,
12291219
) -> Vec<DatatypeComponent> {
12301220
let flds: Vec<_> =
12311221
variant.fields.iter().map(|f| (f.name.to_string(), f.ty(self.tcx, subst))).collect();
@@ -1307,7 +1297,7 @@ impl<'tcx> GotocCtx<'tcx> {
13071297
Some(variant) => {
13081298
// a single enum is pretty much like a struct
13091299
let layout = ctx.layout_of(ty).layout;
1310-
ctx.codegen_variant_struct_fields(variant, subst, &layout, 0)
1300+
ctx.codegen_variant_struct_fields(variant, subst, &layout, Size::ZERO)
13111301
}
13121302
}
13131303
}
@@ -1331,7 +1321,7 @@ impl<'tcx> GotocCtx<'tcx> {
13311321
// of each union field is the name of the corresponding discriminant.
13321322
let discr_t = ctx.codegen_enum_discr_typ(ty);
13331323
let int = ctx.codegen_ty(discr_t);
1334-
let discr_offset = ctx.layout_of(discr_t).size.bits_usize();
1324+
let discr_offset = ctx.layout_of(discr_t).size;
13351325
let initial_offset =
13361326
ctx.variant_min_offset(variants).unwrap_or(discr_offset);
13371327
let mut fields = vec![DatatypeComponent::field("case", int)];
@@ -1382,7 +1372,14 @@ impl<'tcx> GotocCtx<'tcx> {
13821372
?subst,
13831373
"codegen_enum: Niche"
13841374
);
1385-
ctx.codegen_enum_cases(name, pretty_name, adtdef, subst, variants, 0)
1375+
ctx.codegen_enum_cases(
1376+
name,
1377+
pretty_name,
1378+
adtdef,
1379+
subst,
1380+
variants,
1381+
Size::ZERO,
1382+
)
13861383
}
13871384
}
13881385
}
@@ -1393,7 +1390,7 @@ impl<'tcx> GotocCtx<'tcx> {
13931390
pub(crate) fn variant_min_offset(
13941391
&self,
13951392
variants: &IndexVec<VariantIdx, Layout>,
1396-
) -> Option<usize> {
1393+
) -> Option<Size> {
13971394
variants
13981395
.iter()
13991396
.filter_map(|lo| {
@@ -1407,8 +1404,7 @@ impl<'tcx> GotocCtx<'tcx> {
14071404
// fields.
14081405
Some(
14091406
lo.fields()
1410-
.offset(lo.fields().index_by_increasing_offset().nth(0).unwrap())
1411-
.bits_usize(),
1407+
.offset(lo.fields().index_by_increasing_offset().nth(0).unwrap()),
14121408
)
14131409
}
14141410
})
@@ -1481,7 +1477,7 @@ impl<'tcx> GotocCtx<'tcx> {
14811477
def: &'tcx AdtDef,
14821478
subst: &'tcx InternalSubsts<'tcx>,
14831479
layouts: &IndexVec<VariantIdx, Layout>,
1484-
initial_offset: usize,
1480+
initial_offset: Size,
14851481
) -> Vec<DatatypeComponent> {
14861482
def.variants()
14871483
.iter_enumerated()
@@ -1513,7 +1509,7 @@ impl<'tcx> GotocCtx<'tcx> {
15131509
case: &VariantDef,
15141510
subst: &'tcx InternalSubsts<'tcx>,
15151511
variant: &Layout,
1516-
initial_offset: usize,
1512+
initial_offset: Size,
15171513
) -> Type {
15181514
let case_name = format!("{}::{}", name, case.name);
15191515
let pretty_name = format!("{}::{}", pretty_name, case.name);

0 commit comments

Comments
 (0)