mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-11-23 16:35:02 +03:00
Rename pblock fields to be more descriptive.
This commit is contained in:
parent
327003ae56
commit
c6a7ba7cd6
@ -538,9 +538,9 @@ summarizeBlock mem interpState b = do
|
||||
ctx <- gets $ demandInfoCtx . archDemandInfo
|
||||
-- Add all values demanded by non-terminal statements in list.
|
||||
mapM_ (mapM_ (\(Some v) -> demandValue addr v) . stmtDemandedValues ctx)
|
||||
(pblockNonterm b)
|
||||
(pblockStmts b)
|
||||
-- Add values demanded by terminal statements
|
||||
case pblockTerm b of
|
||||
case pblockTermStmt b of
|
||||
ParsedCall finalRegs m_ret_addr -> do
|
||||
-- Record the demands based on the call, and add edges between
|
||||
-- this note and next nodes.
|
||||
|
@ -53,9 +53,9 @@ module Data.Macaw.Discovery
|
||||
, State.pblockAddr
|
||||
, State.blockSize
|
||||
, State.blockReason
|
||||
, State.pblockNonterm
|
||||
, State.pblockStmts
|
||||
, State.blockFinalAbsState
|
||||
, State.pblockTerm
|
||||
, State.pblockTermStmt
|
||||
, State.ParsedTermStmt(..)
|
||||
-- * Simplification
|
||||
, eliminateDeadStmts
|
||||
@ -202,8 +202,8 @@ eliminateDeadStmts ainfo bs0 = elimDeadStmtsInBlock demandSet <$> bs0
|
||||
-- effects and terminal statement to demand set.
|
||||
addParsedBlockDemands :: ParsedBlock arch ids -> DemandComp arch ids ()
|
||||
addParsedBlockDemands b = do
|
||||
mapM_ addStmtDemands (pblockNonterm b)
|
||||
case pblockTerm b of
|
||||
mapM_ addStmtDemands (pblockStmts b)
|
||||
case pblockTermStmt b of
|
||||
ParsedCall regs _ -> do
|
||||
traverseF_ addValueDemands regs
|
||||
PLTStub regs _ _ ->
|
||||
@ -230,8 +230,8 @@ dropUnusedCodeInParsedBlock :: ArchitectureInfo arch
|
||||
dropUnusedCodeInParsedBlock ainfo b =
|
||||
-- Important to force the result list here, since otherwise we
|
||||
-- hold onto the entire input list
|
||||
foldr seq () stmts' `seq` b { pblockNonterm = stmts' }
|
||||
where stmts' = filter stmtPred (pblockNonterm b)
|
||||
foldr seq () stmts' `seq` b { pblockStmts = stmts' }
|
||||
where stmts' = filter stmtPred (pblockStmts b)
|
||||
demandSet =
|
||||
runDemandComp (archDemandContext ainfo) $ do
|
||||
addParsedBlockDemands b
|
||||
@ -781,7 +781,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 parsefd as
|
||||
-- ^ Address of function containing this block.
|
||||
, pctxAddr :: !(ArchSegmentOff arch)
|
||||
-- ^ Address of the current block
|
||||
}
|
||||
@ -1164,9 +1164,9 @@ addBlock src finfo initRegs sz b = do
|
||||
, blockSize = sz
|
||||
, blockReason = foundReason finfo
|
||||
, blockAbstractState = foundAbstractState finfo
|
||||
, pblockNonterm = parsedNonterm pc
|
||||
, pblockStmts = parsedNonterm pc
|
||||
, blockFinalAbsState = parsedAbsState pc
|
||||
, pblockTerm = parsedTerm pc
|
||||
, pblockTermStmt = parsedTerm pc
|
||||
}
|
||||
let pb' = dropUnusedCodeInParsedBlock (archInfo s) pb
|
||||
id %= addFunBlock src pb'
|
||||
@ -1184,9 +1184,9 @@ recordErrorBlock addr finfo maybeError = do
|
||||
, blockSize = 0
|
||||
, blockReason = foundReason finfo
|
||||
, blockAbstractState = foundAbstractState finfo
|
||||
, pblockNonterm = []
|
||||
, pblockStmts = []
|
||||
, blockFinalAbsState = initAbsProcessorState mem (foundAbstractState finfo)
|
||||
, pblockTerm = ParsedTranslateError errMsg
|
||||
, pblockTermStmt = ParsedTranslateError errMsg
|
||||
}
|
||||
id %= addFunBlock addr pb
|
||||
|
||||
|
@ -248,11 +248,11 @@ data ParsedBlock arch ids
|
||||
, blockAbstractState :: !(AbsBlockState (ArchReg arch))
|
||||
-- ^ Abstract state prior to the execution of
|
||||
-- this region.
|
||||
, pblockNonterm :: !([Stmt arch ids])
|
||||
, pblockStmts :: !([Stmt arch ids])
|
||||
-- ^ The non-terminal statements in the block
|
||||
, blockFinalAbsState :: !(AbsProcessorState (ArchReg arch) ids)
|
||||
-- ^ The abstract state of the block just before terminal
|
||||
, pblockTerm :: !(ParsedTermStmt arch ids)
|
||||
, pblockTermStmt :: !(ParsedTermStmt arch ids)
|
||||
-- ^ The terminal statement in the block.
|
||||
}
|
||||
|
||||
@ -264,7 +264,7 @@ instance ArchConstraints arch
|
||||
pretty b =
|
||||
let ppOff o = text (show (incAddr (toInteger o) (segoffAddr (pblockAddr b))))
|
||||
in text (show (pblockAddr b)) PP.<> text ":" <$$>
|
||||
indent 2 (vcat (ppStmt ppOff <$> pblockNonterm b) <$$> ppTermStmt (pblockTerm b))
|
||||
indent 2 (vcat (ppStmt ppOff <$> pblockStmts b) <$$> ppTermStmt (pblockTermStmt b))
|
||||
|
||||
------------------------------------------------------------------------
|
||||
-- DiscoveryFunInfo
|
||||
|
@ -400,7 +400,7 @@ mkParsedBlockRegCFG :: forall h arch ids
|
||||
-> ST h (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
|
||||
mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b = crucGenArchConstraints archFns $ do
|
||||
mkCrucRegCFG archFns halloc "" $ do
|
||||
let strippedBlock = b { M.pblockTerm = termStmtToReturn (M.pblockTerm b) }
|
||||
let strippedBlock = b { M.pblockTermStmt = termStmtToReturn (M.pblockTermStmt b) }
|
||||
|
||||
let entryAddr = M.pblockAddr strippedBlock
|
||||
|
||||
@ -485,10 +485,10 @@ mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks =
|
||||
let entry_addr = M.pblockAddr $ head blocks
|
||||
let first_blocks = zipWith
|
||||
(\block next_block ->
|
||||
block { M.pblockTerm = termStmtToJump (M.pblockTerm block) (M.pblockAddr next_block) })
|
||||
block { M.pblockTermStmt = termStmtToJump (M.pblockTermStmt block) (M.pblockAddr next_block) })
|
||||
(take (length blocks - 1) blocks)
|
||||
(tail blocks)
|
||||
let last_block = (last blocks) { M.pblockTerm = termStmtToReturn (M.pblockTerm (last blocks)) }
|
||||
let last_block = (last blocks) { M.pblockTermStmt = termStmtToReturn (M.pblockTermStmt (last blocks)) }
|
||||
let block_path = first_blocks ++ [last_block]
|
||||
|
||||
-- Get type for representing Machine registers
|
||||
@ -545,8 +545,8 @@ mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks =
|
||||
"the current block follows the previous block in the path"
|
||||
addStmt $ CR.Assume cond msg
|
||||
|
||||
mapM_ (addMacawStmt block_addr) (M.pblockNonterm block)
|
||||
addMacawParsedTermStmt block_label_map block_addr (M.pblockTerm block)
|
||||
mapM_ (addMacawStmt block_addr) (M.pblockStmts block)
|
||||
addMacawParsedTermStmt block_label_map block_addr (M.pblockTermStmt block)
|
||||
pure (reverse (first_crucible_block:first_extra_crucible_blocks))
|
||||
|
||||
pure (entry_label, init_crucible_block :
|
||||
|
@ -1551,8 +1551,8 @@ addParsedBlock archFns memSegMap blockLabelMap posFn regReg macawBlock = do
|
||||
throwError $ "Internal: Could not find block with address " ++ show startAddr
|
||||
(b,bs) <-
|
||||
runCrucGen archFns memSegMap thisPosFn lbl regReg $ do
|
||||
mapM_ (addMacawStmt startAddr) (M.pblockNonterm macawBlock)
|
||||
addMacawParsedTermStmt blockLabelMap startAddr (M.pblockTerm macawBlock)
|
||||
mapM_ (addMacawStmt startAddr) (M.pblockStmts macawBlock)
|
||||
addMacawParsedTermStmt blockLabelMap startAddr (M.pblockTermStmt macawBlock)
|
||||
pure (reverse (b : bs))
|
||||
|
||||
traverseArchStateUpdateMap :: (Applicative m)
|
||||
|
@ -119,7 +119,7 @@ testDiscovery expectedFilename elf = do
|
||||
F.forM_ (M.elems (dfi ^. MD.parsedBlocks)) $ \pb -> do
|
||||
let addr = MD.pblockAddr pb
|
||||
unless (S.member addr ignoredBlocks) $ do
|
||||
let term = MD.pblockTerm pb
|
||||
let term = MD.pblockTermStmt pb
|
||||
T.assertBool ("Unclassified block at " ++ show (MD.pblockAddr pb)) (not (isClassifyFailure term))
|
||||
T.assertBool ("Translate error at " ++ show (MD.pblockAddr pb) ++ " " ++ show term) (not (isTranslateError term))
|
||||
let actualEntry = MD.discoveredFunAddr dfi
|
||||
|
Loading…
Reference in New Issue
Block a user