Added MustReach information to VC gen

1 files changed, 46 insertions, 23 deletions

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index f87e6e51..6ed168c2 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -29,10 +29,10 @@ namespace VC {
     public Dictionary<Block, List<StratifiedCallSite>> recordProcCallSites;

     public VCExpr vcexpr;

 

-    // the following three fields are not being used at the moment

-    public VCExprVar entryExprVar;

-    public Dictionary<Block, Macro> reachMacros;

-    public Dictionary<Block, VCExpr> reachMacroDefinitions;

+    // Must-Reach Information

+    public static bool ComputeMustReachInformation = false;

+    public Dictionary<Block, VCExprVar> mustReachVar;

+    public List<VCExprLetBinding> mustReachBindings;

 

     public StratifiedVC(StratifiedInliningInfo siInfo, HashSet<string> procCalls) {

       info = siInfo;

@@ -78,26 +78,43 @@ namespace VC {
       if(procCalls != null)

          vcexpr = RemoveProcedureCalls.Apply(vcexpr, info.vcgen.prover.VCExprGen, procCalls);

 

-      #if false

-      var impl = info.impl;

-      reachMacros = new Dictionary<Block, Macro>();

-      reachMacroDefinitions = new Dictionary<Block, VCExpr>();

-      foreach (Block b in impl.Blocks) {

-        reachMacros[b] = vcgen.CreateNewMacro();

-        reachMacroDefinitions[b] = VCExpressionGenerator.False;

-      }

-      entryExprVar = vcgen.CreateNewVar(Microsoft.Boogie.Type.Bool);

-      reachMacroDefinitions[impl.Blocks[0]] = entryExprVar;

-      foreach (Block currBlock in impl.Blocks) {

-        GotoCmd gotoCmd = currBlock.TransferCmd as GotoCmd;

-        if (gotoCmd == null) continue;

-        foreach (Block successorBlock in gotoCmd.labelTargets) {

-          VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(BigNum.FromInt(id)), gen.Integer(BigNum.FromInt(currBlock.UniqueId)));

-          VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successorBlock.UniqueId)));

-          reachMacroDefinitions[successorBlock] = gen.Or(reachMacroDefinitions[successorBlock], gen.And(gen.Function(reachMacros[currBlock]), controlTransferExpr));

-        }

+      if (ComputeMustReachInformation && !CommandLineOptions.Clo.UseLabels)

+      {

+          var impl = info.impl;

+          mustReachVar = new Dictionary<Block, VCExprVar>();

+          mustReachBindings = new List<VCExprLetBinding>();

+          foreach (Block b in impl.Blocks)

+              mustReachVar[b] = vcgen.CreateNewVar(Bpl.Type.Bool);

+

+          var dag = new Graph<Block>();

+          dag.AddSource(impl.Blocks[0]);

+          foreach (Block b in impl.Blocks)

+          {

+              var gtc = b.TransferCmd as GotoCmd;

+              if (gtc != null)

+                  foreach (Block dest in gtc.labelTargets)

+                      dag.AddEdge(dest, b);

+          }

+          IEnumerable sortedNodes = dag.TopologicalSort();

+

+          foreach (Block currBlock in dag.TopologicalSort())

+          {

+              if (currBlock == impl.Blocks[0])

+              {

+                  mustReachBindings.Add(gen.LetBinding(mustReachVar[currBlock], VCExpressionGenerator.True));

+                  continue;

+              }

+

+              VCExpr expr = VCExpressionGenerator.False;

+              foreach (var pred in dag.Successors(currBlock))

+              {

+                  VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(gen.Integer(BigNum.FromInt(id)), gen.Integer(BigNum.FromInt(pred.UniqueId)));

+                  VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(currBlock.UniqueId)));

+                  expr = gen.Or(expr, gen.And(mustReachVar[pred], controlTransferExpr));

+              }

+              mustReachBindings.Add(gen.LetBinding(mustReachVar[currBlock], expr));

+          }

       }

-      #endif

 

       callSites = new Dictionary<Block, List<StratifiedCallSite>>();

       foreach (Block b in info.callSites.Keys) {

@@ -116,6 +133,12 @@ namespace VC {
       }

     }

 

+    public VCExpr MustReach(Block block)

+    {

+        Contract.Assert(ComputeMustReachInformation && mustReachVar.ContainsKey(block) && mustReachBindings != null);

+        return info.vcgen.prover.VCExprGen.Let(mustReachBindings, mustReachVar[block]);

+    }

+

     public List<StratifiedCallSite> CallSites {

       get {

         var ret = new List<StratifiedCallSite>();