aarch32-symbolic: Additional register aliases, a bit of commentary

GaloisInc · Sep 20, 2024 · cf1c302 · cf1c302
1 parent 549a263
commit cf1c302
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 1 deletion.
diff --git a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs
@@ -26,7 +26,9 @@ module Data.Macaw.AArch32.Symbolic (
   , r9
   , r10
   , r11
+  , fp
   , r12
+  , ip
   , r13
   , sp
   , r14
@@ -202,6 +204,8 @@ aarch32RegStructType =
 -- 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
@@ -241,12 +245,22 @@ r9 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRe
 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))))

diff --git a/macaw-aarch32-symbolic/tests/Main.hs b/macaw-aarch32-symbolic/tests/Main.hs
@@ -112,10 +112,12 @@ main = do
         , 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 "r14" $ getRegName MAS.r14 TTH.@?= "zenc!rznzuR14"
         , 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" $