mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-24 14:42:23 +03:00
merging
This commit is contained in:
commit
50884f8af8
@ -28,6 +28,7 @@ import Data.Macaw.PPC.Eval ( mkInitialAbsState,
|
||||
absEvalArchFn,
|
||||
absEvalArchStmt,
|
||||
postCallAbsState,
|
||||
postPPCTermStmtAbsState,
|
||||
preserveRegAcrossSyscall
|
||||
)
|
||||
import Data.Macaw.PPC.Identify ( identifyCall,
|
||||
@ -66,7 +67,6 @@ ppc64_linux_info =
|
||||
, MI.archEndianness = MM.BigEndian
|
||||
, MI.jumpTableEntrySize = jumpTableEntrySize proxy
|
||||
, MI.disassembleFn = disassembleFn proxy PPC64.execInstruction
|
||||
, MI.preserveRegAcrossSyscall = preserveRegAcrossSyscall proxy
|
||||
, MI.mkInitialAbsState = mkInitialAbsState proxy
|
||||
, MI.absEvalArchFn = absEvalArchFn proxy
|
||||
, MI.absEvalArchStmt = absEvalArchStmt proxy
|
||||
@ -77,6 +77,7 @@ ppc64_linux_info =
|
||||
, MI.rewriteArchStmt = rewriteStmt
|
||||
, MI.rewriteArchTermStmt = rewriteTermStmt
|
||||
, MI.archDemandContext = archDemandContext proxy
|
||||
, MI.postArchTermStmtAbsState = postPPCTermStmtAbsState (preserveRegAcrossSyscall proxy)
|
||||
}
|
||||
where
|
||||
proxy = Proxy @PPC64.PPC
|
||||
@ -88,7 +89,6 @@ ppc32_linux_info =
|
||||
, MI.archEndianness = MM.BigEndian
|
||||
, MI.jumpTableEntrySize = jumpTableEntrySize proxy
|
||||
, MI.disassembleFn = disassembleFn proxy PPC32.execInstruction
|
||||
, MI.preserveRegAcrossSyscall = preserveRegAcrossSyscall proxy
|
||||
, MI.mkInitialAbsState = mkInitialAbsState proxy
|
||||
, MI.absEvalArchFn = absEvalArchFn proxy
|
||||
, MI.absEvalArchStmt = absEvalArchStmt proxy
|
||||
@ -99,6 +99,7 @@ ppc32_linux_info =
|
||||
, MI.rewriteArchStmt = rewriteStmt
|
||||
, MI.rewriteArchTermStmt = rewriteTermStmt
|
||||
, MI.archDemandContext = archDemandContext proxy
|
||||
, MI.postArchTermStmtAbsState = postPPCTermStmtAbsState (preserveRegAcrossSyscall proxy)
|
||||
}
|
||||
where
|
||||
proxy = Proxy @PPC32.PPC
|
||||
|
@ -1,12 +1,14 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Data.Macaw.PPC.Eval (
|
||||
mkInitialAbsState,
|
||||
absEvalArchFn,
|
||||
absEvalArchStmt,
|
||||
postCallAbsState,
|
||||
postPPCTermStmtAbsState,
|
||||
preserveRegAcrossSyscall
|
||||
) where
|
||||
|
||||
@ -29,6 +31,21 @@ preserveRegAcrossSyscall :: (ArchReg ppc ~ PPCReg ppc, 1 <= RegAddrWidth (PPCReg
|
||||
-> Bool
|
||||
preserveRegAcrossSyscall proxy r = S.member (Some r) (linuxSystemCallPreservedRegisters proxy)
|
||||
|
||||
postPPCTermStmtAbsState :: (PPCArch ppc)
|
||||
=> (forall tp . PPCReg ppc tp -> Bool)
|
||||
-> AbsBlockState (PPCReg ppc)
|
||||
-> PPCTermStmt ids
|
||||
-> MM.MemSegmentOff (RegAddrWidth (ArchReg ppc))
|
||||
-> AbsBlockState (PPCReg ppc)
|
||||
postPPCTermStmtAbsState preservePred s0 stmt nextIP =
|
||||
case stmt of
|
||||
PPCSyscall ->
|
||||
let params = MA.CallParams { MA.postCallStackDelta = 0
|
||||
, MA.preserveReg = preservePred
|
||||
}
|
||||
in MA.absEvalCall params s0 nextIP
|
||||
PPCTrap -> error "Trap isn't handled in the postPPCTermStmtAbsState function yet"
|
||||
|
||||
-- | Set up an initial abstract state that holds at the beginning of a basic
|
||||
-- block.
|
||||
--
|
||||
|
@ -1,4 +1,5 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
module Data.Macaw.PPC.Semantics.PPC32
|
||||
@ -7,14 +8,14 @@ module Data.Macaw.PPC.Semantics.PPC32
|
||||
|
||||
import qualified Data.Constraint as C
|
||||
import Data.Proxy ( Proxy(..) )
|
||||
import qualified Dismantle.PPC as D
|
||||
import Dismantle.PPC
|
||||
import qualified Data.Macaw.CFG as MC
|
||||
import qualified Data.Macaw.Types as MT
|
||||
import SemMC.Architecture.PPC32 ( PPC )
|
||||
import SemMC.Architecture.PPC32.Opcodes ( allSemantics )
|
||||
import SemMC.Architecture.PPC32.Opcodes ( allSemantics, allOpcodeInfo )
|
||||
|
||||
import Data.Macaw.PPC.Generator
|
||||
import Data.Macaw.PPC.Semantics.TH ( genExecInstruction )
|
||||
|
||||
execInstruction :: MC.Value PPC s (MT.BVType 32) -> D.Instruction -> Maybe (PPCGenerator PPC s ())
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (C.Sub C.Dict) allSemantics)
|
||||
execInstruction :: MC.Value PPC s (MT.BVType 32) -> Instruction -> Maybe (PPCGenerator PPC s ())
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (C.Sub C.Dict) allSemantics allOpcodeInfo)
|
||||
|
@ -1,4 +1,5 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
module Data.Macaw.PPC.Semantics.PPC64
|
||||
@ -7,14 +8,14 @@ module Data.Macaw.PPC.Semantics.PPC64
|
||||
|
||||
import qualified Data.Constraint as C
|
||||
import Data.Proxy ( Proxy(..) )
|
||||
import qualified Dismantle.PPC as D
|
||||
import Dismantle.PPC
|
||||
import qualified Data.Macaw.CFG as MC
|
||||
import qualified Data.Macaw.Types as MT
|
||||
import SemMC.Architecture.PPC64 ( PPC )
|
||||
import SemMC.Architecture.PPC64.Opcodes ( allSemantics )
|
||||
import SemMC.Architecture.PPC64.Opcodes ( allSemantics, allOpcodeInfo )
|
||||
|
||||
import Data.Macaw.PPC.Generator
|
||||
import Data.Macaw.PPC.Semantics.TH
|
||||
|
||||
execInstruction :: MC.Value PPC s (MT.BVType 64) -> D.Instruction -> Maybe (PPCGenerator PPC s ())
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (C.Sub C.Dict) allSemantics)
|
||||
execInstruction :: MC.Value PPC s (MT.BVType 64) -> Instruction -> Maybe (PPCGenerator PPC s ())
|
||||
execInstruction = $(genExecInstruction (Proxy @PPC) (C.Sub C.Dict) allSemantics allOpcodeInfo)
|
||||
|
@ -1,6 +1,7 @@
|
||||
{-# LANGUAGE DataKinds #-}
|
||||
{-# LANGUAGE GADTs #-}
|
||||
{-# LANGUAGE KindSignatures #-}
|
||||
{-# LANGUAGE PolyKinds #-}
|
||||
{-# LANGUAGE RankNTypes #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
@ -22,17 +23,26 @@ import Language.Haskell.TH.Syntax
|
||||
import GHC.TypeLits
|
||||
|
||||
import Data.Parameterized.Classes
|
||||
import Data.Parameterized.FreeParamF ( FreeParamF(..) )
|
||||
import qualified Data.Parameterized.Lift as LF
|
||||
import qualified Data.Parameterized.Map as Map
|
||||
import qualified Data.Parameterized.Nonce as PN
|
||||
import qualified Data.Parameterized.ShapedList as SL
|
||||
import Data.Parameterized.Some ( Some(..) )
|
||||
import qualified Data.Parameterized.TraversableFC as FC
|
||||
import Data.Parameterized.Witness ( Witness(..) )
|
||||
import qualified Lang.Crucible.Solver.Interface as SI
|
||||
import qualified Lang.Crucible.Solver.SimpleBuilder as S
|
||||
import qualified Lang.Crucible.Solver.SimpleBackend as S
|
||||
import qualified Lang.Crucible.BaseTypes as S
|
||||
|
||||
import qualified Dismantle.PPC as D
|
||||
import qualified Dismantle.Tablegen.TH.Capture as DT
|
||||
|
||||
import qualified SemMC.BoundVar as BV
|
||||
import SemMC.Formula
|
||||
import qualified SemMC.Architecture as A
|
||||
import qualified SemMC.Architecture.Location as L
|
||||
import qualified SemMC.Architecture.PPC.Location as APPC
|
||||
import qualified Data.Macaw.CFG as M
|
||||
import qualified Data.Macaw.Types as M
|
||||
@ -47,17 +57,161 @@ import Data.Parameterized.NatRepr ( knownNat
|
||||
import Data.Macaw.PPC.Generator
|
||||
import Data.Macaw.PPC.PPCReg
|
||||
|
||||
-- generate a different case for each key/value pair in the map
|
||||
genExecInstruction :: (A.Architecture arch, OrdF a, ShowF a)
|
||||
-- | A different parameterized pair wrapper; the one in Data.Parameterized.Map
|
||||
-- hides the @tp@ parameter under an existential, while we need the variant that
|
||||
-- exposes it.
|
||||
data PairF a b tp = PairF (a tp) (b tp)
|
||||
|
||||
-- | Generate the top-level lambda with a case expression over an instruction
|
||||
-- (casing on opcode)
|
||||
--
|
||||
-- > \ipVar (Instruction opcode operandList) ->
|
||||
-- > case opcode of
|
||||
-- > ${CASES}
|
||||
--
|
||||
-- where each case in ${CASES} is defined by 'mkSemanticsCase'; each case
|
||||
-- matches one opcode.
|
||||
instructionMatcher :: (OrdF a, LF.LiftF a)
|
||||
=> Map.MapF (Witness c a) (PairF (ParameterizedFormula (Sym t) arch) (DT.CaptureInfo c a))
|
||||
-> Q Exp
|
||||
instructionMatcher formulas = do
|
||||
ipVarName <- newName "ipVal"
|
||||
opcodeVar <- newName "opcode"
|
||||
operandListVar <- newName "operands"
|
||||
let cases = map (mkSemanticsCase ipVarName operandListVar) (Map.toList formulas)
|
||||
lamE [varP ipVarName, conP 'D.Instruction [varP opcodeVar, varP operandListVar]] (caseE (varE opcodeVar) cases)
|
||||
|
||||
-- | Generate a single case for one opcode of the case expression.
|
||||
--
|
||||
-- > ADD4 -> ${BODY}
|
||||
--
|
||||
-- where the ${BODY} is generated by 'mkOperandListCase'
|
||||
mkSemanticsCase :: (LF.LiftF a)
|
||||
=> Name
|
||||
-> Name
|
||||
-> Map.Pair (Witness c a) (PairF (ParameterizedFormula (Sym t) arch) (DT.CaptureInfo c a))
|
||||
-> MatchQ
|
||||
mkSemanticsCase ipVarName operandListVar (Map.Pair (Witness opc) (PairF semantics capInfo)) =
|
||||
match (conP (DT.capturedOpcodeName capInfo) []) (normalB (mkOperandListCase ipVarName operandListVar opc semantics capInfo)) []
|
||||
|
||||
-- | 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
|
||||
-- of the form:
|
||||
--
|
||||
-- > case operandList of
|
||||
-- > op1 :> op2 :> op3 :> Nil -> ${BODY}
|
||||
--
|
||||
-- where ${BODY} is generated by 'genCaseBody', which references the operand
|
||||
-- names introduced by this case (e.g., op1, op2, op3). Those names are pulled
|
||||
-- from the DT.CaptureInfo, and have been pre-allocated. See
|
||||
-- Dismantle.Tablegen.TH.Capture.captureInfo for information on how those names
|
||||
-- are generated.
|
||||
--
|
||||
-- Note that the structure of the operand list is actually a little more
|
||||
-- complicated than the above. Each operand actually has an additional level of
|
||||
-- wrapper around it, and really looks like:
|
||||
--
|
||||
-- > Dismantle.PPC.ADD4
|
||||
-- > -> case operands_ayaa of {
|
||||
-- > (Gprc gprc0 :> (Gprc gprc1 :> (Gprc gprc2 :> Nil)))
|
||||
-- > -> ${BODY}
|
||||
--
|
||||
-- in an example with three general purpose register operands.
|
||||
mkOperandListCase :: Name -> Name -> a tp -> ParameterizedFormula (Sym t) arch tp -> DT.CaptureInfo c a tp -> Q Exp
|
||||
mkOperandListCase ipVarName operandListVar opc semantics capInfo = do
|
||||
body <- genCaseBody ipVarName opc semantics (DT.capturedOperandNames capInfo)
|
||||
DT.genCase capInfo operandListVar body
|
||||
|
||||
-- | This is the function that translates formulas (semantics) into expressions
|
||||
-- that construct macaw terms.
|
||||
--
|
||||
-- The stub implementation is essentially
|
||||
--
|
||||
-- > undefined ipVar arg1 arg2
|
||||
--
|
||||
-- to avoid unused variable warnings.
|
||||
--
|
||||
-- The two maps (locVars and opVars) are crucial for translating parameterized
|
||||
-- formulas into expressions.
|
||||
genCaseBody :: forall a sh t arch
|
||||
. Name
|
||||
-> a sh
|
||||
-> ParameterizedFormula (Sym t) arch sh
|
||||
-> SL.ShapedList (FreeParamF Name) sh
|
||||
-> Q Exp
|
||||
genCaseBody ipVarName opc semantics varNames =
|
||||
[| undefined $(tupE (map varE binders)) |]
|
||||
where
|
||||
binders = ipVarName : FC.toListFC unFreeParamF varNames
|
||||
|
||||
locVars :: Map.MapF (SI.BoundVar (Sym t)) (L.Location arch)
|
||||
locVars = Map.foldrWithKey (collectVarForLocation (Proxy @arch)) Map.empty (pfLiteralVars semantics)
|
||||
|
||||
opVars :: Map.MapF (SI.BoundVar (Sym t)) (FreeParamF Name)
|
||||
opVars = SL.foldrFCIndexed (collectOperandVars varNames) Map.empty (pfOperandVars semantics)
|
||||
|
||||
collectVarForLocation :: forall tp arch proxy t
|
||||
. proxy arch
|
||||
-> L.Location arch tp
|
||||
-> SI.BoundVar (Sym t) tp
|
||||
-> Map.MapF (SI.BoundVar (Sym t)) (L.Location arch)
|
||||
-> Map.MapF (SI.BoundVar (Sym t)) (L.Location arch)
|
||||
collectVarForLocation _ loc bv = Map.insert bv loc
|
||||
|
||||
-- | Index variables that map to operands
|
||||
--
|
||||
-- We record the TH 'Name' for the 'SI.BoundVar' that stands in for each
|
||||
-- operand. The idea will be that we will look up bound variables in this map
|
||||
-- to be able to compute a TH expression to refer to it.
|
||||
--
|
||||
-- We have to unwrap and rewrap the 'FreeParamF' because the type parameter
|
||||
-- changes when we switch from 'BV.BoundVar' to 'SI.BoundVar'. See the
|
||||
-- SemMC.BoundVar module for information about the nature of that change
|
||||
-- (basically, from 'Symbol' to BaseType).
|
||||
collectOperandVars :: forall sh tp arch t
|
||||
. SL.ShapedList (FreeParamF Name) sh
|
||||
-> SL.Index sh tp
|
||||
-> BV.BoundVar (Sym t) arch tp
|
||||
-> Map.MapF (SI.BoundVar (Sym t)) (FreeParamF Name)
|
||||
-> Map.MapF (SI.BoundVar (Sym t)) (FreeParamF Name)
|
||||
collectOperandVars varNames ix (BV.BoundVar bv) m =
|
||||
case SL.indexShapedList varNames ix of
|
||||
FreeParamF name -> Map.insert bv (FreeParamF name) m
|
||||
|
||||
-- | Generate an implementation of 'execInstruction' that runs in the
|
||||
-- 'PPCGenerator' monad. We pass in both the original list of semantics files
|
||||
-- along with the list of opcode info objects. We can match them up using
|
||||
-- equality on opcodes (via a MapF). Generating a combined list up-front would
|
||||
-- be ideal, but is difficult for various TH reasons (we can't call 'lift' on
|
||||
-- all of the things we would need to for that).
|
||||
--
|
||||
-- The structure of the term produced is documented in 'instructionMatcher'
|
||||
genExecInstruction :: (A.Architecture arch, OrdF a, ShowF a, LF.LiftF a)
|
||||
=> proxy arch
|
||||
-> (forall sh . c sh C.:- BuildOperandList arch sh)
|
||||
-- ^ A constraint implication to let us extract/weaken the
|
||||
-- constraint in our 'Witness' to the required 'BuildOperandList'
|
||||
-> [(Some (Witness c a), BS.ByteString)]
|
||||
-- ^ A list of opcodes (with constraint information
|
||||
-- witnessed) paired with the bytestrings containing their
|
||||
-- semantics. This comes from semmc.
|
||||
-> [Some (DT.CaptureInfo c a)]
|
||||
-- ^ Extra information for each opcode to let us generate
|
||||
-- some TH to match them. This comes from the semantics
|
||||
-- definitions in semmc.
|
||||
-> Q Exp
|
||||
genExecInstruction _ impl semantics = do
|
||||
genExecInstruction _ impl semantics captureInfo = do
|
||||
Some ng <- runIO PN.newIONonceGenerator
|
||||
sym <- runIO (S.newSimpleBackend ng)
|
||||
formulas <- runIO (loadFormulas sym impl semantics)
|
||||
[| undefined |]
|
||||
let formulasWithInfo = foldr (attachInfo formulas) Map.empty captureInfo
|
||||
instructionMatcher formulasWithInfo
|
||||
where
|
||||
attachInfo m0 (Some ci) m =
|
||||
let co = DT.capturedOpcode ci
|
||||
in case Map.lookup co m0 of
|
||||
Nothing -> m
|
||||
Just pf -> Map.insert co (PairF pf ci) m
|
||||
|
||||
-- SemMC.Formula: instantiateFormula
|
||||
|
||||
|
@ -1 +1 @@
|
||||
Subproject commit d3e21f8cc1a8d6970b019aae6492ec279907d6c5
|
||||
Subproject commit 16beb81bcdb6fe5c5d5a260dbc117fae35a2a85d
|
@ -1 +1 @@
|
||||
Subproject commit b17122e4c53e550c3259d460ea0d85d2379b18da
|
||||
Subproject commit c95d3e7d0f9859bbe59fdc55bf6330dd56481933
|
@ -1 +1 @@
|
||||
Subproject commit eaf0f5137f6cd3628cd576ffebfdcc2781b2e77a
|
||||
Subproject commit fcaefe36c12065b515ec5e97c0287d1c8450fcfa
|
Loading…
Reference in New Issue
Block a user