mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-28 08:34:23 +03:00
[macaw-ppc] ArchitecturInfo updates: mkInitialRegsForBlock, checkForReturnAddr.
This commit is contained in:
parent
f63f9972eb
commit
294299a8eb
@ -20,38 +20,42 @@ module Data.Macaw.PPC (
|
||||
A.PPCPrimFn(..),
|
||||
) where
|
||||
|
||||
import Control.Lens ( (^.) )
|
||||
import Data.Maybe
|
||||
import Data.Proxy ( Proxy(..) )
|
||||
|
||||
import qualified Data.Macaw.Architecture.Info as MI
|
||||
import qualified Data.Macaw.CFG as MC
|
||||
import qualified Data.Macaw.CFG.DemandSet as MDS
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
|
||||
import qualified SemMC.Architecture.PPC32 as PPC32
|
||||
import qualified SemMC.Architecture.PPC64 as PPC64
|
||||
|
||||
import Data.Macaw.PPC.Disassemble ( disassembleFn )
|
||||
import Data.Macaw.PPC.Eval ( mkInitialAbsState,
|
||||
absEvalArchFn,
|
||||
absEvalArchStmt,
|
||||
postCallAbsState,
|
||||
postPPCTermStmtAbsState,
|
||||
preserveRegAcrossSyscall
|
||||
)
|
||||
import Data.Macaw.PPC.Identify ( identifyCall,
|
||||
identifyReturn
|
||||
)
|
||||
import Data.Macaw.PPC.Arch ( rewriteTermStmt,
|
||||
rewriteStmt,
|
||||
rewritePrimFn,
|
||||
ppcPrimFnHasSideEffects,
|
||||
PPCArchConstraints
|
||||
)
|
||||
import qualified Data.Macaw.BinaryLoader as BL
|
||||
import qualified Data.Macaw.BinaryLoader.PPC as BLP
|
||||
import Data.Macaw.PPC.Arch ( rewriteTermStmt
|
||||
, rewriteStmt
|
||||
, rewritePrimFn
|
||||
, ppcPrimFnHasSideEffects
|
||||
, PPCArchConstraints
|
||||
)
|
||||
import qualified Data.Macaw.PPC.Arch as A
|
||||
import Data.Macaw.PPC.Disassemble ( disassembleFn, initialBlockRegs )
|
||||
import Data.Macaw.PPC.Eval ( mkInitialAbsState
|
||||
, absEvalArchFn
|
||||
, absEvalArchStmt
|
||||
, postCallAbsState
|
||||
, postPPCTermStmtAbsState
|
||||
, preserveRegAcrossSyscall
|
||||
)
|
||||
import Data.Macaw.PPC.Identify ( identifyCall
|
||||
, identifyReturn
|
||||
, matchReturn
|
||||
)
|
||||
import qualified Data.Macaw.PPC.PPCReg as R
|
||||
import qualified Data.Macaw.PPC.Semantics.PPC32 as PPC32
|
||||
import qualified Data.Macaw.PPC.Semantics.PPC64 as PPC64
|
||||
import qualified Data.Macaw.PPC.PPCReg as R
|
||||
import qualified Data.Macaw.PPC.Arch as A
|
||||
import qualified Data.Macaw.BinaryLoader.PPC as BLP
|
||||
import qualified Data.Macaw.BinaryLoader as BL
|
||||
|
||||
|
||||
-- | The type tag for 64 bit PowerPC
|
||||
@ -65,7 +69,6 @@ archDemandContext _ =
|
||||
MDS.DemandContext { MDS.demandConstraints = \a -> a
|
||||
, MDS.archFnHasSideEffects = ppcPrimFnHasSideEffects
|
||||
}
|
||||
|
||||
ppc64_linux_info :: ( BLP.HasTOC PPC64.PPC binFmt
|
||||
) =>
|
||||
BL.LoadedBinary PPC64.PPC binFmt
|
||||
@ -74,12 +77,14 @@ ppc64_linux_info binData =
|
||||
MI.ArchitectureInfo { MI.withArchConstraints = \x -> x
|
||||
, MI.archAddrWidth = MM.Addr64
|
||||
, MI.archEndianness = MM.BigEndian
|
||||
, MI.mkInitialRegsForBlock = initialBlockRegs
|
||||
, MI.disassembleFn = disassembleFn proxy PPC64.execInstruction
|
||||
, MI.mkInitialAbsState = mkInitialAbsState proxy binData
|
||||
, MI.absEvalArchFn = absEvalArchFn proxy
|
||||
, MI.absEvalArchStmt = absEvalArchStmt proxy
|
||||
, MI.postCallAbsState = postCallAbsState proxy
|
||||
, MI.identifyCall = identifyCall proxy
|
||||
, MI.checkForReturnAddr = \r s -> isJust $ matchReturn s (r ^. MC.boundValue R.PPC_LNK)
|
||||
, MI.identifyReturn = identifyReturn proxy
|
||||
, MI.rewriteArchFn = rewritePrimFn
|
||||
, MI.rewriteArchStmt = rewriteStmt
|
||||
@ -98,12 +103,14 @@ ppc32_linux_info binData =
|
||||
MI.ArchitectureInfo { MI.withArchConstraints = \x -> x
|
||||
, MI.archAddrWidth = MM.Addr32
|
||||
, MI.archEndianness = MM.BigEndian
|
||||
, MI.mkInitialRegsForBlock = initialBlockRegs
|
||||
, MI.disassembleFn = disassembleFn proxy PPC32.execInstruction
|
||||
, MI.mkInitialAbsState = mkInitialAbsState proxy binData
|
||||
, MI.absEvalArchFn = absEvalArchFn proxy
|
||||
, MI.absEvalArchStmt = absEvalArchStmt proxy
|
||||
, MI.postCallAbsState = postCallAbsState proxy
|
||||
, MI.identifyCall = identifyCall proxy
|
||||
, MI.checkForReturnAddr = \r s -> isJust $ matchReturn s (r ^. MC.boundValue R.PPC_LNK)
|
||||
, MI.identifyReturn = identifyReturn proxy
|
||||
, MI.rewriteArchFn = rewritePrimFn
|
||||
, MI.rewriteArchStmt = rewriteStmt
|
||||
|
@ -8,7 +8,11 @@
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
{-# LANGUAGE TypeSynonymInstances #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
module Data.Macaw.PPC.Disassemble ( disassembleFn ) where
|
||||
module Data.Macaw.PPC.Disassemble
|
||||
( disassembleFn
|
||||
, initialBlockRegs
|
||||
)
|
||||
where
|
||||
|
||||
import Control.Lens ( (&), (^.), (%~), (.~) )
|
||||
import Control.Monad ( unless )
|
||||
@ -189,10 +193,11 @@ tryDisassembleBlock :: (PPCArchConstraints ppc)
|
||||
=> (Value ppc ids (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (Generator ppc ids s ()))
|
||||
-> NC.NonceGenerator (ST s) ids
|
||||
-> ArchSegmentOff ppc
|
||||
-> (RegState (ArchReg ppc) (Value ppc ids))
|
||||
-> Int
|
||||
-> DisM ppc ids s ([Block ppc ids], Int)
|
||||
tryDisassembleBlock lookupSemantics nonceGen startAddr maxSize = do
|
||||
let gs0 = initGenState nonceGen startAddr (initRegState startAddr)
|
||||
tryDisassembleBlock lookupSemantics nonceGen startAddr regState maxSize = do
|
||||
let gs0 = initGenState nonceGen startAddr regState
|
||||
let startOffset = MM.segoffOffset startAddr
|
||||
(nextIPOffset, blocks) <- disassembleBlock lookupSemantics gs0 startAddr 0 (startOffset + fromIntegral maxSize)
|
||||
unless (nextIPOffset > startOffset) $ do
|
||||
@ -215,18 +220,31 @@ disassembleFn :: (PPCArchConstraints ppc)
|
||||
-- ^ A generator of unique IDs used for assignments
|
||||
-> ArchSegmentOff ppc
|
||||
-- ^ The address to disassemble from
|
||||
-> (RegState (ArchReg ppc) (Value ppc ids))
|
||||
-- ^ The initial registers
|
||||
-> Int
|
||||
-- ^ Maximum size of the block (a safeguard)
|
||||
-> MA.AbsBlockState (ArchReg ppc)
|
||||
-- ^ Abstract state of the processor at the start of the block
|
||||
-> ST s ([Block ppc ids], Int, Maybe String)
|
||||
disassembleFn _ lookupSemantics nonceGen startAddr maxSize _ = do
|
||||
mr <- ET.runExceptT (unDisM (tryDisassembleBlock lookupSemantics nonceGen startAddr maxSize))
|
||||
disassembleFn _ lookupSemantics nonceGen startAddr regState maxSize = do
|
||||
mr <- ET.runExceptT (unDisM (tryDisassembleBlock lookupSemantics nonceGen startAddr regState maxSize))
|
||||
case mr of
|
||||
Left (blocks, off, exn) -> return (blocks, off, Just (show exn))
|
||||
Right (blocks, bytes) -> return (blocks, bytes, Nothing)
|
||||
|
||||
|
||||
initialBlockRegs :: forall ids ppc . PPCArchConstraints ppc =>
|
||||
ArchSegmentOff ppc
|
||||
-- ^ The address of the block
|
||||
-> MA.AbsBlockState (ArchReg ppc)
|
||||
-- ^ Abstract state of the processor at the start of the block
|
||||
-> Either String (RegState (ArchReg ppc) (Value ppc ids))
|
||||
-- ^ Error or initial register state for the block
|
||||
initialBlockRegs blkAddr _abState = pure $ initRegState blkAddr
|
||||
|
||||
|
||||
type LocatedError ppc ids = ([Block ppc ids], Int, TranslationError (ArchAddrWidth ppc))
|
||||
|
||||
|
||||
-- | This is a monad for error handling during disassembly
|
||||
--
|
||||
-- It allows for early failure that reports progress (in the form of blocks
|
||||
|
@ -1,9 +1,11 @@
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
module Data.Macaw.PPC.Identify (
|
||||
identifyCall,
|
||||
identifyReturn
|
||||
) where
|
||||
module Data.Macaw.PPC.Identify
|
||||
( identifyCall
|
||||
, identifyReturn
|
||||
, matchReturn
|
||||
)
|
||||
where
|
||||
|
||||
import Control.Lens ( (^.) )
|
||||
import Control.Monad ( guard )
|
||||
@ -30,7 +32,7 @@ import Data.Macaw.PPC.PPCReg
|
||||
identifyCall :: (PPCArchConstraints ppc)
|
||||
=> proxy ppc
|
||||
-> MM.Memory (MC.ArchAddrWidth ppc)
|
||||
-> [MC.Stmt ppc ids]
|
||||
-> Seq.Seq (MC.Stmt ppc ids)
|
||||
-> MC.RegState (MC.ArchReg ppc) (MC.Value ppc ids)
|
||||
-> Maybe (Seq.Seq (MC.Stmt ppc ids), MC.ArchSegmentOff ppc)
|
||||
identifyCall _ mem stmts0 rs
|
||||
@ -39,7 +41,7 @@ identifyCall _ mem stmts0 rs
|
||||
, Just retVal <- simplifyValue (rs ^. MC.boundValue PPC_LNK)
|
||||
, Just retAddrVal <- MC.valueAsMemAddr retVal
|
||||
, Just retAddr <- MM.asSegmentOff mem retAddrVal =
|
||||
Just (Seq.fromList stmts0, retAddr)
|
||||
Just (stmts0, retAddr)
|
||||
| otherwise = Nothing
|
||||
|
||||
|
||||
@ -51,13 +53,13 @@ identifyCall _ mem stmts0 rs
|
||||
-- 'mkInitialAbsState') into the instruction pointer.
|
||||
identifyReturn :: (PPCArchConstraints ppc) =>
|
||||
proxy ppc
|
||||
-> [MC.Stmt ppc ids]
|
||||
-> Seq.Seq (MC.Stmt ppc ids)
|
||||
-> MC.RegState (MC.ArchReg ppc) (MC.Value ppc ids)
|
||||
-> MA.AbsProcessorState (MC.ArchReg ppc) ids
|
||||
-> Maybe (Seq.Seq (MC.Stmt ppc ids))
|
||||
identifyReturn _ stmts regState absState = do
|
||||
Some MA.ReturnAddr <- matchReturn absState (regState ^. MC.boundValue MC.ip_reg)
|
||||
return (Seq.fromList stmts)
|
||||
return stmts
|
||||
|
||||
matchReturn :: (PPCArchConstraints ppc, MC.ArchReg ppc ~ PPCReg ppc)
|
||||
=> MA.AbsProcessorState (MC.ArchReg ppc) ids
|
||||
|
Loading…
Reference in New Issue
Block a user