From 616b266559de33f160e4d7e35ea7d7c7afeaf654 Mon Sep 17 00:00:00 2001 From: Stanislav Lyakhov Date: Fri, 10 May 2024 15:40:11 -0700 Subject: [PATCH] Fix refinement panic caused by duplicate cfg edges Refinement frequently tried to add duplicate edges to the cfg when encountering jump tables, since jump tables often have common targets (e.g. because of a `default` case). Instead of panicking, this is now handled as a benign case where no edge insertion is needed. --- refinement/src/Data/Macaw/Refinement/Path.hs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/refinement/src/Data/Macaw/Refinement/Path.hs b/refinement/src/Data/Macaw/Refinement/Path.hs index b39f76f5..d7dbecd4 100644 --- a/refinement/src/Data/Macaw/Refinement/Path.hs +++ b/refinement/src/Data/Macaw/Refinement/Path.hs @@ -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