summaryrefslogtreecommitdiff
path: root/Source/Houdini/AnnotationDependenceAnalyser.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Houdini/AnnotationDependenceAnalyser.cs')
-rw-r--r--Source/Houdini/AnnotationDependenceAnalyser.cs1756
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;
+ }
+ }
+
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 13:01:48 +0000