Combined some common routines into CheckWellformedAndAssume, which also allows an improvement of the generated Boogie (which will be especially good soon, when reads-clause checking may change)

6 files changed, 126 insertions, 47 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e7a8bedf..992939ec 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1608,8 +1608,7 @@ namespace Microsoft.Dafny {
       Bpl.StmtList stmts;

       // check well-formedness of the preconditions, and then assume each one of them

       foreach (var p in iter.Requires) {

-        CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);

-        builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

+        CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran);

       }

       // check well-formedness of the modifies and reads clauses

       CheckFrameWellFormed(new WFOptions(), iter.Modifies.Expressions, localVariables, builder, etran);

@@ -1651,8 +1650,7 @@ namespace Microsoft.Dafny {
 

       // check well-formedness of the user-defined part of the yield-requires

       foreach (var p in iter.YieldRequires) {

-        CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);

-        builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

+        CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran);

       }

 

       // save the heap (representing the state where yield-requires holds):  $_OldIterHeap := Heap;

@@ -1704,12 +1702,10 @@ namespace Microsoft.Dafny {
       }

 

       foreach (var p in iter.YieldEnsures) {

-        CheckWellformed(p.E, new WFOptions(), localVariables, yeBuilder, yeEtran);

-        yeBuilder.Add(new Bpl.AssumeCmd(p.E.tok, yeEtran.TrExpr(p.E)));

+        CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, yeBuilder, yeEtran);

       }

       foreach (var p in iter.Ensures) {

-        CheckWellformed(p.E, new WFOptions(), localVariables, endBuilder, yeEtran);

-        endBuilder.Add(new Bpl.AssumeCmd(p.E.tok, yeEtran.TrExpr(p.E)));

+        CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, endBuilder, yeEtran);

       }

       builder.Add(new Bpl.IfCmd(iter.tok, null, yeBuilder.Collect(iter.tok), null, endBuilder.Collect(iter.tok)));

 

@@ -2863,8 +2859,7 @@ namespace Microsoft.Dafny {
       } else {

         // check well-formedness of the preconditions, and then assume each one of them

         foreach (MaybeFreeExpression p in m.Req) {

-          CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);

-          builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

+          CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran);

         }

         // check well-formedness of the modifies clause

         CheckFrameWellFormed(new WFOptions(), m.Mod.Expressions, localVariables, builder, etran);

@@ -2902,8 +2897,7 @@ namespace Microsoft.Dafny {
 

         // check wellformedness of postconditions

         foreach (MaybeFreeExpression p in m.Ens) {

-          CheckWellformed(p.E, new WFOptions(), localVariables, builder, etran);

-          builder.Add(new Bpl.AssumeCmd(p.E.tok, etran.TrExpr(p.E)));

+          CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran);

         }

 

         stmts = builder.Collect(m.tok);

@@ -4045,8 +4039,7 @@ namespace Microsoft.Dafny {
       }

 

       foreach (Expression p in f.Req) {

-        CheckWellformed(p, new WFOptions(null, true /* do reads checks */), locals, builder, etran);

-        builder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));

+        CheckWellformedAndAssume(p, new WFOptions(null, true /* do reads checks */), locals, builder, etran);

       }

 

       // check well-formedness of the decreases clauses (including termination, but no reads checks)

@@ -4090,9 +4083,8 @@ namespace Microsoft.Dafny {
       }

       // Now for the ensures clauses

       foreach (Expression p in f.Ens) {

-        CheckWellformed(p, new WFOptions(f, false), locals, postCheckBuilder, etran);

         // assume the postcondition for the benefit of checking the remaining postconditions

-        postCheckBuilder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));

+        CheckWellformedAndAssume(p, new WFOptions(f, false), locals, postCheckBuilder, etran);

       }

       // Here goes the body (and include both termination checks and reads checks)

       StmtListBuilder bodyCheckBuilder = new StmtListBuilder();

@@ -4658,7 +4650,106 @@ namespace Microsoft.Dafny {
       builder.Add(new Bpl.AssumeCmd(expr.tok, CanCallAssumption(expr, etran)));

     }

 

