Bug fix for deterministExtractLoops for Shaobo's example

5 files changed, 120 insertions, 78 deletions

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();
diff --git a/Test/extractloops/detLoopExtract2.bpl b/Test/extractloops/detLoopExtract2.bpl
new file mode 100644
index 00000000..f2befc53
--- /dev/null
+++ b/Test/extractloops/detLoopExtract2.bpl
@@ -0,0 +1,27 @@
+// RUN: %boogie -nologo -nologo -stratifiedInline:1 -extractLoops -deterministicExtractLoops -recursionBound:6  "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+//This example checks the bug fix in the loop extract for http://symdiff.codeplex.com/workitem/4
+procedure {:entrypoint} Main() returns(r:int)
+{ 
+  var i, j : int;
+  var Flag : bool;
+  var b : bool;
+  i := 0;
+  j := 0;
+  Flag := false;
+  while(i<3)
+  {
+    havoc b;
+    if (b || Flag) {
+      i := i + 1;
+      j := j + 1; 
+    }
+    else {
+     Flag := true;
+     j := j + 1;
+    }
+  }
+  assume !(i == j || i == j - 1);
+  return;
+}
diff --git a/Test/extractloops/detLoopExtract2.bpl.expect b/Test/extractloops/detLoopExtract2.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/extractloops/detLoopExtract2.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/snapshots/Snapshots41.v0.bpl b/Test/snapshots/Snapshots41.v0.bpl
index 631fe544..dbfe3e2d 100644
--- a/Test/snapshots/Snapshots41.v0.bpl
+++ b/Test/snapshots/Snapshots41.v0.bpl
@@ -1,35 +1,35 @@
-procedure {:checksum "0"} M(x: int);

-implementation {:id "M"} {:checksum "1"} M(x: int)

-{                     assert x < 20 || 10 <= x;  // always true

-  assert x < 10;  // error

-  call Other(x);  // error: precondition violation

-}

-

-procedure {:checksum "10"} Other(y: int);

-  requires 0 <= y;

-implementation {:id "Other"} {:checksum "11"} Other(y: int)

-{

-}

-

-procedure {:checksum "20"} Posty() returns (z: int);

-  ensures 2 <= z;  // error: postcondition violation

-implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)

-{

-  var t: int;

-  t := 20;

-  if (t < z) {

-  } else {  // the postcondition violation occurs on this 'else' branch

-  }

-}

-

-procedure {:checksum "30"} NoChangeWhazzoeva(u: int);

-implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)

-{

-  assert u != 53;  // error

-}

-

-procedure {:checksum "40"} NoChangeAndCorrect();

-implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect()

-{

-  assert true;

-}

+procedure {:checksum "0"} M(x: int);
+implementation {:id "M"} {:checksum "1"} M(x: int)
+{                     assert x < 20 || 10 <= x;  // always true
+  assert x < 10;  // error
+  call Other(x);  // error: precondition violation
+}
+
+procedure {:checksum "10"} Other(y: int);
+  requires 0 <= y;
+implementation {:id "Other"} {:checksum "11"} Other(y: int)
+{
+}
+
+procedure {:checksum "20"} Posty() returns (z: int);
+  ensures 2 <= z;  // error: postcondition violation
+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
+{
+  var t: int;
+  t := 20;
+  if (t < z) {
+  } else {  // the postcondition violation occurs on this 'else' branch
+  }
+}
+
+procedure {:checksum "30"} NoChangeWhazzoeva(u: int);
+implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
+{
+  assert u != 53;  // error
+}
+
+procedure {:checksum "40"} NoChangeAndCorrect();
+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect()
+{
+  assert true;
+}
diff --git a/Test/snapshots/Snapshots41.v1.bpl b/Test/snapshots/Snapshots41.v1.bpl
index 0cd9fbf9..9864e0e4 100644
--- a/Test/snapshots/Snapshots41.v1.bpl
+++ b/Test/snapshots/Snapshots41.v1.bpl
@@ -1,39 +1,39 @@
-procedure {:checksum "0"} M(x: int);

-implementation {:id "M"} {:checksum "1"} M(x: int)

-{

-assert x < 20 || 10 <= x;  // always true

-  

-       assert x < 10;  // error

-  call Other(x);  // error: precondition violation

-  assert x == 7;  // error: this is a new error in v1

-}

-

-

-       procedure {:checksum "10"} Other(y: int);

-         requires 0 <= y;

-       implementation {:id "Other"} {:checksum "11"} Other(y: int)

-       {

-       }

-

-

-

-procedure {:checksum "20"} Posty() returns (z: int);

-  ensures 2 <= z;  // error: postcondition violation

-implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)

-{

-  var t: int;

-  t := 20;

-  if (t < z) {

-    assert true;  // this is a new assert

-  } else {  // the postcondition violation occurs on this 'else' branch

-  }

-}

-

-  procedure   {:checksum "30"} NoChangeWhazzoeva(u: int);

-  implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)

-  {

-       assert u != 53;  // error

-  }

-

-procedure {:checksum "40"} NoChangeAndCorrect();

-implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; }

+procedure {:checksum "0"} M(x: int);
+implementation {:id "M"} {:checksum "1"} M(x: int)
+{
+assert x < 20 || 10 <= x;  // always true
+  
+       assert x < 10;  // error
+  call Other(x);  // error: precondition violation
+  assert x == 7;  // error: this is a new error in v1
+}
+
+
+       procedure {:checksum "10"} Other(y: int);
+         requires 0 <= y;
+       implementation {:id "Other"} {:checksum "11"} Other(y: int)
+       {
+       }
+
+
+
+procedure {:checksum "20"} Posty() returns (z: int);
+  ensures 2 <= z;  // error: postcondition violation
+implementation {:id "Posty"} {:checksum "21"} Posty() returns (z: int)
+{
+  var t: int;
+  t := 20;
+  if (t < z) {
+    assert true;  // this is a new assert
+  } else {  // the postcondition violation occurs on this 'else' branch
+  }
+}
+
+  procedure   {:checksum "30"} NoChangeWhazzoeva(u: int);
+  implementation {:id "NoChangeWhazzoeva"} {:checksum "3"} NoChangeWhazzoeva(u: int)
+  {
+       assert u != 53;  // error
+  }
+
+procedure {:checksum "40"} NoChangeAndCorrect();
+implementation {:id "NoChangeAndCorrect"} {:checksum "41"} NoChangeAndCorrect() { assert true; }