From 7b82ee26a81c1a94a35b6f6887ab0a54a76b9c03 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 23 Feb 2024 13:27:29 -0800 Subject: [PATCH] Add information about the merged node when ending single-sided analysis This is primarily for the benefit of allowing the UI to precisely determine how to hook up the single-sided nodes to their merge point. --- src/Pate/Verification/StrongestPosts.hs | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 9eba70a6..f4044f08 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -615,7 +615,7 @@ updateCombinedSyncPoint :: GraphNode arch {- ^ diverging node -} -> PairGraph sym arch -> EquivM sym arch (PairGraph sym arch) -updateCombinedSyncPoint divergeNode pg_top = fnTrace "updateCombinedSyncPoint" $ withPG_ pg_top $ do +updateCombinedSyncPoint divergeNode pg_top = withPG_ pg_top $ do priority <- lift $ thisPriority syncsO_ <- fmap Set.toList $ liftPG $ getSyncPoints PBi.OriginalRepr divergeNode syncsP_ <- fmap Set.toList $ liftPG $ getSyncPoints PBi.PatchedRepr divergeNode @@ -632,7 +632,7 @@ updateCombinedSyncPoint divergeNode pg_top = fnTrace "updateCombinedSyncPoint" $ -- the graph as a result of some other operation (e.g. introducing an assertion). -- In the case where the first Original single-sided node is dropped, this ensures that it is -- re-scheduled by re-processing the divergence point. - [] -> withTracing @"message" "Missing Original sync point" $ do + [] -> do divergeNodeO <- toSingleGraphNode PBi.OriginalRepr divergeNode liftPG $ do modify $ queueNode (priority PriorityDomainRefresh) divergeNodeO @@ -668,6 +668,9 @@ updateCombinedSyncPoint divergeNode pg_top = fnTrace "updateCombinedSyncPoint" $ combinedNode <- liftPG $ do Just combinedNode <- return $ combineNodes syncO syncP return combinedNode + withTracingLabel @"node" "Merge Node" combinedNode $ do + emitTrace @"node" syncO + emitTrace @"node" syncP liftEqM $ mergeDualNodes syncO syncP domO_spec domP_spec combinedNode