This repository has been archived by the owner on May 4, 2024. It is now read-only.
[move-prover] preliminary support for type reflection #451
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This commit introduces preliminary support on verifying code that
uses reflection to obtain type information at runtime.
We use a hyperthetical (and intrinsic) call
`fun extension::type_info::type_name<T>(): String`
that returns the type name of `T`.
Being a pure function, this reflection function can be called
from the spec context as well.
In handling reflection, the high-level idea is:
- if `T` is statically known when `type_name<T>` is called, replace this
call with a constant
- if `T` is unknown, full or partially, when this call is invoked,
replace the `type_name` for `T` with a fresh variable
`var #T_name: Vec int`, in particular:
- if `T` is fully unknown, `type_name<T>` will be `#T_name`
- if `T` is partially unknown (e.g., `type_name<vector<T>>`), then
the `type_name` call will be replaced as
`ConcatVec(ConcatVec("vector<", #T_name), ">")`
This instrumentation happens at the translation phase, on the way to
Boogie.
wrwg
approved these changes
Sep 7, 2022
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This commit introduces preliminary support on verifying code that uses reflection to obtain type information at runtime.
We use a hyperthetical (and intrinsic) call
fun extension::type_info::type_name<T>(): Stringthat returns the type name ofT.Being a pure function, this reflection function can be called from the spec context as well.
In handling reflection, the high-level idea is:
Tis statically known whentype_name<T>is called, replace this call with a constantTis unknown, full or partially, when this call is invoked, replace thetype_nameforTwith a fresh variablevar #T_name: Vec int, in particular:Tis fully unknown,type_name<T>will be#T_nameTis partially unknown (e.g.,type_name<vector<T>>), then thetype_namecall will be replaced asConcatVec(ConcatVec("vector<", #T_name), ">")This instrumentation happens at the translation phase, on the way to Boogie.
Motivation
Reasoning with a reflection context
Have you read the Contributing Guidelines on pull requests?
Yes
Test Plan