VCGen: add MergeBlocksIntoPredecessors function

1 files changed, 26 insertions, 0 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 1c3fa979..4fa7f0b7 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -7,6 +7,7 @@ using System;
 using System.Collections;

 using System.Collections.Generic;

 using System.Diagnostics;

+using System.Linq;

 using System.Threading;

 using System.IO;

 using Microsoft.Boogie;

@@ -3036,6 +3037,31 @@ namespace VC {
       }

     }

 

+    /// <summary>

+    /// Simplifies the CFG of the given implementation impl by merging each

+    /// basic block with a single predecessor into that predecessor if the

+    /// predecessor has a single successor.

+    /// </summary>

+    public static void MergeBlocksIntoPredecessors(Program prog, Implementation impl) {

+      var blockGraph = prog.ProcessLoops(impl);

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

+      foreach (var block in blockGraph.Nodes) {

+        try {

+          var pred = blockGraph.Predecessors(block).Single();

+          if (blockGraph.Successors(pred).Single() == block) {

+            Block predMapping;

+            while (predMap.TryGetValue(pred, out predMapping))

+              pred = predMapping;

+            pred.Cmds.AddRange(block.Cmds);

+            pred.TransferCmd = block.TransferCmd;

+            impl.Blocks.Remove(block);

+            predMap[block] = pred;

+          }

+        // If Single throws an exception above (i.e. not exactly one pred/succ), skip this block.

+        } catch (InvalidOperationException) {}

+      }

+    }

+

     static void DumpMap(Hashtable /*Variable->Expr*/ map) {

       Contract.Requires(map != null);

       foreach (DictionaryEntry de in map) {