Updated to Staged Houdini

5 files changed, 877 insertions, 769 deletions

diff --git a/Source/Houdini/AnnotationDependenceAnalyser.cs b/Source/Houdini/AnnotationDependenceAnalyser.cs
new file mode 100644
index 00000000..fd283f3e
--- /dev/null
+++ b/Source/Houdini/AnnotationDependenceAnalyser.cs
@@ -0,0 +1,831 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Boogie.GraphUtil;

+using Microsoft.Basetypes;

+using System.Diagnostics;

+

+namespace Microsoft.Boogie.Houdini {

+

+  public class AnnotationDependenceAnalyser {

+

+    private const string COARSE_STAGES = "COARSE";

+    private const string FINE_STAGES = "FINE";

+    private const string BALANCED_STAGES = "BALANCED";

+

+    private Program prog;

+    private IVariableDependenceAnalyser varDepAnalyser;

+    private IEnumerable<string> CandidateIdentifiers; // Candidate Boolean names

+    private IEnumerable<string> NonCandidateIdentifiers; // Additional names introduced for non-candidate annotations

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

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

+    private Graph<string> AnnotationDependences;

+    private StronglyConnectedComponents<string> SCCs;

+    private Graph<SCC<string>> StagesDAG;

+    private StagedHoudiniPlan Plan;

+

+    public AnnotationDependenceAnalyser(Program prog) {

+      this.prog = prog;

+      this.varDepAnalyser = new VariableDependenceAnalyser(prog);

+      varDepAnalyser.Analyse();

+    }

+

+    public void Analyse() {

+      if (CommandLineOptions.Clo.Trace) {

+        Console.WriteLine("Annotation dependence analysis: Getting annotations");

+      }

+

+      CandidateIdentifiers = GetCandidates();

+      NonCandidateIdentifiers = GetNonCandidateAnnotations();

+

+      DetermineAnnotationVariableDependences();

+

+      ConstructAnnotationDependenceGraph();

+

+      ConstructStagesDAG();

+

+    }

+

+    private IEnumerable<string> AllAnnotationIdentifiers() {

+      HashSet<string> Result = new HashSet<string>();

+      foreach (var c in CandidateIdentifiers) {

+        Result.Add(c);

+      }

+      foreach (var a in NonCandidateIdentifiers) {

+        Result.Add(a);

+      }

+      return Result;

+    }

+

+    private void ConstructStagesDAG()

+    {

+      if (CommandLineOptions.Clo.Trace)

+      {

+        Console.WriteLine("Annotation dependence analysis: Computing SCCs");

+      }

+

+      Adjacency<string> next = new Adjacency<string>(AnnotationDependences.Successors);

+      Adjacency<string> prev = new Adjacency<string>(AnnotationDependences.Predecessors);

+      SCCs = new StronglyConnectedComponents<string>(

+        AnnotationDependences.Nodes, next, prev);

+      SCCs.Compute();

+

+      if (CommandLineOptions.Clo.Trace)

+      {

+        Console.WriteLine("Annotation dependence analysis: Building stages DAG");

+      }

+

+      Dictionary<string, SCC<string>> rep = new Dictionary<string, SCC<string>>();

+      foreach (var scc in SCCs)

+      {

+        foreach (var s in scc)

+        {

+          rep[s] = scc;

+        }

+      }

+

+      StagesDAG = new Graph<SCC<string>>();

+

+      foreach (var edge in AnnotationDependences.Edges)

+      {

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

+        {

+          StagesDAG.AddEdge(rep[edge.Item1], rep[edge.Item2]);

+        }

+      }

+

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

+      foreach (var scc in SCCs)

+      {

+        StagesDAG.AddEdge(scc, dummy);

+      }

+    }

+

+    private void ConstructAnnotationDependenceGraph()

+    {

+      if (CommandLineOptions.Clo.Trace)

+      {

+        Console.WriteLine("Annotation dependence analysis: Building dependence graph");

+      }

+

+      IAnnotationReachabilityChecker reachabilityChecker;

+      

+      if(CommandLineOptions.Clo.StagedHoudiniReachabilityAnalysis) {

+        reachabilityChecker = new AnnotationReachabilityChecker(prog, AllAnnotationIdentifiers());

+      } else {

+        reachabilityChecker = new DummyAnnotationReachabilityChecker();

+      }

+

+      AnnotationDependences = new Graph<string>();

+      foreach (var c in AllAnnotationIdentifiers())

+      {

+        AnnotationDependences.AddEdge(c, c);

+        foreach (var vd in annotationDependsOn[c])

+        {

+          if (variableDirectlyReferredToByAnnotations.ContainsKey(vd))

+          {

+            foreach (var d in variableDirectlyReferredToByAnnotations[vd])

+            {

+              if(reachabilityChecker.MayReach(d, c))

+              {

+                AnnotationDependences.AddEdge(c, d);

+              }

+            }

+          }

+        }

+      }

+

+      if(CommandLineOptions.Clo.StagedHoudiniMergeIgnoredAnnotations) {

+        MergeIgnoredAnnotations();

+      }

+

+    }

+

+    private void MergeIgnoredAnnotations()

+    {

+      var IgnoredAnnotationsToVariables = new Dictionary<string, HashSet<Variable>>();

+      foreach(var c in AllAnnotationIdentifiers()) {

+        IgnoredAnnotationsToVariables[c] = new HashSet<Variable>();

+      }

+      foreach(var ci in AnnotationInstances()) {

+        if(!IgnoredAnnotationsToVariables.ContainsKey(ci.AnnotationIdentifier)) {

+          continue;

+        }

+        VariableCollector vc = new VariableCollector();

+        vc.Visit(ci.Expr);

+        if(vc.usedVars.Select(Item => varDepAnalyser.VariableRelevantToAnalysis(Item, ci.Proc)).Count() != 0) {

+          continue;

+        }

+        foreach(var v in vc.usedVars) {

+          if(varDepAnalyser.Ignoring(v, ci.Proc)) {

+            IgnoredAnnotationsToVariables[ci.AnnotationIdentifier].Add(v);

+          }

+        }

+      }

+      foreach(var c in IgnoredAnnotationsToVariables.Keys) {

+        foreach(var d in IgnoredAnnotationsToVariables.Keys) {

+          if(c == d) {

+            continue;

+          }

+          if(IgnoredAnnotationsToVariables[c].Equals(IgnoredAnnotationsToVariables[d])) {

+            AnnotationDependences.AddEdge(c, d);

+          }

+        }

+      }

+    }

+

+

+

+    private void DetermineAnnotationVariableDependences()

+    {

+      if (CommandLineOptions.Clo.Trace)

+      {

+        Console.WriteLine("Annotation dependence analysis: Working out what annotations depend on");

+      }

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

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

+      foreach (var c in AllAnnotationIdentifiers())

+      {

+        annotationDependsOn[c] = new HashSet<VariableDescriptor>();

+      }

+

+      foreach(var annotationInstance in AnnotationInstances()) {

+        AddDependences(annotationInstance);

+      }

+

+    }

+

+    private IEnumerable<AnnotationInstance> AnnotationInstances()

+    {

+      foreach (var impl in prog.Implementations)

+      {

+        foreach (PredicateCmd p in impl.Blocks.SelectMany(Item => Item.Cmds).OfType<PredicateCmd>())

+        {

+          string c;

+          if(Houdini.MatchCandidate(p.Expr, CandidateIdentifiers, out c)) {

+            yield return new AnnotationInstance(c, impl.Name, p.Expr);

+          } else if((p is AssertCmd) && QKeyValue.FindBoolAttribute(p.Attributes, "originated_from_invariant")) {

+            yield return new AnnotationInstance(GetTagFromNonCandidateAttributes(p.Attributes), impl.Name, p.Expr);

+          }

+        }

+      }

+

+      foreach (var proc in prog.NonInlinedProcedures())

+      {

+        foreach (Requires r in proc.Requires)

+        {

+          string c;

+          if(Houdini.MatchCandidate(r.Condition, CandidateIdentifiers, out c)) {

+            yield return new AnnotationInstance(c, proc.Name, r.Condition);

+          } else {

+            //yield return new AnnotationInstance(GetTagFromNonCandidateAttributes(r.Attributes), proc.Name, r.Condition);

+          }

+        }

+        foreach (Ensures e in proc.Ensures)

+        {

+          string c;

+          if(Houdini.MatchCandidate(e.Condition, CandidateIdentifiers, out c)) {

+            yield return new AnnotationInstance(c, proc.Name, e.Condition);

+          } else {

+            //yield return new AnnotationInstance(GetTagFromNonCandidateAttributes(e.Attributes), proc.Name, e.Condition);

+          }

+        }

+      }

+    }

+

+    internal static string GetTagFromNonCandidateAttributes(QKeyValue Attributes)

+    {

+      string tag = QKeyValue.FindStringAttribute(Attributes, "staged_houdini_tag");

+      Debug.Assert(tag != null);

+      return tag;

+    }

+

+    private bool FindInDAG(Graph<SCC<string>> DAG, SCC<string> toFind, SCC<string> start) {

+      if (toFind == start) {

+        return true;

+      }

+      foreach (var n in DAG.Successors(start)) {

+        if (FindInDAG(DAG, toFind, n)) {

+          return true;

+        }

+      }

+      return false;

+    }

+

+    private void AddDependences(AnnotationInstance ci) {

+      VariableCollector vc = new VariableCollector();

+      vc.VisitExpr(ci.Expr);

+

+      foreach (var v in vc.usedVars.Where(Item => varDepAnalyser.VariableRelevantToAnalysis(Item, ci.Proc))) {

+        VariableDescriptor vd =

+          varDepAnalyser.MakeDescriptor(ci.Proc, v);

+        if (!variableDirectlyReferredToByAnnotations.ContainsKey(vd)) {

+          variableDirectlyReferredToByAnnotations[vd] = new HashSet<string>();

+        }

+        variableDirectlyReferredToByAnnotations[vd].Add(ci.AnnotationIdentifier);

+

+        foreach (var w in varDepAnalyser.DependsOn(vd)) {

+          annotationDependsOn[ci.AnnotationIdentifier].Add(w);

+        }

+      }

+    }

+

+    private bool IsStageDependence(SCC<string> Src, SCC<string> Dst) {

+      foreach (var c in Src) {

+        foreach (var d in AnnotationDependences.Successors(c)) {

+          if (Dst.Contains(d)) {

+            return true;

+          }

+        }

+      }

+      return false;

+    }

+

+

+    public void dump() {

+

+      if(CommandLineOptions.Clo.DebugStagedHoudini) {

+        varDepAnalyser.dump();

+

+        Console.WriteLine("Annotations and the variables they depend on");

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

+        foreach (var entry in annotationDependsOn) {

+          Console.WriteLine(entry.Key + " <- ");

+          foreach (var vd in entry.Value) {

+            Console.WriteLine("  " + vd + ", ");

+          }

+        }

+

+        Console.WriteLine("");

+

+        Console.WriteLine("Variables and the annotations that directly refer to them");

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

+        foreach (var entry in variableDirectlyReferredToByAnnotations) {

+          Console.WriteLine(entry.Key + " <- ");

+          foreach (var annotation in entry.Value) {

+            Console.WriteLine("  " + annotation + ", ");

+          }

+        }

+

+        Console.WriteLine("");

+

+        Console.WriteLine("Annotation dependence graph");

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

+        foreach (var c in AnnotationDependences.Nodes) {

+          Console.WriteLine(c + " <- ");

+          foreach (var d in AnnotationDependences.Successors(c)) {

+            Console.WriteLine("  " + d);

+          }

+        }

+      }

+

+      Console.WriteLine("");

+

+      Console.WriteLine("Strongly connected components");

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

+

+      List<SCC<string>> Components = StagesDAG.TopologicalSort().ToList();

+

+      for (int i = 0; i < Components.Count(); i++) {

+        Console.Write(i + ": ");

+        DumpSCC(Components[i]);

+        Console.WriteLine(); Console.WriteLine();

+      }

+

+      Console.WriteLine("Stages DAG");

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

+      for (int i = 0; i < Components.Count(); i++) {

+        Console.Write(i + " -> { ");

+        bool first = true;

+        foreach (var d in StagesDAG.Successors(Components[i])) {

+          if (first) {

+            first = false;

+          }

+          else {

+            Console.Write(", ");

+          }

+          Console.Write(Components.IndexOf(d));

+        }

+        Console.WriteLine(" }");

+      }

+    

+    }

+

+    private static void DumpSCC(SCC<string> component) {

+      var sortedComponent = component.ToList();

+      sortedComponent.Sort();

+      Console.Write("{ ");

+      bool first = true;

+      foreach (var s in sortedComponent) {

+        if (first) {

+          first = false;

+        }

+        else {

+          Console.Write(", ");

+        }

+        Console.Write(s);

+      }

+      Console.Write(" }");

+    }

+

+    private IEnumerable<string> GetNonCandidateAnnotations() {

+      var Result = new HashSet<string>();

+      int Counter = 0;

+      foreach(var Assertion in prog.Blocks().SelectMany(Item => Item.Cmds).

+        OfType<AssertCmd>()) {

+

+        string unused;

+        if (Houdini.MatchCandidate(Assertion.Expr, CandidateIdentifiers, out unused)) {

+          continue;

+        }

+

+        if (!QKeyValue.FindBoolAttribute(Assertion.Attributes, "originated_from_invariant")) {

+          continue;

+        }

+

+        string Tag = "staged_houdini_tag_" + Counter;

+        Result.Add(Tag);

+        Assertion.Attributes = new QKeyValue(Token.NoToken, "staged_houdini_tag", 

+          new List<object> { Tag }, Assertion.Attributes);

+        Counter++;

+      }

+

+      /*

+      foreach(var Req in prog.NonInlinedProcedures().SelectMany(Item => Item.Requires)) {

+

+        string unused;

+        if (Houdini.MatchCandidate(Req.Condition, CandidateIdentifiers, out unused)) {

+          continue;

+        }

+

+        string Tag = "staged_houdini_tag_" + Counter;

+        Result.Add(Tag);

+        Req.Attributes = new QKeyValue(Token.NoToken, "staged_houdini_tag", 

+          new List<object> { Tag }, Req.Attributes);

+        Counter++;

+

+      }

+

+      foreach(var Ens in prog.NonInlinedProcedures().SelectMany(Item => Item.Ensures)) {

+

+        string unused;

+        if (Houdini.MatchCandidate(Ens.Condition, CandidateIdentifiers, out unused)) {

+          continue;

+        }

+

+        string Tag = "staged_houdini_tag_" + Counter;

+        Result.Add(Tag);

+        Ens.Attributes = new QKeyValue(Token.NoToken, "staged_houdini_tag", 

+          new List<object> { Tag }, Ens.Attributes);

+        Counter++;

+

+      }

+      */

+

+      return Result;

+    }

+

+    private IEnumerable<string> GetCandidates() {

+      return prog.Variables.Where(Item =>

+        QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name);

+    }

+

+

+    public StagedHoudiniPlan ApplyStages() {

+

+        if (NoStages())

+        {

+          // TODO: need to figure out what to do here

+          throw new NotImplementedException();

+        }

+

+        #region Assign annotations to stages at a given level of granularity

+      

+        switch(CommandLineOptions.Clo.StagedHoudini) {

+          case COARSE_STAGES:

+            Plan = ComputeCoarseStages();

+            break;

+          case FINE_STAGES:

+            Plan = ComputeFineStages();

+            break;

+          case BALANCED_STAGES:

+            Plan = ComputeBalancedStages();

+            break;

+          default:

+            Debug.Assert(false);

+            Plan = null;

+            break;

+        }

+

+        foreach(var c in AllAnnotationIdentifiers()) {

+          Debug.Assert(Plan.StageForAnnotation(c) != null);

+        }

+        #endregion

+

+        #region Generate boolean variables to control stages

+        var stageToActiveBoolean = new Dictionary<int, Constant>();

+        var stageToCompleteBoolean = new Dictionary<int, Constant>();

+

+        foreach (var stage in Plan)

+        {

+            var stageActive = new Constant(Token.NoToken,

+                new TypedIdent(Token.NoToken, "_stage_" + stage.GetId() + "_active", Type.Bool),

+                false);

+            stageActive.AddAttribute("stage_active", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) });

+            prog.AddTopLevelDeclaration(stageActive);

+            stageToActiveBoolean[stage.GetId()] = stageActive;

+

+            var stageComplete = new Constant(Token.NoToken, 

+                new TypedIdent(Token.NoToken, "_stage_" + stage.GetId() + "_complete", Type.Bool),

+                false);

+            stageComplete.AddAttribute("stage_complete", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) });

