From 88679e1cc6fb26590886686519987fa958a2735b Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Sat, 25 Feb 2012 14:01:25 -0800
Subject: further fixes related to using uninterpreted function for error
 traces removed Provers.Simplify, Provers.Z3, Provers.TPTP from the solution

---
 Source/VCGeneration/VC.cs | 44 ++++++++++++++++++++++++++++++++++++--------
 1 file changed, 36 insertions(+), 8 deletions(-)

(limited to 'Source/VCGeneration/VC.cs')

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 49fa7144..1c0aeee8 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -607,8 +607,30 @@ namespace VC {
         Hashtable label2Absy;
         Checker ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);
         Contract.Assert(ch != null);
-        VCExpr vc = parent.GenerateVC(impl, null, out label2Absy, ch);
+
+        Variable controlFlowVariable = null;
+        if (!CommandLineOptions.Clo.UseLabels) {
+          foreach (Variable v in impl.LocVars) {
+            if (v.Name == "@cfc") {
+              controlFlowVariable = v;
+              break;
+            }
+          }
+        }
+
+        VCExpr vc = parent.GenerateVC(impl, controlFlowVariable, out label2Absy, ch);
         Contract.Assert(vc != null);
+        
+        if (!CommandLineOptions.Clo.UseLabels) {
+          var ctx = ch.TheoremProver.Context;
+          var bet = ctx.BoogieExprTranslator;
+          VCExpr controlFlowVariableExpr = bet.LookupVariable(controlFlowVariable);
+          VCExpr eqExpr1 = ctx.ExprGen.Eq(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));
+          VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));
+          VCExpr eqExpr2 = ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
+          vc = ctx.ExprGen.Implies(eqExpr1, ctx.ExprGen.Implies(eqExpr2, vc));
+        }
+
         impl.Blocks = backup;
 
         if (CommandLineOptions.Clo.TraceVerify) {
@@ -1537,7 +1559,6 @@ namespace VC {
 		  ));
 
         LocalVariable controlFlowVariable = null;
-
         if (!CommandLineOptions.Clo.UseLabels) {
           controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "@cfc", Microsoft.Boogie.Type.Int));
           impl.LocVars.Add(controlFlowVariable);
@@ -1548,10 +1569,10 @@ namespace VC {
 
         if (!CommandLineOptions.Clo.UseLabels) {
           VCExpr controlFlowVariableExpr = bet.LookupVariable(controlFlowVariable);
-          Contract.Assert(controlFlowVariableExpr != null);
+          VCExpr eqExpr1 = ctx.ExprGen.Eq(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));
           VCExpr controlFlowFunctionAppl = ctx.ExprGen.ControlFlowFunctionApplication(controlFlowVariableExpr, ctx.ExprGen.Integer(BigNum.ZERO));
-          Contract.Assert(controlFlowFunctionAppl != null);
-          vc = ctx.ExprGen.Implies(ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId))), vc);
+          VCExpr eqExpr2 = ctx.ExprGen.Eq(controlFlowFunctionAppl, ctx.ExprGen.Integer(BigNum.FromInt(impl.Blocks[0].UniqueId)));
+          vc = ctx.ExprGen.Implies(eqExpr1, ctx.ExprGen.Implies(eqExpr2, vc));
         }
         
         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
@@ -1667,7 +1688,7 @@ namespace VC {
           break;
         case CommandLineOptions.VCVariety.Dag:
           if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags) {
-            vc = DagVC(cce.NonNull(impl.Blocks[0]), label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context, out assertionCount);
+            vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariable, label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context, out assertionCount);
           } else {
             vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariable, label2absy, ch.TheoremProver.Context, out assertionCount);
           }
@@ -3593,6 +3614,7 @@ namespace VC {
     }
 
     static VCExpr DagVC(Block block,
+                         Variable controlFlowVariable,
                          Hashtable/*<int, Absy!>*/ label2absy,
                          Hashtable/*<Block, VCExpr!>*/ blockEquations,
                          ProverContext proverCtxt,
@@ -3623,8 +3645,14 @@ namespace VC {
         foreach (Block successor in cce.NonNull(gotocmd.labelTargets)) {
           Contract.Assert(successor != null);
           int ac;
-          VCExpr c = DagVC(successor, label2absy, blockEquations, proverCtxt, out ac);
+          VCExpr c = DagVC(successor, controlFlowVariable, label2absy, blockEquations, proverCtxt, out ac);
           assertionCount += ac;
+          if (controlFlowVariable != null) {
+            VCExprVar controlFlowVariableExpr = proverCtxt.BoogieExprTranslator.LookupVariable(controlFlowVariable);
+            VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(block.UniqueId)));
+            VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successor.UniqueId)));
+            c = gen.Implies(controlTransferExpr, c);
+          }  
           SuccCorrect = SuccCorrect == null ? c : gen.And(SuccCorrect, c);
         }
       }
@@ -3632,7 +3660,7 @@ namespace VC {
         SuccCorrect = VCExpressionGenerator.True;
       }
 
-      VCContext context = new VCContext(label2absy, proverCtxt);
+      VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable);
       vc = Wlp.Block(block, SuccCorrect, context);
       assertionCount += context.AssertionCount;
       
-- 
cgit v1.2.3