Skip to content

Expose more regs in syscall ARM #545

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

Draft
2over12 wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

Expose more regs in syscall ARM #545

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
27e10e0
start exposing regs up through r14
2over12 Oct 25, 2025
16ff538
fix up regs
2over12 Oct 26, 2025
1e8442a
fix gen function
2over12 Oct 27, 2025
260e8db
try a different way of doing stubs
2over12 Oct 30, 2025
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
1 change: 1 addition & 0 deletions macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ library
semmc-aarch32,
macaw-aarch32,
macaw-symbolic

hs-source-dirs: src
default-language: Haskell2010
ghc-options: -Wall -Wcompat
Expand Down
22 changes: 9 additions & 13 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 @@ -56,6 +56,7 @@ import qualified Data.Macaw.AArch32.Symbolic.AtomWrapper as AA
import qualified Data.Macaw.AArch32.Symbolic.Functions as AF
import qualified Data.Macaw.AArch32.Symbolic.Panic as AP
import qualified Data.Macaw.AArch32.Symbolic.Regs as AR
import Data.Macaw.Symbolic (ArchRegContext)

aarch32MacawSymbolicFns :: MS.MacawSymbolicArchFunctions SA.AArch32
aarch32MacawSymbolicFns =
Expand Down Expand Up @@ -139,28 +140,23 @@ instance CE.PrettyApp AArch32StmtExtension where
type instance MSB.MacawArchStmtExtension SA.AArch32 =
AArch32StmtExtension

massageRegs :: MapF.MapF MAR.ARMReg (MC.Value SA.AArch32 ids) -> Ctx.Assignment (MC.Value SA.AArch32 ids) (ArchRegContext SA.AArch32)
massageRegs = undefined

aarch32GenFn :: MAA.ARMPrimFn (MC.Value SA.AArch32 ids) tp
-> MSB.CrucGen SA.AArch32 ids s (CR.Atom s (MS.ToCrucibleType tp))
aarch32GenFn fn =
case fn of
MAA.ARMSyscall _imm v0 v1 v2 v3 v4 v5 v6 v7 -> do
a0 <- MSB.valueToCrucible v0
a1 <- MSB.valueToCrucible v1
a2 <- MSB.valueToCrucible v2
a3 <- MSB.valueToCrucible v3
a4 <- MSB.valueToCrucible v4
a5 <- MSB.valueToCrucible v5
a6 <- MSB.valueToCrucible v6
a7 <- MSB.valueToCrucible v7

let syscallArgs = Ctx.Empty Ctx.:> a0 Ctx.:> a1 Ctx.:> a2 Ctx.:> a3 Ctx.:> a4 Ctx.:> a5 Ctx.:> a6 Ctx.:> a7
MAA.ARMSyscall _imm regMap -> do
let rassign = massageRegs regMap
crucibleAssign <- MS.macawAssignToCrucM MSB.valueToCrucible rassign
let argTypes = PC.knownRepr
let retTypes = Ctx.Empty Ctx.:> LCLM.LLVMPointerRepr (PN.knownNat @32) Ctx.:> LCLM.LLVMPointerRepr (PN.knownNat @32)
let retRepr = CT.StructRepr retTypes
syscallArgStructAtom <- MSB.evalAtom (CR.EvalApp (LCE.MkStruct argTypes syscallArgs))
syscallArgStructAtom <- MSB.evalAtom (CR.EvalApp (LCE.MkStruct argTypes crucibleAssign))
let lookupHdlStmt = MS.MacawLookupSyscallHandle argTypes retTypes syscallArgStructAtom
hdlAtom <- MSB.evalMacawStmt lookupHdlStmt
MSB.evalAtom $! CR.Call hdlAtom syscallArgs retRepr
MSB.evalAtom $! CR.Call hdlAtom crucibleAssign retRepr
_ -> do
let f x = AA.AtomWrapper <$> MSB.valueToCrucible x
r <- FC.traverseFC f fn
Expand Down
45 changes: 14 additions & 31 deletions macaw-aarch32/src/Data/Macaw/ARM/Arch.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ import GHC.TypeLits
import qualified Language.ASL.Globals as ASL
import qualified Prettyprinter as PP
import qualified SemMC.Architecture.AArch32 as ARM
import qualified Data.Parameterized.Map as MapF

-- ----------------------------------------------------------------------
-- ARM-specific statement definitions
Expand Down Expand Up @@ -188,14 +189,7 @@ data ARMPrimFn (f :: MT.Type -> Type) tp where
--
-- The system call can return up to two values (in r0 and r1)
ARMSyscall :: WI.W 24
-> f (MT.BVType 32) -- r0
-> f (MT.BVType 32) -- r1
-> f (MT.BVType 32) -- r2
-> f (MT.BVType 32) -- r3
-> f (MT.BVType 32) -- r4
-> f (MT.BVType 32) -- r5
-> f (MT.BVType 32) -- r6
-> f (MT.BVType 32) -- r7 (syscall number)
-> MapF.MapF ARMReg.ARMReg f
-> ARMPrimFn f (MT.TupleType [MT.BVType 32, MT.BVType 32])

