MIR enums #1991

RyanGlScott · 2023-11-27T18:49:59Z

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 VariantTypes at the Crucible level, which are a fair bit more involved than the StructTypes 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 MIRValues 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 crux-mir-comp: Support enums #1990 as a reminder to do this later.

This checks off one box in #1859.

doc/manual/manual.md

RyanGlScott · 2023-12-06T19:24:52Z

crucible-mir-comp/src/Mir/Compositional/Builder.hs

@@ -742,6 +751,8 @@ regToSetup bak p eval shp rv = go shp rv
        refSV <- go refShp refRV
        lenSV <- go lenShp lenRV
        pure $ MS.SetupSlice $ MirSetupSliceRaw refSV lenSV
+    go (EnumShape _ _ _ _ _) _ =
+      error "Enums not currently supported in overrides"


See #1990 for the task of supporting enums in {crucible,crux}-mir-comp.

RyanGlScott · 2023-12-06T19:26:04Z

src/SAWScript/Crucible/MIR/TypeShape.hs

+    -- | A shape for an enum type. Like 'StructShape', this is indexed by
+    -- 'AnyType', so code that matches on 'EnumShape' may need to further match
+    -- on the 'VariantShape's in order to bring additional type information into
+    -- scope.
+    EnumShape :: M.Ty
+              -- ^ The overall enum type.
+              -> [[M.Ty]]
+              -- ^ The field types in each of the enum's variants.
+              -> Assignment VariantShape ctx
+              -- ^ The shapes of the enum type's variants.
+              -> M.Ty
+              -- ^ The discriminant type.
+              -> TypeShape discrTp
+              -- ^ The shape of the discriminant type.
+              -> TypeShape AnyType


This is a new TypeShape constructor that is used extensively in this patch...

RyanGlScott · 2023-12-06T19:26:17Z

src/SAWScript/Crucible/MIR/TypeShape.hs

+-- | The 'TypeShape' of an enum variant, which consists of some number of field
+-- types.
+--
+-- This is indexed by a 'StructType', but that is simply an artifact of the
+-- particular way that @crucible-mir@ encodes enum types. Despite the use of
+-- 'StructType' as a type index, we only use 'VariantShape' for enums, not
+-- structs.
+data VariantShape (tp :: CrucibleType) where
+    VariantShape :: Assignment FieldShape ctx
+                 -- ^ The shapes of the variant's field types.
+                 -> VariantShape (StructType ctx)


...as well as the related VariantShape data type.

RyanGlScott · 2023-12-06T19:27:06Z

src/SAWScript/Crucible/MIR/Setup/Value.hs

+-- | A enum-related MIR 'SetupValue'.
+data MirSetupEnum where


This data type classifies the two ways that one can create an enum value (either via mir_enum_value or mir_fresh_expanded_value).

RyanGlScott · 2023-12-06T19:27:25Z

src/SAWScript/Crucible/MIR/Setup/Value.hs

@@ -157,3 +229,137 @@ data MirSetupSlice
 makeLenses ''MIRCrucibleContext
 makeLenses ''MirAllocSpec
 makeLenses ''MirPointer
