Extract refactorings from #952 (#957)

Source/Core/AST/Absy.cs

@@ -247,71 +247,6 @@ public void SetMetadata<T>(int index, T value)
     #endregion
   }
 
-  public interface ICarriesAttributes
-  {
-    QKeyValue Attributes { get; set; }
-
-    public void ResolveAttributes(ResolutionContext rc)
-    {
-      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next)
-      {
-        kv.Resolve(rc);
-      }
-    }
-
-    public void TypecheckAttributes(TypecheckingContext tc)
-    {
-      var oldGlobalAccessOnlyInOld = tc.GlobalAccessOnlyInOld;
-      tc.GlobalAccessOnlyInOld = false;
-      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next)
-      {
-        kv.Typecheck(tc);
-      }
-      tc.GlobalAccessOnlyInOld = oldGlobalAccessOnlyInOld;
-    }
-
-    public List<int> FindLayers()
-    {
-      List<int> layers = new List<int>();
-      for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next)
-      {
-        if (kv.Key == CivlAttributes.LAYER)
-        {
-          layers.AddRange(kv.Params.Select(o => ((LiteralExpr)o).asBigNum.ToIntSafe));
-        }
-      }
-      return layers.Distinct().OrderBy(l => l).ToList();
-    }
-
-    // Look for {:name string} in list of attributes.
-    public string FindStringAttribute(string name)
-    {
-      return QKeyValue.FindStringAttribute(Attributes, name);
-    }
-
-    public void AddStringAttribute(IToken tok, string name, string parameter)
-    {
-      Attributes = new QKeyValue(tok, name, new List<object>() {parameter}, Attributes);
-    }
-
-    public void CopyIdFrom(IToken tok, ICarriesAttributes src)
-    {
-      var id = src.FindStringAttribute("id");
-      if (id is not null) {
-        AddStringAttribute(tok, "id", id);
-      }
-    }
-
-    public void CopyIdWithModificationsFrom(IToken tok, ICarriesAttributes src, Func<string,TrackedNodeComponent> modifier)
-    {
-      var id = src.FindStringAttribute("id");
-      if (id is not null) {
-        AddStringAttribute(tok, "id", modifier(id).SolverLabel);
-      }
-    }
-
-  }
-
   [ContractClassFor(typeof(Absy))]
   public abstract class AbsyContracts : Absy
   {

Source/Core/AST/CallCmd.cs

@@ -882,7 +882,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
 
           // Do this after copying the attributes so it doesn't get overwritten
           if (callId is not null) {
-            (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req,
+            a.CopyIdWithModificationsFrom(tok, req,
               id => new TrackedCallRequiresGoal(callId, id));
           }
 
@@ -899,7 +899,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
         Contract.Assert(a != null);
         // These probably won't have IDs, but copy if they do.
         if (callId is not null) {
-          (a as ICarriesAttributes).CopyIdWithModificationsFrom(tok, req,
+          a.CopyIdWithModificationsFrom(tok, req,
             id => new TrackedCallRequiresAssumed(callId, id));
         }
 
@@ -1066,7 +1066,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options)
       #endregion
 
       if (callId is not null) {
-        (assume as ICarriesAttributes).CopyIdWithModificationsFrom(tok, e,
+        assume.CopyIdWithModificationsFrom(tok, e,
           id => new TrackedCallEnsures(callId, id));
       }
 

Source/Core/AST/ICarriesAttributes.cs

@@ -0,0 +1,73 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+
+namespace Microsoft.Boogie;
+
+public interface ICarriesAttributes
+{
+  QKeyValue Attributes { get; set; }
+
+  public void ResolveAttributes(ResolutionContext rc)
+  {
+    for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next)
+    {
+      kv.Resolve(rc);
+    }
+  }
+
+  public void TypecheckAttributes(TypecheckingContext tc)
+  {
+    var oldGlobalAccessOnlyInOld = tc.GlobalAccessOnlyInOld;
+    tc.GlobalAccessOnlyInOld = false;
+    for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next)
+    {
+      kv.Typecheck(tc);
+    }
+    tc.GlobalAccessOnlyInOld = oldGlobalAccessOnlyInOld;
+  }
+
+  public List<int> FindLayers()
+  {
+    List<int> layers = new List<int>();
+    for (QKeyValue kv = this.Attributes; kv != null; kv = kv.Next)
+    {
+      if (kv.Key == CivlAttributes.LAYER)
+      {
+        layers.AddRange(kv.Params.Select(o => ((LiteralExpr)o).asBigNum.ToIntSafe));
+      }
+    }
+    return layers.Distinct().OrderBy(l => l).ToList();
+  }
+
+  // Look for {:name string} in list of attributes.
+  public string FindStringAttribute(string name)
+  {
+    return QKeyValue.FindStringAttribute(Attributes, name);
+  }
+
+  public void AddStringAttribute(IToken tok, string name, string parameter)
+  {
+    Attributes = new QKeyValue(tok, name, new List<object>() {parameter}, Attributes);
+  }
+
+}
+
+public static class CarriesAttributesExtensions
+{
+  public static void CopyIdFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src)
+  {
+    var id = src.FindStringAttribute("id");
+    if (id is not null) {
+      dest.AddStringAttribute(tok, "id", id);
+    }
+  }
+
+  public static void CopyIdWithModificationsFrom(this ICarriesAttributes dest, IToken tok, ICarriesAttributes src, Func<string,TrackedNodeComponent> modifier)
+  {
+    var id = src.FindStringAttribute("id");
+    if (id is not null) {
+      dest.AddStringAttribute(tok, "id", modifier(id).SolverLabel);
+    }
+  }
+}

