GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-24 22:53:43 +03:00
Code Issues Projects Releases Wiki Activity

Adding rewriting to macaw-ppc translation

Browse Source
This commit is contained in:
Ben Selfridge 2017-10-27 21:08:47 -07:00
parent 16839e30c1
commit f3f07ff099
8 changed files with 60 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
macaw-ppc/src/Data/Macaw/PPC/Disassemble.hs
View File

@ -38,6 +38,9 @@ import qualified Data.Parameterized.Nonce as NC
import Data.Macaw.PPC.Generator
import Data.Macaw.PPC.PPCReg
import Debug.Trace (trace)
import Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>))
-- | Read one instruction from the 'MM.Memory' at the given segmented offset.
--
-- Returns the instruction and number of bytes consumed /or/ an error.
@ -70,7 +73,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)
. (PPCWidth ppc, ArchConstraints ppc)
=> (Value ppc s (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc s ()))
-> MM.Memory (ArchAddrWidth ppc)
-> GenState ppc s
@ -102,6 +105,7 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
let line = printf "%s: %s" (show curIPAddr) (show (D.ppInstruction i))
addStmt (Comment (T.pack line))
transformer
simplifyCurrentBlock
genResult
case egs1 of
Left genErr -> failAt gs off curIPAddr (GenerationError i genErr)
@ -110,7 +114,7 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
Just preBlock
| Seq.null (resBlockSeq gs1 ^. frontierBlocks)
, v <- preBlock ^. (pBlockState . curIP)
, v == nextIPVal
, trace ("v = " ++ show (pretty v) ++ "\nnextIPVal = " ++ show nextIPVal ++ "\n") $ v == nextIPVal
, nextIPOffset < maxOffset
, Just nextIPSegAddr <- MM.asSegmentOff mem nextIP -> do
let gs2 = GenState { assignIdGen = assignIdGen gs
@ -121,7 +125,7 @@ disassembleBlock lookupSemantics mem gs curIPAddr maxOffset = do
disassembleBlock lookupSemantics mem gs2 nextIPSegAddr maxOffset
_ -> return (nextIPOffset, finishBlock FetchAndExecute gs1)
tryDisassembleBlock :: (PPCWidth ppc)
tryDisassembleBlock :: (PPCWidth ppc, ArchConstraints ppc)
=> (Value ppc s (BVType (ArchAddrWidth ppc)) -> D.Instruction -> Maybe (PPCGenerator ppc s ()))
-> MM.Memory (ArchAddrWidth ppc)
-> NC.NonceGenerator (ST s) s
@ -142,7 +146,7 @@ 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)
disassembleFn :: (PPCWidth ppc, ArchConstraints ppc)
=> 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

33
macaw-ppc/src/Data/Macaw/PPC/Generator.hs
View File

