From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Source/Graph/Graph.cs | 2894 ++++++++++++++++++++++----------------------- Source/Graph/Graph.csproj | 398 +++---- Source/Graph/cce.cs | 384 +++--- 3 files changed, 1838 insertions(+), 1838 deletions(-) (limited to 'Source/Graph') diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 8e5479e3..7f636200 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -1,1447 +1,1447 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Linq; -using System.Collections.Generic; -using System.Text; // for StringBuilder -using System.Diagnostics.Contracts; -namespace Microsoft.Boogie.GraphUtil { - - internal static class Util { - private static string/*!*/ ListToString(IEnumerable xs) { - Contract.Ensures(Contract.Result() != null); - StringBuilder sb = new StringBuilder(); - sb.Append("["); - bool first = true; - foreach (T/*!*/ x in xs) { - Contract.Assert(x != null); - if (!first) - sb.Append(", "); - sb.Append(x.ToString()); - first = false; - } - sb.Append("]"); - return sb.ToString(); - } - public static string/*!*/ MapToString(Dictionary> d) { - Contract.Ensures(Contract.Result() != null); - StringBuilder sb = new StringBuilder(); - sb.Append("{"); - bool first = true; - foreach (KeyValuePair> de in d) { - if (!first) - sb.Append(", "); - Contract.Assert(!object.Equals(de.Key,default(Node))); - sb.Append(de.Key.ToString()); - sb.Append("~>"); - sb.Append(ListToString(de.Value)); - first = false; - } - sb.Append("}"); - return sb.ToString(); - } - } - - // own struct to represent possibly undefined values, because Mono does - // not like arrays with element type T! or T? - public struct Maybe { - private T Value; - public bool IsSet; // initialised with false by the default ctor - public T Val { - get { - Contract.Assume(IsSet); - return Value; - } - set { - Value = value; - IsSet = true; - } - } - public void UnSet() { - IsSet = false; - } - } - - public class DomRelation { - // doms maps (unique) node numbers to the node numbers of the immediate dominator - // to use it on Nodes, one needs the two way mapping between nodes and their numbers. - private int[] doms; // 0 is unused: means undefined - // here are the two mappings - private Maybe[] postOrderNumberToNode; - private Dictionary nodeToPostOrderNumber; - private int sourceNum; // (number for) root of the graph - private Node source; // root of the graph - private Graph graph; - private Dictionary> immediateDominatorMap; - - [NotDelayed] - internal DomRelation(Graph g, Node source) { - this.graph = g; - // slot 0 not used: nodes are numbered from 1 to n so zero - // can represent undefined. - this.source = source; - //:base(); - this.NewComputeDominators(); - } - public Dictionary> ImmediateDominatorMap { - get { - Contract.Assume(this.immediateDominatorMap != null); - return this.immediateDominatorMap; - } - } - public bool DominatedBy(Node dominee, Node dominator, List path = null) { - Contract.Assume(this.nodeToPostOrderNumber != null); - Contract.Assume(this.doms != null); - int domineeNum = this.nodeToPostOrderNumber[dominee]; - int dominatorNum = this.nodeToPostOrderNumber[dominator]; - if (domineeNum == dominatorNum) - return true; - int currentNodeNum = this.doms[domineeNum]; - while (true) { - if (currentNodeNum == dominatorNum) - return true; - if (currentNodeNum == this.sourceNum) - return false; - if (path != null) - path.Add(postOrderNumberToNode[currentNodeNum].Val); - currentNodeNum = this.doms[currentNodeNum]; - } - } - private Dictionary> domMap = null; - [Pure] - public override string ToString() { - Contract.Assume(this.doms != null); - int[] localDoms = this.doms; - Contract.Assume(this.postOrderNumberToNode != null); - if (domMap == null) { - domMap = new Dictionary>(); - for (int i = 1; i < localDoms.Length; i++) { // 0 slot is not used - int domineeNum = i; - int currentNodeNum = domineeNum; - List dominators = new List(); - while (currentNodeNum != this.sourceNum) { - dominators.Add(this.postOrderNumberToNode[currentNodeNum].Val); - currentNodeNum = this.doms[currentNodeNum]; - } - dominators.Add(this.postOrderNumberToNode[this.sourceNum].Val); - domMap.Add(this.postOrderNumberToNode[i].Val, dominators); - } - } - StringBuilder sb = new StringBuilder(); - sb.Append("{"); - bool first = true; - foreach (KeyValuePair> de in domMap) { - if (!first) - sb.Append(", "); - Contract.Assert(!object.Equals(de.Key, default(Node))); - sb.Append(de.Key.ToString()); - sb.Append("~>"); - sb.Append(ListToString(de.Value)); - first = false; - } - sb.Append("}"); - return sb.ToString(); - } - private void PrintIntArray(int[] xs) { - Console.Write("["); - for (int i = 0; i < xs.Length; i++) { - if (0 < i) - Console.Write(", "); - Console.Write(xs[i]); - } - Console.WriteLine("]"); - } - public void PrintList(IEnumerable xs) { - Console.Write("["); - int i = 0; - foreach (T/*!*/ x in xs) { - Contract.Assert(x != null); - if (0 < i) - Console.Write(", "); - Console.Write(x.ToString()); - i++; - } - Console.WriteLine("]"); - } - public string/*!*/ ListToString(IEnumerable xs) { - Contract.Ensures(Contract.Result() != null); - StringBuilder sb = new StringBuilder(); - sb.Append("["); - bool first = true; - foreach (T/*!*/ x in xs) { - Contract.Assert(x != null); - if (!first) - sb.Append(", "); - sb.Append(x.ToString()); - first = false; - } - sb.Append("]"); - return sb.ToString(); - } - - // Keith D. Cooper, Timothy J. Harvey, Ken Kennedy, "A Simple, Fast Dominance Algorithm ", Software Practice and Experience, 2001. - // http://citeseer.ist.psu.edu/cooper01simple.html - private void NewComputeDominators() { - int n = this.graph.Nodes.Count; - this.postOrderNumberToNode = new Maybe[n + 1]; - this.nodeToPostOrderNumber = new Dictionary(); - //HashSet visited = new HashSet(); - //int currentNumber = 1; - Contract.Assume(this.source != null); - //this.PostOrderVisit(this.source, visited, ref currentNumber); - this.PostOrderVisitIterative(this.source); - this.sourceNum = this.nodeToPostOrderNumber[source]; - // for (int i = 1; i <= n; i++){ Console.WriteLine(postOrderNumberToNode[i]); } - this.doms = new int[n + 1]; // 0 is unused: means undefined - Node start_node = this.source; - this.doms[this.nodeToPostOrderNumber[start_node]] = this.nodeToPostOrderNumber[start_node]; - bool changed = true; - // PrintIntArray(doms); - while (changed) { - changed = false; - // for all nodes, b, in reverse postorder (except start_node) - for (int nodeNum = n - 1; 1 <= nodeNum; nodeNum--) { - Node b = this.postOrderNumberToNode[nodeNum].Val; - IEnumerable predecessors = this.graph.Predecessors(b); - // find a predecessor (i.e., a higher number) for which - // the doms array has been set - int new_idom = 0; - int first_processed_predecessor = 0; - #region new_idom <- number of first (processed) predecessor of b (pick one) - foreach (Node p in predecessors) { - if (this.doms[this.nodeToPostOrderNumber[p]] != 0) { - int x = this.nodeToPostOrderNumber[p]; - new_idom = x; - first_processed_predecessor = x; - break; - } - } - #endregion - #region for all other predecessors, p, of b - foreach (Node p in predecessors) { - if (this.nodeToPostOrderNumber[p] == first_processed_predecessor) { - continue; - } - if (this.doms[this.nodeToPostOrderNumber[p]] != 0) - new_idom = intersect(this.nodeToPostOrderNumber[p], new_idom, this.doms); - } - #endregion - if (this.doms[this.nodeToPostOrderNumber[b]] != new_idom) { - this.doms[this.nodeToPostOrderNumber[b]] = new_idom; - changed = true; - } - } - } - #region Populate the Immediate Dominator Map - int sourceNum = this.nodeToPostOrderNumber[this.source]; - immediateDominatorMap = new Dictionary>(); - for (int i = 1; i <= n; i++) { - Node node = this.postOrderNumberToNode[i].Val; - Node idomNode = this.postOrderNumberToNode[this.doms[i]].Val; - if (i == sourceNum && this.doms[i] == sourceNum) { - continue; - } - if (immediateDominatorMap.ContainsKey(idomNode)) { - immediateDominatorMap[idomNode].Add(node); - } else { - List l = new List(); - l.Add(node); - immediateDominatorMap.Add(idomNode, l); - } - } - #endregion - } - private int intersect(int b1, int b2, int[] doms) { - int finger1 = b1; - int finger2 = b2; - while (finger1 != finger2) { - while (finger1 < finger2) { - finger1 = doms[finger1]; - } - while (finger2 < finger1) { - finger2 = doms[finger2]; - } - } - return finger1; - } - private void PostOrderVisit(Node/*!*/ n, HashSet visited, ref int currentNumber) { - Contract.Requires(n != null); - if (visited.Contains(n)) - return; - visited.Add(n); - foreach (Node/*!*/ child in this.graph.Successors(n)) { - Contract.Assert(child != null); - PostOrderVisit(child, visited, ref currentNumber); - } - Contract.Assume(this.postOrderNumberToNode != null); - Contract.Assume(this.nodeToPostOrderNumber != null); - this.postOrderNumberToNode[currentNumber].Val = n; - this.nodeToPostOrderNumber[n] = currentNumber; - currentNumber++; - return; - } - // Iterative version: mimics the above recursive procedure - private void PostOrderVisitIterative(Node n) - { - Contract.Requires(n != null); - var visited = new HashSet(); - var grey = new HashSet(); - var stack = new Stack(); - - int currentNumber = 1; - - stack.Push(n); - visited.Add(n); - - while (stack.Count != 0) - { - var curr = stack.Pop(); - - if (grey.Contains(curr)) - { - Contract.Assume(this.postOrderNumberToNode != null); - Contract.Assume(this.nodeToPostOrderNumber != null); - this.postOrderNumberToNode[currentNumber].Val = curr; - this.nodeToPostOrderNumber[curr] = currentNumber; - currentNumber++; - } - else - { - grey.Add(curr); - stack.Push(curr); - foreach (Node/*!*/ child in this.graph.Successors(curr)) - { - Contract.Assert(child != null); - if (!visited.Contains(child)) - { - visited.Add(child); - stack.Push(child); - } - } - } - - } - - - } - - public Node LeastCommonAncestor(Node n1, Node n2) - { - int num1 = nodeToPostOrderNumber[n1], num2 = nodeToPostOrderNumber[n2]; - int lca = intersect(num1, num2, this.doms); - return postOrderNumberToNode[lca].Val; - } - } - - public class Graph { - private HashSet> es; - private HashSet ns; - private Node source; - private bool reducible; - private HashSet headers; - private Dictionary> backEdgeNodes; - private Dictionary, HashSet> naturalLoops; - private HashSet splitCandidates; - - private DomRelation dominatorMap = null; - private Dictionary> predCache = new Dictionary>(); - private Dictionary> succCache = new Dictionary>(); - private bool predComputed; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(es == null || Contract.ForAll(es, p => p.Item1 != null && p.Item2 != null)); - Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Item2 != null && p.Item1 != null)); - } - - private class PreHeader { - Node/*!*/ myHeader; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(myHeader != null); - } - - internal PreHeader(Node/*!*/ h) { - Contract.Requires(h != null); - myHeader = h; - } - - [Pure] - public override string/*!*/ ToString() { - Contract.Ensures(Contract.Result() != null); - return "#" + myHeader.ToString(); - } - } - - public Graph(HashSet> edges) { - - Contract.Requires(cce.NonNullElements(edges) && Contract.ForAll(edges, p => p.Item1 != null && p.Item2 != null)); - es = edges; - - // original A# - //ns = Set{ x : in es } + Set{ y : in es }; - - // closest Spec# - //ns = new Set{ Tuple p in edges; p.Item1 } + new Set{ Tuple p in edges; p.Item2 }; - - // - HashSet temp = new HashSet(); - foreach (Tuple p in edges) { - Contract.Assert(p.Item1 != null); - temp.Add(p.Item1); - Contract.Assert(p.Item2 != null); - temp.Add(p.Item2); - } - ns = temp; - } - public Graph() { - es = new HashSet>(); - ns = new HashSet(); - } - - // BUGBUG: Set.ToString() should return a non-null string - [Pure] - public override string/*!*/ ToString() { - return "" + es.ToString(); - } - - public void AddSource(Node/*!*/ x) { - Contract.Requires(x != null); - // BUGBUG: This generates bad code in the compiler - //ns += new Set{x}; - ns.Add(x); - source = x; - } - - public void AddEdge(Node/*!*/ source, Node/*!*/ dest) { - Contract.Requires(source != null); - Contract.Requires(dest != null); - //es += Set{}; - //ns += Set{source, dest}; - es.Add(new Tuple(source, dest)); - ns.Add(source); - ns.Add(dest); - predComputed = false; - } - - public HashSet Nodes { - get { - return ns; - } - } - public IEnumerable> Edges { - get { - Contract.Ensures(cce.NonNullElements(Contract.Result>>()) - && Contract.ForAll(Contract.Result>>(), n => - n.Item1 != null && n.Item2 != null)); - return es; - } - } - - public bool Edge(Node/*!*/ x, Node/*!*/ y) { - Contract.Requires(x != null); - Contract.Requires(y != null); - // original A# - // return in es; - return es.Contains(new Tuple(x, y)); - } - - private void ComputePredSuccCaches() { - if (predComputed) - return; - predComputed = true; - predCache = new Dictionary>(); - succCache = new Dictionary>(); - - foreach (Node n in Nodes) { - predCache[n] = new HashSet(); - succCache[n] = new HashSet(); - } - - foreach (Tuple p in Edges) { - Contract.Assert(p.Item1 != null); - Contract.Assert(p.Item2 != null); - HashSet tmp; - - tmp = predCache[p.Item2]; - tmp.Add(p.Item1); - predCache[p.Item2] = tmp; - - tmp = succCache[p.Item1]; - tmp.Add(p.Item2); - succCache[p.Item1] = tmp; - } - } - - public IEnumerable Predecessors(Node n) { - // original A# - //Set result = Set{ x : x in Nodes, Edge(x,n) }; - - ComputePredSuccCaches(); - return predCache[n]; - } - - public IEnumerable Successors(Node n) { - ComputePredSuccCaches(); - return succCache[n]; - } - - public List SuccessorsAsList(Node n) { - ComputePredSuccCaches(); - List ret = new List(); - foreach (Node s in succCache[n]) - ret.Add(s); - return ret; - } - - public DomRelation /*Map>*/ DominatorMap { - get { - Contract.Assert(source != null); - if (this.dominatorMap == null) { - this.dominatorMap = new DomRelation(this, this.source); - } - return this.dominatorMap; - } - } - - public Dictionary> ImmediateDominatorMap { - get { - Contract.Assert(source != null); - if (this.dominatorMap == null) { - this.dominatorMap = new DomRelation(this, this.source); - } - return this.dominatorMap.ImmediateDominatorMap; - } - } - public List ImmediatelyDominatedBy(Node/*!*/ n) { - Contract.Requires(n != null); - List dominees; - this.ImmediateDominatorMap.TryGetValue(n, out dominees); - return dominees == null ? new List() : dominees; - } - - public IEnumerable TopologicalSort(bool reversed = false) { - bool acyclic; - List sortedList; - this.TarjanTopSort(out acyclic, out sortedList, reversed); - return acyclic ? sortedList : new List(); - } - // From Tarjan 1972 - public void TarjanTopSort(out bool acyclic, out List sortedNodes, bool reversed = false) { - int n = this.Nodes.Count; - if (n == 0) { - acyclic = true; - sortedNodes = new List(); - return; - } - int[] incomingEdges = new int[n]; - // need an arbitrary numbering for the nodes to use as indices into - // the arrays used within this algorithm - Dictionary nodeToNumber = new Dictionary(n); - Maybe[] numberToNode = new Maybe[n]; - int counter = 0; - foreach (Node node in this.Nodes) { - numberToNode[counter].Val = node; - nodeToNumber[node] = counter; - counter++; - } - foreach (Tuple e in this.Edges) { - Contract.Assert(e.Item1 != null); - Contract.Assert(e.Item2 != null); - Node/*!*/ target = e.Item2; - incomingEdges[nodeToNumber[target]]++; - } - List sorted = new List(); - int sortedIndex = 0; - while (sortedIndex < n) { - // find a root (i.e., its index) - int rootIndex = -1; - if (reversed) { - for (int i = n-1; i >= 0; i--) { - if (incomingEdges[i] == 0) { - rootIndex = i; - break; - } - } - } else { - for (int i = 0; i < n; i++) { - if (incomingEdges[i] == 0) { - rootIndex = i; - break; - } - } - } - if (rootIndex == -1) { - acyclic = false; - sortedNodes = new List(); - return; - } - // mark root so it won't be used again - incomingEdges[rootIndex] = -1; - Node root = numberToNode[rootIndex].Val; - sorted.Add(root); - ++sortedIndex; - foreach (Node s in this.Successors(root)) { - incomingEdges[nodeToNumber[s]]--; - } - } - acyclic = true; - sortedNodes = sorted; - return; - } - private IEnumerable OldTopologicalSort() { - Tuple> result = this.TopSort(); - return result.Item1 ? result.Item2 : (IEnumerable)new List(); - } - // From AsmL distribution example - private Tuple> TopSort() - { - List S = new List(); - HashSet V = this.Nodes; - HashSet X = new HashSet(); - foreach (Node/*!*/ n in V) { - Contract.Assert(n != null); - X.Add(n); - } - bool change = true; - while (change) - // invariant: X = V - S - { - change = false; - if (X.Count > 0) { - foreach (Node/*!*/ n in X) { - Contract.Assert(n != null); - // see if n has any incoming edges from any other node in X - bool inDegreeZero = true; - foreach (Node/*!*/ u in X) { - Contract.Assert(u != null); - if (this.Edge(u, n)) { - inDegreeZero = false; - break; // no point looking further - } - } - if (inDegreeZero) { - S.Add(n); - X.Remove(n); - change = true; - break; // might as well go back and start looking through X from the beginning - } - } - // Then we made it all the way through X without finding a source node - if (!change) { - return new Tuple>(false, new List()); - } - } - } - return new Tuple>(true, S); - } - - public static bool Acyclic(Graph g, Node source) { - bool acyclic; - List sortedList; - g.TarjanTopSort(out acyclic, out sortedList); - return acyclic; - } - - // [Dragon, Fig. 10.15, p. 604. Algorithm for constructing the natural loop.] - static HashSet NaturalLoop(Graph g, Tuple backEdge) - { - Contract.Requires(backEdge.Item1 != null && backEdge.Item2 != null); - Node/*!*/ n = backEdge.Item1; - Node/*!*/ d = backEdge.Item2; - Stack stack = new Stack(); - HashSet loop = new HashSet(); - loop.Add(d); - if (!n.Equals(d)) // then n is not in loop - { - loop.Add(n); - stack.Push(n); // push n onto stack - } - while (stack.Count > 0) // not empty - { - Node m = stack.Peek(); - stack.Pop(); // pop stack - foreach (Node/*!*/ p in g.Predecessors(m)) { - Contract.Assert(p != null); - if (!(loop.Contains(p))) { - loop.Add(p); - stack.Push(p); // push p onto stack - } - } - } - return loop; - } - - internal struct ReducibleResult { - internal bool reducible; - internal HashSet headers; - internal Dictionary> backEdgeNodes; - internal Dictionary, HashSet> naturalLoops; - internal HashSet splitCandidates; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Contract.ForAll(naturalLoops.Keys, p => p.Item1 != null && p.Item2 != null)); - } - - internal ReducibleResult(bool b, HashSet headers, Dictionary> backEdgeNodes, Dictionary, HashSet> naturalLoops, HashSet splitCandidates) - { - Contract.Requires(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, Key => Key.Item1 != null && Key.Item2 != null)); - this.reducible = b; - this.headers = headers; - this.backEdgeNodes = backEdgeNodes; - this.naturalLoops = naturalLoops; - this.splitCandidates = splitCandidates; - } - - } - - // [Dragon, p. 606] - static ReducibleResult ComputeReducible(Graph g, Node source) { - // first, compute the dom relation - DomRelation /*Map>*/ D = g.DominatorMap; - return ComputeReducible(g, source, D); - } - - static HashSet FindCycle(Graph g, Node source) { - Stack>> stack = new Stack>>(); - HashSet stackAsSet = new HashSet(); - HashSet visited = new HashSet(); - stack.Push(new Tuple>(source, g.SuccessorsAsList(source))); - stackAsSet.Add(source); - while (stack.Count > 0) { - Tuple> tuple = stack.Peek(); - List children = tuple.Item2; - if (children.Count == 0) { - stack.Pop(); - stackAsSet.Remove(tuple.Item1); - continue; - } - Node n = children[0]; - children.RemoveAt(0); - if (stackAsSet.Contains(n)) { - HashSet ret = new HashSet(); - ret.Add(n); - while (true) { - Node x = stack.Pop().Item1; - if (x.Equals(n)) - return ret; - } - } - if (visited.Contains(n)) - continue; - stack.Push(new Tuple>(n, g.SuccessorsAsList(n))); - visited.Add(n); - stackAsSet.Add(n); - System.Diagnostics.Debug.Assert(stack.Count == stackAsSet.Count); - } - return new HashSet(); - } - - // [Dragon, p. 606] - static ReducibleResult ComputeReducible(Graph g, - Node source, - DomRelation/*!*/ DomRelation) { - Contract.Requires(DomRelation != null); - - //Console.WriteLine("[" + DateTime.Now +"]: begin ComputeReducible"); - IEnumerable> edges = g.Edges; - Contract.Assert(Contract.ForAll(edges, n => n.Item1 != null && n.Item2 != null)); - HashSet> backEdges = new HashSet>(); - HashSet> nonBackEdges = new HashSet>(); - foreach (Tuple e in edges) { - Contract.Assert(e.Item1 != null); - Contract.Assert(e.Item2 != null); - Node x = e.Item1; - Node y = e.Item2; // so there is an edge from x to y - if (DomRelation.DominatedBy(x, y)) { // y dom x: which means y dominates x - backEdges.Add(e); - } else { - nonBackEdges.Add(e); - } - } - Graph withoutBackEdges = new Graph(nonBackEdges); - if (!Acyclic(withoutBackEdges, source)) { - return new ReducibleResult(false, - new HashSet(), - new Dictionary>(), - new Dictionary, HashSet>(), - FindCycle(withoutBackEdges, source)); - } else { - // original A#: - //Set headers = Set{ d : in backEdges }; - HashSet headers = new HashSet(); - foreach (Tuple e in backEdges) { - - Contract.Assert(e.Item1 != null); - Contract.Assert(e.Item2 != null); - headers.Add(e.Item2); - } - // original A#: - //Map> backEdgeNodes = Map{ h -> bs : h in headers, bs = Set{ b : in backEdges, x == h } }; - Dictionary> backEdgeNodes = new Dictionary>(); - foreach (Node/*!*/ h in headers) { - Contract.Assert(h != null); - HashSet bs = new HashSet(); - foreach (Tuple backedge in backEdges) { - Contract.Assert(backedge.Item1 != null); - Contract.Assert(backedge.Item2 != null); - if (backedge.Item2.Equals(h)) { - bs.Add(backedge.Item1); - } - } - backEdgeNodes.Add(h, bs); - } - - // original A#: - //Map,Set> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges }; - Dictionary, HashSet> naturalLoops = new Dictionary, HashSet>(); - foreach (Tuple e in backEdges) { - Contract.Assert(e.Item1 != null && e.Item2 != null); - naturalLoops.Add(e, NaturalLoop(g, e)); - } - - //Console.WriteLine("[" + DateTime.Now +"]: end ComputeReducible"); - return new ReducibleResult(true, headers, backEdgeNodes, naturalLoops, new HashSet()); - } - } - - public bool Reducible { - get { - return reducible; - } - } - public IEnumerable Headers { - get { - return headers; - } - } - public IEnumerable BackEdgeNodes(Node/*!*/ h) { - Contract.Requires(h != null); - // original A#: - //return h in backEdgeNodes ? backEdgeNodes[h] : null; - return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable)new List()); - } - public IEnumerable NaturalLoops(Node/*!*/ header, Node/*!*/ backEdgeNode) { - Contract.Requires(header != null); - Contract.Requires(backEdgeNode != null); - Tuple e = new Tuple(backEdgeNode, header); - return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable)new List(); - } - public HashSet SplitCandidates { - get { - return splitCandidates; - } - } - public void ComputeLoops() { - ReducibleResult r = ComputeReducible(this, this.source); - this.reducible = r.reducible; - this.headers = r.headers; - this.backEdgeNodes = r.backEdgeNodes; - this.naturalLoops = r.naturalLoops; - this.splitCandidates = r.splitCandidates; - return; - } - - public IEnumerable SortHeadersByDominance() - { - Graph dag = new Graph(); - foreach (Node b in headers) - { - dag.AddSource(b); - foreach (Node c in headers) - { - if (b.Equals(c)) continue; - if (DominatorMap.DominatedBy(b, c)) - { - System.Diagnostics.Debug.Assert(!DominatorMap.DominatedBy(c, b)); - dag.AddEdge(b, c); - } - } - } - return dag.TopologicalSort(); - } - - public string ToDot(Func NodeLabel = null, Func NodeStyle = null) { - NodeLabel = NodeLabel ?? (n => n.ToString()); - NodeStyle = NodeStyle ?? (n => "[shape=box]"); - var s = new StringBuilder(); - s.AppendLine("digraph G {"); - foreach (var n in Nodes) - s.AppendLine(" \"" + NodeLabel(n) + "\" " + NodeStyle(n) + ";"); - foreach (var e in Edges) - s.AppendLine(" \"" + NodeLabel(e.Item1) + "\" -> \"" + NodeLabel(e.Item2) + "\";"); - s.AppendLine("}"); - return s.ToString(); - } - - public ICollection ComputeReachable() { - ICollection result = new HashSet(); - Stack stack = new Stack(); - stack.Push(source); - while(!(stack.Count() == 0)) { - Node n = stack.Pop(); - result.Add(n); - foreach(var m in Successors(n)) { - if(!result.Contains(m)) { - stack.Push(m); - } - } - } - return result; - } - - } // end: class Graph - - public static class GraphAlgorithms - { - - - public static Graph Dual(this Graph g, Node dummySource) - { - var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList(); - Node source; - if (exits.Count == 0) - exits.Add(dummySource); - var dual = new Graph(new HashSet>(g.Edges.Select(e => new Tuple(e.Item2, e.Item1)))); - if (exits.Count == 1) - { - dual.AddSource(exits[0]); - source = exits[0]; - } - else - { - dual.AddSource(dummySource); - source = dummySource; - foreach (var exit in exits) - dual.AddEdge(dummySource, exit); - } - - #region Dual graph may not be connected, so add an edge from the dual graph's soure node to any unreachable node - foreach (var n in dual.Nodes.Where(Item => !dual.ComputeReachable().Contains(Item))) - { - dual.AddEdge(source, n); - } - #endregion - - return dual; - } - - public static List> LoopyTopSort(this Graph g) - { - Contract.Assert(g.Reducible); - - int n = g.Nodes.Count; - var nodeToNumber = new Dictionary(n); - var numberToNode = new Node[n]; - var allNodes = new List(); - int counter = 0; - foreach (Node node in g.Nodes) - { - numberToNode[counter] = node; - nodeToNumber[node] = counter; - allNodes.Add(counter); - counter++; - } - - var loops = new List[n]; - foreach (var h in g.Headers) - { - var loopNodes = new HashSet(); - foreach (var b in g.BackEdgeNodes(h)) - loopNodes.UnionWith(g.NaturalLoops(h, b)); - loops[nodeToNumber[h]] = - new List(loopNodes.Select(node => nodeToNumber[node])); - } - - var successors = new List[n]; - var predecessors = new List[n]; - int[] incomingEdges = new int[n]; - - for (int i = 0; i < n; i++) - predecessors[i] = new List(); - - foreach (var e in g.Edges) - { - Contract.Assert(e.Item1 != null); - Contract.Assert(e.Item2 != null); - int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2]; - if (loops[target] == null || !loops[target].Contains(source)) - { - if (successors[source] == null) - successors[source] = new List(); - successors[source].Add(target); - incomingEdges[target]++; - } - predecessors[target].Add(source); - } - - var sortedNodes = new List>(); - var sortedNodesInternal = new List(); - - var regionStack = new Stack>>(); - regionStack.Push(new Tuple>(default(Node), allNodes)); - - while (regionStack.Count != 0) - { - var rootIndexes = new List(); - foreach (var i in regionStack.Peek().Item2) - { - if (incomingEdges[i] == 0) - rootIndexes.Add(i); - } - if (rootIndexes.Count() == 0) - { - var region = regionStack.Pop(); - if (regionStack.Count != 0) { - sortedNodes.Add(new Tuple(region.Item1, true)); - sortedNodesInternal.Add(nodeToNumber[region.Item1]); - } - continue; - } - int rootIndex = rootIndexes[0]; - int maxPredIndex = -1; - foreach (var i in rootIndexes) { - foreach (var p in predecessors[i]) { - int predIndex = - sortedNodesInternal.FindLastIndex(x => x == p); - if (predIndex > maxPredIndex) { - rootIndex = i; - maxPredIndex = predIndex; - } - } - } - incomingEdges[rootIndex] = -1; - sortedNodes.Add(new Tuple(numberToNode[rootIndex], false)); - sortedNodesInternal.Add(rootIndex); - if (successors[rootIndex] != null) - foreach (int s in successors[rootIndex]) - incomingEdges[s]--; - if (loops[rootIndex] != null) - regionStack.Push(new Tuple>(numberToNode[rootIndex], - loops[rootIndex])); - } - - return sortedNodes; - } - - // Algorithm from Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren, - // "The Program Dependence Graph and Its Use in Optimization" - public static Dictionary> ControlDependence(this Graph g) where Node : class, new() - { - Graph dual = g.Dual(new Node()); - DomRelation pdom = dual.DominatorMap; - - var result = new Dictionary>(); - - var S = g.Edges.Where(e => !pdom.DominatedBy(e.Item1, e.Item2)); - foreach (var edge in S) - { - var L = pdom.LeastCommonAncestor(edge.Item1, edge.Item2); - var deps = new List(); - if (L == edge.Item1) - { - pdom.DominatedBy(edge.Item2, edge.Item1, deps); - deps.Add(edge.Item2); - deps.Add(edge.Item1); - } - else - { - pdom.DominatedBy(edge.Item2, L, deps); - deps.Add(edge.Item2); - } - if (result.ContainsKey(edge.Item1)) - { - result[edge.Item1].UnionWith(deps); - } - else - { - result[edge.Item1] = new HashSet(deps); - } - } - - return result; - } - - public static void TransitiveClosure(this Dictionary> graph) where Node : class { - bool changed; - do { - changed = false; - foreach (var entry in graph) { - var newSuccessors = new HashSet(entry.Value); - foreach (var successor in entry.Value) { - if (graph.ContainsKey(successor)) - newSuccessors.UnionWith(graph[successor]); - } - if (newSuccessors.Count != entry.Value.Count) { - entry.Value.UnionWith(newSuccessors); - changed = true; - } - } - } while (changed); - } - - } - - public delegate System.Collections.IEnumerable/**//*!*/ Adjacency(T/*!*/ node); - - - // An SCC is a set of nodes - public sealed class SCC : ICollection - { - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(nodesMap != null); - } - - private IDictionary/*!*/ nodesMap = new Dictionary(); - private ICollection/*!*/ nodes - { - get - { - return cce.NonNull(nodesMap.Keys); - } - } - - [Pure] - [GlobalAccess(false)] - [Escapes(true, false)] - System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator() - { - Contract.Ensures(Contract.Result() != null); - - return ((System.Collections.IEnumerable)nodes).GetEnumerator(); - } - - [Pure] - [GlobalAccess(false)] - [Escapes(true, false)] - IEnumerator/*!*/ IEnumerable.GetEnumerator() - { - Contract.Ensures(Contract.Result>() != null); - - return ((IEnumerable)nodes).GetEnumerator(); - } - - public int Count - { - get - { - return nodes.Count; - } - } - public bool IsReadOnly - { - get - { - return nodesMap.IsReadOnly; - } - } - public void Add(Node item) - { - nodesMap.Add(item, null); - } - public void Clear() - { - nodesMap.Clear(); - } - [Pure] - public bool Contains(Node item) - { - return nodesMap.ContainsKey(item); - } - public void CopyTo(Node[] array, int arrayIndex) - { - //Contract.Requires(array != null); - nodes.CopyTo(array, arrayIndex); - } - public bool Remove(Node item) - { - return nodesMap.Remove(item); - } - } - - public sealed class StronglyConnectedComponents : IEnumerable/*!*/> where Node : class - { - private readonly IDictionary/*!*/ graph; - [ContractInvariantMethod] - void graphInvariantMethod() - { - Contract.Invariant(Contract.ForAll(graph, entry => entry.Key != null)); - Contract.Invariant(preds != null); - Contract.Invariant(succs != null); - } - private readonly Adjacency/*!*/ preds; - private readonly Adjacency/*!*/ succs; - - private bool computed = false; - public bool Computed - { - get - { - return computed; - } - } - - [NotDelayed] - public StronglyConnectedComponents(System.Collections.IEnumerable/**/ graph, Adjacency preds, Adjacency succs) - : base() - { - Contract.Requires(succs != null); - Contract.Requires(preds != null); - Contract.Requires(graph != null); - Contract.Ensures(!Computed); - IDictionary/*!*/ dict = new Dictionary(); - foreach (Node/*!*/ n in graph) - { - Contract.Assert(n != null); - dict.Add(n, null); - } - - this.graph = dict; - this.preds = preds; - this.succs = succs; - } - - [Pure] - [GlobalAccess(false)] - [Escapes(true, false)] - System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator() - { - Contract.Ensures(Contract.Result() != null); - - return ((System.Collections.IEnumerable)sccs).GetEnumerator(); - } - - [Pure] - [GlobalAccess(false)] - [Escapes(true, false)] - IEnumerator/*!*/>/*!*/ IEnumerable/*!*/>.GetEnumerator() - { - Contract.Ensures(Contract.Result>>() != null); - - Contract.Assume(Computed); - Contract.Assert(cce.NonNullElements((IEnumerable/*!*/>)sccs));//REVIEW - return ((IEnumerable/*!*/>)sccs).GetEnumerator(); - } - - private readonly IList/*!*/>/*!*/ sccs = new List/*!*/>(); - [ContractInvariantMethod] - void sccsInvariant() - { - Contract.Invariant(cce.NonNullElements(sccs)); - } - - - public void Compute() - { - Contract.Requires(!Computed); - Contract.Ensures(Computed); - // Compute post times on graph with edges reversed - this.dfsNext = this.preds; - foreach (Node/*!*/ n in cce.NonNull(graph.Keys)) - { - Contract.Assert(n != null); - if (!seen.ContainsKey(n)) - { - OrderNodes(n); - } - } - - // Clear seen - seen.Clear(); - - // Compute SCCs - this.dfsNext = this.succs; - while (postOrder.Count > 0) - { - Node/*!*/ n = postOrder.Pop(); - Contract.Assert(n != null); - - if (!seen.ContainsKey(n)) - { - SCC/*!*/ curr = new SCC(); - FindSCCs(n, curr); - sccs.Add(curr); - } - } - - // Clear seen - seen.Clear(); - - this.computed = true; - } - - private Adjacency/*?*/ dfsNext = null; - - private readonly IDictionary/*!*/ seen = new Dictionary(); - private readonly Stack/*!*/ postOrder = new Stack(); - [ContractInvariantMethod] - void ObjectInvariant() - { - Contract.Invariant(seen != null); - Contract.Invariant(cce.NonNullElements(postOrder)); - } - - - // DFS to order nodes by post times - private void OrderNodes(Node node) - { - Contract.Requires(node != null); - seen.Add(node, null); - - Contract.Assert(dfsNext != null); - System.Collections.IEnumerable/*!*/ nexts = dfsNext(node); - Contract.Assert(nexts != null); - foreach (Node/*!*/ n in nexts) - { - Contract.Assert(n != null); - if (graph.ContainsKey(n) && !seen.ContainsKey(n)) - { - OrderNodes(n); - } - } - - postOrder.Push(node); - } - - // DFS to compute SCCs - private void FindSCCs(Node node, SCC currSCC) - { - Contract.Requires(currSCC != null); - Contract.Requires(node != null); - //modifies currSCC.*; - seen.Add(node, null); - currSCC.Add(node); - - Contract.Assert(dfsNext != null); - System.Collections.IEnumerable/*!*/ nexts = dfsNext(node); - Contract.Assert(nexts != null); - foreach (Node/*!*/ n in nexts) - { - Contract.Assert(n != null); - if (graph.ContainsKey(n) && !seen.ContainsKey(n)) - { - FindSCCs(n, currSCC); - } - } - } - - [Pure] - public override string ToString() - { - Contract.Ensures(Contract.Result() != null); - string outStr = ""; - int i = 0; - - foreach (ICollection component in this) - { - string/*!*/ tmp = System.String.Format("\nComponent #{0} = ", i++); - Contract.Assert(tmp != null); - outStr += tmp; - - bool firstInRow = true; - - foreach (Node b in component) - { - string/*!*/ tmpComponent = System.String.Format("{0}{1}", firstInRow ? "" : ", ", b); - Contract.Assert(tmpComponent != null); - outStr += tmpComponent; - firstInRow = false; - } - } - return outStr; - } - - } - - public class GraphProgram { - static void TestGraph(T/*!*/ source, params Tuple[] edges) { - Contract.Requires(source != null); - Contract.Requires(Contract.ForAll(edges, pair => pair.Item1 != null && pair.Item2 != null)); - HashSet> es = new HashSet>(); - foreach (Tuple e in edges) { - Contract.Assert(e.Item1 != null && e.Item2 != null); - es.Add(e); - } - Graph g = new Graph(es); - g.AddSource(source); - Console.WriteLine("G = " + g); - g.ComputeLoops(); - Console.WriteLine("G's Dominator Map = " + g.DominatorMap); - Console.WriteLine("G's Immediate Dominator Map = " + Util.MapToString(g.ImmediateDominatorMap)); - Console.WriteLine("G is reducible: " + (g.Reducible ? "yes" : "no")); - } - - static void Main(string[] args) - //requires forall{string s in args; s != null}; - { - Console.WriteLine("Spec# says hello!"); - // This generates bad IL -- need to fix a bug in the compiler - //Graph g = new Graph(new Set>{ new Tuple(1,2), new Tuple(1,3), new Tuple(2,3) }); - - Console.WriteLine(""); - TestGraph('a', - new Tuple('a', 'b'), - new Tuple('a', 'c'), - new Tuple('b', 'c') - ); - - Console.WriteLine(""); - TestGraph('a', - new Tuple('a', 'b'), - new Tuple('a', 'c'), - new Tuple('b', 'd'), - new Tuple('c', 'e'), - new Tuple('c', 'f'), - new Tuple('d', 'e'), - new Tuple('e', 'd'), - new Tuple('e', 'f'), - new Tuple('f', 'e') - ); - - Console.WriteLine(""); - TestGraph('a', - new Tuple('a', 'b'), - new Tuple('a', 'c'), - new Tuple('b', 'c'), - new Tuple('c', 'b') - ); - - Console.WriteLine(""); - TestGraph(1, - new Tuple(1, 2), - new Tuple(1, 3), - new Tuple(2, 3) - ); - - Console.WriteLine(""); - TestGraph(1, - new Tuple(1, 2), - new Tuple(1, 3), - new Tuple(2, 3), - new Tuple(3, 2) - ); - - Console.WriteLine(""); - TestGraph(2, - new Tuple(2, 3), - new Tuple(2, 4), - new Tuple(3, 2) - ); - - Console.WriteLine(""); - TestGraph('a', - new Tuple('a', 'b'), - new Tuple('a', 'c'), - new Tuple('b', 'c'), - new Tuple('b', 'b') - ); - - - } - } - -} +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Linq; +using System.Collections.Generic; +using System.Text; // for StringBuilder +using System.Diagnostics.Contracts; +namespace Microsoft.Boogie.GraphUtil { + + internal static class Util { + private static string/*!*/ ListToString(IEnumerable xs) { + Contract.Ensures(Contract.Result() != null); + StringBuilder sb = new StringBuilder(); + sb.Append("["); + bool first = true; + foreach (T/*!*/ x in xs) { + Contract.Assert(x != null); + if (!first) + sb.Append(", "); + sb.Append(x.ToString()); + first = false; + } + sb.Append("]"); + return sb.ToString(); + } + public static string/*!*/ MapToString(Dictionary> d) { + Contract.Ensures(Contract.Result() != null); + StringBuilder sb = new StringBuilder(); + sb.Append("{"); + bool first = true; + foreach (KeyValuePair> de in d) { + if (!first) + sb.Append(", "); + Contract.Assert(!object.Equals(de.Key,default(Node))); + sb.Append(de.Key.ToString()); + sb.Append("~>"); + sb.Append(ListToString(de.Value)); + first = false; + } + sb.Append("}"); + return sb.ToString(); + } + } + + // own struct to represent possibly undefined values, because Mono does + // not like arrays with element type T! or T? + public struct Maybe { + private T Value; + public bool IsSet; // initialised with false by the default ctor + public T Val { + get { + Contract.Assume(IsSet); + return Value; + } + set { + Value = value; + IsSet = true; + } + } + public void UnSet() { + IsSet = false; + } + } + + public class DomRelation { + // doms maps (unique) node numbers to the node numbers of the immediate dominator + // to use it on Nodes, one needs the two way mapping between nodes and their numbers. + private int[] doms; // 0 is unused: means undefined + // here are the two mappings + private Maybe[] postOrderNumberToNode; + private Dictionary nodeToPostOrderNumber; + private int sourceNum; // (number for) root of the graph + private Node source; // root of the graph + private Graph graph; + private Dictionary> immediateDominatorMap; + + [NotDelayed] + internal DomRelation(Graph g, Node source) { + this.graph = g; + // slot 0 not used: nodes are numbered from 1 to n so zero + // can represent undefined. + this.source = source; + //:base(); + this.NewComputeDominators(); + } + public Dictionary> ImmediateDominatorMap { + get { + Contract.Assume(this.immediateDominatorMap != null); + return this.immediateDominatorMap; + } + } + public bool DominatedBy(Node dominee, Node dominator, List path = null) { + Contract.Assume(this.nodeToPostOrderNumber != null); + Contract.Assume(this.doms != null); + int domineeNum = this.nodeToPostOrderNumber[dominee]; + int dominatorNum = this.nodeToPostOrderNumber[dominator]; + if (domineeNum == dominatorNum) + return true; + int currentNodeNum = this.doms[domineeNum]; + while (true) { + if (currentNodeNum == dominatorNum) + return true; + if (currentNodeNum == this.sourceNum) + return false; + if (path != null) + path.Add(postOrderNumberToNode[currentNodeNum].Val); + currentNodeNum = this.doms[currentNodeNum]; + } + } + private Dictionary> domMap = null; + [Pure] + public override string ToString() { + Contract.Assume(this.doms != null); + int[] localDoms = this.doms; + Contract.Assume(this.postOrderNumberToNode != null); + if (domMap == null) { + domMap = new Dictionary>(); + for (int i = 1; i < localDoms.Length; i++) { // 0 slot is not used + int domineeNum = i; + int currentNodeNum = domineeNum; + List dominators = new List(); + while (currentNodeNum != this.sourceNum) { + dominators.Add(this.postOrderNumberToNode[currentNodeNum].Val); + currentNodeNum = this.doms[currentNodeNum]; + } + dominators.Add(this.postOrderNumberToNode[this.sourceNum].Val); + domMap.Add(this.postOrderNumberToNode[i].Val, dominators); + } + } + StringBuilder sb = new StringBuilder(); + sb.Append("{"); + bool first = true; + foreach (KeyValuePair> de in domMap) { + if (!first) + sb.Append(", "); + Contract.Assert(!object.Equals(de.Key, default(Node))); + sb.Append(de.Key.ToString()); + sb.Append("~>"); + sb.Append(ListToString(de.Value)); + first = false; + } + sb.Append("}"); + return sb.ToString(); + } + private void PrintIntArray(int[] xs) { + Console.Write("["); + for (int i = 0; i < xs.Length; i++) { + if (0 < i) + Console.Write(", "); + Console.Write(xs[i]); + } + Console.WriteLine("]"); + } + public void PrintList(IEnumerable xs) { + Console.Write("["); + int i = 0; + foreach (T/*!*/ x in xs) { + Contract.Assert(x != null); + if (0 < i) + Console.Write(", "); + Console.Write(x.ToString()); + i++; + } + Console.WriteLine("]"); + } + public string/*!*/ ListToString(IEnumerable xs) { + Contract.Ensures(Contract.Result() != null); + StringBuilder sb = new StringBuilder(); + sb.Append("["); + bool first = true; + foreach (T/*!*/ x in xs) { + Contract.Assert(x != null); + if (!first) + sb.Append(", "); + sb.Append(x.ToString()); + first = false; + } + sb.Append("]"); + return sb.ToString(); + } + + // Keith D. Cooper, Timothy J. Harvey, Ken Kennedy, "A Simple, Fast Dominance Algorithm ", Software Practice and Experience, 2001. + // http://citeseer.ist.psu.edu/cooper01simple.html + private void NewComputeDominators() { + int n = this.graph.Nodes.Count; + this.postOrderNumberToNode = new Maybe[n + 1]; + this.nodeToPostOrderNumber = new Dictionary(); + //HashSet visited = new HashSet(); + //int currentNumber = 1; + Contract.Assume(this.source != null); + //this.PostOrderVisit(this.source, visited, ref currentNumber); + this.PostOrderVisitIterative(this.source); + this.sourceNum = this.nodeToPostOrderNumber[source]; + // for (int i = 1; i <= n; i++){ Console.WriteLine(postOrderNumberToNode[i]); } + this.doms = new int[n + 1]; // 0 is unused: means undefined + Node start_node = this.source; + this.doms[this.nodeToPostOrderNumber[start_node]] = this.nodeToPostOrderNumber[start_node]; + bool changed = true; + // PrintIntArray(doms); + while (changed) { + changed = false; + // for all nodes, b, in reverse postorder (except start_node) + for (int nodeNum = n - 1; 1 <= nodeNum; nodeNum--) { + Node b = this.postOrderNumberToNode[nodeNum].Val; + IEnumerable predecessors = this.graph.Predecessors(b); + // find a predecessor (i.e., a higher number) for which + // the doms array has been set + int new_idom = 0; + int first_processed_predecessor = 0; + #region new_idom <- number of first (processed) predecessor of b (pick one) + foreach (Node p in predecessors) { + if (this.doms[this.nodeToPostOrderNumber[p]] != 0) { + int x = this.nodeToPostOrderNumber[p]; + new_idom = x; + first_processed_predecessor = x; + break; + } + } + #endregion + #region for all other predecessors, p, of b + foreach (Node p in predecessors) { + if (this.nodeToPostOrderNumber[p] == first_processed_predecessor) { + continue; + } + if (this.doms[this.nodeToPostOrderNumber[p]] != 0) + new_idom = intersect(this.nodeToPostOrderNumber[p], new_idom, this.doms); + } + #endregion + if (this.doms[this.nodeToPostOrderNumber[b]] != new_idom) { + this.doms[this.nodeToPostOrderNumber[b]] = new_idom; + changed = true; + } + } + } + #region Populate the Immediate Dominator Map + int sourceNum = this.nodeToPostOrderNumber[this.source]; + immediateDominatorMap = new Dictionary>(); + for (int i = 1; i <= n; i++) { + Node node = this.postOrderNumberToNode[i].Val; + Node idomNode = this.postOrderNumberToNode[this.doms[i]].Val; + if (i == sourceNum && this.doms[i] == sourceNum) { + continue; + } + if (immediateDominatorMap.ContainsKey(idomNode)) { + immediateDominatorMap[idomNode].Add(node); + } else { + List l = new List(); + l.Add(node); + immediateDominatorMap.Add(idomNode, l); + } + } + #endregion + } + private int intersect(int b1, int b2, int[] doms) { + int finger1 = b1; + int finger2 = b2; + while (finger1 != finger2) { + while (finger1 < finger2) { + finger1 = doms[finger1]; + } + while (finger2 < finger1) { + finger2 = doms[finger2]; + } + } + return finger1; + } + private void PostOrderVisit(Node/*!*/ n, HashSet visited, ref int currentNumber) { + Contract.Requires(n != null); + if (visited.Contains(n)) + return; + visited.Add(n); + foreach (Node/*!*/ child in this.graph.Successors(n)) { + Contract.Assert(child != null); + PostOrderVisit(child, visited, ref currentNumber); + } + Contract.Assume(this.postOrderNumberToNode != null); + Contract.Assume(this.nodeToPostOrderNumber != null); + this.postOrderNumberToNode[currentNumber].Val = n; + this.nodeToPostOrderNumber[n] = currentNumber; + currentNumber++; + return; + } + // Iterative version: mimics the above recursive procedure + private void PostOrderVisitIterative(Node n) + { + Contract.Requires(n != null); + var visited = new HashSet(); + var grey = new HashSet(); + var stack = new Stack(); + + int currentNumber = 1; + + stack.Push(n); + visited.Add(n); + + while (stack.Count != 0) + { + var curr = stack.Pop(); + + if (grey.Contains(curr)) + { + Contract.Assume(this.postOrderNumberToNode != null); + Contract.Assume(this.nodeToPostOrderNumber != null); + this.postOrderNumberToNode[currentNumber].Val = curr; + this.nodeToPostOrderNumber[curr] = currentNumber; + currentNumber++; + } + else + { + grey.Add(curr); + stack.Push(curr); + foreach (Node/*!*/ child in this.graph.Successors(curr)) + { + Contract.Assert(child != null); + if (!visited.Contains(child)) + { + visited.Add(child); + stack.Push(child); + } + } + } + + } + + + } + + public Node LeastCommonAncestor(Node n1, Node n2) + { + int num1 = nodeToPostOrderNumber[n1], num2 = nodeToPostOrderNumber[n2]; + int lca = intersect(num1, num2, this.doms); + return postOrderNumberToNode[lca].Val; + } + } + + public class Graph { + private HashSet> es; + private HashSet ns; + private Node source; + private bool reducible; + private HashSet headers; + private Dictionary> backEdgeNodes; + private Dictionary, HashSet> naturalLoops; + private HashSet splitCandidates; + + private DomRelation dominatorMap = null; + private Dictionary> predCache = new Dictionary>(); + private Dictionary> succCache = new Dictionary>(); + private bool predComputed; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(es == null || Contract.ForAll(es, p => p.Item1 != null && p.Item2 != null)); + Contract.Invariant(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, p => p.Item2 != null && p.Item1 != null)); + } + + private class PreHeader { + Node/*!*/ myHeader; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(myHeader != null); + } + + internal PreHeader(Node/*!*/ h) { + Contract.Requires(h != null); + myHeader = h; + } + + [Pure] + public override string/*!*/ ToString() { + Contract.Ensures(Contract.Result() != null); + return "#" + myHeader.ToString(); + } + } + + public Graph(HashSet> edges) { + + Contract.Requires(cce.NonNullElements(edges) && Contract.ForAll(edges, p => p.Item1 != null && p.Item2 != null)); + es = edges; + + // original A# + //ns = Set{ x : in es } + Set{ y : in es }; + + // closest Spec# + //ns = new Set{ Tuple p in edges; p.Item1 } + new Set{ Tuple p in edges; p.Item2 }; + + // + HashSet temp = new HashSet(); + foreach (Tuple p in edges) { + Contract.Assert(p.Item1 != null); + temp.Add(p.Item1); + Contract.Assert(p.Item2 != null); + temp.Add(p.Item2); + } + ns = temp; + } + public Graph() { + es = new HashSet>(); + ns = new HashSet(); + } + + // BUGBUG: Set.ToString() should return a non-null string + [Pure] + public override string/*!*/ ToString() { + return "" + es.ToString(); + } + + public void AddSource(Node/*!*/ x) { + Contract.Requires(x != null); + // BUGBUG: This generates bad code in the compiler + //ns += new Set{x}; + ns.Add(x); + source = x; + } + + public void AddEdge(Node/*!*/ source, Node/*!*/ dest) { + Contract.Requires(source != null); + Contract.Requires(dest != null); + //es += Set{}; + //ns += Set{source, dest}; + es.Add(new Tuple(source, dest)); + ns.Add(source); + ns.Add(dest); + predComputed = false; + } + + public HashSet Nodes { + get { + return ns; + } + } + public IEnumerable> Edges { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>>()) + && Contract.ForAll(Contract.Result>>(), n => + n.Item1 != null && n.Item2 != null)); + return es; + } + } + + public bool Edge(Node/*!*/ x, Node/*!*/ y) { + Contract.Requires(x != null); + Contract.Requires(y != null); + // original A# + // return in es; + return es.Contains(new Tuple(x, y)); + } + + private void ComputePredSuccCaches() { + if (predComputed) + return; + predComputed = true; + predCache = new Dictionary>(); + succCache = new Dictionary>(); + + foreach (Node n in Nodes) { + predCache[n] = new HashSet(); + succCache[n] = new HashSet(); + } + + foreach (Tuple p in Edges) { + Contract.Assert(p.Item1 != null); + Contract.Assert(p.Item2 != null); + HashSet tmp; + + tmp = predCache[p.Item2]; + tmp.Add(p.Item1); + predCache[p.Item2] = tmp; + + tmp = succCache[p.Item1]; + tmp.Add(p.Item2); + succCache[p.Item1] = tmp; + } + } + + public IEnumerable Predecessors(Node n) { + // original A# + //Set result = Set{ x : x in Nodes, Edge(x,n) }; + + ComputePredSuccCaches(); + return predCache[n]; + } + + public IEnumerable Successors(Node n) { + ComputePredSuccCaches(); + return succCache[n]; + } + + public List SuccessorsAsList(Node n) { + ComputePredSuccCaches(); + List ret = new List(); + foreach (Node s in succCache[n]) + ret.Add(s); + return ret; + } + + public DomRelation /*Map>*/ DominatorMap { + get { + Contract.Assert(source != null); + if (this.dominatorMap == null) { + this.dominatorMap = new DomRelation(this, this.source); + } + return this.dominatorMap; + } + } + + public Dictionary> ImmediateDominatorMap { + get { + Contract.Assert(source != null); + if (this.dominatorMap == null) { + this.dominatorMap = new DomRelation(this, this.source); + } + return this.dominatorMap.ImmediateDominatorMap; + } + } + public List ImmediatelyDominatedBy(Node/*!*/ n) { + Contract.Requires(n != null); + List dominees; + this.ImmediateDominatorMap.TryGetValue(n, out dominees); + return dominees == null ? new List() : dominees; + } + + public IEnumerable TopologicalSort(bool reversed = false) { + bool acyclic; + List sortedList; + this.TarjanTopSort(out acyclic, out sortedList, reversed); + return acyclic ? sortedList : new List(); + } + // From Tarjan 1972 + public void TarjanTopSort(out bool acyclic, out List sortedNodes, bool reversed = false) { + int n = this.Nodes.Count; + if (n == 0) { + acyclic = true; + sortedNodes = new List(); + return; + } + int[] incomingEdges = new int[n]; + // need an arbitrary numbering for the nodes to use as indices into + // the arrays used within this algorithm + Dictionary nodeToNumber = new Dictionary(n); + Maybe[] numberToNode = new Maybe[n]; + int counter = 0; + foreach (Node node in this.Nodes) { + numberToNode[counter].Val = node; + nodeToNumber[node] = counter; + counter++; + } + foreach (Tuple e in this.Edges) { + Contract.Assert(e.Item1 != null); + Contract.Assert(e.Item2 != null); + Node/*!*/ target = e.Item2; + incomingEdges[nodeToNumber[target]]++; + } + List sorted = new List(); + int sortedIndex = 0; + while (sortedIndex < n) { + // find a root (i.e., its index) + int rootIndex = -1; + if (reversed) { + for (int i = n-1; i >= 0; i--) { + if (incomingEdges[i] == 0) { + rootIndex = i; + break; + } + } + } else { + for (int i = 0; i < n; i++) { + if (incomingEdges[i] == 0) { + rootIndex = i; + break; + } + } + } + if (rootIndex == -1) { + acyclic = false; + sortedNodes = new List(); + return; + } + // mark root so it won't be used again + incomingEdges[rootIndex] = -1; + Node root = numberToNode[rootIndex].Val; + sorted.Add(root); + ++sortedIndex; + foreach (Node s in this.Successors(root)) { + incomingEdges[nodeToNumber[s]]--; + } + } + acyclic = true; + sortedNodes = sorted; + return; + } + private IEnumerable OldTopologicalSort() { + Tuple> result = this.TopSort(); + return result.Item1 ? result.Item2 : (IEnumerable)new List(); + } + // From AsmL distribution example + private Tuple> TopSort() + { + List S = new List(); + HashSet V = this.Nodes; + HashSet X = new HashSet(); + foreach (Node/*!*/ n in V) { + Contract.Assert(n != null); + X.Add(n); + } + bool change = true; + while (change) + // invariant: X = V - S + { + change = false; + if (X.Count > 0) { + foreach (Node/*!*/ n in X) { + Contract.Assert(n != null); + // see if n has any incoming edges from any other node in X + bool inDegreeZero = true; + foreach (Node/*!*/ u in X) { + Contract.Assert(u != null); + if (this.Edge(u, n)) { + inDegreeZero = false; + break; // no point looking further + } + } + if (inDegreeZero) { + S.Add(n); + X.Remove(n); + change = true; + break; // might as well go back and start looking through X from the beginning + } + } + // Then we made it all the way through X without finding a source node + if (!change) { + return new Tuple>(false, new List()); + } + } + } + return new Tuple>(true, S); + } + + public static bool Acyclic(Graph g, Node source) { + bool acyclic; + List sortedList; + g.TarjanTopSort(out acyclic, out sortedList); + return acyclic; + } + + // [Dragon, Fig. 10.15, p. 604. Algorithm for constructing the natural loop.] + static HashSet NaturalLoop(Graph g, Tuple backEdge) + { + Contract.Requires(backEdge.Item1 != null && backEdge.Item2 != null); + Node/*!*/ n = backEdge.Item1; + Node/*!*/ d = backEdge.Item2; + Stack stack = new Stack(); + HashSet loop = new HashSet(); + loop.Add(d); + if (!n.Equals(d)) // then n is not in loop + { + loop.Add(n); + stack.Push(n); // push n onto stack + } + while (stack.Count > 0) // not empty + { + Node m = stack.Peek(); + stack.Pop(); // pop stack + foreach (Node/*!*/ p in g.Predecessors(m)) { + Contract.Assert(p != null); + if (!(loop.Contains(p))) { + loop.Add(p); + stack.Push(p); // push p onto stack + } + } + } + return loop; + } + + internal struct ReducibleResult { + internal bool reducible; + internal HashSet headers; + internal Dictionary> backEdgeNodes; + internal Dictionary, HashSet> naturalLoops; + internal HashSet splitCandidates; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Contract.ForAll(naturalLoops.Keys, p => p.Item1 != null && p.Item2 != null)); + } + + internal ReducibleResult(bool b, HashSet headers, Dictionary> backEdgeNodes, Dictionary, HashSet> naturalLoops, HashSet splitCandidates) + { + Contract.Requires(naturalLoops == null || Contract.ForAll(naturalLoops.Keys, Key => Key.Item1 != null && Key.Item2 != null)); + this.reducible = b; + this.headers = headers; + this.backEdgeNodes = backEdgeNodes; + this.naturalLoops = naturalLoops; + this.splitCandidates = splitCandidates; + } + + } + + // [Dragon, p. 606] + static ReducibleResult ComputeReducible(Graph g, Node source) { + // first, compute the dom relation + DomRelation /*Map>*/ D = g.DominatorMap; + return ComputeReducible(g, source, D); + } + + static HashSet FindCycle(Graph g, Node source) { + Stack>> stack = new Stack>>(); + HashSet stackAsSet = new HashSet(); + HashSet visited = new HashSet(); + stack.Push(new Tuple>(source, g.SuccessorsAsList(source))); + stackAsSet.Add(source); + while (stack.Count > 0) { + Tuple> tuple = stack.Peek(); + List children = tuple.Item2; + if (children.Count == 0) { + stack.Pop(); + stackAsSet.Remove(tuple.Item1); + continue; + } + Node n = children[0]; + children.RemoveAt(0); + if (stackAsSet.Contains(n)) { + HashSet ret = new HashSet(); + ret.Add(n); + while (true) { + Node x = stack.Pop().Item1; + if (x.Equals(n)) + return ret; + } + } + if (visited.Contains(n)) + continue; + stack.Push(new Tuple>(n, g.SuccessorsAsList(n))); + visited.Add(n); + stackAsSet.Add(n); + System.Diagnostics.Debug.Assert(stack.Count == stackAsSet.Count); + } + return new HashSet(); + } + + // [Dragon, p. 606] + static ReducibleResult ComputeReducible(Graph g, + Node source, + DomRelation/*!*/ DomRelation) { + Contract.Requires(DomRelation != null); + + //Console.WriteLine("[" + DateTime.Now +"]: begin ComputeReducible"); + IEnumerable> edges = g.Edges; + Contract.Assert(Contract.ForAll(edges, n => n.Item1 != null && n.Item2 != null)); + HashSet> backEdges = new HashSet>(); + HashSet> nonBackEdges = new HashSet>(); + foreach (Tuple e in edges) { + Contract.Assert(e.Item1 != null); + Contract.Assert(e.Item2 != null); + Node x = e.Item1; + Node y = e.Item2; // so there is an edge from x to y + if (DomRelation.DominatedBy(x, y)) { // y dom x: which means y dominates x + backEdges.Add(e); + } else { + nonBackEdges.Add(e); + } + } + Graph withoutBackEdges = new Graph(nonBackEdges); + if (!Acyclic(withoutBackEdges, source)) { + return new ReducibleResult(false, + new HashSet(), + new Dictionary>(), + new Dictionary, HashSet>(), + FindCycle(withoutBackEdges, source)); + } else { + // original A#: + //Set headers = Set{ d : in backEdges }; + HashSet headers = new HashSet(); + foreach (Tuple e in backEdges) { + + Contract.Assert(e.Item1 != null); + Contract.Assert(e.Item2 != null); + headers.Add(e.Item2); + } + // original A#: + //Map> backEdgeNodes = Map{ h -> bs : h in headers, bs = Set{ b : in backEdges, x == h } }; + Dictionary> backEdgeNodes = new Dictionary>(); + foreach (Node/*!*/ h in headers) { + Contract.Assert(h != null); + HashSet bs = new HashSet(); + foreach (Tuple backedge in backEdges) { + Contract.Assert(backedge.Item1 != null); + Contract.Assert(backedge.Item2 != null); + if (backedge.Item2.Equals(h)) { + bs.Add(backedge.Item1); + } + } + backEdgeNodes.Add(h, bs); + } + + // original A#: + //Map,Set> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges }; + Dictionary, HashSet> naturalLoops = new Dictionary, HashSet>(); + foreach (Tuple e in backEdges) { + Contract.Assert(e.Item1 != null && e.Item2 != null); + naturalLoops.Add(e, NaturalLoop(g, e)); + } + + //Console.WriteLine("[" + DateTime.Now +"]: end ComputeReducible"); + return new ReducibleResult(true, headers, backEdgeNodes, naturalLoops, new HashSet()); + } + } + + public bool Reducible { + get { + return reducible; + } + } + public IEnumerable Headers { + get { + return headers; + } + } + public IEnumerable BackEdgeNodes(Node/*!*/ h) { + Contract.Requires(h != null); + // original A#: + //return h in backEdgeNodes ? backEdgeNodes[h] : null; + return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable)new List()); + } + public IEnumerable NaturalLoops(Node/*!*/ header, Node/*!*/ backEdgeNode) { + Contract.Requires(header != null); + Contract.Requires(backEdgeNode != null); + Tuple e = new Tuple(backEdgeNode, header); + return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable)new List(); + } + public HashSet SplitCandidates { + get { + return splitCandidates; + } + } + public void ComputeLoops() { + ReducibleResult r = ComputeReducible(this, this.source); + this.reducible = r.reducible; + this.headers = r.headers; + this.backEdgeNodes = r.backEdgeNodes; + this.naturalLoops = r.naturalLoops; + this.splitCandidates = r.splitCandidates; + return; + } + + public IEnumerable SortHeadersByDominance() + { + Graph dag = new Graph(); + foreach (Node b in headers) + { + dag.AddSource(b); + foreach (Node c in headers) + { + if (b.Equals(c)) continue; + if (DominatorMap.DominatedBy(b, c)) + { + System.Diagnostics.Debug.Assert(!DominatorMap.DominatedBy(c, b)); + dag.AddEdge(b, c); + } + } + } + return dag.TopologicalSort(); + } + + public string ToDot(Func NodeLabel = null, Func NodeStyle = null) { + NodeLabel = NodeLabel ?? (n => n.ToString()); + NodeStyle = NodeStyle ?? (n => "[shape=box]"); + var s = new StringBuilder(); + s.AppendLine("digraph G {"); + foreach (var n in Nodes) + s.AppendLine(" \"" + NodeLabel(n) + "\" " + NodeStyle(n) + ";"); + foreach (var e in Edges) + s.AppendLine(" \"" + NodeLabel(e.Item1) + "\" -> \"" + NodeLabel(e.Item2) + "\";"); + s.AppendLine("}"); + return s.ToString(); + } + + public ICollection ComputeReachable() { + ICollection result = new HashSet(); + Stack stack = new Stack(); + stack.Push(source); + while(!(stack.Count() == 0)) { + Node n = stack.Pop(); + result.Add(n); + foreach(var m in Successors(n)) { + if(!result.Contains(m)) { + stack.Push(m); + } + } + } + return result; + } + + } // end: class Graph + + public static class GraphAlgorithms + { + + + public static Graph Dual(this Graph g, Node dummySource) + { + var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList(); + Node source; + if (exits.Count == 0) + exits.Add(dummySource); + var dual = new Graph(new HashSet>(g.Edges.Select(e => new Tuple(e.Item2, e.Item1)))); + if (exits.Count == 1) + { + dual.AddSource(exits[0]); + source = exits[0]; + } + else + { + dual.AddSource(dummySource); + source = dummySource; + foreach (var exit in exits) + dual.AddEdge(dummySource, exit); + } + + #region Dual graph may not be connected, so add an edge from the dual graph's soure node to any unreachable node + foreach (var n in dual.Nodes.Where(Item => !dual.ComputeReachable().Contains(Item))) + { + dual.AddEdge(source, n); + } + #endregion + + return dual; + } + + public static List> LoopyTopSort(this Graph g) + { + Contract.Assert(g.Reducible); + + int n = g.Nodes.Count; + var nodeToNumber = new Dictionary(n); + var numberToNode = new Node[n]; + var allNodes = new List(); + int counter = 0; + foreach (Node node in g.Nodes) + { + numberToNode[counter] = node; + nodeToNumber[node] = counter; + allNodes.Add(counter); + counter++; + } + + var loops = new List[n]; + foreach (var h in g.Headers) + { + var loopNodes = new HashSet(); + foreach (var b in g.BackEdgeNodes(h)) + loopNodes.UnionWith(g.NaturalLoops(h, b)); + loops[nodeToNumber[h]] = + new List(loopNodes.Select(node => nodeToNumber[node])); + } + + var successors = new List[n]; + var predecessors = new List[n]; + int[] incomingEdges = new int[n]; + + for (int i = 0; i < n; i++) + predecessors[i] = new List(); + + foreach (var e in g.Edges) + { + Contract.Assert(e.Item1 != null); + Contract.Assert(e.Item2 != null); + int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2]; + if (loops[target] == null || !loops[target].Contains(source)) + { + if (successors[source] == null) + successors[source] = new List(); + successors[source].Add(target); + incomingEdges[target]++; + } + predecessors[target].Add(source); + } + + var sortedNodes = new List>(); + var sortedNodesInternal = new List(); + + var regionStack = new Stack>>(); + regionStack.Push(new Tuple>(default(Node), allNodes)); + + while (regionStack.Count != 0) + { + var rootIndexes = new List(); + foreach (var i in regionStack.Peek().Item2) + { + if (incomingEdges[i] == 0) + rootIndexes.Add(i); + } + if (rootIndexes.Count() == 0) + { + var region = regionStack.Pop(); + if (regionStack.Count != 0) { + sortedNodes.Add(new Tuple(region.Item1, true)); + sortedNodesInternal.Add(nodeToNumber[region.Item1]); + } + continue; + } + int rootIndex = rootIndexes[0]; + int maxPredIndex = -1; + foreach (var i in rootIndexes) { + foreach (var p in predecessors[i]) { + int predIndex = + sortedNodesInternal.FindLastIndex(x => x == p); + if (predIndex > maxPredIndex) { + rootIndex = i; + maxPredIndex = predIndex; + } + } + } + incomingEdges[rootIndex] = -1; + sortedNodes.Add(new Tuple(numberToNode[rootIndex], false)); + sortedNodesInternal.Add(rootIndex); + if (successors[rootIndex] != null) + foreach (int s in successors[rootIndex]) + incomingEdges[s]--; + if (loops[rootIndex] != null) + regionStack.Push(new Tuple>(numberToNode[rootIndex], + loops[rootIndex])); + } + + return sortedNodes; + } + + // Algorithm from Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren, + // "The Program Dependence Graph and Its Use in Optimization" + public static Dictionary> ControlDependence(this Graph g) where Node : class, new() + { + Graph dual = g.Dual(new Node()); + DomRelation pdom = dual.DominatorMap; + + var result = new Dictionary>(); + + var S = g.Edges.Where(e => !pdom.DominatedBy(e.Item1, e.Item2)); + foreach (var edge in S) + { + var L = pdom.LeastCommonAncestor(edge.Item1, edge.Item2); + var deps = new List(); + if (L == edge.Item1) + { + pdom.DominatedBy(edge.Item2, edge.Item1, deps); + deps.Add(edge.Item2); + deps.Add(edge.Item1); + } + else + { + pdom.DominatedBy(edge.Item2, L, deps); + deps.Add(edge.Item2); + } + if (result.ContainsKey(edge.Item1)) + { + result[edge.Item1].UnionWith(deps); + } + else + { + result[edge.Item1] = new HashSet(deps); + } + } + + return result; + } + + public static void TransitiveClosure(this Dictionary> graph) where Node : class { + bool changed; + do { + changed = false; + foreach (var entry in graph) { + var newSuccessors = new HashSet(entry.Value); + foreach (var successor in entry.Value) { + if (graph.ContainsKey(successor)) + newSuccessors.UnionWith(graph[successor]); + } + if (newSuccessors.Count != entry.Value.Count) { + entry.Value.UnionWith(newSuccessors); + changed = true; + } + } + } while (changed); + } + + } + + public delegate System.Collections.IEnumerable/**//*!*/ Adjacency(T/*!*/ node); + + + // An SCC is a set of nodes + public sealed class SCC : ICollection + { + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(nodesMap != null); + } + + private IDictionary/*!*/ nodesMap = new Dictionary(); + private ICollection/*!*/ nodes + { + get + { + return cce.NonNull(nodesMap.Keys); + } + } + + [Pure] + [GlobalAccess(false)] + [Escapes(true, false)] + System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator() + { + Contract.Ensures(Contract.Result() != null); + + return ((System.Collections.IEnumerable)nodes).GetEnumerator(); + } + + [Pure] + [GlobalAccess(false)] + [Escapes(true, false)] + IEnumerator/*!*/ IEnumerable.GetEnumerator() + { + Contract.Ensures(Contract.Result>() != null); + + return ((IEnumerable)nodes).GetEnumerator(); + } + + public int Count + { + get + { + return nodes.Count; + } + } + public bool IsReadOnly + { + get + { + return nodesMap.IsReadOnly; + } + } + public void Add(Node item) + { + nodesMap.Add(item, null); + } + public void Clear() + { + nodesMap.Clear(); + } + [Pure] + public bool Contains(Node item) + { + return nodesMap.ContainsKey(item); + } + public void CopyTo(Node[] array, int arrayIndex) + { + //Contract.Requires(array != null); + nodes.CopyTo(array, arrayIndex); + } + public bool Remove(Node item) + { + return nodesMap.Remove(item); + } + } + + public sealed class StronglyConnectedComponents : IEnumerable/*!*/> where Node : class + { + private readonly IDictionary/*!*/ graph; + [ContractInvariantMethod] + void graphInvariantMethod() + { + Contract.Invariant(Contract.ForAll(graph, entry => entry.Key != null)); + Contract.Invariant(preds != null); + Contract.Invariant(succs != null); + } + private readonly Adjacency/*!*/ preds; + private readonly Adjacency/*!*/ succs; + + private bool computed = false; + public bool Computed + { + get + { + return computed; + } + } + + [NotDelayed] + public StronglyConnectedComponents(System.Collections.IEnumerable/**/ graph, Adjacency preds, Adjacency succs) + : base() + { + Contract.Requires(succs != null); + Contract.Requires(preds != null); + Contract.Requires(graph != null); + Contract.Ensures(!Computed); + IDictionary/*!*/ dict = new Dictionary(); + foreach (Node/*!*/ n in graph) + { + Contract.Assert(n != null); + dict.Add(n, null); + } + + this.graph = dict; + this.preds = preds; + this.succs = succs; + } + + [Pure] + [GlobalAccess(false)] + [Escapes(true, false)] + System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator() + { + Contract.Ensures(Contract.Result() != null); + + return ((System.Collections.IEnumerable)sccs).GetEnumerator(); + } + + [Pure] + [GlobalAccess(false)] + [Escapes(true, false)] + IEnumerator/*!*/>/*!*/ IEnumerable/*!*/>.GetEnumerator() + { + Contract.Ensures(Contract.Result>>() != null); + + Contract.Assume(Computed); + Contract.Assert(cce.NonNullElements((IEnumerable/*!*/>)sccs));//REVIEW + return ((IEnumerable/*!*/>)sccs).GetEnumerator(); + } + + private readonly IList/*!*/>/*!*/ sccs = new List/*!*/>(); + [ContractInvariantMethod] + void sccsInvariant() + { + Contract.Invariant(cce.NonNullElements(sccs)); + } + + + public void Compute() + { + Contract.Requires(!Computed); + Contract.Ensures(Computed); + // Compute post times on graph with edges reversed + this.dfsNext = this.preds; + foreach (Node/*!*/ n in cce.NonNull(graph.Keys)) + { + Contract.Assert(n != null); + if (!seen.ContainsKey(n)) + { + OrderNodes(n); + } + } + + // Clear seen + seen.Clear(); + + // Compute SCCs + this.dfsNext = this.succs; + while (postOrder.Count > 0) + { + Node/*!*/ n = postOrder.Pop(); + Contract.Assert(n != null); + + if (!seen.ContainsKey(n)) + { + SCC/*!*/ curr = new SCC(); + FindSCCs(n, curr); + sccs.Add(curr); + } + } + + // Clear seen + seen.Clear(); + + this.computed = true; + } + + private Adjacency/*?*/ dfsNext = null; + + private readonly IDictionary/*!*/ seen = new Dictionary(); + private readonly Stack/*!*/ postOrder = new Stack(); + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(seen != null); + Contract.Invariant(cce.NonNullElements(postOrder)); + } + + + // DFS to order nodes by post times + private void OrderNodes(Node node) + { + Contract.Requires(node != null); + seen.Add(node, null); + + Contract.Assert(dfsNext != null); + System.Collections.IEnumerable/*!*/ nexts = dfsNext(node); + Contract.Assert(nexts != null); + foreach (Node/*!*/ n in nexts) + { + Contract.Assert(n != null); + if (graph.ContainsKey(n) && !seen.ContainsKey(n)) + { + OrderNodes(n); + } + } + + postOrder.Push(node); + } + + // DFS to compute SCCs + private void FindSCCs(Node node, SCC currSCC) + { + Contract.Requires(currSCC != null); + Contract.Requires(node != null); + //modifies currSCC.*; + seen.Add(node, null); + currSCC.Add(node); + + Contract.Assert(dfsNext != null); + System.Collections.IEnumerable/*!*/ nexts = dfsNext(node); + Contract.Assert(nexts != null); + foreach (Node/*!*/ n in nexts) + { + Contract.Assert(n != null); + if (graph.ContainsKey(n) && !seen.ContainsKey(n)) + { + FindSCCs(n, currSCC); + } + } + } + + [Pure] + public override string ToString() + { + Contract.Ensures(Contract.Result() != null); + string outStr = ""; + int i = 0; + + foreach (ICollection component in this) + { + string/*!*/ tmp = System.String.Format("\nComponent #{0} = ", i++); + Contract.Assert(tmp != null); + outStr += tmp; + + bool firstInRow = true; + + foreach (Node b in component) + { + string/*!*/ tmpComponent = System.String.Format("{0}{1}", firstInRow ? "" : ", ", b); + Contract.Assert(tmpComponent != null); + outStr += tmpComponent; + firstInRow = false; + } + } + return outStr; + } + + } + + public class GraphProgram { + static void TestGraph(T/*!*/ source, params Tuple[] edges) { + Contract.Requires(source != null); + Contract.Requires(Contract.ForAll(edges, pair => pair.Item1 != null && pair.Item2 != null)); + HashSet> es = new HashSet>(); + foreach (Tuple e in edges) { + Contract.Assert(e.Item1 != null && e.Item2 != null); + es.Add(e); + } + Graph g = new Graph(es); + g.AddSource(source); + Console.WriteLine("G = " + g); + g.ComputeLoops(); + Console.WriteLine("G's Dominator Map = " + g.DominatorMap); + Console.WriteLine("G's Immediate Dominator Map = " + Util.MapToString(g.ImmediateDominatorMap)); + Console.WriteLine("G is reducible: " + (g.Reducible ? "yes" : "no")); + } + + static void Main(string[] args) + //requires forall{string s in args; s != null}; + { + Console.WriteLine("Spec# says hello!"); + // This generates bad IL -- need to fix a bug in the compiler + //Graph g = new Graph(new Set>{ new Tuple(1,2), new Tuple(1,3), new Tuple(2,3) }); + + Console.WriteLine(""); + TestGraph('a', + new Tuple('a', 'b'), + new Tuple('a', 'c'), + new Tuple('b', 'c') + ); + + Console.WriteLine(""); + TestGraph('a', + new Tuple('a', 'b'), + new Tuple('a', 'c'), + new Tuple('b', 'd'), + new Tuple('c', 'e'), + new Tuple('c', 'f'), + new Tuple('d', 'e'), + new Tuple('e', 'd'), + new Tuple('e', 'f'), + new Tuple('f', 'e') + ); + + Console.WriteLine(""); + TestGraph('a', + new Tuple('a', 'b'), + new Tuple('a', 'c'), + new Tuple('b', 'c'), + new Tuple('c', 'b') + ); + + Console.WriteLine(""); + TestGraph(1, + new Tuple(1, 2), + new Tuple(1, 3), + new Tuple(2, 3) + ); + + Console.WriteLine(""); + TestGraph(1, + new Tuple(1, 2), + new Tuple(1, 3), + new Tuple(2, 3), + new Tuple(3, 2) + ); + + Console.WriteLine(""); + TestGraph(2, + new Tuple(2, 3), + new Tuple(2, 4), + new Tuple(3, 2) + ); + + Console.WriteLine(""); + TestGraph('a', + new Tuple('a', 'b'), + new Tuple('a', 'c'), + new Tuple('b', 'c'), + new Tuple('b', 'b') + ); + + + } + } + +} diff --git a/Source/Graph/Graph.csproj b/Source/Graph/Graph.csproj index b4adf6e4..66759719 100644 --- a/Source/Graph/Graph.csproj +++ b/Source/Graph/Graph.csproj @@ -1,199 +1,199 @@ - - - - Debug - AnyCPU - 9.0.21022 - 2.0 - {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} - Library - Properties - Graph - Graph - v4.0 - 512 - 1 - true - ..\InterimKey.snk - - - 3.5 - - publish\ - true - Disk - false - Foreground - 7 - Days - false - false - true - 0 - 1.0.0.%2a - false - false - true - Client - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - False - False - True - False - False - False - False - False - False - False - False - True - False - False - False - - - - - - - - - - - - - Full - %28none%29 - AllRules.ruleset - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - AllRules.ruleset - - - true - bin\z3apidebug\ - DEBUG;TRACE - full - AnyCPU - - - true - GlobalSuppressions.cs - prompt - Migrated rules for Graph.ruleset - true - 4 - false - - - true - bin\Checked\ - DEBUG;TRACE - full - AnyCPU - bin\Debug\Graph.dll.CodeAnalysisLog.xml - true - GlobalSuppressions.cs - prompt - AllRules.ruleset - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets - ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules - True - False - True - False - False - False - False - False - False - False - False - False - True - False - False - False - - - - - - - False - Full - Build - 0 - 4 - false - - - true - bin\QED\ - DEBUG;TRACE - full - AnyCPU - prompt - AllRules.ruleset - - - - - - - - - version.cs - - - - - - {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} - CodeContractsExtender - - - - - - - - False - .NET Framework 3.5 SP1 Client Profile - false - - - False - .NET Framework 3.5 SP1 - true - - - False - Windows Installer 3.1 - true - - - - - + + + + Debug + AnyCPU + 9.0.21022 + 2.0 + {69A2B0B8-BCAC-4101-AE7A-556FCC58C06E} + Library + Properties + Graph + Graph + v4.0 + 512 + 1 + true + ..\InterimKey.snk + + + 3.5 + + publish\ + true + Disk + false + Foreground + 7 + Days + false + false + true + 0 + 1.0.0.%2a + false + false + true + Client + + + true + full + false + bin\Debug\ + DEBUG;TRACE + prompt + 4 + False + False + True + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + + + + + + + Full + %28none%29 + AllRules.ruleset + + + pdbonly + true + bin\Release\ + TRACE + prompt + 4 + AllRules.ruleset + + + true + bin\z3apidebug\ + DEBUG;TRACE + full + AnyCPU + + + true + GlobalSuppressions.cs + prompt + Migrated rules for Graph.ruleset + true + 4 + false + + + true + bin\Checked\ + DEBUG;TRACE + full + AnyCPU + bin\Debug\Graph.dll.CodeAnalysisLog.xml + true + GlobalSuppressions.cs + prompt + AllRules.ruleset + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets + ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + True + False + True + False + False + False + False + False + False + False + False + False + True + False + False + False + + + + + + + False + Full + Build + 0 + 4 + false + + + true + bin\QED\ + DEBUG;TRACE + full + AnyCPU + prompt + AllRules.ruleset + + + + + + + + + version.cs + + + + + + {ACCC0156-0921-43ED-8F67-AD8BDC8CDE31} + CodeContractsExtender + + + + + + + + False + .NET Framework 3.5 SP1 Client Profile + false + + + False + .NET Framework 3.5 SP1 + true + + + False + Windows Installer 3.1 + true + + + + + diff --git a/Source/Graph/cce.cs b/Source/Graph/cce.cs index ef594484..1e0b12a5 100644 --- a/Source/Graph/cce.cs +++ b/Source/Graph/cce.cs @@ -1,193 +1,193 @@ -using System; -using SA=System.Attribute; -using System.Collections.Generic; -using System.Diagnostics.Contracts; -using System.Text; -//using Microsoft.Boogie; - -/// -/// A class containing static methods to extend the functionality of Code Contracts -/// - -public static class cce { - //[Pure] - //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { - // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); - //} - [Pure] - public static T NonNull(T t) { - Contract.Assert(t != null); - return t; - } - [Pure] - public static bool NonNullElements(IEnumerable collection) { - return collection != null && Contract.ForAll(collection, c => c != null); - } - [Pure] - public static bool NonNullElements(IDictionary collection) { - return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair)); - } - //[Pure] - //public static bool NonNullElements(VariableSeq collection) { - // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); - //} - /// - /// For possibly-null lists of non-null elements - /// - /// - /// - /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! - /// - [Pure] - public static bool NonNullElements(IEnumerable collection, bool nullability) { - return (nullability && collection == null) || cce.NonNullElements(collection); - //Should be the same as: - /*if(nullability&&collection==null) - * return true; - * return cce.NonNullElements(collection) - */ - - } - [Pure] - public static bool NonNullElements(KeyValuePair kvp) { - return kvp.Key != null && kvp.Value != null; - } - [Pure] - public static bool NonNullElements(IEnumerator iEnumerator) { - return iEnumerator != null; - } - //[Pure] - //public static bool NonNullElements(Graphing.Graph graph) { - // return cce.NonNullElements(graph.TopologicalSort()); - //} - [Pure] - public static void BeginExpose(object o) { - } - [Pure] - public static void EndExpose() { - } - [Pure] - public static bool IsPeerConsistent(object o) { - return true; - } - [Pure] - public static bool IsConsistent(object o) { - return true; - } - [Pure] - public static bool IsExposable(object o) { - return true; - } - [Pure] - public static bool IsExposed(object o) { - return true; - } - [Pure] - public static bool IsNew(object o) { - return true; - } - public static class Owner { - [Pure] - public static bool Same(object o, object p) { - return true; - } - [Pure] - public static void AssignSame(object o, object p) { - } - [Pure] - public static object ElementProxy(object o) { - return o; - } - [Pure] - public static bool None(object o) { - return true; - } - [Pure] - public static bool Different(object o, object p) { - return true; - } - [Pure] - public static bool New(object o) { - return true; - } - } - [Pure] - public static void LoopInvariant(bool p) { - Contract.Assert(p); - } - public class UnreachableException : Exception { - public UnreachableException() { - } - } - //[Pure] - //public static bool IsValid(Microsoft.Dafny.Expression expression) { - // return true; - //} - //public static List toList(PureCollections.Sequence s) { - // List toRet = new List(); - // foreach (T t in s.elems) - // if(t!=null) - // toRet.Add(t); - // return toRet; - //} - - //internal static bool NonNullElements(Set set) { - // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); - //} -} - -public class PeerAttribute : SA { -} -public class RepAttribute : SA { -} -public class CapturedAttribute : SA { -} -public class NotDelayedAttribute : SA { -} -public class NoDefaultContractAttribute : SA { -} -public class VerifyAttribute : SA { - public VerifyAttribute(bool b) { - - } -} -public class StrictReadonlyAttribute : SA { -} -public class AdditiveAttribute : SA { -} -public class ReadsAttribute : SA { - public enum Reads { - Nothing, - Everything, - }; - public ReadsAttribute(object o) { - } -} -public class GlobalAccessAttribute : SA { - public GlobalAccessAttribute(bool b) { - } -} -public class EscapesAttribute : SA { - public EscapesAttribute(bool b, bool b_2) { - } -} -public class NeedsContractsAttribute : SA { - public NeedsContractsAttribute() { - } - public NeedsContractsAttribute(bool ret, bool parameters) { - } - public NeedsContractsAttribute(bool ret, int[] parameters) { - } -} -public class ImmutableAttribute : SA { -} -public class InsideAttribute : SA { -} -public class SpecPublicAttribute : SA { -} -public class ElementsPeerAttribute : SA { -} -public class ResultNotNewlyAllocatedAttribute : SA { -} -public class OnceAttribute : SA { +using System; +using SA=System.Attribute; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +//using Microsoft.Boogie; + +/// +/// A class containing static methods to extend the functionality of Code Contracts +/// + +public static class cce { + //[Pure] + //public static bool NonNullElements(Microsoft.Dafny.Graph collection) { + // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //} + [Pure] + public static T NonNull(T t) { + Contract.Assert(t != null); + return t; + } + [Pure] + public static bool NonNullElements(IEnumerable collection) { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullElements(IDictionary collection) { + return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair)); + } + //[Pure] + //public static bool NonNullElements(VariableSeq collection) { + // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + //} + /// + /// For possibly-null lists of non-null elements + /// + /// + /// + /// If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>! + /// + [Pure] + public static bool NonNullElements(IEnumerable collection, bool nullability) { + return (nullability && collection == null) || cce.NonNullElements(collection); + //Should be the same as: + /*if(nullability&&collection==null) + * return true; + * return cce.NonNullElements(collection) + */ + + } + [Pure] + public static bool NonNullElements(KeyValuePair kvp) { + return kvp.Key != null && kvp.Value != null; + } + [Pure] + public static bool NonNullElements(IEnumerator iEnumerator) { + return iEnumerator != null; + } + //[Pure] + //public static bool NonNullElements(Graphing.Graph graph) { + // return cce.NonNullElements(graph.TopologicalSort()); + //} + [Pure] + public static void BeginExpose(object o) { + } + [Pure] + public static void EndExpose() { + } + [Pure] + public static bool IsPeerConsistent(object o) { + return true; + } + [Pure] + public static bool IsConsistent(object o) { + return true; + } + [Pure] + public static bool IsExposable(object o) { + return true; + } + [Pure] + public static bool IsExposed(object o) { + return true; + } + [Pure] + public static bool IsNew(object o) { + return true; + } + public static class Owner { + [Pure] + public static bool Same(object o, object p) { + return true; + } + [Pure] + public static void AssignSame(object o, object p) { + } + [Pure] + public static object ElementProxy(object o) { + return o; + } + [Pure] + public static bool None(object o) { + return true; + } + [Pure] + public static bool Different(object o, object p) { + return true; + } + [Pure] + public static bool New(object o) { + return true; + } + } + [Pure] + public static void LoopInvariant(bool p) { + Contract.Assert(p); + } + public class UnreachableException : Exception { + public UnreachableException() { + } + } + //[Pure] + //public static bool IsValid(Microsoft.Dafny.Expression expression) { + // return true; + //} + //public static List toList(PureCollections.Sequence s) { + // List toRet = new List(); + // foreach (T t in s.elems) + // if(t!=null) + // toRet.Add(t); + // return toRet; + //} + + //internal static bool NonNullElements(Set set) { + // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); + //} +} + +public class PeerAttribute : SA { +} +public class RepAttribute : SA { +} +public class CapturedAttribute : SA { +} +public class NotDelayedAttribute : SA { +} +public class NoDefaultContractAttribute : SA { +} +public class VerifyAttribute : SA { + public VerifyAttribute(bool b) { + + } +} +public class StrictReadonlyAttribute : SA { +} +public class AdditiveAttribute : SA { +} +public class ReadsAttribute : SA { + public enum Reads { + Nothing, + Everything, + }; + public ReadsAttribute(object o) { + } +} +public class GlobalAccessAttribute : SA { + public GlobalAccessAttribute(bool b) { + } +} +public class EscapesAttribute : SA { + public EscapesAttribute(bool b, bool b_2) { + } +} +public class NeedsContractsAttribute : SA { + public NeedsContractsAttribute() { + } + public NeedsContractsAttribute(bool ret, bool parameters) { + } + public NeedsContractsAttribute(bool ret, int[] parameters) { + } +} +public class ImmutableAttribute : SA { +} +public class InsideAttribute : SA { +} +public class SpecPublicAttribute : SA { +} +public class ElementsPeerAttribute : SA { +} +public class ResultNotNewlyAllocatedAttribute : SA { +} +public class OnceAttribute : SA { } \ No newline at end of file -- cgit v1.2.3