SetupValue: Use proper TTG-style extension fields

This removes all of the `HasSetup* :: Bool` type families in favor of new `X*
:: Type` type families. These largely serve the same purpose of distinguishing
which constructors of `SetupValue` are permissible in each language backend,
but they are permit bundling additional, language-specific information into a
`SetupValue`. For instance, the `XSetupStruct` instance for `LLVM` evaluates to
`Bool`, representing whether we are dealing with an LLVM packed struct or not,
and the `XSetupCast` instance for `LLVM` evaluates to an LLVM `Type` to
represent the type to cast to.

One consequence of this design, aside from some `SetupValue` fields moving
around, is that `ppSetupValue` now must perform case analysis on which language
backend is currently in use in order to pretty-print any backend-specific data.
This is accomplished with the new `SAWExt` data type and the corresponding
`IsExt` class.

There is a lot of code that shifts around in this patch, but everything is
still functionally equivalent. In a subsequent patch, I will introduce
additional data into MIR-specific extension fields.

Fixes #1914.

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

@@ -635,11 +635,11 @@ substMethodSpec sc sm ms = do
         MS.SetupVar _ -> return sv
         MS.SetupTerm tt -> MS.SetupTerm <$> goTypedTerm tt
         MS.SetupNull _ -> return sv
-        MS.SetupStruct b packed svs -> MS.SetupStruct b packed <$> mapM goSetupValue svs
+        MS.SetupStruct b svs -> MS.SetupStruct b <$> mapM goSetupValue svs
         MS.SetupArray b svs -> MS.SetupArray b <$> mapM goSetupValue svs
         MS.SetupElem b sv idx -> MS.SetupElem b <$> goSetupValue sv <*> pure idx
         MS.SetupField b sv name -> MS.SetupField b <$> goSetupValue sv <*> pure name
-        MS.SetupCast v _ _ -> case v of {}
+        MS.SetupCast v _ -> case v of {}
         MS.SetupUnion v _ _ -> case v of {}
         MS.SetupGlobal _ _ -> return sv
         MS.SetupGlobalInitializer _ _ -> return sv
@@ -677,14 +677,14 @@ regToSetup bak p eval shp rv = go shp rv
 
     go :: forall tp. TypeShape tp -> RegValue sym tp ->
         BuilderT sym t (OverrideSim p sym MIR rtp args ret) (MS.SetupValue MIR)
-    go (UnitShape _) () = return $ MS.SetupStruct () False []
+    go (UnitShape _) () = return $ MS.SetupStruct () []
     go (PrimShape _ btpr) expr = do
         -- Record all vars used in `expr`
         cache <- use msbVisitCache
         visitExprVars cache expr $ \var -> do
             msbPrePost p . seVars %= Set.insert (Some var)
         liftIO $ MS.SetupTerm <$> eval btpr expr
-    go (TupleShape _ _ flds) rvs = MS.SetupStruct () False <$> goFields flds rvs
+    go (TupleShape _ _ flds) rvs = MS.SetupStruct () <$> goFields flds rvs
     go (ArrayShape _ _ shp) vec = do
         svs <- case vec of
             MirVector_Vector v -> mapM (go shp) (toList v)
@@ -695,7 +695,7 @@ regToSetup bak p eval shp rv = go shp rv
         return $ MS.SetupArray () svs
     go (StructShape _ _ flds) (AnyValue tpr rvs)
       | Just Refl <- testEquality tpr shpTpr =
-        MS.SetupStruct () False <$> goFields flds rvs
+        MS.SetupStruct () <$> goFields flds rvs
       | otherwise = error $ "regToSetup: type error: expected " ++ show shpTpr ++
         ", but got Any wrapping " ++ show tpr
       where shpTpr = StructRepr $ fmapFC fieldShapeType flds

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

@@ -356,7 +356,7 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
   where
     go :: forall tp. TypeShape tp -> RegValue sym tp -> MS.SetupValue MIR ->
         MirOverrideMatcher sym ()
