Skip to content

Commit

Permalink
Merge pull request minirust#148 from essickmango/enum_variant_projection
Browse files Browse the repository at this point in the history
Enum variant projection
  • Loading branch information
RalfJung authored Nov 24, 2023
2 parents 6b49148 + d3eeae1 commit d40e2f6
Show file tree
Hide file tree
Showing 7 changed files with 127 additions and 0 deletions.
11 changes: 11 additions & 0 deletions spec/lang/step/expressions.md
Original file line number Diff line number Diff line change
Expand Up @@ -264,5 +264,16 @@ impl<M: Memory> Machine<M> {
let ptr = self.ptr_offset_inbounds(root.ptr, offset.bytes())?;
ret((Place { ptr, ..root }, field_ty))
}

fn eval_place(&mut self, PlaceExpr::Downcast { root, variant_idx }: PlaceExpr) -> NdResult<(Place<M>, Type)> {
let (root, ty) = self.eval_place(root)?;
// We only need to downcast the enum type into the variant data type
// since all the enum data must have the same size with offset 0 (invariant).
let var_ty = match ty {
Type::Enum { variants, .. } => variants[variant_idx].ty,
_ => panic!("enum downcast on non-enum"),
};
ret((root, var_ty))
}
}
```
8 changes: 8 additions & 0 deletions spec/lang/syntax.md
Original file line number Diff line number Diff line change
Expand Up @@ -175,6 +175,14 @@ pub enum PlaceExpr {
#[specr::indirection]
index: ValueExpr,
},
/// Enum variant downcast.
Downcast {
/// The base enum to project to the specific variant.
#[specr::indirection]
root: PlaceExpr,
/// The variant index to project to.
variant_idx: Int,
},
}
```

Expand Down
8 changes: 8 additions & 0 deletions spec/lang/well-formed.md
Original file line number Diff line number Diff line change
Expand Up @@ -313,6 +313,14 @@ impl PlaceExpr {
_ => throw!(),
}
}
Downcast { root, variant_idx } => {
let root = root.check_wf::<T>(locals, prog)?;
match root {
// A valid downcast points to an existing variant.
Type::Enum { variants, .. } => variants.get(variant_idx)?.ty,
_ => throw!(),
}
}
})
}
}
Expand Down
85 changes: 85 additions & 0 deletions tooling/minitest/src/tests/enum_downcast.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,85 @@
use crate::*;

/// Ill-formed: Downcasting to an out-of-bounds variant.
#[test]
fn out_of_bounds_downcast() {
let u8_t = int_ty(Signedness::Unsigned, size(1));
let enum_ty = enum_ty(&[enum_variant(u8_t, &[])], Discriminator::Known(0.into()), size(1), align(1));
let locals = &[enum_ty, u8_t];
let stmts = &[
storage_live(0),
storage_live(1),
assign(local(1), load(downcast(local(0), 1))), // ill-formed here, variant 1 doesn't exist
];
let prog = small_program(locals, stmts);
assert_ill_formed(prog);
}

/// Works: Both assigning to and from a downcast.
#[test]
fn valid_downcast() {
let u8_t = int_ty(Signedness::Unsigned, size(1));
let enum_ty = enum_ty(&[enum_variant(u8_t, &[])], Discriminator::Known(0.into()), size(1), align(1));
let locals = &[enum_ty, u8_t];
let stmts = &[
storage_live(0),
storage_live(1),
assign(downcast(local(0), 0), const_int(42u8)),
assign(local(1), load(downcast(local(0), 0))),
];
let prog = small_program(locals, stmts);
assert_stop(prog);
}


