Improvements to Staged Houdini

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);

+

+    }

+  }

+

 }