From 8d7686cd88736d117e37eb9bf9dd17404a294ff4 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 3 Oct 2012 12:32:19 -0700 Subject: bunch of refactorings - moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs --- Source/Graph/Graph.cs | 419 +++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 416 insertions(+), 3 deletions(-) (limited to 'Source/Graph') diff --git a/Source/Graph/Graph.cs b/Source/Graph/Graph.cs index 2d2eb90b..947a5882 100644 --- a/Source/Graph/Graph.cs +++ b/Source/Graph/Graph.cs @@ -3,11 +3,12 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved. // //----------------------------------------------------------------------------- -using System; +using System; +using System.Linq; using System.Collections.Generic; using System.Text; // for StringBuilder using System.Diagnostics.Contracts; -namespace Graphing { +namespace Microsoft.Boogie.GraphUtil { internal static class Util { private static string/*!*/ ListToString(IEnumerable xs) { @@ -873,7 +874,419 @@ namespace Graphing { s.AppendLine("}"); return s.ToString(); } - } // end: class Graph + } // end: class Graph + + public static class GraphAlgorithms + { + + public static Graph Dual(this Graph g, Node dummySource) + { + var exits = g.Nodes.Where(n => g.Successors(n).Count() == 0).ToList(); + if (exits.Count == 0) + return null; + var dual = new Graph(new HashSet>(g.Edges.Select(e => new Tuple(e.Item2, e.Item1)))); + if (exits.Count == 1) + dual.AddSource(exits[0]); + else + { + dual.AddSource(dummySource); + foreach (var exit in exits) + dual.AddEdge(dummySource, exit); + } + return dual; + } + + public static List> LoopyTopSort(this Graph g) + { + Contract.Assert(g.Reducible); + + int n = g.Nodes.Count; + var nodeToNumber = new Dictionary(n); + var numberToNode = new Node[n]; + var allNodes = new List(); + int counter = 0; + foreach (Node node in g.Nodes) + { + numberToNode[counter] = node; + nodeToNumber[node] = counter; + allNodes.Add(counter); + counter++; + } + + var loops = new List[n]; + foreach (var h in g.Headers) + { + var loopNodes = new HashSet(); + foreach (var b in g.BackEdgeNodes(h)) + loopNodes.UnionWith(g.NaturalLoops(h, b)); + loops[nodeToNumber[h]] = + new List(loopNodes.Select(node => nodeToNumber[node])); + } + + var successors = new List[n]; + int[] incomingEdges = new int[n]; + + foreach (var e in g.Edges) + { + Contract.Assert(e.Item1 != null); + Contract.Assert(e.Item2 != null); + int source = nodeToNumber[e.Item1], target = nodeToNumber[e.Item2]; + if (loops[target] == null || !loops[target].Contains(source)) + { + if (successors[source] == null) + successors[source] = new List(); + successors[source].Add(target); + incomingEdges[target]++; + } + } + + var sortedNodes = new List>(); + + var regionStack = new Stack>>(); + regionStack.Push(new Tuple>(default(Node), allNodes)); + + while (regionStack.Count != 0) + { + int rootIndex = -1; + foreach (var i in regionStack.Peek().Item2) + { + if (incomingEdges[i] == 0) + { + rootIndex = i; + break; + } + } + if (rootIndex == -1) + { + var region = regionStack.Pop(); + if (regionStack.Count != 0) + sortedNodes.Add(new Tuple(region.Item1, true)); + continue; + } + incomingEdges[rootIndex] = -1; + sortedNodes.Add(new Tuple(numberToNode[rootIndex], false)); + if (successors[rootIndex] != null) + foreach (int s in successors[rootIndex]) + incomingEdges[s]--; + if (loops[rootIndex] != null) + regionStack.Push(new Tuple>(numberToNode[rootIndex], + loops[rootIndex])); + } + + return sortedNodes; + } + + // Algorithm from Jeanne Ferrante, Karl J. Ottenstein, Joe D. Warren, + // "The Program Dependence Graph and Its Use in Optimization" + public static Dictionary> ControlDependence(this Graph g) where Node : class, new() + { + Graph dual = g.Dual(new Node()); + DomRelation pdom = dual.DominatorMap; + var result = new Dictionary>(); + + var S = g.Edges.Where(e => !pdom.DominatedBy(e.Item1, e.Item2)); + foreach (var edge in S) + { + var L = pdom.LeastCommonAncestor(edge.Item1, edge.Item2); + var deps = new List(); + if (L == edge.Item1) + { + pdom.DominatedBy(edge.Item2, edge.Item1, deps); + deps.Add(edge.Item2); + deps.Add(edge.Item1); + } + else + { + pdom.DominatedBy(edge.Item2, L, deps); + deps.Add(edge.Item2); + } + if (result.ContainsKey(edge.Item1)) + { + result[edge.Item1].UnionWith(deps); + } + else + { + result[edge.Item1] = new HashSet(deps); + } + } + return result; + } + + } + + public delegate System.Collections.IEnumerable/**//*!*/ Adjacency(T/*!*/ node); + + + // An SCC is a set of nodes + public sealed class SCC : ICollection + { + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(nodesMap != null); + } + + private IDictionary/*!*/ nodesMap = new Dictionary(); + private ICollection/*!*/ nodes + { + get + { + return cce.NonNull(nodesMap.Keys); + } + } + + [Pure] + [GlobalAccess(false)] + [Escapes(true, false)] + System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator() + { + Contract.Ensures(Contract.Result() != null); + + return ((System.Collections.IEnumerable)nodes).GetEnumerator(); + } + + [Pure] + [GlobalAccess(false)] + [Escapes(true, false)] + IEnumerator/*!*/ IEnumerable.GetEnumerator() + { + Contract.Ensures(Contract.Result>() != null); + + return ((IEnumerable)nodes).GetEnumerator(); + } + + public int Count + { + get + { + return nodes.Count; + } + } + public bool IsReadOnly + { + get + { + return nodesMap.IsReadOnly; + } + } + public void Add(Node item) + { + nodesMap.Add(item, null); + } + public void Clear() + { + nodesMap.Clear(); + } + [Pure] + public bool Contains(Node item) + { + return nodesMap.ContainsKey(item); + } + public void CopyTo(Node[] array, int arrayIndex) + { + //Contract.Requires(array != null); + nodes.CopyTo(array, arrayIndex); + } + public bool Remove(Node item) + { + return nodesMap.Remove(item); + } + } + + public sealed class StronglyConnectedComponents : IEnumerable/*!*/> where Node : class + { + private readonly IDictionary/*!*/ graph; + [ContractInvariantMethod] + void graphInvariantMethod() + { + Contract.Invariant(Contract.ForAll(graph, entry => entry.Key != null)); + Contract.Invariant(preds != null); + Contract.Invariant(succs != null); + } + private readonly Adjacency/*!*/ preds; + private readonly Adjacency/*!*/ succs; + + private bool computed = false; + public bool Computed + { + get + { + return computed; + } + } + + [NotDelayed] + public StronglyConnectedComponents(System.Collections.IEnumerable/**/ graph, Adjacency preds, Adjacency succs) + : base() + {//BASEMOVE DANGER + Contract.Requires(succs != null); + Contract.Requires(preds != null); + Contract.Requires(graph != null); + Contract.Ensures(!Computed); + IDictionary/*!*/ dict = new Dictionary(); + foreach (Node/*!*/ n in graph) + { + Contract.Assert(n != null); + dict.Add(n, null); + } + + this.graph = dict; + this.preds = preds; + this.succs = succs; + //:base(); + } + + [Pure] + [GlobalAccess(false)] + [Escapes(true, false)] + System.Collections.IEnumerator/*!*/ System.Collections.IEnumerable.GetEnumerator() + { + Contract.Ensures(Contract.Result() != null); + + return ((System.Collections.IEnumerable)sccs).GetEnumerator(); + } + + [Pure] + [GlobalAccess(false)] + [Escapes(true, false)] + IEnumerator/*!*/>/*!*/ IEnumerable/*!*/>.GetEnumerator() + { + Contract.Ensures(Contract.Result>>() != null); + + Contract.Assume(Computed); + Contract.Assert(cce.NonNullElements((IEnumerable/*!*/>)sccs));//REVIEW + return ((IEnumerable/*!*/>)sccs).GetEnumerator(); + } + + private readonly IList/*!*/>/*!*/ sccs = new List/*!*/>(); + [ContractInvariantMethod] + void sccsInvariant() + { + Contract.Invariant(cce.NonNullElements(sccs)); + } + + + public void Compute() + { + Contract.Requires(!Computed); + Contract.Ensures(Computed); + // Compute post times on graph with edges reversed + this.dfsNext = this.preds; + foreach (Node/*!*/ n in cce.NonNull(graph.Keys)) + { + Contract.Assert(n != null); + if (!seen.ContainsKey(n)) + { + OrderNodes(n); + } + } + + // Clear seen + seen.Clear(); + + // Compute SCCs + this.dfsNext = this.succs; + while (postOrder.Count > 0) + { + Node/*!*/ n = postOrder.Pop(); + Contract.Assert(n != null); + + if (!seen.ContainsKey(n)) + { + SCC/*!*/ curr = new SCC(); + FindSCCs(n, curr); + sccs.Add(curr); + } + } + + // Clear seen + seen.Clear(); + + this.computed = true; + } + + private Adjacency/*?*/ dfsNext = null; + + private readonly IDictionary/*!*/ seen = new Dictionary(); + private readonly Stack/*!*/ postOrder = new Stack(); + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(seen != null); + Contract.Invariant(cce.NonNullElements(postOrder)); + } + + + // DFS to order nodes by post times + private void OrderNodes(Node node) + { + Contract.Requires(node != null); + seen.Add(node, null); + + Contract.Assert(dfsNext != null); + System.Collections.IEnumerable/*!*/ nexts = dfsNext(node); + Contract.Assert(nexts != null); + foreach (Node/*!*/ n in nexts) + { + Contract.Assert(n != null); + if (graph.ContainsKey(n) && !seen.ContainsKey(n)) + { + OrderNodes(n); + } + } + + postOrder.Push(node); + } + + // DFS to compute SCCs + private void FindSCCs(Node node, SCC currSCC) + { + Contract.Requires(currSCC != null); + Contract.Requires(node != null); + //modifies currSCC.*; + seen.Add(node, null); + currSCC.Add(node); + + Contract.Assert(dfsNext != null); + System.Collections.IEnumerable/*!*/ nexts = dfsNext(node); + Contract.Assert(nexts != null); + foreach (Node/*!*/ n in nexts) + { + Contract.Assert(n != null); + if (graph.ContainsKey(n) && !seen.ContainsKey(n)) + { + FindSCCs(n, currSCC); + } + } + } + + [Pure] + public override string ToString() + { + Contract.Ensures(Contract.Result() != null); + string outStr = ""; + int i = 0; + + foreach (ICollection component in this) + { + string/*!*/ tmp = System.String.Format("\nComponent #{0} = ", i++); + Contract.Assert(tmp != null); + outStr += tmp; + + bool firstInRow = true; + + foreach (Node b in component) + { + string/*!*/ tmpComponent = System.String.Format("{0}{1}", firstInRow ? "" : ", ", b); + Contract.Assert(tmpComponent != null); + outStr += tmpComponent; + firstInRow = false; + } + } + return outStr; + } + + } public class GraphProgram { static void TestGraph(T/*!*/ source, params Tuple[] edges) { -- cgit v1.2.3