-    go (UnitShape _) () (MS.SetupStruct () False []) = return ()
+    go (UnitShape _) () (MS.SetupStruct () []) = return ()
     go (PrimShape _ _btpr) expr (MS.SetupTerm tt) = do
         loc <- use MS.osLocation
         exprTerm <- liftIO $ eval expr
@@ -390,14 +390,14 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
                         ("mismatch on " ++ show (W4.exprType expr) ++ ": expected " ++
                             show (W4.printSymExpr val))
                         ""
-    go (TupleShape _ _ flds) rvs (MS.SetupStruct () False svs) = goFields flds rvs svs
+    go (TupleShape _ _ flds) rvs (MS.SetupStruct () svs) = goFields flds rvs svs
     go (ArrayShape _ _ shp) vec (MS.SetupArray () svs) = case vec of
         MirVector_Vector v -> zipWithM_ (\x y -> go shp x y) (toList v) svs
         MirVector_PartialVector pv -> forM_ (zip (toList pv) svs) $ \(p, sv) -> do
             rv <- liftIO $ readMaybeType sym "vector element" (shapeType shp) p
             go shp rv sv
         MirVector_Array _ -> error $ "matchArg: MirVector_Array NYI"
-    go (StructShape _ _ flds) (AnyValue tpr rvs) (MS.SetupStruct () False svs)
+    go (StructShape _ _ flds) (AnyValue tpr rvs) (MS.SetupStruct () svs)
       | Just Refl <- testEquality tpr shpTpr = goFields flds rvs svs
       | otherwise = error $ "matchArg: type error: expected " ++ show shpTpr ++
         ", but got Any wrapping " ++ show tpr
@@ -510,7 +510,7 @@ setupToReg :: forall sym t st fs tp.
 setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
   where
     go :: forall tp. TypeShape tp -> MS.SetupValue MIR -> IO (RegValue sym tp)
-    go (UnitShape _) (MS.SetupStruct _ False []) = return ()
+    go (UnitShape _) (MS.SetupStruct _ []) = return ()
     go (PrimShape _ btpr) (MS.SetupTerm tt) = do
         term <- liftIO $ SAW.scInstantiateExt sc termSub $ SAW.ttTerm tt
         Some expr <- termToExpr sym sc regMap term
@@ -519,11 +519,11 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
             Nothing -> error $ "setupToReg: expected " ++ show btpr ++ ", but got " ++
                 show (W4.exprType expr)
         return expr
-    go (TupleShape _ _ flds) (MS.SetupStruct _ False svs) = goFields flds svs
+    go (TupleShape _ _ flds) (MS.SetupStruct _ svs) = goFields flds svs
     go (ArrayShape _ _ shp) (MS.SetupArray _ svs) = do
         rvs <- mapM (go shp) svs
         return $ MirVector_Vector $ V.fromList rvs
-    go (StructShape _ _ flds) (MS.SetupStruct _ False svs) =
+    go (StructShape _ _ flds) (MS.SetupStruct _ svs) =
         AnyValue (StructRepr $ fmapFC fieldShapeType flds) <$> goFields flds svs
     go (TransparentShape _ shp) sv = go shp sv
     go (RefShape _ _ _ tpr) (MS.SetupVar alloc) = case Map.lookup alloc allocMap of

src/SAWScript/Crucible/Common/MethodSpec.hs

@@ -15,8 +15,10 @@ Grow\", and is prevalent across the Crucible codebase.
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeFamilyDependencies #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -32,23 +34,19 @@ module SAWScript.Crucible.Common.MethodSpec
   , AllocSpec
   , TypeName
   , ExtType
-  , CastType
   , PointsTo
   , AllocGlobal
   , ResolvedState
 
