Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support unevaluated constants in specs #1332

Merged
merged 1 commit into from
Feb 28, 2023

Conversation

Aurel300
Copy link
Member

Fix #1268.

Constant encoding is a bit of a mess. There are some functions in Enconder to specifically handle scalar constants, there is encode_snapshot_constant, and there is the ConstantsEncoderInterface (@vakaras) which is a copy of the Encoder version but without using the encode_snapshot_constant

Anyway, this PR adds support for unevaluated constants (for example, a reference to a constant) in the pure function encoder. In the MIR these are represented as "promoted" items, i.e. sub-bodies of MIR bodies identified by a pair the owner DefId and a Promoted index. We can run such bodies through the pure function encoder to get a snapshot encoding of the "execution" of such a constant. Since #1304 this works for enums too, thanks to rust-lang/rust#107267.

@fpoli
Copy link
Member

fpoli commented Feb 28, 2023

I rebased. test-crates should work now.

@Aurel300 Aurel300 merged commit 8fce8f9 into viperproject:master Feb 28, 2023
@Aurel300 Aurel300 deleted the feature/constants branch February 28, 2023 19:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Unsupported constant type Ref(...)
2 participants