@ -2,6 +2,8 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
module Data.Macaw.PPC.Generator (
GenResult(..),
@ -20,6 +22,7 @@ module Data.Macaw.PPC.Generator (
addAssignment,
getReg,
getRegValue,
simplifyCurrentBlock,
-- * Lenses
blockState,
curPPCState,
@ -42,6 +45,7 @@ import Data.Word (Word64)
import Data.Macaw.CFG
import Data.Macaw.CFG.Block
import Data.Macaw.CFG.Rewriter
import qualified Data.Macaw.Memory as MM
import qualified Data.Parameterized.Map as MapF
import qualified Data.Parameterized.NatRepr as NR
@ -49,6 +53,8 @@ import qualified Data.Parameterized.Nonce as NC
import Data.Macaw.PPC.PPCReg
import Debug.Trace (trace)
-- GenResult
data GenResult ppc s =
@ -172,7 +178,7 @@ genResult = do
, resState = Just (s ^. blockState)
}
addStmt :: Stmt ppc s -> PPCGenerator ppc s ()
addStmt :: (ArchConstraints ppc) => Stmt ppc s -> PPCGenerator ppc s ()
addStmt stmt = (blockState . pBlockStmts) %= (Seq.|> stmt)
newAssignId :: PPCGenerator ppc s (AssignId s tp)
@ -184,7 +190,8 @@ newAssignId = do
liftST :: ST s a -> PPCGenerator ppc s a
liftST = PPCGenerator . lift . lift
addAssignment :: AssignRhs ppc s tp
addAssignment :: ArchConstraints ppc
=> AssignRhs ppc s tp
-> PPCGenerator ppc s (Assignment ppc s tp)
addAssignment rhs = do
l <- newAssignId
@ -203,8 +210,26 @@ getRegValue r = do
genState <- St.get
return (genState ^. blockState ^. pBlockState ^. boundValue r)
-- evalApp :: App (Value PPC s) tp -> PPCGenerator ppc s (Value PPC s tp)
-- evalApp = undefined
simplifyCurrentBlock :: forall ppc s . ArchConstraints ppc => PPCGenerator ppc s ()
simplifyCurrentBlock = do
genState <- St.get
let nonceGen = assignIdGen genState
stmts = genState ^. blockState . pBlockStmts
ctx = RewriteContext { rwctxNonceGen = nonceGen
, rwctxArchFn = undefined -- wrapArchFn nonceGen
, rwctxArchStmt = appendRewrittenArchStmt
, rwctxConstraints = withConstraints
}
(stmts', _) <- liftST $ runRewriter ctx $ do
collectRewrittenStmts $ do
mapM_ rewriteStmt stmts
blockState . pBlockStmts .= Seq.fromList stmts'
where withConstraints :: (forall a . (RegisterInfo (ArchReg ppc) => a) -> a)
withConstraints x = x
-- wrapArchFn ng archFn = do
-- name <- NC.freshNonce ng
-- return $ AssignedValue (Assignment name (EvalArchFn archFn (typeRepr archFn)))
-- eval :: Expr ppc s tp -> PPCGenerator ppc s (Value PPC s tp)
-- eval (ValueExpr v) = return v

10
macaw-ppc/src/Data/Macaw/PPC/Identify.hs
View File

@ -12,12 +12,18 @@ import qualified Data.Macaw.Memory as MM
import Data.Macaw.PPC.PPCReg
identifyCall :: proxy ppc
import Debug.Trace (trace)
import Data.List (intercalate)
identifyCall :: MC.ArchConstraints ppc
=> proxy ppc
-> MM.Memory (MC.ArchAddrWidth ppc)
-> [MC.Stmt ppc ids]
-> MC.RegState (MC.ArchReg ppc) (MC.Value ppc ids)
-> Maybe (Seq.Seq (MC.Stmt ppc ids), MC.ArchSegmentOff ppc)
identifyCall = undefined
identifyCall _ mem stmts rs = trace ("identifyCall:\n\n" ++
intercalate "\n" (map show stmts))
Nothing
identifyReturn :: (PPCWidth ppc)
=> proxy ppc

1
macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC32.hs
View File

@ -16,6 +16,7 @@ import SemMC.Architecture.PPC32.Opcodes ( allSemantics, allOpcodeInfo
import Data.Macaw.PPC.Generator
import Data.Macaw.PPC.Semantics.TH ( genExecInstruction )
import Data.Macaw.PPC.Arch
execInstruction :: MC.Value PPC s (MT.BVType 32) -> Instruction -> Maybe (PPCGenerator PPC s ())
execInstruction = $(genExecInstruction (Proxy @PPC) (C.Sub C.Dict) allSemantics allOpcodeInfo)

1
macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC64.hs
View File

@ -16,6 +16,7 @@ import SemMC.Architecture.PPC64.Opcodes ( allSemantics, allOpcodeInfo
import Data.Macaw.PPC.Generator
import Data.Macaw.PPC.Semantics.TH
import Data.Macaw.PPC.Arch
execInstruction :: MC.Value PPC s (MT.BVType 64) -> Instruction -> Maybe (PPCGenerator PPC s ())
execInstruction = $(genExecInstruction (Proxy @PPC) (C.Sub C.Dict) allSemantics allOpcodeInfo)

16
macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs
View File

@ -1,4 +1,5 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
@ -62,8 +63,8 @@ import Data.Parameterized.NatRepr ( knownNat
)
import Data.Macaw.PPC.Generator
import Data.Macaw.PPC.PPCReg
import Data.Macaw.PPC.Operand
import Data.Macaw.PPC.PPCReg
-- run stack with --ghc-options=-ddump-splices
@ -263,7 +264,7 @@ type family FromCrucibleBaseType (btp :: S.BaseType) :: M.Type where
-- Add an expression in the PPCGenerator monad. This returns a Macaw value
-- corresponding to the added expression.
addExpr :: Expr ppc ids tp -> PPCGenerator ppc ids (M.Value ppc ids tp)
addExpr :: M.ArchConstraints ppc => Expr ppc ids tp -> PPCGenerator ppc ids (M.Value ppc ids tp)
addExpr expr = do
case expr of
ValueExpr val -> return val
@ -764,7 +765,7 @@ crucAppToExprTH elt interps = case elt of
crucAppToExpr :: S.App (S.Elt t) ctp -> PPCGenerator ppc ids (Expr ppc ids (FromCrucibleBaseType ctp))
crucAppToExpr :: (M.ArchConstraints ppc) => S.App (S.Elt t) ctp -> PPCGenerator ppc ids (Expr ppc ids (FromCrucibleBaseType ctp))
crucAppToExpr S.TrueBool = return $ ValueExpr (M.BoolValue True)
crucAppToExpr S.FalseBool = return $ ValueExpr (M.BoolValue False)
crucAppToExpr (S.NotBool bool) = (AppExpr . M.NotApp) <$> addElt bool
@ -880,7 +881,8 @@ locToRegTH _ loc = [| undefined |]
-- will modify the location by the function encoded in the formula.
interpretFormula :: forall ppc t ctp s .
(1 <= APPC.ArchRegWidth ppc,
M.RegAddrWidth (PPCReg ppc) ~ APPC.ArchRegWidth ppc)
M.RegAddrWidth (PPCReg ppc) ~ APPC.ArchRegWidth ppc,
M.ArchConstraints ppc)
=> APPC.Location ppc ctp
-> S.Elt t ctp
-> PPCGenerator ppc s ()
@ -894,16 +896,16 @@ interpretFormula loc elt = do
curPPCState . M.boundValue reg .= M.AssignedValue assignment
-- Convert a Crucible element into an expression.
eltToExpr :: S.Elt t ctp -> PPCGenerator ppc ids (Expr ppc ids (FromCrucibleBaseType ctp))
eltToExpr :: M.ArchConstraints ppc => S.Elt t ctp -> PPCGenerator ppc ids (Expr ppc ids (FromCrucibleBaseType ctp))
eltToExpr (S.BVElt w val loc) = return $ ValueExpr (M.BVValue w val)
eltToExpr (S.AppElt appElt) = crucAppToExpr (S.appEltApp appElt)
eltToExpr (S.BoundVarElt sbv) = undefined
-- Add a Crucible element in the PPCGenerator monad.
addElt :: S.Elt t ctp -> PPCGenerator ppc ids (M.Value ppc ids (FromCrucibleBaseType ctp))
addElt :: M.ArchConstraints ppc => S.Elt t ctp -> PPCGenerator ppc ids (M.Value ppc ids (FromCrucibleBaseType ctp))
addElt elt = eltToExpr elt >>= addExpr
addElt' :: S.Elt t ctp -> PPCGenerator ppc ids (M.Value ppc ids (FromCrucibleBaseType ctp))
addElt' :: M.ArchConstraints ppc => S.Elt t ctp -> PPCGenerator ppc ids (M.Value ppc ids (FromCrucibleBaseType ctp))
addElt' elt = case elt of
S.BVElt w val loc -> return $ M.BVValue w val
S.AppElt appElt -> do x <- crucAppToExpr (S.appEltApp appElt)

3
macaw-ppc/tests/PPC64Tests.hs
View File

@ -93,10 +93,11 @@ testDiscovery expectedFilename elf =
let actualEntry = fromIntegral (fromJust (MM.asAbsoluteAddr (MM.relativeSegmentAddr (MD.discoveredFunAddr dfi))))
actualBlockStarts = S.fromList [ fromIntegral (fromJust (MM.asAbsoluteAddr (MM.relativeSegmentAddr (MD.pblockAddr pbr))))
| pbr <- M.elems (dfi ^. MD.parsedBlocks)
, trace (show pbr) True
]
case (S.member actualEntry ignoredBlocks, M.lookup actualEntry expectedEntries) of
(True, _) -> return ()
(_, Nothing) -> T.assertFailure (printf "Unexpected entry point: 0x%x" actualEntry)
(_, Nothing) -> T.assertFailure (printf "Unexpected block start: 0x%x" actualEntry)
(_, Just expectedBlockStarts) ->
T.assertEqual (printf "Block starts for 0x%x" actualEntry) expectedBlockStarts (actualBlockStarts `S.difference` ignoredBlocks)

4
macaw-ppc/tests/ppc/test-just-exit.s.expected
View File

@ -1,3 +1,3 @@
R { funcs = [(0x400144, [0x400144])]
, ignoreBlocks = [0x40015a]
R { funcs = [(0x10000148, [0x10000148])]
, ignoreBlocks = [0x1000015c]
}