Source/Core/VariableDependenceAnalyser.cs

@@ -515,63 +515,64 @@ private void MakeIgnoreList()
 
     private Dictionary<Block, HashSet<Block>> ComputeGlobalControlDependences()
     {
-      Dictionary<Block, HashSet<Block>> GlobalCtrlDep = new Dictionary<Block, HashSet<Block>>();
-      Dictionary<Implementation, Dictionary<Block, HashSet<Block>>> LocalCtrlDeps =
+      var globalCtrlDep = new Dictionary<Block, HashSet<Block>>();
+      var localCtrlDeps =
         new Dictionary<Implementation, Dictionary<Block, HashSet<Block>>>();
 
       // Work out and union together local control dependences
-      foreach (var Impl in prog.NonInlinedImplementations())
+      foreach (var impl in prog.NonInlinedImplementations())
       {
-        Graph<Block> blockGraph = prog.ProcessLoops(options, Impl);
-        LocalCtrlDeps[Impl] = blockGraph.ControlDependence(new Block(prog.tok));
-        foreach (var KeyValue in LocalCtrlDeps[Impl])
+        var blockGraph = prog.ProcessLoops(options, impl);
+        localCtrlDeps[impl] = blockGraph.ControlDependence(new Block(prog.tok));
+        foreach (var keyValue in localCtrlDeps[impl])
         {
-          GlobalCtrlDep.Add(KeyValue.Key, KeyValue.Value);
+          globalCtrlDep.Add(keyValue.Key, keyValue.Value);
         }
       }
 
-      Graph<Implementation> callGraph = Program.BuildCallGraph(options, prog);
+      var callGraph = Program.BuildCallGraph(options, prog);
 
       // Add inter-procedural control dependence nodes based on calls
-      foreach (var Impl in prog.NonInlinedImplementations())
+      foreach (var impl in prog.NonInlinedImplementations())
       {
-        foreach (var b in Impl.Blocks)
+        foreach (var b in impl.Blocks)
         {
           foreach (var cmd in b.Cmds.OfType<CallCmd>())
           {
-            var DirectCallee = GetImplementation(cmd.callee);
-            if (DirectCallee != null)
+            var directCallee = GetImplementation(cmd.callee);
+            if (directCallee == null)
             {
-              HashSet<Implementation> IndirectCallees = ComputeIndirectCallees(callGraph, DirectCallee);
-              foreach (var control in GetControllingBlocks(b, LocalCtrlDeps[Impl]))
+              continue;
+            }
+
+            var indirectCallees = ComputeIndirectCallees(callGraph, directCallee);
+            foreach (var control in GetControllingBlocks(b, localCtrlDeps[impl]))
+            {
+              foreach (var c in indirectCallees.Select(Item => Item.Blocks).SelectMany(Item => Item))
               {
-                foreach (var c in IndirectCallees.Select(Item => Item.Blocks).SelectMany(Item => Item))
-                {
-                  GlobalCtrlDep[control].Add(c);
-                }
+                globalCtrlDep[control].Add(c);
               }
             }
           }
         }
       }
 
       // Compute transitive closure
-      GlobalCtrlDep.TransitiveClosure();
+      globalCtrlDep.TransitiveClosure();
 
       // Finally reverse the dependences
 
-      Dictionary<Block, HashSet<Block>> result = new Dictionary<Block, HashSet<Block>>();
-
-      foreach (var KeyValue in GlobalCtrlDep)
+      var result = new Dictionary<Block, HashSet<Block>>();
+      foreach (var keyValue in globalCtrlDep)
       {
-        foreach (var v in KeyValue.Value)
+        foreach (var v in keyValue.Value)
         {
           if (!result.ContainsKey(v))
           {
             result[v] = new HashSet<Block>();
           }
 
-          result[v].Add(KeyValue.Key);
+          result[v].Add(keyValue.Key);
         }
       }
 

Source/Graph/Graph.cs

@@ -99,22 +99,22 @@ public bool DominatedBy(Node dominee, Node dominator, List<Node> path = null)
         return true;
       }
 
