diff options
Diffstat (limited to 'Source/Houdini/AnnotationDependenceAnalyser.cs')
-rw-r--r-- | Source/Houdini/AnnotationDependenceAnalyser.cs | 1756 |
1 files changed, 878 insertions, 878 deletions
diff --git a/Source/Houdini/AnnotationDependenceAnalyser.cs b/Source/Houdini/AnnotationDependenceAnalyser.cs index e925d413..dacac233 100644 --- a/Source/Houdini/AnnotationDependenceAnalyser.cs +++ b/Source/Houdini/AnnotationDependenceAnalyser.cs @@ -1,878 +1,878 @@ -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")) {
- var tag = GetTagFromNonCandidateAttributes(p.Attributes);
- if (tag != null) {
- yield return new AnnotationInstance(tag, 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 {
- var tag = GetTagFromNonCandidateAttributes(r.Attributes);
- if (tag != null) {
- yield return new AnnotationInstance(tag, 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 {
- var tag = GetTagFromNonCandidateAttributes(e.Attributes);
- if (tag != null) {
- yield return new AnnotationInstance(tag, proc.Name, e.Condition);
- }
- }
- }
- }
- }
-
- internal static string GetTagFromNonCandidateAttributes(QKeyValue Attributes)
- {
- string tag = QKeyValue.FindStringAttribute(Attributes, "staged_houdini_tag");
- 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 bool OnlyRefersToConstants(Expr e) {
- VariableCollector vc = new VariableCollector();
- vc.Visit(e);
- return vc.usedVars.OfType<Constant>().Count() == vc.usedVars.Count();
- }
-
- 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;
- }
-
- if (OnlyRefersToConstants(Assertion.Expr)) {
- 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;
- }
-
- if (OnlyRefersToConstants(Req.Condition)) {
- 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;
- }
-
- if (OnlyRefersToConstants(Ens.Condition)) {
- 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())
- {
- Debug.Assert(false);
- var TrivialGraph = new Graph<ScheduledStage>();
- TrivialGraph.AddSource(new ScheduledStage(0, new HashSet<string>()));
- return new StagedHoudiniPlan(TrivialGraph);
- }
-
- #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);
- if (tag == null) {
- newCmds.Add(a);
- } else {
- 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 {
- string tag = GetTagFromNonCandidateAttributes(r.Attributes);
- if (tag == null) {
- newRequires.Add(r);
- } else {
- 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 {
- string tag = GetTagFromNonCandidateAttributes(e.Attributes);
- if (tag == null) {
- newEnsures.Add(e);
- } else {
- newEnsures.Add(new Ensures(e.tok, false,
- Expr.Imp(Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(tag).GetId()]), e.Condition),
- e.Comment, e.Attributes));
- newEnsures.Add(new Ensures(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 {
- var tag = AnnotationDependenceAnalyser.GetTagFromNonCandidateAttributes(assertCmd.Attributes);
- if (tag != null) {
- AddAnnotationOccurrence(tag, 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);
- if(tag != null) {
- 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);
- if(tag != null) {
- 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;
- }
- }
-
-}
+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")) { + var tag = GetTagFromNonCandidateAttributes(p.Attributes); + if (tag != null) { + yield return new AnnotationInstance(tag, 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 { + var tag = GetTagFromNonCandidateAttributes(r.Attributes); + if (tag != null) { + yield return new AnnotationInstance(tag, 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 { + var tag = GetTagFromNonCandidateAttributes(e.Attributes); + if (tag != null) { + yield return new AnnotationInstance(tag, proc.Name, e.Condition); + } + } + } + } + } + + internal static string GetTagFromNonCandidateAttributes(QKeyValue Attributes) + { + string tag = QKeyValue.FindStringAttribute(Attributes, "staged_houdini_tag"); + 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 bool OnlyRefersToConstants(Expr e) { + VariableCollector vc = new VariableCollector(); + vc.Visit(e); + return vc.usedVars.OfType<Constant>().Count() == vc.usedVars.Count(); + } + + 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; + } + + if (OnlyRefersToConstants(Assertion.Expr)) { + 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; + } + + if (OnlyRefersToConstants(Req.Condition)) { + 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; + } + + if (OnlyRefersToConstants(Ens.Condition)) { + 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()) + { + Debug.Assert(false); + var TrivialGraph = new Graph<ScheduledStage>(); + TrivialGraph.AddSource(new ScheduledStage(0, new HashSet<string>())); + return new StagedHoudiniPlan(TrivialGraph); + } + + #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); + if (tag == null) { + newCmds.Add(a); + } else { + 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 { + string tag = GetTagFromNonCandidateAttributes(r.Attributes); + if (tag == null) { + newRequires.Add(r); + } else { + 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 { + string tag = GetTagFromNonCandidateAttributes(e.Attributes); + if (tag == null) { + newEnsures.Add(e); + } else { + newEnsures.Add(new Ensures(e.tok, false, + Expr.Imp(Expr.Ident(stageToActiveBoolean[Plan.StageForAnnotation(tag).GetId()]), e.Condition), + e.Comment, e.Attributes)); + newEnsures.Add(new Ensures(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 { + var tag = AnnotationDependenceAnalyser.GetTagFromNonCandidateAttributes(assertCmd.Attributes); + if (tag != null) { + AddAnnotationOccurrence(tag, 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); + if(tag != null) { + 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); + if(tag != null) { + 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; + } + } + +} |