From c7f74de7fae661883ca13bb09d557272de659e03 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 19 Feb 2013 14:26:31 -0800 Subject: CR/LF line ending delta --- Source/Graph/Graph.cs | 1930 ++++++++++++++++++++++++------------------------- 1 file changed, 965 insertions(+), 965 deletions(-) (limited to 'Source/Graph') diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 10c15b40..4d58cbe7 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -1,879 +1,879 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- +//----------------------------------------------------------------------------- +// +// 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) - { - var nums = new HashSet(); - int num1 = nodeToPostOrderNumber[n1], num2 = nodeToPostOrderNumber[n2]; - - while (true) - { - if (!nums.Add(num1)) - return postOrderNumberToNode[num1].Val; - if (!nums.Add(num2)) - return postOrderNumberToNode[num2].Val; - num1 = doms[num1]; num2 = doms[num2]; - } - } - } - - 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 acyclic; - List sortedList; - this.TarjanTopSort(out acyclic, out sortedList); - return acyclic ? sortedList : new List(); - } - // From Tarjan 1972 - public void TarjanTopSort(out bool acyclic, out List sortedNodes) { - 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; - 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(); - } +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) + { + var nums = new HashSet(); + int num1 = nodeToPostOrderNumber[n1], num2 = nodeToPostOrderNumber[n2]; + + while (true) + { + if (!nums.Add(num1)) + return postOrderNumberToNode[num1].Val; + if (!nums.Add(num2)) + return postOrderNumberToNode[num2].Val; + num1 = doms[num1]; num2 = doms[num2]; + } + } + } + + 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 acyclic; + List sortedList; + this.TarjanTopSort(out acyclic, out sortedList); + return acyclic ? sortedList : new List(); + } + // From Tarjan 1972 + public void TarjanTopSort(out bool acyclic, out List sortedNodes) { + 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; + 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(); + } } // end: class Graph public static class GraphAlgorithms @@ -1285,93 +1285,93 @@ namespace Microsoft.Boogie.GraphUtil { 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') - ); - - - } - } - -} + } + + 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') + ); + + + } + } + +} -- cgit v1.2.3