modified letvc generation so that the use of control flow function and labels is decoupled. Former is controled by controlFlowVariable and the latter by label2Absy.

2 files changed, 42 insertions, 21 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index f3d08edb..8c8b17a0 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -232,18 +232,18 @@ namespace VC {
       ModelViewInfo mvInfo;

       info.gotoCmdOrigins = PassifyImpl(impl, program, out mvInfo);

       Contract.Assert(info.exitIncarnationMap != null);

-      Hashtable/*<int, Absy!>*/ label2absy;

       VCExpressionGenerator gen = checker.VCExprGen;

       Contract.Assert(gen != null);

       Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;

       Contract.Assert(translator != null);

-      

-      VCExpr vcexpr = gen.Not(GenerateVC(impl, info.controlFlowVariable, out label2absy, checker));

+

+      TypecheckingContext tc = new TypecheckingContext(null);

+      impl.Typecheck(tc);

+      VCExpr vcexpr = gen.Not(LetVC(impl.Blocks[0], info.controlFlowVariable, null, checker.TheoremProver.Context));

       Contract.Assert(vcexpr != null);

       ResetPredecessors(impl.Blocks);

       VCExpr reachvcexpr = GenerateReachVC(impl, info, checker);

       vcexpr = gen.And(vcexpr, reachvcexpr);

-      info.label2absy = label2absy;

       

       List<VCExprVar> privateVars = new List<VCExprVar>();

       foreach (Variable v in impl.LocVars) {

@@ -299,9 +299,9 @@ namespace VC {
     protected VCExpr GenerateReachVC(Implementation impl, LazyInliningInfo info, Checker ch) {

       Variable controlFlowVariable = info.controlFlowVariable;

       VCExpressionGenerator gen = ch.VCExprGen;

-      Boogie2VCExprTranslator translator = ch.TheoremProver.Context.BoogieExprTranslator;

       ProverContext proverCtxt = ch.TheoremProver.Context;

-      VCExprVar controlFlowVariableExpr = proverCtxt.BoogieExprTranslator.LookupVariable(controlFlowVariable);

+      Boogie2VCExprTranslator translator = proverCtxt.BoogieExprTranslator;

+      VCExprVar controlFlowVariableExpr = translator.LookupVariable(controlFlowVariable);

 

       Block exitBlock = null;

       Dictionary<Block, VCExprVar> reachVars = new Dictionary<Block, VCExprVar>();

@@ -2743,7 +2743,13 @@ namespace VC {
         GotoCmd gotoCmd = transferCmd as GotoCmd;

         if (gotoCmd == null) break;

         int nextBlockId = errModel.LookupControlFlowFunctionAt(cfcValue, b.UniqueId);

-        b = (Block)cce.NonNull(info.label2absy)[nextBlockId];

+        foreach (Block x in gotoCmd.labelTargets) {

+          if (nextBlockId == x.UniqueId) {

+            b = x;

+            break;

+          }

+        }

+        //b = (Block)cce.NonNull(info.label2absy)[nextBlockId];

         trace.Add(b);

       }

       Contract.Assert(false);throw new cce.UnreachableException();

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index 0b2c3225..23be6082 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -68,13 +68,18 @@ namespace VC {
       }

       

       int id = b.UniqueId;

+      if (ctxt.Label2absy != null) {

+        ctxt.Label2absy[id] = b;

+      }

+

       try {

         cce.BeginExpose(ctxt);

-        ctxt.Label2absy[id] = b;

-        if (ctxt.ControlFlowVariable != null)

+        if (ctxt.Label2absy == null) {

           return res;

-        else

+        }

+        else {

           return gen.Implies(gen.LabelPos(cce.NonNull(id.ToString()), VCExpressionGenerator.True), res);

+        }

       } finally {

         cce.EndExpose();

       }

@@ -97,9 +102,13 @@ namespace VC {
         VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

           return gen.Implies(C, N);

-        } else {

+        }

+        else {

           int id = ac.UniqueId;

-          ctxt.Label2absy[id] = ac;

+          if (ctxt.Label2absy != null) {

+            ctxt.Label2absy[id] = ac;

+          }

+

           switch (Subsumption(ac)) {

             case CommandLineOptions.SubsumptionOption.Never:

               break;

@@ -112,25 +121,31 @@ namespace VC {
               }

               break;

             default:

-              Contract.Assert(false);throw new cce.UnreachableException();  // unexpected case

+              Contract.Assert(false); throw new cce.UnreachableException();  // unexpected case

           }

-          

+

           // (MSchaef) Hack: This line might be useless, but at least it is not harmful

           // need to test it

-          if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) 

+          if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed)

             return gen.Implies(C, N);

-          

-          if (ctxt.ControlFlowVariable != null)

-          {

+

+          if (ctxt.ControlFlowVariable == null) {

+            Contract.Assert(ctxt.Label2absy != null);

+            return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), C), N);

+          }

+          else {

             VCExpr controlFlowVariableExpr = ctxt.Ctxt.BoogieExprTranslator.LookupVariable(ctxt.ControlFlowVariable);

             Contract.Assert(controlFlowVariableExpr != null);

             VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(b.UniqueId)));

             Contract.Assert(controlFlowFunctionAppl != null);

             VCExpr assertFailure = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(ac.UniqueId)));

-            return gen.And(gen.Implies(assertFailure, C), gen.Implies(C, N));

+            if (ctxt.Label2absy == null) {

+              return gen.AndSimp(gen.Implies(assertFailure, C), gen.Implies(C, N));

+            }

+            else {

+              return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), gen.Implies(assertFailure, C)), gen.Implies(C, N));

+            }

           }

-          else

-            return gen.AndSimp(gen.LabelNeg(cce.NonNull(id.ToString()), C), N);

         }

 

       } else if (cmd is AssumeCmd) {