From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Core/InterProceduralReachabilityGraph.cs | 612 ++++++++++++------------ 1 file changed, 306 insertions(+), 306 deletions(-) (limited to 'Source/Core/InterProceduralReachabilityGraph.cs') diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs index d75a4b7d..73c88bca 100644 --- a/Source/Core/InterProceduralReachabilityGraph.cs +++ b/Source/Core/InterProceduralReachabilityGraph.cs @@ -1,306 +1,306 @@ - -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using System.Diagnostics; -using Microsoft.Boogie.GraphUtil; - -namespace Microsoft.Boogie -{ - - public interface IInterproceduralReachabilityGraph { - - bool MayReach(Block src, Block dst); - - void dump(); - - Block GetNewEntryBlock(string p); - - Block GetNewExitBlock(string p); - - Block GetNewBlock(Block block); - } - - public class InterproceduralReachabilityGraph : IInterproceduralReachabilityGraph - { - - private Program prog; - private HashSet nodes; - private Dictionary originalToNew; - private Dictionary newProcedureEntryNodes; - private Dictionary newProcedureExitNodes; - - private Graph reachabilityGraph; - - public InterproceduralReachabilityGraph(Program prog) { - this.prog = prog; - originalToNew = new Dictionary(); - newProcedureEntryNodes = new Dictionary(); - newProcedureExitNodes = new Dictionary(); - nodes = new HashSet(); - - ProcessImplementations(); - - ProcessBodilessProcedures(); - - PatchUpGotoTargets(); - - AddCallAndReturnEdges(); - - reachabilityGraph = new Graph(); - - foreach(var n in nodes) { - GotoCmd gotoCmd = n.TransferCmd as GotoCmd; - if(gotoCmd != null) { - foreach(Block b in gotoCmd.labelTargets) { - reachabilityGraph.AddEdge(n, b); - } - } - } - - foreach(var n in nodes) { - // If there are disconnected nodes, put them into the - // graph as self-loops so that every node is represented in - // the graph - if(!reachabilityGraph.Nodes.Contains(n)) { - reachabilityGraph.AddEdge(n, n); - } - } - } - - private IEnumerable OriginalProgramBlocks() - { - return prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item); - } - - private void AddCallAndReturnEdges() - { - #region Add call and return edges - foreach (var n in nodes) - { - if (n.Cmds.Count == 1 && n.Cmds[0] is CallCmd) - { - string proc = ((CallCmd)n.Cmds[0]).callee; - GotoCmd gotoCmd = n.TransferCmd as GotoCmd; - Debug.Assert(gotoCmd != null); - - for (int i = 0; i < gotoCmd.labelTargets.Count; i++) - { - (newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelTargets.Add(gotoCmd.labelTargets[i]); - (newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelNames.Add(gotoCmd.labelNames[i]); - } - gotoCmd.labelTargets = new List { newProcedureEntryNodes[proc] }; - gotoCmd.labelNames = new List { newProcedureEntryNodes[proc].Label }; - } - } - #endregion - } - - private void PatchUpGotoTargets() - { - #region Patch up goto targets - foreach (var n in nodes) - { - var gotoCmd = n.TransferCmd as GotoCmd; - if (gotoCmd != null) - { - List newTargets = new List(); - foreach (Block t in gotoCmd.labelTargets) - { - if (originalToNew.ContainsKey(t)) - { - newTargets.Add(originalToNew[t]); - } - else - { - newTargets.Add(t); - } - } - gotoCmd.labelTargets = newTargets; - } - } - #endregion - } - - private void ProcessBodilessProcedures() - { - #region Add single node CFG for procedures with no body - foreach (var proc in prog.Procedures) - { - if (!newProcedureEntryNodes.ContainsKey(proc.Name)) - { - Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new List(), new GotoCmd(Token.NoToken, new List())); - nodes.Add(newBlock); - newProcedureEntryNodes[proc.Name] = newBlock; - newProcedureExitNodes[proc.Name] = newBlock; - } - } - #endregion - } - - private void ProcessImplementations() - { - #region Transform implementation CFGs so that every call is in its own basic block - foreach (var impl in prog.Implementations) - { - string exitLabel = "__" + impl.Name + "_newExit"; - Block newExit = new Block(Token.NoToken, exitLabel, new List(), new GotoCmd(Token.NoToken, new List())); - nodes.Add(newExit); - newProcedureExitNodes[impl.Name] = newExit; - foreach (Block b in impl.Blocks) - { - Block prev = null; - int i = 0; - foreach (List cmds in SeparateCallCmds(b.Cmds)) - { - Block newBlock; - if (prev == null) - { - newBlock = new Block(b.tok, "__" + impl.Name + "_" + b.Label, new List(cmds.ToArray()), null); - nodes.Add(newBlock); - originalToNew[b] = newBlock; - if (impl.Blocks[0] == b) - { - newProcedureEntryNodes[impl.Name] = newBlock; - } - } - else - { - string label = "__" + impl.Name + "_" + b.Label + "_call_" + i; - newBlock = new Block(b.tok, label, new List(cmds.ToArray()), null); - nodes.Add(newBlock); - originalToNew[newBlock] = newBlock; - prev.TransferCmd = new GotoCmd(Token.NoToken, new List { label }, new List { newBlock }); - } - prev = newBlock; - i++; - } - Debug.Assert(prev != null); - if (b.TransferCmd is ReturnCmd || (b.TransferCmd is GotoCmd && - ((GotoCmd)b.TransferCmd).labelTargets.Count == 0)) - { - prev.TransferCmd = new GotoCmd(Token.NoToken, new List { exitLabel }, new List { newExit }); - } - else - { - if(b.TransferCmd is ReturnCmd) { - prev.TransferCmd = new ReturnCmd(b.TransferCmd.tok); - } else { - var gotoCmd = b.TransferCmd as GotoCmd; - Debug.Assert(gotoCmd != null); - prev.TransferCmd = new GotoCmd(gotoCmd.tok, gotoCmd.labelNames, gotoCmd.labelTargets); - } - } - } - } - #endregion - } - - private static List> SeparateCallCmds(List Cmds) { - List> result = new List>(); - int currentIndex = 0; - while(currentIndex < Cmds.Count) { - if(Cmds[currentIndex] is CallCmd) { - result.Add(new List { Cmds[currentIndex] }); - currentIndex++; - } else { - List nonCallCmds = new List(); - while(currentIndex < Cmds.Count && !(Cmds[currentIndex] is CallCmd)) { - nonCallCmds.Add(Cmds[currentIndex]); - currentIndex++; - } - result.Add(nonCallCmds); - } - } - if(result.Count == 0) { - result.Add(new List()); - } - return result; - } - - private Graph> ReachabilityGraphSCCsDAG; - private Dictionary> BlockToSCC; - - private Dictionary, HashSet> MayReachCache = new Dictionary, HashSet>(); - - public bool MayReach(Block src, Block dst) { - if (ReachabilityGraphSCCsDAG == null) { - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Interprocedural reachability: computing SCCs"); - } - Adjacency next = new Adjacency(reachabilityGraph.Successors); - Adjacency prev = new Adjacency(reachabilityGraph.Predecessors); - StronglyConnectedComponents ReachabilitySCCs = new StronglyConnectedComponents( - reachabilityGraph.Nodes, next, prev); - ReachabilitySCCs.Compute(); - - BlockToSCC = new Dictionary>(); - foreach (var scc in ReachabilitySCCs) { - foreach (var s in scc) { - BlockToSCC[s] = scc; - } - } - - ReachabilityGraphSCCsDAG = new Graph>(); - foreach (var edge in reachabilityGraph.Edges) { - if (BlockToSCC[edge.Item1] != BlockToSCC[edge.Item2]) { - ReachabilityGraphSCCsDAG.AddEdge(BlockToSCC[edge.Item1], BlockToSCC[edge.Item2]); - } - } - - SCC dummy = new SCC(); - foreach (var n in reachabilityGraph.Nodes) { - ReachabilityGraphSCCsDAG.AddEdge(BlockToSCC[n], dummy); - } - - if (CommandLineOptions.Clo.Trace) { - Console.WriteLine("Interprocedural reachability: SCCs computed!"); - } - } - return ReachableFrom(BlockToSCC[src]).Contains(dst); - } - - private HashSet ReachableFrom(SCC scc) { - if (!MayReachCache.ContainsKey(scc)) { - HashSet result = new HashSet(); - if (scc.Count() > 0) { - result.UnionWith(scc); - foreach (var nextSCC in ReachabilityGraphSCCsDAG.Successors(scc)) { - result.UnionWith(ReachableFrom(nextSCC)); - } - } - MayReachCache[scc] = result; - } - return MayReachCache[scc]; - } - - public void dump() { - foreach(var n in nodes) { - Console.WriteLine(n.Label + " -> {"); - GotoCmd gotoCmd = n.TransferCmd as GotoCmd; - if(n != null) { - foreach(Block m in gotoCmd.labelTargets) { - Console.WriteLine(" " + m.Label); - } - } - Console.WriteLine("}"); - } - } - - public Block GetNewEntryBlock(string proc) { - return newProcedureEntryNodes[proc]; - } - - public Block GetNewExitBlock(string proc) { - return newProcedureExitNodes[proc]; - } - - public Block GetNewBlock(Block b) { - return originalToNew[b]; - } - - } - - -} + +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Diagnostics; +using Microsoft.Boogie.GraphUtil; + +namespace Microsoft.Boogie +{ + + public interface IInterproceduralReachabilityGraph { + + bool MayReach(Block src, Block dst); + + void dump(); + + Block GetNewEntryBlock(string p); + + Block GetNewExitBlock(string p); + + Block GetNewBlock(Block block); + } + + public class InterproceduralReachabilityGraph : IInterproceduralReachabilityGraph + { + + private Program prog; + private HashSet nodes; + private Dictionary originalToNew; + private Dictionary newProcedureEntryNodes; + private Dictionary newProcedureExitNodes; + + private Graph reachabilityGraph; + + public InterproceduralReachabilityGraph(Program prog) { + this.prog = prog; + originalToNew = new Dictionary(); + newProcedureEntryNodes = new Dictionary(); + newProcedureExitNodes = new Dictionary(); + nodes = new HashSet(); + + ProcessImplementations(); + + ProcessBodilessProcedures(); + + PatchUpGotoTargets(); + + AddCallAndReturnEdges(); + + reachabilityGraph = new Graph(); + + foreach(var n in nodes) { + GotoCmd gotoCmd = n.TransferCmd as GotoCmd; + if(gotoCmd != null) { + foreach(Block b in gotoCmd.labelTargets) { + reachabilityGraph.AddEdge(n, b); + } + } + } + + foreach(var n in nodes) { + // If there are disconnected nodes, put them into the + // graph as self-loops so that every node is represented in + // the graph + if(!reachabilityGraph.Nodes.Contains(n)) { + reachabilityGraph.AddEdge(n, n); + } + } + } + + private IEnumerable OriginalProgramBlocks() + { + return prog.Implementations.Select(Item => Item.Blocks).SelectMany(Item => Item); + } + + private void AddCallAndReturnEdges() + { + #region Add call and return edges + foreach (var n in nodes) + { + if (n.Cmds.Count == 1 && n.Cmds[0] is CallCmd) + { + string proc = ((CallCmd)n.Cmds[0]).callee; + GotoCmd gotoCmd = n.TransferCmd as GotoCmd; + Debug.Assert(gotoCmd != null); + + for (int i = 0; i < gotoCmd.labelTargets.Count; i++) + { + (newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelTargets.Add(gotoCmd.labelTargets[i]); + (newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelNames.Add(gotoCmd.labelNames[i]); + } + gotoCmd.labelTargets = new List { newProcedureEntryNodes[proc] }; + gotoCmd.labelNames = new List { newProcedureEntryNodes[proc].Label }; + } + } + #endregion + } + + private void PatchUpGotoTargets() + { + #region Patch up goto targets + foreach (var n in nodes) + { + var gotoCmd = n.TransferCmd as GotoCmd; + if (gotoCmd != null) + { + List newTargets = new List(); + foreach (Block t in gotoCmd.labelTargets) + { + if (originalToNew.ContainsKey(t)) + { + newTargets.Add(originalToNew[t]); + } + else + { + newTargets.Add(t); + } + } + gotoCmd.labelTargets = newTargets; + } + } + #endregion + } + + private void ProcessBodilessProcedures() + { + #region Add single node CFG for procedures with no body + foreach (var proc in prog.Procedures) + { + if (!newProcedureEntryNodes.ContainsKey(proc.Name)) + { + Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new List(), new GotoCmd(Token.NoToken, new List())); + nodes.Add(newBlock); + newProcedureEntryNodes[proc.Name] = newBlock; + newProcedureExitNodes[proc.Name] = newBlock; + } + } + #endregion + } + + private void ProcessImplementations() + { + #region Transform implementation CFGs so that every call is in its own basic block + foreach (var impl in prog.Implementations) + { + string exitLabel = "__" + impl.Name + "_newExit"; + Block newExit = new Block(Token.NoToken, exitLabel, new List(), new GotoCmd(Token.NoToken, new List())); + nodes.Add(newExit); + newProcedureExitNodes[impl.Name] = newExit; + foreach (Block b in impl.Blocks) + { + Block prev = null; + int i = 0; + foreach (List cmds in SeparateCallCmds(b.Cmds)) + { + Block newBlock; + if (prev == null) + { + newBlock = new Block(b.tok, "__" + impl.Name + "_" + b.Label, new List(cmds.ToArray()), null); + nodes.Add(newBlock); + originalToNew[b] = newBlock; + if (impl.Blocks[0] == b) + { + newProcedureEntryNodes[impl.Name] = newBlock; + } + } + else + { + string label = "__" + impl.Name + "_" + b.Label + "_call_" + i; + newBlock = new Block(b.tok, label, new List(cmds.ToArray()), null); + nodes.Add(newBlock); + originalToNew[newBlock] = newBlock; + prev.TransferCmd = new GotoCmd(Token.NoToken, new List { label }, new List { newBlock }); + } + prev = newBlock; + i++; + } + Debug.Assert(prev != null); + if (b.TransferCmd is ReturnCmd || (b.TransferCmd is GotoCmd && + ((GotoCmd)b.TransferCmd).labelTargets.Count == 0)) + { + prev.TransferCmd = new GotoCmd(Token.NoToken, new List { exitLabel }, new List { newExit }); + } + else + { + if(b.TransferCmd is ReturnCmd) { + prev.TransferCmd = new ReturnCmd(b.TransferCmd.tok); + } else { + var gotoCmd = b.TransferCmd as GotoCmd; + Debug.Assert(gotoCmd != null); + prev.TransferCmd = new GotoCmd(gotoCmd.tok, gotoCmd.labelNames, gotoCmd.labelTargets); + } + } + } + } + #endregion + } + + private static List> SeparateCallCmds(List Cmds) { + List> result = new List>(); + int currentIndex = 0; + while(currentIndex < Cmds.Count) { + if(Cmds[currentIndex] is CallCmd) { + result.Add(new List { Cmds[currentIndex] }); + currentIndex++; + } else { + List nonCallCmds = new List(); + while(currentIndex < Cmds.Count && !(Cmds[currentIndex] is CallCmd)) { + nonCallCmds.Add(Cmds[currentIndex]); + currentIndex++; + } + result.Add(nonCallCmds); + } + } + if(result.Count == 0) { + result.Add(new List()); + } + return result; + } + + private Graph> ReachabilityGraphSCCsDAG; + private Dictionary> BlockToSCC; + + private Dictionary, HashSet> MayReachCache = new Dictionary, HashSet>(); + + public bool MayReach(Block src, Block dst) { + if (ReachabilityGraphSCCsDAG == null) { + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Interprocedural reachability: computing SCCs"); + } + Adjacency next = new Adjacency(reachabilityGraph.Successors); + Adjacency prev = new Adjacency(reachabilityGraph.Predecessors); + StronglyConnectedComponents ReachabilitySCCs = new StronglyConnectedComponents( + reachabilityGraph.Nodes, next, prev); + ReachabilitySCCs.Compute(); + + BlockToSCC = new Dictionary>(); + foreach (var scc in ReachabilitySCCs) { + foreach (var s in scc) { + BlockToSCC[s] = scc; + } + } + + ReachabilityGraphSCCsDAG = new Graph>(); + foreach (var edge in reachabilityGraph.Edges) { + if (BlockToSCC[edge.Item1] != BlockToSCC[edge.Item2]) { + ReachabilityGraphSCCsDAG.AddEdge(BlockToSCC[edge.Item1], BlockToSCC[edge.Item2]); + } + } + + SCC dummy = new SCC(); + foreach (var n in reachabilityGraph.Nodes) { + ReachabilityGraphSCCsDAG.AddEdge(BlockToSCC[n], dummy); + } + + if (CommandLineOptions.Clo.Trace) { + Console.WriteLine("Interprocedural reachability: SCCs computed!"); + } + } + return ReachableFrom(BlockToSCC[src]).Contains(dst); + } + + private HashSet ReachableFrom(SCC scc) { + if (!MayReachCache.ContainsKey(scc)) { + HashSet result = new HashSet(); + if (scc.Count() > 0) { + result.UnionWith(scc); + foreach (var nextSCC in ReachabilityGraphSCCsDAG.Successors(scc)) { + result.UnionWith(ReachableFrom(nextSCC)); + } + } + MayReachCache[scc] = result; + } + return MayReachCache[scc]; + } + + public void dump() { + foreach(var n in nodes) { + Console.WriteLine(n.Label + " -> {"); + GotoCmd gotoCmd = n.TransferCmd as GotoCmd; + if(n != null) { + foreach(Block m in gotoCmd.labelTargets) { + Console.WriteLine(" " + m.Label); + } + } + Console.WriteLine("}"); + } + } + + public Block GetNewEntryBlock(string proc) { + return newProcedureEntryNodes[proc]; + } + + public Block GetNewExitBlock(string proc) { + return newProcedureExitNodes[proc]; + } + + public Block GetNewBlock(Block b) { + return originalToNew[b]; + } + + } + + +} -- cgit v1.2.3