Add support for irreducible CFG (#1032)

This PR addresses Issue #921.

**Added:**

Conversion of irreducible flow graphs by _Node Splitting_ (see Dragon
book section 9.7.6). For every irreducible loop found, we duplicate one
of the nodes (we first try to duplicate one that does not have
invariants, if that exists) and all of the nodes that it dominates.

 **Tests:**
The former _Irreducible.bpl_ test from _test0_ has been dropped and a
new dedicated directory has been created: _irreduciblecfg_. 6 other
test-cases have been added:

-  _Canonical.bpl_: similar to the previous Irreducible.bpl
- _BackEdgeCounter.bpl_: A test case provided by @gauravpartha on the
corresponding issue to justify why _Back Edge Elimination_ shouldn't be
done directly on irreducible CFGs.
- _CanonicalConditions.bpl_: A simple canonical irreducible CFG with
some conditions
- _Tangled.bpl_: A larger irreducible CFG that has to maintain an
invariant
- _Unsound.bpl_: A while + goto example provided by @petemud on the
corresponding issue. It previously gave a false positive with the
/extractLoops option. With the current approach, the failing trace is
successfully identified.
- _Await.bpl_: A simplified and slightly modified version of the example
that we initially wanted to verify when we opened the issue.

---------

Co-authored-by: Shaz Qadeer <[email protected]>

Author: radumcostache

Source/Core/AST/GotoBoogie/Block.cs

@@ -7,7 +7,7 @@ namespace Microsoft.Boogie;
 
 public sealed class Block : Absy
 {
-  
+
   public string Label { get; set; } // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
 
   [Rep]
@@ -49,7 +49,6 @@ public enum VisitState
   public int SuccCount;
 
   private HashSet<Variable> liveVarsBefore;
-
   public IEnumerable<Variable> LiveVarsBefore
   {
     get
@@ -97,10 +96,11 @@ public bool IsLive(Variable v)
     return LiveVarsBefore.Contains(v);
   }
 
-  public static Block ShallowClone(Block block) {
+  public static Block ShallowClone(Block block)
+  {
     return new Block(block.tok, block.Label, block.Cmds, block.TransferCmd);
   }
-  
+
   public Block(IToken tok, TransferCmd cmd)
     : this(tok, "", new List<Cmd>(), new ReturnCmd(tok))
   {
@@ -196,4 +196,55 @@ public override Absy StdDispatch(StandardVisitor visitor)
     Contract.Ensures(Contract.Result<Absy>() != null);
     return visitor.VisitBlock(this);
   }
+
+  public bool HasInvariant()
+  {
+    return Cmds.Count >= 1 && Cmds[0] is AssertCmd;
+  }
+  
+  public void SubstituteBranchTargets(Dictionary<Block, Block> subst)
+  {
+    TransferCmd transferCmd = this.TransferCmd;
+    if (transferCmd is not GotoCmd)
+    {
+      return;
+    }
+
+    GotoCmd gotoCmd = (GotoCmd)transferCmd;
+    foreach (Block currentBlock in gotoCmd.LabelTargets.ToList())
+    {
+      if (subst.TryGetValue(currentBlock, out Block dupBlock))
+      {
+        gotoCmd.RemoveTarget(currentBlock);
+        gotoCmd.AddTarget(dupBlock);
+      }
+    }
+  }
+
+  public Block DuplicateBlock(Dictionary<Block, int> nextLabels)
+  {
+    List<Cmd> dupCmds = new List<Cmd>();
+    this.Cmds.ForEach(dupCmds.Add);
+
+    TransferCmd splitTransferCmd = this.TransferCmd;
+    TransferCmd dupTransferCmd;
+
+    if (splitTransferCmd is not GotoCmd)
+    {
+      dupTransferCmd = new ReturnCmd(Token.NoToken);
+    }
+    else
+    {
+      List<string> dupLabelNames = [.. ((GotoCmd)splitTransferCmd).LabelNames];
+      List<Block> dupLabelTargets = new List<Block>();
+      ((GotoCmd)splitTransferCmd).LabelTargets.ForEach(dupLabelTargets.Add);
+
+      dupTransferCmd = new GotoCmd(Token.NoToken, dupLabelNames, dupLabelTargets);
+    }
+
+    Block dupBlock = new Block(Token.NoToken, this.Label + "_dup_" + nextLabels[this], dupCmds, dupTransferCmd);
+    nextLabels[this]++;
+    nextLabels.Add(dupBlock, 0);
+    return dupBlock;
+  }
 }