Move classes into separate files and some methods into separate classes

Source/Houdini/HoudiniSession.cs

@@ -129,7 +129,7 @@ public class HoudiniStatistics
     public HashSet<TrackedNodeComponent> CoveredElements { get; } = new();
     private VCExpr conjecture;
     private ProverInterface.ErrorHandler handler;
-    ConditionGeneration.VerificationResultCollector collector;
+    VerificationResultCollector collector;
     HashSet<Variable> unsatCoreSet;
     HashSet<Variable> houdiniConstants;
     public HashSet<Variable> houdiniAssertConstants;
@@ -163,7 +163,7 @@ public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterf
       this.Description = impl.Name;
       this.houdini = houdini;
       this.stats = stats;
-      collector = new ConditionGeneration.VerificationResultCollector(houdini.Options);
+      collector = new VerificationResultCollector(houdini.Options);
       collector.OnProgress?.Invoke("HdnVCGen", 0, 0, 0.0);
 
       vcgen.ConvertCFG2DAG(run, taskID: taskID);

Source/VCGeneration/BlockListComparer.cs

@@ -0,0 +1,29 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using Microsoft.Boogie;
+
+namespace VC;
+
+class BlockListComparer : IEqualityComparer<List<Block>>
+{
+  public bool Equals(List<Block> x, List<Block> y)
+  {
+    return x == y || x.SequenceEqual(y);
+  }
+
+  public int GetHashCode(List<Block> obj)
+  {
+    int h = 0;
+    Contract.Assume(obj != null);
+    foreach (var b in obj)
+    {
+      if (b != null)
+      {
+        h += b.GetHashCode();
+      }
+    }
+
+    return h;
+  }
+}

Source/VCGeneration/BlockStats.cs

@@ -0,0 +1,40 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
+
+namespace VC;
+
+class BlockStats
+{
+  public bool bigBlock;
+  public int id;
+  public double assertionCost;
+  public double assumptionCost; // before multiplier
+  public double incomingPaths;
+
+  public List<Block> /*!>!*/
+    virtualSuccessors = new List<Block>();
+
+  public List<Block> /*!>!*/
+    virtualPredecessors = new List<Block>();
+
+  public HashSet<Block> reachableBlocks;
+  public readonly Block block;
+
+  [ContractInvariantMethod]
+  void ObjectInvariant()
+  {
+    Contract.Invariant(cce.NonNullElements(virtualSuccessors));
+    Contract.Invariant(cce.NonNullElements(virtualPredecessors));
+    Contract.Invariant(block != null);
+  }
+
+
+  public BlockStats(Block b, int i)
+  {
+    Contract.Requires(b != null);
+    block = b;
+    assertionCost = -1;
+    id = i;
+  }
+}

Source/VCGeneration/BlockTransformations.cs

@@ -0,0 +1,64 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using Microsoft.Boogie;
+
+namespace VCGeneration;
+
+public static class BlockTransformations
+{
+    public static List<Block> PostProcess(List<Block> blocks)
+    {
+      void DeleteFalseGotos (Block b)
+      {
+        var firstFalseIdx = b.Cmds.FindIndex(IsAssumeFalse);
+        if (firstFalseIdx != -1)
+        {
+          b.Cmds = b.Cmds.Take(firstFalseIdx + 1).ToList();
+          b.TransferCmd = (b.TransferCmd is GotoCmd) ? new ReturnCmd(b.tok) : b.TransferCmd;
+        }
+
+        return;
+
+        bool IsAssumeFalse (Cmd c) { return c is AssumeCmd ac && ac.Expr is LiteralExpr le && !le.asBool; }
+      }
+
+      bool ContainsAssert(Block b)
+      {
+        return b.Cmds.Exists(IsNonTrivialAssert);
+        bool IsNonTrivialAssert (Cmd c) { return c is AssertCmd ac && !(ac.Expr is LiteralExpr le && le.asBool); }
+      }
+
+      blocks.ForEach(DeleteFalseGotos); // make blocks ending in assume false leaves of the CFG-DAG -- this is probably unnecessary, may have been done previously
+      var todo = new Stack<Block>();
+      var peeked = new HashSet<Block>();
+      var interestingBlocks = new HashSet<Block>();
+      todo.Push(blocks[0]);
+      while(todo.Any())
+      {
+        var currentBlock = todo.Peek();
+        var pop = peeked.Contains(currentBlock);
+        peeked.Add(currentBlock);
+        var interesting = false;
+        var exit = currentBlock.TransferCmd as GotoCmd;
+        if (exit != null && !pop) {
+          exit.labelTargets.ForEach(b => todo.Push(b));
+        } else if (exit != null) {
+          Contract.Assert(pop);
+          var gtc = new GotoCmd(exit.tok, exit.labelTargets.Where(l => interestingBlocks.Contains(l)).ToList());
+          currentBlock.TransferCmd = gtc;
+          interesting = interesting || gtc.labelTargets.Count() != 0;
+        }
+        if (pop)
+        {
+          interesting = interesting || ContainsAssert(currentBlock);
+          if (interesting) {
+            interestingBlocks.Add(currentBlock);
+          }
+          todo.Pop();
+        }
+      }
+      interestingBlocks.Add(blocks[0]); // must not be empty
+      return blocks.Where(b => interestingBlocks.Contains(b)).ToList(); // this is not the same as interestingBlocks.ToList() because the resulting lists will have different orders.
+    }
+}

