Feature request: more information in enum layout

[N1ark]

TL;DR: Charon needs more information regarding niche layouts, as otherwise we cannot reliably compute whether a tag is valid

The current information Charon outputs for an enum layout is actually not sufficient to detect some fun cases of UB reliably. I discovered this through this miri test.

In particular it has this enum:

enum Foo {
    Var1,       // variant 0, tag 2
    Var2(bool), // variant 1, untagged (valid values are 0=false and 1=true)
    Var3,       // variant 2, tag 4
}

And then does this:

let invalid: Foo = mem::transmute(3u8);
assert!(matches!(invalid, Foo::Var2(_)));

Although line 1 is UB with validity checks, Miri allows disabling those, in which case instead we get UB on line 2 for a different reason:

• the niche_variants range of the enum (which variants are niches) is 0..=2 (it includes 1, but 1 is the untagged variant)
• however using 3 is not valid, and is verified in const-eval by these lines
  https://github.com/rust-lang/rust/blob/1b7d722f429f09c87b08b757d89c689c6cf7f6e7/compiler/rustc_const_eval/src/interpret/discriminant.rs#L177-L181
• basically, we're in the niche range (0..=2) but we're using the untagged variant (1), so it's invalid
• however Charon currently only exports the fact variant 1 is niched and that variants 0 and 2 have tags 2 and 4 respectively; there is no information on what the niche range is; as such the only way to detect this UB is by deserialising the whole value with validity checks, which is "too much work", we should be able to detect it earlier.

The solution to this is extending TagEncoding::Niche to include the niche_variants range and niche_start, enabling client to reproduce the const-eval calculation of tags.

cc @firefighterduck this might be of interest to you :3

[Nadrieril]

First allow me to remove the initial validity-related UB (play):

enum Foo {
    Var1,       // variant 0, tag 2
    Var2(bool), // variant 1, untagged (valid values are 0=false and 1=true)
    Var3,       // variant 2, tag 4
}

fn main() {
    let x = 3u8;
    let invalid: *const Foo = (&raw const x).cast();
    unsafe {
        let is_niched = matches!(*invalid, Foo::Var2(_));
    }
}

In my mental model, reading a niched discriminant checks if the discriminant range has any of the bitpatterns that indicate a specific variant, otherwise consider that the niched variant is active.

As you describe, Miri flags this example to be UB. I think that's wrong, and is an artifact of how rustc encodes niches. Note in particular that x = 42 is fine for Miri, 3 is the only value that causes UB here.

Fixing the issue in Charon would amount to adding extra information to Charon layouts that rhymes with "oh btw if the discriminant read sees the bitpattern 3 that's UB", which I don't see a compelling semantic reason for.

[firefighterduck]

Funnily enough, we had all that information at one point (see e.g.

charon/charon/src/ast/types.rs

Line 359 in 60fd406

tagged_variants_start: VariantId,

), but then decided to ignore all the complicated tag handling (since that's rustc internal logic and can change at anytime) and just store the current data (with a FIXME that might or might not be what you want: https://github.com/AeneasVerif/charon/blob/main/charon/src/ast/types.rs#L396).

Also, since in my experience these concepts are difficult to understand and easy to get wrong, let me make clear that we're all on the same page:

• niche_variants is a range of variant indices, even though they currently are the same as their discriminants
• The relation between the tag, aka in-memory representation of the discriminant, and the variant id is an implementation detail of rustc and can potentially change at any time
• One can always translate between tag and discriminant, but validity of discriminants still seems to be an open question

So I don't think you can get away without explicitly checking whether the tag corresponds to a niche variant or whether it is valid for the untagged variant (for which you don't need the niche_variants but just the tag type and the field types).

[Nadrieril]

Yeah, I removed that complexity on the assumption that these were implementation details that would not affect the opsem. Seems I was wrong x') (I still think Miri is wrong)

[N1ark]

oh fun thanks for the unsafe-code-guidelines link i hadn't seen that! i agree on all three points.

for which you don't need the niche_variants but just the tag type and the field types

i think this is a bit fragile, or at the very least unpractical; niches can come from "complicated types", not only a simple bool, and needing to recursively check the validity of the whole value is a lot more expensive than just having a range of "niche variants" i can check against

im going to wait for the outcome of the zulip discussion anyways; this is a corner-case and I'm happy with saying "Miri makes a choice that is non-standard so we don't care"

[N1ark]

as an outcome to that Zulip discussion, I provide another possible fix which is that we instead extend TagEncoding::Niche to have invalid_tags, which contains the list of tag values that are not valid; this corresponds to the tag computed the usual way for niched variants, but instead for the untagged variant + all uninhabited variants

so in the example above we'd have TagEncoding::Niche { untagged_variant: 1, invalid_tags: vec![3] }

[firefighterduck]

Not sure whether you'd also need this, but rustc explicitly stores the range of valid tags, in the example above 0..=4. Together with the additional information that 3 would correspond to the untagged variant, that might be sufficient to check for UB.

[N1ark]

not sure I understand what is the range of valid tags in what you linked; this shows each variant has a tag stored, but this doesn't give us an easy to use range of tags, we'd need to compute it anyways (?)

[firefighterduck]

Nope, that's not the tag per variant, but it contains a valid range of tags for all variants. That seems to be the relevant part, since Ralf also used this for a PR to Miri.

[RalfJung]

TL;DR: Charon needs more information regarding niche layouts, as otherwise we cannot reliably compute whether a tag is valid

FWIW you might be interested in how MiniRust represents enum niche layouts. Maybe that's overkill for you, but this is what you get if you want to represent "all current and future enum layout optimizations". At least I hope it'll be able to cover everything rustc does in the future. ;)
See this thesis for details; I'm also happy to answer questions.

[RalfJung]

this is a corner-case and I'm happy with saying "Miri makes a choice that is non-standard so we don't care"

Turns out that's not right; codegen actually makes this code UB on the LLVM IR level. So, any tool that wants to be faithful to the de-facto semantics of real Rust needs to make this same choice.

[Nadrieril]

See this thesis for details

Oh hell yes, I like the look of that. Let's add that to Charon.