Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

aarch32-symbolic: Named Indexes into ArchRegContext AArch32 #438

Merged
merged 2 commits into from
Sep 20, 2024
Merged

aarch32-symbolic: Named Indexes into ArchRegContext AArch32 #438

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
549a263
aarch32-symbolic: Named `Index`es into `ArchRegContext AArch32`
Sep 20, 2024
cf1c302
aarch32-symbolic: Additional register aliases, a bit of commentary
Sep 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
82 changes: 82 additions & 0 deletions macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,23 @@ module Data.Macaw.AArch32.Symbolic (
, lookupReg
, updateReg
, AF.AArch32Exception(..)
, r0
, r1
, r2
, r3
, r4
, r5
, r6
, r7
, r8
, r9
, r10
, r11
, r12
, r13
, sp
, r14
, lr
) where

import qualified Data.Text as T
Expand Down Expand Up @@ -181,6 +198,71 @@ 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).

type GlobalsCtx = MS.CtxToCrucibleType (PC.MapCtx ToMacawTypeWrapper LAG.SimpleGlobalsCtx)
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved

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
Comment on lines +211 to +213
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should mention this in #410.


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))))

r11 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
r11 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 11 (LCLM.LLVMPointerType 32))))
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved

r12 :: Ctx.Index (MS.MacawCrucibleRegTypes SA.AArch32) (LCLM.LLVMPointerType 32)
r12 = Ctx.extendIndex (Ctx.nextIndex (Ctx.knownSize @_ @(GlobalsCtx Ctx.<+> CtxRepeat 12 (LCLM.LLVMPointerType 32))))
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved

-- | 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))))
langston-barrett marked this conversation as resolved.
Show resolved Hide resolved

-- | 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 =
Expand Down
46 changes: 40 additions & 6 deletions macaw-aarch32-symbolic/tests/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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(..) )
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -85,11 +98,32 @@ 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 "r12" $ getRegName MAS.r12 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 "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
Expand Down
Loading