aarch32-symbolic: Add SIMD register Indexes, factor registers into a module

macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal

@@ -20,6 +20,7 @@ extra-source-files:  CHANGELOG.md
 library
   exposed-modules:     Data.Macaw.AArch32.Symbolic
                        Data.Macaw.AArch32.Symbolic.ABI
+                       Data.Macaw.AArch32.Symbolic.Regs
   other-modules:       Data.Macaw.AArch32.Symbolic.AtomWrapper
                        Data.Macaw.AArch32.Symbolic.Functions
                        Data.Macaw.AArch32.Symbolic.Panic

macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs

@@ -6,38 +6,17 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module Data.Macaw.AArch32.Symbolic (
   aarch32MacawSymbolicFns
   , lookupReg
   , updateReg
   , AF.AArch32Exception(..)
-  , r0
-  , r1
-  , r2
-  , r3
-  , r4
-  , r5
-  , r6
-  , r7
-  , r8
-  , r9
-  , r10
-  , r11
-  , fp
-  , r12
-  , ip
-  , r13
-  , sp
-  , r14
-  , lr
   ) where
 
 import qualified Data.Text as T
 import           GHC.Stack ( HasCallStack )
-import           GHC.TypeLits
 
 import           Control.Lens ( (&), (%~) )
 import           Control.Monad ( void )
@@ -51,19 +30,15 @@ import qualified Data.Macaw.Symbolic.Backend as MSB
 import qualified Data.Macaw.Types as MT
 import qualified Data.Parameterized.Classes as PC
 import qualified Data.Parameterized.Context as Ctx
-import qualified Data.Parameterized.CtxFuns as PC
 import qualified Data.Parameterized.Map as MapF
 import qualified Data.Parameterized.NatRepr as PN
 import qualified Data.Parameterized.TraversableF as TF
 import qualified Data.Parameterized.TraversableFC as FC
-import           Data.Proxy ( Proxy(..) )
 import qualified Data.Sequence as Seq
-import qualified What4.BaseTypes as WT
 import qualified What4.ProgramLoc as WP
 import qualified What4.Symbol as WS
 import qualified What4.Utils.StringLiteral as WUS
 
-import qualified Language.ASL.Globals as LAG
 import qualified SemMC.Architecture.AArch32 as SA
 import qualified Data.Macaw.ARM.Arch as MAA
 import qualified Data.Macaw.ARM.ARMReg as MAR
@@ -80,14 +55,15 @@ import qualified Lang.Crucible.Types as CT
 import qualified Data.Macaw.AArch32.Symbolic.AtomWrapper as AA
 import qualified Data.Macaw.AArch32.Symbolic.Functions as AF
 import qualified Data.Macaw.AArch32.Symbolic.Panic as AP