+            prog.AddTopLevelDeclaration(stageComplete);

+            stageToCompleteBoolean[stage.GetId()] = stageComplete;

+        }

+        #endregion

+

+        #region Adapt annotation assertions to take account of stages

+        foreach (var b in prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item))

+        {

+            List<Cmd> newCmds = new List<Cmd>();

+            foreach (var cmd in b.Cmds)

+            {

+                var a = cmd as AssertCmd;

+                string c;

+                if (a != null) {

+                    if (Houdini.MatchCandidate(a.Expr, CandidateIdentifiers, out c))

+                    {

+                        newCmds.Add(new AssertCmd(a.tok, Houdini.AddConditionToCandidate(a.Expr,

+                            Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(c).GetId()]), c), a.Attributes));

+                        newCmds.Add(new AssumeCmd(a.tok, Houdini.AddConditionToCandidate(a.Expr,

+                            Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(c).GetId()]), c), a.Attributes));

+                    } else if (QKeyValue.FindBoolAttribute(a.Attributes, "originated_from_invariant")) {

+                        string tag = GetTagFromNonCandidateAttributes(a.Attributes);

+                        newCmds.Add(new AssertCmd(a.tok, Expr.Imp(

+                            Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(tag).GetId()]), a.Expr),

+                            a.Attributes));

