GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-28 01:35:33 +03:00
Code Issues Projects Releases Wiki Activity

[refinement] some updates/fixes to FuncBlockPath building.

Browse Source
This commit is contained in:
Kevin Quick 2019-01-29 14:33:15 -08:00
parent e410b88b36
commit 9945a2898e
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
1 changed files with 9 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
refinement/src/Data/Macaw/Refinement/Path.hs
View File

@ -78,8 +78,12 @@ bldFPath :: DiscoveryFunInfo arch ids
bldFPath _fi x@(_, []) = x
bldFPath fi (fs, b:bs) =
let nextBlkAddrs = blockTransferTo fi b
isPathElemForBlock bid (Path pid _ _) = bid == pid
isTopLevelPathEntry = not $ null $ filter (isPathElemForBlock b) fs
updPath = if null nextBlkAddrs
then Path b [] [] : fs
then if isTopLevelPathEntry
then fs
else b $ Path b [] [] : fs
else foldr (bldFPath' fi b) fs nextBlkAddrs
in bldFPath fi (updPath, bs)
@ -93,6 +97,7 @@ bldFPath' fi b nextAddr fs =
let nextBlkID = blockInFunction fi nextAddr
isPathElemForBlock bid (Path pid _ _) = bid == pid
isTopLevelPathEntry e = not $ null $ filter (isPathElemForBlock e) fs
-- until an if "ancestor" is attached to any callees it appears
-- to be a terminal path point. When a callee is identified,
@ -118,7 +123,9 @@ bldFPath' fi b nextAddr fs =
then case ancPathElem of
Nothing -> updPath
Just _ -> filter (not . isPathElemForBlock b) updPath -- remove terminal entry
else Path b [] [] : p -- new terminal entry
else if isTopLevelPathEntry cb
then p
else Path cb [Path b [] []] [] : p -- new terminal entry
in case nextBlkID of
Nothing -> fs -- target addr was external to this function; ignore it