diff --git a/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal b/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal index d0c93d2f..0fbe5f8b 100644 --- a/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal +++ b/macaw-aarch32-symbolic/macaw-aarch32-symbolic.cabal @@ -42,6 +42,7 @@ library semmc-aarch32, macaw-aarch32, macaw-symbolic + hs-source-dirs: src default-language: Haskell2010 ghc-options: -Wall -Wcompat diff --git a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs index aad320b9..8920730e 100644 --- a/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs +++ b/macaw-aarch32-symbolic/src/Data/Macaw/AArch32/Symbolic.hs @@ -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 = @@ -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 diff --git a/macaw-aarch32/src/Data/Macaw/ARM/Arch.hs b/macaw-aarch32/src/Data/Macaw/ARM/Arch.hs index fdf9ddf2..372196e1 100644 --- a/macaw-aarch32/src/Data/Macaw/ARM/Arch.hs +++ b/macaw-aarch32/src/Data/Macaw/ARM/Arch.hs @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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