+    void CheckWellformedAndAssume(Expression expr, WFOptions options, List<Variable> locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {

+      Contract.Requires(expr != null);

+      Contract.Requires(expr.Type != null && expr.Type.IsBoolType);

+      Contract.Requires(options != null);

+      Contract.Requires(locals != null);

+      Contract.Requires(builder != null);

+      Contract.Requires(etran != null);

+      Contract.Requires(predef != null);

+      if (expr is BinaryExpr) {

+        var e = (BinaryExpr)expr;

+        switch (e.ResolvedOp) {

+          case BinaryExpr.ResolvedOpcode.And:

+            // WF[e0]; assume e0; WF[e1]; assume e1;

+            CheckWellformedAndAssume(e.E0, options, locals, builder, etran);

+            CheckWellformedAndAssume(e.E1, options, locals, builder, etran);

+            return;

+          case BinaryExpr.ResolvedOpcode.Imp: {

+              // if (*) {

+              //   WF[e0]; assume e0; WF[e1]; assume e1;

+              // } else {

+              //   assume e0 ==> e1;

+              // }

+              var bAnd = new Bpl.StmtListBuilder();

+              CheckWellformedAndAssume(e.E0, options, locals, bAnd, etran);

+              CheckWellformedAndAssume(e.E1, options, locals, bAnd, etran);

+              var bImp = new Bpl.StmtListBuilder();

+              bImp.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(expr)));

+              builder.Add(new Bpl.IfCmd(expr.tok, null, bAnd.Collect(expr.tok), null, bImp.Collect(expr.tok)));

+            }

+            return;

+          case BinaryExpr.ResolvedOpcode.Or: {

+              // if (*) {

+              //   WF[e0]; assume e0;

+              // } else {

+              //   assume !e0;

+              //   WF[e1]; assume e1;

+              // }

+              var b0 = new Bpl.StmtListBuilder();

+              CheckWellformedAndAssume(e.E0, options, locals, b0, etran);

+              var b1 = new Bpl.StmtListBuilder();

+              b1.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0))));

+              CheckWellformedAndAssume(e.E1, options, locals, b1, etran);

+              builder.Add(new Bpl.IfCmd(expr.tok, null, b0.Collect(expr.tok), null, b1.Collect(expr.tok)));

+            }

+            return;

+          default:

+            break;

+        }

+      } else if (expr is ITEExpr) {

+        var e = (ITEExpr)expr;

+        // if (*) {

+        //   WF[test]; assume test;

+        //   WF[thn]; assume thn;

+        // } else {

+        //   assume !test;

+        //   WF[els]; assume els;

+        // }

+        var bThn = new Bpl.StmtListBuilder();

+        CheckWellformedAndAssume(e.Test, options, locals, bThn, etran);

+        CheckWellformedAndAssume(e.Thn, options, locals, bThn, etran);

+        var bEls = new Bpl.StmtListBuilder();

+        bEls.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Not(etran.TrExpr(e.Test))));

+        CheckWellformedAndAssume(e.Els, options, locals, bEls, etran);

+        builder.Add(new Bpl.IfCmd(expr.tok, null, bThn.Collect(expr.tok), null, bEls.Collect(expr.tok)));

+        return;

+      } else if (expr is QuantifierExpr) {

+        var e = (QuantifierExpr)expr;

+        // For (Q x :: body(x)), introduce fresh local variable x'.  Then:

+        //   havoc x'

+        //   WF[body(x')]; assume body(x');

+        // If the quantifier is universal, then continue as:

+        //   assume (\forall x :: body(x));

+        var typeMap = new Dictionary<TypeParameter, Type>();

+        var copies = new List<TypeParameter>();

+        copies = Map(e.TypeArgs, tp => e.Refresh(tp, CurrentIdGenerator));

+        typeMap = Util.Dict(e.TypeArgs, Map(copies, tp => (Type)new UserDefinedType(tp)));

+        var newLocals = Map(copies, tp => new Bpl.LocalVariable(tp.tok, new TypedIdent(tp.tok, nameTypeParam(tp), predef.Ty)));

+        locals.AddRange(newLocals);

+        var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran, typeMap);  // ??

+        var s = new Substituter(null, substMap, typeMap, this);

+        var body = Substitute(e.LogicalBody(), null, substMap, typeMap);

+        builder.Add(new Bpl.HavocCmd(expr.tok, newLocals.ConvertAll(v => new Bpl.IdentifierExpr(v.tok, v))));

+        CheckWellformedAndAssume(body, options, locals, builder, etran);

+        if (e is ForallExpr) {

+          builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(expr)));

+        }

+        return;

+      }

+      // resort to the behavior of simply checking well-formedness followed by assuming the translated expression

+      CheckWellformedWithResult(expr, options, null, null, locals, builder, etran);

+      builder.Add(new Bpl.AssumeCmd(expr.tok, etran.TrExpr(expr)));

+    }

