Add support for irreducible CFG

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,9 @@ 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;
+  }
 }

Source/Graph/Graph.cs

@@ -994,6 +994,10 @@ static HashSet<Node> FindCycle(Graph<Node> g, Node source)
             {
               return ret;
             }
+            else
+            {
+              ret.Add(x);
+            }
           }
         }
 

Source/VCGeneration/Transformations/RemoveBackEdges.cs

@@ -2,6 +2,7 @@
 using System.Collections.Generic;
 using System.Diagnostics;
 using System.Diagnostics.Contracts;
+using System.Linq;
 using Microsoft.Boogie;
 using Microsoft.Boogie.GraphUtil;
 using VC;
@@ -73,6 +74,115 @@ public void ConvertCfg2Dag(ImplementationRun run, Dictionary<Block, List<Block>>
 
     #endregion
   }
+  private static void SubstituteBranchTargets(Block b, Dictionary<Block, Block> subst)
+  {
+    TransferCmd transferCmd = b.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);
+      }      
+    }
+  }
+
+  private static Block DuplicateBlock(Block b, Dictionary<Block, int> nextLabels)
+  {
+    List<Cmd> dupCmds = new List<Cmd>();
+    b.Cmds.ForEach(dupCmds.Add);
+
+    TransferCmd splitTransferCmd = b.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, b.Label + "_dup_" + nextLabels[b], dupCmds, dupTransferCmd);
+    nextLabels[b]++;
+    nextLabels.Add(dupBlock, 0);
+    return dupBlock;
+  }
+  private Graph<Block> ConvertToReducible(Implementation impl)
+  {
+    Dictionary<Block, int> nextLabels = impl.Blocks.ToDictionary(b => b, _ => 0);
+    Graph<Block> g = Program.GraphFromImpl(impl);
+    impl.ComputePredecessorsForBlocks();
+    g.ComputeLoops(); // this is the call that does all of the processing
+    while (!g.Reducible)
+    {
+      // We will be looking for a block that can be split, and for a looply connected block that has an invariant
+      Block splitBlock = g.SplitCandidates
+        .FirstOrDefault(b => b.Predecessors.Count > 1 && !b.HasInvariant())
+        ?? g.SplitCandidates.FirstOrDefault(b => b.Predecessors.Count > 1);
+
+      // splitBlock should be a perfectly good split candidate now.
+      // We have to find the nodes that are dominated by it, to duplicate them too
+      List<Block> region = [.. impl.Blocks.Where(b => g.DominatorMap.DominatedBy(b, splitBlock))];
+      foreach (Block pred in splitBlock.Predecessors)
+      {
+        if (g.DominatorMap.DominatedBy(pred, splitBlock))
+        {
+          continue;
+        }
+
+        // duplicate the splitBlock
+        Block dupBlock = DuplicateBlock(splitBlock, nextLabels);
+
+        // Remove edge of the previous block
+        GotoCmd predGoto = (GotoCmd)pred.TransferCmd;
+        predGoto.RemoveTarget(splitBlock);
+
+        // Update the edge for the duplicate
+        predGoto.AddTarget(dupBlock);
+
+        // Add the duplicate block to the implementation
+        impl.Blocks.Add(dupBlock);
+
+        // duplicate the whole region
+        Dictionary<Block, Block> duplicatesDict = new Dictionary<Block, Block>
+        {
+          { splitBlock, dupBlock }
+        };
+
+        foreach (Block currentBlock in region)
+        {
+          if (currentBlock != splitBlock)
+          {
+            Block newBlock = DuplicateBlock(currentBlock, nextLabels);
+            impl.Blocks.Add(newBlock);
+            duplicatesDict[currentBlock] = newBlock;
+          }
+        }
+
+        // Replace the blocks in the region with their duplicates
+        duplicatesDict.Values.ForEach(b => SubstituteBranchTargets(b, duplicatesDict));
+      }
+
+      impl.PruneUnreachableBlocks(generator.Options);
+      impl.ComputePredecessorsForBlocks();
+      g = Program.GraphFromImpl(impl);
+      g.ComputeLoops();
+    }
+
+    return g;
+  }
 
   private void ConvertCfg2DagStandard(Implementation impl, Dictionary<Block, List<Block>> edgesCut, int taskID)
   {
@@ -82,18 +192,13 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary<Block, List<
 
     #region Create the graph by adding the source node and each edge
 
-    Graph<Block> g = Program.GraphFromImpl(impl);
+    // Graph<Block> g = Program.GraphFromImpl(impl);
+    Graph<Block> g = ConvertToReducible(impl);
 
     #endregion
 
     //Graph<Block> g = program.ProcessLoops(impl);
 
-    g.ComputeLoops(); // this is the call that does all of the processing
-    if (!g.Reducible)
-    {
-      throw new VCGenException("Irreducible flow graphs are unsupported.");
-    }
-
     #endregion
 
     #region Cut the backedges, push assert/assume statements from loop header into predecessors, change them all into assume statements at top of loop, introduce havoc statements
@@ -112,25 +217,32 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary<Block, List<
 
       List<Cmd> prefixOfPredicateCmdsInit = new List<Cmd>();
       List<Cmd> prefixOfPredicateCmdsMaintained = new List<Cmd>();
-      for (int i = 0, n = header.Cmds.Count; i < n; i++) {
-        if (header.Cmds[i] is not PredicateCmd predicateCmd) {
-          if (header.Cmds[i] is CommentCmd) {
+      for (int i = 0, n = header.Cmds.Count; i < n; i++)
+      {
+        if (header.Cmds[i] is not PredicateCmd predicateCmd)
+        {
+          if (header.Cmds[i] is CommentCmd)
+          {
             // ignore
             continue;
           }
 
           break; // stop when an assignment statement (or any other non-predicate cmd) is encountered
         }
 
-        if (predicateCmd is AssertCmd assertCmd) {
+        if (predicateCmd is AssertCmd assertCmd)
+        {
           AssertCmd initAssertCmd;
 
-          if (generator.Options.ConcurrentHoudini) {
+          if (generator.Options.ConcurrentHoudini)
+          {
             Contract.Assert(taskID >= 0);
             initAssertCmd = generator.Options.Cho[taskID].DisableLoopInvEntryAssert
               ? new LoopInitAssertCmd(assertCmd.tok, Expr.True, assertCmd)
               : new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
-          } else {
+          }
+          else
+          {
             initAssertCmd = new LoopInitAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
           }
 
@@ -143,12 +255,15 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary<Block, List<
           prefixOfPredicateCmdsInit.Add(initAssertCmd);
 
           LoopInvMaintainedAssertCmd maintainedAssertCmd;
-          if (generator.Options.ConcurrentHoudini) {
+          if (generator.Options.ConcurrentHoudini)
+          {
             Contract.Assert(taskID >= 0);
             maintainedAssertCmd = generator.Options.Cho[taskID].DisableLoopInvMaintainedAssert
               ? new LoopInvMaintainedAssertCmd(assertCmd.tok, Expr.True, assertCmd)
               : new LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
-          } else {
+          }
+          else
+          {
             maintainedAssertCmd = new LoopInvMaintainedAssertCmd(assertCmd.tok, assertCmd.Expr, assertCmd);
           }
 
@@ -166,9 +281,12 @@ private void ConvertCfg2DagStandard(Implementation impl, Dictionary<Block, List<
             id => new TrackedInvariantAssumed(id));
 
           header.Cmds[i] = assume;
-        } else {
+        }
+        else
+        {
           Contract.Assert(predicateCmd is AssumeCmd);
-          if (generator.Options.AlwaysAssumeFreeLoopInvariants) {
+          if (generator.Options.AlwaysAssumeFreeLoopInvariants)
+          {
             // Usually, "free" stuff, like free loop invariants (and the assume statements
             // that stand for such loop invariants) are ignored on the checking side.  This
             // command-line option changes that behavior to always assume the conditions.
@@ -324,16 +442,10 @@ private void ConvertCfg2DagkInduction(Implementation impl, Dictionary<Block, Lis
 
       #region Create the graph by adding the source node and each edge
 
-      Graph<Block> g = Program.GraphFromImpl(impl);
+      Graph<Block> g = ConvertToReducible(impl);
 
       #endregion
 
-      g.ComputeLoops(); // this is the call that does all of the processing
-      if (!g.Reducible)
-      {
-        throw new VCGenException("Irreducible flow graphs are unsupported.");
-      }
-
       #endregion
 
       foreach (Block header in Cce.NonNull(g.Headers))

Test/irreduciblecfg/Await.bpl

@@ -0,0 +1,44 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+var new: int;
+procedure await_eq_add(val : int)
+    modifies new;
+    ensures val == old(val);
+    ensures (new == old(new) + val);
+{
+    var x : int;
+    var tmp : bool;
+    assume tmp == true;
+    B: 
+        havoc x;
+        if (x == val) {
+            goto E;
+        }
+        else {
+            goto C;
+        }
+    C: 
+        if (tmp == true) {
+            havoc x;
+        }
+        goto D;
+    D: 
+        if (x != val) {
+            goto C;
+        }
+        else {
+            goto E;
+        }
+    E:
+        havoc tmp;
+        if (tmp == true) {
+            new := new + x;
+            goto G;
+        }
+        else {
+            goto C;
+        }
+    G:
+}

Test/irreduciblecfg/BackEdgeCounter.bpl

@@ -0,0 +1,26 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure irreducible() {
+    var i: int;
+    var j: int;
+
+    i := 1;
+    goto B1, B4;
+
+    B1:
+        assume j > 0;
+        goto B2;
+
+    B2:
+        assert i > 0;
+        goto B3;
+
+    B3:
+        assert j > 0;
+        goto B4;
+
+    B4:
+        i := i+1;
+        goto B2;
+}

Test/irreduciblecfg/BackEdgeCounter.bpl.expect

@@ -0,0 +1,5 @@
+BackEdgeCounter.bpl(20,9): Error: this loop invariant could not be proved on entry
+Execution trace:
+    BackEdgeCounter.bpl(8,7): anon0
+
+Boogie program verifier finished with 0 verified, 1 error

Test/irreduciblecfg/Canonical.bpl

@@ -0,0 +1,11 @@
+// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L: Boogie program verifier finished with 1 verified, 0 errors
+
+procedure Irreducible ()
+{
+A: goto B,C;
+B: goto C,D;
+C: goto B;
+D: return;
+}