+                        newCmds.Add(new AssumeCmd(a.tok, Expr.Imp(

+                            Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(tag).GetId()]), a.Expr),

+                            a.Attributes));

+                    }

+                }

+                else

+                {

+                    newCmds.Add(cmd);

+                }

+            }

+            b.Cmds = newCmds;

+        }

+        #endregion

+

+        #region Adapt pre/postconditions to take account of stages

+        foreach (var p in prog.NonInlinedProcedures())

+        {

+

+          #region Handle the preconditions

+          List<Requires> newRequires = new List<Requires>();

+          foreach(Requires r in p.Requires) {

+            string c;

+            if (Houdini.MatchCandidate(r.Condition, CandidateIdentifiers, out c)) {

+              newRequires.Add(new Requires(r.tok, false, 

+                Houdini.AddConditionToCandidate(r.Condition,

+                Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(c).GetId()]), c),

+                r.Comment, r.Attributes));

+              newRequires.Add(new Requires(r.tok, true, 

+                Houdini.AddConditionToCandidate(r.Condition,

+                Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(c).GetId()]), c),

+                r.Comment, r.Attributes));

+            } else {

+              newRequires.Add(r);

+              /*string tag = GetTagFromNonCandidateAttributes(r.Attributes);

+              newRequires.Add(new Requires(r.tok, false, 

+                Expr.Imp(Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(tag).GetId()]), r.Condition),

+                r.Comment, r.Attributes));

+              newRequires.Add(new Requires(r.tok, true, 

+                Expr.Imp(Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(tag).GetId()]), r.Condition),

+                r.Comment, r.Attributes));*/

+            }

+          }

+          p.Requires = newRequires;

+          #endregion

+

+          #region Handle the postconditions

+          List<Ensures> newEnsures = new List<Ensures>();

+          foreach(Ensures e in p.Ensures) {

+            string c;

+            if (Houdini.MatchCandidate(e.Condition, CandidateIdentifiers, out c)) {

+              int stage = Plan.StageForAnnotation(c).GetId();

+              newEnsures.Add(new Ensures(e.tok, false, 

+                Houdini.AddConditionToCandidate(e.Condition,

+                Expr.Ident(stageToActiveBoolean[stage]), c),

+                e.Comment, e.Attributes));

+              newEnsures.Add(new Ensures(e.tok, true, 

+                Houdini.AddConditionToCandidate(e.Condition,

+                Expr.Ident(stageToCompleteBoolean[stage]), c),

+                e.Comment, e.Attributes));

+            } else {

+              newEnsures.Add(e);

+              /*string tag = GetTagFromNonCandidateAttributes(e.Attributes);

+              newRequires.Add(new Requires(e.tok, false, 

+                Expr.Imp(Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(tag).GetId()]), e.Condition),

+                e.Comment, e.Attributes));

+              newRequires.Add(new Requires(e.tok, true, 

+                Expr.Imp(Expr.Ident(stageToCompleteBoolean[Plan.StageForAnnotation(tag).GetId()]), e.Condition),

+                e.Comment, e.Attributes));*/

+            }

+          }

+          p.Ensures = newEnsures;

+          #endregion

+

+        }

+        #endregion

+

+        return Plan;

+

+    }

+

+    private int FindLargestStage() {

+      return StagesDAG.Nodes.Select(Item => Item.Count()).Max();

+    }

+

+

+    private StagedHoudiniPlan ComputeCoarseStages()

+    {

+        foreach(var n in StagesDAG.Nodes) {

+          Debug.Assert(!StagesDAG.Successors(n).Contains(n));

+        }

+

+        Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();

+

+        var done = new Dictionary<SCC<string>, ScheduledStage>();

+        done[GetStartNodeOfStagesDAG()] = new ScheduledStage(0, new HashSet<string>());

+

+        for(int stageId = 1; done.Count() != StagesDAG.Nodes.Count(); stageId++)

+        {

+            var Stage = new ScheduledStage(stageId, new HashSet<string>());

+            HashSet<SCC<string>> AssignedToThisStage = new HashSet<SCC<string>>();

+

+            foreach (var n in StagesDAG.Nodes.Where(Item => !done.ContainsKey(Item)))

+            {

+              if(StagesDAG.Successors(n).Where(Item => !done.ContainsKey(Item)).Count() == 0) {

+                foreach(var s in StagesDAG.Successors(n)) {

+                  Debug.Assert(s != n);

+                  Debug.Assert(Stage != done[s]);

+                  Dependences.AddEdge(Stage, done[s]);

+                }

+                foreach (var a in n)

+                {

+                  Stage.AddAnnotation(a);

+                }

+                AssignedToThisStage.Add(n);

+              }

+            }

+

+            foreach(var n in AssignedToThisStage) {

+              done[n] = Stage;

+            }

+        }

+        return new StagedHoudiniPlan(Dependences);

+    }

+

+    private StagedHoudiniPlan ComputeBalancedStages()

+    {

+      Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();

+      var done = new Dictionary<SCC<string>, ScheduledStage>();

+      done[GetStartNodeOfStagesDAG()] = new ScheduledStage(0, new HashSet<string>());

+

+      int maxStageSize = 200;

+

+      for(int stageId = 1; done.Count() != StagesDAG.Nodes.Count(); stageId++)

+      {

+        int stageSize = 0;

+        ScheduledStage Stage = new ScheduledStage(stageId, new HashSet<string>());

+        HashSet<SCC<string>> AddedToThisStage = new HashSet<SCC<string>>();

+

+        foreach (var n in StagesDAG.Nodes.Where(Item => !done.ContainsKey(Item)))

+        {

+          if(stageSize + n.Count() > maxStageSize) {

+            continue;

+          }

+          if(StagesDAG.Successors(n).Where(Item => !done.ContainsKey(Item)).Count() == 0) {

+            foreach (var c in n)

+            {

+              Stage.AddAnnotation(c);

+              stageSize++;

+            }

+            foreach(var s in StagesDAG.Successors(n)) {

+              Dependences.AddEdge(Stage, done[s]);

+            }

+            AddedToThisStage.Add(n);

+          }

+        }

+        foreach(var n in AddedToThisStage) {

+          done[n] = Stage;

+        }

+        if(stageSize == 0) {

+          maxStageSize *= 2;

+        }

+      }

+      return new StagedHoudiniPlan(Dependences);

+    }

+

+    private StagedHoudiniPlan ComputeFineStages()

