summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar allydonaldson <unknown>2013-05-29 08:02:16 +0100
committerGravatar allydonaldson <unknown>2013-05-29 08:02:16 +0100
commit3b0b6a95957a01969a85ab0b3e98de350247e0c6 (patch)
treeaf560445254b59634d3e9b8bc6f27fdffe4522ea
parentdf16e47b755f4d756d234f99bb3e30fcc311812d (diff)
Improvements to Staged Houdini
-rw-r--r--Source/Core/CommandLineOptions.cs8
-rw-r--r--Source/Core/Core.csproj1
-rw-r--r--Source/Core/InterProceduralReachabilityGraph.cs291
-rw-r--r--Source/Houdini/CandidateDependenceAnalyser.cs288
4 files changed, 420 insertions, 168 deletions
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 @@
<Compile Include="AbsyQuant.cs" />
<Compile Include="AbsyType.cs" />
<Compile Include="BitvectorAnalysis.cs" />
+ <Compile Include="InterProceduralReachabilityGraph.cs" />
<Compile Include="CommandLineOptions.cs" />
<Compile Include="DeadVarElim.cs" />
<Compile Include="Duplicator.cs" />
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<Block> nodes;
+ private Dictionary<Block, Block> originalToNew;
+ private Dictionary<string, Block> newProcedureEntryNodes;
+ private Dictionary<string, Block> newProcedureExitNodes;
+
+ private Graph<Block> reachabilityGraph;
+
+ public InterproceduralReachabilityGraph(Program prog) {
+ this.prog = prog;
+ originalToNew = new Dictionary<Block,Block>();
+ newProcedureEntryNodes = new Dictionary<string,Block>();
+ newProcedureExitNodes = new Dictionary<string,Block>();
+ nodes = new HashSet<Block>();
+
+ ProcessImplementations();
+
+ ProcessBodilessProcedures();
+
+ PatchUpGotoTargets();
+
+ AddCallAndReturnEdges();
+
+ reachabilityGraph = new Graph<Block>();
+
+ 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<Block> OriginalProgramBlocks()
+ {
+ return prog.TopLevelDeclarations.OfType<Implementation>().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<Procedure>())
+ {
+ 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<Implementation>())
+ {
+ 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<List<Cmd>> partition = PartitionCmds(b.Cmds);
+ Block prev = null;
+ int i = 0;
+ foreach (List<Cmd> 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<List<Cmd>> PartitionCmds(CmdSeq cmds) {
+ List<List<Cmd>> result = new List<List<Cmd>>();
+ List<Cmd> current = new List<Cmd>();
+ result.Add(current);
+ foreach(Cmd cmd in cmds) {
+ if(cmd is CallCmd && current.Count > 0) {
+ current = new List<Cmd>();
+ result.Add(current);
+ }
+ current.Add(cmd);
+ }
+ return result;
+ }
+
+ private Graph<SCC<Block>> ReachabilityGraphSCCsDAG;
+ private Dictionary<Block, SCC<Block>> BlockToSCC;
+
+ private Dictionary<SCC<Block>, HashSet<Block>> MayReachCache = new Dictionary<SCC<Block>, HashSet<Block>>();
+
+ public bool MayReach(Block src, Block dst) {
+ if (ReachabilityGraphSCCsDAG == null) {
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Interprocedural reachability: computing SCCs");
+ }
+ Adjacency<Block> next = new Adjacency<Block>(reachabilityGraph.Successors);
+ Adjacency<Block> prev = new Adjacency<Block>(reachabilityGraph.Predecessors);
+ StronglyConnectedComponents<Block> ReachabilitySCCs = new StronglyConnectedComponents<Block>(
+ reachabilityGraph.Nodes, next, prev);
+ ReachabilitySCCs.Compute();
+
+ BlockToSCC = new Dictionary<Block, SCC<Block>>();
+ foreach (var scc in ReachabilitySCCs) {
+ foreach (var s in scc) {
+ BlockToSCC[s] = scc;
+ }
+ }
+
+ ReachabilityGraphSCCsDAG = new Graph<SCC<Block>>();
+ foreach (var edge in reachabilityGraph.Edges) {
+ if (BlockToSCC[edge.Item1] != BlockToSCC[edge.Item2]) {
+ ReachabilityGraphSCCsDAG.AddEdge(BlockToSCC[edge.Item1], BlockToSCC[edge.Item2]);
+ }
+ }
+
+ SCC<Block> dummy = new SCC<Block>();
+ 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<Block> ReachableFrom(SCC<Block> scc) {
+ if (!MayReachCache.ContainsKey(scc)) {
+ HashSet<Block> result = new HashSet<Block>();
+ 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<string>();
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<string, List<Block>> procedureCFGs = new Dictionary<string, List<Block>>();
- Dictionary<string, HashSet<Block>> candidateToUse = new Dictionary<string, HashSet<Block>>();
-
- #region Prepare implementations
- foreach (var impl in prog.TopLevelDeclarations.OfType<Implementation>()) {
- procedureCFGs[impl.Name] = PrepareImplementationForCandidateReachability(impl);
- }
- #endregion
-
- #region Prepare any procedures that do not have implementations
- foreach (var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {
- 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<Block> newCFG = new List<Block>();
- Dictionary<Block, Block> oldToNew = new Dictionary<Block, Block>();
-
- foreach(var bb in procedureCFGs[proc]) {
- List<List<Cmd>> partition = new List<List<Cmd>>();
- List<Cmd> current = new List<Cmd>();
- partition.Add(current);
- foreach(Cmd cmd in bb.Cmds) {
- if(cmd is CallCmd && current.Count > 0) {
- current = new List<Cmd>();
- 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<Block> 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<Block> { requiresBlock, ensuresBlock };
- }
-
- private static List<Block> PrepareImplementationForCandidateReachability(Implementation impl)
- {
- // Clone the BBs and keep patchup map
- List<Block> newBBs = new List<Block>();
- Dictionary<Block, Block> oldToNew = new Dictionary<Block, Block>();
- 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<Block> newBBs, Dictionary<Block, Block> 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<string> candidates;
+ private IInterproceduralReachabilityGraph reachabilityGraph;
+ private Dictionary<string, HashSet<object>> candidateToOccurences;
+
+ internal CandidateReachabilityChecker(Program prog, IEnumerable<string> candidates) {
+ this.prog = prog;
+ this.candidates = candidates;
+ this.reachabilityGraph = new InterproceduralReachabilityGraph(prog);
+ this.candidateToOccurences = new Dictionary<string,HashSet<object>>();
+
+ // Add all candidate occurrences in blocks
+ foreach(Block b in prog.TopLevelDeclarations.OfType<Implementation>().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<Procedure>()) {
+ foreach(Requires r in proc.Requires) {
+ string c;
+ if(Houdini.Houdini.MatchCandidate(r.Condition, candidates, out c)) {
+ AddCandidateOccurrence(c, new Tuple<string, PrePost>(proc.Name, PrePost.PRE));
+ }
+ }
+ }
+
+ // Add all candidate occurrences in preconditions
+ foreach(var proc in prog.TopLevelDeclarations.OfType<Procedure>()) {
+ foreach(Ensures e in proc.Ensures) {
+ string c;
+ if(Houdini.Houdini.MatchCandidate(e.Condition, candidates, out c)) {
+ AddCandidateOccurrence(c, new Tuple<string, PrePost>(proc.Name, PrePost.POST));
+ }
+ }
+ }
+
+ }
+
+ private void AddCandidateOccurrence(string c, object o) {
+ Debug.Assert(o is Block || o is Tuple<string, PrePost>);
+ if(!candidateToOccurences.ContainsKey(c)) {
+ candidateToOccurences[c] = new HashSet<object>();
+ }
+ 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<string, PrePost>);
+ Debug.Assert(dOccurrence is Block || dOccurrence is Tuple<string, PrePost>);
+
+ 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<string, PrePost>);
+
+ var stringPrePostPair = cOccurrence as Tuple<string, PrePost>;
+ if(stringPrePostPair != null) {
+ if(stringPrePostPair.Item2 == PrePost.PRE) {
+ return reachabilityGraph.GetNewEntryBlock(stringPrePostPair.Item1);
+ } else {
+ return reachabilityGraph.GetNewExitBlock(stringPrePostPair.Item1);
+ }
+ }
+
+ return reachabilityGraph.GetNewBlock((Block)cOccurrence);
+
+ }
+ }
+
}