Staged Houdini

3 files changed, 394 insertions, 71 deletions

diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs
new file mode 100644
index 00000000..a7083497
--- /dev/null
+++ b/Source/Houdini/CandidateDependenceAnalyser.cs
@@ -0,0 +1,346 @@
+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 {

+

+  public class CandidateDependenceAnalyser {

+

+    private const int COARSE_STAGES = 1;

+    private const int FINE_STAGES = 2;

+

+    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;

+

+    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();

+

+      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>();

+      }

+

+      // Candidate loop invariants

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

+        foreach(var b in impl.Blocks) {

+          foreach (Cmd c in b.Cmds) {

+            var p = c as PredicateCmd;

+            if (p != null) {

+              CheckExpr(impl.Name, p.Expr);

+            }

+          }

+        }

+      }

+

+      foreach (var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {

+        foreach (Requires r in proc.Requires) {

+          CheckExpr(proc.Name, r.Condition);

+        }

+        foreach (Ensures e in proc.Ensures) {

+          CheckExpr(proc.Name, e.Condition);

+        }

+      }

+

+      if (CommandLineOptions.Clo.Trace) {

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

+      }

+

+      CandidateDependences = new Graph<string>();

+

+      foreach (var c in candidates) {

+        foreach (var vd in candidateDependsOn[c]) {

+          if (variableDirectlyReferredToByCandidates.ContainsKey(vd)) {

+            foreach (var d in variableDirectlyReferredToByCandidates[vd]) {

+              CandidateDependences.AddEdge(c, d);

+            }

+          }

+        }

+      }

+

+      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 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 CheckExpr(string proc, Expr e) {

+      string candidate;

+      Houdini.Houdini.MatchCandidate(e, candidates, out candidate);

+      if (candidate != null) {

+        VariableCollector vc = new VariableCollector();

+        vc.VisitExpr(e);

+

+        foreach (var v in vc.usedVars.Where(Item => !(Item is Constant))) {

+          VariableDescriptor vd =

+            varDepAnalyser.MakeDescriptor(proc, v);

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

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

+          }

+          variableDirectlyReferredToByCandidates[vd].Add(candidate);

+

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

+            candidateDependsOn[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() {

+

+      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("\n");

+      }

+

+      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.TopLevelDeclarations.OfType<Variable>().Where(Item =>

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

+    }

+

+

+    public void ApplyStages() {

+

+      IEnumerable<Constant> candidates = prog.TopLevelDeclarations.OfType<Constant>().

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

+

+      if (candidates.Count() == 0) {

+        return;

+      }

+

+      if (StagesDAG.Nodes.Count() == 0) {

+        return;

+      }

+

+      

+      Debug.Assert(CommandLineOptions.Clo.StagedHoudini == COARSE_STAGES ||

+                   CommandLineOptions.Clo.StagedHoudini == FINE_STAGES);

+

+      if (CommandLineOptions.Clo.StagedHoudini == COARSE_STAGES) {

+        SCC<string> start = null;

+        foreach (var n in StagesDAG.Nodes) {

+          if (StagesDAG.Successors(n).Count() == 0) {

+            start = n;

+            break;

+          }

+        }

+        System.Diagnostics.Debug.Assert(start != null);

+

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

+        done.Add(start);

+

+        bool finished = false;

+        int stageId = 0;

+        while (!finished) {

+          finished = true;

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

+          foreach (var n in StagesDAG.Nodes) {

+            if (!done.Contains(n)) {

+              finished = false;

+              bool ready = true;

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

+                if (!done.Contains(m)) {

+                  ready = false;

+                  break;

+                }

+              }

+              if (ready) {

+                stage.Add(n);

+                done.Add(n);

+              }

+            }

+          }

+

+          foreach (var scc in stage) {

+            foreach (var candidate in candidates) {

+              if (scc.Contains(candidate.Name)) {

+                candidate.Attributes = new QKeyValue(Token.NoToken, "stage_id", new List<object>() {

+                  new LiteralExpr(Token.NoToken, BigNum.FromInt(stageId))

+                }, candidate.Attributes);

+              }

+            }

+          }

+

+          stageId++;

+        }

+

+      }

+      else {

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

+        components.Reverse();

+

+        System.Diagnostics.Debug.Assert(components[0].Count() == 0);

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

+          foreach (var c in candidates) {

+            if (components[i].Contains(c.Name)) {

+              c.Attributes = new QKeyValue(Token.NoToken, "stage_id", new List<object>() {

+              new LiteralExpr(Token.NoToken, BigNum.FromInt(i - 1))

+            }, c.Attributes);

+            }

+          }

+

+        }

+

+      }

+

+

+

+    }

+  }

+

+}

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 6d740fdb..a39f4fdb 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -328,7 +328,7 @@ namespace Microsoft.Boogie.Houdini {
       

       if (CommandLineOptions.Clo.Trace)

         Console.WriteLine("Building call graph...");

-      this.callGraph = BuildCallGraph();

+      this.callGraph = Program.BuildCallGraph(program);

       if (CommandLineOptions.Clo.Trace)

         Console.WriteLine("Number of implementations = {0}", callGraph.Nodes.Count);

 

@@ -493,36 +493,6 @@ namespace Microsoft.Boogie.Houdini {
         // contant -> set of implementations that have an assume command with that constant

         public Dictionary<string, HashSet<Implementation>> assumedInImpl { get; private set; }

     }

-      

-    private Graph<Implementation> BuildCallGraph() {

-      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;

-    }

     

     private WorkQueue BuildWorkList(Program program) {

       // adding implementations to the workqueue from the bottom of the call graph upwards

@@ -1059,9 +1029,10 @@ namespace Microsoft.Boogie.Houdini {
 

     /// <summary>

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

-    /// any preconditions or postconditions guarded by the constant are replaced with

-    /// regular conditions, and any assertions guarded by the constant are replaced with

-    /// assumptions.  If a constant is assigned "false", any preconditions or postconditions

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

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

+    /// 

+    /// If a constant is assigned "false", any preconditions or postconditions

     /// guarded by the constant are replaced with "true", and assertions guarded by the constant

     /// are removed.

     /// 

@@ -1094,46 +1065,51 @@ namespace Microsoft.Boogie.Houdini {
         block.Cmds = newCmds;

       }

 

-      // Treat requires and ensures

-      new ApplyAssignmentVisitor(this, prog).VisitProgram(prog);

-

-      // Remove the existential constants

-      prog.TopLevelDeclarations.RemoveAll(item => (item is Variable) && 

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

-    }

-

-    class ApplyAssignmentVisitor : StandardVisitor {

-

-      private Houdini houdini;

-      private Program prog;

-

-      internal ApplyAssignmentVisitor(Houdini houdini, Program prog) {

-        this.houdini = houdini;

-        this.prog = prog;

-      }

-

-      public override Requires VisitRequires(Requires requires) {

-        requires.Condition = ApplyAssignment(requires.Condition);

-        return requires;

-      }

-

-      public override Ensures VisitEnsures(Ensures ensures) {

-        ensures.Condition = ApplyAssignment(ensures.Condition);

-        return ensures;

-      }

+      foreach (var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {

+        RequiresSeq newRequires = new RequiresSeq();

+        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]) {

+              Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];

+              Hashtable subst = new Hashtable();

+              subst[cVarProg] = Expr.True;

+              newRequires.Add(new Requires(Token.NoToken, true,

+                Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), r.Condition),

+                r.Comment, r.Attributes));

+            }

+          }