-      int currentNodeNum = nodeNumberToImmediateDominator[domineeNum];
+      int currentDominatorNum = nodeNumberToImmediateDominator[domineeNum];
       while (true)
       {
-        if (currentNodeNum == dominatorNum)
+        if (currentDominatorNum == dominatorNum)
         {
           return true;
         }
 
-        if (currentNodeNum == sourceNum)
+        if (currentDominatorNum == sourceNum)
         {
           return false;
         }
 
-        path?.Add(postOrderNumberToNode[currentNodeNum]);
+        path?.Add(postOrderNumberToNode[currentDominatorNum]);
 
-        currentNodeNum = nodeNumberToImmediateDominator[currentNodeNum];
+        currentDominatorNum = nodeNumberToImmediateDominator[currentDominatorNum];
       }
     }
 
@@ -429,8 +429,8 @@ public class Graph<Node>
     private HashSet<Node> splitCandidates;
 
     private DomRelation<Node> dominatorMap = null;
-    private Dictionary<Node, HashSet<Node>> predCache = new Dictionary<Node, HashSet<Node>>();
-    private Dictionary<Node, HashSet<Node>> succCache = new Dictionary<Node, HashSet<Node>>();
+    private Dictionary<Node, HashSet<Node>> predCache = new();
+    private Dictionary<Node, HashSet<Node>> succCache = new();
     private bool predComputed;
 
     [ContractInvariantMethod]

Source/Houdini/Houdini.cs

@@ -491,7 +491,7 @@ protected void Initialize(TextWriter traceWriter, Program program, HoudiniSessio
           }
 
           var session = new HoudiniSession(this, vcgen, proverInterface, program, 
-            new ImplementationRun(impl, traceWriter), stats, taskID: GetTaskID());
+            new ImplementationRun(impl, traceWriter), stats, taskId: GetTaskID());
           houdiniSessions.Add(impl, session);
         }
         catch (VCGenException)

Source/Houdini/HoudiniSession.cs

@@ -8,6 +8,7 @@
 using System.Linq;
 using System.Threading;
 using System.Threading.Tasks;
+using VCGeneration.Transformations;
 
 namespace Microsoft.Boogie.Houdini
 {
@@ -157,7 +158,7 @@ public bool InUnsatCore(Variable constant)
     }
 
     public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, ProverInterface proverInterface, Program program,
-      ImplementationRun run, HoudiniStatistics stats, int taskID = -1)
+      ImplementationRun run, HoudiniStatistics stats, int taskId = -1)
     {
       var impl = run.Implementation;
       this.Description = impl.Name;
@@ -166,7 +167,7 @@ public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, Pro
       collector = new VerificationResultCollector(houdini.Options);
       collector.OnProgress?.Invoke("HdnVCGen", 0, 0, 0.0);
 
-      vcgen.ConvertCFG2DAG(run, taskID: taskID);
+      new RemoveBackEdges(vcgen).ConvertCfg2Dag(run, taskID: taskId);
       var gotoCmdOrigins = vcgen.PassifyImpl(run, out var mvInfo);
 
       ExistentialConstantCollector.CollectHoudiniConstants(houdini, impl, out var ecollector);

Source/VCGeneration/AssertCounterexample.cs

@@ -39,8 +39,8 @@ public override byte[] Checksum
 
   public override Counterexample Clone()
   {
-    var ret = new AssertCounterexample(options, Trace, AugmentedTrace, FailingAssert, Model, MvInfo, Context, ProofRun);
-    ret.calleeCounterexamples = calleeCounterexamples;
+    var ret = new AssertCounterexample(Options, Trace, AugmentedTrace, FailingAssert, Model, MvInfo, Context, ProofRun);
+    ret.CalleeCounterexamples = CalleeCounterexamples;
     return ret;
   }
 }