-
Notifications
You must be signed in to change notification settings - Fork 62
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
crux-mir-comp
: Support enums
#1990
Labels
subsystem: crucible-mir-comp
Issues related to compositional Rust verification with crucible-mir-comp or crux-mir-comp
tech debt
Issues that document or involve technical debt
type: enhancement
Issues describing an improvement to an existing feature or capability
Milestone
Comments
RyanGlScott
added
type: enhancement
Issues describing an improvement to an existing feature or capability
subsystem: crucible-mir-comp
Issues related to compositional Rust verification with crucible-mir-comp or crux-mir-comp
labels
Nov 22, 2023
RyanGlScott
added a commit
that referenced
this issue
Nov 27, 2023
This adds basic support for enums in the MIR backend. In particular: * There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue` function that constructs a value representing a specific enum variant, where the `String` indicates which variant to use. * The `mir_fresh_expanded_value` command can now create symbolic enum values. Implementation-wise, much of the complexity in this patch arises from the fact that MIR enums are represented with `VariantType`s at the Crucible level, which are a fair bit more involved than the `StructType`s used to power MIR structs. Some highlights of the implementation are: * There is now a new `EnumShape` constructor for `TypeShape`, which is in turn defined in terms of a new `VariantShape` data type that characterizes the shapes of all the fields in an enum variant. * There is a `MirSetupEnum` data type (exported by `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms of enum `MIRValue`s that one can construct. Currently, there is `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns when it creates a fresh enum value). * TODO RGS: Say something about symbolic enums * For now, there is no `crux-mir-comp` support for enums. We could conceivable add support, but there is not a pressing need to do so right now. I have opened #1990 as a reminder to do this later. This checks off one box in #1859.
Merged
RyanGlScott
added a commit
that referenced
this issue
Nov 27, 2023
This adds basic support for enums in the MIR backend. In particular: * There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue` function that constructs a value representing a specific enum variant, where the `String` indicates which variant to use. * The `mir_fresh_expanded_value` command can now create symbolic enum values. Implementation-wise, much of the complexity in this patch arises from the fact that MIR enums are represented with `VariantType`s at the Crucible level, which are a fair bit more involved than the `StructType`s used to power MIR structs. Some highlights of the implementation are: * There is now a new `EnumShape` constructor for `TypeShape`, which is in turn defined in terms of a new `VariantShape` data type that characterizes the shapes of all the fields in an enum variant. * There is a `MirSetupEnum` data type (exported by `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms of enum `MIRValue`s that one can construct. Currently, there is `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns when it creates a fresh enum value). * TODO RGS: Say something about symbolic enums * For now, there is no `crux-mir-comp` support for enums. We could conceivable add support, but there is not a pressing need to do so right now. I have opened #1990 as a reminder to do this later. This checks off one box in #1859.
RyanGlScott
added a commit
that referenced
this issue
Nov 29, 2023
This adds basic support for enums in the MIR backend. In particular: * There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue` function that constructs a value representing a specific enum variant, where the `String` indicates which variant to use. * The `mir_fresh_expanded_value` command can now create symbolic enum values. Implementation-wise, much of the complexity in this patch arises from the fact that MIR enums are represented with `VariantType`s at the Crucible level, which are a fair bit more involved than the `StructType`s used to power MIR structs. Some highlights of the implementation are: * There is now a new `EnumShape` constructor for `TypeShape`, which is in turn defined in terms of a new `VariantShape` data type that characterizes the shapes of all the fields in an enum variant. * There is a `MirSetupEnum` data type (exported by `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms of enum `MIRValue`s that one can construct. Currently, there is `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns when it creates a fresh enum value). * TODO RGS: Say something about symbolic enums * For now, there is no `crux-mir-comp` support for enums. We could conceivable add support, but there is not a pressing need to do so right now. I have opened #1990 as a reminder to do this later. This checks off one box in #1859.
RyanGlScott
added a commit
that referenced
this issue
Dec 6, 2023
This adds basic support for enums in the MIR backend. In particular: * There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue` function that constructs a value representing a specific enum variant, where the `String` indicates which variant to use. * The `mir_fresh_expanded_value` command can now create symbolic enum values. Implementation-wise, much of the complexity in this patch arises from the fact that MIR enums are represented with `VariantType`s at the Crucible level, which are a fair bit more involved than the `StructType`s used to power MIR structs. Some highlights of the implementation are: * There is now a new `EnumShape` constructor for `TypeShape`, which is in turn defined in terms of a new `VariantShape` data type that characterizes the shapes of all the fields in an enum variant. * There is a `MirSetupEnum` data type (exported by `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms of enum `MIRValue`s that one can construct. Currently, there is `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns when it creates a fresh enum value). * The implementation of symbolic enum values in particular is somewhat complicated. I have written `Note [Symbolic enums]` to go over the general approach and highlight some potential pitfalls in implementing them. * For now, there is no `crux-mir-comp` support for enums. We could conceivable add support, but there is not a pressing need to do so right now. I have opened #1990 as a reminder to do this later. This checks off one box in #1859.
RyanGlScott
added a commit
that referenced
this issue
Dec 15, 2023
This adds basic support for enums in the MIR backend. In particular: * There is now a `mir_enum_value : MIRAdt -> String -> [MIRValue] -> MIRValue` function that constructs a value representing a specific enum variant, where the `String` indicates which variant to use. * The `mir_fresh_expanded_value` command can now create symbolic enum values. Implementation-wise, much of the complexity in this patch arises from the fact that MIR enums are represented with `VariantType`s at the Crucible level, which are a fair bit more involved than the `StructType`s used to power MIR structs. Some highlights of the implementation are: * There is now a new `EnumShape` constructor for `TypeShape`, which is in turn defined in terms of a new `VariantShape` data type that characterizes the shapes of all the fields in an enum variant. * There is a `MirSetupEnum` data type (exported by `SAWScript.Crucible.MIR.MethodSpecIR`) which categorizes the different forms of enum `MIRValue`s that one can construct. Currently, there is `MirSetupEnumVariant` (which is what `mir_enum_value` returns) and `MirSetupEnumSymbolic` (which is what `mir_fresh_expanded_value` returns when it creates a fresh enum value). * The implementation of symbolic enum values in particular is somewhat complicated. I have written `Note [Symbolic enums]` to go over the general approach and highlight some potential pitfalls in implementing them. * For now, there is no `crux-mir-comp` support for enums. We could conceivable add support, but there is not a pressing need to do so right now. I have opened #1990 as a reminder to do this later. This checks off one box in #1859.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
subsystem: crucible-mir-comp
Issues related to compositional Rust verification with crucible-mir-comp or crux-mir-comp
tech debt
Issues that document or involve technical debt
type: enhancement
Issues describing an improvement to an existing feature or capability
Currently,
crux-mir-comp
will simply crash if you write a specification involving enums, as seen in this variant of thespec_struct.rs
test case:This ticket exists as a reminder to implement enum support.
The text was updated successfully, but these errors were encountered: