From deef37064f673be0391a7224ed8551b1e68be829 Mon Sep 17 00:00:00 2001
From: Shuvendu Lahiri <shuvendu@microsoft.com>
Date: Mon, 26 Oct 2015 17:27:52 -0700
Subject: Bug fix for deterministExtractLoops for Shaobo's example

---
 Source/Core/Absy.cs | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

(limited to 'Source')

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c2e68002..8c04007b 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -750,15 +750,28 @@ namespace Microsoft.Boogie {
             Contract.Assert(block != null);
             var auxCmd = block.TransferCmd as GotoCmd;
             if (auxCmd == null) continue;
-            foreach(var bl in auxCmd.labelTargets)
+            foreach (var bl in auxCmd.labelTargets)
             {
                 if (loopBlocks.Contains(bl)) continue;
-                immSuccBlks.Add(bl); 
+                immSuccBlks.Add(bl);
             }
         }
         return immSuccBlks;
     }
 
+    private HashSet<Block> GetBlocksInAllNaturalLoops(Block header, Graph<Block/*!*/>/*!*/ g)
+    {
+        Contract.Assert(CommandLineOptions.Clo.DeterministicExtractLoops, "Can only be called with /deterministicExtractLoops option");
+        var allBlocksInNaturalLoops = new HashSet<Block>();
+        foreach (Block/*!*/ source in g.BackEdgeNodes(header))
+        {
+            Contract.Assert(source != null);
+            g.NaturalLoops(header, source).Iter(b => allBlocksInNaturalLoops.Add(b));
+        }
+        return allBlocksInNaturalLoops;
+    }
+
+
     void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g,
                                   List<Implementation/*!*/>/*!*/ loopImpls,
                                   Dictionary<string, Dictionary<string, Block>> fullMap) {
@@ -975,8 +988,8 @@ namespace Microsoft.Boogie {
                 GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;
                 Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null && 
                     auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1);
-                var blksThatBreakOut = GetBreakBlocksOfLoop(header, source, g);
-                var loopNodes = g.NaturalLoops(header, source);
+                //BUGFIX on 10/26/15: this contains nodes present in NaturalLoops for a different backedgenode
+                var loopNodes = GetBlocksInAllNaturalLoops(header, g); //var loopNodes = g.NaturalLoops(header, source); 
                 foreach(var bl in auxGotoCmd.labelTargets) {
                     if (!loopNodes.Contains(bl)) {
                         Block auxNewBlock = new Block();
-- 
cgit v1.2.3