From dbce1b1265474456ba32a9bbf79d9c7dbd71a12b Mon Sep 17 00:00:00 2001 From: Luke Maurer Date: Fri, 21 Dec 2018 11:45:32 -0800 Subject: [PATCH] Refactor to use AnyPPC --- .../src/Data/Macaw/PPC/Symbolic.hs | 92 +++++++++---------- macaw-ppc/src/Data/Macaw/PPC.hs | 2 + macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs | 52 ++++++----- submodules/semmc | 2 +- 4 files changed, 71 insertions(+), 77 deletions(-) diff --git a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs index 80255449..77ab09d1 100644 --- a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs +++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs @@ -63,7 +63,6 @@ import qualified Data.Macaw.Types as MT import qualified Data.Macaw.Symbolic as MS import qualified Data.Macaw.Symbolic.PersistentState as MS import qualified Data.Macaw.PPC as MP -import Data.Macaw.PPC.PPCReg ( ArchWidth ) import qualified Data.Macaw.PPC.Symbolic.AtomWrapper as A import qualified Data.Macaw.PPC.Symbolic.Functions as F @@ -91,20 +90,19 @@ ppc32MacawSymbolicFns = , MS.crucGenArchTermStmt = ppcGenTermStmt } -type RegSize ppc = MC.RegAddrWidth (MP.PPCReg ppc) -type RegContext ppc - = (Ctx.EmptyCtx Ctx.::> MT.BVType (RegSize ppc)) -- IP - C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType (RegSize ppc)) -- LNK - C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType (RegSize ppc)) -- CTR - C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType (RegSize ppc)) -- XER - C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType 32) -- CR - C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType 32) -- FPSCR - C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType 32) -- VSCR - C.<+> R.CtxRepeat 32 (MT.BVType (RegSize ppc)) -- GPRs - C.<+> R.CtxRepeat 64 (MT.BVType 128) -- VSRs +type RegSize v = MC.RegAddrWidth (MP.PPCReg (MP.AnyPPC v)) +type RegContext v + = (Ctx.EmptyCtx Ctx.::> MT.BVType (RegSize v)) -- IP + C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType (RegSize v)) -- LNK + C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType (RegSize v)) -- CTR + C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType (RegSize v)) -- XER + C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType 32) -- CR + C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType 32) -- FPSCR + C.<+> (Ctx.EmptyCtx Ctx.::> MT.BVType 32) -- VSCR + C.<+> R.CtxRepeat 32 (MT.BVType (RegSize v)) -- GPRs + C.<+> R.CtxRepeat 64 (MT.BVType 128) -- VSRs -type instance MS.ArchRegContext MP.PPC64 = RegContext MP.PPC64 -type instance MS.ArchRegContext MP.PPC32 = RegContext MP.PPC32 +type instance MS.ArchRegContext (MP.AnyPPC v) = RegContext v type RegAssign ppc f = Ctx.Assignment f (MS.ArchRegContext ppc) @@ -158,9 +156,9 @@ instance MS.ArchInfo MP.PPC32 where ppcRegName :: MP.PPCReg ppc tp -> C.SolverSymbol ppcRegName r = C.systemSymbol ("!" ++ show (MC.prettyF r)) -ppcRegAssignment :: forall ppc - . (1 <= RegSize ppc) - => Ctx.Assignment (MP.PPCReg ppc) (RegContext ppc) +ppcRegAssignment :: forall v + . ( MP.KnownVariant v ) + => Ctx.Assignment (MP.PPCReg (MP.AnyPPC v)) (RegContext v) ppcRegAssignment = (Ctx.Empty Ctx.:> MP.PPC_IP Ctx.:> MP.PPC_LNK @@ -169,32 +167,27 @@ ppcRegAssignment = Ctx.:> MP.PPC_CR Ctx.:> MP.PPC_FPSCR Ctx.:> MP.PPC_VSCR) - Ctx.<++> (R.repeatAssign (MP.PPC_GP . D.GPR . fromIntegral) :: Ctx.Assignment (MP.PPCReg ppc) (R.CtxRepeat 32 (MT.BVType (RegSize ppc)))) - Ctx.<++> (R.repeatAssign (MP.PPC_FR . D.VSReg . fromIntegral) :: Ctx.Assignment (MP.PPCReg ppc) (R.CtxRepeat 64 (MT.BVType 128))) + Ctx.<++> (R.repeatAssign (MP.PPC_GP . D.GPR . fromIntegral) :: Ctx.Assignment (MP.PPCReg (MP.AnyPPC v)) (R.CtxRepeat 32 (MT.BVType (RegSize v)))) + Ctx.<++> (R.repeatAssign (MP.PPC_FR . D.VSReg . fromIntegral) :: Ctx.Assignment (MP.PPCReg (MP.AnyPPC v)) (R.CtxRepeat 64 (MT.BVType 128))) -data PPCSymbolicException ppc = MissingRegisterInState (Some (MP.PPCReg ppc)) +data PPCSymbolicException v = MissingRegisterInState (Some (MP.PPCReg (MP.AnyPPC v))) -deriving instance (Typeable ppc) => Show (PPCSymbolicException ppc) +deriving instance Show (PPCSymbolicException v) -instance (Typeable ppc) => X.Exception (PPCSymbolicException ppc) +instance Typeable v => X.Exception (PPCSymbolicException v) -regIndexMap :: forall ppc - . (1 <= RegSize ppc, 1 <= MC.ArchAddrWidth ppc, - MS.ArchRegContext ppc ~ RegContext ppc, - MC.ArchReg ppc ~ MP.PPCReg ppc, - ArchWidth ppc) - => MS.RegIndexMap ppc +regIndexMap :: forall v + . MP.KnownVariant v + => MS.RegIndexMap (MP.AnyPPC v) regIndexMap = MS.mkRegIndexMap assgn sz where - assgn = ppcRegAssignment @ppc + assgn = ppcRegAssignment @v sz = Ctx.size (MS.typeCtxToCrucible (FC.fmapFC MT.typeRepr assgn)) -lookupReg :: (1 <= RegSize ppc, 1 <= MC.ArchAddrWidth ppc, - X.MonadThrow m, - Typeable ppc, - MS.ArchRegContext ppc ~ RegContext ppc, - MC.ArchReg ppc ~ MP.PPCReg ppc, - ArchWidth ppc) +lookupReg :: forall v ppc m f tp + . (MP.KnownVariant v, + ppc ~ MP.AnyPPC v, + X.MonadThrow m) => MP.PPCReg ppc tp -> Ctx.Assignment f (MS.MacawCrucibleRegTypes ppc) -> m (f (MS.ToCrucibleType tp)) @@ -203,12 +196,10 @@ lookupReg r asgn = Nothing -> X.throwM (MissingRegisterInState (Some r)) Just pair -> return (asgn Ctx.! MS.crucibleIndex pair) -updateReg :: (1 <= RegSize ppc, 1 <= MC.ArchAddrWidth ppc, - MS.ArchRegContext ppc ~ RegContext ppc, - MC.ArchReg ppc ~ MP.PPCReg ppc, - Typeable ppc, - X.MonadThrow m, - ArchWidth ppc) +updateReg :: forall v ppc m f tp + . (MP.KnownVariant v, + ppc ~ MP.AnyPPC v, + X.MonadThrow m) => MP.PPCReg ppc tp -> (f (MS.ToCrucibleType tp) -> f (MS.ToCrucibleType tp)) -> Ctx.Assignment f (MS.MacawCrucibleRegTypes ppc) @@ -218,8 +209,8 @@ updateReg r upd asgn = do Nothing -> X.throwM (MissingRegisterInState (Some r)) Just pair -> return (asgn & MapF.ixF (MS.crucibleIndex pair) %~ upd) -ppcGenFn :: forall ids s tp ppc - . (MS.MacawArchStmtExtension ppc ~ PPCStmtExtension ppc) +ppcGenFn :: forall ids s tp v ppc + . ( ppc ~ MP.AnyPPC v ) => MP.PPCPrimFn ppc (MC.Value ppc ids) tp -> MS.CrucGen ppc ids s (C.Atom s (MS.ToCrucibleType tp)) ppcGenFn fn = do @@ -228,8 +219,8 @@ ppcGenFn fn = do r <- FC.traverseFC f fn MS.evalArchStmt (PPCPrimFn r) -ppcGenStmt :: forall ppc ids s - . (MS.MacawArchStmtExtension ppc ~ PPCStmtExtension ppc) +ppcGenStmt :: forall v ids s ppc + . ( ppc ~ MP.AnyPPC v ) => MP.PPCStmt ppc (MC.Value ppc ids) -> MS.CrucGen ppc ids s () ppcGenStmt s = do @@ -238,8 +229,8 @@ ppcGenStmt s = do s' <- TF.traverseF f s void (MS.evalArchStmt (PPCPrimStmt s')) -ppcGenTermStmt :: forall ppc ids s - . (MS.MacawArchStmtExtension ppc ~ PPCStmtExtension ppc) +ppcGenTermStmt :: forall v ids s ppc + . ( ppc ~ MP.AnyPPC v ) => MP.PPCTermStmt ids -> MC.RegState (MP.PPCReg ppc) (MC.Value ppc ids) -> MS.CrucGen ppc ids s () @@ -276,7 +267,7 @@ instance FC.TraversableFC (PPCStmtExtension ppc) where traverseFC f (PPCPrimStmt s) = PPCPrimStmt <$> TF.traverseF (A.liftAtomTrav f) s traverseFC _f (PPCPrimTerm t) = pure (PPCPrimTerm t) -instance (1 <= MC.RegAddrWidth (MC.ArchReg ppc)) => C.TypeApp (PPCStmtExtension ppc) where +instance (1 <= MC.ArchAddrWidth ppc) => C.TypeApp (PPCStmtExtension ppc) where appType (PPCPrimFn x) = MS.typeToCrucible (MT.typeRepr x) appType (PPCPrimStmt _s) = C.UnitRepr appType (PPCPrimTerm _t) = C.UnitRepr @@ -288,6 +279,5 @@ instance C.PrettyApp (PPCStmtExtension ppc) where MC.ppArchStmt (A.liftAtomIn ppSub) s ppApp _ppSub (PPCPrimTerm t) = MC.prettyF t -type instance MS.MacawArchStmtExtension MP.PPC64 = PPCStmtExtension MP.PPC64 -type instance MS.MacawArchStmtExtension MP.PPC32 = PPCStmtExtension MP.PPC32 - +type instance MS.MacawArchStmtExtension (MP.AnyPPC v) = + PPCStmtExtension (MP.AnyPPC v) diff --git a/macaw-ppc/src/Data/Macaw/PPC.hs b/macaw-ppc/src/Data/Macaw/PPC.hs index b6912693..7eaced00 100644 --- a/macaw-ppc/src/Data/Macaw/PPC.hs +++ b/macaw-ppc/src/Data/Macaw/PPC.hs @@ -17,6 +17,8 @@ module Data.Macaw.PPC ( V32, PPC64, PPC32, + PPC.VariantRepr(..), + PPC.KnownVariant(..), -- * PPC Types R.PPCReg(..), A.PPCTermStmt(..), diff --git a/macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs b/macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs index 632c9b5b..ed19b31d 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs @@ -1,14 +1,17 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE UndecidableInstances #-} @@ -36,12 +39,15 @@ import qualified Data.Parameterized.TH.GADT as TH import qualified Text.PrettyPrint.ANSI.Leijen as PP import qualified Dismantle.PPC as D +import qualified SemMC.Architecture.PPC as PPC import qualified SemMC.Architecture.PPC.Location as APPC -import qualified SemMC.Architecture.PPC32 as PPC32 -import qualified SemMC.Architecture.PPC64 as PPC64 -- | The register type for PowerPC, parameterized by architecture to support -- both PowerPC32 and PowerPC64 + +-- TODO: Refactor so that this takes the PPC variant as an argument +-- rather than the architecture (which is always @PPC.AnyPPC v@ for +-- some @v@). This is likely to be disruptive. data PPCReg arch tp where PPC_GP :: (w ~ MC.RegAddrWidth (PPCReg arch), 1 <= w) => D.GPR -> PPCReg arch (BVType w) PPC_FR :: D.VSReg -> PPCReg arch (BVType 128) @@ -104,22 +110,19 @@ linuxCalleeSaveRegisters :: (w ~ MC.RegAddrWidth (PPCReg ppc), 1 <= w) linuxCalleeSaveRegisters _ = S.fromList [ Some (PPC_GP (D.GPR rnum)) | rnum <- [14..31] ] -type instance MC.RegAddrWidth (PPCReg PPC32.PPC) = 32 -type instance MC.RegAddrWidth (PPCReg PPC64.PPC) = 64 - -type instance MC.ArchReg PPC64.PPC = PPCReg PPC64.PPC -type instance MC.ArchReg PPC32.PPC = PPCReg PPC32.PPC +type instance MC.RegAddrWidth (PPCReg (PPC.AnyPPC v)) = PPC.AddrWidth v +type instance MC.ArchReg (PPC.AnyPPC v) = PPCReg (PPC.AnyPPC v) +{-# DEPRECATED + ArchWidth "Use 'SemMC.Architecture.AddrWidth' and 'SemMC.Architecture.addrWidth'." +#-} class ArchWidth arch where pointerNatRepr :: proxy arch -> NatRepr (MC.RegAddrWidth (PPCReg arch)) -instance ArchWidth PPC32.PPC where - pointerNatRepr _ = n32 +instance PPC.KnownVariant v => ArchWidth (PPC.AnyPPC v) where + pointerNatRepr _ = PPC.addrWidth (PPC.knownVariant @v) -instance ArchWidth PPC64.PPC where - pointerNatRepr _ = n64 - -instance (ArchWidth ppc) => HasRepr (PPCReg ppc) TypeRepr where +instance (PPC.KnownVariant v, ppc ~ PPC.AnyPPC v) => HasRepr (PPCReg ppc) TypeRepr where typeRepr r = case r of PPC_GP {} -> BVTypeRepr (pointerNatRepr (Proxy @ppc)) @@ -132,22 +135,22 @@ instance (ArchWidth ppc) => HasRepr (PPCReg ppc) TypeRepr where PPC_FPSCR -> BVTypeRepr n32 PPC_VSCR -> BVTypeRepr n32 - -instance ( ArchWidth ppc - , MC.ArchReg ppc ~ PPCReg ppc - , MM.MemWidth (MC.RegAddrWidth (MC.ArchReg ppc)) - , 1 <= MC.RegAddrWidth (PPCReg ppc) - , KnownNat (MC.RegAddrWidth (PPCReg ppc))) - => MC.RegisterInfo (PPCReg ppc) where +-- The MM.MemWidth constraint is always satisfiable, but sadly it has +-- to be included since GHC doesn't *know* it's always satisfiable :-\ +instance ( PPC.KnownVariant v, MM.MemWidth (PPC.AddrWidth v) + ) => + MC.RegisterInfo (PPCReg (PPC.AnyPPC v)) where archRegs = ppcRegs sp_reg = PPC_GP (D.GPR 1) ip_reg = PPC_IP syscall_num_reg = PPC_GP (D.GPR 0) syscallArgumentRegs = [ PPC_GP (D.GPR rnum) | rnum <- [3..10] ] -ppcRegs :: forall w ppc - . (w ~ MC.RegAddrWidth (PPCReg ppc), 1 <= w) - => [Some (PPCReg ppc)] +-- FIXME These should probably live somewhere else? + +ppcRegs :: forall v + . ( PPC.KnownVariant v ) + => [Some (PPCReg (PPC.AnyPPC v))] ppcRegs = concat [ gprs , sprs , fprs @@ -163,8 +166,7 @@ ppcRegs = concat [ gprs -- | Translate a location from the semmc semantics into a location suitable for -- use in macaw -locToRegTH :: (1 <= APPC.ArchRegWidth ppc, - MC.RegAddrWidth (PPCReg ppc) ~ APPC.ArchRegWidth ppc) +locToRegTH :: (PPC.KnownVariant v, ppc ~ PPC.AnyPPC v) => proxy ppc -> APPC.Location ppc ctp -> Q Exp diff --git a/submodules/semmc b/submodules/semmc index 22e5860e..2a10cd25 160000 --- a/submodules/semmc +++ b/submodules/semmc @@ -1 +1 @@ -Subproject commit 22e5860e7010c7472c73987912aa562b0b93e329 +Subproject commit 2a10cd2558ca0fd098625e10d20a84ef5b5ace97