From 07f7c5bd1600d1fbe90eba8f8f150fe526626568 Mon Sep 17 00:00:00 2001
From: akashlal <unknown>
Date: Sun, 5 Sep 2010 13:31:35 +0000
Subject: Delete unreachable Blocks of an Impl before calling ExtractLoops().
 This helps avoid a crash inside NewComputeDominators().

---
 Source/Core/Absy.cs | 40 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

(limited to 'Source/Core')

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 8daf39df..63f6d28d 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -631,6 +631,7 @@ namespace Microsoft.Boogie {
 
       Graph<Block/*!*/> g = new Graph<Block/*!*/>();
       g.AddSource(impl.Blocks[0]); // there is always at least one node in the graph
+
       foreach (Block b in impl.Blocks) {
         Contract.Assert(b != null);
         GotoCmd gtc = b.TransferCmd as GotoCmd;
@@ -644,12 +645,51 @@ namespace Microsoft.Boogie {
       return g;
     }
 
+    // Delete unreachable Blocks of an Impl. This helps avoid a bug inside
+    // NewComputeDominators
+
+    public void pruneUnreachableBlocks(Implementation impl)
+    {
+        // Do a BFS to find all reachable blocks
+        List<Block> reachableBlocks = new List<Block>();
+        Set<string> visited = new Set<string>();
+        List<Block> worklist = new List<Block>();
+
+        visited.Add(impl.Blocks[0].Label);
+        worklist.Add(impl.Blocks[0]);
+
+        while (worklist.Count != 0)
+        {
+            var block = worklist[0];
+            worklist.RemoveAt(0);
+
+            reachableBlocks.Add(block);
+            GotoCmd gc = block.TransferCmd as GotoCmd;
+            if(gc == null) continue;
+
+            foreach (Block succ in gc.labelTargets)
+            {
+                if (visited.Contains(succ.Label)) continue;
+                visited.Add(succ.Label);
+                worklist.Add(succ);
+            }
+        }
+
+        // Delete unreachable blocks
+       
+        // Make sure that the start block hasn't changed.
+        Contract.Assert(reachableBlocks[0] == impl.Blocks[0]);
+
+        impl.Blocks = reachableBlocks;
+    }
+
     public Dictionary<string, Dictionary<string, Block>> ExtractLoops() {
       List<Implementation/*!*/>/*!*/ loopImpls = new List<Implementation/*!*/>();
       Dictionary<string, Dictionary<string, Block>> fullMap = new Dictionary<string, Dictionary<string, Block>>();
       foreach (Declaration d in this.TopLevelDeclarations) {
         Implementation impl = d as Implementation;
         if (impl != null && impl.Blocks != null && impl.Blocks.Count > 0) {
+          pruneUnreachableBlocks(impl);
           Graph<Block/*!*/>/*!*/ g = GraphFromImpl(impl);
           g.ComputeLoops();
           if (!g.Reducible) {
-- 
cgit v1.2.3