+import qualified Data.Macaw.AArch32.Symbolic.Regs as AR
 
 aarch32MacawSymbolicFns :: MS.MacawSymbolicArchFunctions SA.AArch32
 aarch32MacawSymbolicFns =
   MSB.MacawSymbolicArchFunctions
   { MSB.crucGenArchConstraints = \x -> x
   , MSB.crucGenArchRegName = aarch32RegName
-  , MSB.crucGenRegAssignment = aarch32RegAssignment
-  , MSB.crucGenRegStructType = aarch32RegStructType
+  , MSB.crucGenRegAssignment = AR.aarch32RegAssignment
+  , MSB.crucGenRegStructType = AR.aarch32RegStructType
   , MSB.crucGenArchFn = aarch32GenFn
   , MSB.crucGenArchStmt = aarch32GenStmt
   , MSB.crucGenArchTermStmt = aarch32GenTermStmt
@@ -163,120 +139,6 @@ instance CE.PrettyApp AArch32StmtExtension where
 type instance MSB.MacawArchStmtExtension SA.AArch32 =
   AArch32StmtExtension
 
--- | All of the registers tracked in the AArch32 machine code model
---
--- Note that this set is significantly larger than the user-visible
--- architectural state and includes a large number of hidden state from the ASL
--- semantics
---
--- See Note [ARM Registers]
-type RegContext = PC.MapCtx ToMacawTypeWrapper (LAG.SimpleGlobalsCtx Ctx.<+> LAG.GPRCtx Ctx.<+> LAG.SIMDCtx)
-type instance MS.ArchRegContext SA.AArch32 = RegContext
-
-data ToMacawTypeWrapper :: PC.TyFun WT.BaseType MT.Type -> Type
-type instance PC.Apply ToMacawTypeWrapper t = BaseToMacawType t
-
-aarch32RegAssignment :: Ctx.Assignment MAR.ARMReg RegContext
-aarch32RegAssignment =
-  I.runIdentity (PC.traverseMapCtx (Proxy @AsMacawReg) asARMReg (FC.fmapFC LAG.SimpleGlobalRef LAG.simpleGlobalRefs Ctx.<++> LAG.gprGlobalRefsSym Ctx.<++> LAG.simdGlobalRefsSym))
-
-data AsMacawReg :: PC.TyFun Symbol MT.Type -> Type
-type instance PC.Apply AsMacawReg s = BaseToMacawType (LAG.GlobalsType s)
-
-asARMReg :: (Monad m) => LAG.GlobalRef s -> m (MAR.ARMReg (BaseToMacawType (LAG.GlobalsType s)))
-asARMReg gr =
-  case LAG.globalRefRepr gr of
-    WT.BaseBoolRepr -> return (MAR.ARMGlobalBool gr)
-    WT.BaseBVRepr _ -> return (MAR.ARMGlobalBV gr)
-    WT.BaseStructRepr Ctx.Empty -> return MAR.ARMDummyReg
-    tp -> AP.panic AP.AArch32 "asARMReg" ["Unexpected type: " ++ show tp]
-
-type family BaseToMacawType (t :: WT.BaseType) :: MT.Type where
-  BaseToMacawType WT.BaseBoolType = MT.BoolType
-  BaseToMacawType (WT.BaseBVType n) = MT.BVType n
-  BaseToMacawType (WT.BaseStructType Ctx.EmptyCtx) = MT.TupleType '[]
-
-aarch32RegStructType :: CT.TypeRepr (MS.ArchRegStruct SA.AArch32)
-aarch32RegStructType =
-  CT.StructRepr (MS.typeCtxToCrucible (FC.fmapFC MT.typeRepr aarch32RegAssignment))
-
--- The following definitions for rN are tightly coupled to that of
--- ArchRegContext for AArch32. Unit tests in the test suite ensure that they are
--- consistent with regIndexMap (below).
-
--- | Local helper, not exported. The \"globals\" come before the GPRs in the
--- ArchRegContext.
-type GlobalsCtx = MS.CtxToCrucibleType (PC.MapCtx ToMacawTypeWrapper LAG.SimpleGlobalsCtx)
-
-type family CtxRepeat (n :: Nat) (c :: k) :: Ctx.Ctx k where
-  CtxRepeat 0 c = Ctx.EmptyCtx
-  CtxRepeat n c = CtxRepeat (n - 1) c Ctx.::> c
-
-r0 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r0 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 0 (LCLM.LLVMPointerType 32))))
-
-r1 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r1 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 1 (LCLM.LLVMPointerType 32))))
-
-r2 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r2 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 2 (LCLM.LLVMPointerType 32))))
-
-r3 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r3 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 3 (LCLM.LLVMPointerType 32))))
-
-r4 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r4 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 4 (LCLM.LLVMPointerType 32))))
-
-r5 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r5 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 5 (LCLM.LLVMPointerType 32))))
-
-r6 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r6 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 6 (LCLM.LLVMPointerType 32))))
-
-r7 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r7 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 7 (LCLM.LLVMPointerType 32))))
-
-r8 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r8 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 8 (LCLM.LLVMPointerType 32))))
-
-r9 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r9 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 9 (LCLM.LLVMPointerType 32))))
-
-r10 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r10 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 10 (LCLM.LLVMPointerType 32))))
-
--- | Frame pointer, AKA 'fp'
-r11 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r11 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 11 (LCLM.LLVMPointerType 32))))
-
--- | Frame pointer, AKA 'r11'
-fp :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-fp = r11
-
--- | Intra-procedure call scratch register, AKA 'ip'
-r12 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r12 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 12 (LCLM.LLVMPointerType 32))))
-
--- | Intra-procedure call scratch register, AKA 'r12'
-ip :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-ip = r12
-
--- | Stack pointer, AKA 'sp'
-r13 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r13 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 13 (LCLM.LLVMPointerType 32))))
-
--- | Stack pointer, AKA 'r13'
-sp :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-sp = r13
-
--- | Link register, AKA 'lr'
-r14 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-r14 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 14 (LCLM.LLVMPointerType 32))))
-
--- | Link register, AKA 'r14'
-lr :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
-lr = r14
-
 aarch32GenFn :: MAA.ARMPrimFn (MC.Value SA.AArch32 ids) tp
              -> MSB.CrucGen SA.AArch32 ids s (CR.Atom s (MS.ToCrucibleType tp))
 aarch32GenFn fn =
