mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-24 00:42:28 +03:00
Consolidated constraints into one: PPCArchConstraints
This commit is contained in:
parent
7dd2a2a385
commit
eff3fa6425
@ -39,16 +39,15 @@ import Data.Macaw.PPC.Arch ( rewriteTermStmt,
|
||||
rewritePrimFn,
|
||||
valuesInPPCStmt,
|
||||
ppcPrimFnHasSideEffects,
|
||||
PPCArch
|
||||
PPCArchConstraints
|
||||
)
|
||||
import Data.Macaw.PPC.PPCReg ( PPCWidth )
|
||||
import qualified Data.Macaw.PPC.Semantics.PPC32 as PPC32
|
||||
import qualified Data.Macaw.PPC.Semantics.PPC64 as PPC64
|
||||
|
||||
addValueListDemands :: [Some (Value ppc ids)] -> MDS.DemandComp ppc ids ()
|
||||
addValueListDemands = mapM_ (viewSome MDS.addValueDemands)
|
||||
|
||||
archDemandContext :: (PPCArch ppc) => proxy ppc -> MDS.DemandContext ppc ids
|
||||
archDemandContext :: (PPCArchConstraints ppc) => proxy ppc -> MDS.DemandContext ppc ids
|
||||
archDemandContext _ =
|
||||
MDS.DemandContext { MDS.addArchStmtDemands = addValueListDemands . valuesInPPCStmt
|
||||
, MDS.addArchFnDemands = addValueListDemands . FC.foldMapFC (\v -> [ Some v ])
|
||||
@ -57,7 +56,7 @@ archDemandContext _ =
|
||||
|
||||
-- | NOTE: There isn't necessarily one answer for this. This will need to turn
|
||||
-- into a function. With PIC jump tables, it can be smaller than the native size.
|
||||
jumpTableEntrySize :: (PPCWidth ppc) => proxy ppc -> MM.MemWord (ArchAddrWidth ppc)
|
||||
jumpTableEntrySize :: (PPCArchConstraints ppc) => proxy ppc -> MM.MemWord (ArchAddrWidth ppc)
|
||||
jumpTableEntrySize _ = 4
|
||||
|
||||
ppc64_linux_info :: MI.ArchitectureInfo PPC64.PPC
|
||||
|
@ -8,6 +8,7 @@
|
||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Data.Macaw.PPC.Arch (
|
||||
PPCTermStmt(..),
|
||||
rewriteTermStmt,
|
||||
@ -18,17 +19,23 @@ module Data.Macaw.PPC.Arch (
|
||||
rewritePrimFn,
|
||||
ppcPrimFnHasSideEffects,
|
||||
PPCArchStmt,
|
||||
PPCArch
|
||||
-- PPCArch,
|
||||
PPCArchConstraints
|
||||
) where
|
||||
|
||||
import GHC.TypeLits
|
||||
|
||||
import qualified Text.PrettyPrint.ANSI.Leijen as PP
|
||||
import qualified Data.Parameterized.TraversableFC as FC
|
||||
import qualified Data.Parameterized.TraversableF as TF
|
||||
import Data.Parameterized.Some ( Some(..) )
|
||||
import qualified Data.Macaw.CFG as MC
|
||||
import Data.Macaw.CFG.Rewriter ( Rewriter, rewriteValue, evalRewrittenArchFn )
|
||||
import Data.Macaw.CFG.Block ( Block )
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
import qualified Data.Macaw.Types as MT
|
||||
|
||||
import qualified Dismantle.PPC as D
|
||||
import qualified SemMC.Architecture.PPC32 as PPC32
|
||||
import qualified SemMC.Architecture.PPC64 as PPC64
|
||||
|
||||
@ -106,7 +113,7 @@ ppcPrimFnHasSideEffects pf =
|
||||
case pf of
|
||||
IDiv {} -> False
|
||||
|
||||
rewritePrimFn :: (PPCWidth ppc, MC.ArchFn ppc ~ PPCPrimFn ppc)
|
||||
rewritePrimFn :: (PPCArchConstraints ppc, MC.ArchFn ppc ~ PPCPrimFn ppc)
|
||||
=> PPCPrimFn ppc (MC.Value ppc src) tp
|
||||
-> Rewriter ppc src tgt (MC.Value ppc tgt tp)
|
||||
rewritePrimFn f =
|
||||
@ -140,8 +147,38 @@ type instance MC.ArchFn PPC32.PPC = PPCPrimFn PPC32.PPC
|
||||
valuesInPPCStmt :: PPCArchStmt ppc ids -> [Some (MC.Value ppc ids)]
|
||||
valuesInPPCStmt (PPCArchStmt s) = TF.foldMapF (\x -> [Some x]) s
|
||||
|
||||
type PPCArch ppc = ( MC.ArchTermStmt ppc ~ PPCTermStmt
|
||||
, PPCWidth ppc
|
||||
, MC.ArchStmt ppc ~ PPCArchStmt ppc
|
||||
, MC.ArchFn ppc ~ PPCPrimFn ppc
|
||||
)
|
||||
type PPCArchConstraints ppc = ( MC.ArchReg ppc ~ PPCReg ppc
|
||||
, MC.ArchFn ppc ~ PPCPrimFn ppc
|
||||
, MC.ArchStmt ppc ~ PPCArchStmt ppc
|
||||
, MC.ArchTermStmt ppc ~ PPCTermStmt
|
||||
, ArchWidth ppc
|
||||
, MM.MemWidth (MC.RegAddrWidth (MC.ArchReg ppc))
|
||||
, 1 <= MC.RegAddrWidth (PPCReg ppc)
|
||||
, KnownNat (MC.RegAddrWidth (PPCReg ppc))
|
||||
, MC.ArchConstraints ppc
|
||||
)
|
||||
|
||||
-- type PPCWidth ppc = (ArchWidth ppc,
|
||||
-- MC.ArchReg ppc ~ PPCReg ppc,
|
||||
-- MM.MemWidth (MC.RegAddrWidth (MC.ArchReg ppc)),
|
||||
-- 1 <= MC.RegAddrWidth (PPCReg ppc),
|
||||
-- KnownNat (MC.RegAddrWidth (PPCReg ppc)))
|
||||
|
||||
-- instance ( PPCWidth ppc ) => MC.RegisterInfo (PPCReg ppc) where
|
||||
-- archRegs = ppcRegs
|
||||
-- sp_reg = PPC_GP (D.GPR 1)
|
||||
-- ip_reg = PPC_IP
|
||||
-- syscall_num_reg = PPC_GP (D.GPR 0)
|
||||
-- syscallArgumentRegs = [ PPC_GP (D.GPR rnum) | rnum <- [3..10] ]
|
||||
|
||||
-- instance ( ArchWidth ppc
|
||||
-- , MC.ArchReg ppc ~ PPCReg ppc
|
||||
-- , MM.MemWidth (MC.RegAddrWidth (MC.ArchReg ppc))
|
||||
-- , 1 <= MC.RegAddrWidth (PPCReg ppc)
|
||||
-- , KnownNat (MC.RegAddrWidth (PPCReg ppc))
|
||||
-- ) => MC.RegisterInfo (PPCReg ppc) where
|
||||
-- archRegs = ppcRegs
|
||||
-- sp_reg = PPC_GP (D.GPR 1)
|
||||
-- ip_reg = PPC_IP
|
||||
-- syscall_num_reg = PPC_GP (D.GPR 0)
|
||||
-- syscallArgumentRegs = [ PPC_GP (D.GPR rnum) | rnum <- [3..10] ]
|
||||
|
@ -74,7 +74,7 @@ readInstruction mem addr = MM.addrWidthClass (MM.memAddrWidth mem) $ do
|
||||
Nothing -> ET.throwError (MM.InvalidInstruction (MM.relativeSegmentAddr addr) contents)
|
||||
|
||||
disassembleBlock :: forall ppc s
|
||||
. (PPCWidth ppc, PPCArchConstraints ppc s)
|
||||
. PPCArchConstraints ppc
|
||||
=> (Value ppc s (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc s ()))
|
||||
-> MM.Memory (ArchAddrWidth ppc)
|
||||
-> GenState ppc s
|
||||
@ -103,8 +103,8 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
|
||||
-- state transformer), we apply the state transformer and then extract
|
||||
-- a result from the state of the 'PPCGenerator'.
|
||||
egs1 <- liftST $ evalGenerator gs $ do
|
||||
let line = printf "%s: %s" (show curIPAddr) (show (D.ppInstruction i))
|
||||
addStmt (Comment (T.pack line))
|
||||
let lineStr = printf "%s: %s" (show curIPAddr) (show (D.ppInstruction i))
|
||||
addStmt (Comment (T.pack lineStr))
|
||||
transformer
|
||||
genResult
|
||||
case egs1 of
|
||||
@ -133,7 +133,7 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
|
||||
--
|
||||
-- The full rewriter is too heavyweight here, as it produces new bound values
|
||||
-- instead of fully reducing the calculation we want to a literal.
|
||||
simplifyValue :: (PPCWidth ppc, PPCArchConstraints ppc s) => Value ppc s (BVType (ArchAddrWidth ppc)) -> Maybe (Value ppc s (BVType (ArchAddrWidth ppc)))
|
||||
simplifyValue :: PPCArchConstraints ppc => Value ppc s (BVType (ArchAddrWidth ppc)) -> Maybe (Value ppc s (BVType (ArchAddrWidth ppc)))
|
||||
simplifyValue v =
|
||||
case v of
|
||||
BVValue {} -> Just v
|
||||
@ -145,7 +145,9 @@ simplifyValue v =
|
||||
Just (RelocatableValue rep (MM.incAddr v1 addr))
|
||||
_ -> Nothing
|
||||
|
||||
tryDisassembleBlock :: (PPCWidth ppc, PPCArchConstraints ppc s)
|
||||
tryDisassembleBlock :: ( PPCArchConstraints ppc
|
||||
, Show (Block ppc s)
|
||||
, Show (BlockSeq ppc s))
|
||||
=> (Value ppc s (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc s ()))
|
||||
-> MM.Memory (ArchAddrWidth ppc)
|
||||
-> NC.NonceGenerator (ST s) s
|
||||
@ -166,7 +168,9 @@ tryDisassembleBlock lookupSemantics mem nonceGen startAddr maxSize = do
|
||||
--
|
||||
-- Return a list of disassembled blocks as well as the total number of bytes
|
||||
-- occupied by those blocks.
|
||||
disassembleFn :: (PPCWidth ppc, PPCArchConstraints ppc s)
|
||||
disassembleFn :: ( PPCArchConstraints ppc
|
||||
, Show (Block ppc s)
|
||||
, Show (BlockSeq ppc s))
|
||||
=> proxy ppc
|
||||
-> (Value ppc s (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc s ()))
|
||||
-- ^ A function to look up the semantics for an instruction. The
|
||||
|
@ -31,7 +31,7 @@ preserveRegAcrossSyscall :: (ArchReg ppc ~ PPCReg ppc, 1 <= RegAddrWidth (PPCReg
|
||||
-> Bool
|
||||
preserveRegAcrossSyscall proxy r = S.member (Some r) (linuxSystemCallPreservedRegisters proxy)
|
||||
|
||||
postPPCTermStmtAbsState :: (PPCArch ppc)
|
||||
postPPCTermStmtAbsState :: (PPCArchConstraints ppc)
|
||||
=> (forall tp . PPCReg ppc tp -> Bool)
|
||||
-> AbsBlockState (PPCReg ppc)
|
||||
-> PPCTermStmt ids
|
||||
@ -58,7 +58,7 @@ postPPCTermStmtAbsState preservePred s0 stmt nextIP =
|
||||
--
|
||||
-- One value that is definitely set is the link register, which holds the
|
||||
-- abstract return value.
|
||||
mkInitialAbsState :: (PPCWidth ppc)
|
||||
mkInitialAbsState :: (PPCArchConstraints ppc)
|
||||
=> proxy ppc
|
||||
-> MM.Memory (RegAddrWidth (ArchReg ppc))
|
||||
-> ArchSegmentOff ppc
|
||||
@ -67,7 +67,7 @@ mkInitialAbsState _ _mem startAddr =
|
||||
MA.top & MA.setAbsIP startAddr
|
||||
& MA.absRegState . boundValue PPC_LNK .~ MA.ReturnAddr
|
||||
|
||||
absEvalArchFn :: (PPCArch ppc)
|
||||
absEvalArchFn :: (PPCArchConstraints ppc)
|
||||
=> proxy ppc
|
||||
-> AbsProcessorState (ArchReg ppc) ids
|
||||
-> ArchFn ppc (Value ppc ids) tp
|
||||
@ -87,7 +87,7 @@ absEvalArchStmt _ s _ = s
|
||||
-- | 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)
|
||||
postCallAbsState :: (PPCArchConstraints ppc)
|
||||
=> proxy ppc
|
||||
-> AbsBlockState (ArchReg ppc)
|
||||
-> ArchSegmentOff ppc
|
||||
|
@ -42,7 +42,6 @@ import GHC.TypeLits
|
||||
import Control.Monad (forM_)
|
||||
import Debug.Trace
|
||||
import Control.Lens
|
||||
import Data.Parameterized.TraversableFC
|
||||
import qualified Control.Monad.Except as ET
|
||||
import Control.Monad.ST ( ST )
|
||||
import Control.Monad.Trans ( lift )
|
||||
@ -59,9 +58,11 @@ import qualified Data.Parameterized.NatRepr as NR
|
||||
import qualified Data.Parameterized.Nonce as NC
|
||||
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
import Data.Macaw.PPC.Arch (rewritePrimFn, PPCPrimFn, PPCArch, PPCArchStmt)
|
||||
|
||||
import Debug.Trace (trace)
|
||||
import Data.Macaw.PPC.Arch ( rewritePrimFn
|
||||
, PPCPrimFn
|
||||
-- , PPCArch
|
||||
, PPCArchConstraints
|
||||
, PPCArchStmt)
|
||||
|
||||
-- GenResult
|
||||
|
||||
@ -80,19 +81,19 @@ data Expr ppc s tp where
|
||||
------------------------------------------------------------------------
|
||||
-- BlockSeq
|
||||
data BlockSeq ppc s = BlockSeq
|
||||
{ _nextBlockID :: !Word64
|
||||
{ nextBlockID :: !Word64
|
||||
-- ^ index of next block
|
||||
, _frontierBlocks :: !(Seq.Seq (Block ppc s))
|
||||
-- ^ Blocks added to CFG
|
||||
}
|
||||
|
||||
deriving instance Show (Block ppc s) => Show (BlockSeq ppc s)
|
||||
deriving instance (PPCWidth ppc, PPCArch ppc) => Show (Block ppc s)
|
||||
deriving instance (PPCWidth ppc, PPCArch ppc) => Show (TermStmt ppc s)
|
||||
deriving instance (PPCArchConstraints ppc) => Show (Block ppc s)
|
||||
deriving instance (PPCArchConstraints ppc) => Show (TermStmt ppc s)
|
||||
|
||||
-- | Control flow blocs generated so far.
|
||||
nextBlockID :: Simple Lens (BlockSeq ppc s) Word64
|
||||
nextBlockID = lens _nextBlockID (\s v -> s { _nextBlockID = v })
|
||||
-- nextBlockID :: Simple Lens (BlockSeq ppc s) Word64
|
||||
-- nextBlockID = lens _nextBlockID (\s v -> s { _nextBlockID = v })
|
||||
|
||||
-- | Blocks that are not in CFG that end with a FetchAndExecute,
|
||||
-- which we need to analyze to compute new potential branch targets.
|
||||
@ -132,12 +133,16 @@ initGenState :: NC.NonceGenerator (ST s) s
|
||||
-> GenState ppc s
|
||||
initGenState nonceGen addr st =
|
||||
GenState { assignIdGen = nonceGen
|
||||
, blockSeq = BlockSeq { _nextBlockID = 0, _frontierBlocks = Seq.empty }
|
||||
, blockSeq = BlockSeq { nextBlockID = 0, _frontierBlocks = Seq.empty }
|
||||
, _blockState = emptyPreBlock st 0 addr
|
||||
, genAddr = addr
|
||||
}
|
||||
|
||||
initRegState :: (KnownNat (RegAddrWidth (PPCReg ppc)), ArchReg ppc ~ PPCReg ppc, 1 <= RegAddrWidth (PPCReg ppc), MM.MemWidth (RegAddrWidth (PPCReg ppc)), ArchWidth ppc)
|
||||
initRegState :: ( KnownNat (RegAddrWidth (PPCReg ppc))
|
||||
, ArchReg ppc ~ PPCReg ppc
|
||||
, 1 <= RegAddrWidth (PPCReg ppc)
|
||||
, MM.MemWidth (RegAddrWidth (PPCReg ppc))
|
||||
, ArchWidth ppc)
|
||||
=> ArchSegmentOff ppc
|
||||
-> RegState (PPCReg ppc) (Value ppc s)
|
||||
initRegState startIP = mkRegState Initial
|
||||
@ -222,18 +227,8 @@ getRegValue r = do
|
||||
genState <- St.get
|
||||
return (genState ^. blockState ^. pBlockState ^. boundValue r)
|
||||
|
||||
type PPCArchConstraints ppc s = ( ArchReg ppc ~ PPCReg ppc
|
||||
, ArchFn ppc ~ PPCPrimFn ppc
|
||||
, ArchStmt ppc ~ PPCArchStmt ppc
|
||||
, ArchWidth ppc
|
||||
, KnownNat (RegAddrWidth (PPCReg ppc))
|
||||
, Show (Block ppc s)
|
||||
, Show (BlockSeq ppc s)
|
||||
, ArchConstraints ppc
|
||||
)
|
||||
|
||||
simplifyCurrentBlock
|
||||
:: forall ppc s . PPCArchConstraints ppc s => PPCGenerator ppc s ()
|
||||
:: forall ppc s . PPCArchConstraints ppc => PPCGenerator ppc s ()
|
||||
simplifyCurrentBlock = do
|
||||
genState <- St.get
|
||||
let nonceGen = assignIdGen genState
|
||||
@ -254,24 +249,3 @@ simplifyCurrentBlock = do
|
||||
-- eval :: Expr ppc s tp -> PPCGenerator ppc s (Value PPC s tp)
|
||||
-- eval (ValueExpr v) = return v
|
||||
-- eval (AppExpr a) = evalAp =<< traverseFC eval a
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
@ -11,6 +11,7 @@ import qualified Data.Macaw.CFG as MC
|
||||
import qualified Data.Macaw.Memory as MM
|
||||
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
import Data.Macaw.PPC.Arch
|
||||
|
||||
import Debug.Trace (trace)
|
||||
import Data.List (intercalate)
|
||||
@ -25,7 +26,7 @@ identifyCall _ mem stmts rs = trace ("identifyCall:\n\n" ++
|
||||
intercalate "\n" (map show stmts))
|
||||
Nothing
|
||||
|
||||
identifyReturn :: (PPCWidth ppc)
|
||||
identifyReturn :: (PPCArchConstraints ppc)
|
||||
=> proxy ppc
|
||||
-> [MC.Stmt ppc ids]
|
||||
-> MC.RegState (MC.ArchReg ppc) (MC.Value ppc ids)
|
||||
|
@ -24,7 +24,6 @@ import qualified Data.Word.Indexed as W
|
||||
import qualified Data.Int.Indexed as I
|
||||
import qualified Dismantle.PPC as D
|
||||
|
||||
import qualified SemMC.Architecture.PPC.Location as L
|
||||
import qualified SemMC.Architecture.PPC32 as PPC32
|
||||
import qualified SemMC.Architecture.PPC64 as PPC64
|
||||
import qualified Data.Macaw.PPC.PPCReg as R
|
||||
|
@ -114,13 +114,14 @@ instance (ArchWidth ppc) => HasRepr (PPCReg ppc) TypeRepr where
|
||||
PPC_CR -> BVTypeRepr n32
|
||||
PPC_XER -> BVTypeRepr (pointerNatRepr (Proxy @ppc))
|
||||
|
||||
type PPCWidth ppc = (ArchWidth ppc,
|
||||
MC.ArchReg ppc ~ PPCReg ppc,
|
||||
MM.MemWidth (MC.RegAddrWidth (MC.ArchReg ppc)),
|
||||
1 <= MC.RegAddrWidth (PPCReg ppc),
|
||||
KnownNat (MC.RegAddrWidth (PPCReg ppc)))
|
||||
type PPCWidth ppc = ()
|
||||
|
||||
instance (PPCWidth ppc) => MC.RegisterInfo (PPCReg ppc) where
|
||||
instance ( ArchWidth ppc
|
||||
, MC.ArchReg ppc ~ PPCReg ppc
|
||||
, MM.MemWidth (MC.RegAddrWidth (MC.ArchReg ppc))
|
||||
, 1 <= MC.RegAddrWidth (PPCReg ppc)
|
||||
, KnownNat (MC.RegAddrWidth (PPCReg ppc)))
|
||||
=> MC.RegisterInfo (PPCReg ppc) where
|
||||
archRegs = ppcRegs
|
||||
sp_reg = PPC_GP (D.GPR 1)
|
||||
ip_reg = PPC_IP
|
||||
|
Loading…
Reference in New Issue
Block a user