Staged Houdini

6 files changed, 955 insertions, 26 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 616a0e21..c3a9a164 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -739,6 +739,36 @@ namespace Microsoft.Boogie {
         fullMap[procName][blockName] = block;

     }

 

+    public static Graph<Implementation> BuildCallGraph(Program program) {

+      Graph<Implementation> callGraph = new Graph<Implementation>();

+      Dictionary<Procedure, HashSet<Implementation>> procToImpls = new Dictionary<Procedure, HashSet<Implementation>>();

+      foreach (Declaration decl in program.TopLevelDeclarations) {

+        Procedure proc = decl as Procedure;

+        if (proc == null) continue;

+        procToImpls[proc] = new HashSet<Implementation>();

+      }

+      foreach (Declaration decl in program.TopLevelDeclarations) {

+        Implementation impl = decl as Implementation;

+        if (impl == null || impl.SkipVerification) continue;

+        callGraph.AddSource(impl);

+        procToImpls[impl.Proc].Add(impl);

+      }

+      foreach (Declaration decl in program.TopLevelDeclarations) {

+        Implementation impl = decl as Implementation;

+        if (impl == null || impl.SkipVerification) continue;

+        foreach (Block b in impl.Blocks) {

+          foreach (Cmd c in b.Cmds) {

+            CallCmd cc = c as CallCmd;

+            if (cc == null) continue;

+            foreach (Implementation callee in procToImpls[cc.Proc]) {

+              callGraph.AddEdge(impl, callee);

+            }

+          }

+        }

+      }

+      return callGraph;

+    }

+

     public static Graph<Block/*!*/>/*!*/ GraphFromImpl(Implementation impl) {

       Contract.Requires(impl != null);

       Contract.Ensures(cce.NonNullElements(Contract.Result<Graph<Block>>().TopologicalSort()));

@@ -896,16 +926,17 @@ namespace Microsoft.Boogie {
 

     private int invariantGenerationCounter = 0;

 

-    public Constant MakeExistentialBoolean() {

+    public Constant MakeExistentialBoolean(int StageId) {

       Constant ExistentialBooleanConstant = new Constant(Token.NoToken, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false);

       invariantGenerationCounter++;

       ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });

+      ExistentialBooleanConstant.AddAttribute("stage_id", new object[] { new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(StageId)) });

       TopLevelDeclarations.Add(ExistentialBooleanConstant);

       return ExistentialBooleanConstant;

     }

 

-    public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null) {

-      Constant ExistentialBooleanConstant = MakeExistentialBoolean();

+    public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null, int StageId = 0) {

+      Constant ExistentialBooleanConstant = MakeExistentialBoolean(StageId);

       IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);

       PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));

       if (tag != null)

