mirror of
https://github.com/GaloisInc/macaw.git
synced 2024-12-28 08:34:23 +03:00
[refinement] a function may have multiple paths to different exit points.
An "exit point" is a block which does not transfer to another block within the function. An exit may be a RET or a JMP or an ite representing different JMP targets; at this time it is assumed that the latter cannot mix external and internal JMP targets.
This commit is contained in:
parent
263f852924
commit
138666b410
@ -1,6 +1,7 @@
|
||||
module Data.Macaw.Refinement.FuncBlockUtils
|
||||
( BlockIdentifier
|
||||
, blockID
|
||||
, blockInFunction
|
||||
, blockTransferTo
|
||||
, funBlockIDs
|
||||
, funForBlock
|
||||
|
@ -2,12 +2,17 @@ module Data.Macaw.Refinement.Path
|
||||
( FuncBlockPath
|
||||
, buildFuncPath
|
||||
, pathDepth
|
||||
, pathTo
|
||||
, takePath
|
||||
)
|
||||
where
|
||||
|
||||
import Data.Macaw.Discovery.State ( DiscoveryFunInfo )
|
||||
import Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier, funBlockIDs, blockTransferTo )
|
||||
import Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier
|
||||
, blockInFunction
|
||||
, blockTransferTo
|
||||
, funBlockIDs
|
||||
)
|
||||
import Data.Parameterized.Some
|
||||
|
||||
|
||||
@ -17,12 +22,16 @@ data FuncBlockPath arch =
|
||||
[FuncBlockPath arch] -- ancestors to this block (non-loop)
|
||||
[BlockIdentifier arch] -- previously seen ancestors (loop)
|
||||
|
||||
buildFuncPath :: Some (DiscoveryFunInfo arch) -> FuncBlockPath arch
|
||||
|
||||
-- | Builds a list of all the back-paths through the specific
|
||||
-- function. The returned list is a list of all the exit points of
|
||||
-- the function, with a FuncBlockPath tree indicating the blocks
|
||||
-- forming the path to that exit point.
|
||||
buildFuncPath :: Some (DiscoveryFunInfo arch) -> [FuncBlockPath arch]
|
||||
buildFuncPath sfi@(Some fi) =
|
||||
let blks = funBlockIDs sfi
|
||||
in case fst $ bldFPath fi ([], blks) of
|
||||
[fp] -> fp
|
||||
_ -> error "Non-singular function path"
|
||||
in fst $ bldFPath fi ([], blks)
|
||||
|
||||
|
||||
bldFPath :: DiscoveryFunInfo arch ids
|
||||
-> ([FuncBlockPath arch], [BlockIdentifier arch])
|
||||
@ -30,6 +39,12 @@ bldFPath :: DiscoveryFunInfo arch ids
|
||||
bldFPath _fi x@(_, []) = x
|
||||
bldFPath fi (fs, b:_) = ([Path b [] []], [])
|
||||
|
||||
-- | Given a function's call paths, return the subset of the call
|
||||
-- paths that terminates with the specified block.
|
||||
pathTo :: BlockIdentifier arch -> [FuncBlockPath arch] -> Maybe (FuncBlockPath arch)
|
||||
pathTo blkID fpath = undefined
|
||||
|
||||
|
||||
takePath :: Int -> FuncBlockPath arch -> FuncBlockPath arch
|
||||
takePath n (Path blkid anc loop) =
|
||||
if n > 0
|
||||
|
@ -124,7 +124,7 @@ import Data.Macaw.Discovery.State ( DiscoveryFunInfo
|
||||
, stmtsTerm
|
||||
)
|
||||
import Data.Macaw.Refinement.FuncBlockUtils ( BlockIdentifier, blockID, funForBlock )
|
||||
import Data.Macaw.Refinement.Path ( FuncBlockPath, buildFuncPath, pathDepth, takePath )
|
||||
import Data.Macaw.Refinement.Path ( FuncBlockPath, buildFuncPath, pathDepth, pathTo, takePath )
|
||||
import qualified Data.Macaw.CFG as MC
|
||||
import qualified Data.Macaw.Symbolic as MS
|
||||
import Data.Map (Map)
|
||||
@ -217,9 +217,9 @@ isUnknownTransfer pb =
|
||||
refineBlockTransfer :: DiscoveryState arch
|
||||
-> Some (ParsedBlock arch)
|
||||
-> Maybe (DiscoveryState arch)
|
||||
refineBlockTransfer inpDS blk@(Some pBlk) =
|
||||
refineBlockTransfer inpDS blk =
|
||||
let path = buildFuncPath <$> funForBlock blk inpDS
|
||||
in case path of
|
||||
in case path >>= pathTo (blockID blk) of
|
||||
Nothing -> error "unable to find function path for block" -- internal error
|
||||
Just p -> do soln <- refinePath inpDS p (pathDepth p) 0 Nothing
|
||||
return $ updateDiscovery soln blk inpDS
|
||||
|
Loading…
Reference in New Issue
Block a user