From b4ca323f23d5a084a7f0e259819301c09597b583 Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 25 Sep 2024 15:04:38 -0400 Subject: [PATCH] ppc-symbolic: Factor register-related definitions into their own module --- macaw-ppc-symbolic/macaw-ppc-symbolic.cabal | 1 + .../src/Data/Macaw/PPC/Symbolic.hs | 130 +-------------- .../src/Data/Macaw/PPC/Symbolic/Regs.hs | 155 ++++++++++++++++++ 3 files changed, 162 insertions(+), 124 deletions(-) create mode 100644 macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Regs.hs diff --git a/macaw-ppc-symbolic/macaw-ppc-symbolic.cabal b/macaw-ppc-symbolic/macaw-ppc-symbolic.cabal index 0c129de8..90f4871a 100644 --- a/macaw-ppc-symbolic/macaw-ppc-symbolic.cabal +++ b/macaw-ppc-symbolic/macaw-ppc-symbolic.cabal @@ -17,6 +17,7 @@ cabal-version: >=1.10 library exposed-modules: Data.Macaw.PPC.Symbolic + Data.Macaw.PPC.Symbolic.Regs other-modules: Data.Macaw.PPC.Symbolic.AtomWrapper Data.Macaw.PPC.Symbolic.Functions Data.Macaw.PPC.Symbolic.Panic diff --git a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs index 296f56ee..66d6cbae 100644 --- a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs +++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs @@ -1,15 +1,12 @@ -{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} @@ -19,46 +16,23 @@ module Data.Macaw.PPC.Symbolic ( ppcMacawEvalFn, F.SymFuns, F.newSymFuns, - getReg, - lookupReg, - updateReg, F.SemanticsError(..), - -- * Register names - IP, - LNK, - CTR, - XER, - CR, - FPSCR, - VSCR, - GP, - FR, - -- * Other types - RegContext ) where import GHC.TypeLits -import Control.Lens ( (^.), (%~), (&) ) import Control.Monad ( void ) -import qualified Control.Monad.Catch as X import Control.Monad.IO.Class ( liftIO ) import qualified Data.Functor.Identity as I import qualified Data.Kind as DK import qualified Data.Parameterized.Context as Ctx -import qualified Data.Parameterized.Map as MapF -import Data.Parameterized.Some ( Some(..) ) import qualified Data.Parameterized.TraversableF as TF import qualified Data.Parameterized.TraversableFC as FC -import Data.Typeable ( Typeable ) -import qualified Dismantle.PPC as D import qualified Lang.Crucible.Backend as C import qualified Lang.Crucible.CFG.Expr as C import qualified Lang.Crucible.CFG.Reg as C import qualified Lang.Crucible.LLVM.MemModel as Mem import qualified Lang.Crucible.Types as C -import qualified What4.Interface as C -import qualified What4.Symbol as C import qualified Data.Macaw.CFG as MC import qualified Data.Macaw.Types as MT @@ -72,7 +46,7 @@ import qualified SemMC.Architecture.PPC as SP import qualified Data.Macaw.PPC.Symbolic.AtomWrapper as A import qualified Data.Macaw.PPC.Symbolic.Functions as F import qualified Data.Macaw.PPC.Symbolic.Panic as P -import qualified Data.Macaw.PPC.Symbolic.Repeat as R +import qualified Data.Macaw.PPC.Symbolic.Regs as Regs ppcMacawSymbolicFns :: ( SP.KnownVariant v , 1 <= SP.AddrWidth v @@ -81,43 +55,14 @@ ppcMacawSymbolicFns :: ( SP.KnownVariant v ppcMacawSymbolicFns = MSB.MacawSymbolicArchFunctions { MSB.crucGenArchConstraints = \x -> x - , MSB.crucGenArchRegName = ppcRegName - , MSB.crucGenRegAssignment = ppcRegAssignment - , MSB.crucGenRegStructType = ppcRegStructType + , MSB.crucGenArchRegName = Regs.ppcRegName + , MSB.crucGenRegAssignment = Regs.ppcRegAssignment + , MSB.crucGenRegStructType = Regs.ppcRegStructType , MSB.crucGenArchFn = ppcGenFn , MSB.crucGenArchStmt = ppcGenStmt , MSB.crucGenArchTermStmt = ppcGenTermStmt } -type RegSize v = MC.RegAddrWidth (MP.PPCReg 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.AnyPPC v) = RegContext v - -type RegAssign ppc f = Ctx.Assignment f (MS.ArchRegContext ppc) - -type IP = 0 -type LNK = 1 -type CTR = 2 -type XER = 3 -type CR = 4 -type FPSCR = 5 -type VSCR = 6 -type GP n = 7 + n -type FR n = 39 + n - -getReg :: forall n t f ppc . (Ctx.Idx n (MS.ArchRegContext ppc) t) => RegAssign ppc f -> f t -getReg = (^. (Ctx.field @n)) - ppcMacawEvalFn :: ( C.IsSymInterface sym , 1 <= SP.AddrWidth v ) @@ -164,55 +109,6 @@ instance MS.IsMemoryModel mem => MS.GenArchInfo mem (SP.AnyPPC SP.V32) where , MS.updateReg = archUpdateReg } -ppcRegName :: MP.PPCReg v tp -> C.SolverSymbol -ppcRegName r = C.systemSymbol ("r!" ++ show (MC.prettyF r)) - -ppcRegAssignment :: forall v - . ( MP.KnownVariant v ) - => Ctx.Assignment (MP.PPCReg v) (RegContext v) -ppcRegAssignment = - (Ctx.Empty Ctx.:> MP.PPC_IP - Ctx.:> MP.PPC_LNK - Ctx.:> MP.PPC_CTR - Ctx.:> MP.PPC_XER - 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 v) (R.CtxRepeat 32 (MT.BVType (RegSize v)))) - Ctx.<++> (R.repeatAssign (MP.PPC_FR . D.VSReg . fromIntegral) :: Ctx.Assignment (MP.PPCReg v) (R.CtxRepeat 64 (MT.BVType 128))) - -ppcRegStructType :: forall v - . ( MP.KnownVariant v ) - => C.TypeRepr (MS.ArchRegStruct (MP.AnyPPC v)) -ppcRegStructType = - C.StructRepr (MS.typeCtxToCrucible $ FC.fmapFC MT.typeRepr ppcRegAssignment) - -data PPCSymbolicException v = MissingRegisterInState (Some (MP.PPCReg v)) - -deriving instance Show (PPCSymbolicException v) - -instance Typeable v => X.Exception (PPCSymbolicException v) - -regIndexMap :: forall v - . MP.KnownVariant v - => MSB.RegIndexMap (MP.AnyPPC v) -regIndexMap = MSB.mkRegIndexMap assgn sz - where - assgn = ppcRegAssignment @v - sz = Ctx.size (MS.typeCtxToCrucible (FC.fmapFC MT.typeRepr assgn)) - -lookupReg :: forall v ppc m f tp - . (MP.KnownVariant v, - ppc ~ MP.AnyPPC v, - X.MonadThrow m) - => MP.PPCReg v tp - -> Ctx.Assignment f (MS.MacawCrucibleRegTypes ppc) - -> m (f (MS.ToCrucibleType tp)) -lookupReg r asgn = - case MapF.lookup r regIndexMap of - Nothing -> X.throwM (MissingRegisterInState (Some r)) - Just pair -> return (asgn Ctx.! MSB.crucibleIndex pair) - archLookupReg :: ( MP.KnownVariant v , ppc ~ MP.AnyPPC v ) => @@ -220,26 +116,13 @@ archLookupReg :: ( MP.KnownVariant v -> MP.PPCReg v tp -> MCR.RegEntry sym (MS.ToCrucibleType tp) archLookupReg regEntry reg = - case lookupReg reg (MCR.regValue regEntry) of + case Regs.lookupReg reg (MCR.regValue regEntry) of Just (MCRV.RV val) -> MCR.RegEntry (MS.typeToCrucible $ MT.typeRepr reg) val Nothing -> P.panic P.PPC "archLookupReg" ["unexpected register: " ++ show (MC.prettyF reg)] -updateReg :: forall v ppc m f tp - . (MP.KnownVariant v, - ppc ~ MP.AnyPPC v, - X.MonadThrow m) - => MP.PPCReg v tp - -> (f (MS.ToCrucibleType tp) -> f (MS.ToCrucibleType tp)) - -> Ctx.Assignment f (MS.MacawCrucibleRegTypes ppc) - -> m (Ctx.Assignment f (MS.MacawCrucibleRegTypes ppc)) -updateReg r upd asgn = do - case MapF.lookup r regIndexMap of - Nothing -> X.throwM (MissingRegisterInState (Some r)) - Just pair -> return (asgn & MapF.ixF (MSB.crucibleIndex pair) %~ upd) - archUpdateReg :: ( MP.KnownVariant v , ppc ~ MP.AnyPPC v ) => @@ -248,14 +131,13 @@ archUpdateReg :: ( MP.KnownVariant v -> MCRV.RegValue sym (MS.ToCrucibleType tp) -> MCR.RegEntry sym (MS.ArchRegStruct (MP.AnyPPC v)) archUpdateReg regEntry reg val = - case updateReg reg (const $ MCRV.RV val) (MCR.regValue regEntry) of + case Regs.updateReg reg (const $ MCRV.RV val) (MCR.regValue regEntry) of Just r -> regEntry { MCR.regValue = r } Nothing -> P.panic P.PPC "archUpdateReg" ["unexpected register: " ++ show (MC.prettyF reg)] - ppcGenFn :: forall ids s tp v ppc . ( ppc ~ MP.AnyPPC v , 1 <= SP.AddrWidth v diff --git a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Regs.hs b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Regs.hs new file mode 100644 index 00000000..cefeb6bc --- /dev/null +++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic/Regs.hs @@ -0,0 +1,155 @@ +{-| +Copyright : (c) Galois, Inc 2024 +Maintainer : Langston Barrett + +PPC registers. + +This module is meant to be imported qualified, as it exports many terse names. +-} + +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Data.Macaw.PPC.Symbolic.Regs + ( RegContext + , PPCSymbolicException(..) + , ppcRegName + , ppcRegAssignment + , ppcRegStructType + , getReg + , regIndexMap + , lookupReg + , updateReg + , IP + , LNK + , CTR + , XER + , CR + , FPSCR + , VSCR + , GP + , FR + ) where + +import Control.Lens ( (^.), (%~), (&) ) +import qualified Control.Monad.Catch as X +import qualified Data.Parameterized.Context as Ctx +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.Some ( Some(..) ) +import qualified Data.Parameterized.TraversableFC as FC +import Data.Typeable ( Typeable ) +import qualified Dismantle.PPC as D +import GHC.TypeLits +import qualified Lang.Crucible.Types as C +import qualified What4.Interface as C +import qualified What4.Symbol as C + +import qualified Data.Macaw.CFG as MC +import qualified Data.Macaw.Types as MT +import qualified Data.Macaw.Symbolic as MS +import qualified Data.Macaw.Symbolic.Backend as MSB +import qualified Data.Macaw.PPC as MP + +import qualified Data.Macaw.PPC.Symbolic.Repeat as R + +type RegSize v = MC.RegAddrWidth (MP.PPCReg 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.AnyPPC v) = RegContext v + +type RegAssign ppc f = Ctx.Assignment f (MS.ArchRegContext ppc) + +type IP = 0 +type LNK = 1 +type CTR = 2 +type XER = 3 +type CR = 4 +type FPSCR = 5 +type VSCR = 6 +type GP n = 7 + n +type FR n = 39 + n + +getReg :: forall n t f ppc . (Ctx.Idx n (MS.ArchRegContext ppc) t) => RegAssign ppc f -> f t +getReg = (^. (Ctx.field @n)) + +ppcRegName :: MP.PPCReg v tp -> C.SolverSymbol +ppcRegName r = C.systemSymbol ("r!" ++ show (MC.prettyF r)) + +ppcRegAssignment :: forall v + . ( MP.KnownVariant v ) + => Ctx.Assignment (MP.PPCReg v) (RegContext v) +ppcRegAssignment = + (Ctx.Empty Ctx.:> MP.PPC_IP + Ctx.:> MP.PPC_LNK + Ctx.:> MP.PPC_CTR + Ctx.:> MP.PPC_XER + 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 v) (R.CtxRepeat 32 (MT.BVType (RegSize v)))) + Ctx.<++> (R.repeatAssign (MP.PPC_FR . D.VSReg . fromIntegral) :: Ctx.Assignment (MP.PPCReg v) (R.CtxRepeat 64 (MT.BVType 128))) + +ppcRegStructType :: forall v + . ( MP.KnownVariant v ) + => C.TypeRepr (MS.ArchRegStruct (MP.AnyPPC v)) +ppcRegStructType = + C.StructRepr (MS.typeCtxToCrucible $ FC.fmapFC MT.typeRepr ppcRegAssignment) + +data PPCSymbolicException v = MissingRegisterInState (Some (MP.PPCReg v)) + +deriving instance Show (PPCSymbolicException v) + +instance Typeable v => X.Exception (PPCSymbolicException v) + +regIndexMap :: forall v + . MP.KnownVariant v + => MSB.RegIndexMap (MP.AnyPPC v) +regIndexMap = MSB.mkRegIndexMap assgn sz + where + assgn = ppcRegAssignment @v + sz = Ctx.size (MS.typeCtxToCrucible (FC.fmapFC MT.typeRepr assgn)) + +lookupReg :: forall v ppc m f tp + . (MP.KnownVariant v, + ppc ~ MP.AnyPPC v, + X.MonadThrow m) + => MP.PPCReg v tp + -> Ctx.Assignment f (MS.MacawCrucibleRegTypes ppc) + -> m (f (MS.ToCrucibleType tp)) +lookupReg r asgn = + case MapF.lookup r regIndexMap of + Nothing -> X.throwM (MissingRegisterInState (Some r)) + Just pair -> return (asgn Ctx.! MSB.crucibleIndex pair) + +updateReg :: forall v ppc m f tp + . (MP.KnownVariant v, + ppc ~ MP.AnyPPC v, + X.MonadThrow m) + => MP.PPCReg v tp + -> (f (MS.ToCrucibleType tp) -> f (MS.ToCrucibleType tp)) + -> Ctx.Assignment f (MS.MacawCrucibleRegTypes ppc) + -> m (Ctx.Assignment f (MS.MacawCrucibleRegTypes ppc)) +updateReg r upd asgn = do + case MapF.lookup r regIndexMap of + Nothing -> X.throwM (MissingRegisterInState (Some r)) + Just pair -> return (asgn & MapF.ixF (MSB.crucibleIndex pair) %~ upd)