aarch32-symbolic: Named Indexes into ArchRegContext AArch32 (#438)

... like the ones for x86_64. These will help in development of a
concrete syntax for macaw-symbolic-aarch32, and can be helpful when
setting up or interpreting the results from symbolic execution.

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

@@ -14,6 +14,25 @@ module Data.Macaw.AArch32.Symbolic (
   , 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
@@ -181,6 +200,83 @@ 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 =

macaw-aarch32-symbolic/tests/Main.hs

@@ -16,6 +16,7 @@ import qualified Data.Foldable as F
 import qualified Data.Map as Map
 import           Data.Maybe ( mapMaybe )
 import qualified Data.Parameterized.Classes as PC
+import qualified Data.Parameterized.Context as Ctx
 import qualified Data.Parameterized.Nonce as PN
 import           Data.Parameterized.Some ( Some(..) )
 import           Data.Proxy ( Proxy(..) )
@@ -31,7 +32,7 @@ import qualified Test.Tasty.Runners as TTR
 import qualified Language.ASL.Globals as ASL
 import qualified Data.Macaw.Architecture.Info as MAI
 
-import           Data.Macaw.AArch32.Symbolic ()
+import qualified Data.Macaw.AArch32.Symbolic as MAS
 import qualified Data.Macaw.ARM as MA
 import qualified Data.Macaw.ARM.ARMReg as MAR
 import qualified Data.Macaw.CFG as MC
@@ -73,6 +74,18 @@ ingredients = TT.includingOptions [ TTO.Option (Proxy @SaveSMT)
                                   , TTO.Option (Proxy @SaveMacaw)
                                   ] : TT.defaultIngredients
 
+getRegName ::
+  Ctx.Index (MS.MacawCrucibleRegTypes MA.ARM) t ->
+  String
+getRegName reg =
+  case Ctx.intIndex (Ctx.indexVal reg) (Ctx.size regs) of
+    Just (Some i) ->
+      let r = regs Ctx.! i
+          rName = MS.crucGenArchRegName MAS.aarch32MacawSymbolicFns r
+      in show rName
+    Nothing -> error "impossible"
+  where regs = MS.crucGenRegAssignment MAS.aarch32MacawSymbolicFns
+
 main :: IO ()
 main = do
   -- These are pass/fail in that the assertions in the "pass" set are true (and
@@ -85,11 +98,34 @@ main = do
   let passTests mmPreset = TT.testGroup "True assertions" (map (mkSymExTest passRes mmPreset) passTestFilePaths)
   let failTests mmPreset = TT.testGroup "False assertions" (map (mkSymExTest failRes mmPreset) failTestFilePaths)
   TT.defaultMainWithIngredients ingredients $
-    TT.testGroup "Binary Tests" $
-    map (\mmPreset ->
-          TT.testGroup (MST.describeMemModelPreset mmPreset)
-                       [passTests mmPreset, failTests mmPreset])
-        [MST.DefaultMemModel, MST.LazyMemModel]
+    TT.testGroup "macaw-aarch32-symbolic tests"
+    [ TT.testGroup "Unit tests" 
+        [ TTH.testCase "r0" $ getRegName MAS.r0 TTH.@?= "zenc!rznzuR0"
+        , TTH.testCase "r1" $ getRegName MAS.r1 TTH.@?= "zenc!rznzuR1"
+        , TTH.testCase "r2" $ getRegName MAS.r2 TTH.@?= "zenc!rznzuR2"
+        , TTH.testCase "r3" $ getRegName MAS.r3 TTH.@?= "zenc!rznzuR3"
+        , TTH.testCase "r4" $ getRegName MAS.r4 TTH.@?= "zenc!rznzuR4"
+        , TTH.testCase "r5" $ getRegName MAS.r5 TTH.@?= "zenc!rznzuR5"
+        , TTH.testCase "r6" $ getRegName MAS.r6 TTH.@?= "zenc!rznzuR6"
+        , TTH.testCase "r7" $ getRegName MAS.r7 TTH.@?= "zenc!rznzuR7"
+        , TTH.testCase "r8" $ getRegName MAS.r8 TTH.@?= "zenc!rznzuR8"
+        , TTH.testCase "r9" $ getRegName MAS.r9 TTH.@?= "zenc!rznzuR9"
+        , TTH.testCase "r10" $ getRegName MAS.r10 TTH.@?= "zenc!rznzuR10"
+        , TTH.testCase "r11" $ getRegName MAS.r11 TTH.@?= "zenc!rznzuR11"
+        , TTH.testCase "fp" $ getRegName MAS.fp TTH.@?= "zenc!rznzuR11"
+        , TTH.testCase "r12" $ getRegName MAS.r12 TTH.@?= "zenc!rznzuR12"
+        , TTH.testCase "ip" $ getRegName MAS.ip TTH.@?= "zenc!rznzuR12"
+        , TTH.testCase "r13" $ getRegName MAS.r13 TTH.@?= "zenc!rznzuR13"
+        , TTH.testCase "sp" $ getRegName MAS.sp TTH.@?= "zenc!rznzuR13"
+        , TTH.testCase "r14" $ getRegName MAS.r14 TTH.@?= "zenc!rznzuR14"
+        , TTH.testCase "lr" $ getRegName MAS.lr TTH.@?= "zenc!rznzuR14"
+        ]
+    , TT.testGroup "Binary Tests" $
+        map (\mmPreset ->
+              TT.testGroup (MST.describeMemModelPreset mmPreset)
+                           [passTests mmPreset, failTests mmPreset])
+            [MST.DefaultMemModel, MST.LazyMemModel]
+    ]
 
 hasTestPrefix :: Some (M.DiscoveryFunInfo arch) -> Maybe (BS8.ByteString, Some (M.DiscoveryFunInfo arch))
 hasTestPrefix (Some dfi) = do