Source/VCGeneration/CommandTransformations.cs

@@ -0,0 +1,17 @@
+using Microsoft.Boogie;
+using VC;
+
+namespace VCGeneration;
+
+public class CommandTransformations
+{
+  public static Cmd AssertIntoAssume(VCGenOptions options, Cmd c)
+  {
+    if (c is AssertCmd assrt)
+    {
+      return VCGen.AssertTurnedIntoAssume(options, assrt);
+    }
+
+    return c;
+  }
+}

Source/VCGeneration/ConditionGeneration.cs

@@ -1,7 +1,6 @@
 using System;
 using System.Linq;
 using System.Collections;
-using System.Collections.Concurrent;
 using System.Collections.Generic;
 using System.Diagnostics;
 using System.Threading;
@@ -511,46 +510,6 @@ public virtual void Close()
     }
 
 
-    public class VerificationResultCollector : VerifierCallback
-    {
-      private readonly VCGenOptions options;
-
-      public VerificationResultCollector(VCGenOptions options) : base(options.PrintProverWarnings)
-      {
-        this.options = options;
-      }
-
-      [ContractInvariantMethod]
-      void ObjectInvariant()
-      {
-        Contract.Invariant(cce.NonNullElements(examples));
-        Contract.Invariant(cce.NonNullElements(vcResults));
-      }
-
-      public readonly ConcurrentQueue<Counterexample> examples = new();
-      public readonly ConcurrentQueue<VerificationRunResult> vcResults = new();
-
-      public override void OnCounterexample(Counterexample ce, string /*?*/ reason)
-      {
-        //Contract.Requires(ce != null);
-        ce.InitializeModelStates();
-        examples.Enqueue(ce);
-      }
-
-      public override void OnUnreachableCode(ImplementationRun run)
-      {
-        //Contract.Requires(impl != null);
-        run.OutputWriter.WriteLine("found unreachable code:");
-        EmitImpl(options, run, false);
-        // TODO report error about next to last in seq
-      }
-
-      public override void OnVCResult(VerificationRunResult result)
-      {
-        vcResults.Enqueue(result);
-      }
-    }
-
     public static void EmitImpl(VCGenOptions options, ImplementationRun run, bool printDesugarings)
     {
       var impl = run.Implementation;

Source/VCGeneration/FocusAttribute.cs

@@ -0,0 +1,139 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using Microsoft.Boogie;
+using VC;
+using Block = Microsoft.Boogie.Block;
+using Cmd = Microsoft.Boogie.Cmd;
+using PredicateCmd = Microsoft.Boogie.PredicateCmd;
+using QKeyValue = Microsoft.Boogie.QKeyValue;
+using ReturnCmd = Microsoft.Boogie.ReturnCmd;
+using TransferCmd = Microsoft.Boogie.TransferCmd;
+using VCGenOptions = Microsoft.Boogie.VCGenOptions;
+
+namespace VCGeneration;
+
+public static class FocusAttribute
+{
+  public static List<Split> FocusImpl(VCGenOptions options, ImplementationRun run, Dictionary<TransferCmd, ReturnCmd> gotoCmdOrigins, VCGen par)
+  {
+    bool IsFocusCmd(Cmd c) {
+      return c is PredicateCmd p && QKeyValue.FindBoolAttribute(p.Attributes, "focus");
+    }
+
+    List<Block> GetFocusBlocks(List<Block> blocks) {
+      return blocks.Where(blk => blk.Cmds.Any(c => IsFocusCmd(c))).ToList();
+    }
+
+    var impl = run.Implementation;
+    var dag = Program.GraphFromImpl(impl);
+    var topoSorted = dag.TopologicalSort().ToList();
+    // By default, we process the foci in a top-down fashion, i.e., in the topological order.
+    // If the user sets the RelaxFocus flag, we use the reverse (topological) order.
+    var focusBlocks = GetFocusBlocks(topoSorted);
+    if (par.CheckerPool.Options.RelaxFocus) {
+      focusBlocks.Reverse();
+    }
+    if (!focusBlocks.Any()) {
+      var f = new List<Split>();
+      f.Add(new Split(options, impl.Blocks, gotoCmdOrigins, par, run));
+      return f;
+    }
+    // finds all the blocks dominated by focusBlock in the subgraph
+    // which only contains vertices of subgraph.
+    HashSet<Block> DominatedBlocks(Block focusBlock, IEnumerable<Block> subgraph)
+    {
+      var dominators = new Dictionary<Block, HashSet<Block>>();
+      var todo = new Queue<Block>();
+      foreach (var b in topoSorted.Where(blk => subgraph.Contains(blk)))
+      {
+        var s = new HashSet<Block>();
+        var pred = b.Predecessors.Where(subgraph.Contains).ToList();
+        if (pred.Count != 0)
+        {
+          s.UnionWith(dominators[pred[0]]);
+          pred.ForEach(blk => s.IntersectWith(dominators[blk]));
+        }
+        s.Add(b);
+        dominators[b] = s;
+      }
+      return subgraph.Where(blk => dominators[blk].Contains(focusBlock)).ToHashSet();
+    }
+
+    Cmd DisableSplits(Cmd c)
+    {
+      if (c is PredicateCmd pc)
+      {
+        for (var kv = pc.Attributes; kv != null; kv = kv.Next)
+        {
+          if (kv.Key == "split")
+          {
+            kv.AddParam(new LiteralExpr(Token.NoToken, false));
+          }
+        }
+      }
+      return c;
+    }
+
+    var Ancestors = new Dictionary<Block, HashSet<Block>>();
+    var Descendants = new Dictionary<Block, HashSet<Block>>();
+    focusBlocks.ForEach(fb => Ancestors[fb] = dag.ComputeReachability(fb, false).ToHashSet());
+    focusBlocks.ForEach(fb => Descendants[fb] = dag.ComputeReachability(fb, true).ToHashSet());
+    var s = new List<Split>();
+    var duplicator = new Duplicator();
+    void FocusRec(int focusIdx, IEnumerable<Block> blocks, IEnumerable<Block> freeBlocks)
+    {
+      if (focusIdx == focusBlocks.Count())
+      {
+        // it is important for l to be consistent with reverse topological order.
+        var l = dag.TopologicalSort().Where(blk => blocks.Contains(blk)).Reverse();
+        // assert that the root block, impl.Blocks[0], is in l
+        Contract.Assert(l.ElementAt(l.Count() - 1) == impl.Blocks[0]);
+        var newBlocks = new List<Block>();
+        var oldToNewBlockMap = new Dictionary<Block, Block>(blocks.Count());
+        foreach (Block b in l)
+        {
+          var newBlock = (Block)duplicator.Visit(b);
+          newBlocks.Add(newBlock);
+          oldToNewBlockMap[b] = newBlock;
+          // freeBlocks consist of the predecessors of the relevant foci.
+          // Their assertions turn into assumes and any splits inside them are disabled.
+          if(freeBlocks.Contains(b))
+          {
+            newBlock.Cmds = b.Cmds.Select(c => CommandTransformations.AssertIntoAssume(options, c)).Select(c => DisableSplits(c)).ToList();
+          }
+          if (b.TransferCmd is GotoCmd gtc)
+          {
+            var targets = gtc.labelTargets.Where(blk => blocks.Contains(blk));
+            newBlock.TransferCmd = new GotoCmd(gtc.tok,
+                                          targets.Select(blk => oldToNewBlockMap[blk].Label).ToList(),
+                                          targets.Select(blk => oldToNewBlockMap[blk]).ToList());
+          }
+        }
+        newBlocks.Reverse();
+        Contract.Assert(newBlocks[0] == oldToNewBlockMap[impl.Blocks[0]]);
+        s.Add(new Split(options, BlockTransformations.PostProcess(newBlocks), gotoCmdOrigins, par, run));
+      }
+      else if (!blocks.Contains(focusBlocks[focusIdx])
+                || freeBlocks.Contains(focusBlocks[focusIdx]))
+      {
+        FocusRec(focusIdx + 1, blocks, freeBlocks);
+      }
+      else
+      {
+        var b = focusBlocks[focusIdx]; // assert b in blocks
+        var dominatedBlocks = DominatedBlocks(b, blocks);
+        // the first part takes all blocks except the ones dominated by the focus block
+        FocusRec(focusIdx + 1, blocks.Where(blk => !dominatedBlocks.Contains(blk)), freeBlocks);
+        var ancestors = Ancestors[b];
+        ancestors.Remove(b);
+        var descendants = Descendants[b];
+        // the other part takes all the ancestors, the focus block, and the descendants.
+        FocusRec(focusIdx + 1, ancestors.Union(descendants).Intersect(blocks), ancestors.Union(freeBlocks));
+      }
+    }
+
+    FocusRec(0, impl.Blocks, new List<Block>());
+    return s;
+  }
+}