From 23a34b0b43e4bad8c1919d65e38f76117ab8b20e Mon Sep 17 00:00:00 2001 From: tabarbe Date: Fri, 27 Aug 2010 00:24:40 +0000 Subject: Boogie: Renaming the Graph files in preparation for the commit of my port. --- Source/Graph/Graph.cs | 746 +++++++++++++++++++++++++++++++++++++++++++++ Source/Graph/Graph.csproj | 93 ++++++ Source/Graph/Graph.ssc | 746 --------------------------------------------- Source/Graph/Graph.sscproj | 93 ------ 4 files changed, 839 insertions(+), 839 deletions(-) create mode 100644 Source/Graph/Graph.cs create mode 100644 Source/Graph/Graph.csproj delete mode 100644 Source/Graph/Graph.ssc delete mode 100644 Source/Graph/Graph.sscproj (limited to 'Source/Graph') diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs new file mode 100644 index 00000000..12f7fd8c --- /dev/null +++ b/Source/Graph/Graph.cs @@ -0,0 +1,746 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Collections.Generic; +using Microsoft.SpecSharp.Collections; +using Microsoft.Contracts; +using System.Text; // for StringBuilder +namespace Graphing{ + +internal static class Util{ + private static string! ListToString(IEnumerable xs){ + StringBuilder sb = new StringBuilder(); + sb.Append("["); + bool first = true; + foreach(T! x in xs){ + if (!first) sb.Append(", "); + sb.Append(x.ToString()); + first = false; + } + sb.Append("]"); + return sb.ToString(); + } + public static string! MapToString(Dictionary> d){ + StringBuilder sb = new StringBuilder(); + sb.Append("{"); + bool first = true; + foreach (KeyValuePair> de in d){ + if (!first) sb.Append(", "); + 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 { assume IsSet; return Value; } + set { Value = value; IsSet = true; } + } + public void UnSet() { + IsSet = false; + } +} + +internal 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 { assume this.immediateDominatorMap != null; return this.immediateDominatorMap; } + } + public bool DominatedBy(Node dominee, Node dominator){ + assume this.nodeToPostOrderNumber != null; + assume this.doms != null; + int domineeNum = this.nodeToPostOrderNumber[dominee]; + int dominatorNum = this.nodeToPostOrderNumber[dominator]; + if (domineeNum == dominatorNum) return true; + int currentNodeNum = this.doms[domineeNum]; + do { + if (currentNodeNum == dominatorNum) return true; + currentNodeNum = this.doms[currentNodeNum]; + } while (currentNodeNum != this.sourceNum); + return false; + } + private Dictionary>? domMap = null; + [Pure] + public override string ToString(){ + assume this.doms != null; + int[] localDoms = this.doms; + 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(", "); + 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){ + if (0 < i) Console.Write(", "); + Console.Write(x.ToString()); + i++; + } + Console.WriteLine("]"); + } + public string! ListToString(IEnumerable xs){ + StringBuilder sb = new StringBuilder(); + sb.Append("["); + bool first = true; + foreach(T! x in xs){ + 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(); + Dictionary visited = new Dictionary(n); + int currentNumber = 1; + assume this.source != null; + this.PostOrderVisit(this.source, visited, ref currentNumber); + 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, Dictionary visited, ref int currentNumber){ + if (visited.ContainsKey(n)) return; + visited[n] = true; + foreach(Node! child in this.graph.Successors(n)){ + PostOrderVisit(child, visited, ref currentNumber); + } + assume this.postOrderNumberToNode != null; + assume this.nodeToPostOrderNumber != null; + this.postOrderNumberToNode[currentNumber].Val = n; + this.nodeToPostOrderNumber[n] = currentNumber; + currentNumber++; + return; + } +} +public class Graph { + private Set> es; + private Set ns; + private Node source; + private bool reducible; + private Set headers; + private Map> backEdgeNodes; + private Map,Set> naturalLoops; + private DomRelation? dominatorMap = null; + private Dictionary> predCache = new Dictionary>(); + private Dictionary> succCache = new Dictionary>(); + private bool predComputed; + + private class PreHeader { + Node! myHeader; + internal PreHeader(Node! h) { myHeader = h; } + + [Pure] + public override string! ToString() { return "#" + myHeader.ToString(); } + } + + public Graph(Set> edges) + { + es = edges; + + // original A# + //ns = Set{ x : in es } + Set{ y : in es }; + + // closest Spec# + //ns = new Set{ Pair p in edges; p.First } + new Set{ Pair p in edges; p.Second }; + + // + Set temp = new Set(); + foreach (Pair p in edges){ + temp.Add(p.First); + temp.Add(p.Second); + } + ns = temp; + } + public Graph() + { es = new Set>(); ns = new Set(); } + + // BUGBUG: Set.ToString() should return a non-null string + [Pure] + public override string! ToString() { return "" + es.ToString(); } + + public void AddSource(Node! x) + { + // BUGBUG: This generates bad code in the compiler + //ns += new Set{x}; + ns.Add(x); + source = x; + } + + public void AddEdge(Node! source, Node! dest) + { + //es += Set{}; + //ns += Set{source, dest}; + es.Add(new Pair(source,dest)); + ns.Add(source); + ns.Add(dest); + predComputed = false; + } + + public Set Nodes { get { return ns; } } + public IEnumerable> Edges { get { return es; } } + + public bool Edge(Node! x, Node! y) { + // original A# + // return in es; + return es.Contains(new Pair(x,y)); + } + + private void ComputePredSuccCaches() + { + if (predComputed) return; + predComputed = true; + predCache = new Dictionary>(); + succCache = new Dictionary>(); + + foreach (Node n in Nodes) { + predCache[n] = new Set(); + succCache[n] = new Set(); + } + + foreach(Pair p in Edges){ + Set tmp; + + tmp = predCache[p.Second]; + tmp.Add(p.First); + predCache[p.Second] = tmp; + + tmp = succCache[p.First]; + tmp.Add(p.Second); + succCache[p.First] = tmp; + } + } + + internal IEnumerable Predecessors(Node n) + { + // original A# + //Set result = Set{ x : x in Nodes, Edge(x,n) }; + + ComputePredSuccCaches(); + return predCache[n]; + } + + internal IEnumerable Successors(Node n) + { + ComputePredSuccCaches(); + return succCache[n]; + } + + internal DomRelation /*Map>*/ DominatorMap + { + get { + assert source != null; + if (this.dominatorMap == null){ + this.dominatorMap = new DomRelation(this, this.source); + } + return this.dominatorMap; + } + } + + public Dictionary> ImmediateDominatorMap + { + get { + assert source != null; + if (this.dominatorMap == null){ + this.dominatorMap = new DomRelation(this, this.source); + } + return this.dominatorMap.ImmediateDominatorMap; + } + } + public List ImmediatelyDominatedBy(Node! n) { + 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 (Pair e in this.Edges){ + Node! target = e.Second; + 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() + { + Pair> result = this.TopSort(); + return result.First ? result.Second : (IEnumerable)new Seq(); + } + // From AsmL distribution example + private Pair> TopSort() + { + Seq S = new Seq(); + Set V = this.Nodes; + Set X = new Set(); + foreach (Node! n in V){ X.Add(n); } + bool change = true; + while ( change ) + // invariant: X = V - S + { + change = false; + if (X.Count > 0){ + foreach (Node! n in X){ + // see if n has any incoming edges from any other node in X + bool inDegreeZero = true; + foreach(Node! u in X){ + 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 Pair>(false,new Seq()); + } + } + } + return new Pair>(true,S); + } + + public static bool Acyclic(Graph g, Node source) + { + bool acyclic; + List sortedList; + g.TarjanTopSort(out acyclic, out sortedList); + return acyclic; + } + + // + // [Dragon, pp. 670--671] + // returns map D s.t. d in D(n) iff d dom n + // + static private Map> OldComputeDominators(Graph g, Node! source){ + assert g.source != null; + Set N = g.Nodes; + Set nonSourceNodes = N - new Set(source); + Map> D = new Map>(); + D[source] = new Set(source); + foreach (Node! n in nonSourceNodes){ + D[n] = N; + } + bool change = true; + while ( change ){ + change = false; + foreach (Node! n in nonSourceNodes){ + + // original A# + //Set> allPreds = new Set>{ Node p in this.Predecessors(n) ; D[p] }; + + Set> allPreds = new Set>(); + foreach(Node! p in g.Predecessors(n)) allPreds.Add(D[p]); + Set temp = new Set(n) + Set.BigIntersect(allPreds); + if ( temp != D[n] ){ + change = true; + D[n] = temp; + } + } + } + return D; + } + + // [Dragon, Fig. 10.15, p. 604. Algorithm for constructing the natural loop.] + static Set NaturalLoop(Graph g, Pair backEdge) + { + Node! n = backEdge.First; + Node! d = backEdge.Second; + Seq stack = new Seq(); + Set loop = new Set(d); + if ( !n.Equals(d) ) // then n is not in loop + { + loop.Add(n); + stack = new Seq(n) + stack; // push n onto stack + } + while ( stack.Count > 0) // not empty + { + Node m = stack.Head; + stack = stack.Tail; // pop stack + foreach (Node! p in g.Predecessors(m)) + { + if ( !(loop.Contains(p)) ) + { + loop.Add(p); + stack = new Seq(p) + stack; // push p onto stack + } + } + } + return loop; + } + + internal struct ReducibleResult{ + internal bool reducible; + internal Set headers; + internal Map> backEdgeNodes; + internal Map,Set> naturalLoops; + internal ReducibleResult(bool b, + Set headers, + Map> backEdgeNodes, + Map,Set> naturalLoops){ + this.reducible = b; + this.headers = headers; + this.backEdgeNodes = backEdgeNodes; + this.naturalLoops = naturalLoops; + } + + } + + // [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); + } + + // [Dragon, p. 606] + static ReducibleResult ComputeReducible(Graph g, + Node source, + DomRelation! DomRelation) { + + //Console.WriteLine("[" + DateTime.Now +"]: begin ComputeReducible"); + IEnumerable> edges = g.Edges; + Set> backEdges = new Set>(); + Set> nonBackEdges = new Set>(); + foreach (Pair e in edges){ + Node x = e.First; + Node y = e.Second; // 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); + } + } + if ( !Acyclic(new Graph(nonBackEdges), source) ){ + return new ReducibleResult(false, + new Set(), + new Map>(), + new Map,Set>()); + }else{ + // original A#: + //Set headers = Set{ d : in backEdges }; + Set headers = new Set(); + foreach(Pair e in backEdges) + headers.Add(e.Second); + // original A#: + //Map> backEdgeNodes = Map{ h -> bs : h in headers, bs = Set{ b : in backEdges, x == h } }; + Map> backEdgeNodes = new Map>(); + foreach(Node! h in headers){ + Set bs = new Set(); + foreach(Pair backedge in backEdges){ + if (backedge.Second.Equals(h)){ + bs.Add(backedge.First); + } + } + backEdgeNodes.Add(h,bs); + } + + // original A#: + //Map,Set> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges }; + Map,Set> naturalLoops = new Map,Set>(); + foreach (Pair e in backEdges){ + naturalLoops.Add(e,NaturalLoop(g,e)); + } + + //Console.WriteLine("[" + DateTime.Now +"]: end ComputeReducible"); + return new ReducibleResult(true, headers, backEdgeNodes, naturalLoops); + } + } + + public bool Reducible { get { return reducible; } } + public IEnumerable Headers { get { return headers; } } + public IEnumerable BackEdgeNodes(Node! h){ + // original A#: + //return h in backEdgeNodes ? backEdgeNodes[h] : null; + return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable)new Seq()); + } + public IEnumerable NaturalLoops(Node! header, Node! backEdgeNode) + { + Pair e = new Pair(backEdgeNode,header); + return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable)new Seq(); + } + + 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; + return; + } + + +} // end: class Graph + +public class GraphProgram +{ + static void TestGraph(T! source, params Pair[] edges){ + Set> es = new Set>(); + foreach (Pair e in edges) 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 Pair(1,2), new Pair(1,3), new Pair(2,3) }); + + Console.WriteLine(""); + TestGraph('a', + new Pair('a','b'), + new Pair('a','c'), + new Pair('b','c') + ); + + Console.WriteLine(""); + TestGraph('a', + new Pair('a','b'), + new Pair('a','c'), + new Pair('b','d'), + new Pair('c','e'), + new Pair('c','f'), + new Pair('d','e'), + new Pair('e','d'), + new Pair('e','f'), + new Pair('f','e') + ); + + Console.WriteLine(""); + TestGraph('a', + new Pair('a','b'), + new Pair('a','c'), + new Pair('b','c'), + new Pair('c','b') + ); + + Console.WriteLine(""); + TestGraph(1, + new Pair(1,2), + new Pair(1,3), + new Pair(2,3) + ); + + Console.WriteLine(""); + TestGraph(1, + new Pair(1,2), + new Pair(1,3), + new Pair(2,3), + new Pair(3,2) + ); + + Console.WriteLine(""); + TestGraph(2, + new Pair(2,3), + new Pair(2,4), + new Pair(3,2) + ); + + Console.WriteLine(""); + TestGraph('a', + new Pair('a','b'), + new Pair('a','c'), + new Pair('b','c'), + new Pair('b','b') + ); + + + } +} + +} diff --git a/Source/Graph/Graph.csproj b/Source/Graph/Graph.csproj new file mode 100644 index 00000000..e849b569 --- /dev/null +++ b/Source/Graph/Graph.csproj @@ -0,0 +1,93 @@ + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/Source/Graph/Graph.ssc b/Source/Graph/Graph.ssc deleted file mode 100644 index 12f7fd8c..00000000 --- a/Source/Graph/Graph.ssc +++ /dev/null @@ -1,746 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Collections.Generic; -using Microsoft.SpecSharp.Collections; -using Microsoft.Contracts; -using System.Text; // for StringBuilder -namespace Graphing{ - -internal static class Util{ - private static string! ListToString(IEnumerable xs){ - StringBuilder sb = new StringBuilder(); - sb.Append("["); - bool first = true; - foreach(T! x in xs){ - if (!first) sb.Append(", "); - sb.Append(x.ToString()); - first = false; - } - sb.Append("]"); - return sb.ToString(); - } - public static string! MapToString(Dictionary> d){ - StringBuilder sb = new StringBuilder(); - sb.Append("{"); - bool first = true; - foreach (KeyValuePair> de in d){ - if (!first) sb.Append(", "); - 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 { assume IsSet; return Value; } - set { Value = value; IsSet = true; } - } - public void UnSet() { - IsSet = false; - } -} - -internal 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 { assume this.immediateDominatorMap != null; return this.immediateDominatorMap; } - } - public bool DominatedBy(Node dominee, Node dominator){ - assume this.nodeToPostOrderNumber != null; - assume this.doms != null; - int domineeNum = this.nodeToPostOrderNumber[dominee]; - int dominatorNum = this.nodeToPostOrderNumber[dominator]; - if (domineeNum == dominatorNum) return true; - int currentNodeNum = this.doms[domineeNum]; - do { - if (currentNodeNum == dominatorNum) return true; - currentNodeNum = this.doms[currentNodeNum]; - } while (currentNodeNum != this.sourceNum); - return false; - } - private Dictionary>? domMap = null; - [Pure] - public override string ToString(){ - assume this.doms != null; - int[] localDoms = this.doms; - 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(", "); - 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){ - if (0 < i) Console.Write(", "); - Console.Write(x.ToString()); - i++; - } - Console.WriteLine("]"); - } - public string! ListToString(IEnumerable xs){ - StringBuilder sb = new StringBuilder(); - sb.Append("["); - bool first = true; - foreach(T! x in xs){ - 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(); - Dictionary visited = new Dictionary(n); - int currentNumber = 1; - assume this.source != null; - this.PostOrderVisit(this.source, visited, ref currentNumber); - 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, Dictionary visited, ref int currentNumber){ - if (visited.ContainsKey(n)) return; - visited[n] = true; - foreach(Node! child in this.graph.Successors(n)){ - PostOrderVisit(child, visited, ref currentNumber); - } - assume this.postOrderNumberToNode != null; - assume this.nodeToPostOrderNumber != null; - this.postOrderNumberToNode[currentNumber].Val = n; - this.nodeToPostOrderNumber[n] = currentNumber; - currentNumber++; - return; - } -} -public class Graph { - private Set> es; - private Set ns; - private Node source; - private bool reducible; - private Set headers; - private Map> backEdgeNodes; - private Map,Set> naturalLoops; - private DomRelation? dominatorMap = null; - private Dictionary> predCache = new Dictionary>(); - private Dictionary> succCache = new Dictionary>(); - private bool predComputed; - - private class PreHeader { - Node! myHeader; - internal PreHeader(Node! h) { myHeader = h; } - - [Pure] - public override string! ToString() { return "#" + myHeader.ToString(); } - } - - public Graph(Set> edges) - { - es = edges; - - // original A# - //ns = Set{ x : in es } + Set{ y : in es }; - - // closest Spec# - //ns = new Set{ Pair p in edges; p.First } + new Set{ Pair p in edges; p.Second }; - - // - Set temp = new Set(); - foreach (Pair p in edges){ - temp.Add(p.First); - temp.Add(p.Second); - } - ns = temp; - } - public Graph() - { es = new Set>(); ns = new Set(); } - - // BUGBUG: Set.ToString() should return a non-null string - [Pure] - public override string! ToString() { return "" + es.ToString(); } - - public void AddSource(Node! x) - { - // BUGBUG: This generates bad code in the compiler - //ns += new Set{x}; - ns.Add(x); - source = x; - } - - public void AddEdge(Node! source, Node! dest) - { - //es += Set{}; - //ns += Set{source, dest}; - es.Add(new Pair(source,dest)); - ns.Add(source); - ns.Add(dest); - predComputed = false; - } - - public Set Nodes { get { return ns; } } - public IEnumerable> Edges { get { return es; } } - - public bool Edge(Node! x, Node! y) { - // original A# - // return in es; - return es.Contains(new Pair(x,y)); - } - - private void ComputePredSuccCaches() - { - if (predComputed) return; - predComputed = true; - predCache = new Dictionary>(); - succCache = new Dictionary>(); - - foreach (Node n in Nodes) { - predCache[n] = new Set(); - succCache[n] = new Set(); - } - - foreach(Pair p in Edges){ - Set tmp; - - tmp = predCache[p.Second]; - tmp.Add(p.First); - predCache[p.Second] = tmp; - - tmp = succCache[p.First]; - tmp.Add(p.Second); - succCache[p.First] = tmp; - } - } - - internal IEnumerable Predecessors(Node n) - { - // original A# - //Set result = Set{ x : x in Nodes, Edge(x,n) }; - - ComputePredSuccCaches(); - return predCache[n]; - } - - internal IEnumerable Successors(Node n) - { - ComputePredSuccCaches(); - return succCache[n]; - } - - internal DomRelation /*Map>*/ DominatorMap - { - get { - assert source != null; - if (this.dominatorMap == null){ - this.dominatorMap = new DomRelation(this, this.source); - } - return this.dominatorMap; - } - } - - public Dictionary> ImmediateDominatorMap - { - get { - assert source != null; - if (this.dominatorMap == null){ - this.dominatorMap = new DomRelation(this, this.source); - } - return this.dominatorMap.ImmediateDominatorMap; - } - } - public List ImmediatelyDominatedBy(Node! n) { - 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 (Pair e in this.Edges){ - Node! target = e.Second; - 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() - { - Pair> result = this.TopSort(); - return result.First ? result.Second : (IEnumerable)new Seq(); - } - // From AsmL distribution example - private Pair> TopSort() - { - Seq S = new Seq(); - Set V = this.Nodes; - Set X = new Set(); - foreach (Node! n in V){ X.Add(n); } - bool change = true; - while ( change ) - // invariant: X = V - S - { - change = false; - if (X.Count > 0){ - foreach (Node! n in X){ - // see if n has any incoming edges from any other node in X - bool inDegreeZero = true; - foreach(Node! u in X){ - 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 Pair>(false,new Seq()); - } - } - } - return new Pair>(true,S); - } - - public static bool Acyclic(Graph g, Node source) - { - bool acyclic; - List sortedList; - g.TarjanTopSort(out acyclic, out sortedList); - return acyclic; - } - - // - // [Dragon, pp. 670--671] - // returns map D s.t. d in D(n) iff d dom n - // - static private Map> OldComputeDominators(Graph g, Node! source){ - assert g.source != null; - Set N = g.Nodes; - Set nonSourceNodes = N - new Set(source); - Map> D = new Map>(); - D[source] = new Set(source); - foreach (Node! n in nonSourceNodes){ - D[n] = N; - } - bool change = true; - while ( change ){ - change = false; - foreach (Node! n in nonSourceNodes){ - - // original A# - //Set> allPreds = new Set>{ Node p in this.Predecessors(n) ; D[p] }; - - Set> allPreds = new Set>(); - foreach(Node! p in g.Predecessors(n)) allPreds.Add(D[p]); - Set temp = new Set(n) + Set.BigIntersect(allPreds); - if ( temp != D[n] ){ - change = true; - D[n] = temp; - } - } - } - return D; - } - - // [Dragon, Fig. 10.15, p. 604. Algorithm for constructing the natural loop.] - static Set NaturalLoop(Graph g, Pair backEdge) - { - Node! n = backEdge.First; - Node! d = backEdge.Second; - Seq stack = new Seq(); - Set loop = new Set(d); - if ( !n.Equals(d) ) // then n is not in loop - { - loop.Add(n); - stack = new Seq(n) + stack; // push n onto stack - } - while ( stack.Count > 0) // not empty - { - Node m = stack.Head; - stack = stack.Tail; // pop stack - foreach (Node! p in g.Predecessors(m)) - { - if ( !(loop.Contains(p)) ) - { - loop.Add(p); - stack = new Seq(p) + stack; // push p onto stack - } - } - } - return loop; - } - - internal struct ReducibleResult{ - internal bool reducible; - internal Set headers; - internal Map> backEdgeNodes; - internal Map,Set> naturalLoops; - internal ReducibleResult(bool b, - Set headers, - Map> backEdgeNodes, - Map,Set> naturalLoops){ - this.reducible = b; - this.headers = headers; - this.backEdgeNodes = backEdgeNodes; - this.naturalLoops = naturalLoops; - } - - } - - // [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); - } - - // [Dragon, p. 606] - static ReducibleResult ComputeReducible(Graph g, - Node source, - DomRelation! DomRelation) { - - //Console.WriteLine("[" + DateTime.Now +"]: begin ComputeReducible"); - IEnumerable> edges = g.Edges; - Set> backEdges = new Set>(); - Set> nonBackEdges = new Set>(); - foreach (Pair e in edges){ - Node x = e.First; - Node y = e.Second; // 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); - } - } - if ( !Acyclic(new Graph(nonBackEdges), source) ){ - return new ReducibleResult(false, - new Set(), - new Map>(), - new Map,Set>()); - }else{ - // original A#: - //Set headers = Set{ d : in backEdges }; - Set headers = new Set(); - foreach(Pair e in backEdges) - headers.Add(e.Second); - // original A#: - //Map> backEdgeNodes = Map{ h -> bs : h in headers, bs = Set{ b : in backEdges, x == h } }; - Map> backEdgeNodes = new Map>(); - foreach(Node! h in headers){ - Set bs = new Set(); - foreach(Pair backedge in backEdges){ - if (backedge.Second.Equals(h)){ - bs.Add(backedge.First); - } - } - backEdgeNodes.Add(h,bs); - } - - // original A#: - //Map,Set> naturalLoops = Map{ e -> NaturalLoop(g,e) : e in backEdges }; - Map,Set> naturalLoops = new Map,Set>(); - foreach (Pair e in backEdges){ - naturalLoops.Add(e,NaturalLoop(g,e)); - } - - //Console.WriteLine("[" + DateTime.Now +"]: end ComputeReducible"); - return new ReducibleResult(true, headers, backEdgeNodes, naturalLoops); - } - } - - public bool Reducible { get { return reducible; } } - public IEnumerable Headers { get { return headers; } } - public IEnumerable BackEdgeNodes(Node! h){ - // original A#: - //return h in backEdgeNodes ? backEdgeNodes[h] : null; - return (backEdgeNodes.ContainsKey(h) ? backEdgeNodes[h] : (IEnumerable)new Seq()); - } - public IEnumerable NaturalLoops(Node! header, Node! backEdgeNode) - { - Pair e = new Pair(backEdgeNode,header); - return naturalLoops.ContainsKey(e) ? naturalLoops[e] : (IEnumerable)new Seq(); - } - - 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; - return; - } - - -} // end: class Graph - -public class GraphProgram -{ - static void TestGraph(T! source, params Pair[] edges){ - Set> es = new Set>(); - foreach (Pair e in edges) 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 Pair(1,2), new Pair(1,3), new Pair(2,3) }); - - Console.WriteLine(""); - TestGraph('a', - new Pair('a','b'), - new Pair('a','c'), - new Pair('b','c') - ); - - Console.WriteLine(""); - TestGraph('a', - new Pair('a','b'), - new Pair('a','c'), - new Pair('b','d'), - new Pair('c','e'), - new Pair('c','f'), - new Pair('d','e'), - new Pair('e','d'), - new Pair('e','f'), - new Pair('f','e') - ); - - Console.WriteLine(""); - TestGraph('a', - new Pair('a','b'), - new Pair('a','c'), - new Pair('b','c'), - new Pair('c','b') - ); - - Console.WriteLine(""); - TestGraph(1, - new Pair(1,2), - new Pair(1,3), - new Pair(2,3) - ); - - Console.WriteLine(""); - TestGraph(1, - new Pair(1,2), - new Pair(1,3), - new Pair(2,3), - new Pair(3,2) - ); - - Console.WriteLine(""); - TestGraph(2, - new Pair(2,3), - new Pair(2,4), - new Pair(3,2) - ); - - Console.WriteLine(""); - TestGraph('a', - new Pair('a','b'), - new Pair('a','c'), - new Pair('b','c'), - new Pair('b','b') - ); - - - } -} - -} diff --git a/Source/Graph/Graph.sscproj b/Source/Graph/Graph.sscproj deleted file mode 100644 index e849b569..00000000 --- a/Source/Graph/Graph.sscproj +++ /dev/null @@ -1,93 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - \ No newline at end of file -- cgit v1.2.3