+

     void CheckWellformed(Expression expr, WFOptions options, List<Variable> locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {

+      Contract.Requires(expr != null);

+      Contract.Requires(options != null);

+      Contract.Requires(locals != null);

+      Contract.Requires(builder != null);

+      Contract.Requires(etran != null);

+      Contract.Requires(predef != null);

       CheckWellformedWithResult(expr, options, null, null, locals, builder, etran);

     }

 

diff --git a/Test/dafny0/Definedness.dfy.expect b/Test/dafny0/Definedness.dfy.expect
index 41073c0e..5d823616 100644
--- a/Test/dafny0/Definedness.dfy.expect
+++ b/Test/dafny0/Definedness.dfy.expect
@@ -161,19 +161,15 @@ Definedness.dfy(215,10): Error BP5003: A postcondition might not hold on this re
 Definedness.dfy(217,46): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

+    (0,0): anon3_Else

 Definedness.dfy(224,22): Error: target object may be null

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon2

-    (0,0): anon6_Then

+    (0,0): anon3_Then

 Definedness.dfy(237,10): Error BP5003: A postcondition might not hold on this return path.

 Definedness.dfy(240,24): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon2

-    (0,0): anon8_Else

+    (0,0): anon3_Else

 

 Dafny program verifier finished with 21 verified, 37 errors

diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect
index 4b9aa202..f5112bfe 100644
--- a/Test/dafny0/FunctionSpecifications.dfy.expect
+++ b/Test/dafny0/FunctionSpecifications.dfy.expect
@@ -10,19 +10,19 @@ FunctionSpecifications.dfy(45,3): Error BP5003: A postcondition might not hold o
 FunctionSpecifications.dfy(40,24): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon11_Else

-    (0,0): anon14_Else

-    (0,0): anon15_Then

+    (0,0): anon13_Else

+    (0,0): anon16_Else

+    (0,0): anon17_Then

 FunctionSpecifications.dfy(53,11): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon8_Then

-    (0,0): anon3

+    (0,0): anon9_Then

+    (0,0): anon4

 FunctionSpecifications.dfy(59,10): Error BP5003: A postcondition might not hold on this return path.

 FunctionSpecifications.dfy(60,22): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

+    (0,0): anon6_Else

 FunctionSpecifications.dfy(108,23): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -49,9 +49,7 @@ FunctionSpecifications.dfy(135,20): Error BP5003: A postcondition might not hold
 FunctionSpecifications.dfy(137,29): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Then

-    (0,0): anon2

-    (0,0): anon6_Else

+    (0,0): anon3_Else

 FunctionSpecifications.dfy(146,3): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect
index 090cf99d..1cd17d16 100644
--- a/Test/dafny0/Reads.dfy.expect
+++ b/Test/dafny0/Reads.dfy.expect
@@ -1,22 +1,18 @@
 Reads.dfy(9,30): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Then

 Reads.dfy(18,30): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-    (0,0): anon11_Then

-    (0,0): anon12_Then

+    (0,0): anon9_Then

+    (0,0): anon3

 Reads.dfy(28,50): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon8_Then

 Reads.dfy(37,43): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Then

-    (0,0): anon8_Then

+    (0,0): anon6_Then

 Reads.dfy(51,30): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 0a274281..b475502a 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -9,15 +9,13 @@ SmallTests.dfy(66,51): Error: possible division by zero
 Execution trace:

     (0,0): anon0

     (0,0): anon12_Else

-    (0,0): anon3

     (0,0): anon13_Else

 SmallTests.dfy(67,22): Error: target object may be null

 Execution trace:

     (0,0): anon0

     (0,0): anon12_Then

-    (0,0): anon3

     (0,0): anon13_Then

-    (0,0): anon6

+    (0,0): anon14_Then

 SmallTests.dfy(86,24): Error: target object may be null

 Execution trace:

     (0,0): anon0

diff --git a/Test/dafny0/Superposition.dfy.expect b/Test/dafny0/Superposition.dfy.expect
index 4b8e354f..eccb16b0 100644
--- a/Test/dafny0/Superposition.dfy.expect
+++ b/Test/dafny0/Superposition.dfy.expect
@@ -14,7 +14,7 @@ Superposition.dfy(27,15): Error BP5003: A postcondition might not hold on this r
 Superposition.dfy(28,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

+    (0,0): anon6_Else

 

 Verifying CheckWellformed$$_0_M0.C.R ...

   [5 proof obligations]  error

@@ -22,7 +22,7 @@ Superposition.dfy(33,15): Error BP5003: A postcondition might not hold on this r
 Superposition.dfy(34,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Else

+    (0,0): anon6_Else

 

 Verifying CheckWellformed$$_1_M1.C.M ...

   [0 proof obligations]  verified

@@ -36,9 +36,9 @@ Superposition.dfy(50,25): Error BP5003: A postcondition might not hold on this r
 Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-    (0,0): anon7_Else

-    (0,0): anon9_Then

-    (0,0): anon6

+    (0,0): anon8_Else

+    (0,0): anon10_Then

+    (0,0): anon7

 

 Verifying CheckWellformed$$_1_M1.C.Q ...

   [0 proof obligations]  verified