From f3f07ff09993f58175d52164295a557dadf62fc4 Mon Sep 17 00:00:00 2001 From: Ben Selfridge Date: Fri, 27 Oct 2017 21:08:47 -0700 Subject: [PATCH] Adding rewriting to macaw-ppc translation --- macaw-ppc/src/Data/Macaw/PPC/Disassemble.hs | 12 ++++--- macaw-ppc/src/Data/Macaw/PPC/Generator.hs | 33 ++++++++++++++++--- macaw-ppc/src/Data/Macaw/PPC/Identify.hs | 10 ++++-- .../src/Data/Macaw/PPC/Semantics/PPC32.hs | 1 + .../src/Data/Macaw/PPC/Semantics/PPC64.hs | 1 + macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs | 16 +++++---- macaw-ppc/tests/PPC64Tests.hs | 3 +- macaw-ppc/tests/ppc/test-just-exit.s.expected | 4 +-- 8 files changed, 60 insertions(+), 20 deletions(-) diff --git a/macaw-ppc/src/Data/Macaw/PPC/Disassemble.hs b/macaw-ppc/src/Data/Macaw/PPC/Disassemble.hs index 13e4e1af..dd4fad43 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Disassemble.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Disassemble.hs @@ -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 diff --git a/macaw-ppc/src/Data/Macaw/PPC/Generator.hs b/macaw-ppc/src/Data/Macaw/PPC/Generator.hs index 80b961bc..92bc7d6e 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Generator.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Generator.hs @@ -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 diff --git a/macaw-ppc/src/Data/Macaw/PPC/Identify.hs b/macaw-ppc/src/Data/Macaw/PPC/Identify.hs index 3b542167..4ec42618 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Identify.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Identify.hs @@ -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 diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC32.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC32.hs index ba714aaf..5c5e7b1c 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC32.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC32.hs @@ -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) diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC64.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC64.hs index c282861b..96ff68e3 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC64.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/PPC64.hs @@ -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) diff --git a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs index 64f5b002..bfc811c4 100644 --- a/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs +++ b/macaw-ppc/src/Data/Macaw/PPC/Semantics/TH.hs @@ -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) diff --git a/macaw-ppc/tests/PPC64Tests.hs b/macaw-ppc/tests/PPC64Tests.hs index 7e4c5926..551a844c 100644 --- a/macaw-ppc/tests/PPC64Tests.hs +++ b/macaw-ppc/tests/PPC64Tests.hs @@ -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) diff --git a/macaw-ppc/tests/ppc/test-just-exit.s.expected b/macaw-ppc/tests/ppc/test-just-exit.s.expected index 9545afa6..b7654401 100644 --- a/macaw-ppc/tests/ppc/test-just-exit.s.expected +++ b/macaw-ppc/tests/ppc/test-just-exit.s.expected @@ -1,3 +1,3 @@ -R { funcs = [(0x400144, [0x400144])] - , ignoreBlocks = [0x40015a] +R { funcs = [(0x10000148, [0x10000148])] + , ignoreBlocks = [0x1000015c] } \ No newline at end of file