-- | Signed division at @w@ bits. Both operands are treated as signed. The
Expand Down Expand Up @@ -386,10 +380,12 @@ instance MC.IsArchFn ARMPrimFn where
let ppUnary s v' = s PP.<+> v'
ppBinary s v1' v2' = s PP.<+> v1' PP.<+> v2'
ppTernary s v1' v2' v3' = s PP.<+> v1' PP.<+> v2' PP.<+> v3'
ppSC s imm r0 r1 r2 r3 r4 r5 r6 r7 = s PP.<+> PP.viaShow imm PP.<+> r0 PP.<+> r1 PP.<+> r2 PP.<+> r3 PP.<+> r4 PP.<+> r5 PP.<+> r6 PP.<+> r7
ppSC s imm rMapDoc = s PP.<+> PP.viaShow imm PP.<+> rMapDoc
in case f of
ARMSyscall imm r0 r1 r2 r3 r4 r5 r6 r7 ->
ppSC "arm_syscall" imm <$> pp r0 <*> pp r1 <*> pp r2 <*> pp r3 <*> pp r4 <*> pp r5 <*> pp r6 <*> pp r7
ARMSyscall imm rMap ->
let lst = TF.toListF pp rMap
regArgs = PP.cat <$> sequenceA lst in
ppSC "arm_syscall" imm <$> regArgs
UDiv _ lhs rhs -> ppBinary "arm_udiv" <$> pp lhs <*> pp rhs
SDiv _ lhs rhs -> ppBinary "arm_sdiv" <$> pp lhs <*> pp rhs
URem _ lhs rhs -> ppBinary "arm_urem" <$> pp lhs <*> pp rhs
Expand Down Expand Up @@ -429,8 +425,9 @@ instance FCls.FoldableFC ARMPrimFn where
instance FCls.TraversableFC ARMPrimFn where
traverseFC go f =
case f of
ARMSyscall imm r0 r1 r2 r3 r4 r5 r6 r7 ->
ARMSyscall imm <$> go r0 <*> go r1 <*> go r2 <*> go r3 <*> go r4 <*> go r5 <*> go r6 <*> go r7
ARMSyscall imm rMap ->
let x = TF.traverseF go rMap in
ARMSyscall imm <$> x
UDiv rep lhs rhs -> UDiv rep <$> go lhs <*> go rhs
SDiv rep lhs rhs -> SDiv rep <$> go lhs <*> go rhs
URem rep lhs rhs -> URem rep <$> go lhs <*> go rhs
Expand Down Expand Up @@ -560,8 +557,8 @@ rewritePrimFn :: ARMPrimFn (MC.Value ARM.AArch32 src) tp
-> Rewriter ARM.AArch32 s src tgt (MC.Value ARM.AArch32 tgt tp)
rewritePrimFn f =
case f of
ARMSyscall imm r0 r1 r2 r3 r4 r5 r6 r7 -> do
tgtFn <- ARMSyscall imm <$> rewriteValue r0 <*> rewriteValue r1 <*> rewriteValue r2 <*> rewriteValue r3 <*> rewriteValue r4 <*> rewriteValue r5 <*> rewriteValue r6 <*> rewriteValue r7
ARMSyscall imm rMap -> do
tgtFn <- ARMSyscall imm <$> TF.traverseF rewriteValue rMap
evalRewrittenArchFn tgtFn
UDiv rep lhs rhs -> do
tgtFn <- UDiv rep <$> rewriteValue lhs <*> rewriteValue rhs
Expand Down Expand Up @@ -652,14 +649,7 @@ a32InstructionMatcher (ARMDis.Instruction opc operands) =
ARMDis.SVC_A1 ->
case operands of
ARMDis.Bv4 _opPred ARMDis.:< ARMDis.Bv24 imm ARMDis.:< ARMDis.Nil -> Just $ do
sc <- ARMSyscall imm <$> G.getRegVal ARMReg.r0
<*> G.getRegVal ARMReg.r1
<*> G.getRegVal ARMReg.r2
<*> G.getRegVal ARMReg.r3
<*> G.getRegVal ARMReg.r4
<*> G.getRegVal ARMReg.r5
<*> G.getRegVal ARMReg.r6
<*> G.getRegVal ARMReg.r7
sc <- ARMSyscall imm . MC.regStateMap <$> G.getRegs
res <- G.addExpr =<< evalArchFn sc
-- res is a tuple of form (R1, R0). This is reversed from the
-- user provided return Assignment of empty :> R0 :> R1 because
Expand Down Expand Up @@ -706,14 +696,7 @@ t32InstructionMatcher (ThumbDis.Instruction opc operands) =
-- so we can just zero extend the immediate value and use the same
-- syscall representation in macaw
let imm24 = zeroExtend imm8 (NR.knownNat @24)
sc <- ARMSyscall imm24 <$> G.getRegVal ARMReg.r0
<*> G.getRegVal ARMReg.r1
<*> G.getRegVal ARMReg.r2
<*> G.getRegVal ARMReg.r3
<*> G.getRegVal ARMReg.r4
<*> G.getRegVal ARMReg.r5
<*> G.getRegVal ARMReg.r6
<*> G.getRegVal ARMReg.r7
sc <- ARMSyscall imm24 . MC.regStateMap <$> G.getRegs
res <- G.addExpr =<< evalArchFn sc
-- res is a tuple of form (R1, R0). This is reversed from the
-- user provided return Assignment of empty :> R0 :> R1 because
Expand Down
Loading