Delete unreachable Blocks of an Impl before calling ExtractLoops().

This helps avoid a crash inside NewComputeDominators().

1 files changed, 40 insertions, 0 deletions

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) {