+    {

+      Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();

+      var done = new Dictionary<SCC<string>, ScheduledStage>();

+

+      List<SCC<string>> components = StagesDAG.TopologicalSort().ToList();

+      components.Reverse();

+

+      for (int i = 0; i < components.Count(); i++)

+      {

+        ScheduledStage Stage = new ScheduledStage(i, new HashSet<string>());

+        done[components[i]] = Stage;

+        foreach (var c in components[i])

+        {

+          Stage.AddAnnotation(c);

+        }

+        foreach(var s in StagesDAG.Successors(components[i])) {

+          Dependences.AddEdge(Stage, done[s]);

+        }

+      }

+      return new StagedHoudiniPlan(Dependences);

+    }

+

+    private SCC<string> GetStartNodeOfStagesDAG()

+    {

+      return StagesDAG.Nodes.Where(Item => StagesDAG.Successors(Item).Count() == 0).

+        ToList()[0];

+    }

+

+    private bool NoStages()

+    {

+        return AllAnnotationIdentifiers().Count() == 0 || StagesDAG.Nodes.Count() == 0;

+    }

+  }

+

+  interface IAnnotationReachabilityChecker {

+    bool MayReach(string c, string d);

+  }

+

+  class DummyAnnotationReachabilityChecker : IAnnotationReachabilityChecker {

+    public bool MayReach(string c, string d) {

+      return true;

+    }

+  }

+

+  class AnnotationReachabilityChecker : IAnnotationReachabilityChecker {

+

+    private enum PrePost {

+      PRE, POST

+    }

+

+    private Program prog;

+    private IEnumerable<string> AnnotationIdentifiers;

+    private IInterproceduralReachabilityGraph reachabilityGraph;

+    private Dictionary<string, HashSet<object>> annotationToOccurences;

+

+    internal AnnotationReachabilityChecker(Program prog, IEnumerable<string> AnnotationIdentifiers) {

+      this.prog = prog;

+      this.AnnotationIdentifiers = AnnotationIdentifiers;

+      this.reachabilityGraph = new InterproceduralReachabilityGraph(prog);

+      this.annotationToOccurences = new Dictionary<string,HashSet<object>>();

+

+      // Add all annotation occurrences in blocks

+      foreach(Block b in prog.Blocks()) {

+        foreach(var assertCmd in b.Cmds.OfType<AssertCmd>()) {

+          string c;

+          if(Houdini.MatchCandidate(assertCmd.Expr, AnnotationIdentifiers, out c)) {

+            AddAnnotationOccurrence(c, b);

+          } else {

+            AddAnnotationOccurrence(AnnotationDependenceAnalyser.GetTagFromNonCandidateAttributes(assertCmd.Attributes), b);

+          }

+        }

+      }

+

+      // Add all annotation occurrences in pre and post conditions

+      foreach(var proc in prog.NonInlinedProcedures()) {

+        foreach(Requires r in proc.Requires) {

+          string c;

+          if(Houdini.MatchCandidate(r.Condition, AnnotationIdentifiers, out c)) {

+            AddAnnotationOccurrence(c, new Tuple<string, PrePost>(proc.Name, PrePost.PRE));

+          } else {

+            string tag = AnnotationDependenceAnalyser.GetTagFromNonCandidateAttributes(r.Attributes);

+            AddAnnotationOccurrence(tag, new Tuple<string, PrePost>(proc.Name, PrePost.PRE));

+          }

+        }

+        foreach(Ensures e in proc.Ensures) {

+          string c;

+          if(Houdini.MatchCandidate(e.Condition, AnnotationIdentifiers, out c)) {

+            AddAnnotationOccurrence(c, new Tuple<string, PrePost>(proc.Name, PrePost.POST));

+          } else {

+            string tag = AnnotationDependenceAnalyser.GetTagFromNonCandidateAttributes(e.Attributes);

+            AddAnnotationOccurrence(tag, new Tuple<string, PrePost>(proc.Name, PrePost.PRE));

+          }

+        }

+      }

+      

+    }

+

+    private void AddAnnotationOccurrence(string c, object o) {

+      Debug.Assert(o is Block || o is Tuple<string, PrePost>);

+      if(!annotationToOccurences.ContainsKey(c)) {

+        annotationToOccurences[c] = new HashSet<object>();

+      }

+      annotationToOccurences[c].Add(o);

+    }

+

+    public bool MayReach(string c, string d) {

+      foreach(object cOccurrence in annotationToOccurences[c]) {

+        foreach(object dOccurrence in annotationToOccurences[d]) {

+          if(OccurrencesMayReach(cOccurrence, dOccurrence)) {

+            return true;

+          }

+        }

+      }

+      return false;

+    }

+

+    private bool OccurrencesMayReach(object cOccurrence, object dOccurrence) {

+      Debug.Assert(cOccurrence is Block || cOccurrence is Tuple<string, PrePost>);

+      Debug.Assert(dOccurrence is Block || dOccurrence is Tuple<string, PrePost>);

+

+      Block cInterproceduralBlock = GetInterproceduralBlock(cOccurrence);

+      Block dInterproceduralBlock = GetInterproceduralBlock(dOccurrence);

+

+      return reachabilityGraph.MayReach(cInterproceduralBlock, dInterproceduralBlock);

+

+    }

+

+    private Block GetInterproceduralBlock(object cOccurrence)

+    {

+      Debug.Assert(cOccurrence is Block || cOccurrence is Tuple<string, PrePost>);

+

+      var stringPrePostPair = cOccurrence as Tuple<string, PrePost>;

+      if(stringPrePostPair != null) {

+        if(stringPrePostPair.Item2 == PrePost.PRE) {

+          return reachabilityGraph.GetNewEntryBlock(stringPrePostPair.Item1);

+        } else {

+          return reachabilityGraph.GetNewExitBlock(stringPrePostPair.Item1);

+        }

+      }

+

+      return reachabilityGraph.GetNewBlock((Block)cOccurrence);

+

+    }

+  }

+

+  class AnnotationInstance {

+    public string AnnotationIdentifier;

+    public string Proc;

+    public Expr Expr;

+

+    internal AnnotationInstance(string AnnotationIdentifier, string Proc, Expr Expr) {

+      this.AnnotationIdentifier = AnnotationIdentifier;

+      this.Proc = Proc;

+      this.Expr = Expr;

+    }

+  }

+

+}

diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs
deleted file mode 100644
index 12bad0ac..00000000
--- a/Source/Houdini/CandidateDependenceAnalyser.cs
+++ /dev/null
@@ -1,731 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using Microsoft.Boogie.GraphUtil;

-using Microsoft.Basetypes;

-using System.Diagnostics;

-

