mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-24 08:53:12 +03:00
Modify genExecInstruction to use functions for opcode semantics bodies.
Pass operand and architecture types and instead of case opcode of ADD -> case operands of Just GPR gpr0 :< Nil of -> SSA-semantics Generate: let opc_ADD operands = case operands of Just GPR gpr0 :< Nil of -> SSA-semantics in case opcode of ADD -> opc_ADD operand This provides better encapsulation for the individual operands and more specific control over the types (at the cost of a pair of additional type specifications in the call). This also seems to reduce memory consumption by about half.
This commit is contained in:
parent
334b799dd8
commit
a3fe4a0f6b
@ -21,4 +21,11 @@ import Data.Macaw.PPC.PPCReg ( locToRegTH )
|
||||
import Data.Macaw.PPC.Semantics.TH ( ppcAppEvaluator, ppcNonceAppEval )
|
||||
|
||||
execInstruction :: MC.Value PPC ids (MT.BVType 32) -> Instruction -> Maybe (Generator PPC ids s ())
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (locToRegTH (Proxy @PPC)) ppcNonceAppEval ppcAppEvaluator 'ppcInstructionMatcher allSemantics allOpcodeInfo)
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (locToRegTH (Proxy @PPC))
|
||||
ppcNonceAppEval
|
||||
ppcAppEvaluator
|
||||
'ppcInstructionMatcher
|
||||
allSemantics allOpcodeInfo
|
||||
([t| Dismantle.PPC.Operand |], [t| PPC |])
|
||||
)
|
||||
|
||||
|
@ -21,4 +21,5 @@ import Data.Macaw.PPC.PPCReg ( locToRegTH )
|
||||
import Data.Macaw.PPC.Semantics.TH ( ppcAppEvaluator, ppcNonceAppEval )
|
||||
|
||||
execInstruction :: MC.Value PPC ids (MT.BVType 64) -> Instruction -> Maybe (Generator PPC ids s ())
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (locToRegTH (Proxy @PPC)) ppcNonceAppEval ppcAppEvaluator 'ppcInstructionMatcher allSemantics allOpcodeInfo)
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (locToRegTH (Proxy @PPC)) ppcNonceAppEval ppcAppEvaluator 'ppcInstructionMatcher allSemantics allOpcodeInfo
|
||||
([t| Dismantle.PPC.Operand |], [t| PPC |]))
|
||||
|
@ -37,6 +37,7 @@ import qualified Control.Concurrent.Async as Async
|
||||
import qualified Data.Functor.Const as C
|
||||
import Data.Proxy ( Proxy(..) )
|
||||
import qualified Data.List as L
|
||||
import Data.Semigroup
|
||||
import qualified Data.Text as T
|
||||
import Language.Haskell.TH
|
||||
import Language.Haskell.TH.Syntax
|
||||
@ -102,25 +103,54 @@ instructionMatcher :: (OrdF a, LF.LiftF a, A.Architecture arch)
|
||||
-- ^ The name of the architecture-specific instruction
|
||||
-- matcher to run before falling back to the generic one
|
||||
-> Map.MapF a (PairF (ParameterizedFormula (Sym t) arch) (DT.CaptureInfo a))
|
||||
-> (Q Type, Q Type)
|
||||
-> Q Exp
|
||||
instructionMatcher ltr ena ae archSpecificMatcher formulas = do
|
||||
instructionMatcher ltr ena ae archSpecificMatcher formulas operandResultType = do
|
||||
ipVarName <- newName "ipVal"
|
||||
opcodeVar <- newName "opcode"
|
||||
operandListVar <- newName "operands"
|
||||
let normalCases = map (mkSemanticsCase ltr ena ae ipVarName operandListVar) (Map.toList formulas)
|
||||
let fallthroughCase = match wildP (normalB [| error ("Unimplemented instruction: " ++ show $(varE opcodeVar)) |]) []
|
||||
let allCases = concat [ normalCases
|
||||
(normalCases, bodyDefs) <- unzip <$> mapM (mkSemanticsCase ltr ena ae ipVarName operandListVar operandResultType) (Map.toList formulas)
|
||||
(fallthruNm, unimp) <- unimplementedInstruction
|
||||
fallthroughCase <- match wildP (normalB (appE (varE fallthruNm) (varE opcodeVar))) []
|
||||
let allCases :: [Match]
|
||||
allCases = concat [ normalCases
|
||||
, [fallthroughCase]
|
||||
]
|
||||
[| \ $(varP ipVarName) i@(D.Instruction $(varP opcodeVar) $(varP operandListVar)) ->
|
||||
case $(varE archSpecificMatcher) i of
|
||||
Just action -> Just action
|
||||
Nothing -> $(caseE (varE opcodeVar) allCases)
|
||||
|]
|
||||
instrVar <- newName "i"
|
||||
instrArg <- asP instrVar [p| D.Instruction $(varP opcodeVar) $(varP operandListVar) |]
|
||||
matcherRes <- appE (varE archSpecificMatcher) (varE instrVar)
|
||||
actionVar <- newName "action"
|
||||
let instrCase = LetE (unimp : fullDefs) $ CaseE (VarE opcodeVar) allCases
|
||||
fullDefs = concatMap (\(t,i) -> [t,i]) bodyDefs
|
||||
return $ LamE [(VarP ipVarName), instrArg] $
|
||||
CaseE matcherRes
|
||||
[ Match (ConP 'Just [VarP actionVar])
|
||||
(NormalB $ AppE (ConE 'Just) (VarE actionVar)) []
|
||||
, Match (ConP 'Nothing [])
|
||||
(NormalB instrCase) []
|
||||
]
|
||||
|
||||
|
||||
unimplementedInstruction :: Q (Name, Dec)
|
||||
unimplementedInstruction = do
|
||||
fname <- newName "noMatch"
|
||||
arg1Nm <- newName "unknownOpcode"
|
||||
fdecl <- funD fname
|
||||
[clause [varP arg1Nm]
|
||||
(normalB [| error ("Unimplemented instruction: " ++ show $(varE arg1Nm)) |])
|
||||
[]]
|
||||
return (fname, fdecl)
|
||||
|
||||
|
||||
-- | Generate a single case for one opcode of the case expression.
|
||||
-- Generates two parts: the case match, which calls a function to
|
||||
-- handle the match, and the function definition for handling the
|
||||
-- match (inlining the function body would create a more complicated
|
||||
-- case expression which makes GHC much slower).
|
||||
--
|
||||
-- > ADD4 -> ${BODY}
|
||||
-- > ADD4 -> bodyfun operands
|
||||
-- >
|
||||
-- > bodyfun operands = ${BODY}
|
||||
--
|
||||
-- where the ${BODY} is generated by 'mkOperandListCase'
|
||||
mkSemanticsCase :: (LF.LiftF a, A.Architecture arch)
|
||||
@ -129,10 +159,26 @@ mkSemanticsCase :: (LF.LiftF a, A.Architecture arch)
|
||||
-> (forall tp . BoundVarInterpretations arch t -> S.App (S.Elt t) tp -> Maybe (MacawQ arch t Exp))
|
||||
-> Name
|
||||
-> Name
|
||||
-> (Q Type, Q Type)
|
||||
-> Map.Pair a (PairF (ParameterizedFormula (Sym t) arch) (DT.CaptureInfo a))
|
||||
-> MatchQ
|
||||
mkSemanticsCase ltr ena ae ipVarName operandListVar (Map.Pair opc (PairF semantics capInfo)) =
|
||||
match (conP (DT.capturedOpcodeName capInfo) []) (normalB (mkOperandListCase ltr ena ae ipVarName operandListVar opc semantics capInfo)) []
|
||||
-> Q (Match, (Dec, Dec))
|
||||
mkSemanticsCase ltr ena ae ipVarName operandListVar operandResultType (Map.Pair opc (PairF semantics capInfo)) =
|
||||
do arg1Nm <- newName "operands"
|
||||
ofname <- newName $ "opc_" <> (filter ((/=) '"') $ nameBase $ DT.capturedOpcodeName capInfo)
|
||||
lTypeVar <- newName "l"
|
||||
idsTypeVar <- newName "ids"
|
||||
sTypeVar <- newName "s"
|
||||
ofsig <- sigD ofname [t| SL.List $(fst operandResultType) $(varT lTypeVar)
|
||||
-> Maybe (G.Generator $(snd operandResultType)
|
||||
$(varT idsTypeVar)
|
||||
$(varT sTypeVar) ()) |]
|
||||
ofdef <- funD ofname
|
||||
[clause [varP arg1Nm]
|
||||
(normalB (mkOperandListCase ltr ena ae ipVarName arg1Nm opc semantics capInfo))
|
||||
[]]
|
||||
mtch <- match (conP (DT.capturedOpcodeName capInfo) []) (normalB (appE (varE ofname) (varE operandListVar))) []
|
||||
return (mtch, (ofsig, ofdef))
|
||||
|
||||
|
||||
-- | For each opcode case, we have a sub-case expression to destructure the
|
||||
-- operand list into names that we can reference. This generates an expression
|
||||
@ -274,10 +320,11 @@ genExecInstruction :: forall arch (a :: [Symbol] -> *) (proxy :: * -> *)
|
||||
-- ^ Extra information for each opcode to let us generate
|
||||
-- some TH to match them. This comes from the semantics
|
||||
-- definitions in semmc.
|
||||
-> (Q Type, Q Type)
|
||||
-> Q Exp
|
||||
genExecInstruction _ ltr ena ae archInsnMatcher semantics captureInfo = do
|
||||
genExecInstruction _ ltr ena ae archInsnMatcher semantics captureInfo operandResultType = do
|
||||
logCfg <- runIO $ U.mkNonLogCfg
|
||||
r <- genExecInstructionLogging (Proxy @arch) ltr ena ae archInsnMatcher semantics captureInfo logCfg
|
||||
r <- genExecInstructionLogging (Proxy @arch) ltr ena ae archInsnMatcher semantics captureInfo operandResultType logCfg
|
||||
runIO $ U.logEndWith logCfg
|
||||
return r
|
||||
|
||||
@ -317,11 +364,12 @@ genExecInstructionLogStdErr :: forall arch (a :: [Symbol] -> *) (proxy :: * -> *
|
||||
-- ^ Extra information for each opcode to let us generate
|
||||
-- some TH to match them. This comes from the semantics
|
||||
-- definitions in semmc.
|
||||
-> (Q Type, Q Type)
|
||||
-> Q Exp
|
||||
genExecInstructionLogStdErr _ ltr ena ae archInsnMatcher semantics captureInfo = do
|
||||
genExecInstructionLogStdErr _ ltr ena ae archInsnMatcher semantics captureInfo operandResultType = do
|
||||
logCfg <- runIO $ U.mkLogCfg "genExecInstruction"
|
||||
logThread <- runIO $ U.asyncLinked (U.stdErrLogEventConsumer (const True) logCfg)
|
||||
r <- genExecInstructionLogging (Proxy @arch) ltr ena ae archInsnMatcher semantics captureInfo logCfg
|
||||
r <- genExecInstructionLogging (Proxy @arch) ltr ena ae archInsnMatcher semantics captureInfo operandResultType logCfg
|
||||
runIO $ U.logEndWith logCfg
|
||||
runIO $ Async.wait logThread
|
||||
return r
|
||||
@ -368,19 +416,20 @@ genExecInstructionLogging :: forall arch (a :: [Symbol] -> *) (proxy :: * -> *)
|
||||
-- ^ Extra information for each opcode to let us generate
|
||||
-- some TH to match them. This comes from the semantics
|
||||
-- definitions in semmc.
|
||||
-> (Q Type, Q Type)
|
||||
-> U.LogCfg
|
||||
-- ^ Logging configuration (explicit rather than
|
||||
-- the typical implicit expression because I don't
|
||||
-- know how to pass implicits to TH splices
|
||||
-- invocations.
|
||||
-> Q Exp
|
||||
genExecInstructionLogging _ ltr ena ae archInsnMatcher semantics captureInfo logcfg =
|
||||
genExecInstructionLogging _ ltr ena ae archInsnMatcher semantics captureInfo operandResultType logcfg =
|
||||
U.withLogCfg logcfg $ do
|
||||
Some ng <- runIO PN.newIONonceGenerator
|
||||
sym <- runIO (S.newSimpleBackend ng)
|
||||
formulas <- runIO (loadFormulas sym semantics)
|
||||
let formulasWithInfo = foldr (attachInfo formulas) Map.empty captureInfo
|
||||
instructionMatcher ltr ena ae archInsnMatcher formulasWithInfo
|
||||
instructionMatcher ltr ena ae archInsnMatcher formulasWithInfo operandResultType
|
||||
where
|
||||
attachInfo m0 (Some ci) m =
|
||||
let co = DT.capturedOpcode ci
|
||||
|
Loading…
Reference in New Issue
Block a user