GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-25 21:54:51 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #381 from GaloisInc/fix/refinement-cfg-panic

Browse Source 
Fix refinement panic caused by duplicate cfg edges
This commit is contained in:
Stanislav Lyakhov 2024-05-10 16:49:31 -07:00 committed by GitHub
commit 4b2f7df44e
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 5 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -166,10 +166,13 @@ mkPartialCFG fi = computeBackEdges graph
tgtId = case M.lookup (FBU.blockID tgtBlock) addrNodes of
Just tgtId' -> tgtId'
Nothing -> panic $ "Cannot find target ID: " ++ show (FBU.blockID tgtBlock)
-- Since `tgtId` and `srcId` are confirmed to be valid nodes in the cfg,
-- the `Nothing` case implies that the edge already exists, so we don't need to insert it.
-- This can occur with jump tables that have common targets (e.g. a `default` case in a switch).
g = case G.insertLabeledEdge g0 srcId tgtId () of
Just (_e, g') -> g'
Nothing -> panic $ "Cannot find edge between "
++ show srcId ++ " and " ++ show tgtId
Nothing -> g0
in g
buildCFG gr (_addr, pb) =
let nodeId = case M.lookup (FBU.blockID pb) (cfgAddrNodes gr) of