-namespace Microsoft.Boogie.Houdini {

-

-  public class CandidateDependenceAnalyser {

-

-    private const string COARSE_STAGES = "COARSE";

-    private const string FINE_STAGES = "FINE";

-    private const string BALANCED_STAGES = "BALANCED";

-

-    private Program prog;

-    private IVariableDependenceAnalyser varDepAnalyser;

-    private IEnumerable<string> candidates;

-    private Dictionary<string, HashSet<VariableDescriptor>> candidateDependsOn;

-    private Dictionary<VariableDescriptor, HashSet<string>> variableDirectlyReferredToByCandidates;

-    private Graph<string> CandidateDependences;

-    private StronglyConnectedComponents<string> SCCs;

-    private Graph<SCC<string>> StagesDAG;

-    private StagedHoudiniPlan Plan;

-

-    public CandidateDependenceAnalyser(Program prog) {

-      this.prog = prog;

-      this.varDepAnalyser = new VariableDependenceAnalyser(prog);

-      varDepAnalyser.Analyse();

-    }

-

-    public void Analyse() {

-      if (CommandLineOptions.Clo.Trace) {

-        Console.WriteLine("Candidate dependence analysis: Getting candidates");

-      }

-

-      candidates = GetCandidates();

-

-      DetermineCandidateVariableDependences();

-

-      ConstructCandidateDependenceGraph();

-

-      ConstructStagesDAG();

-

-    }

-

-    private void ConstructStagesDAG()

-    {

-      if (CommandLineOptions.Clo.Trace)

-      {

-        Console.WriteLine("Candidate dependence analysis: Computing SCCs");

-      }

-

-      Adjacency<string> next = new Adjacency<string>(CandidateDependences.Successors);

-      Adjacency<string> prev = new Adjacency<string>(CandidateDependences.Predecessors);

-      SCCs = new StronglyConnectedComponents<string>(

-        CandidateDependences.Nodes, next, prev);

-      SCCs.Compute();

-

-      if (CommandLineOptions.Clo.Trace)

-      {

-        Console.WriteLine("Candidate dependence analysis: Building stages DAG");

-      }

-

-      Dictionary<string, SCC<string>> rep = new Dictionary<string, SCC<string>>();

-      foreach (var scc in SCCs)

-      {

-        foreach (var s in scc)

-        {

-          rep[s] = scc;

-        }

-      }

-

-      StagesDAG = new Graph<SCC<string>>();

-

-      foreach (var edge in CandidateDependences.Edges)

-      {

-        if (rep[edge.Item1] != rep[edge.Item2])

-        {

-          StagesDAG.AddEdge(rep[edge.Item1], rep[edge.Item2]);

-        }

-      }

-

-      SCC<string> dummy = new SCC<string>();

-      foreach (var scc in SCCs)

-      {

-        StagesDAG.AddEdge(scc, dummy);

-      }

-    }

-

-    private void ConstructCandidateDependenceGraph()

-    {

-      if (CommandLineOptions.Clo.Trace)

-      {

-        Console.WriteLine("Candidate dependence analysis: Building dependence graph");

-      }

-

-      ICandidateReachabilityChecker reachabilityChecker;

-      

-      if(CommandLineOptions.Clo.StagedHoudiniReachabilityAnalysis) {

-        reachabilityChecker = new CandidateReachabilityChecker(prog, candidates);

-      } else {

-        reachabilityChecker = new DummyCandidateReachabilityChecker();

-      }

-

-      CandidateDependences = new Graph<string>();

-      foreach (var c in candidates)

-      {

-        CandidateDependences.AddEdge(c, c);

-        foreach (var vd in candidateDependsOn[c])

-        {

-          if (variableDirectlyReferredToByCandidates.ContainsKey(vd))

-          {

-            foreach (var d in variableDirectlyReferredToByCandidates[vd])

-            {

-              if(reachabilityChecker.MayReach(d, c))

-              {

-                CandidateDependences.AddEdge(c, d);

-              }

-            }

-          }

-        }

-      }

-

-      if(CommandLineOptions.Clo.StagedHoudiniMergeIgnoredCandidates) {

-        MergeIgnoredCandidates();

-      }

-

-    }

-

-    private void MergeIgnoredCandidates()

-    {

-      var IgnoredCandidatesToVariables = new Dictionary<string, HashSet<Variable>>();

-      foreach(var c in candidates) {

-        IgnoredCandidatesToVariables[c] = new HashSet<Variable>();

-      }

-      foreach(var ci in CandidateInstances()) {

-        if(!IgnoredCandidatesToVariables.ContainsKey(ci.Candidate)) {

-          continue;

-        }

-        VariableCollector vc = new VariableCollector();

-        vc.Visit(ci.Expr);

-        if(vc.usedVars.Select(Item => varDepAnalyser.VariableRelevantToAnalysis(Item, ci.Proc)).Count() != 0) {

-          continue;

-        }

-        foreach(var v in vc.usedVars) {

-          if(varDepAnalyser.Ignoring(v, ci.Proc)) {

-            IgnoredCandidatesToVariables[ci.Candidate].Add(v);

-          }

-        }

-      }

-      foreach(var c in IgnoredCandidatesToVariables.Keys) {

-        foreach(var d in IgnoredCandidatesToVariables.Keys) {

-          if(c == d) {

-            continue;

-          }

-          if(IgnoredCandidatesToVariables[c].Equals(IgnoredCandidatesToVariables[d])) {

-            CandidateDependences.AddEdge(c, d);

-          }

-        }

-      }

-    }

-

-

-

-    private void DetermineCandidateVariableDependences()

-    {

-      if (CommandLineOptions.Clo.Trace)

-      {

-        Console.WriteLine("Candidate dependence analysis: Working out what candidates depend on");

-      }

-      candidateDependsOn = new Dictionary<string, HashSet<VariableDescriptor>>();

-      variableDirectlyReferredToByCandidates = new Dictionary<VariableDescriptor, HashSet<string>>();

-      foreach (var c in candidates)

-      {

-        candidateDependsOn[c] = new HashSet<VariableDescriptor>();

-      }

-

-      foreach(var candidateInstance in CandidateInstances()) {

-        AddDependences(candidateInstance);

-      }

-

-    }

-

-    private IEnumerable<CandidateInstance> CandidateInstances()

-    {

-      foreach (var impl in prog.Implementations)

-      {

-        foreach (var b in impl.Blocks) {

-          foreach (Cmd cmd in b.Cmds)

-          {

-            var p = cmd as PredicateCmd;

-            if (p != null)

-            {

-              string c;

-              if(Houdini.MatchCandidate(p.Expr, candidates, out c)) {

-                yield return new CandidateInstance(c, impl.Name, p.Expr);

-              }

-            }

-          }

-        }

-      }

-

-      foreach (var proc in prog.Procedures)

-      {

-        foreach (Requires r in proc.Requires)

-        {

-          string c;

-          if(Houdini.MatchCandidate(r.Condition, candidates, out c)) {

-            yield return new CandidateInstance(c, proc.Name, r.Condition);

-          }

-        }

-        foreach (Ensures e in proc.Ensures)

-        {

-          string c;

-          if(Houdini.MatchCandidate(e.Condition, candidates, out c)) {

-            yield return new CandidateInstance(c, proc.Name, e.Condition);

-          }

-        }

-      }

-    }

-

-    private bool FindInDAG(Graph<SCC<string>> DAG, SCC<string> toFind, SCC<string> start) {

-      if (toFind == start) {

-        return true;

-      }

-      foreach (var n in DAG.Successors(start)) {

-        if (FindInDAG(DAG, toFind, n)) {

-          return true;

-        }

-      }

-      return false;

-    }

-

-    private void AddDependences(CandidateInstance ci) {

-      VariableCollector vc = new VariableCollector();

-      vc.VisitExpr(ci.Expr);

-

-      foreach (var v in vc.usedVars.Where(Item => varDepAnalyser.VariableRelevantToAnalysis(Item, ci.Proc))) {

-        VariableDescriptor vd =

-          varDepAnalyser.MakeDescriptor(ci.Proc, v);

-        if (!variableDirectlyReferredToByCandidates.ContainsKey(vd)) {

-          variableDirectlyReferredToByCandidates[vd] = new HashSet<string>();

-        }

-        variableDirectlyReferredToByCandidates[vd].Add(ci.Candidate);

-

-        foreach (var w in varDepAnalyser.DependsOn(vd)) {

-          candidateDependsOn[ci.Candidate].Add(w);

-        }

-      }

-    }

-

-    private bool IsStageDependence(SCC<string> Src, SCC<string> Dst) {

-      foreach (var c in Src) {

-        foreach (var d in CandidateDependences.Successors(c)) {

-          if (Dst.Contains(d)) {

-            return true;

-          }

-        }

-      }

-      return false;

-    }

-

-

-    public void dump() {

-

-      if(CommandLineOptions.Clo.DebugStagedHoudini) {

-        varDepAnalyser.dump();

-      }

-

-      /*Console.WriteLine("Candidates and the variables they depend on");

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

-      foreach (var entry in candidateDependsOn) {

-        Console.WriteLine(entry.Key + " <- ");

-        foreach (var vd in entry.Value) {

-          Console.WriteLine("  " + vd + ", ");

-        }

-      }

-

-      Console.WriteLine("");

-

-      Console.WriteLine("Variables and the candidates that directly refer to them");

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

-      foreach (var entry in variableDirectlyReferredToByCandidates) {

-        Console.WriteLine(entry.Key + " <- ");

-        foreach (var candidate in entry.Value) {

-          Console.WriteLine("  " + candidate + ", ");

-        }

-      }

-

-      Console.WriteLine("");*/

-

-      /*

-      Console.WriteLine("Candidate dependence graph");

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

-      foreach (var c in CandidateDependences.Nodes) {

-        Console.WriteLine(c + " <- ");

-        foreach (var d in CandidateDependences.Successors(c)) {

-          Console.WriteLine("  " + d);

-        }

-      }*/

-

-      Console.WriteLine("");

-

-      Console.WriteLine("Strongly connected components");

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

-

-      List<SCC<string>> Components = StagesDAG.TopologicalSort().ToList();

-

-      for (int i = 0; i < Components.Count(); i++) {

-        Console.Write(i + ": ");

-        DumpSCC(Components[i]);

-        Console.WriteLine(); Console.WriteLine();

-      }

-

-      Console.WriteLine("Stages DAG");

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

-      for (int i = 0; i < Components.Count(); i++) {

-        Console.Write(i + " -> { ");

-        bool first = true;

-        foreach (var d in StagesDAG.Successors(Components[i])) {

-          if (first) {

-            first = false;

-          }

-          else {

-            Console.Write(", ");

-          }

-          Console.Write(Components.IndexOf(d));

-        }

-        Console.WriteLine(" }");

-      }

-    

-    }

-

-    private static void DumpSCC(SCC<string> component) {

-      var sortedComponent = component.ToList();

-      sortedComponent.Sort();

-      Console.Write("{ ");

-      bool first = true;

-      foreach (var s in sortedComponent) {

-        if (first) {

-          first = false;

-        }

-        else {

-          Console.Write(", ");

-        }

-        Console.Write(s);

-      }

-      Console.Write(" }");

-    }

-

-    private IEnumerable<string> GetCandidates() {

-      return prog.Variables.Where(Item =>

-        QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name);

-    }

-

-

-    public StagedHoudiniPlan ApplyStages() {

-

-        if (NoStages())

-        {

-            return null;

-        }

-

-        #region Assign candidates to stages at a given level of granularity

-      

-        switch(CommandLineOptions.Clo.StagedHoudini) {

-          case COARSE_STAGES:

-            Plan = ComputeCoarseStages();

-            break;

-          case FINE_STAGES:

-            Plan = ComputeFineStages();

-            break;

-          case BALANCED_STAGES:

-            Plan = ComputeBalancedStages();

-            break;

-          default:

-            Debug.Assert(false);

-            Plan = null;

-            break;

-        }

-        

-        foreach(var c in candidates) {

-          Debug.Assert(Plan.StageForCandidate(c) != null);

-        }

-        #endregion

-

-        #region Generate boolean variables to control stages

-        var stageToActiveBoolean = new Dictionary<int, Constant>();

-        var stageToCompleteBoolean = new Dictionary<int, Constant>();

-

-        foreach (var stage in Plan)

-        {

-            var stageActive = new Constant(Token.NoToken,

-                new TypedIdent(Token.NoToken, "_stage_" + stage.GetId() + "_active", Type.Bool),

-                false);

-            stageActive.AddAttribute("stage_active", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) });

-            prog.AddTopLevelDeclaration(stageActive);

-            stageToActiveBoolean[stage.GetId()] = stageActive;

-

-            var stageComplete = new Constant(Token.NoToken, 

-                new TypedIdent(Token.NoToken, "_stage_" + stage.GetId() + "_complete", Type.Bool),

-                false);

-            stageComplete.AddAttribute("stage_complete", new object[] { new LiteralExpr(Token.NoToken, BigNum.FromInt(stage.GetId())) });

-            prog.AddTopLevelDeclaration(stageComplete);

-            stageToCompleteBoolean[stage.GetId()] = stageComplete;

-        }

-        #endregion

-

-        #region Adapt candidate assertions to take account of stages

-        foreach (var b in prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item))

