fixed the problem with codexprs

now positive/negative context is detected and appropriate translation is done

3 files changed, 51 insertions, 37 deletions

diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index e4101d49..c5c61546 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie.VCExprAST {
     }

   }

 

-  public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings, bool isAssumeContext);

+  public delegate VCExpr/*!*/ CodeExprConverter(CodeExpr/*!*/ codeExpr, Hashtable/*<Block, VCExprVar!>*//*!*/ blockVariables, List<VCExprLetBinding> bindings, bool isPositiveContext);

 

   public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {

     // Stack on which the various Visit-methods put the result of the translation

@@ -375,13 +375,42 @@ namespace Microsoft.Boogie.VCExprAST {
       return node;

     }

 

+    public bool isPositiveContext = true;

     private VCExpr TranslateNAryExpr(NAryExpr node) {

       Contract.Requires(node != null);

       Contract.Ensures(Contract.Result<VCExpr>() != null);

+     

+      bool flipContextForArg0 = false;

+      if (node.Fun is UnaryOperator)

+      {

+          UnaryOperator oper = (UnaryOperator)node.Fun;

+          if (oper.Op == UnaryOperator.Opcode.Neg)

+              flipContextForArg0 = true;

+      }

+      else if (node.Fun is BinaryOperator)

+      {

+          BinaryOperator oper = (BinaryOperator)node.Fun;

+          if (oper.Op == BinaryOperator.Opcode.Imp)

+              flipContextForArg0 = true;

+          else if (oper.Op == BinaryOperator.Opcode.Iff) {

+              Expr one = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List<Expr> { node.Args[0], node.Args[1] });

+              Expr two = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.Imp), new List<Expr> { node.Args[1], node.Args[0] });

+              NAryExpr cmpd = new NAryExpr(node.tok, new BinaryOperator(node.tok, BinaryOperator.Opcode.And), new List<Expr> { one, two });

+              TypecheckingContext tc = new TypecheckingContext(null);

+              cmpd.Typecheck(tc);

+              return TranslateNAryExpr(cmpd);

+          }

+      }

+

       int n = node.Args.Count;

       List<VCExpr/*!*/>/*!*/ vcs = new List<VCExpr/*!*/>(n);

+        

       for (int i = 0; i < n; i++) {

+        if (i == 0 && flipContextForArg0)

+            isPositiveContext = !isPositiveContext;

         vcs.Add(Translate(cce.NonNull(node.Args)[i]));

+        if (i == 0 && flipContextForArg0)

+            isPositiveContext = !isPositiveContext;

       }

 

       if (node.Type == null) {

@@ -618,12 +647,11 @@ namespace Microsoft.Boogie.VCExprAST {
     public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr) {

       //Contract.Requires(codeExpr != null);

       Contract.Ensures(Contract.Result<Expr>() != null);

-

       Contract.Assume(codeExprConverter != null);

 

       Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();

       List<VCExprLetBinding/*!*/> bindings = new List<VCExprLetBinding/*!*/>();

-      VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings, false);

+      VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings, isPositiveContext);

       Push(e);

       return codeExpr;

     }

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 7cd9f9c2..ca74c1d2 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1345,7 +1345,7 @@ namespace VC {
             this.ctx = ctx;

         }

 

-        public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, Hashtable blockVariables, List<VCExprLetBinding> bindings, bool isAssumeContext)

+        public VCExpr CodeExprToVerificationCondition(CodeExpr codeExpr, Hashtable blockVariables, List<VCExprLetBinding> bindings, bool isPositiveContext)

         {

             VCGen vcgen = new VCGen(new Program(), null, false, new List<Checker>());

             vcgen.variable2SequenceNumber = new Dictionary<Variable, int>();

@@ -1356,12 +1356,8 @@ namespace VC {
             vcgen.AddBlocksBetween(codeExpr.Blocks);

             Dictionary<Variable, Expr> gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new List<IdentifierExpr>(), new ModelViewInfo(codeExpr));

             int ac;  // computed, but then ignored for this CodeExpr

-            VCExpr startCorrect = VCGen.LetVCIterative(codeExpr.Blocks, null, label2absy, ctx, out ac, isAssumeContext);

+            VCExpr startCorrect = VCGen.LetVCIterative(codeExpr.Blocks, null, label2absy, ctx, out ac, isPositiveContext);

             VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);

