diff --git a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs index 0f9b2946..186705cc 100644 --- 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 index 837a23e9..f3a75c59 100644 --- 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" $