-        {

-            List<Cmd> newCmds = new List<Cmd>();

-            foreach (var cmd in b.Cmds)

-            {

-                var a = cmd as AssertCmd;

-                string c;

-                if (a != null && (Houdini.MatchCandidate(a.Expr, candidates, out c)))

-                {

-                    newCmds.Add(new AssertCmd(a.tok, Houdini.AddConditionToCandidate(a.Expr,

-                        new IdentifierExpr(Token.NoToken, stageToActiveBoolean[Plan.StageForCandidate(c).GetId()]), c), a.Attributes));

-                    newCmds.Add(new AssumeCmd(a.tok, Houdini.AddConditionToCandidate(a.Expr,

-                        new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[Plan.StageForCandidate(c).GetId()]), c), a.Attributes));

-                }

-                else

-                {

-                    newCmds.Add(cmd);

-                }

-            }

-            b.Cmds = newCmds;

-        }

-        #endregion

-

-        #region Adapt candidate pre/postconditions to take account of stages

-        foreach (var p in prog.Procedures)

-        {

-

-          #region Handle the preconditions

-          List<Requires> newRequires = new List<Requires>();

-          foreach(Requires r in p.Requires) {

-            string c;

-            if (Houdini.MatchCandidate(r.Condition, candidates, out c)) {

-              newRequires.Add(new Requires(r.tok, false, 

-                Houdini.AddConditionToCandidate(r.Condition,

-                new IdentifierExpr(Token.NoToken, stageToActiveBoolean[Plan.StageForCandidate(c).GetId()]), c),

-                r.Comment, r.Attributes));

-              newRequires.Add(new Requires(r.tok, true, 

-                Houdini.AddConditionToCandidate(r.Condition,

-                new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[Plan.StageForCandidate(c).GetId()]), c),

-                r.Comment, r.Attributes));

-            } else {

-              newRequires.Add(r);

-            }

-          }

-          p.Requires = newRequires;

-          #endregion

-

-          #region Handle the postconditions

-          List<Ensures> newEnsures = new List<Ensures>();

-          foreach(Ensures e in p.Ensures) {

-            string c;

-            if (Houdini.MatchCandidate(e.Condition, candidates, out c)) {

-              int stage = Plan.StageForCandidate(c).GetId();

-              Constant activeBoolean = stageToActiveBoolean[stage];

-              newEnsures.Add(new Ensures(e.tok, false, 

-                Houdini.AddConditionToCandidate(e.Condition,

-                new IdentifierExpr(Token.NoToken, activeBoolean), c),

-                e.Comment, e.Attributes));

-              newEnsures.Add(new Ensures(e.tok, true, 

-                Houdini.AddConditionToCandidate(e.Condition,

-                new IdentifierExpr(Token.NoToken, stageToCompleteBoolean[stage]), c),

-                e.Comment, e.Attributes));

-            } else {

-              newEnsures.Add(e);

-            }

-          }

-          p.Ensures = newEnsures;

-          #endregion

-

-        }

-        #endregion

-

-        return Plan;

-

-    }

-

-    private int FindLargestStage() {

-      return StagesDAG.Nodes.Select(Item => Item.Count()).Max();

-    }

-

-

-    private StagedHoudiniPlan ComputeCoarseStages()

-    {

-        foreach(var n in StagesDAG.Nodes) {

-          Debug.Assert(!StagesDAG.Successors(n).Contains(n));

-        }

-

-        Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();

-

-        var done = new Dictionary<SCC<string>, ScheduledStage>();

-        done[GetStartNodeOfStagesDAG()] = new ScheduledStage(0, new HashSet<string>());

-

-        for(int stageId = 1; done.Count() != StagesDAG.Nodes.Count(); stageId++)

-        {

-            var Stage = new ScheduledStage(stageId, new HashSet<string>());

-            HashSet<SCC<string>> AssignedToThisStage = new HashSet<SCC<string>>();

-

-            foreach (var n in StagesDAG.Nodes.Where(Item => !done.ContainsKey(Item)))

-            {

-              if(StagesDAG.Successors(n).Where(Item => !done.ContainsKey(Item)).Count() == 0) {

-                foreach(var s in StagesDAG.Successors(n)) {

-                  Debug.Assert(s != n);

-                  Debug.Assert(Stage != done[s]);

-                  Dependences.AddEdge(Stage, done[s]);

-                }

-                foreach (var c in n)

-                {

-                  Stage.AddCandidate(c);

-                }

-                AssignedToThisStage.Add(n);

-              }

-            }

-

-            foreach(var n in AssignedToThisStage) {

-              done[n] = Stage;

-            }

-        }

-        return new StagedHoudiniPlan(Dependences);

-    }

