added sound loop unrolling

4 files changed, 22 insertions, 13 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 402b5c68..6729532e 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -591,7 +591,7 @@ namespace Microsoft.Boogie {
       Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);

 

       if (CommandLineOptions.Clo.LoopUnrollCount != -1) {

-        program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

+        program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount, CommandLineOptions.Clo.SoundLoopUnrolling);

       }

 

       Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c8c052b7..e89671dd 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -341,7 +341,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public void UnrollLoops(int n) {

+    public void UnrollLoops(int n, bool uc) {

       Contract.Requires(0 <= n);

       foreach (Declaration d in this.TopLevelDeclarations) {

         Implementation impl = d as Implementation;

@@ -351,7 +351,7 @@ namespace Microsoft.Boogie {
             Block start = impl.Blocks[0];

             Contract.Assume(start != null);

             Contract.Assume(cce.IsConsistent(start));

-            impl.Blocks = LoopUnroll.UnrollLoops(start, n);

+            impl.Blocks = LoopUnroll.UnrollLoops(start, n, uc);

           }

           cce.EndExpose();

         }

@@ -522,7 +522,7 @@ namespace Microsoft.Boogie {
       // header_last block that was created because of splitting header.

       Dictionary<Block, Block> newBlocksCreated = new Dictionary<Block, Block>();

 

-      bool headRecursion = false; // testing an option to put recursive call before loop body 

+      bool headRecursion = false; // testing an option to put recursive call before loop body

 

       IEnumerable<Block> sortedHeaders = g.SortHeadersByDominance();

       foreach (Block/*!*/ header in sortedHeaders)

@@ -841,7 +841,7 @@ namespace Microsoft.Boogie {
 

                     // unroll

                     Block start = impl.Blocks[0];

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

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

 

                     // Now construct the "map back" information

                     // Resulting block label -> original block

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4192259d..06474981 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -437,6 +437,7 @@ namespace Microsoft.Boogie {
     }

 

     public int LoopUnrollCount = -1;  // -1 means don't unroll loops

+    public bool SoundLoopUnrolling = false;

     public int LoopFrameConditions = -1;  // -1 means not specified -- this will be replaced by the "implications" section below

     public int ModifiesDefault = 5;

     public bool LocalModifiesChecks = true;

@@ -1182,6 +1183,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("alwaysAssumeFreeLoopInvariants", ref AlwaysAssumeFreeLoopInvariants, true) ||

               ps.CheckBooleanFlag("nologo", ref DontShowLogo) ||

               ps.CheckBooleanFlag("proverLogAppend", ref SimplifyLogFileAppend) ||

+              ps.CheckBooleanFlag("soundLoopUnrolling", ref SoundLoopUnrolling) ||

               ps.CheckBooleanFlag("checkInfer", ref InstrumentWithAsserts) ||

               ps.CheckBooleanFlag("interprocInfer", ref IntraproceduralInfer, false) ||

               ps.CheckBooleanFlag("restartProver", ref RestartProverPerVC) ||

@@ -1421,6 +1423,8 @@ namespace Microsoft.Boogie {
 

   /loopUnroll:<n>

                 unroll loops, following up to n back edges (and then some)

+  /soundLoopUnrolling

+                sound loop unrolling

   /printModel:<n>

                 0 (default) - do not print Z3's error model

                 1 - print Z3's error model

diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs
index 580cbdc5..ed523840 100644
--- a/Source/Core/LoopUnroll.cs
+++ b/Source/Core/LoopUnroll.cs
@@ -10,7 +10,7 @@ using Microsoft.Boogie.GraphUtil;
 

 namespace Microsoft.Boogie {

   public class LoopUnroll {

-    public static List<Block/*!*/>/*!*/ UnrollLoops(Block start, int unrollMaxDepth) {

+    public static List<Block/*!*/>/*!*/ UnrollLoops(Block start, int unrollMaxDepth, bool soundLoopUnrolling) {

       Contract.Requires(start != null);

 

       Contract.Requires(0 <= unrollMaxDepth);

@@ -32,7 +32,7 @@ namespace Microsoft.Boogie {
         }

       }

 

-      LoopUnroll lu = new LoopUnroll(unrollMaxDepth, containingSCC, new List<Block/*!*/>());

+      LoopUnroll lu = new LoopUnroll(unrollMaxDepth, soundLoopUnrolling, containingSCC, new List<Block/*!*/>());

       lu.Visit(gStart);

       lu.newBlockSeqGlobal.Reverse();

       return lu.newBlockSeqGlobal;

@@ -172,6 +172,7 @@ namespace Microsoft.Boogie {
     readonly List<Block/*!*/>/*!*/ newBlockSeqGlobal;

     readonly Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>>/*!*/ containingSCC;

     readonly int c;

+    readonly bool soundLoopUnrolling;

     readonly LoopUnroll next;

     readonly LoopUnroll/*!*/ head;

 

@@ -185,7 +186,7 @@ namespace Microsoft.Boogie {
 

 

     [NotDelayed]

-    private LoopUnroll(int unrollMaxDepth, Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>>/*!*/ scc, List<Block/*!*/>/*!*/ newBlockSeqGlobal)

+    private LoopUnroll(int unrollMaxDepth, bool soundLoopUnrolling, Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>>/*!*/ scc, List<Block/*!*/>/*!*/ newBlockSeqGlobal)

       : base() {//BASEMOVE DANGER

       Contract.Requires(cce.NonNullElements(newBlockSeqGlobal));

       Contract.Requires(cce.NonNullDictionaryAndValues(scc) && Contract.ForAll(scc.Values, v => cce.NonNullElements(v)));

@@ -196,21 +197,22 @@ namespace Microsoft.Boogie {
       //:base();

       this.head = this;

       if (unrollMaxDepth != 0) {

-        next = new LoopUnroll(unrollMaxDepth - 1, scc, newBlockSeqGlobal, this);

+        next = new LoopUnroll(unrollMaxDepth - 1, soundLoopUnrolling, scc, newBlockSeqGlobal, this);

       }

     }

 

-    private LoopUnroll(int unrollMaxDepth, Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>> scc, List<Block/*!*/>/*!*/ newBlockSeqGlobal, LoopUnroll head) {

+    private LoopUnroll(int unrollMaxDepth, bool soundLoopUnrolling, Dictionary<GraphNode/*!*/, SCC<GraphNode/*!*/>> scc, List<Block/*!*/>/*!*/ newBlockSeqGlobal, LoopUnroll head) {

       Contract.Requires(head != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(scc));

       Contract.Requires(cce.NonNullElements(newBlockSeqGlobal));

       Contract.Requires(0 <= unrollMaxDepth);

       this.newBlockSeqGlobal = newBlockSeqGlobal;

       this.c = unrollMaxDepth;

+      this.soundLoopUnrolling = soundLoopUnrolling;

       this.containingSCC = scc;

       this.head = head;

       if (unrollMaxDepth != 0) {

-        next = new LoopUnroll(unrollMaxDepth - 1, scc, newBlockSeqGlobal, head);

+        next = new LoopUnroll(unrollMaxDepth - 1, soundLoopUnrolling, scc, newBlockSeqGlobal, head);

       }

     }

 

@@ -238,8 +240,11 @@ namespace Microsoft.Boogie {
               break;

             }

           }

-          body.Add(new AssumeCmd(orig.tok, Bpl.Expr.False));

-

+          if (soundLoopUnrolling) {

+            body.Add(new AssertCmd(orig.tok, Bpl.Expr.False));

+          } else {

+            body.Add(new AssumeCmd(orig.tok, Bpl.Expr.False));

+          }

           tcmd = new ReturnCmd(orig.TransferCmd.tok);

 

         } else {