diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index ce1ceb89a2..6040fcddb6 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -648,7 +648,7 @@ substMethodSpec sc sm ms = do goSetupEnum (MirSetupEnumVariant adt variant discr variantIdx svs) = MirSetupEnumVariant adt variant discr variantIdx <$> mapM goSetupValue svs - goSetupEnum sv@(MirSetupEnumSymbolic _) = + goSetupEnum sv@(MirSetupEnumSymbolic _ _ _) = return sv goSetupSlice (MirSetupSliceRaw ref len) = @@ -749,7 +749,7 @@ 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 _ _ _ _) _ = + go (EnumShape _ _ _ _ _) _ = error "Enums not currently supported in overrides" go (FnPtrShape _ _ _) _ = error "Function pointers not currently supported in overrides" diff --git a/crucible-mir-comp/src/Mir/Compositional/Clobber.hs b/crucible-mir-comp/src/Mir/Compositional/Clobber.hs index 64301bdf93..e2288de83c 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Clobber.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Clobber.hs @@ -62,7 +62,7 @@ clobberSymbolic sym loc nameStr shp rv = go shp rv ", but got Any wrapping " ++ show tpr where shpTpr = StructRepr $ fmapFC fieldShapeType flds go (TransparentShape _ shp) rv = go shp rv - go (EnumShape _ _ _ _) _rv = + go (EnumShape _ _ _ _ _) _rv = error "Enums not currently supported in overrides" go (FnPtrShape _ _ _) _rv = error "Function pointers not currently supported in overrides" @@ -122,7 +122,7 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv ref' <- go refShp ref len' <- go lenShp len pure $ Ctx.Empty Ctx.:> RV ref' Ctx.:> RV len' - go (EnumShape _ _ _ _) _rv = + go (EnumShape _ _ _ _ _) _rv = error "Enums not currently supported in overrides" go (FnPtrShape _ _ _) _rv = error "Function pointers not currently supported in overrides" diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index a749268ec1..e83d18eea6 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -544,7 +544,7 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv refRV <- go refShp refSV lenRV <- go lenShp lenSV pure $ Ctx.Empty Ctx.:> RV refRV Ctx.:> RV lenRV - go (EnumShape _ _ _ _) _ = + go (EnumShape _ _ _ _ _) _ = error "Enums not currently supported in overrides" go (FnPtrShape _ _ _) _ = error "Function pointers not currently supported in overrides" diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 37ebe45463..df09f9b4dc 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -337,7 +337,7 @@ munge sym shp rv = do AnyValue tpr <$> goFields flds rvs | otherwise = error $ "munge: StructShape AnyValue with NYI TypeRepr " ++ show tpr go (TransparentShape _ shp) rv = go shp rv - go (EnumShape _ _ _ _) _ = + go (EnumShape _ _ _ _ _) _ = error "Enums not currently supported in overrides" go (FnPtrShape _ _ _) _ = error "Function pointers not currently supported in overrides" diff --git a/intTests/test_mir_fresh_expanded_value_enum/Makefile b/intTests/test_mir_fresh_expanded_value_enum/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_fresh_expanded_value_enum/Makefile @@ -0,0 +1,13 @@ +all: test.linked-mir.json + +test.linked-mir.json: test.rs + saw-rustc $< + $(MAKE) remove-unused-build-artifacts + +.PHONY: remove-unused-build-artifacts +remove-unused-build-artifacts: + rm -f test libtest.mir libtest.rlib + +.PHONY: clean +clean: remove-unused-build-artifacts + rm -f test.linked-mir.json diff --git a/intTests/test_mir_fresh_expanded_value_enum/test.linked-mir.json b/intTests/test_mir_fresh_expanded_value_enum/test.linked-mir.json new file mode 100644 index 0000000000..7b202fff9e --- /dev/null +++ b/intTests/test_mir_fresh_expanded_value_enum/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"}},"pos":"test.rs:2:11: 2:12","rhs":{"kind":"Discriminant","ty":"ty::isize","val":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"}},"kind":"Move"},"discr_span":"test.rs:3:9: 3:16","kind":"SwitchInt","pos":"test.rs:2:5: 2:12","switch_ty":"ty::isize","targets":["bb1","bb3","bb2"],"values":["0","1"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:4:17: 4:19","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"27"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Goto","pos":"test.rs:4:17: 4:19","target":"bb4"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Unreachable","pos":"test.rs:2:11: 2:12"}},"blockid":"bb2"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:3:14: 3:15","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:3:20: 3:21","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"kind":"Goto","pos":"test.rs:3:20: 3:21","target":"bb4"}},"blockid":"bb3"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:6:2: 6:2"}},"blockid":"bb4"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}]},"name":"test/b38ac280::f","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:13:7: 13:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":true,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Tuple::e93222e871854c41"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::779a68152b60006a"},"kind":"Constant"},"kind":"Call","pos":"test.rs:13:5: 13:9"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:14:2: 14:2"}},"blockid":"bb1"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":true,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"test/b38ac280::gg","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:9:7: 9:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::946bbc4c46985e3c"},"kind":"Constant"},"kind":"Call","pos":"test.rs:9:5: 9:9"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:10:2: 10:2"}},"blockid":"bb1"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"test/b38ac280::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::u32"],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::u32"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/b38ac280::f","kind":"Item","substs":[]},"name":"test/b38ac280::f"},{"inst":{"def_id":"test/b38ac280::gg","kind":"Item","substs":[]},"name":"test/b38ac280::gg"},{"inst":{"def_id":"test/b38ac280::g","kind":"Item","substs":[]},"name":"test/b38ac280::g"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Adt::3fa7c2d95c7fce06","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::u32"]}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::FnDef::779a68152b60006a","ty":{"defid":"test/b38ac280::g","kind":"FnDef"}},{"name":"ty::FnDef::946bbc4c46985e3c","ty":{"defid":"test/b38ac280::f","kind":"FnDef"}}],"roots":["test/b38ac280::f","test/b38ac280::g","test/b38ac280::gg"]} \ No newline at end of file diff --git a/intTests/test_mir_fresh_expanded_value_enum/test.rs b/intTests/test_mir_fresh_expanded_value_enum/test.rs new file mode 100644 index 0000000000..86f7563545 --- /dev/null +++ b/intTests/test_mir_fresh_expanded_value_enum/test.rs @@ -0,0 +1,14 @@ +pub fn f(x: Option) -> u32 { + match x { + Some(x) => x, + None => 27, + } +} + +pub fn g(x: Option) { + f(x); +} + +pub fn gg(x: Option) { + g(x); +} diff --git a/intTests/test_mir_fresh_expanded_value_enum/test.saw b/intTests/test_mir_fresh_expanded_value_enum/test.saw new file mode 100644 index 0000000000..276161f0aa --- /dev/null +++ b/intTests/test_mir_fresh_expanded_value_enum/test.saw @@ -0,0 +1,44 @@ +enable_experimental; + +m <- mir_load_module "test.linked-mir.json"; + +let option_u32_adt = mir_find_adt m "core::option::Option" [mir_u32]; + +let f_none_spec = do { + let x = mir_enum_value option_u32_adt "None" []; + + mir_execute_func [x]; + + mir_return (mir_term {{ 27 : [32] }}); +}; + +let f_some_spec = do { + ret <- mir_fresh_var "ret" mir_u32; + let x = mir_enum_value option_u32_adt "Some" [mir_term ret]; + + mir_execute_func [x]; + + mir_return (mir_term ret); +}; + +let g_spec = do { + x <- mir_fresh_expanded_value "x" (mir_adt option_u32_adt); + + mir_execute_func [x]; +}; + +let gg_spec = do { + xx <- mir_fresh_expanded_value "xx" (mir_adt option_u32_adt); + + mir_execute_func [xx]; +}; + +f_none_ov <- mir_verify m "test::f" [] false f_none_spec z3; +f_some_ov <- mir_verify m "test::f" [] false f_some_spec z3; + +mir_verify m "test::g" [] false g_spec z3; +g_ov <- mir_verify m "test::g" [f_none_ov, f_some_ov] false g_spec z3; + +mir_verify m "test::gg" [] false gg_spec z3; +// TODO RGS: Investigate why this doesn't work +// mir_verify m "test::gg" [g_ov] false gg_spec z3; diff --git a/intTests/test_mir_fresh_expanded_value_enum/test.sh b/intTests/test_mir_fresh_expanded_value_enum/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_fresh_expanded_value_enum/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index 6af330a821..2f8aee057f 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -267,7 +267,7 @@ ppSetupValue setupval = case setupval of ppMirSetupEnum :: MirSetupEnum -> PP.Doc ann ppMirSetupEnum (MirSetupEnumVariant _defId variantName _discr _varIdx fields) = PP.pretty variantName PP.<+> ppSetupStructDefault fields - ppMirSetupEnum (MirSetupEnumSymbolic _defId) = + ppMirSetupEnum (MirSetupEnumSymbolic _defId _discr _variants) = PP.pretty "" ppMirSetupSlice :: MirSetupSlice -> PP.Doc ann diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index d04619a27c..fc12476977 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -58,12 +58,13 @@ module SAWScript.Crucible.MIR.Builtins ) where import Control.Lens -import Control.Monad (foldM, forM, forM_, unless, when) +import Control.Monad (foldM, forM, forM_, unless, when, zipWithM) import qualified Control.Monad.Catch as X import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Reader (runReaderT) import Control.Monad.State (MonadState(..), StateT(..), execStateT, gets) import Control.Monad.Trans.Class (MonadTrans(..)) +import qualified Data.BitVector.Sized as BV import qualified Data.ByteString.Lazy as BSL import Data.Foldable (for_) import qualified Data.Foldable.WithIndex as FWI @@ -78,6 +79,7 @@ import qualified Data.Parameterized.Context as Ctx import qualified Data.Parameterized.Map as MapF import Data.Parameterized.NatRepr (knownNat, natValue) import Data.Parameterized.Some (Some(..)) +import qualified Data.Parameterized.TraversableFC as FC import qualified Data.Parameterized.TraversableFC.WithIndex as FCI import qualified Data.Set as Set import qualified Data.Text as Text @@ -306,7 +308,7 @@ constructExpandedSetupValue cc sc = go Mir.TyArray _ n -> do elems <- traverse - (\i -> go (pfx <> "." <> Text.pack (show i)) elemShp) + (\i -> go (pfx <> "_" <> Text.pack (show i)) elemShp) [0..n-1] pure $ MS.SetupArray elemTy elems _ -> @@ -332,19 +334,20 @@ constructExpandedSetupValue cc sc = go adt_not_found_panic "StructShape" adtName _ -> non_adt_type_panic "StructShape" ty - EnumShape ty _ _ _ -> + EnumShape ty _ variantShps _ discrShp -> case ty of Mir.TyAdt adtName _ _ -> case col ^. Mir.adts . at adtName of Just adt@(Mir.Adt _ kind _ _ _ _ _) -> case kind of Mir.Enum _ -> - pure $ MS.SetupEnum $ MirSetupEnumSymbolic adt - _ -> + MS.SetupEnum <$> goEnum pfx adt discrShp variantShps + Mir.Struct -> panic "constructExpandedSetupValue" - [ "Expected enum, encountered " ++ - show kind - ] + ["Expected enum, encountered struct"] + Mir.Union -> + panic "constructExpandedSetupValue" + ["Expected enum, encountered union"] Nothing -> adt_not_found_panic "EnumShape" adtName _ -> @@ -353,13 +356,24 @@ constructExpandedSetupValue cc sc = go case ty of Mir.TyAdt adtName _ _ -> do case col ^. Mir.adts . at adtName of - Just adt@(Mir.Adt _ kind _ _ _ _ _) -> + Just adt@(Mir.Adt adtNm kind variants _ _ _ _) -> case kind of Mir.Struct -> do val <- go pfx shp' pure $ MS.SetupStruct adt [val] - Mir.Enum{} -> - pure $ MS.SetupEnum $ MirSetupEnumSymbolic adt + Mir.Enum{} + | [variant] <- variants + -> do val <- go pfx shp' + let discr = getEnumVariantDiscr variant + pure $ MS.SetupEnum + $ MirSetupEnumVariant adt variant discr 0 [val] + + | otherwise + -> panic "constructExpandedSetupValue" + [ "`repr(transparent)` enum that doesn't have exactly one variant" + , "Enum: " ++ show adtNm + , "Number of variants: " ++ show (length variants) + ] Mir.Union -> panic "constructExpandedSetupValue" [ "Unexpected `repr(transparent)` union:" @@ -376,6 +390,50 @@ constructExpandedSetupValue cc sc = go FnPtrShape ty _ _ -> X.throwM $ MIRFreshExpandedValueUnsupportedType ty + goEnum :: + forall discrShp variantCtx. + Text -> + Mir.Adt -> + TypeShape discrShp -> + Ctx.Assignment VariantShape variantCtx -> + CrucibleSetup MIR MirSetupEnum + goEnum pfx adt@(Mir.Adt _ _ variants _ _ _ _) discrShp variantShps = + mccWithBackend cc $ \bak -> + do let sym = backendGetSym bak + + IsBVShape _ discrW <- pure $ testDiscriminantIsBV discrShp + let discrSym = W4.safeSymbol (Text.unpack pfx ++ "_discr") + discrVal <- liftIO $ W4.freshConstant sym discrSym (W4.BaseBVRepr discrW) + + -- TODO RGS: Document this carefully, explain why we need it + possibleDiscrVals <- liftIO $ + traverse (W4.bvLit sym discrW . BV.mkBV discrW) + (map getEnumVariantDiscr variants) + possibleDiscrPred <- liftIO $ + foldM + (\z possibleDiscrVal -> do + p <- W4.bvEq sym discrVal possibleDiscrVal + W4.orPred sym p z) + (W4.falsePred sym) + possibleDiscrVals + loc <- SS.toW4Loc "mir_fresh_expanded_value" <$> lift (lift getPosition) + liftIO $ Crucible.addAssumption bak $ + Crucible.GenericAssumption loc "TODO RGS" possibleDiscrPred + + let variantAssns :: [Some (Ctx.Assignment FieldShape)] + variantAssns = + FC.toListFC + (\(VariantShape fldShps) -> Some fldShps) + variantShps + variantVals <- + zipWithM + (\variant (Some fldShps) -> + let variantPfx = pfx <> "_" <> getEnumVariantShortName variant in + goFlds variantPfx fldShps) + variants + variantAssns + pure $ MirSetupEnumSymbolic adt discrVal variantVals + goFlds :: forall ctx. Text -> Ctx.Assignment FieldShape ctx -> @@ -383,7 +441,7 @@ constructExpandedSetupValue cc sc = go goFlds pfx fldShps = sequenceA $ FCI.itoListFC (\idx fldShp -> - let pfx' = pfx <> "." <> Text.pack (show idx) in + let pfx' = pfx <> "_" <> Text.pack (show idx) in case fldShp of ReqField shp' -> go pfx' shp' OptField shp' -> go pfx' shp') @@ -632,19 +690,12 @@ mir_enum_value adt variantNm vs = case adt of Mir.Adt adtNm (Mir.Enum _) variants _ _ _ _ -> do (variantIdx, variant) <- - case FWI.ifind (\_ v -> variantDefIdMatches (v ^. Mir.vname)) variants of + case FWI.ifind (\_ v -> variantDefIdMatches v) variants of Just iv -> pure iv Nothing -> X.throwM $ MIREnumValueVariantNotFound adtNm variantNm - discr <- - case variant ^. Mir.discrval of - Just discr -> pure discr - Nothing -> - panic "mir_enum_value" - [ "discrval not set for variant:" - , show (variant ^. Mir.vname) - ] + let discr = getEnumVariantDiscr variant pure $ MS.SetupEnum $ MirSetupEnumVariant adt variant discr variantIdx vs Mir.Adt adtNm Mir.Struct _ _ _ _ _ -> X.throwM $ MIREnumValueNonEnum adtNm "struct" @@ -655,17 +706,13 @@ mir_enum_value adt variantNm vs = variantNmText = Text.pack variantNm -- Check if the user-supplied String argument matches the name of the given - -- variant's DefId. For instance, the variant might be named + -- variant's DefId. For instance, the variant DefId might be named -- @core::option[0]::Option[0]::Some[0]@, but the user will simply write - -- @Some@, so this function decomposes the DefId to retrieve the @Some@ - -- portion. - variantDefIdMatches :: Mir.DefId -> Bool - variantDefIdMatches variantDefId - | Just (_, (variantNmText', _idx)) <- List.unsnoc (variantDefId ^. Mir.didPath) - = variantNmText == variantNmText' - - | otherwise - = False + -- @Some@, so we must strip off the other parts of the DefId before checking + -- if the two are the same. + variantDefIdMatches :: Mir.Variant -> Bool + variantDefIdMatches variant = + getEnumVariantShortName variant == variantNmText ----- -- MIR slices @@ -1233,6 +1280,20 @@ findFn rm nm = do Just x -> return x Nothing -> fail $ "Couldn't find MIR function named: " ++ nm +-- | Given a full enum variant identifier (e.g., +-- @core::option[0]::Option[0]::Some[0]@, retrieve the part of the identifier +-- that corresponds to the variant's shorthand name (e.g., @Some@). +getEnumVariantShortName :: Mir.Variant -> Text +getEnumVariantShortName variant + | Just (_, (variantNm, _)) <- List.unsnoc (variant ^. Mir.vname . Mir.didPath) + = variantNm + + | otherwise + = panic "getEnumVariantShortName" + [ "Malformed enum variant identifier" + , show $ variant ^. Mir.vname + ] + getMIRCrucibleContext :: CrucibleSetup MIR MIRCrucibleContext getMIRCrucibleContext = view Setup.csCrucibleContext <$> get diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index a30c213b5f..9b75463a43 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -7,6 +7,7 @@ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} @@ -908,8 +909,9 @@ instantiateSetupValue sc s v = instantiateSetupEnum (MirSetupEnumVariant adt variant discr variantIdx vs) = MirSetupEnumVariant adt variant discr variantIdx <$> mapM (instantiateSetupValue sc s) vs - instantiateSetupEnum v'@(MirSetupEnumSymbolic _adt) = - return v' + instantiateSetupEnum (MirSetupEnumSymbolic adt discr variants) = + MirSetupEnumSymbolic adt discr <$> + mapM (mapM (instantiateSetupValue sc s)) variants instantiateSetupSlice :: MirSetupSlice -> IO MirSetupSlice instantiateSetupSlice (MirSetupSliceRaw ref len) = @@ -1082,34 +1084,23 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = Mir.TyAdt _ _ _, MS.SetupStruct adt zs) | let xsTpr = Crucible.StructRepr (FC.fmapFC fieldShapeType xsFldShps) - , Just Refl <- W4.testEquality tpr xsTpr -> - case adt of - Mir.Adt nm Mir.Struct variants _ _ _ _ -> do - variant <- - case variants of - [variant] -> - pure variant - _ -> - panic "matchArg" - [ "Encountered struct Adt with " ++ - show (length variants) ++ - " variants:" - , show nm - ] - let ys = variant ^.. Mir.vfields . each . Mir.fty - matchFields sym xsFldShps xs ys zs - Mir.Adt nm (Mir.Enum _) _ _ _ _ _ -> - panic "matchArg" - [ "Expected struct type, received enum:" - , show nm - ] - Mir.Adt nm Mir.Union _ _ _ _ _ -> - panic "matchArg" - [ "Expected struct type, received union:" - , show nm - ] - - (MIRVal (EnumShape _ variantShps _ discrShp) + , Just Refl <- W4.testEquality tpr xsTpr -> do + let variants = adt ^. Mir.adtvariants + variant <- + case variants of + [variant] -> + pure variant + _ -> + panic "matchArg" + [ "Encountered struct Adt with " ++ + show (length variants) ++ + " variants:" + , show $ adt ^. Mir.adtname + ] + let ys = variant ^.. Mir.vfields . each . Mir.fty + matchFields sym xsFldShps xs ys zs + + (MIRVal (EnumShape _ _ variantShps _ discrShp) (Crucible.AnyValue (Mir.RustEnumRepr discrTpr variantCtx) (Ctx.Empty @@ -1124,7 +1115,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = MirSetupEnumVariant adt variant discr variantIdxInt zs -> do Some variantIdx <- pure $ variantIntIndex (adt ^. Mir.adtname) variantIdxInt (Ctx.size variantAssn) - VariantShape _ xsFldShps <- pure $ variantShps Ctx.! variantIdx + VariantShape xsFldShps <- pure $ variantShps Ctx.! variantIdx let Crucible.VB expectedVariant = variantAssn Ctx.! variantIdx let ys = variant ^.. Mir.vfields . each . Mir.fty @@ -1136,18 +1127,45 @@ matchArg opts sc cc cs prepost md actual expectedTy expected = W4.bvEq sym expectedDiscr actualDiscr addAssert discrEq md =<< notEq - -- Ensure that the variant is defined, i.e., that the predicate in - -- the underlying PartialExpr holds. - (xsPred, xs) <- - case expectedVariant of - W4.PE xsPred xs -> pure (xsPred, xs) - W4.Unassigned -> fail_ - addAssert xsPred md =<< notEq + case expectedVariant of + W4.PE xsPred xs -> do + -- Ensure that the variant is defined, i.e., that the predicate + -- in the underlying PartialExpr holds. + addAssert xsPred md =<< notEq + -- Finally, ensure that the fields match point-wise. + matchFields sym xsFldShps xs ys zs + W4.Unassigned -> + pure () + + MirSetupEnumSymbolic adt expectedDiscr variantFlds -> do + -- Ensure that the discriminant values match. + IsBVShape _ actualDiscrW <- pure $ testDiscriminantIsBV discrShp + Refl <- + case W4.testEquality (W4.bvWidth expectedDiscr) actualDiscrW of + Just r -> pure r + Nothing -> fail_ + discrEq <- liftIO $ + W4.bvEq sym expectedDiscr actualDiscr + addAssert discrEq md =<< notEq - -- Finally, ensure that the fields match point-wise. - matchFields sym xsFldShps xs ys zs - MirSetupEnumSymbolic{} -> - error "TODO RGS: Symbolic enums" + -- Ensure that each variant branch matches. + -- TODO RGS: Type applications kinda sus + sequence_ @_ @_ @() + [ case xPE of + W4.PE xsPred xs -> do + -- Ensure that the variant is defined, i.e., that the + -- predicate in the underlying PartialExpr holds. + addAssert xsPred md =<< notEq + -- Finally, ensure that the fields match point-wise. + matchFields sym xsFldShps xs ys zs + W4.Unassigned -> + pure () + | (Some (Functor.Pair (VariantShape xsFldShps) (Crucible.VB xPE)), ys, zs) <- + zip3 + (FC.toListFC Some (Ctx.zipWith Functor.Pair variantShps variantAssn)) + (map (\v -> v ^.. Mir.vfields . each . Mir.fty) (adt ^. Mir.adtvariants)) + variantFlds + ] -- match the fields of a tuple point-wise (MIRVal (TupleShape _ _ xsFldShps) xs, Mir.TyTuple ys, MS.SetupTuple () zs) -> @@ -1330,8 +1348,8 @@ matchPointsTos opts sc cc spec prepost = go False [] setupEnum :: MirSetupEnum -> Set AllocIndex setupEnum (MirSetupEnumVariant _ _ _ _ xs) = foldMap setupVars xs - setupEnum (MirSetupEnumSymbolic _) = - Set.empty + setupEnum (MirSetupEnumSymbolic _ _ variants) = + foldMap (foldMap setupVars) variants -- Compute the set of variable identifiers in a 'MirSetupSlice' setupSlice :: MirSetupSlice -> Set AllocIndex diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index ac34c083d8..df8fc1343a 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs @@ -35,6 +35,7 @@ module SAWScript.Crucible.MIR.ResolveSetupValue , findStaticVar , staticRefMux -- * Enum discriminants + , getEnumVariantDiscr , testDiscriminantIsBV , variantIntIndex -- * Types of errors @@ -142,7 +143,7 @@ ppMIRVal sym (MIRVal shp val) = | otherwise -> error "Malformed MIRVal struct" - EnumShape _ variantShps _ _ + EnumShape _ _ variantShps _ _ | AnyValue (Mir.RustEnumRepr _ variantCtx) (Ctx.Empty Ctx.:> RV _ Ctx.:> RV variants) <- val , Just Refl <- W4.testEquality (FC.fmapFC variantShapeType variantShps) variantCtx @@ -178,7 +179,7 @@ ppMIRVal sym (MIRVal shp val) = (Ctx.Assignment (RegValue' Sym)))) firstConcreteVariant variantShapes variantBranches = List.firstJust - (\(Some (Functor.Pair (VariantShape _ fldShps) (VB branch))) -> + (\(Some (Functor.Pair (VariantShape fldShps) (VB branch))) -> case branch of W4.PE fldPred fldVals | W4.asConstantPred fldPred == Just True @@ -292,7 +293,7 @@ typeOfSetupValue mcc env nameEnv val = case enum_ of MirSetupEnumVariant adt _ _ _ _ -> pure $ mirAdtToTy adt - MirSetupEnumSymbolic adt -> + MirSetupEnumSymbolic adt _ _ -> pure $ mirAdtToTy adt MS.SetupTuple () vals -> do tys <- traverse (typeOfSetupValue mcc env nameEnv) vals @@ -385,8 +386,8 @@ resolveSetupVal mcc env tyenv nameEnv val = checkFields nm "Struct" "struct fields" expectedFlds actualFldTys -- Finally, construct a MIRVal of the appropriate shape. - Some fldAssn <- pure $ variantFieldsToAssn sym flds' - let (fldShpAssn, valAssn) = Ctx.unzip fldAssn + Some (Functor.Pair fldShpAssn valAssn) <- + pure $ variantFieldsToAssns sym flds' let structShp = StructShape (mirAdtToTy adt) actualFldTys fldShpAssn let structTpr = StructRepr (FC.fmapFC fieldShapeType fldShpAssn) pure $ MIRVal structShp (AnyValue structTpr valAssn) @@ -430,9 +431,11 @@ resolveSetupVal mcc env tyenv nameEnv val = -- Construct an EnumShape and RustEnumRepr. This requires mapping -- over /all/ variants, not just the particular variant that we -- are building. - Some variantShps <- + let variantTys = + map (\v -> v ^.. Mir.vfields . each . Mir.fty) variants + Some expectedVariantShps <- pure $ Ctx.fromList $ - map (\variantTys -> + map (\fldTys -> case Ctx.fromList $ map (\ty -> @@ -441,11 +444,15 @@ resolveSetupVal mcc env tyenv nameEnv val = if Mir.canInitialize col ty then Some $ ReqField shp else Some $ OptField shp) - variantTys of - Some fldAssn -> Some $ VariantShape variantTys fldAssn) - (map (\v -> v ^.. Mir.vfields . each . Mir.fty) variants) - let enumShp = EnumShape (mirAdtToTy adt) variantShps discrTp discrShp - let variantTprs = FC.fmapFC variantShapeType variantShps + fldTys of + Some fldAssn -> Some $ VariantShape fldAssn) + variantTys + let enumShp = + EnumShape + (mirAdtToTy adt) variantTys + expectedVariantShps discrTp discrShp + let variantTprs = + FC.fmapFC variantShapeType expectedVariantShps let enumTpr = Mir.RustEnumRepr discrTpr variantTprs @@ -453,13 +460,14 @@ resolveSetupVal mcc env tyenv nameEnv val = -- Construct the VariantShape of the particular variant that we -- are building. Some variantIdx <- pure $ - variantIntIndex nm variantIdxInt (Ctx.size variantShps) - VariantShape _ expectedFldAssn <- pure $ variantShps Ctx.! variantIdx + variantIntIndex nm variantIdxInt $ + Ctx.size expectedVariantShps + VariantShape expectedFldAssn <- + pure $ expectedVariantShps Ctx.! variantIdx -- Check that the actual field values match the expected types. - Some actualFldValAssn <- pure $ variantFieldsToAssn sym flds' - let (actualFldAssn, actualValAssn) = - Ctx.unzip actualFldValAssn + Some (Functor.Pair actualFldAssn actualValAssn) <- + pure $ variantFieldsToAssns sym flds' Refl <- case W4.testEquality expectedFldAssn actualFldAssn of Just r -> pure r @@ -475,7 +483,107 @@ resolveSetupVal mcc env tyenv nameEnv val = Ctx.empty Ctx.:> RV discrVal Ctx.:> RV (injectVariant sym variantTprs variantIdx actualValAssn) - pure $ MIRVal enumShp (AnyValue enumTpr enumVal) + pure $ MIRVal enumShp $ AnyValue enumTpr enumVal + Mir.Adt nm Mir.Struct _ _ _ _ _ -> + panic "resolveSetupVal" + [ "Expected enum type, received struct:" + , show nm + ] + Mir.Adt nm Mir.Union _ _ _ _ _ -> + panic "resolveSetupVal" + [ "Expected enum type, received union:" + , show nm + ] + MirSetupEnumSymbolic adt discrVal variantFlds -> + case adt of + Mir.Adt nm (Mir.Enum discrTp) variants _ _ _ _ -> do + -- TODO RGS: Document this carefully + -- TODO RGS: Factor out code in common + let discrW = W4.bvWidth discrVal + let discrTpr = BVRepr discrW + let discrShp = tyToShapeEq col discrTp discrTpr + + {- + -- TODO RGS: Delete me + MIRVal discrShp discrVal <- resolveSetupVal mcc env tyenv nameEnv discr + let discrTpr = shapeType discrShp + let discrTp = shapeMirTy discrShp + -} + + variantFlds' <- + zipWithM + (\variant flds -> do + let variantDiscr = getEnumVariantDiscr variant + variantDiscrBV <- W4.bvLit sym discrW $ BV.mkBV discrW variantDiscr + branch <- W4.bvEq sym variantDiscrBV discrVal + flds' <- traverse (resolveSetupVal mcc env tyenv nameEnv) flds + let expectedFlds = variant ^. Mir.vfields + let actualFldTys = map (\(MIRVal shp _) -> shapeMirTy shp) flds' + checkFields + nm + "Enum" + ("fields in enum variant " ++ show (variant ^. Mir.vname)) + expectedFlds + actualFldTys + Some (Functor.Pair fldShpAssn valAssn) <- + pure $ variantFieldsToAssns sym flds' + pure $ Some + $ Functor.Pair + (VariantShape fldShpAssn) + (VB (W4.PE branch valAssn))) + variants + variantFlds + Some variantBranchAssn <- pure $ Ctx.fromList variantFlds' + let (actualVariantShps, branchAssn) = + Ctx.unzip variantBranchAssn + + -- Construct an EnumShape and RustEnumRepr. This requires mapping + -- over /all/ variants, not just the particular variant that we + -- are building. + -- + -- TODO RGS: Factor this out in common with the case above + let variantTys = + map (\v -> v ^.. Mir.vfields . each . Mir.fty) variants + Some expectedVariantShps <- + pure $ Ctx.fromList $ + map (\fldTys -> + case Ctx.fromList $ + map + (\ty -> + case tyToShape col ty of + Some shp -> + if Mir.canInitialize col ty + then Some $ ReqField shp + else Some $ OptField shp) + fldTys of + Some fldAssn -> Some $ VariantShape fldAssn) + variantTys + let enumShp = + EnumShape + (mirAdtToTy adt) variantTys + expectedVariantShps discrTp discrShp + let variantTprs = + FC.fmapFC variantShapeType expectedVariantShps + let enumTpr = Mir.RustEnumRepr + discrTpr + variantTprs + + Refl <- + case W4.testEquality expectedVariantShps actualVariantShps of + Just r -> pure r + Nothing -> + panic "resolveSetupVal" + [ "Enum variant shape mismatch" + , "Expected: " ++ show expectedVariantShps + , "Actual: " ++ show actualVariantShps + ] + + -- Finally, construct a MIRVal. + let enumVal = + Ctx.empty + Ctx.:> RV discrVal + Ctx.:> RV branchAssn + pure $ MIRVal enumShp $ AnyValue enumTpr enumVal Mir.Adt nm Mir.Struct _ _ _ _ _ -> panic "resolveSetupVal" [ "Expected enum type, received struct:" @@ -486,8 +594,6 @@ resolveSetupVal mcc env tyenv nameEnv val = [ "Expected enum type, received union:" , show nm ] - MirSetupEnumSymbolic _adt -> - error "TODO RGS: Symbolic enums" MS.SetupTuple () flds -> do flds' <- traverse (resolveSetupVal mcc env tyenv nameEnv) flds let fldMirTys = map (\(MIRVal shp _) -> shapeMirTy shp) flds' @@ -620,19 +726,29 @@ resolveSetupVal mcc env tyenv nameEnv val = MIRVal shp fld' <- resolveSetupVal mcc env tyenv nameEnv fld pure $ MIRVal (TransparentShape (mirAdtToTy adt) shp) fld' - -- Given the list of fields in a struct or enum variant, construct an - -- Assignment, consisting of each field's type and value. - variantFieldsToAssn :: + -- Given the list of fields in a struct or enum variant, construct two + -- Assignments, where the first Assignment consists of each field's type, + -- and the second assignment consists of each field's value. + variantFieldsToAssns :: Sym -> [MIRVal] -> - Some (Ctx.Assignment (Functor.Product FieldShape (RegValue' Sym))) - variantFieldsToAssn sym flds = - Ctx.fromList $ - map (\(MIRVal shp v) -> - if Mir.canInitialize col (shapeMirTy shp) - then Some $ Functor.Pair (ReqField shp) (RV v) - else Some $ Functor.Pair (OptField shp) (RV (W4.justPartExpr sym v))) - flds + Some (Functor.Product + (Ctx.Assignment FieldShape) + (Ctx.Assignment (RegValue' Sym))) + variantFieldsToAssns sym flds + | Some fldValAssn <- someFldValAssn + , (fldAssn, valAssn) <- Ctx.unzip fldValAssn + = Some $ Functor.Pair fldAssn valAssn + where + someFldValAssn :: + Some (Ctx.Assignment (Functor.Product FieldShape (RegValue' Sym))) + someFldValAssn = + Ctx.fromList $ + map (\(MIRVal shp v) -> + if Mir.canInitialize col (shapeMirTy shp) + then Some $ Functor.Pair (ReqField shp) (RV v) + else Some $ Functor.Pair (OptField shp) (RV (W4.justPartExpr sym v))) + flds -- | An intermediate data structure that is only used by -- 'resolveSetupSliceFromArray'. @@ -886,7 +1002,7 @@ equalValsPred cc mv1 mv2 = goFldAssn fldShp fldAssn1 fldAssn2 (_, _) -> pure $ W4.falsePred sym - goTy (EnumShape _ variantShp _ discrShp) any1 any2 = + goTy (EnumShape _ _ variantShp _ discrShp) any1 any2 = case (any1, any2) of (AnyValue (Mir.RustEnumRepr discrTpr1 variantCtx1) (Ctx.Empty Ctx.:> RV discr1 Ctx.:> RV variant1), @@ -960,7 +1076,7 @@ equalValsPred cc mv1 mv2 = goVariantAssn variantShp vbAssn1 vbAssn2 = FCI.ifoldrMFC (\idx (Functor.Pair (VB var1) (VB var2)) z -> do - VariantShape _ fldShp <- pure $ variantShp Ctx.! idx + VariantShape fldShp <- pure $ variantShp Ctx.! idx varPred <- goVariantFlds fldShp var1 var2 liftIO $ W4.andPred sym varPred z) (W4.truePred sym) @@ -1397,6 +1513,19 @@ staticTyRef static = (static ^. Mir.sTy) (staticMutability static) +-- | Retrieve the discriminant corresponding to an enum variant. This function +-- will panic if the variant does not contain a discriminant. +getEnumVariantDiscr :: Mir.Variant -> Integer +getEnumVariantDiscr variant = + case variant ^. Mir.discrval of + Just discr -> + discr + Nothing -> + panic "getEnumVariantDiscr" + [ "discrval not set for variant:" + , show (variant ^. Mir.vname) + ] + -- | An enum's discriminant should have an integral type such as @isize@ or -- @i8@, which this function checks. If this is not the case, this function will -- panic. diff --git a/src/SAWScript/Crucible/MIR/Setup/Value.hs b/src/SAWScript/Crucible/MIR/Setup/Value.hs index 9c0d540f3c..c1cee9578e 100644 --- a/src/SAWScript/Crucible/MIR/Setup/Value.hs +++ b/src/SAWScript/Crucible/MIR/Setup/Value.hs @@ -12,10 +12,13 @@ module, plus additional functionality) instead. -} {-# Language DataKinds #-} +{-# Language GADTs #-} {-# Language OverloadedStrings #-} {-# Language RankNTypes #-} +{-# Language StandaloneDeriving #-} {-# Language TemplateHaskell #-} {-# Language TypeFamilies #-} +{-# Language TypeOperators #-} module SAWScript.Crucible.MIR.Setup.Value ( -- * @MIRCrucibleContext@ @@ -67,6 +70,7 @@ import Mir.DefId import Mir.Generator import Mir.Intrinsics import qualified Mir.Mir as M +import qualified What4.Interface as W4 import SAWScript.Crucible.Common import qualified SAWScript.Crucible.Common.Setup.Value as MS @@ -143,50 +147,64 @@ data MirPointer sym tp = MirPointer } -- | A enum-related MIR 'SetupValue'. -data MirSetupEnum - = MirSetupEnumVariant M.Adt M.Variant Integer Int [MS.SetupValue MIR] - -- ^ A specific variant of an enum, where: - -- - -- * The 'M.Adt' represents the enum type. - -- - -- * The 'M.Variant' represents the variant. - -- - -- * The 'Integer' is the discriminant value for the variant. - -- - -- * The 'Int' is the index of the variant within the list of all the enum's - -- variants. In most circumstances, this index will be the same as the - -- discriminant value, but the index can be different if a variant uses an - -- explicit value. For instance, in this example: - -- - -- @ - -- enum A { - -- A0, - -- A1, - -- } - -- - -- enum B { - -- B0 = 42, - -- B1, - -- } - -- @ - -- - -- The indexes for @A0@ and @B0@ are both @0@, and the indexes for @A1@ - -- and @B1@ are both @1@. The discriminant values are different, however. - -- The discriminants for @A0@ and @A1@ are @0@ and @1@, respectively, - -- while the discriminants for @B0@ and @B1@ are @42@ and @43@, - -- respectively. - -- - -- * The list of 'MS.SetupValue's are the values of the variant's fields. - -- - -- Note that the discriminant value and index are accessible within the - -- 'M.Variant', but retrieving the information is somewhat involved. (See - -- the implementation of @mir_enum_value@.) For this reason, we store - -- this information separately in 'MirSetupEnumVariant' to make it easier - -- to look up later. - | MirSetupEnumSymbolic M.Adt - -- ^ A symbolic enum value, where the 'M.Adt' represents the enum type. - -- This is only used in the implementation of @mir_fresh_expanded_value@. - deriving Show +data MirSetupEnum where + -- | A specific variant of an enum, where: + -- + -- * The 'M.Adt' represents the enum type. + -- + -- * The 'M.Variant' represents the variant. + -- + -- * The 'Integer' is the discriminant value for the variant. + -- + -- * The 'Int' is the index of the variant within the list of all the enum's + -- variants. In most circumstances, this index will be the same as the + -- discriminant value, but the index can be different if a variant uses an + -- explicit value. For instance, in this example: + -- + -- @ + -- enum A { + -- A0, + -- A1, + -- } + -- + -- enum B { + -- B0 = 42, + -- B1, + -- } + -- @ + -- + -- The indexes for @A0@ and @B0@ are both @0@, and the indexes for @A1@ + -- and @B1@ are both @1@. The discriminant values are different, however. + -- The discriminants for @A0@ and @A1@ are @0@ and @1@, respectively, + -- while the discriminants for @B0@ and @B1@ are @42@ and @43@, + -- respectively. + -- + -- * The list of 'MS.SetupValue's are the values of the variant's fields. + -- + -- Note that the discriminant value and index are accessible within the + -- 'M.Variant', but retrieving the information is somewhat involved. (See + -- the implementation of @mir_enum_value@.) For this reason, we store this + -- information separately in 'MirSetupEnumVariant' to make it easier to look + -- up later. + MirSetupEnumVariant :: + M.Adt -> + M.Variant -> + Integer -> + Int -> + [MS.SetupValue MIR] -> + MirSetupEnum + + -- | A symbolic enum value, where the 'M.Adt' represents the enum type. + -- This is only used in the implementation of @mir_fresh_expanded_value@. + -- + -- TODO RGS: Say something about the last fields + MirSetupEnumSymbolic :: + (1 <= w) => + M.Adt -> + W4.SymBV Sym w -> + [[MS.SetupValue MIR]] -> + MirSetupEnum +deriving instance Show MirSetupEnum -- | A slice-related MIR 'SetupValue'. data MirSetupSlice diff --git a/src/SAWScript/Crucible/MIR/TypeShape.hs b/src/SAWScript/Crucible/MIR/TypeShape.hs index b20ffffc97..92aa2f80c8 100644 --- a/src/SAWScript/Crucible/MIR/TypeShape.hs +++ b/src/SAWScript/Crucible/MIR/TypeShape.hs @@ -106,6 +106,8 @@ data TypeShape (tp :: CrucibleType) where -- 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 @@ -139,7 +141,7 @@ instance PP.Pretty (FieldShape tp) where deriving instance Show (FieldShape tp) instance ShowF FieldShape --- | The 'TypeShape' of an enum variant, which consists of some numer of field +-- | 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 @@ -147,9 +149,7 @@ instance ShowF FieldShape -- 'StructType' as a type index, we only use 'VariantShape' for enums, not -- structs. data VariantShape (tp :: CrucibleType) where - VariantShape :: [M.Ty] - -- ^ The types of the variant's fields. - -> Assignment FieldShape ctx + VariantShape :: Assignment FieldShape ctx -- ^ The shapes of the variant's field types. -> VariantShape (StructType ctx) @@ -222,8 +222,10 @@ tyToShape col = go goEnum ty discrTy vs | Some discrShp <- go discrTy , Some variants <- loop vs Empty - = Some $ EnumShape ty variants discrTy discrShp + = Some $ EnumShape ty variantTys variants discrTy discrShp where + variantTys = map variantFieldTys vs + loop :: forall ctx. [M.Variant] -> @@ -238,7 +240,7 @@ tyToShape col = go goVariant :: M.Variant -> Some VariantShape goVariant v | Some flds <- goFields tys - = Some $ VariantShape tys flds + = Some $ VariantShape flds where tys = variantFieldTys v @@ -296,7 +298,7 @@ shapeType = go go (TupleShape _ _ flds) = StructRepr $ fmapFC fieldShapeType flds go (ArrayShape _ _ shp) = MirVectorRepr $ shapeType shp go (StructShape _ _ _flds) = AnyRepr - go (EnumShape _ _ _ _variants) = AnyRepr + go (EnumShape _ _ _ _ _variants) = AnyRepr go (TransparentShape _ shp) = go shp go (RefShape _ _ _ tpr) = MirReferenceRepr tpr go (SliceShape _ _ _ tpr) = MirSliceRepr tpr @@ -307,7 +309,7 @@ fieldShapeType (ReqField shp) = shapeType shp fieldShapeType (OptField shp) = MaybeRepr $ shapeType shp variantShapeType :: VariantShape tp -> TypeRepr tp -variantShapeType (VariantShape _ flds) = +variantShapeType (VariantShape flds) = StructRepr $ fmapFC fieldShapeType flds shapeMirTy :: TypeShape tp -> M.Ty @@ -316,7 +318,7 @@ shapeMirTy (PrimShape ty _) = ty shapeMirTy (TupleShape ty _ _) = ty shapeMirTy (ArrayShape ty _ _) = ty shapeMirTy (StructShape ty _ _) = ty -shapeMirTy (EnumShape ty _ _ _) = ty +shapeMirTy (EnumShape ty _ _ _ _) = ty shapeMirTy (TransparentShape ty _) = ty shapeMirTy (RefShape ty _ _ _) = ty shapeMirTy (SliceShape ty _ _ _) = ty