-

-    private StagedHoudiniPlan ComputeBalancedStages()

-    {

-      Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();

-      var done = new Dictionary<SCC<string>, ScheduledStage>();

-      done[GetStartNodeOfStagesDAG()] = new ScheduledStage(0, new HashSet<string>());

-

-      int maxStageSize = 200;

-

-      for(int stageId = 1; done.Count() != StagesDAG.Nodes.Count(); stageId++)

-      {

-        int stageSize = 0;

-        ScheduledStage Stage = new ScheduledStage(stageId, new HashSet<string>());

-        HashSet<SCC<string>> AddedToThisStage = new HashSet<SCC<string>>();

-

-        foreach (var n in StagesDAG.Nodes.Where(Item => !done.ContainsKey(Item)))

-        {

-          if(stageSize + n.Count() > maxStageSize) {

-            continue;

-          }

-          if(StagesDAG.Successors(n).Where(Item => !done.ContainsKey(Item)).Count() == 0) {

-            foreach (var c in n)

-            {

-              Stage.AddCandidate(c);

-              stageSize++;

-            }

-            foreach(var s in StagesDAG.Successors(n)) {

-              Dependences.AddEdge(Stage, done[s]);

-            }

-            AddedToThisStage.Add(n);

-          }

-        }

-        foreach(var n in AddedToThisStage) {

-          done[n] = Stage;

-        }

-        if(stageSize == 0) {

-          maxStageSize *= 2;

-        }

-      }

-      return new StagedHoudiniPlan(Dependences);

-    }

-

-    private StagedHoudiniPlan ComputeFineStages()

-    {

-      Graph<ScheduledStage> Dependences = new Graph<ScheduledStage>();

-      var done = new Dictionary<SCC<string>, ScheduledStage>();

-

-      List<SCC<string>> components = StagesDAG.TopologicalSort().ToList();

-      components.Reverse();

-

-      for (int i = 0; i < components.Count(); i++)

-      {

-        ScheduledStage Stage = new ScheduledStage(i, new HashSet<string>());

-        done[components[i]] = Stage;

-        foreach (var c in components[i])

-        {

-          Stage.AddCandidate(c);

-        }

-        foreach(var s in StagesDAG.Successors(components[i])) {

-          Dependences.AddEdge(Stage, done[s]);

-        }

-      }

-      return new StagedHoudiniPlan(Dependences);

-    }

-

-    private SCC<string> GetStartNodeOfStagesDAG()

-    {

-      return StagesDAG.Nodes.Where(Item => StagesDAG.Successors(Item).Count() == 0).

-        ToList()[0];

-    }

-

-    private bool NoStages()

-    {

-        return candidates.Count() == 0 || StagesDAG.Nodes.Count() == 0;

-    }

-  }

-

-  interface ICandidateReachabilityChecker {

-    bool MayReach(string c, string d);

-  }

-

-  class DummyCandidateReachabilityChecker : ICandidateReachabilityChecker {

-    public bool MayReach(string c, string d) {

-      return true;

-    }

-  }

-

-  class CandidateReachabilityChecker : ICandidateReachabilityChecker {

-

-    private enum PrePost {

-      PRE, POST

-    }

-

-    private Program prog;

-    private IEnumerable<string> candidates;

-    private IInterproceduralReachabilityGraph reachabilityGraph;

-    private Dictionary<string, HashSet<object>> candidateToOccurences;

-

-    internal CandidateReachabilityChecker(Program prog, IEnumerable<string> candidates) {

-      this.prog = prog;

-      this.candidates = candidates;

-      this.reachabilityGraph = new InterproceduralReachabilityGraph(prog);

-      this.candidateToOccurences = new Dictionary<string,HashSet<object>>();

-

-      // Add all candidate occurrences in blocks

-      foreach(Block b in prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item)) {

-        foreach(Cmd cmd in b.Cmds) {

-          AssertCmd assertCmd = cmd as AssertCmd;

-          if(assertCmd != null) {

-            string c;

-            if(Houdini.MatchCandidate(assertCmd.Expr, candidates, out c)) {

-              AddCandidateOccurrence(c, b);

-            }

-          }

-        }

-      }

-

-      // Add all candidate occurrences in preconditions

-      foreach(var proc in prog.Procedures) {

-        foreach(Requires r in proc.Requires) {

-          string c;

-          if(Houdini.MatchCandidate(r.Condition, candidates, out c)) {

-            AddCandidateOccurrence(c, new Tuple<string, PrePost>(proc.Name, PrePost.PRE));

-          }

-        }

-      }

-

-      // Add all candidate occurrences in preconditions

-      foreach(var proc in prog.Procedures) {

-        foreach(Ensures e in proc.Ensures) {

-          string c;

-          if(Houdini.MatchCandidate(e.Condition, candidates, out c)) {

-            AddCandidateOccurrence(c, new Tuple<string, PrePost>(proc.Name, PrePost.POST));

-          }

-        }

-      }

-      

-    }

-

-    private void AddCandidateOccurrence(string c, object o) {

-      Debug.Assert(o is Block || o is Tuple<string, PrePost>);

-      if(!candidateToOccurences.ContainsKey(c)) {

-        candidateToOccurences[c] = new HashSet<object>();

-      }

-      candidateToOccurences[c].Add(o);

-    }

-

-    public bool MayReach(string c, string d) {

-      foreach(object cOccurrence in candidateToOccurences[c]) {

-        foreach(object dOccurrence in candidateToOccurences[d]) {

-          if(OccurrencesMayReach(cOccurrence, dOccurrence)) {

-            return true;

-          }

-        }

-      }

-      return false;

-    }

-

-    private bool OccurrencesMayReach(object cOccurrence, object dOccurrence) {

-      Debug.Assert(cOccurrence is Block || cOccurrence is Tuple<string, PrePost>);

-      Debug.Assert(dOccurrence is Block || dOccurrence is Tuple<string, PrePost>);

-

-      Block cInterproceduralBlock = GetInterproceduralBlock(cOccurrence);

-      Block dInterproceduralBlock = GetInterproceduralBlock(dOccurrence);

-

-      return reachabilityGraph.MayReach(cInterproceduralBlock, dInterproceduralBlock);

-

-      throw new NotImplementedException();

-    }

-

-    private Block GetInterproceduralBlock(object cOccurrence)

-    {

-      Debug.Assert(cOccurrence is Block || cOccurrence is Tuple<string, PrePost>);

-

-      var stringPrePostPair = cOccurrence as Tuple<string, PrePost>;

-      if(stringPrePostPair != null) {

-        if(stringPrePostPair.Item2 == PrePost.PRE) {

-          return reachabilityGraph.GetNewEntryBlock(stringPrePostPair.Item1);

-        } else {

-          return reachabilityGraph.GetNewExitBlock(stringPrePostPair.Item1);

-        }

-      }

-

-      return reachabilityGraph.GetNewBlock((Block)cOccurrence);

-

-    }

-  }

-

-  class CandidateInstance {

-    public string Candidate;

-    public string Proc;

-    public Expr Expr;

-

-    internal CandidateInstance(string Candidate, string Proc, Expr Expr) {

-      this.Candidate = Candidate;

-      this.Proc = Proc;

-      this.Expr = Expr;

-    }

-  }

-

-}

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index fef24688..986d0fff 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -1164,7 +1164,7 @@ namespace Microsoft.Boogie.Houdini {
     }

 

     /// <summary>

-    /// Transforms given program based on Houdini assignment.  If a constant is assigned "true",

+    /// Transforms given program based on Houdini outcome.  If a constant is assigned "true",

     /// any preconditions or postconditions guarded by the constant are made free, and any assertions 

     /// guarded by the constant are replaced with assumptions.

     /// 

