Optimize blocks (#919)

### Changes

1. Perform block coalescing for each split
2. Add a post-split simplification that removes empty blocks with at
most one outgoing or incoming edge

### Testing
- Updated the test `AssumeFalseSplit.bpl` to take into account
simplification (2)

Source/Core/AST/AbsyCmd.cs

@@ -3539,6 +3539,11 @@ public GotoCmd(IToken /*!*/ tok, List<Block> /*!*/ blockSeq)
       this.labelTargets = blockSeq;
     }
 
+    public void RemoveTarget(Block b) {
+      labelNames.Remove(b.Label);
+      labelTargets.Remove(b);
+    }
+
     public void AddTarget(Block b)
     {
       Contract.Requires(b != null);

Source/Core/AST/Program.cs

@@ -3,7 +3,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
-using System.Text;
 using Microsoft.Boogie.GraphUtil;
 
 namespace Microsoft.Boogie;
@@ -501,26 +500,30 @@ public static Graph<Implementation> BuildCallGraph(CoreOptions options, Program
 
   public static Graph<Block> GraphFromBlocks(List<Block> blocks, bool forward = true)
   {
-    Graph<Block> g = new Graph<Block>();
+    var result = new Graph<Block>();
+    if (!blocks.Any())
+    {
+      return result;
+    }
     void AddEdge(Block a, Block b) {
       Contract.Assert(a != null && b != null);
       if (forward) {
-        g.AddEdge(a, b);
+        result.AddEdge(a, b);
       } else {
-        g.AddEdge(b, a);
+        result.AddEdge(b, a);
       }
     }
 
-    g.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph
-    foreach (Block b in blocks)
+    result.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph
+    foreach (var block in blocks)
     {
-      if (b.TransferCmd is GotoCmd gtc)
+      if (block.TransferCmd is GotoCmd gtc)
       {
         Contract.Assume(gtc.labelTargets != null);
-        gtc.labelTargets.ForEach(dest => AddEdge(b, dest));
+        gtc.labelTargets.ForEach(dest => AddEdge(block, dest));
       }
     }
-    return g;
+    return result;
   }
 
   public static Graph<Block /*!*/> /*!*/ GraphFromImpl(Implementation impl, bool forward = true)

Source/Core/Analysis/BlockCoalescer.cs

@@ -1,165 +1,161 @@
+#nullable enable
+
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 
 namespace Microsoft.Boogie;
 
 public class BlockCoalescer : ReadOnlyVisitor
 {
   public static void CoalesceBlocks(Program program)
   {
-    Contract.Requires(program != null);
-    BlockCoalescer blockCoalescer = new BlockCoalescer();
+    var blockCoalescer = new BlockCoalescer();
     blockCoalescer.Visit(program);
   }
 
-  private static HashSet<Block /*!*/> /*!*/ ComputeMultiPredecessorBlocks(Implementation /*!*/ impl)
+  private static HashSet<Block> ComputeMultiPredecessorBlocks(Block rootBlock)
   {
-    Contract.Requires(impl != null);
     Contract.Ensures(cce.NonNullElements(Contract.Result<HashSet<Block>>()));
-    HashSet<Block /*!*/> visitedBlocks = new HashSet<Block /*!*/>();
-    HashSet<Block /*!*/> multiPredBlocks = new HashSet<Block /*!*/>();
-    Stack<Block /*!*/> dfsStack = new Stack<Block /*!*/>();
-    dfsStack.Push(impl.Blocks[0]);
+    var visitedBlocks = new HashSet<Block /*!*/>();
+    var result = new HashSet<Block>();
+    var dfsStack = new Stack<Block>();
+    dfsStack.Push(rootBlock);
     while (dfsStack.Count > 0)
     {
-      Block /*!*/
-        b = dfsStack.Pop();
-      Contract.Assert(b != null);
-      if (visitedBlocks.Contains(b))
+      var /*!*/ block = dfsStack.Pop();
+      Contract.Assert(block != null);
+      if (!visitedBlocks.Add(block))
       {
-        multiPredBlocks.Add(b);
+        result.Add(block);
         continue;
       }
 
-      visitedBlocks.Add(b);
-      if (b.TransferCmd == null)
+      if (block.TransferCmd == null)
       {
         continue;
       }
 
-      if (b.TransferCmd is ReturnCmd)
+      if (block.TransferCmd is ReturnCmd)
       {
         continue;
       }
 
-      Contract.Assert(b.TransferCmd is GotoCmd);
-      GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
+      Contract.Assert(block.TransferCmd is GotoCmd);
+      var gotoCmd = (GotoCmd) block.TransferCmd;
       if (gotoCmd.labelTargets == null)
       {
         continue;
       }
 
-      foreach (Block /*!*/ succ in gotoCmd.labelTargets)
+      foreach (var /*!*/ succ in gotoCmd.labelTargets)
       {
         Contract.Assert(succ != null);
         dfsStack.Push(succ);
       }
     }
 
-    return multiPredBlocks;
+    return result;
   }
 
   public override Implementation VisitImplementation(Implementation impl)
   {
-    //Contract.Requires(impl != null);
-    Contract.Ensures(Contract.Result<Implementation>() != null);
-    //Console.WriteLine("Procedure {0}", impl.Name);
-    //Console.WriteLine("Initial number of blocks = {0}", impl.Blocks.Count);
-
-    HashSet<Block /*!*/> multiPredBlocks = ComputeMultiPredecessorBlocks(impl);
-    Contract.Assert(cce.NonNullElements(multiPredBlocks));
-    HashSet<Block /*!*/> visitedBlocks = new HashSet<Block /*!*/>();
-    HashSet<Block /*!*/> removedBlocks = new HashSet<Block /*!*/>();
-    Stack<Block /*!*/> dfsStack = new Stack<Block /*!*/>();
-    dfsStack.Push(impl.Blocks[0]);
-    while (dfsStack.Count > 0)
+    var newBlocks = CoalesceFromRootBlock(impl.Blocks);
+    impl.Blocks = newBlocks;
+    foreach (var block in impl.Blocks)
     {
-      Block /*!*/
-        b = dfsStack.Pop();
-      Contract.Assert(b != null);
-      if (visitedBlocks.Contains(b))
+      if (block.TransferCmd is ReturnCmd)
       {
         continue;
       }
 
-      visitedBlocks.Add(b);
-      if (b.TransferCmd == null)
+      var gotoCmd = (GotoCmd)block.TransferCmd;
+      gotoCmd.labelNames = new List<string>();
+      foreach (var successor in gotoCmd.labelTargets)
+      {
+        gotoCmd.labelNames.Add(successor.Label);
+      }
+    }
+    return impl;
+  }
+
+  public static List<Block> CoalesceFromRootBlock(List<Block> blocks)
+  {
+    if (!blocks.Any())
+    {
+      return blocks;
+    }
+    var multiPredecessorBlocks = ComputeMultiPredecessorBlocks(blocks[0]);
+    Contract.Assert(cce.NonNullElements(multiPredecessorBlocks));
+    var visitedBlocks = new HashSet<Block>();
+    var removedBlocks = new HashSet<Block>();
+    var toVisit = new Stack<Block>();
+    toVisit.Push(blocks[0]);
+    while (toVisit.Count > 0)
+    {
+      var block = toVisit.Pop();
+      Contract.Assert(block != null);
+      if (!visitedBlocks.Add(block))
       {
         continue;
       }
 
-      if (b.TransferCmd is ReturnCmd)
+      if (block.TransferCmd == null)
       {
         continue;
       }
 
-      Contract.Assert(b.TransferCmd is GotoCmd);
-      GotoCmd gotoCmd = (GotoCmd) b.TransferCmd;
+      if (block.TransferCmd is ReturnCmd)
+      {
+        continue;
+      }
+
+      Contract.Assert(block.TransferCmd is GotoCmd);
+      var gotoCmd = (GotoCmd) block.TransferCmd;
       if (gotoCmd.labelTargets == null)
       {
         continue;
       }
 
-      if (gotoCmd.labelTargets.Count == 1)
+      if (gotoCmd.labelTargets.Count != 1)
       {
-        Block /*!*/
-          succ = cce.NonNull(gotoCmd.labelTargets[0]);
-        if (!multiPredBlocks.Contains(succ))
+        foreach (var aSuccessor in gotoCmd.labelTargets)
         {
-          foreach (Cmd /*!*/ cmd in succ.Cmds)
-          {
-            Contract.Assert(cmd != null);
-            b.Cmds.Add(cmd);
-          }
-
-          b.TransferCmd = succ.TransferCmd;
-          if (!b.tok.IsValid && succ.tok.IsValid)
-          {
-            b.tok = succ.tok;
-            b.Label = succ.Label;
-          }
-
-          removedBlocks.Add(succ);
-          dfsStack.Push(b);
-          visitedBlocks.Remove(b);
-          continue;
+          Contract.Assert(aSuccessor != null);
+          toVisit.Push(aSuccessor);
         }
+        continue;
       }
 
-      foreach (Block /*!*/ succ in gotoCmd.labelTargets)
+      var successor = cce.NonNull(gotoCmd.labelTargets[0]);
+      if (multiPredecessorBlocks.Contains(successor))
       {
-        Contract.Assert(succ != null);
-        dfsStack.Push(succ);
+        toVisit.Push(successor);
+        continue;
       }
-    }
 
-    List<Block /*!*/> newBlocks = new List<Block /*!*/>();
-    foreach (Block /*!*/ b in impl.Blocks)
-    {
-      Contract.Assert(b != null);
-      if (visitedBlocks.Contains(b) && !removedBlocks.Contains(b))
+      block.Cmds.AddRange(successor.Cmds);
+      block.TransferCmd = successor.TransferCmd;
+      if (!block.tok.IsValid && successor.tok.IsValid)
       {
-        newBlocks.Add(b);
+        block.tok = successor.tok;
+        block.Label = successor.Label;
       }
+
+      removedBlocks.Add(successor);
+      toVisit.Push(block);
+      visitedBlocks.Remove(block);
     }
 
-    impl.Blocks = newBlocks;
-    foreach (Block b in impl.Blocks)
+    var newBlocks = new List<Block>();
+    foreach (var block in blocks)
     {
-      if (b.TransferCmd is ReturnCmd)
-      {
-        continue;
-      }
-
-      GotoCmd gotoCmd = b.TransferCmd as GotoCmd;
-      gotoCmd.labelNames = new List<string>();
-      foreach (Block succ in gotoCmd.labelTargets)
+      Contract.Assert(block != null);
+      if (visitedBlocks.Contains(block) && !removedBlocks.Contains(block))
       {
-        gotoCmd.labelNames.Add(succ.Label);
+        newBlocks.Add(block);
       }
     }
-
-    // Console.WriteLine("Final number of blocks = {0}", impl.Blocks.Count);
-    return impl;
+    return newBlocks;
   }
 }

Source/Core/Analysis/LiveVariableAnalysis/GenKillWeight.cs

@@ -1,4 +1,4 @@
-using System.Collections.Generic;
+using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 
 namespace Microsoft.Boogie;

Source/Core/Analysis/LiveVariableAnalysis/InterProcGenKill.cs

@@ -4,7 +4,6 @@
 
 namespace Microsoft.Boogie
 {
-  // Interprocedural Gen/Kill Analysis
   public class InterProcGenKill
   {
     private CoreOptions options;
@@ -554,19 +553,6 @@ public void Compute()
         varsLiveAtEntry.Add(cfg.impl.Name, lv);
         varsLiveSummary.Add(cfg.impl.Name, cfg.summary);
       }
-
-      /*
-      foreach(Block/*!*/
-      /* b in mainImpl.Blocks){
-Contract.Assert(b != null);
-//Set<Variable!> lv = cfg.weightBefore[b].getLiveVars();
-b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b];
-//foreach(GlobalVariable/*!*/
-      /* v in program.GlobalVariables){Contract.Assert(v != null);
-//  b.liveVarsBefore.Add(v);
-//}
-}
-*/
     }
 
     // Called when summaries have already been computed

Source/ExecutionEngine/ExecutionEngine.cs

@@ -224,7 +224,7 @@ public void CoalesceBlocks(Program program)
           Options.OutputWriter.WriteLine("Coalescing blocks...");
         }
 
-        Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+        BlockCoalescer.CoalesceBlocks(program);
       }
     }
 
