ppc-symbolic: Indexes for registers (#445)

GaloisInc · Sep 26, 2024 · 30b4579 · 30b4579
1 parent 206a864
commit 30b4579
Show file tree

Hide file tree

Showing 4 changed files with 547 additions and 130 deletions.
diff --git 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
@@ -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,82 +109,20 @@ 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
                  ) =>
                  MCR.RegEntry sym (MS.ArchRegStruct (MP.AnyPPC 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