-  , BoolToType
-  , B
-
-  , HasSetupNull
-  , HasSetupStruct
-  , HasSetupArray
-  , HasSetupElem
-  , HasSetupField
-  , HasSetupGlobal
-  , HasSetupCast
-  , HasSetupUnion
-  , HasSetupGlobalInitializer
+  , XSetupNull
+  , XSetupStruct
+  , XSetupArray
+  , XSetupElem
+  , XSetupField
+  , XSetupGlobal
+  , XSetupCast
+  , XSetupUnion
+  , XSetupGlobalInitializer
 
   , SetupValue(..)
   , SetupValueHas
@@ -62,7 +60,7 @@ module SAWScript.Crucible.Common.MethodSpec
   , setupToTypedTerm
   , setupToTerm
 
-  , HasGhostState
+  , XGhostState
   , GhostValue
   , GhostType
   , GhostGlobal
@@ -111,10 +109,12 @@ module SAWScript.Crucible.Common.MethodSpec
   , makeCrucibleMethodSpecIR
   ) where
 
+import           Data.Kind (Type)
 import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Set (Set)
 import           Data.Time.Clock
+import           Data.Void (absurd)
 
 import           Control.Monad.Trans.Maybe
 import           Control.Monad.Trans (lift)
@@ -126,16 +126,21 @@ import           Data.Parameterized.Nonce
 -- what4
 import           What4.ProgramLoc (ProgramLoc(plSourceLoc), Position)
 
+import           Lang.Crucible.JVM (JVM)
 import qualified Lang.Crucible.Types as Crucible
   (IntrinsicType, EmptyCtx)
 import qualified Lang.Crucible.CFG.Common as Crucible (GlobalVar)
+import           Mir.Intrinsics (MIR)
 
 import qualified Cryptol.Utils.PP as Cryptol
 
 import           Verifier.SAW.TypedTerm as SAWVerifier
 import           Verifier.SAW.SharedTerm as SAWVerifier
 
 import           SAWScript.Crucible.Common.Setup.Value
+import           SAWScript.Crucible.LLVM.Setup.Value (LLVM)
+import           SAWScript.Crucible.JVM.Setup.Value ()
+import           SAWScript.Crucible.MIR.Setup.Value ()
 import           SAWScript.Options
 import           SAWScript.Prover.SolverStats
 import           SAWScript.Utils (bullets)
@@ -153,30 +158,75 @@ stateCond PostState = "postcondition"
 --------------------------------------------------------------------------------
 -- ** SetupValue
 
+-- | A singleton type that encodes the extensions used for each SAW backend.
+-- Matching on a value of type @'SAWExt' ext@ allows one to learn which backend
+-- is currently in use.
+data SAWExt :: Type -> Type where
+  LLVMExt :: SAWExt (LLVM arch)
+  JVMExt  :: SAWExt JVM
+  MIRExt  :: SAWExt MIR
+
+-- | This allows checking which SAW backend we are using at runtime.
+class IsExt ext where
+  sawExt :: SAWExt ext
+
+instance IsExt (LLVM arch) where
+  sawExt = LLVMExt
+instance IsExt JVM where
+  sawExt = JVMExt
+instance IsExt MIR where
+  sawExt = MIRExt
+
 -- | Note that most 'SetupValue' concepts (like allocation indices)
 --   are implementation details and won't be familiar to users.
---   Consider using 'resolveSetupValue' and printing an 'LLVMVal'
---   with @PP.pretty@ instead.
-ppSetupValue :: Show (CastType ext) => SetupValue ext -> PP.Doc ann
+--   Consider using 'resolveSetupValue' and printing the language-specific value
+--   (e.g., an 'LLVMVal') with @PP.pretty@ instead.
+ppSetupValue :: forall ext ann. IsExt ext => SetupValue ext -> PP.Doc ann
 ppSetupValue setupval = case setupval of
   SetupTerm tm   -> ppTypedTerm tm
   SetupVar i     -> ppAllocIndex i
   SetupNull _    -> PP.pretty "NULL"
