mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-18 11:31:35 +03:00
Implement postCallAbsState and absEvalArchStmt
absEvalArchStmt is trivial (for now)
This commit is contained in:
parent
ac776b7340
commit
711eabc058
@ -59,8 +59,16 @@ absEvalArchStmt :: proxy ppc
|
|||||||
-> AbsProcessorState (ArchReg ppc) ids
|
-> AbsProcessorState (ArchReg ppc) ids
|
||||||
absEvalArchStmt _ s _ = s
|
absEvalArchStmt _ s _ = s
|
||||||
|
|
||||||
postCallAbsState :: proxy ppc
|
-- | There should be no difference in stack height before and after a call, as
|
||||||
|
-- the callee pushes the return address if required. Return values are also
|
||||||
|
-- passed in registers.
|
||||||
|
postCallAbsState :: (PPCWidth ppc)
|
||||||
|
=> proxy ppc
|
||||||
-> AbsBlockState (ArchReg ppc)
|
-> AbsBlockState (ArchReg ppc)
|
||||||
-> ArchSegmentOff ppc
|
-> ArchSegmentOff ppc
|
||||||
-> AbsBlockState (ArchReg ppc)
|
-> AbsBlockState (ArchReg ppc)
|
||||||
postCallAbsState = undefined
|
postCallAbsState proxy = MA.absEvalCall params
|
||||||
|
where
|
||||||
|
params = MA.CallParams { MA.postCallStackDelta = 0
|
||||||
|
, MA.preserveReg = \r -> S.member (Some r) (linuxCalleeSaveRegisters proxy)
|
||||||
|
}
|
||||||
|
@ -13,6 +13,7 @@
|
|||||||
module Data.Macaw.PPC.PPCReg (
|
module Data.Macaw.PPC.PPCReg (
|
||||||
PPCReg(..),
|
PPCReg(..),
|
||||||
linuxSystemCallPreservedRegisters,
|
linuxSystemCallPreservedRegisters,
|
||||||
|
linuxCalleeSaveRegisters,
|
||||||
PPCWidth,
|
PPCWidth,
|
||||||
ArchWidth(..)
|
ArchWidth(..)
|
||||||
) where
|
) where
|
||||||
@ -77,6 +78,12 @@ linuxSystemCallPreservedRegisters :: (w ~ MC.RegAddrWidth (PPCReg ppc), 1 <= w)
|
|||||||
linuxSystemCallPreservedRegisters _ =
|
linuxSystemCallPreservedRegisters _ =
|
||||||
S.fromList [ Some (PPC_GP (D.GPR rnum)) | rnum <- [14..31] ]
|
S.fromList [ Some (PPC_GP (D.GPR rnum)) | rnum <- [14..31] ]
|
||||||
|
|
||||||
|
linuxCalleeSaveRegisters :: (w ~ MC.RegAddrWidth (PPCReg ppc), 1 <= w)
|
||||||
|
=> proxy ppc
|
||||||
|
-> S.Set (Some (PPCReg ppc))
|
||||||
|
linuxCalleeSaveRegisters _ =
|
||||||
|
S.fromList [ Some (PPC_GP (D.GPR rnum)) | rnum <- [14..31] ]
|
||||||
|
|
||||||
type instance MC.RegAddrWidth (PPCReg PPC32.PPC) = 32
|
type instance MC.RegAddrWidth (PPCReg PPC32.PPC) = 32
|
||||||
type instance MC.RegAddrWidth (PPCReg PPC64.PPC) = 64
|
type instance MC.RegAddrWidth (PPCReg PPC64.PPC) = 64
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user