Support for irreducible graphs (with extractLoops)

5 files changed, 183 insertions, 67 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index dc5fe47f..cb0ca968 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -747,28 +747,59 @@ namespace Microsoft.Boogie {
       }

     }

 

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

-          try {

-            Graph<Block> g = ProcessLoops(impl);

-            CreateProceduresForLoops(impl, g, loopImpls, fullMap);

-          }

-          catch (IrreducibleLoopException e) {

-            System.Diagnostics.Debug.Assert(!fullMap.ContainsKey(impl.Name));

-            fullMap[impl.Name] = null;

-          }

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

+            {

+                try

+                {

+                    Graph<Block> g = ProcessLoops(impl);

+                    CreateProceduresForLoops(impl, g, loopImpls, fullMap);

+                }

+                catch (IrreducibleLoopException e)

+                {

+                    System.Diagnostics.Debug.Assert(!fullMap.ContainsKey(impl.Name));

+                    fullMap[impl.Name] = null;

+

+                    // statically unroll loops in this procedure

+

+                    // First, build a map of the current blocks

+                    var origBlocks = new Dictionary<string, Block>();

+                    foreach (var blk in impl.Blocks) origBlocks.Add(blk.Label, blk);

+

+                    // unroll

+                    Block start = impl.Blocks[0];

+                    impl.Blocks = LoopUnroll.UnrollLoops(start, CommandLineOptions.Clo.RecursionBound);

+

+                    // Now construct the "map back" information

+                    // Resulting block label -> original block

+                    var blockMap = new Dictionary<string, Block>();

+                    foreach (var blk in impl.Blocks)

+                    {

+                        var sl = LoopUnroll.sanitizeLabel(blk.Label);

+                        if (sl == blk.Label) blockMap.Add(blk.Label, blk);

+                        else

+                        {

+                            Contract.Assert(origBlocks.ContainsKey(sl));

+                            blockMap.Add(blk.Label, origBlocks[sl]);

+                        }

+                    }

+                    fullMap[impl.Name] = blockMap;

+                }

+            }

         }

-      }

-      foreach (Implementation/*!*/ loopImpl in loopImpls) {

-        Contract.Assert(loopImpl != null);

-        TopLevelDeclarations.Add(loopImpl);

-        TopLevelDeclarations.Add(loopImpl.Proc);

-      }

-      return fullMap;

+        foreach (Implementation/*!*/ loopImpl in loopImpls)

+        {

+            Contract.Assert(loopImpl != null);

+            TopLevelDeclarations.Add(loopImpl);

+            TopLevelDeclarations.Add(loopImpl.Proc);

+        }

