From fcff1b7c3df0b71d6bcc7d21cf925b04d639ff60 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Wed, 27 Feb 2019 11:34:24 -0800 Subject: [PATCH] Update all source files for NoStarIsType pragma. --- symbolic/src/Data/Macaw/Symbolic/CrucGen.hs | 17 +++++++++-------- .../src/Data/Macaw/Symbolic/PersistentState.hs | 5 +++-- 2 files changed, 12 insertions(+), 10 deletions(-) diff --git a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs index 19723565..8c09968b 100644 --- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs +++ b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs @@ -84,6 +84,7 @@ import Control.Monad.Except import Control.Monad.ST import Control.Monad.State.Strict import Data.Bits +import qualified Data.Kind as K import qualified Data.Macaw.CFG as M import qualified Data.Macaw.CFG.Block as M import qualified Data.Macaw.Discovery.State as M @@ -127,14 +128,14 @@ import Data.Macaw.Symbolic.PersistentState -- -- The registers are stored in an 'Ctx.Assignment' tagged with their Macaw -- types; this is a conversion of those Macaw types into Crucible types. -type MacawCrucibleRegTypes (arch :: *) = CtxToCrucibleType (ArchRegContext arch) +type MacawCrucibleRegTypes (arch :: K.Type) = CtxToCrucibleType (ArchRegContext arch) -- | The type of the register file in the symbolic simulator -- -- At run time, this is an 'Ctx.Assignment' of registers (where each register -- has a Crucible type, which is mapped via 'CtxToCrucibleType' from its Macaw -- type). -type ArchRegStruct (arch :: *) = C.StructType (MacawCrucibleRegTypes arch) +type ArchRegStruct (arch :: K.Type) = C.StructType (MacawCrucibleRegTypes arch) type ArchAddrCrucibleType arch = MM.LLVMPointerType (M.ArchAddrWidth arch) @@ -163,7 +164,7 @@ type ArchAddrWidthRepr arch = M.AddrWidthRepr (M.ArchAddrWidth arch) -- -- The simplest examples are support for systems call instructions and other -- instructions with effects not expressible as Crucible code. -type family MacawArchStmtExtension (arch :: *) :: (C.CrucibleType -> *) -> C.CrucibleType -> * +type family MacawArchStmtExtension (arch :: K.Type) :: (C.CrucibleType -> K.Type) -> C.CrucibleType -> K.Type type MacawArchConstraints arch = ( TraversableFC (MacawArchStmtExtension arch) @@ -239,8 +240,8 @@ type BVPtr a = MM.LLVMPointerType (M.ArchAddrWidth a) -- | The extra expressions required to extend Crucible to support simulating -- Macaw programs -data MacawExprExtension (arch :: *) - (f :: C.CrucibleType -> *) +data MacawExprExtension (arch :: K.Type) + (f :: C.CrucibleType -> K.Type) (tp :: C.CrucibleType) where -- | Test to see if a given operation ('MacawOverflowOp') overflows -- @@ -317,8 +318,8 @@ instance C.TypeApp (MacawExprExtension arch) where -- Note that the various @*Ptr@ operations below are statements, rather than -- expressions, because they need to access memory (via the Crucible global -- variable that contains the current memory model). -data MacawStmtExtension (arch :: *) - (f :: C.CrucibleType -> *) +data MacawStmtExtension (arch :: K.Type) + (f :: C.CrucibleType -> K.Type) (tp :: C.CrucibleType) where @@ -535,7 +536,7 @@ instance C.TypeApp (MacawArchStmtExtension arch) -- MacawExt -- | The Crucible extension used to represent Macaw-specific operations -data MacawExt (arch :: *) +data MacawExt (arch :: K.Type) type instance C.ExprExtension (MacawExt arch) = MacawExprExtension arch type instance C.StmtExtension (MacawExt arch) = MacawStmtExtension arch diff --git a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs index 2fc8bef5..f6ce9fe9 100644 --- a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs +++ b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs @@ -44,6 +44,7 @@ module Data.Macaw.Symbolic.PersistentState import Control.Monad.ST (ST) +import qualified Data.Kind as K import qualified Data.Macaw.CFG as M import qualified Data.Macaw.Types as M import Data.Parameterized.Classes @@ -55,8 +56,8 @@ import Data.Parameterized.Nonce (NonceGenerator) import Data.Parameterized.TraversableF import Data.Parameterized.TraversableFC import qualified Lang.Crucible.CFG.Reg as CR -import qualified Lang.Crucible.Types as C import qualified Lang.Crucible.LLVM.MemModel as MM +import qualified Lang.Crucible.Types as C ------------------------------------------------------------------------ -- Type mappings @@ -179,7 +180,7 @@ memReprToCrucible = typeToCrucible . M.typeRepr -- -- For a hypothetical architecture with two 64 bit general purpose registers and -- a single 32 bit flags register. -type family ArchRegContext (arch :: *) :: Ctx M.Type +type family ArchRegContext (arch :: K.Type) :: Ctx M.Type -- | This relates an index from macaw to Crucible. data IndexPair ctx tp = IndexPair