@@ -1172,9 +1172,12 @@ namespace Microsoft.Boogie.Houdini {
     /// guarded by the constant are replaced with "true", and assertions guarded by the constant

     /// are removed.

     /// 

-    /// In addition, all Houdini constants are removed.

+    /// In addition, all Houdini constants are removed from the program.

     /// </summary>

-    public void ApplyAssignment(Program prog) {

+    public static void ApplyAssignment(Program prog, HoudiniOutcome outcome) {

+

+      var Candidates = prog.TopLevelDeclarations.OfType<Constant>().Where

+            (Item => QKeyValue.FindBoolAttribute(Item.Attributes, "existential")).Select(Item => Item.Name);

 

       // Treat all assertions

       // TODO: do we need to also consider assumptions?

@@ -1183,9 +1186,9 @@ namespace Microsoft.Boogie.Houdini {
         foreach (Cmd cmd in block.Cmds) {

           string c;

           AssertCmd assertCmd = cmd as AssertCmd;

-          if (assertCmd != null && MatchCandidate(assertCmd.Expr, out c)) {

-            var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];

-            if (currentHoudiniState.Assignment[cVar]) {

+          if (assertCmd != null && MatchCandidate(assertCmd.Expr, Candidates, out c)) {

+            var cVar = outcome.assignment.Keys.Where(item => item.Equals(c)).ToList()[0];

+            if (outcome.assignment[cVar]) {

               Dictionary<Variable, Expr> cToTrue = new Dictionary<Variable, Expr>();

               Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0];

               cToTrue[cVarProg] = Expr.True;

@@ -1205,9 +1208,9 @@ namespace Microsoft.Boogie.Houdini {
         List<Requires> newRequires = new List<Requires>();

         foreach (Requires r in proc.Requires) {

           string c;

-          if (MatchCandidate(r.Condition, out c)) {

-            var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];

-            if (currentHoudiniState.Assignment[cVar]) {

+          if (MatchCandidate(r.Condition, Candidates, out c)) {

+            var cVar = outcome.assignment.Keys.Where(item => item.Equals(c)).ToList()[0];

+            if (outcome.assignment[cVar]) {

               Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0];

               Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();

               subst[cVarProg] = Expr.True;

@@ -1225,9 +1228,9 @@ namespace Microsoft.Boogie.Houdini {
         List<Ensures> newEnsures = new List<Ensures>();

         foreach (Ensures e in proc.Ensures) {

           string c;

-          if (MatchCandidate(e.Condition, out c)) {

-            var cVar = currentHoudiniState.Assignment.Keys.Where(item => item.Name.Equals(c)).ToList()[0];

-            if (currentHoudiniState.Assignment[cVar]) {

+          if (MatchCandidate(e.Condition, Candidates, out c)) {

+            var cVar = outcome.assignment.Keys.Where(item => item.Equals(c)).ToList()[0];

+            if (outcome.assignment[cVar]) {

               Variable cVarProg = prog.Variables.Where(item => item.Name.Equals(c)).ToList()[0];

               Dictionary<Variable, Expr> subst = new Dictionary<Variable, Expr>();

               subst[cVarProg] = Expr.True;

@@ -1244,8 +1247,8 @@ namespace Microsoft.Boogie.Houdini {
       }

 

       // Remove the existential constants

-      prog.RemoveTopLevelDeclarations(item => (item is Variable) && 

-           (houdiniConstants.Select(c => c.Name).Contains((item as Variable).Name)));

+      prog.RemoveTopLevelDeclarations(item => (item is Constant) && 

+               (Candidates.Any(item2 => item2.Equals((item as Constant).Name))));

     }

 

   }

diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj
index bed0ef6c..dcb42ef7 100644
--- a/Source/Houdini/Houdini.csproj
+++ b/Source/Houdini/Houdini.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <PropertyGroup>

     <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

@@ -97,7 +97,7 @@
     </Compile>

     <Compile Include="AbstractHoudini.cs" />

     <Compile Include="Checker.cs" />

-    <Compile Include="CandidateDependenceAnalyser.cs" />

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

     <Compile Include="Houdini.cs" />

     <Compile Include="StagedHoudini.cs" />

     <Compile Include="ConcurrentHoudini.cs" />

@@ -151,4 +151,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file
diff --git a/Source/Houdini/StagedHoudini.cs b/Source/Houdini/StagedHoudini.cs
index 56d4a07a..49482b3d 100644
--- a/Source/Houdini/StagedHoudini.cs
+++ b/Source/Houdini/StagedHoudini.cs
@@ -31,12 +31,18 @@ namespace Microsoft.Boogie.Houdini
         houdiniInstances[i] = new List<Houdini>();

       }

 

-      var candidateDependenceAnalyser = new CandidateDependenceAnalyser(program);

-      candidateDependenceAnalyser.Analyse();

-      this.plan = candidateDependenceAnalyser.ApplyStages();

+      var annotationDependenceAnalyser = new AnnotationDependenceAnalyser(program);

+      annotationDependenceAnalyser.Analyse();

+      this.plan = annotationDependenceAnalyser.ApplyStages();

       if (CommandLineOptions.Clo.Trace)

       {

-        candidateDependenceAnalyser.dump();

+        annotationDependenceAnalyser.dump();

+

+        if(CommandLineOptions.Clo.DebugStagedHoudini) {

+          Console.WriteLine("Plan\n====\n");

+          Console.WriteLine(this.plan);

+        }

+        

         EmitProgram("staged.bpl");

       }

     }

@@ -68,7 +74,6 @@ namespace Microsoft.Boogie.Houdini
           h[0].Close();

         }

       }

-      Console.WriteLine("Used " + count + " houdini instances");

       #endregion

 

       return UnifyOutcomes();

@@ -228,11 +233,11 @@ namespace Microsoft.Boogie.Houdini
   public class StagedHoudiniPlan : IEnumerable<ScheduledStage> {

 

     private Graph<ScheduledStage> ScheduledStages;

-    private Dictionary<string, ScheduledStage> CandidateToStage;

+    private Dictionary<string, ScheduledStage> AnnotationToStage;

 

     internal StagedHoudiniPlan(Graph<ScheduledStage> ScheduledStages) {

       this.ScheduledStages = ScheduledStages;

-      this.CandidateToStage = new Dictionary<string, ScheduledStage>();

+      this.AnnotationToStage = new Dictionary<string, ScheduledStage>();

       foreach(var s in this) {

         Debug.Assert(!GetDependences(s).Contains(s));

       }

@@ -268,13 +273,13 @@ namespace Microsoft.Boogie.Houdini
         return this.GetEnumerator();

     }

 

-    internal ScheduledStage StageForCandidate(string c) {

-      if(CandidateToStage.ContainsKey(c)) {

-        return CandidateToStage[c];

+    internal ScheduledStage StageForAnnotation(string c) {

+      if(AnnotationToStage.ContainsKey(c)) {

+        return AnnotationToStage[c];

       }

       foreach(var s in ScheduledStages.Nodes) {

-        if(s.ContainsCandidate(c)) {

-          CandidateToStage[c] = s;

+        if(s.ContainsAnnotation(c)) {

+          AnnotationToStage[c] = s;

           return s;

         }

       }

@@ -299,19 +304,19 @@ namespace Microsoft.Boogie.Houdini
 

   public class ScheduledStage {

     private int Id;

-    private HashSet<string> Candidates;

+    private HashSet<string> Annotations;

 

-    public ScheduledStage(int Id, HashSet<string> Candidates) {

+    public ScheduledStage(int Id, HashSet<string> Annotations) {

       this.Id = Id;

-      this.Candidates = Candidates;

+      this.Annotations = Annotations;

     }

 

-    internal void AddCandidate(string c) {

-      Candidates.Add(c);

+    internal void AddAnnotation(string a) {

+      Annotations.Add(a);

     }

 

-    internal bool ContainsCandidate(string c) {

-      return Candidates.Contains(c);

+    internal bool ContainsAnnotation(string a) {

+      return Annotations.Contains(a);

     }

 

     public int GetId() {

@@ -319,13 +324,13 @@ namespace Microsoft.Boogie.Houdini
     }

 

     public int Count() {

-      return Candidates.Count();

+      return Annotations.Count();

     }

 

     public override string ToString()

     {

       string result = "ID: " + Id + "{ ";

-      foreach(var c in Candidates) {

+      foreach(var c in Annotations) {

         result += c + " ";

       }

       result += "}\n";