mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-23 16:35:02 +03:00
Introduce ParsedBranch constructor.
This commit is contained in:
Joe Hendrix
parent
3331a19571
commit
8aa4650683
@ -1088,7 +1088,7 @@ setAbsIP :: RegisterInfo r
|
||||
-> AbsBlockState r
|
||||
setAbsIP a b
|
||||
-- Check to avoid reassigning next IP if it is not needed.
|
||||
| CodePointers s False <- b^.absRegState^.curIP
|
||||
| CodePointers s False <- b^.absRegState^.boundValue ip_reg
|
||||
, Set.size s == 1
|
||||
, Set.member a s =
|
||||
b
|
||||
@ -1316,12 +1316,12 @@ finalAbsBlockState :: forall a ids
|
||||
-> RegState (ArchReg a) (Value a ids)
|
||||
-- ^ Final values for abstract processor state
|
||||
-> AbsBlockState (ArchReg a)
|
||||
finalAbsBlockState c s =
|
||||
finalAbsBlockState c regs =
|
||||
let transferReg :: ArchReg a tp -> ArchAbsValue a tp
|
||||
transferReg r = transferValue c (s^.boundValue r)
|
||||
transferReg r = transferValue c (regs^.boundValue r)
|
||||
in AbsBlockState { _absRegState = mkRegState transferReg
|
||||
, _startAbsStack = c^.curAbsStack
|
||||
, _initIndexBounds = Jmp.nextBlockBounds (c^.indexBounds) s
|
||||
, _initIndexBounds = Jmp.nextBlockBounds (c^.indexBounds) regs
|
||||
}
|
||||
|
||||
------------------------------------------------------------------------
|
||||
|
||||
@ -242,7 +242,7 @@ data FunctionArgsState arch ids = FAS
|
||||
_blockTransfer :: !(Map (ArchLabel arch) (ResultDemandsMap (ArchReg arch)))
|
||||
|
||||
-- | If a demand d is demanded of block lbl then the block demands S, s.t.
|
||||
-- blockDemandMap ^. at lbl ^. at d = Just S
|
||||
-- `blockDemandMap ^. at lbl ^. at d = Just S1
|
||||
, _blockDemandMap :: !(Map (ArchLabel arch) (DemandMap (ArchReg arch)))
|
||||
|
||||
-- | Maps each global block label to the set of blocks that have intra-procedural
|
||||
@ -352,15 +352,21 @@ addBlockDemands lbl m =
|
||||
blockDemandMap %= Map.insertWith demandMapUnion lbl m
|
||||
|
||||
|
||||
-- Figure out the deps of the given registers and update the state for the current label
|
||||
-- | Given a block and a maping from register to value after the block
|
||||
-- has executed, this traverses the registers that will be available
|
||||
-- in future blocks, and records a mapping from those registers to
|
||||
-- their input dependencies.
|
||||
recordBlockTransfer :: forall arch ids
|
||||
. ( OrdF (ArchReg arch)
|
||||
, FoldableFC (ArchFn arch)
|
||||
)
|
||||
=> ArchLabel arch
|
||||
-- ^ Label for the current block.
|
||||
-> RegState (ArchReg arch) (Value arch ids)
|
||||
-- ^ Map from registers to values.
|
||||
-> [Some (ArchReg arch)]
|
||||
-> FunctionArgsM arch ids () -- Map (Some N.RegisterName) RegDeps
|
||||
-- ^ List of registers that subsequent blocks may depend on.
|
||||
-> FunctionArgsM arch ids ()
|
||||
recordBlockTransfer lbl s rs = do
|
||||
let doReg :: Some (ArchReg arch)
|
||||
-> State (AssignmentCache (ArchReg arch) ids)
|
||||
@ -436,16 +442,6 @@ calculateGlobalFixpoint s = go (s^.alwaysDemandMap) (s^.alwaysDemandMap)
|
||||
let ds' = ds1 `demandSetDifference` ds2 in
|
||||
if ds' == mempty then Nothing else Just ds'
|
||||
|
||||
transferDemands :: OrdF r
|
||||
=> Map (Some r) (DemandSet r)
|
||||
-> DemandSet r
|
||||
-> DemandSet r
|
||||
transferDemands xfer (DemandSet regs funs) =
|
||||
-- Using ix here means we ignore any registers we don't know about,
|
||||
-- e.g. caller-saved registers after a function call.
|
||||
-- FIXME: is this the correct behavior?
|
||||
mconcat (DemandSet mempty funs : [ xfer ^. ix r | r <- Set.toList regs ])
|
||||
|
||||
-- A function call is the only block type that results in the
|
||||
-- generation of function call demands, so we split that aspect out
|
||||
-- (callee saved are handled in summarizeBlock).
|
||||
@ -575,6 +571,14 @@ summarizeBlock mem interpState addr stmts = do
|
||||
recordBlockTransfer lbl procState archRegs
|
||||
addIntraproceduralJumpTarget interpState lbl tgtAddr
|
||||
|
||||
ParsedBranch nextRegs cond trueAddr falseAddr -> do
|
||||
demandValue lbl cond
|
||||
-- record all propagations
|
||||
let notIP (Some r) = isNothing (testEquality r ip_reg)
|
||||
recordBlockTransfer lbl nextRegs (filter notIP archRegs)
|
||||
addIntraproceduralJumpTarget interpState lbl trueAddr
|
||||
addIntraproceduralJumpTarget interpState lbl falseAddr
|
||||
|
||||
ParsedLookupTable finalRegs lookup_idx vec -> do
|
||||
demandValue lbl lookup_idx
|
||||
-- record all propagations
|
||||
@ -633,6 +637,17 @@ summarizeIter mem ist = do
|
||||
summarizeBlock mem ist (pblockAddr reg) (blockStatementList reg)
|
||||
summarizeIter mem ist
|
||||
|
||||
|
||||
transferDemands :: OrdF r
|
||||
=> Map (Some r) (DemandSet r)
|
||||
-> DemandSet r
|
||||
-> DemandSet r
|
||||
transferDemands xfer (DemandSet regs funs) =
|
||||
-- Using ix here means we ignore any registers we don't know about,
|
||||
-- e.g. caller-saved registers after a function call.
|
||||
-- FIXME: is this the correct behavior?
|
||||
mconcat (DemandSet mempty funs : [ xfer ^. ix r | r <- Set.toList regs ])
|
||||
|
||||
calculateOnePred :: (OrdF (ArchReg arch))
|
||||
=> DemandMap (ArchReg arch)
|
||||
-> ArchLabel arch
|
||||
@ -646,7 +661,6 @@ calculateOnePred newDemands predLbl = do
|
||||
-- update uses, returning value before this iteration
|
||||
seenDemands <- use (blockDemandMap . ix lbl')
|
||||
addBlockDemands lbl' demands'
|
||||
-- seenDemands <- blockDemandMap . ix lbl' <<%= demandMapUnion demands'
|
||||
|
||||
|
||||
let diff :: OrdF r => DemandSet r -> DemandSet r -> Maybe (DemandSet r)
|
||||
|
||||
@ -209,6 +209,8 @@ addStatementListDemands sl = do
|
||||
traverseF_ addValueDemands regs
|
||||
ParsedJump regs _ -> do
|
||||
traverseF_ addValueDemands regs
|
||||
ParsedBranch regs _ _ _ -> do
|
||||
traverseF_ addValueDemands regs
|
||||
ParsedLookupTable regs _idx _tbl -> do
|
||||
traverseF_ addValueDemands regs
|
||||
ParsedReturn regs -> do
|
||||
@ -807,7 +809,7 @@ data ParseContext arch ids =
|
||||
-- intra-procedural jumps to the entry points of new
|
||||
-- functions.
|
||||
, pctxFunAddr :: !(ArchSegmentOff arch)
|
||||
-- ^ Address of function this block is being parsed as
|
||||
-- ^ Address of function this block is being parsefd as
|
||||
, pctxAddr :: !(ArchSegmentOff arch)
|
||||
-- ^ Address of the current block
|
||||
}
|
||||
@ -900,6 +902,17 @@ removeUnassignedRegs initRegs finalRegs =
|
||||
where initVal = initRegs^.boundValue r
|
||||
in MapF.filterWithKey keepReg (regStateMap finalRegs)
|
||||
|
||||
-- | This returns true if the address may be the target of a
|
||||
-- intra-procedural control flow transfer.
|
||||
--
|
||||
-- Specifically this checks if the address is executable and not the current
|
||||
-- function address or a known function address.
|
||||
allowedIntraTarget :: ParseContext arch ids -> ArchSegmentOff arch -> Bool
|
||||
allowedIntraTarget ctx addr
|
||||
= segmentFlags (segoffSegment addr) `Perm.hasPerm` Perm.execute
|
||||
&& addr /= pctxFunAddr ctx
|
||||
&& addr `Set.notMember` pctxKnownFnEntries ctx
|
||||
|
||||
-- | Return true if any value in structure contains the given
|
||||
-- identifier.
|
||||
containsAssignId :: forall t arch ids itp
|
||||
@ -939,30 +952,53 @@ parseFetchAndExecute ctx idx initRegs stmts absProcState finalRegs = do
|
||||
-- Try to figure out what control flow statement we have.
|
||||
case () of
|
||||
-- The block ends with a Mux, so we turn this into a `ParsedIte` statement.
|
||||
_ | Just (Mux _ c t f) <- valueAsApp (finalRegs^.boundValue ip_reg) -> do
|
||||
_ | Just (Mux _ c t f) <- valueAsApp (finalRegs^.boundValue ip_reg)
|
||||
, Just trueTgtAddr <- valueAsSegmentOff mem t
|
||||
-- Check that true branch is an allowed intra-procedural branch target
|
||||
, allowedIntraTarget ctx trueTgtAddr
|
||||
, Just falseTgtAddr <- valueAsSegmentOff mem f
|
||||
-- Check that false branch is an allowed intra-procedural branch target
|
||||
, allowedIntraTarget ctx falseTgtAddr -> do
|
||||
|
||||
mapM_ (recordWriteStmt ainfo mem absProcState') stmts
|
||||
|
||||
let l_regs = refineProcStateBounds c True $
|
||||
refineProcState c absTrue absProcState'
|
||||
let l_regs' = absEvalStmts ainfo l_regs stmts
|
||||
let lState = finalRegs & boundValue ip_reg .~ t
|
||||
(tStmts,trueIdx) <-
|
||||
parseFetchAndExecute ctx (idx+1) initRegs Seq.empty l_regs' lState
|
||||
-- Registers with true value set.
|
||||
let trueRegs = finalRegs & boundValue ip_reg .~ t
|
||||
-- Abstract state after true regs.
|
||||
let trueEvalState =
|
||||
let refinedTrueState = refineProcStateBounds c True $
|
||||
refineProcState c absTrue absProcState'
|
||||
in absEvalStmts ainfo refinedTrueState stmts
|
||||
let trueAbsState = finalAbsBlockState trueEvalState trueRegs
|
||||
|
||||
let r_regs = refineProcStateBounds c False $
|
||||
refineProcState c absFalse absProcState'
|
||||
let r_regs' = absEvalStmts ainfo r_regs stmts
|
||||
let rState = finalRegs & boundValue ip_reg .~ f
|
||||
|
||||
(fStmts,falseIdx) <-
|
||||
parseFetchAndExecute ctx trueIdx initRegs Seq.empty r_regs' rState
|
||||
-- Merge block state and add intra jump target.
|
||||
|
||||
let tStmts = StatementList { stmtsIdent = idx+1
|
||||
, stmtsNonterm = []
|
||||
, stmtsTerm = ParsedJump trueRegs trueTgtAddr
|
||||
, stmtsAbsState = trueEvalState
|
||||
}
|
||||
|
||||
let falseRegs = finalRegs & boundValue ip_reg .~ f
|
||||
let falseEvalState =
|
||||
let refinedFalseState = refineProcStateBounds c False $
|
||||
refineProcState c absFalse absProcState'
|
||||
in absEvalStmts ainfo refinedFalseState stmts
|
||||
let falseAbsState = finalAbsBlockState falseEvalState falseRegs
|
||||
intraJumpTargets %= ([(trueTgtAddr, trueAbsState), (falseTgtAddr, falseAbsState)]++)
|
||||
let fStmts = StatementList { stmtsIdent = idx + 2
|
||||
, stmtsNonterm = []
|
||||
, stmtsTerm = ParsedJump falseRegs falseTgtAddr
|
||||
, stmtsAbsState = falseEvalState
|
||||
}
|
||||
|
||||
let ret = StatementList { stmtsIdent = idx
|
||||
, stmtsNonterm = toList stmts
|
||||
, stmtsTerm = ParsedIte c tStmts fStmts
|
||||
, stmtsAbsState = absProcState'
|
||||
}
|
||||
pure (ret, falseIdx)
|
||||
pure (ret, idx + 3)
|
||||
|
||||
-- Use architecture-specific callback to check if last statement was a call.
|
||||
-- Note that in some cases the call is known not to return, and thus
|
||||
@ -1007,16 +1043,8 @@ parseFetchAndExecute ctx idx initRegs stmts absProcState finalRegs = do
|
||||
|
||||
-- Jump to a block within this function.
|
||||
| Just tgt_mseg <- valueAsSegmentOff mem (finalRegs^.boundValue ip_reg)
|
||||
-- Check target block address is in executable segment.
|
||||
, segmentFlags (segoffSegment tgt_mseg) `Perm.hasPerm` Perm.execute
|
||||
|
||||
-- Check the target address is not the entry point of this function.
|
||||
-- N.B. These should instead decompile into calls or tail calls.
|
||||
, tgt_mseg /= pctxFunAddr ctx
|
||||
|
||||
-- If we are trusting known function entries, then only mark as an
|
||||
-- intra-procedural jump if the target is not a known function entry.
|
||||
, not (tgt_mseg `Set.member` pctxKnownFnEntries ctx) -> do
|
||||
-- Check that target is an allowed intra-procedural branch target.
|
||||
, allowedIntraTarget ctx tgt_mseg -> do
|
||||
|
||||
mapM_ (recordWriteStmt ainfo mem absProcState') stmts
|
||||
-- Merge block state and add intra jump target.
|
||||
@ -1039,7 +1067,6 @@ parseFetchAndExecute ctx idx initRegs stmts absProcState finalRegs = do
|
||||
abst = finalAbsBlockState absProcState' finalRegs
|
||||
|
||||
seq abst $ do
|
||||
|
||||
forM_ entries $ \tgtAddr -> do
|
||||
let abst' = abst & setAbsIP tgtAddr
|
||||
intraJumpTargets %= ((tgtAddr, abst'):)
|
||||
|
||||
@ -162,6 +162,15 @@ data ParsedTermStmt arch ids
|
||||
!(Relocation (ArchAddrWidth arch))
|
||||
-- | A jump to an explicit address within a function.
|
||||
| ParsedJump !(RegState (ArchReg arch) (Value arch ids)) !(ArchSegmentOff arch)
|
||||
-- | @ParsedBranch regs cond trueAddr falseAddr@ represents a conditional
|
||||
-- branch that jumps to `trueAddr` if `cond` is true and `falseAddr` otherwise.
|
||||
--
|
||||
-- The value assigned to the IP in `regs` should reflect this if-then-else
|
||||
-- structure.
|
||||
| ParsedBranch !(RegState (ArchReg arch) (Value arch ids))
|
||||
!(Value arch ids BoolType)
|
||||
!(ArchSegmentOff arch)
|
||||
!(ArchSegmentOff arch)
|
||||
-- | A lookup table that branches to one of a vector of addresses.
|
||||
--
|
||||
-- The registers store the registers, the value contains the index to jump
|
||||
@ -212,6 +221,9 @@ ppTermStmt ppOff tstmt =
|
||||
ParsedJump s addr ->
|
||||
text "jump" <+> text (show addr) <$$>
|
||||
indent 2 (pretty s)
|
||||
ParsedBranch r c t f ->
|
||||
text "branch" <+> pretty c <+> text (show t) <+> text (show f) <$$>
|
||||
indent 2 (pretty r)
|
||||
ParsedLookupTable s idx entries ->
|
||||
text "ijump" <+> pretty idx <$$>
|
||||
indent 2 (vcat (imap (\i v -> int i <+> text ":->" <+> text (show v))
|
||||
|
||||
@ -361,6 +361,7 @@ termStmtToReturn sl = sl { M.stmtsTerm = tm }
|
||||
tm0@M.ParsedReturn{} -> tm0
|
||||
M.ParsedCall r _ -> M.ParsedReturn r
|
||||
M.ParsedJump r _ -> M.ParsedReturn r
|
||||
M.ParsedBranch r _ _ _ -> M.ParsedReturn r
|
||||
M.ParsedLookupTable r _ _ -> M.ParsedReturn r
|
||||
M.ParsedIte b l r -> M.ParsedIte b (termStmtToReturn l) (termStmtToReturn r)
|
||||
M.ParsedArchTermStmt _ r _ -> M.ParsedReturn r
|
||||
@ -379,6 +380,7 @@ termStmtToJump sl addr = sl { M.stmtsTerm = tm }
|
||||
tm :: M.ParsedTermStmt arch ids
|
||||
tm = case M.stmtsTerm sl of
|
||||
M.ParsedJump r _ -> M.ParsedJump r addr
|
||||
M.ParsedBranch r _ _ _ -> M.ParsedJump r addr
|
||||
M.ParsedCall r _ -> M.ParsedJump r addr
|
||||
M.ParsedReturn r -> M.ParsedJump r addr
|
||||
M.ParsedLookupTable r _ _ -> M.ParsedJump r addr
|
||||
|
||||
@ -1411,6 +1411,12 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
|
||||
M.ParsedJump regs nextAddr -> do
|
||||
setMachineRegs =<< createRegStruct regs
|
||||
addTermStmt $ CR.Jump (parsedBlockLabel blockLabelMap nextAddr 0)
|
||||
M.ParsedBranch regs c trueAddr falseAddr -> do
|
||||
setMachineRegs =<< createRegStruct regs
|
||||
crucCond <- valueToCrucible c
|
||||
let tlbl = parsedBlockLabel blockLabelMap trueAddr 0
|
||||
let flbl = parsedBlockLabel blockLabelMap falseAddr 0
|
||||
addTermStmt $! CR.Br crucCond tlbl flbl
|
||||
M.ParsedLookupTable regs idx possibleAddrs -> do
|
||||
setMachineRegs =<< createRegStruct regs
|
||||
addSwitch blockLabelMap idx possibleAddrs
|
||||
|
||||
Loading…
Reference in New Issue
Block a user