@@ -437,7 +299,7 @@ aarch32GenTermStmt ts regs mfallthroughLabel =
 regIndexMap :: MSB.RegIndexMap SA.AArch32
 regIndexMap = MSB.mkRegIndexMap asgn sz
   where
-    asgn = aarch32RegAssignment
+    asgn = AR.aarch32RegAssignment
     sz = Ctx.size (MS.typeCtxToCrucible (FC.fmapFC MT.typeRepr asgn))
 
 indexForReg
@@ -477,27 +339,3 @@ aarch32LookupReg :: MCR.RegEntry sym (MS.ArchRegStruct SA.AArch32)
 aarch32LookupReg regs reg =
   case lookupReg reg (MCR.regValue regs) of
     MCRV.RV val -> MCR.RegEntry (MS.typeToCrucible (MT.typeRepr reg)) val
-
-{- Note [ARM Registers]
-
-The symbolic execution (and the code discovery in macaw-aarch32) track a
-superset of the user-visible architectural state, which only includes the GPRs
-and SIMD registers.  The extended state includes low-level architectural details
-referenced by the ASL semantics.
-
-In asl-translator, the set of architectural state is referred to as the
-"tracked" registers (or allGlobalRefs).  This is state that must be maintained
-during code discovery and symbolic execution, which includes things like:
-
-- The IT state
-- Branch taken/not taken flags
-- Various flags
-
-Note that there are "untracked" state, which is architectural state referred to
-in the semantics, but that is entirely local to an instruction.  These are
-equivalent to local variables and do not appear in the post states of any
-instructions.  We do not track those in the symbolic execution because they are
-effectively inlined when we symbolically execute the ASL semantics into formulas
-for semmc.
-
--}

macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic/ABI.hs

@@ -72,7 +72,7 @@ module Data.Macaw.AArch32.Symbolic.ABI
 
 import Control.Lens qualified as Lens
 import Data.Coerce (coerce)
-import Data.Macaw.AArch32.Symbolic qualified as AArch32S
+import Data.Macaw.AArch32.Symbolic.Regs qualified as MASR
 import Data.Macaw.ARM qualified as AArch32
 import Data.Macaw.Symbolic qualified as MS
 import Data.Macaw.Symbolic.Stack qualified as MSS
@@ -99,8 +99,8 @@ stackPointerReg ::
     (StackPointer sym)
 stackPointerReg =
   Lens.lens
-    (\regs -> StackPointer (C.unRV (regs Lens.^. ixF' AArch32S.sp)))
-    (\regs v -> regs Lens.& ixF' AArch32S.sp Lens..~ C.RV (getStackPointer v))
+    (\regs -> StackPointer (C.unRV (regs Lens.^. ixF' MASR.sp)))
+    (\regs v -> regs Lens.& ixF' MASR.sp Lens..~ C.RV (getStackPointer v))
 
 -- | Align the stack pointer to a particular 'CLD.Alignment'.
 alignStackPointer ::