-            if (isAssumeContext)

-            {

-                vce = ctx.ExprGen.Not(vce);

-            }

             if (vcgen.CurrentLocalVariables.Count != 0)

             {

                 Boogie2VCExprTranslator translator = ctx.BoogieExprTranslator;

@@ -1378,15 +1374,12 @@ namespace VC {
                         vce = ctx.ExprGen.Implies(ctx.ExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce);

                     }

                 }

-                if (isAssumeContext)

-                {

-                    vce = ctx.ExprGen.Exists(boundVars, new List<VCTrigger>(), vce);

-                }

-                else

-                {

-                    vce = ctx.ExprGen.Forall(boundVars, new List<VCTrigger>(), vce);

-                }

+                vce = ctx.ExprGen.Forall(boundVars, new List<VCTrigger>(), vce);

             }

+            if (isPositiveContext)

+            {

+                vce = ctx.ExprGen.Not(vce);

+            } 

             return vce;

         }

     }

@@ -2717,7 +2710,7 @@ namespace VC {
                                  Dictionary<int, Absy> label2absy,

                                  ProverContext proverCtxt,

                                  out int assertionCount,

-                                 bool isAssumeContext = false)

+                                 bool isPositiveContext = true)

     {

       Contract.Requires(blocks != null);

       Contract.Requires(proverCtxt != null);

@@ -2755,7 +2748,7 @@ namespace VC {
           else {

             SuccCorrect = proverCtxt.BoogieExprTranslator.Translate(re.Expr);

           }

-          if (isAssumeContext)

+          if (isPositiveContext)

           {

               SuccCorrect = gen.Not(SuccCorrect);

           }

@@ -2776,7 +2769,7 @@ namespace VC {
           SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);

         }

 

-        VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr);

+        VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariableExpr, isPositiveContext);

         VCExpr vc = Wlp.Block(block, SuccCorrect, context);

         assertionCount += context.AssertionCount;

 

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index b1e69c38..bb2a2785 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -24,22 +24,24 @@ namespace VC {
     [Rep] public readonly ProverContext Ctxt;

     public readonly VCExpr ControlFlowVariableExpr;

     public int AssertionCount;  // counts the number of assertions for which Wlp has been computed

-    

-    public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt)

+    public bool isPositiveContext;

+

+    public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, bool isPositiveContext = true)

     {

       Contract.Requires(ctxt != null);

       this.Label2absy = label2absy;

       this.Ctxt = ctxt;

+      this.isPositiveContext = isPositiveContext;

     }

-    

-    public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr)

+

+    public VCContext(Dictionary<int, Absy> label2absy, ProverContext ctxt, VCExpr controlFlowVariableExpr, bool isPositiveContext = true)

     {

       Contract.Requires(ctxt != null);

       this.Label2absy = label2absy;

       this.Ctxt = ctxt;

       this.ControlFlowVariableExpr = controlFlowVariableExpr;

+      this.isPositiveContext = isPositiveContext;

     }

-    

   }

 

   #region A class to compute wlp of a passive command program

@@ -95,7 +97,9 @@ namespace VC {
       Contract.Assert(gen != null);

       if (cmd is AssertCmd) {

         AssertCmd ac = (AssertCmd)cmd;

+        ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext;

         VCExpr C = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);

+        ctxt.Ctxt.BoogieExprTranslator.isPositiveContext = !ctxt.Ctxt.BoogieExprTranslator.isPositiveContext; 

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

           return gen.Implies(C, N);

         } else {

@@ -159,18 +163,7 @@ namespace VC {
             }

           }

         }

-

-        CodeExpr codeExpr = ac.Expr as CodeExpr;

-        if (codeExpr != null)

-        {

-            Hashtable blockVariables = new Hashtable();

-            List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();

-            return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.codeExprConverter(codeExpr, blockVariables, bindings, true), N);

-        }

-        else

-        {

-            return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);

-        }

+        return gen.ImpliesSimp(ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr), N);

       } else {

         Console.WriteLine(cmd.ToString());

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