runtimeverification / runtimeverification/mir-semantics

Support for enums

Open
#499 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

P-token P-Token M2
Dominant language
Python
Stars
52
Forks
5
PR merge metrics
No merged PRs in 30d

Description

Essentially, the Aggregate constructor of the Value sort will require an additional indicator of which variant of a represented enum is being used. The AggregateKind is available at creation and contains a VariantIdx (wrapped Int) which numbers the variants from 0 .. N (presumably in source code order).

The Rvalue::Discriminant operation retrieves an indicator of which variant is being matched (and 0 for all values that are not enums).
However, as it turned out, this indicator is not the VariantIdx included in the AggregateKind that is provided upon creation of the Value. Specifically, the discriminant of enum variants can be set to arbitrary unique usizes using

enum Thing {                     #[repr(u8)]
  A = 65,                        enum ThingWithFields {
  B, // = 66,                      X(x:isize) = 88,
  D = 68,                          Y(y: isize, z:u8) = 89,
}                                }

and the discriminant for A will be 65, whereas the AggregateKind for an A contains a VariantIdx of 0.

The SwitchInt terminator will use these Discriminant values, whereas the Downcast projection uses the VariantIdx.

Reliable information about what exactly the Discriminant should return is difficult to find, and part of its semantics is even not fully determined among experts, see this discussion.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start by reading the linked Rust discussion in issue 91095 to establish the unresolved discriminant semantics. Then trace the Aggregate constructor, Rvalue::Discriminant, SwitchInt, and Downcast concepts described here. Done means enum variants with explicit discriminants and VariantIdx-based downcasts have clearly defined, consistently supported behavior.

Written by the indexing model from the issue text.

Assessment

Tech stack
rust
Domain
compilers
Issue type
Feature
Difficulty
5/5
Estimated time
Over a week
Activity status
Stale
Clarity
Needs clarification
Newbie friendliness
25/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.