+        return fullMap;

     }

 

     public override Absy StdDispatch(StandardVisitor visitor) {

diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs
index 91d8842a..3b61ad3e 100644
--- a/Source/Core/LoopUnroll.cs
+++ b/Source/Core/LoopUnroll.cs
@@ -37,6 +37,20 @@ namespace Microsoft.Boogie {
       return lu.newBlockSeqGlobal;

     }

 

+    // This is supposed to "undo" to effect of loop unrolling

+    // on block labels. It essentially removes the "#num" from the end 

+    // of lab, if there is something like this

+    public static string sanitizeLabel(string lab)

+    {

+        if (!lab.Contains("#"))

+            return lab;

+

+        // Find the last occurrance of "#"

+        int pos = lab.LastIndexOf('#');

+

+        return lab.Substring(0, pos);

+    }

+

     private static System.Collections.IEnumerable/*<GraphNode/*!>/*!*/ Succs(GraphNode n) {

       Contract.Requires(n != null);

       Contract.Ensures(Contract.Result<System.Collections.IEnumerable>() != null);

diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
index b3efbe02..9a6c95a3 100644
--- a/Test/extractloops/Answer
+++ b/Test/extractloops/Answer
@@ -1,58 +1,81 @@
 ----- Running regression test t1.bpl

 t1.bpl(38,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        t1.bpl(19,3): anon0

-        t1.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t1.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t1.bpl(27,3): anon3_LoopBody

-        t1.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t1.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t1.bpl(27,3): anon3_LoopBody

-        t1.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t1.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t1.bpl(33,3): anon3_LoopDone

-        t1.bpl(37,3): anon2

+    t1.bpl(19,3): anon0

+    t1.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t1.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t1.bpl(27,3): anon3_LoopBody

+    t1.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t1.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t1.bpl(27,3): anon3_LoopBody

+    t1.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t1.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t1.bpl(33,3): anon3_LoopDone

+    t1.bpl(37,3): anon2

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

 ----- Running regression test t2.bpl

 t2.bpl(51,5): Error BP5001: This assertion might not hold.

 Execution trace:

-        t2.bpl(19,3): anon0

-        t2.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t2.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t2.bpl(27,3): anon3_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(37,3): lab1_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(37,3): lab1_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(42,3): lab1_LoopDone

-        t2.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t2.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t2.bpl(27,3): anon3_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(37,3): lab1_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(37,3): lab1_LoopBody

-        t2.bpl(34,3): lab1_LoopHead

-        t2.bpl(42,3): lab1_LoopDone

-        t2.bpl(23,3): anon3_LoopHead

-        Inlined call to procedure foo begins

-            t2.bpl(11,5): anon0

-        Inlined call to procedure foo ends

-        t2.bpl(46,3): anon3_LoopDone

-        t2.bpl(50,3): anon2

+    t2.bpl(19,3): anon0

+    t2.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t2.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t2.bpl(27,3): anon3_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(37,3): lab1_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(37,3): lab1_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(42,3): lab1_LoopDone

+    t2.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t2.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t2.bpl(27,3): anon3_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(37,3): lab1_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(37,3): lab1_LoopBody

+    t2.bpl(34,3): lab1_LoopHead

+    t2.bpl(42,3): lab1_LoopDone

+    t2.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t2.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t2.bpl(46,3): anon3_LoopDone

+    t2.bpl(50,3): anon2

+

+Boogie program verifier finished with 0 verified, 1 error

+-----

+----- Running regression test t3.bpl with recursion bound 2

+

+Boogie program verifier finished with 1 verified, 0 errors

+-----

+----- Running regression test t3.bpl with recursion bound 4

+t3.bpl(38,5): Error BP5001: This assertion might not hold.

+Execution trace:

+    t3.bpl(19,3): anon0

+    t3.bpl(27,3): anon3_LoopBody

+    t3.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t3.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t3.bpl(27,3): anon3_LoopBody

+    t3.bpl(23,3): anon3_LoopHead

+    Inlined call to procedure foo begins

+        t3.bpl(11,5): anon0

+    Inlined call to procedure foo ends

+    t3.bpl(33,3): anon3_LoopDone

+    t3.bpl(37,3): anon2

 

 Boogie program verifier finished with 0 verified, 1 error

 -----

diff --git a/Test/extractloops/runtest.bat b/Test/extractloops/runtest.bat
index dbc524c0..1ee560b9 100644
--- a/Test/extractloops/runtest.bat
+++ b/Test/extractloops/runtest.bat
@@ -10,4 +10,10 @@ echo -----
 echo ----- Running regression test t2.bpl

 %BGEXE% %* /noinfer /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 t2.bpl

 echo -----

+echo ----- Running regression test t3.bpl with recursion bound 2

+%BGEXE% %* /noinfer /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /recursionBound:2 t3.bpl

+echo -----

+echo ----- Running regression test t3.bpl with recursion bound 4

+%BGEXE% %* /noinfer /stratifiedInline:1 /extractLoops /removeEmptyBlocks:0 /coalesceBlocks:0 /recursionBound:4 t3.bpl

+echo -----

 

diff --git a/Test/extractloops/t3.bpl b/Test/extractloops/t3.bpl
new file mode 100644
index 00000000..e5fad6d1
--- /dev/null
+++ b/Test/extractloops/t3.bpl
@@ -0,0 +1,42 @@
+var g: int;

+

+procedure A();

+  requires g == 0;

+  modifies g;

+

+procedure {:inline 1} {:verify false} foo(); 

+

+implementation foo() {

+  var t: int;

+  t := 0;

+}

+

+implementation A()

+{

+  var x: int;

+  var y: int;

+

+  anon0:

+    x := 4;

+    goto anon3_LoopHead, anon3_LoopBody;

+

+  anon3_LoopHead:

+    call foo();

+    goto anon3_LoopDone, anon3_LoopBody;

+

+  anon3_LoopBody:

+    assume g < x;

+    g := g + 1;

+    x := x - 1;

+    goto anon3_LoopHead;

+

+  anon3_LoopDone:

+    assume g >= x;

+    goto anon2;

+

+  anon2:

+    assert x == 1;

+    return;

+}

+

+