From 3b0b6a95957a01969a85ab0b3e98de350247e0c6 Mon Sep 17 00:00:00 2001 From: allydonaldson Date: Wed, 29 May 2013 08:02:16 +0100 Subject: Improvements to Staged Houdini --- Source/Core/CommandLineOptions.cs | 8 + Source/Core/Core.csproj | 1 + Source/Core/InterProceduralReachabilityGraph.cs | 291 ++++++++++++++++++++++++ Source/Houdini/CandidateDependenceAnalyser.cs | 288 ++++++++++------------- 4 files changed, 420 insertions(+), 168 deletions(-) create mode 100644 Source/Core/InterProceduralReachabilityGraph.cs (limited to 'Source') diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 2d78e677..0bb5e6de 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -397,6 +397,7 @@ namespace Microsoft.Boogie { public bool HoudiniUseCrossDependencies = false; public int StagedHoudini = 0; public bool DebugStagedHoudini = false; + public bool StagedHoudiniReachabilityAnalysis = false; public string VariableDependenceIgnore = null; public string AbstractHoudini = null; public bool UseUnsatCoreForContractInfer = false; @@ -891,6 +892,13 @@ namespace Microsoft.Boogie { return true; } + case "stagedHoudiniReachabilityAnalysis": { + if (ps.ConfirmArgumentCount(0)) { + StagedHoudiniReachabilityAnalysis = true; + } + return true; + } + case "debugStagedHoudini": { if (ps.ConfirmArgumentCount(0)) { DebugStagedHoudini = true; diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index e6db6e9d..d41fb40b 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -152,6 +152,7 @@ + diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs new file mode 100644 index 00000000..0c026757 --- /dev/null +++ b/Source/Core/InterProceduralReachabilityGraph.cs @@ -0,0 +1,291 @@ + +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); + } + } + } + + } + + private IEnumerable OriginalProgramBlocks() + { + return prog.TopLevelDeclarations.OfType().Select(Item => Item.Blocks).SelectMany(Item => Item); + } + + private void AddCallAndReturnEdges() + { + #region Add call and return edges + foreach (var n in nodes) + { + if (n.Cmds.Length == 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.Length; i++) + { + (newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelTargets.Add(gotoCmd.labelTargets[i]); + (newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelNames.Add(gotoCmd.labelNames[i]); + } + gotoCmd.labelTargets = new BlockSeq { newProcedureEntryNodes[proc] }; + gotoCmd.labelNames = new StringSeq { 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) + { + BlockSeq newTargets = new BlockSeq(); + 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.TopLevelDeclarations.OfType()) + { + if (!newProcedureEntryNodes.ContainsKey(proc.Name)) + { + Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new CmdSeq(), new GotoCmd(Token.NoToken, new BlockSeq())); + 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.TopLevelDeclarations.OfType()) + { + string exitLabel = "__" + impl.Name + "_newExit"; + Block newExit = new Block(Token.NoToken, exitLabel, new CmdSeq(), new GotoCmd(Token.NoToken, new BlockSeq())); + nodes.Add(newExit); + newProcedureExitNodes[impl.Name] = newExit; + foreach (Block b in impl.Blocks) + { + List> partition = PartitionCmds(b.Cmds); + Block prev = null; + int i = 0; + foreach (List cmds in partition) + { + Block newBlock; + if (prev == null) + { + newBlock = new Block(b.tok, "__" + impl.Name + "_" + b.Label, new CmdSeq(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 CmdSeq(cmds.ToArray()), null); + nodes.Add(newBlock); + originalToNew[newBlock] = newBlock; + prev.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq { label }, new BlockSeq { newBlock }); + } + prev = newBlock; + i++; + } + Debug.Assert(prev != null); + if (b.TransferCmd is ReturnCmd || (b.TransferCmd is GotoCmd && + ((GotoCmd)b.TransferCmd).labelTargets.Length == 0)) + { + prev.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq { exitLabel }, new BlockSeq { 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 List> PartitionCmds(CmdSeq cmds) { + List> result = new List>(); + List current = new List(); + result.Add(current); + foreach(Cmd cmd in cmds) { + if(cmd is CallCmd && current.Count > 0) { + current = new List(); + result.Add(current); + } + current.Add(cmd); + } + 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]; + } + + } + + +} diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs index 96b52fa9..f00514cf 100644 --- a/Source/Houdini/CandidateDependenceAnalyser.cs +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -37,8 +37,6 @@ namespace Microsoft.Boogie { DetermineCandidateVariableDependences(); - //ConstructCandidateReachabilityGraph(); - ConstructCandidateDependenceGraph(); ConstructStagesDAG(); @@ -96,6 +94,14 @@ namespace Microsoft.Boogie { Console.WriteLine("Candidate dependence analysis: Building dependence graph"); } + ICandidateReachabilityChecker reachabilityChecker; + + if(CommandLineOptions.Clo.StagedHoudiniReachabilityAnalysis) { + reachabilityChecker = new CandidateReachabilityChecker(prog, candidates); + } else { + reachabilityChecker = new DummyCandidateReachabilityChecker(); + } + CandidateDependences = new Graph(); foreach (var c in candidates) { @@ -106,7 +112,7 @@ namespace Microsoft.Boogie { { foreach (var d in variableDirectlyReferredToByCandidates[vd]) { - if (MayReach(c, d)) + if(reachabilityChecker.MayReach(d, c)) { CandidateDependences.AddEdge(c, d); } @@ -116,172 +122,7 @@ namespace Microsoft.Boogie { } } - private void ConstructCandidateReachabilityGraph() - { - Dictionary> procedureCFGs = new Dictionary>(); - Dictionary> candidateToUse = new Dictionary>(); - - #region Prepare implementations - foreach (var impl in prog.TopLevelDeclarations.OfType()) { - procedureCFGs[impl.Name] = PrepareImplementationForCandidateReachability(impl); - } - #endregion - - #region Prepare any procedures that do not have implementations - foreach (var proc in prog.TopLevelDeclarations.OfType()) { - if(!procedureCFGs.ContainsKey(proc.Name)) { - procedureCFGs[proc.Name] = PrepareProcedureForCandidateReachability(proc); - } - } - #endregion - - #region Transform prepared CFGs so that every call is in its own basic block - foreach(var proc in procedureCFGs.Keys) { - List newCFG = new List(); - Dictionary oldToNew = new Dictionary(); - - foreach(var bb in procedureCFGs[proc]) { - List> partition = new List>(); - List current = new List(); - partition.Add(current); - foreach(Cmd cmd in bb.Cmds) { - if(cmd is CallCmd && current.Count > 0) { - current = new List(); - partition.Add(current); - } - current.Add(cmd); - } - - if(partition.Count > 1) { - Block last = null; - int i = 0; - foreach(var cmdList in partition) { - Block newBB = new Block(bb.tok, bb.Label + "_" + i, new CmdSeq(cmdList.ToArray()), null); - newCFG.Add(newBB); - if(last == null) { - oldToNew[bb] = newBB; - } else { - oldToNew[newBB] = newBB; - last.TransferCmd = new GotoCmd(last.tok, new BlockSeq { newBB }); - } - last = newBB; - i++; - } - Debug.Assert(last != null); - Debug.Assert(last.TransferCmd == null); - last.TransferCmd = bb.TransferCmd; - } else { - newCFG.Add(bb); - oldToNew[bb] = bb; - } - - } - - ApplyPatchupMap(newCFG, oldToNew); - procedureCFGs[proc] = newCFG; - - } - #endregion - - #region Replace calls with inter-procedural edges - foreach(var bb in procedureCFGs.Values.SelectMany(Item => Item)) { - if(bb.Cmds.Length == 1 && bb.Cmds[0] is CallCmd) { - Debug.Assert(bb.TransferCmd is GotoCmd); - string proc = (bb.Cmds[0] as CallCmd).callee; - - Block returnBB = procedureCFGs[proc].Last(); - if(returnBB.TransferCmd is ReturnCmd) { - returnBB.TransferCmd = bb.TransferCmd; - } else { - Debug.Assert(returnBB.TransferCmd is GotoCmd); - GotoCmd gotoCmd = returnBB.TransferCmd as GotoCmd; - gotoCmd.labelTargets.AddRange(((GotoCmd)bb.TransferCmd).labelTargets); - } - - Block entryBB = procedureCFGs[proc].First(); - bb.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq { entryBB }); - } - } - #endregion - - throw new NotImplementedException(); - - } - - private static List PrepareProcedureForCandidateReachability(Procedure proc) - { - Block ensuresBlock = new Block(proc.tok, "postconditions", - EnsuresToAssertSequence(proc.Ensures), - new ReturnCmd(Token.NoToken)); - Block requiresBlock = new Block(proc.tok, "preconditions", - RequiresToAssertSequence(proc.Requires), - new GotoCmd(Token.NoToken, new BlockSeq { ensuresBlock })); - return new List { requiresBlock, ensuresBlock }; - } - - private static List PrepareImplementationForCandidateReachability(Implementation impl) - { - // Clone the BBs and keep patchup map - List newBBs = new List(); - Dictionary oldToNew = new Dictionary(); - foreach (var bb in impl.Blocks) - { - Block newBB = new Block(bb.tok, bb.Label, bb.Cmds, bb.TransferCmd); - oldToNew[bb] = newBB; - newBBs.Add(newBB); - } - ApplyPatchupMap(newBBs, oldToNew); - Block newEntry = new Block(Token.NoToken, "preconditions", - RequiresToAssertSequence(impl.Proc.Requires), - new GotoCmd(Token.NoToken, new BlockSeq { newBBs[0] })); - - Block newExit = new Block(Token.NoToken, "postconditions", - EnsuresToAssertSequence(impl.Proc.Ensures), - new ReturnCmd(Token.NoToken)); - - foreach (var newBB in newBBs) - { - if (newBB.TransferCmd is ReturnCmd || - (newBB.TransferCmd is GotoCmd && ((GotoCmd)newBB.TransferCmd).labelTargets.Length == 0)) - { - newBB.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq { newExit }); - } - } - - newBBs.Insert(0, newEntry); - newBBs.Add(newExit); - return newBBs; - } - - private static void ApplyPatchupMap(List newBBs, Dictionary oldToNew) - { - foreach (var newBB in newBBs) - { - GotoCmd gotoCmd = newBB.TransferCmd as GotoCmd; - if (gotoCmd != null) - { - gotoCmd.labelTargets = new BlockSeq(((Block[])gotoCmd.labelTargets.ToArray()). - Select(Item => oldToNew[Item]).ToArray()); - } - } - } - - private static CmdSeq RequiresToAssertSequence(RequiresSeq Requires) - { - return new CmdSeq(((Requires[])Requires.ToArray()).Select( - Item => new AssertCmd(Item.tok, Item.Condition)).ToArray()); - } - - private static CmdSeq EnsuresToAssertSequence(EnsuresSeq Ensures) - { - return new CmdSeq(((Ensures[])Ensures.ToArray()).Select( - Item => new AssertCmd(Item.tok, Item.Condition)).ToArray()); - } - private bool MayReach(string c, string d) - { - return true; - } private void DetermineCandidateVariableDependences() { @@ -669,4 +510,115 @@ namespace Microsoft.Boogie { } } + interface ICandidateReachabilityChecker { + bool MayReach(string c, string d); + } + + class DummyCandidateReachabilityChecker : ICandidateReachabilityChecker { + public bool MayReach(string c, string d) { + return true; + } + } + + class CandidateReachabilityChecker : ICandidateReachabilityChecker { + + private enum PrePost { + PRE, POST + } + + private Program prog; + private IEnumerable candidates; + private IInterproceduralReachabilityGraph reachabilityGraph; + private Dictionary> candidateToOccurences; + + internal CandidateReachabilityChecker(Program prog, IEnumerable candidates) { + this.prog = prog; + this.candidates = candidates; + this.reachabilityGraph = new InterproceduralReachabilityGraph(prog); + this.candidateToOccurences = new Dictionary>(); + + // Add all candidate occurrences in blocks + foreach(Block b in prog.TopLevelDeclarations.OfType().Select(Item => Item.Blocks).SelectMany(Item => Item)) { + foreach(Cmd cmd in b.Cmds) { + AssertCmd assertCmd = cmd as AssertCmd; + if(assertCmd != null) { + string c; + if(Houdini.Houdini.MatchCandidate(assertCmd.Expr, candidates, out c)) { + AddCandidateOccurrence(c, b); + } + } + } + } + + // Add all candidate occurrences in preconditions + foreach(var proc in prog.TopLevelDeclarations.OfType()) { + foreach(Requires r in proc.Requires) { + string c; + if(Houdini.Houdini.MatchCandidate(r.Condition, candidates, out c)) { + AddCandidateOccurrence(c, new Tuple(proc.Name, PrePost.PRE)); + } + } + } + + // Add all candidate occurrences in preconditions + foreach(var proc in prog.TopLevelDeclarations.OfType()) { + foreach(Ensures e in proc.Ensures) { + string c; + if(Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) { + AddCandidateOccurrence(c, new Tuple(proc.Name, PrePost.POST)); + } + } + } + + } + + private void AddCandidateOccurrence(string c, object o) { + Debug.Assert(o is Block || o is Tuple); + if(!candidateToOccurences.ContainsKey(c)) { + candidateToOccurences[c] = new HashSet(); + } + candidateToOccurences[c].Add(o); + } + + public bool MayReach(string c, string d) { + foreach(object cOccurrence in candidateToOccurences[c]) { + foreach(object dOccurrence in candidateToOccurences[d]) { + if(OccurrencesMayReach(cOccurrence, dOccurrence)) { + return true; + } + } + } + return false; + } + + private bool OccurrencesMayReach(object cOccurrence, object dOccurrence) { + Debug.Assert(cOccurrence is Block || cOccurrence is Tuple); + Debug.Assert(dOccurrence is Block || dOccurrence is Tuple); + + Block cInterproceduralBlock = GetInterproceduralBlock(cOccurrence); + Block dInterproceduralBlock = GetInterproceduralBlock(dOccurrence); + + return reachabilityGraph.MayReach(cInterproceduralBlock, dInterproceduralBlock); + + throw new NotImplementedException(); + } + + private Block GetInterproceduralBlock(object cOccurrence) + { + Debug.Assert(cOccurrence is Block || cOccurrence is Tuple); + + var stringPrePostPair = cOccurrence as Tuple; + if(stringPrePostPair != null) { + if(stringPrePostPair.Item2 == PrePost.PRE) { + return reachabilityGraph.GetNewEntryBlock(stringPrePostPair.Item1); + } else { + return reachabilityGraph.GetNewExitBlock(stringPrePostPair.Item1); + } + } + + return reachabilityGraph.GetNewBlock((Block)cOccurrence); + + } + } + } -- cgit v1.2.3