+          else {

+            newRequires.Add(r);

+          }

+        }

+        proc.Requires = newRequires;

 

-      private Expr ApplyAssignment(Expr e) {

-        string c;

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

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

-          Hashtable cToTrue = new Hashtable();

-          Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];

-          cToTrue[cVarProg] = houdini.currentHoudiniState.Assignment[cVar] ? Expr.True : Expr.False;

-          return Substituter.Apply(Substituter.SubstitutionFromHashtable(cToTrue), e);

+        EnsuresSeq newEnsures = new EnsuresSeq();

+        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]) {

+              Variable cVarProg = prog.TopLevelDeclarations.OfType<Variable>().Where(item => item.Name.Equals(c)).ToList()[0];

+              Hashtable subst = new Hashtable();

+              subst[cVarProg] = Expr.True;

+              newEnsures.Add(new Ensures(Token.NoToken, true,

+                Substituter.Apply(Substituter.SubstitutionFromHashtable(subst), e.Condition),

+                e.Comment, e.Attributes));

+            }

+          }

+          else {

+            newEnsures.Add(e);

+          }

         }

-        return e;

+        proc.Ensures = newEnsures;

       }

 

+      // Remove the existential constants

+      prog.TopLevelDeclarations.RemoveAll(item => (item is Variable) && 

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

     }

 

   }

diff --git a/Source/Houdini/Houdini.csproj b/Source/Houdini/Houdini.csproj
index 2d2b0373..06d68dba 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>

@@ -80,6 +80,7 @@
     </Compile>

     <Compile Include="AbstractHoudini.cs" />

     <Compile Include="Checker.cs" />

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

     <Compile Include="Houdini.cs" />

   </ItemGroup>

   <ItemGroup>