diff options
| -rw-r--r-- | Source/Boogie.sln | 7 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 8 | ||||
| -rw-r--r-- | Source/Core/VariableDependenceAnalyser.cs | 32 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 2 | ||||
| -rw-r--r-- | Source/Houdini/AnnotationDependenceAnalyser.cs | 831 | ||||
| -rw-r--r-- | Source/Houdini/CandidateDependenceAnalyser.cs | 731 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.cs | 31 | ||||
| -rw-r--r-- | Source/Houdini/Houdini.csproj | 6 | ||||
| -rw-r--r-- | Source/Houdini/StagedHoudini.cs | 47 |
9 files changed, 904 insertions, 791 deletions
diff --git a/Source/Boogie.sln b/Source/Boogie.sln index aabaed90..be3b0422 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -1,8 +1,6 @@
Microsoft Visual Studio Solution File, Format Version 12.00
-# Visual Studio 2013
-VisualStudioVersion = 12.0.31101.0
-MinimumVisualStudioVersion = 10.0.40219.1
+# Visual Studio 2012
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758C1E3-824A-439F-AA2F-0BA1143E8C8D}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BoogieDriver", "BoogieDriver\BoogieDriver.csproj", "{DAB6BAA4-7AF7-449F-96AB-F58F34D03A7A}"
@@ -48,6 +46,9 @@ Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "UnitTests", "UnitTests", "{ EndProject
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = ".nuget", ".nuget", "{83CAF6FB-75EB-422D-B341-D61E07A0FAEB}"
ProjectSection(SolutionItems) = preProject
+ .nuget\NuGet.Config = .nuget\NuGet.Config
+ .nuget\NuGet.exe = .nuget\NuGet.exe
+ .nuget\NuGet.targets = .nuget\NuGet.targets
.nuget\packages.config = .nuget\packages.config
EndProjectSection
EndProject
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 35e1edc9..6bed4e75 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -447,8 +447,8 @@ namespace Microsoft.Boogie { public string StagedHoudini = null;
public bool DebugStagedHoudini = false;
public bool StagedHoudiniReachabilityAnalysis = false;
- public bool StagedHoudiniMergeIgnoredCandidates = false;
- public int StagedHoudiniThreads = 2;
+ public bool StagedHoudiniMergeIgnoredAnnotations = false;
+ public int StagedHoudiniThreads = 1;
public string VariableDependenceIgnore = null;
public string AbstractHoudini = null;
public bool UseUnsatCoreForContractInfer = false;
@@ -1018,9 +1018,9 @@ namespace Microsoft.Boogie { return true;
}
- case "stagedHoudiniMergeIgnoredCandidates": {
+ case "stagedHoudiniMergeIgnoredAnnotations": {
if (ps.ConfirmArgumentCount(0)) {
- StagedHoudiniMergeIgnoredCandidates = true;
+ StagedHoudiniMergeIgnoredAnnotations = true;
}
return true;
}
diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index c429e199..70e33581 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -141,7 +141,7 @@ namespace Microsoft.Boogie { dependsOnNonTransitive.AddEdge(descriptor, descriptor);
}
- foreach (var Proc in NonInlinedProcedures()) {
+ foreach (var Proc in prog.NonInlinedProcedures()) {
List<Variable> parameters = new List<Variable>();
parameters.AddRange(Proc.InParams);
@@ -152,7 +152,7 @@ namespace Microsoft.Boogie { }
}
- foreach (var Impl in NonInlinedImplementations()) {
+ foreach (var Impl in prog.NonInlinedImplementations()) {
List<Variable> locals = new List<Variable>();
locals.AddRange(Impl.LocVars);
@@ -163,16 +163,6 @@ namespace Microsoft.Boogie { }
}
- private IEnumerable<Procedure> NonInlinedProcedures() {
- return prog.Procedures.
- Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1);
- }
-
- private IEnumerable<Implementation> NonInlinedImplementations() {
- return prog.Implementations.
- Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1);
- }
-
private List<VariableDescriptor> ComputeDependencyChain(VariableDescriptor source, VariableDescriptor target, HashSet<VariableDescriptor> visited) {
if(source.Equals(target)) {
return new List<VariableDescriptor> { target };
@@ -259,7 +249,7 @@ namespace Microsoft.Boogie { }
ControllingBlockToVariables = ComputeControllingVariables(BlockToControllingBlocks);
- foreach (var Impl in NonInlinedImplementations()) {
+ foreach (var Impl in prog.NonInlinedImplementations()) {
if (CommandLineOptions.Clo.Trace) {
Console.WriteLine("Variable dependence analysis: Analysing " + Impl.Name);
@@ -345,7 +335,7 @@ namespace Microsoft.Boogie { 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 Impl in prog.NonInlinedImplementations()) {
foreach (var b in Impl.Blocks) {
result[b] = GetControlDependencyVariables(Impl.Name, b);
}
@@ -639,4 +629,18 @@ namespace Microsoft.Boogie { }
+ public static class Helper {
+
+ public static IEnumerable<Procedure> NonInlinedProcedures(this Program prog) {
+ return prog.Procedures.
+ Where(Item => QKeyValue.FindIntAttribute(Item.Attributes, "inline", -1) == -1);
+ }
+
+ public static IEnumerable<Implementation> NonInlinedImplementations(this Program prog) {
+ return prog.Implementations.
+ Where(Item => QKeyValue.FindIntAttribute(Item.Proc.Attributes, "inline", -1) == -1);
+ }
+
+ }
+
}
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 89f9a2c3..ae833dbf 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1348,7 +1348,7 @@ namespace Microsoft.Boogie return PipelineOutcome.Done;
}
- private static Program ProgramFromFile(string filename) {
+ public static Program ProgramFromFile(string filename) {
Program p = ParseBoogieProgram(new List<string> { filename }, false);
System.Diagnostics.Debug.Assert(p != null);
LinearTypeChecker linearTypeChecker;
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";
|