/// UB: Assigning to first byte of variant 0 doesn't init both data bytes of variant 1.
#[test]
fn downcasts_give_different_place() {
// setup enum where the first two bytes are data (u8 / u16) and the third byte is the tag.
let u8_t = int_ty(Signedness::Unsigned, size(1));
let variant1 = enum_variant(tuple_ty(&[(size(1), u8_t)], size(4), align(2)), &[(size(2), 0u8)]);
let u16_t = int_ty(Signedness::Unsigned, size(2));
let variant2 = enum_variant(tuple_ty(&[(size(0), u16_t)], size(4), align(2)), &[(size(2), 1u8)]);
let discriminator = Discriminator::Unknown {
offset: size(2),
fallback: GcCow::new(Discriminator::Invalid),
children: [(0, Discriminator::Known(0.into())), (1, Discriminator::Known(1.into()))].into_iter().collect()
};
let enum_ty = enum_ty(&[variant1, variant2], discriminator, size(4), align(2));

let locals = &[enum_ty, u16_t];
let stmts = &[
storage_live(0),
storage_live(1),
assign(field(downcast(local(0), 0), 0), const_int(42u8)),
assign(local(1), load(field(downcast(local(0), 1), 0))), // UB here, only the lower byte is initialized
];
let prog = small_program(locals, stmts);
assert_ub(prog, "load at type Int(IntType { signed: Unsigned, size: Size(2 bytes) }) but the data in memory violates the validity invariant");
}

/// Works: Assigning to both bytes of variant 1 allows reads from variant 0.
#[test]
fn downcasts_give_different_place2() {
// setup enum where the first two bytes are data (u8 / u16) and the third byte is the tag.
let u8_t = int_ty(Signedness::Unsigned, size(1));
let variant1 = enum_variant(tuple_ty(&[(size(1), u8_t)], size(4), align(2)), &[(size(2), 0)]);
let u16_t = int_ty(Signedness::Unsigned, size(2));
let variant2 = enum_variant(tuple_ty(&[(size(0), u16_t)], size(4), align(2)), &[(size(2), 1)]);
let discriminator = Discriminator::Unknown {
offset: size(2),
fallback: GcCow::new(Discriminator::Invalid),
children: [(0, Discriminator::Known(0.into())), (1, Discriminator::Known(1.into()))].into_iter().collect()
};
let enum_ty = enum_ty(&[variant1, variant2], discriminator, size(4), align(2));

let locals = &[enum_ty, u8_t];
let stmts = &[
storage_live(0),
storage_live(1),
assign(field(downcast(local(0), 1), 0), const_int(42u16)),
assign(local(1), load(field(downcast(local(0), 0), 0))),
];
let prog = small_program(locals, stmts);
assert_stop(prog);
}
1 change: 1 addition & 0 deletions tooling/minitest/src/tests/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ mod concurrency;
mod data_race;
mod dereferenceable;
mod div_zero;
mod enum_downcast;
mod enum_representation;
mod heap_intrinsics;
mod ill_formed;
Expand Down
8 changes: 8 additions & 0 deletions tooling/miniutil/src/build/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -216,6 +216,14 @@ pub fn index(root: PlaceExpr, index: ValueExpr) -> PlaceExpr {
}
}

/// An enum downcast into the variant at the specified index.
pub fn downcast(root: PlaceExpr, variant_idx: impl Into<Int>) -> PlaceExpr {
PlaceExpr::Downcast {
root: GcCow::new(root),
variant_idx: variant_idx.into(),
}
}

/// A place suited for zero-sized accesses.
pub fn zst_place() -> PlaceExpr {
let ptr = ValueExpr::Constant(Constant::InvalidPointer(1.into()), <*const ()>::get_type());
Expand Down
6 changes: 6 additions & 0 deletions tooling/miniutil/src/fmt/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,12 @@ pub(super) fn fmt_place_expr(p: PlaceExpr, comptypes: &mut Vec<CompType>) -> Fmt
// This can be considered atomic due to the same reasoning as for PlaceExpr::Field, see above.
FmtExpr::Atomic(format!("{root}[{index}]"))
}
PlaceExpr::Downcast { root, variant_idx } => {
let root = fmt_place_expr(root.extract(), comptypes).to_atomic_string();
// This is not atomic as `local(1) as variant 3.0` illustrates. (Field 0 of downcast)
// We can't do it nicely like in the Rust MIR ({root} as {variant name}) since we have no variant names.
FmtExpr::NonAtomic(format!("{root} as variant {variant_idx}"))
}
}
}

Expand Down

0 comments on commit d40e2f6

Please sign in to comment.