+
+{-
+Note [Symbolic enums]


A large piece of documentation that I wrote about the approach to handling symbolic enum values.

RyanGlScott · 2023-12-06T19:28:31Z

src/SAWScript/Crucible/MIR/ResolveSetupValue.hs

+                [ "Expected struct type, received union:"
+                , show nm
+                ]
+    MS.SetupEnum enum_ ->


This implements turning a SetupEnum into a value that Crucible can reason about. (It's quite involved, sadly—sorry.)

RyanGlScott · 2023-12-06T19:29:02Z

src/SAWScript/Crucible/MIR/Override.hs

+    -- In order to match an enum value, we first check to see if the expected
+    -- value is a specific enum variant or a symbolic enum...
+    (MIRVal (EnumShape _ _ variantShps _ discrShp)
+            (Crucible.AnyValue
+              (Mir.RustEnumRepr discrTpr variantCtx)
+              (Ctx.Empty
+                Ctx.:> Crucible.RV actualDiscr
+                Ctx.:> Crucible.RV variantAssn)),
+     _,
+     MS.SetupEnum enum_)


This implements matching one enum value against another.

RyanGlScott · 2023-12-06T19:29:47Z

src/SAWScript/Crucible/MIR/Builtins.hs

+    -- Create a fresh symbolic enum value, as described in
+    -- Note [Symboliic enums] in SAWScript.Crucible.MIR.Setup.Value.
+    goEnum ::
+      forall discrShp variantCtx.
+      Text ->
+      Mir.Adt ->
+      TypeShape discrShp ->
+      Ctx.Assignment VariantShape variantCtx ->
+      CrucibleSetup MIR MirSetupEnum


This generates all of the symbolic variables used in a symbolic enum value.

RyanGlScott · 2023-12-06T19:30:30Z

doc/manual/manual.md

+constructing a struct value), and `mir_enum_value` (for constructing an enum
+value) commands in turn take a `MIRAdt` as an argument.
+
+#### Enums


Documentation about enums.

spernsteiner

Looks good - just a few typos and minor comments

doc/manual/manual.md

src/SAWScript/Crucible/MIR/Builtins.hs

src/SAWScript/Crucible/MIR/Override.hs

src/SAWScript/Crucible/MIR/ResolveSetupValue.hs

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 force-pushed the T1859-mir_enums branch from 35dfc90 to d44eae1 Compare November 27, 2023 20:48

qsctr reviewed Nov 29, 2023

View reviewed changes

doc/manual/manual.md Outdated Show resolved Hide resolved

RyanGlScott force-pushed the T1859-mir_enums branch from d44eae1 to 14c7213 Compare November 29, 2023 12:55

RyanGlScott force-pushed the T1859-mir_enums branch from 14c7213 to b77ee63 Compare December 6, 2023 19:22

RyanGlScott marked this pull request as ready for review December 6, 2023 19:23

RyanGlScott commented Dec 6, 2023

View reviewed changes

RyanGlScott requested review from qsctr and spernsteiner December 6, 2023 19:30

RyanGlScott mentioned this pull request Dec 6, 2023

Start a SAW Rust verification tutorial #1939

Merged

spernsteiner approved these changes Dec 14, 2023

View reviewed changes

RyanGlScott force-pushed the T1859-mir_enums branch from b77ee63 to 658f6fd Compare December 15, 2023 12:15

RyanGlScott added the ready-to-merge If at least one person approves this PR, automatically merge it when CI finishes successfully. label Dec 15, 2023

mergify bot merged commit 63093c3 into master Dec 15, 2023
40 checks passed

mergify bot deleted the T1859-mir_enums branch December 15, 2023 13:09

RyanGlScott mentioned this pull request Dec 15, 2023

Support Rust verification in SAW via crucible-mir #1859

Closed

29 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

MIR enums #1991

MIR enums #1991

RyanGlScott commented Nov 27, 2023 •

edited

RyanGlScott Dec 6, 2023

RyanGlScott Dec 6, 2023

RyanGlScott Dec 6, 2023

RyanGlScott Dec 6, 2023

RyanGlScott Dec 6, 2023

RyanGlScott Dec 6, 2023

RyanGlScott Dec 6, 2023

RyanGlScott Dec 6, 2023

RyanGlScott Dec 6, 2023

spernsteiner left a comment

		-- \| A enum-related MIR 'SetupValue'.
		data MirSetupEnum where

MIR enums #1991

MIR enums #1991

Conversation

RyanGlScott commented Nov 27, 2023 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

spernsteiner left a comment

Choose a reason for hiding this comment

RyanGlScott commented Nov 27, 2023 •

edited