@@ -2907,6 +2938,7 @@ namespace Microsoft.Boogie {
       this.scc = new StronglyConnectedComponents<Block/*!*/>(this.Blocks, next, prev);

       scc.Compute();

 

+

       foreach (Block/*!*/ block in this.Blocks) {

         Contract.Assert(block != null);

         block.Predecessors = new BlockSeq();

@@ -2991,15 +3023,17 @@ namespace Microsoft.Boogie {
           reachableBlocks.Add(b);

           reachable.Add(b);

           if (b.TransferCmd is GotoCmd) {

-            foreach (Cmd/*!*/ s in b.Cmds) {

-              Contract.Assert(s != null);

-              if (s is PredicateCmd) {

-                LiteralExpr e = ((PredicateCmd)s).Expr as LiteralExpr;

-                if (e != null && e.IsFalse) {

-                  // This statement sequence will never reach the end, because of this "assume false" or "assert false".

-                  // Hence, it does not reach its successors.

-                  b.TransferCmd = new ReturnCmd(b.TransferCmd.tok);

-                  goto NEXT_BLOCK;

+            if (CommandLineOptions.Clo.PruneInfeasibleEdges) {

+              foreach (Cmd/*!*/ s in b.Cmds) {

+                Contract.Assert(s != null);

+                if (s is PredicateCmd) {

+                  LiteralExpr e = ((PredicateCmd)s).Expr as LiteralExpr;

+                  if (e != null && e.IsFalse) {

+                    // This statement sequence will never reach the end, because of this "assume false" or "assert false".

+                    // Hence, it does not reach its successors.

+                    b.TransferCmd = new ReturnCmd(b.TransferCmd.tok);

+                    goto NEXT_BLOCK;

+                  }

                 }

               }

             }

@@ -3153,7 +3187,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class VariableSeq : PureCollections.Sequence {

+  public sealed class VariableSeq : List<Variable> {

     public VariableSeq(params Variable[]/*!*/ args)

       : base(args) {

       Contract.Requires(args != null);

@@ -3192,6 +3226,11 @@ namespace Microsoft.Boogie {
         return res;

       }

     }

+    public int Length {

+      get {

+        return Count;

+      }

+    }

   }

 

   public sealed class TypeSeq : PureCollections.Sequence {

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 46d2c064..e94367ad 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -395,6 +395,7 @@ namespace Microsoft.Boogie {
     public bool ContractInfer = false;

     public bool ExplainHoudini = false;

     public bool HoudiniUseCrossDependencies = false;

+    public int StagedHoudini = 0;

     public string AbstractHoudini = null;

     public bool UseUnsatCoreForContractInfer = false;

     public bool PrintAssignment = false;

@@ -490,6 +491,7 @@ namespace Microsoft.Boogie {
 

     public bool RemoveEmptyBlocks = true;

     public bool CoalesceBlocks = true;

+    public bool PruneInfeasibleEdges = true;

 

     [Rep]

     public ProverFactory TheProverFactory;

@@ -861,6 +863,21 @@ namespace Microsoft.Boogie {
             return true;

           }

 

+        case "noPruneInfeasibleEdges": {

+            if (ps.ConfirmArgumentCount(0)) {

+              PruneInfeasibleEdges = false;

+            }

+            return true;

+        }

+

+        case "stagedHoudini": {

+            int sh = 0;

+            if (ps.GetNumericArgument(ref sh, 3)) {

+              StagedHoudini = sh;

+            }

+            return true;

+          }

+

         case "abstractHoudini":

             {

                 if (ps.ConfirmArgumentCount(1))

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index eb581edd..e6db6e9d 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -168,6 +168,7 @@
     <Compile Include="StandardVisitor.cs" />

     <Compile Include="TypeAmbiguitySeeker.cs" />

     <Compile Include="Util.cs" />

+    <Compile Include="VariableDependenceAnalyser.cs" />

     <Compile Include="VCExp.cs" />

     <Compile Include="..\version.cs" />

     <Compile Include="Xml.cs" />

diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs
index d51fcdb3..cb7b01a3 100644
--- a/Source/Core/DeadVarElim.cs
+++ b/Source/Core/DeadVarElim.cs
@@ -55,16 +55,16 @@ namespace Microsoft.Boogie {
 

       if (CommandLineOptions.Clo.Trace)

       {

-          Console.WriteLine();

-          Console.WriteLine("Running modset analysis ...");

-          int procCount = 0;

-          foreach (Declaration/*!*/ decl in program.TopLevelDeclarations)

-          {

-              Contract.Assert(decl != null);

-              if (decl is Procedure)

-                  procCount++;

-          }

-          Console.WriteLine("Number of procedures = {0}", procCount);

+//          Console.WriteLine();

+//          Console.WriteLine("Running modset analysis ...");

+//          int procCount = 0;

+//          foreach (Declaration/*!*/ decl in program.TopLevelDeclarations)

+//          {

+//              Contract.Assert(decl != null);

+//              if (decl is Procedure)

+//                  procCount++;

+//          }

+//          Console.WriteLine("Number of procedures = {0}", procCount);*/

       }

 

       modSets = new Dictionary<Procedure/*!*/, HashSet<Variable/*!*/>/*!*/>();

@@ -115,8 +115,8 @@ namespace Microsoft.Boogie {
           }

       }

 

-      if (CommandLineOptions.Clo.Trace)

-      {

+      if (false /*CommandLineOptions.Clo.Trace*/)      {

+

           Console.WriteLine("Number of procedures with nonempty modsets = {0}", modSets.Keys.Count);

           foreach (Procedure/*!*/ x in modSets.Keys)

           {

diff --git a/Source/Core/PureCollections.cs b/Source/Core/PureCollections.cs
index 15a6c629..f984ecd4 100644
--- a/Source/Core/PureCollections.cs
+++ b/Source/Core/PureCollections.cs
@@ -569,7 +569,7 @@ namespace PureCollections {
       object[] n = new object[card];

       int ct = 0;

       Contract.Assert(this.elems != null);

-      for (int i = 0; i < elems.Length; i++)

+      for (int i = 0; i < card; i++)

         n[ct++] = elems[i];

       return n;

     }

diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs
new file mode 100644
index 00000000..be9fdcb4
--- /dev/null
+++ b/Source/Core/VariableDependenceAnalyser.cs
@@ -0,0 +1,872 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics;

+using Microsoft.Boogie;

+using Microsoft.Boogie.GraphUtil;

+

+

+namespace Microsoft.Boogie {

+

+  public interface IVariableDependenceAnalyser {

+

+    void Analyse();

+    VariableDescriptor MakeDescriptor(string proc, Variable v);

+    HashSet<VariableDescriptor> DependsOn(VariableDescriptor v);

+    void dump();

+

+  }

+

+  public abstract class VariableDescriptor : IComparable {

+    internal readonly string Name;

+    internal VariableDescriptor(string Name) {

+      this.Name = Name;

+    }

+

+    public override string ToString() {

+      return Name;

+    }

+

+    public override bool Equals(object that) {

+

+      if (object.ReferenceEquals(this, that)) {

+        return true;

+      }

+

+      VariableDescriptor thatDescriptor = that as VariableDescriptor;

+

+      if (thatDescriptor == null) {

+        return false;

+      }

+

+      return base.Equals(thatDescriptor) &&

+        this.Name.Equals(thatDescriptor.Name);

+    }

+

+    public override int GetHashCode() {

+      return Name.GetHashCode();

+    }

+

+    public int CompareTo(object that) {

+      return this.ToString().CompareTo(that.ToString());

+    }

+

+  }

+

+  class LocalDescriptor : VariableDescriptor {

+    internal readonly string Proc;

+    internal LocalDescriptor(string Proc, string Name)

+      : base(Name) {

+      this.Proc = Proc;

+    }

+

+    public override string ToString() {

+      return Proc + "." + base.ToString();

+    }

+

+    public override bool Equals(object that) {

+

+      if (object.ReferenceEquals(this, that)) {

+        return true;

+      }

+

+      LocalDescriptor thatDescriptor = that as LocalDescriptor;

+

+      if (thatDescriptor == null) {

+        return false;

+      }

+

+      return base.Equals(thatDescriptor) &&

+        this.Proc.Equals(thatDescriptor.Proc);

+

+    }

+

+    public override int GetHashCode() {

+      return (33 * base.GetHashCode())

+           + this.Proc.GetHashCode();

+    }

+

+  }

+

+  class GlobalDescriptor : VariableDescriptor {

+    internal GlobalDescriptor(string name) : base(name) { }

+

+    public override bool Equals(object that) {

+

+      if (object.ReferenceEquals(this, that)) {

+        return true;

+      }

+

+      GlobalDescriptor thatDescriptor = that as GlobalDescriptor;

+

+      if (thatDescriptor == null) {

+        return false;

+      }

+

+      return base.Equals(thatDescriptor);

+

+    }

+

+    public override int GetHashCode() {

+      return base.GetHashCode();

+    }

+  

+  }

+

+  /// <summary>

+  /// Given a Boogie program, computes a graph that over-approximates dependences

+  /// between program variables.

+  /// </summary>

+  public class VariableDependenceAnalyser : IVariableDependenceAnalyser {

+

+    private Graph<VariableDescriptor> dependsOnNonTransitive;

+    private Program prog;

+    private Dictionary<Block, HashSet<Block>> BlockToControllingBlocks;

+    private Dictionary<Block, HashSet<VariableDescriptor>> ControllingBlockToVariables;

+

+    public VariableDependenceAnalyser(Program prog) {

+      this.prog = prog;

+      dependsOnNonTransitive = new Graph<VariableDescriptor>();

+    }

+

+

+    private void Initialise() {

+      foreach (var descriptor in

+        prog.TopLevelDeclarations.OfType<Variable>().Where(Item => !(Item is Constant)).

+          Select(Variable => Variable.Name).

+          Select(Name => new GlobalDescriptor(Name))) {

+        dependsOnNonTransitive.AddEdge(descriptor, descriptor);

+      }

+

+      foreach (var Proc in NonInlinedProcedures()) {

+

+        List<Variable> parameters = new List<Variable>();

+        parameters.AddRange(Proc.InParams);

+        parameters.AddRange(Proc.OutParams);

+        foreach (var descriptor in

+          parameters.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Proc.Name, Name))) {

+          dependsOnNonTransitive.AddEdge(descriptor, descriptor);

+        }

+      }

+

+      foreach (var Impl in NonInlinedImplementations()) {

+

+        List<Variable> locals = new List<Variable>();

+        locals.AddRange(Impl.LocVars);

+        foreach (var descriptor in

+          locals.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Impl.Name, Name))) {

+          dependsOnNonTransitive.AddEdge(descriptor, descriptor);

+        }

+      }

+    }

+

+    private IEnumerable<Procedure> NonInlinedProcedures() {

+      return prog.TopLevelDeclarations.OfType<Procedure>().

+        Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1);

+    }

+

+    private IEnumerable<Implementation> NonInlinedImplementations() {

+      return prog.TopLevelDeclarations.OfType<Implementation>().

+        Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1);

+    }

+

+    public void Analyse() {

+

+      /* The algorithm is as follows:

+       * 

+       * 1. Build global control dependence graph.  First build control dependence graph for each procedure,

+       *    and union them.  Then examine each procedure.  If block B is control-dependent on block C, make

+       *    every block that can be indirectly reached via a call from B control-dependent on C.

+       *    

+       * 2. Take transitive closure of global control dependence graph.

+       * 

+       * 3. For every block B such that some other block is control-dependent on B, determine those variables

+       *    which B tests.  If B tests v, and C is control-depdendent on B, we say that v "controls" the

+       *    statements appearing in C.

+       *    

+       * 4. Consider each statement to work out variable dependences.  v may depend on u if:

+	     *       - there is a statement v := e where u appears in e

+	     *       - there is a statement call ... := foo(..., e, ...) where v is formal in parameter of foo 

+       *         corresponding to e and u appears in e

+       *       - there is a statement call ..., v, ... := foo(...) where u is formal out parameter of foo 

+       *         correspondnig to v

+	     *       - there is a statement v := ... controlled by u

+	     *       - there is a statement call ... := foo(...) controlled by u where v is a formal in parameter

+       *         of foo

+	     *       - there is a statement call ..., v, ... := foo(...) controlled by u

+       *       

+       * 5. Finialise variable dependence graph by taking its transitive closure.

+       * 

+       */

+

+      if (CommandLineOptions.Clo.Trace) {

+        Console.WriteLine("Variable dependence analysis: Initialising");

+      }

+

+      Initialise();

+

+      if (CommandLineOptions.Clo.Trace) {

+        Console.WriteLine("Variable dependence analysis: Computing control dependence info");

+      }

+

+      BlockToControllingBlocks = ComputeGlobalControlDependences();

+

+      if (CommandLineOptions.Clo.Trace) {

+        Console.WriteLine("Variable dependence analysis: Computing control dependence variables");

+      }

+

+      ControllingBlockToVariables = ComputeControllingVariables(BlockToControllingBlocks);

+      foreach (var Impl in NonInlinedImplementations()) {

+

+        if (CommandLineOptions.Clo.Trace) {

+          Console.WriteLine("Variable dependence analysis: Analysing " + Impl.Name);

+        }

+

+        Analyse(Impl);

+      }

+    }

+

+    private void Analyse(Implementation Impl) {

+      string proc = Impl.Name;

+      foreach (Block b in Impl.Blocks) {

+        Analyse(proc, b);

+      }

+    }

+

+    private void Analyse(string proc, Block b) {

+      foreach (Cmd cmd in b.Cmds) {

+        AssignCmd assign = cmd as AssignCmd;

+        if (assign != null) {

+          HandleAssign(proc, b, assign);

+        }

+        CallCmd call = cmd as CallCmd;

+        if (call != null) {

+          HandleCall(proc, b, call);

+        }

+      }

+    }

+

+    private void HandleCall(string proc, Block b, CallCmd call) {

+      foreach (var formalActualPair in call.Proc.InParams.Zip(call.Ins)) {

+        var formalIn = MakeDescriptor(call.callee, formalActualPair.Item1);

+        AddDependences(formalIn, GetReferencedVariables(formalActualPair.Item2, proc));

+        AddControlDependences(b, formalIn);

+      }

+

+      foreach (var formalActualPair in call.Proc.OutParams.Zip(call.Outs)) {

+        var actualOut = MakeDescriptor(proc, formalActualPair.Item2.Decl);

+        AddDependences(actualOut, GetReferencedVariables(new IdentifierExpr(Token.NoToken, formalActualPair.Item1), call.callee));

+        AddControlDependences(b, actualOut);

+      }

+

+    }

+

+    private void HandleAssign(string proc, Block b, AssignCmd assign) {

+      foreach (var assignPair in assign.Lhss.Zip(assign.Rhss)) {

+        VariableDescriptor assignedVariable = MakeDescriptor(proc, assignPair.Item1.DeepAssignedVariable);

+        AddDependences(assignedVariable, GetReferencedVariables(assignPair.Item1, proc));

+        AddDependences(assignedVariable, GetReferencedVariables(assignPair.Item2, proc));

+        AddControlDependences(b, assignedVariable);

+      }

+    }

+

+    private void AddControlDependences(Block b, VariableDescriptor v) {

+      if (!BlockToControllingBlocks.ContainsKey(b)) {

+        return;

+      }

+      foreach (var controller in BlockToControllingBlocks[b]) {

+        AddDependences(v, ControllingBlockToVariables[controller]);

+      }

+    }

+

+    private IEnumerable<VariableDescriptor> GetReferencedVariables(Absy node, string proc) {

+      var VarCollector = new VariableCollector();

+      VarCollector.Visit(node);

+      return VarCollector.usedVars.Where(Item => !(Item is Constant)).Select(Item => MakeDescriptor(proc, Item));

+    }

+

+    void AddDependences(VariableDescriptor v, IEnumerable<VariableDescriptor> vs) {

+      foreach (var n in vs) {

+        dependsOnNonTransitive.AddEdge(v, n);

+      }

+    }

+

+    private Dictionary<Block, HashSet<VariableDescriptor>> ComputeControllingVariables(Dictionary<Block, HashSet<Block>> GlobalCtrlDep) {

+      Dictionary<Block, HashSet<VariableDescriptor>> result = new Dictionary<Block, HashSet<VariableDescriptor>>();

+      foreach (var Impl in NonInlinedImplementations()) {

+        foreach (var b in Impl.Blocks) {

+          result[b] = GetControlDependencyVariables(Impl.Name, b);

+        }

+      }

+      return result;

+    }

+

+    private HashSet<VariableDescriptor> GetControlDependencyVariables(string proc, Block b) {

+

+      // This method works under the assumption that assume statements

+      // relevant to control flow between basic blocks have the "partition" attribute

+

+      HashSet<VariableDescriptor> result = new HashSet<VariableDescriptor>();

+      var gotoCmd = b.TransferCmd as GotoCmd;

+      if (gotoCmd != null && gotoCmd.labelTargets.Length >= 2) {

+        foreach (Block succ in gotoCmd.labelTargets) {

+          foreach (Cmd c in succ.Cmds) {

+            AssumeCmd a = c as AssumeCmd;

+            if (a != null && QKeyValue.FindBoolAttribute(a.Attributes, "partition")) {

+              var VarCollector = new VariableCollector();

+              VarCollector.VisitExpr(a.Expr);

+              result.UnionWith(VarCollector.usedVars.Where(Item => !(Item is Constant)).Select(

+                Item => MakeDescriptor(proc, Item)));

+            }

+            else {

+              break;

+            }

+          }

+        }

+      }

+      return result;

+    }

+

+    private Dictionary<Block, HashSet<Block>> ComputeGlobalControlDependences() {

+

+      Dictionary<Block, HashSet<Block>> GlobalCtrlDep = new Dictionary<Block, HashSet<Block>>();

+      Dictionary<Implementation, Dictionary<Block, HashSet<Block>>> LocalCtrlDeps = new Dictionary<Implementation, Dictionary<Block, HashSet<Block>>>();

+

+      // Work out and union together local control dependences

+      foreach (var Impl in prog.TopLevelDeclarations.OfType<Implementation>()) {

+        Graph<Block> blockGraph = prog.ProcessLoops(Impl);

+        LocalCtrlDeps[Impl] = blockGraph.ControlDependence();

+        foreach (var KeyValue in LocalCtrlDeps[Impl]) {

+          GlobalCtrlDep.Add(KeyValue.Key, KeyValue.Value);

+        }

+      }

+

+      Graph<Implementation> callGraph = Program.BuildCallGraph(prog);

+

+      // Add inter-procedural control dependence nodes based on calls

+      foreach (var Impl in prog.TopLevelDeclarations.OfType<Implementation>()) {

+        foreach (var b in Impl.Blocks) {

+          foreach (var cmd in b.Cmds.OfType<CallCmd>()) {

+            var DirectCallee = GetImplementation(cmd.callee);

+            if (DirectCallee != null) {

+              HashSet<Implementation> IndirectCallees = ComputeIndirectCallees(callGraph, DirectCallee);

+              foreach (var control in GetControllingBlocks(b, LocalCtrlDeps[Impl])) {

+                foreach (var c in IndirectCallees.Select(Item => Item.Blocks).SelectMany(Item => Item)) {

+                  GlobalCtrlDep[control].Add(c);

+                }

+              }

+            }

+          }

+        }

+      }

+

+      // Compute transitive closure

+      GlobalCtrlDep.TransitiveClosure();

+

+      // Finally reverse the dependences

+

+      Dictionary<Block, HashSet<Block>> result = new Dictionary<Block, HashSet<Block>>();

+

+      foreach (var KeyValue in GlobalCtrlDep) {

+        foreach (var v in KeyValue.Value) {

+          if (!result.ContainsKey(v)) {

+            result[v] = new HashSet<Block>();

+          }

+          result[v].Add(KeyValue.Key);

+        }

+      }

+

+      return result;

+    }

+

+    private HashSet<Implementation> ComputeIndirectCallees(Graph<Implementation> callGraph, Implementation DirectCallee) {

+      return ComputeIndirectCallees(callGraph, DirectCallee, new HashSet<Implementation>());

+    }

+

+    private HashSet<Implementation> ComputeIndirectCallees(Graph<Implementation> callGraph, Implementation DirectCallee, HashSet<Implementation> seen) {

+      if (seen.Contains(DirectCallee)) {

+        return new HashSet<Implementation>();

+      }

+      HashSet<Implementation> result = new HashSet<Implementation>();

+      result.Add(DirectCallee);

+      seen.Add(DirectCallee);

+      foreach (var succ in callGraph.Successors(DirectCallee)) {

+        result.UnionWith(ComputeIndirectCallees(callGraph, succ, seen));

+      }

+      return result;

+    }

+

+    private HashSet<Block> GetControllingBlocks(Block b, Dictionary<Block, HashSet<Block>> ctrlDep) {

+      HashSet<Block> result = new HashSet<Block>();

+      foreach (var KeyValue in ctrlDep) {

+        if (KeyValue.Value.Contains(b)) {

+          result.Add(KeyValue.Key);

+        }

+      }

+      return result;

+    }

+

+    private Implementation GetImplementation(string proc) {

+      foreach (var Impl in prog.TopLevelDeclarations.OfType<Implementation>()) {

+        if (Impl.Name.Equals(proc)) {

+          return Impl;

+        }

+      }

+      return null;

+    }

+

+    public VariableDescriptor MakeDescriptor(string proc, Variable v) {

+

+      // Check whether there is an (Impl, v) match

+      var MatchingLocals = dependsOnNonTransitive.Nodes.Where(Item => Item is LocalDescriptor).Select(

+        Item => (LocalDescriptor)Item).Where(Item => Item.Proc.Equals(proc) &&

+          Item.Name.Equals(v.Name));

+      if (MatchingLocals.Count() > 0) {

+        Debug.Assert(MatchingLocals.Count() == 1);

+        return MatchingLocals.ToArray()[0];

+      }

+

+      // It must be a global with same name as v

+      return dependsOnNonTransitive.Nodes.Where(Item => Item is GlobalDescriptor &&

+        Item.Name.Equals(v.Name)).ToArray()[0];

+    }

+

+    private Dictionary<SCC<VariableDescriptor>, HashSet<VariableDescriptor>> DependsOnCache = new Dictionary<SCC<VariableDescriptor>, HashSet<VariableDescriptor>>();

+

+    private Graph<SCC<VariableDescriptor>> DependsOnSCCsDAG;

+    private Dictionary<VariableDescriptor, SCC<VariableDescriptor>> VariableDescriptorToSCC;

+

+    public HashSet<VariableDescriptor> DependsOn(VariableDescriptor v) {

+      if (DependsOnSCCsDAG == null) {

+        if (CommandLineOptions.Clo.Trace) {

+          Console.WriteLine("Variable dependence: computing SCCs");

+        }

+        Adjacency<VariableDescriptor> next = new Adjacency<VariableDescriptor>(dependsOnNonTransitive.Successors);

+        Adjacency<VariableDescriptor> prev = new Adjacency<VariableDescriptor>(dependsOnNonTransitive.Predecessors);

+        StronglyConnectedComponents<VariableDescriptor> DependsOnSCCs = new StronglyConnectedComponents<VariableDescriptor>(

+          dependsOnNonTransitive.Nodes, next, prev);

+        DependsOnSCCs.Compute();

+

+        VariableDescriptorToSCC = new Dictionary<VariableDescriptor, SCC<VariableDescriptor>>();

+        foreach (var scc in DependsOnSCCs) {

+          foreach (var s in scc) {

+            VariableDescriptorToSCC[s] = scc;

+          }

+        }

+

+        DependsOnSCCsDAG = new Graph<SCC<VariableDescriptor>>();

+        foreach (var edge in dependsOnNonTransitive.Edges) {

+          if (VariableDescriptorToSCC[edge.Item1] != VariableDescriptorToSCC[edge.Item2]) {

+            DependsOnSCCsDAG.AddEdge(VariableDescriptorToSCC[edge.Item1], VariableDescriptorToSCC[edge.Item2]);

+          }

+        }

+

+        SCC<VariableDescriptor> dummy = new SCC<VariableDescriptor>();

+        foreach (var n in dependsOnNonTransitive.Nodes) {

+          DependsOnSCCsDAG.AddEdge(VariableDescriptorToSCC[n], dummy);

+        }

+

+        if (CommandLineOptions.Clo.Trace) {

+          Console.WriteLine("Variable dependence: SCCs computed!");

+        }

+      }

+      return DependsOn(VariableDescriptorToSCC[v]);

+    }

+

+    public HashSet<VariableDescriptor> DependsOn(SCC<VariableDescriptor> vSCC) {

+

+      if (!DependsOnCache.ContainsKey(vSCC)) {

+        HashSet<VariableDescriptor> result = new HashSet<VariableDescriptor>();

+        if (vSCC.Count() > 0) {

+          result.UnionWith(vSCC);

+          foreach (var wSCC in DependsOnSCCsDAG.Successors(vSCC)) {

+            result.UnionWith(DependsOn(wSCC));

+          }

+        }

+        DependsOnCache[vSCC] = result;

+      }

+      return DependsOnCache[vSCC];

+    }

+

+    public void dump() {

+

+      Console.WriteLine("Variable dependence information");

+      Console.WriteLine("===============================");

+

+      Console.WriteLine("Global variables");

+      Console.WriteLine("================");

+

+      foreach (var GlobalEntry in dependsOnNonTransitive.Nodes.Where(Item => Item is GlobalDescriptor)) {

+        dump(GlobalEntry);

+      }

+

+      foreach (var proc in Procedures()) {

+        Console.WriteLine("Variables of " + proc);

+        Console.WriteLine("=====================");

+        foreach (var LocalEntry in dependsOnNonTransitive.Nodes.Where(Item => Item is LocalDescriptor

+          && ((LocalDescriptor)Item).Proc.Equals(proc))) {

+          dump(LocalEntry);

+        }

+      }

+    }

+

+    private void dump(VariableDescriptor vd) {

+      Console.Write(vd + " <- {");

+      bool first = true;

+

+      var SortedDependents = DependsOn(vd).ToList();

+      SortedDependents.Sort();

+      foreach (var Descriptor in SortedDependents) {

+        Console.Write((first ? "" : ",") + "\n  " + Descriptor);

+        if (first) {

+          first = false;

+        }

+      }

+      Debug.Assert(!first);

+      Console.WriteLine("\n}\n");

+    }

+

+    private HashSet<string> Procedures() {

+      return new HashSet<string>(dependsOnNonTransitive.Nodes.Where(Item =>

+              Item is LocalDescriptor).Select(Item => ((LocalDescriptor)Item).Proc));

+    }

+

+  }

+  

+

+  /// <summary>

+  /// Given a Boogie program, computes a graph that over-approximates dependences

+  /// between program variables.

+  /// </summary>

+  public class OldVariableDependenceAnalyser : IVariableDependenceAnalyser {

+

+    private Program prog;

+

+    public Dictionary<VariableDescriptor, HashSet<VariableDescriptor>> dependsOn;

+

+    private Dictionary<string, HashSet<VariableDescriptor>> callControlDependences;

+

+    private bool ProcedureChanged;

+

+    public OldVariableDependenceAnalyser(Program prog) {

+      this.prog = prog;

+      dependsOn = new Dictionary<VariableDescriptor, HashSet<VariableDescriptor>>();

+      callControlDependences = new Dictionary<string, HashSet<VariableDescriptor>>();

+    }

+    

+    public void Analyse() {

+

+      Initialise();

+

+      ProcedureChanged = true;

+      while (ProcedureChanged) {

+        ProcedureChanged = false;

+

+        foreach (var Impl in NonInlinedImplementations()) {

+          Analyse(Impl);

+        }

+

+      }

+

+    }

+

+    private Dictionary<string, int> temp = new Dictionary<string,int>();

+

+    private void Analyse(Implementation Impl) {

+

+      if (!temp.ContainsKey(Impl.Name)) {

+        temp[Impl.Name] = 0;

+      }

+

+      temp[Impl.Name]++;

+

+      var ctrlDep = GetControlDependenceTransitiveClosure(Impl);

+

+      var orderedBlocks = GetOrderedBlocks(Impl);

+

+      bool changed;

+      do {

+        changed = false;

+        foreach (Block block in orderedBlocks) {

+          Analyse(Impl, block, ctrlDep, ref changed);

+        }

+      } while (changed);

+

+    }

+

+    private void Analyse(Implementation Impl, Block block, 

+          Dictionary<Block, HashSet<Block>> ctrlDep, ref bool changed) {

+

+      // First, work out the set of all variables that are involved in tests on which

+      // this block is control-dependent

+      HashSet<VariableDescriptor> ctrlDepVars = GetControlDependencyVariables(block, Impl.Name, ctrlDep);

+      // Take incoming control dependences for the procedure

+      ctrlDepVars.UnionWith(callControlDependences[Impl.Name]);

+

+      var ControlInflucencingVariables = GetDependentVariables(ctrlDepVars);

+

+      foreach (var c in block.Cmds) {

+

+        var assign = c as AssignCmd;

+        if (assign != null) {

+

+          foreach (var assignPair in assign.Lhss.Zip(assign.Rhss)) {

+            VariableDescriptor assignedVariable = MakeDescriptor(Impl.Name, assignPair.Item1.DeepAssignedVariable);

+            AddDependences(assignedVariable, GetDependentVariables(GetReferencedVariables(assignPair.Item1, Impl.Name)), ref changed);

+            AddDependences(assignedVariable, GetDependentVariables(GetReferencedVariables(assignPair.Item2, Impl.Name)), ref changed);

+            AddDependences(assignedVariable, ControlInflucencingVariables, ref changed);

+          }

+        }

+

+        var call = c as CallCmd;

+        if (call != null) {

+          AddCallControlDependences(call.callee, ctrlDepVars);

+

+          foreach(var formalActualPair in call.Proc.InParams.Zip(call.Ins)) {

+            bool unused = false; // When we find that the in parameters of the called procedure have been changed, we do not need to necessarily continue processing this procedure

+            AddDependences(MakeDescriptor(call.callee, formalActualPair.Item1),

+              GetDependentVariables(GetReferencedVariables(formalActualPair.Item2, Impl.Name)), ref unused);

+            AddDependences(MakeDescriptor(call.callee, formalActualPair.Item1),

+              ControlInflucencingVariables, ref unused);

+          }

+

+          foreach (var formalActualPair in call.Proc.OutParams.Zip(call.Outs)) {

+            AddDependences(MakeDescriptor(Impl.Name, formalActualPair.Item2.Decl),

+              GetDependentVariables(GetReferencedVariables(new IdentifierExpr(Token.NoToken, formalActualPair.Item1), call.callee)), ref changed);

+            AddDependences(MakeDescriptor(Impl.Name, formalActualPair.Item2.Decl),

+              ControlInflucencingVariables, ref changed);

+          }

+

+        }

+

+      }

+

+    }

+

+    private IEnumerable<VariableDescriptor> GetDependentVariables(IEnumerable<VariableDescriptor> vars) {

+      HashSet<VariableDescriptor> result = new HashSet<VariableDescriptor>();

+      foreach (var v in vars) {

+        result.UnionWith(dependsOn[v]);

+      }

+      return result;

+    }

+

+    private IEnumerable<VariableDescriptor> GetReferencedVariables(Absy node, string proc) {

+      var VarCollector = new VariableCollector();

+      VarCollector.Visit(node);

+      IEnumerable<VariableDescriptor> result = VarCollector.usedVars.Where(Item => !(Item is Constant)).Select(Item => MakeDescriptor(proc, Item));

+      return result;

+    }

+

+    public VariableDescriptor MakeDescriptor(string proc, Variable v) {

+

+      // Check whether there is an (Impl, v) match

+      var MatchingLocals = dependsOn.Keys.Where(Item => Item is LocalDescriptor).Select(

+        Item => (LocalDescriptor)Item).Where(Item => Item.Proc.Equals(proc) &&

+          Item.Name.Equals(v.Name));

+      if(MatchingLocals.Count() > 0) {

+        Debug.Assert(MatchingLocals.Count() == 1);

+        return MatchingLocals.ToArray()[0];

+      }

+

+      // It must be a global with same name as v

+      return dependsOn.Keys.Where(Item => Item is GlobalDescriptor &&

+        Item.Name.Equals(v.Name)).ToArray()[0];

+    }

+

+    private Dictionary<Block, HashSet<VariableDescriptor>> ControlDependencyVariablesCache = new Dictionary<Block,HashSet<VariableDescriptor>>();

+

+    private HashSet<VariableDescriptor> GetControlDependencyVariables(Block b, string proc, Dictionary<Block, HashSet<Block>> ctrlDep) {

+

+      if (!ControlDependencyVariablesCache.ContainsKey(b)) {

+        HashSet<VariableDescriptor> ctrlDepVars = new HashSet<VariableDescriptor>();

+        foreach (var k in ctrlDep.Keys) {

+          if (ctrlDep[k].Contains(b)) {

+            foreach (Variable v in GetControlDependencyVariables(k)) {

+              ctrlDepVars.Add(MakeDescriptor(proc, v));

+            }

+          }

+        }

+        ControlDependencyVariablesCache[b] = ctrlDepVars;

+      }

+

+      return ControlDependencyVariablesCache[b];

+    }

+

+    private static HashSet<Variable> GetControlDependencyVariables(Block b) {

+

+      // This method works under the assumption that assume statements

+      // relevant to control flow between basic blocks have the "partition" attribute

+

+      HashSet<Variable> result = new HashSet<Variable>();

+      if (b.TransferCmd is GotoCmd) {

+        foreach (Block succ in ((GotoCmd)b.TransferCmd).labelTargets) {

+          foreach (Cmd c in succ.Cmds) {

+            AssumeCmd a = c as AssumeCmd;

+            if (a != null && QKeyValue.FindBoolAttribute(a.Attributes, "partition")) {

+              var VarCollector = new VariableCollector();

+              VarCollector.VisitExpr(a.Expr);

+              result.UnionWith(VarCollector.usedVars.Where(Item => !(Item is Constant)));

+            }

+            else {

+              break;

+            }

+          }

+        }

+      }

+      return result;

+    }

+

+    private void Initialise() {

+      foreach (var descriptor in

+        prog.TopLevelDeclarations.OfType<Variable>().Where(Item => !(Item is Constant)).

+          Select(Variable => Variable.Name).

+          Select(Name => new GlobalDescriptor(Name))) {

+        dependsOn.Add(descriptor, new HashSet<VariableDescriptor> { descriptor });

+      }

+

+      foreach (var Proc in NonInlinedProcedures()) {

+

+        callControlDependences[Proc.Name] = new HashSet<VariableDescriptor>();

+

+        List<Variable> parameters = new List<Variable>();

+        parameters.AddRange(Proc.InParams);

+        parameters.AddRange(Proc.OutParams);

+        foreach (var descriptor in

+          parameters.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Proc.Name, Name))) {

+          dependsOn.Add(descriptor, new HashSet<VariableDescriptor> { descriptor });

+        }

+      }

+

+      foreach (var Impl in NonInlinedImplementations()) {

+

+        List<Variable> locals = new List<Variable>();

+        locals.AddRange(Impl.LocVars);

+        foreach (var descriptor in

+          locals.Select(Variable => Variable.Name).Select(Name => new LocalDescriptor(Impl.Name, Name))) {

+          dependsOn.Add(descriptor, new HashSet<VariableDescriptor> { descriptor });

+        }

+      }

+    }

+

+    private IEnumerable<Procedure> NonInlinedProcedures() {

+      return prog.TopLevelDeclarations.OfType<Procedure>().

+        Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1);

+    }

+

+    private IEnumerable<Implementation> NonInlinedImplementations() {

+      return prog.TopLevelDeclarations.OfType<Implementation>().

+        Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1);

+    }

+

+

+

+    public void dump() {

+

+      Console.WriteLine("Variable dependence information");

+      Console.WriteLine("===============================");

+

+      Console.WriteLine("Global variables");

+      Console.WriteLine("================");

+

+      foreach (var GlobalEntry in dependsOn.Where(Item => Item.Key is GlobalDescriptor)) {

+        dump(GlobalEntry);

+      }

+

+      foreach (var proc in Procedures()) {

+        Console.WriteLine("Variables of " + proc);

+        Console.WriteLine("=====================");

+        foreach (var LocalEntry in dependsOn.Where(Item => Item.Key is LocalDescriptor

+          && ((LocalDescriptor)Item.Key).Proc.Equals(proc))) {

+          dump(LocalEntry);

+        }

+      }

+    }

+

+    private static void dump(KeyValuePair<VariableDescriptor,HashSet<VariableDescriptor>> Entry)

+    {

+        Console.Write(Entry.Key + " <- {");

+        bool first = true;

+

+        var SortedDependents = Entry.Value.ToList();

+        SortedDependents.Sort();

+      

+        foreach(var Descriptor in SortedDependents) {

+          Console.Write((first ? "" : ",") + "\n  " + Descriptor);

+          if (first) {

+            first = false;

+          }

+        }

+        Console.WriteLine("\n}\n");

+    }

+    

+    private HashSet<string> Procedures() {

+      return new HashSet<string>(dependsOn.Where(Item =>

+              Item.Key is LocalDescriptor).Select(Item => ((LocalDescriptor)Item.Key).Proc));

+    }

+

+    void AddDependences(VariableDescriptor v, IEnumerable<VariableDescriptor> vs, ref bool Changed) {

+      foreach (var n in vs) {

+        if (!dependsOn[v].Contains(n)) {

+          dependsOn[v].Add(n);

+          ProcedureChanged = true;

+          Changed = true;

+        }

+      }

+    }

+

+    private void AddCallControlDependences(string Proc, HashSet<VariableDescriptor> ctrlDepVars) {

+      foreach (var n in ctrlDepVars) {

+        if (!callControlDependences[Proc].Contains(n)) {

+          callControlDependences[Proc].Add(n);

+          ProcedureChanged = true;

+        }

+      }

+    }

+

+

+    private Dictionary<string, Dictionary<Block, HashSet<Block>>> ControlDependenceCache = new Dictionary<string, Dictionary<Block, HashSet<Block>>>();

+

+    private Dictionary<Block, HashSet<Block>> GetControlDependenceTransitiveClosure(Implementation Impl) {

+      if (!ControlDependenceCache.ContainsKey(Impl.Name)) {

+        Graph<Block> blockGraph = prog.ProcessLoops(Impl);

+        Dictionary<Block, HashSet<Block>> ctrlDep = blockGraph.ControlDependence();

+        ctrlDep.TransitiveClosure();

+        ControlDependenceCache[Impl.Name] = ctrlDep;

+      }

+      return ControlDependenceCache[Impl.Name];

+    }

+

+    private Dictionary<string, List<Block>> OrderedBlocksCache = new Dictionary<string,List<Block>>();

+

+    private List<Block> GetOrderedBlocks(Implementation Impl) {

+      if (!OrderedBlocksCache.ContainsKey(Impl.Name)) {

+        List<Block> orderedBlocks = PostOrder(Impl.Blocks[0], new HashSet<Block>());

+        Debug.Assert(orderedBlocks.Count() == Impl.Blocks.Count());

+        orderedBlocks.Reverse();

+        OrderedBlocksCache[Impl.Name] = orderedBlocks;

+      }

+      return OrderedBlocksCache[Impl.Name];

+    }

+

+    private List<Block> PostOrder(Block b, HashSet<Block> seen) {

+      seen.Add(b);

+      List<Block> result = new List<Block>();

+      if(b.TransferCmd is GotoCmd) {

+        foreach (Block c in ((GotoCmd)b.TransferCmd).labelTargets) {

+          if (!seen.Contains(c)) {

+            result.AddRange(PostOrder(c, seen));

+          }

+        }

+      }

+      result.Add(b);

+      return result;

+    }

+

+    public HashSet<VariableDescriptor> DependsOn(VariableDescriptor vd) {

+      return dependsOn[vd];

+    }

+

+  }

+}