@@ -240,7 +240,7 @@ public void CollectModSets(Program program)
 
     public void EliminateDeadVariables(Program program)
     {
-      Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+      UnusedVarEliminator.Eliminate(program);
     }
 
     public void PrintBplFile(string filename, Program program, 
@@ -737,14 +737,15 @@ public async Task<IReadOnlyList<IVerificationTask>> GetVerificationTasks(Program
         var writer = TextWriter.Null;
         var vcGenerator = new VerificationConditionGenerator(processedProgram.Program, CheckerPool);
 
+
         var run = new ImplementationRun(implementation, writer);
         var collector = new VerificationResultCollector(Options);
         vcGenerator.PrepareImplementation(run, collector, out _,
           out var gotoCmdOrigins,
           out var modelViewInfo);
 
         ConditionGeneration.ResetPredecessors(run.Implementation.Blocks);
-        var splits = ManualSplitFinder.FocusAndSplit(Options, run, gotoCmdOrigins, vcGenerator).ToList();
+        var splits = ManualSplitFinder.FocusAndSplit(program, Options, run, gotoCmdOrigins, vcGenerator).ToList();
         for (var index = 0; index < splits.Count; index++) {
           var split = splits[index];
           split.SplitIndex = index;

Source/ExecutionEngine/VerificationTask.cs

@@ -44,7 +44,7 @@ public VerificationTask(ExecutionEngine engine, ProcessedProgram processedProgra
 
   public IVerificationTask FromSeed(int newSeed)
   {
-    var split = new ManualSplit(Split.Options, Split.Blocks, Split.GotoCmdOrigins, 
+    var split = new ManualSplit(Split.Options, () => Split.Blocks, Split.GotoCmdOrigins, 
       Split.parent, Split.Run, Split.Token, newSeed);
     split.SplitIndex = Split.SplitIndex;
     return new VerificationTask(engine, ProcessedProgram, split, modelViewInfo);

Source/UnitTests/ExecutionEngineTests/ExecutionEngineTest.cs

@@ -99,9 +99,9 @@ procedure Procedure(y: int)
     var tasks = await engine.GetVerificationTasks(program);
 
     // The first split is empty. Maybe it can be optimized away
-    Assert.AreEqual(5, tasks.Count);
+    Assert.AreEqual(4, tasks.Count);
 
-    var outcomes = new List<SolverOutcome> { SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid };
+    var outcomes = new List<SolverOutcome> { SolverOutcome.Invalid, SolverOutcome.Valid, SolverOutcome.Invalid, SolverOutcome.Valid };
     for (var index = 0; index < outcomes.Count; index++)
     {
       var result0 = await tasks[index].TryRun()!.ToTask();