Implemented block coalescing invoked right after type checking.

Controlled by the option /coalesceBlocks (default is to perform the optimization).

4 files changed, 106 insertions, 3 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.ssc b/Source/BoogieDriver/BoogieDriver.ssc
index 035879ec..7b22d6fe 100644
--- a/Source/BoogieDriver/BoogieDriver.ssc
+++ b/Source/BoogieDriver/BoogieDriver.ssc
@@ -420,6 +420,11 @@ namespace Microsoft.Boogie
       // Eliminate dead variables

       Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);

       

+      // Coalesce blocks

+      if (CommandLineOptions.Clo.CoalesceBlocks) {

+        Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);

+      }

+      

       // Inline

       List<Declaration!>! TopLevelDeclarations = program.TopLevelDeclarations;

       if (CommandLineOptions.Clo.ProcedureInlining != CommandLineOptions.Inlining.None) {

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index bd54d624..2dd85a65 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -162,7 +162,8 @@ namespace Microsoft.Boogie
     public bool useDoomDebug = false; // Will use doomed analysis to search for errors if set

     

     public bool RemoveEmptyBlocks = true;

-

+	public bool CoalesceBlocks = true;

+	

     [Rep] public ProverFactory TheProverFactory;

     public string ProverName;

     [Peer] public List<string!>! ProverOptions = new List<string!>();

@@ -842,6 +843,25 @@ namespace Microsoft.Boogie
             }

             break;

             

+          case "-coalesceBlocks":

+          case "/coalesceBlocks":

+            if (ps.ConfirmArgumentCount(1))

+            {

+              switch (args[ps.i])

+              {

+                case "0": 

+                  CoalesceBlocks = false;

+                  break;

+                case "1":

+                  CoalesceBlocks = true;

+                  break;

+                default:

+                  ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                  break;

+              }

+            }

+            break;

+

           case "/DoomDebug":

             vcVariety = VCVariety.Doomed;

             useDoomDebug = true;

@@ -1846,6 +1866,8 @@ namespace Microsoft.Boogie
                               1 = perform live variable analysis (default)

   /noVerify      : skip VC generation and invocation of the theorem prover

   /noRemoveEmptyBlocks : do not remove empty blocks during VC generation

+  /coalesceBlocks:<c> : 0 = do not coalesce blocks

+                        1 = coalesce blocks (default)

   /vc:<variety>  : n = nested block (default for non-/prover:z3),

                    m = nested block reach,

                    b = flat block, r = flat block reach,

diff --git a/Source/Core/DeadVarElim.ssc b/Source/Core/DeadVarElim.ssc
index c7b0c7d8..e60a59c3 100644
--- a/Source/Core/DeadVarElim.ssc
+++ b/Source/Core/DeadVarElim.ssc
@@ -45,8 +45,84 @@ namespace Microsoft.Boogie
     }

   } 

   

+  public class BlockCoalescer : StandardVisitor { 

+    public static void CoalesceBlocks(Program! program) {

+      BlockCoalescer blockCoalescer = new BlockCoalescer();

+      blockCoalescer.Visit(program);

+    }

+    

+    private static Set<Block!>! ComputeMultiPredecessorBlocks(Implementation !impl) {

+      Set<Block!> visitedBlocks = new Set<Block!>();

+      Set<Block!> multiPredBlocks = new Set<Block!>();

+      Stack<Block!> dfsStack = new Stack<Block!>();

+      dfsStack.Push(impl.Blocks[0]);

+      while (dfsStack.Count > 0) {

+        Block! b = dfsStack.Pop();

+        if (visitedBlocks.Contains(b)) {

+          multiPredBlocks.Add(b);

+          continue;

+        }

+        visitedBlocks.Add(b);

+        if (b.TransferCmd == null) continue;

+        if (b.TransferCmd is ReturnCmd) continue;

+        assert b.TransferCmd is GotoCmd;

+        GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;

+        if (gotoCmd.labelTargets == null) continue;

+        foreach (Block! succ in gotoCmd.labelTargets) {

+          dfsStack.Push(succ);

+        }

+      }

+      return multiPredBlocks;

+    }

+    

+    public override Implementation! VisitImplementation(Implementation! impl) {

+      Set<Block!> multiPredBlocks = ComputeMultiPredecessorBlocks(impl);

+      Set<Block!> visitedBlocks = new Set<Block!>();

+      Set<Block!> removedBlocks = new Set<Block!>();

+      Stack<Block!> dfsStack = new Stack<Block!>();

+      dfsStack.Push(impl.Blocks[0]);

+      while (dfsStack.Count > 0) {

+        Block! b = dfsStack.Pop();

+        if (visitedBlocks.Contains(b)) continue;

+        visitedBlocks.Add(b);

+        if (b.TransferCmd == null) continue;

+        if (b.TransferCmd is ReturnCmd) continue;

+        assert b.TransferCmd is GotoCmd;

+        GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;

+        if (gotoCmd.labelTargets == null) continue;

+        if (gotoCmd.labelTargets.Length == 1) {

+          Block! succ = (!)gotoCmd.labelTargets[0];

+          if (!multiPredBlocks.Contains(succ)) {

+            foreach (Cmd! cmd in succ.Cmds) {

+              b.Cmds.Add(cmd);

+            }

+            b.TransferCmd = succ.TransferCmd;

+            if (!b.tok.IsValid && succ.tok.IsValid)

+              b.tok = succ.tok;

+            removedBlocks.Add(succ);

+            dfsStack.Push(b);

+            visitedBlocks.Remove(b);

+            continue;

+          }

+        } 

+        foreach (Block! succ in gotoCmd.labelTargets) {

+          dfsStack.Push(succ);

+        }

+      }

+      

+      List<Block!> newBlocks = new List<Block!>();

+      foreach (Block! b in impl.Blocks) {

+        if (!removedBlocks.Contains(b)) {

+          newBlocks.Add(b);

+        }

+      }

+      impl.Blocks = newBlocks;

+      return impl;

+    }

+  }

+  

   public class LiveVariableAnalysis {

-	public static void ComputeLiveVariables(Program! program, Implementation! impl) {

+	public static void ComputeLiveVariables(Implementation! impl) {

 	  Microsoft.Boogie.Helpers.ExtraTraceInformation("Starting live variable analysis");

 	  Graphing.Graph<Block> dag = new Graph<Block>();

       dag.AddSource((!)impl.Blocks[0]); // there is always at least one node in the graph

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index 24104fb4..a9b47222 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -1754,7 +1754,7 @@ namespace VC
       #endregion

     

       if (CommandLineOptions.Clo.LiveVariableAnalysis) {

-	    Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(program, impl);

+	    Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);

 	  }

 	  

       Convert2PassiveCmd(impl);