-  SetupStruct _ packed vs
-    | packed     -> PP.angles (PP.braces (commaList (map ppSetupValue vs)))
-    | otherwise  -> PP.braces (commaList (map ppSetupValue vs))
+  SetupStruct x vs ->
+    case (ext, x) of
+      (LLVMExt, packed) ->
+        ppSetupStructLLVM packed vs
+      (JVMExt, empty) ->
+        absurd empty
+      (MIRExt, ()) ->
+        ppSetupStructDefault vs
   SetupArray _ vs  -> PP.brackets (commaList (map ppSetupValue vs))
   SetupElem _ v i  -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ show i)
   SetupField _ v f -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ f)
   SetupUnion _ v u -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ u)
-  SetupCast _ v tp -> PP.parens (ppSetupValue v) PP.<> PP.pretty (" AS " ++ show tp)
+  SetupCast x v ->
+    case (ext, x) of
+      (LLVMExt, tp) ->
+        PP.parens (ppSetupValue v) PP.<> PP.pretty (" AS " ++ show tp)
+      (JVMExt, empty) ->
+        absurd empty
+      (MIRExt, empty) ->
+        absurd empty
   SetupGlobal _ nm -> PP.pretty ("global(" ++ nm ++ ")")
   SetupGlobalInitializer _ nm -> PP.pretty ("global_initializer(" ++ nm ++ ")")
   where
+    ext :: SAWExt ext
+    ext = sawExt @ext
+
     commaList :: [PP.Doc ann] -> PP.Doc ann
     commaList []     = PP.emptyDoc
     commaList (x:xs) = x PP.<> PP.hcat (map (\y -> PP.comma PP.<+> y) xs)
 
+    ppSetupStructLLVM ::
+         Bool
+         -- ^ 'True' if this is an LLVM packed struct, 'False' otherwise.
+      -> [SetupValue ext] -> PP.Doc ann
+    ppSetupStructLLVM packed vs
+      | packed    = PP.angles (ppSetupStructDefault vs)
+      | otherwise = ppSetupStructDefault vs
+
+    ppSetupStructDefault :: [SetupValue ext] -> PP.Doc ann
+    ppSetupStructDefault vs = PP.braces (commaList (map ppSetupValue vs))
+
 ppAllocIndex :: AllocIndex -> PP.Doc ann
 ppAllocIndex i = PP.pretty '@' <> PP.viaShow i
 
@@ -224,7 +274,7 @@ setupToTerm opts sc =
   \case
     SetupTerm term -> return (ttTerm term)
 
-    SetupStruct _ _ fields ->
+    SetupStruct _ fields ->
       do ts <- mapM (setupToTerm opts sc) fields
          lift $ scTuple sc ts
 
@@ -248,7 +298,7 @@ setupToTerm opts sc =
              typ <- lift $ scTypeOf sc et
              lift $ scAt sc lent typ art ixt
 
-        SetupStruct _ _ fs ->
+        SetupStruct _ fs ->
           do st <- setupToTerm opts sc base
              lift $ scTupleSelector sc st ind (length fs)
 
@@ -270,14 +320,14 @@ type GhostGlobal = Crucible.GlobalVar GhostType
 data SetupCondition ext where
   SetupCond_Equal    :: ConditionMetadata -> SetupValue ext -> SetupValue ext -> SetupCondition ext
   SetupCond_Pred     :: ConditionMetadata -> TypedTerm -> SetupCondition ext
-  SetupCond_Ghost    :: B (HasGhostState ext) ->
+  SetupCond_Ghost    :: XGhostState ext ->
                         ConditionMetadata ->
                         GhostGlobal ->
                         TypedTerm ->
                         SetupCondition ext
 
 deriving instance ( SetupValueHas Show ext
-                  , Show (B (HasGhostState ext))
+                  , Show (XGhostState ext)
                   ) => Show (SetupCondition ext)
 
 -- | Verification state (either pre- or post-) specification