From edbcee34946788472469626d46a6deddd429a2f6 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 20 Sep 2024 15:59:52 -0400 Subject: [PATCH] aarch32-symbolic: Named `Index`es 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. --- .../src/Data/Macaw/AArch32/Symbolic.hs | 96 +++++++++++++++++++ macaw-aarch32-symbolic/tests/Main.hs | 48 ++++++++-- 2 files changed, 138 insertions(+), 6 deletions(-) diff --git a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs index 90c86e96..186705cc 100644 --- a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs +++ b/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 = diff --git a/macaw-aarch32-symbolic/tests/Main.hs b/macaw-aarch32-symbolic/tests/Main.hs index ca86be36..f3a75c59 100644 --- a/macaw-aarch32-symbolic/tests/Main.hs +++ b/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