Commits on Dec 15, 2023

1. MIR enums …

   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 committed Dec 15, 2023
   Configuration menu

   • View commit details
   • Copy full SHA for 658f6fd
   • Browse repository at this point

   Copy the full SHA

   658f6fd View commit details

   Browse the repository at this point in the history