Fix uses of heap parameter in verifier-translation of comprehension e…

…xpressions (#1166)

* Use correct heap when defining frame for lambda expr

* Fix crash

Fixes #1163

* Add regression test

* Make sure allocation tests are performed

* Use correct heap throughout comprehension translation

* Note that wish has been granted

* Assume lambda-expr parameters are allocated on entry

* Adjust for changes in error-path output

Source/Dafny/Translator.cs

@@ -5681,15 +5681,21 @@ Bpl.Cmd CaptureState(Statement stmt) {
       return CaptureState(stmt.EndTok, true, null);
     }
 
-    void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause, BoogieStmtListBuilder/*!*/ builder, List<Variable>/*!*/ localVariables, string name)
+    void DefineFrame(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ frameClause,
+      BoogieStmtListBuilder/*!*/ builder, List<Variable>/*!*/ localVariables, string name, ExpressionTranslator/*?*/ etran = null)
     {
       Contract.Requires(tok != null);
       Contract.Requires(cce.NonNullElements(frameClause));
       Contract.Requires(builder != null);
       Contract.Requires(cce.NonNullElements(localVariables));
       Contract.Requires(predef != null);
 
-      var etran = new ExpressionTranslator(this, predef, tok);
+      if (etran == null) {
+        // This is the common case. It means that the frame will be defined in terms of the usual variable $Heap.
+        // The one case where a frame is needed for a different heap is for lambda expressions, because they may
+        // sit inside of an "old" expression.
+        etran = new ExpressionTranslator(this, predef, tok);
+      }
       // Declare a local variable $_Frame: <alpha>[ref, Field alpha]bool
       Bpl.IdentifierExpr theFrame = etran.TheFrame(tok);  // this is a throw-away expression, used only to extract the type and name of the $_Frame variable
       Contract.Assert(theFrame.Type != null);  // follows from the postcondition of TheFrame
@@ -7890,37 +7896,37 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu
 
         builder.Add(new Bpl.CommentCmd("Begin Comprehension WF check"));
         BplIfIf(e.tok, lam != null, null, builder, nextBuilder => {
-          var substMap = SetupBoundVarsAsLocals(e.BoundVars, out var typeAntecedents, nextBuilder, locals, etran, typeMap);
+          var comprehensionEtran = etran;
+          if (lam != null) {
+            // Havoc heap
+            locals.Add(BplLocalVar(CurrentIdGenerator.FreshId((etran.UsesOldHeap ? "$Heap_at_" : "") + "$lambdaHeap#"), predef.HeapType, out var lambdaHeap));
+            comprehensionEtran = new ExpressionTranslator(comprehensionEtran, lambdaHeap);
+            nextBuilder.Add(new HavocCmd(expr.tok, Singleton((Bpl.IdentifierExpr)comprehensionEtran.HeapExpr)));
+            nextBuilder.Add(new AssumeCmd(expr.tok, FunctionCall(expr.tok, BuiltinFunction.IsGoodHeap, null, comprehensionEtran.HeapExpr)));
+            nextBuilder.Add(new AssumeCmd(expr.tok, HeapSameOrSucc(etran.HeapExpr, comprehensionEtran.HeapExpr)));
+          }
+
+          var substMap = SetupBoundVarsAsLocals(e.BoundVars, out var typeAntecedents, nextBuilder, locals, comprehensionEtran, typeMap);
           BplIfIf(e.tok, true, typeAntecedents, nextBuilder, newBuilder => {
             var s = new Substituter(null, substMap, typeMap);
             var body = Substitute(e.Term, null, substMap, typeMap);
             var bodyLeft = mc != null ? Substitute(mc.TermLeft, null, substMap, typeMap) : null;
-            var substMapPrime = mc != null ? SetupBoundVarsAsLocals(e.BoundVars, newBuilder, locals, etran, typeMap, "#prime") : null;
+            var substMapPrime = mc != null ? SetupBoundVarsAsLocals(e.BoundVars, newBuilder, locals, comprehensionEtran, typeMap, "#prime") : null;
             var bodyLeftPrime = mc != null ? Substitute(mc.TermLeft, null, substMapPrime, typeMap) : null;
             var bodyPrime = mc != null ? Substitute(e.Term, null, substMapPrime, typeMap) : null;
             List<FrameExpression> reads = null;
 
             var newOptions = options;
-            var newEtran = etran;
             if (lam != null) {
-              // Havoc heap
-              Bpl.Expr oldHeap;
-              locals.Add(BplLocalVar(CurrentIdGenerator.FreshId("$oldHeap#"), predef.HeapType, out oldHeap));
-              newBuilder.Add(BplSimplestAssign(oldHeap, etran.HeapExpr));
-              newBuilder.Add(new HavocCmd(expr.tok, Singleton((Bpl.IdentifierExpr)etran.HeapExpr)));
-              newBuilder.Add(new AssumeCmd(expr.tok,
-                FunctionCall(expr.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr)));
-              newBuilder.Add(new AssumeCmd(expr.tok, HeapSameOrSucc(oldHeap, etran.HeapExpr)));
-
               // Set up a new frame
               var frameName = CurrentIdGenerator.FreshId("$_Frame#l");
               reads = lam.Reads.ConvertAll(s.SubstFrameExpr);
-              DefineFrame(e.tok, reads, newBuilder, locals, frameName);
-              newEtran = new ExpressionTranslator(newEtran, frameName);
+              DefineFrame(e.tok, reads, newBuilder, locals, frameName, comprehensionEtran);
+              comprehensionEtran = new ExpressionTranslator(comprehensionEtran, frameName);
 
               // Check frame WF and that it read covers itself
               newOptions = new WFOptions(options.SelfCallsAllowance, true /* check reads clauses */, true /* delay reads checks */);
-              CheckFrameWellFormed(newOptions, reads, locals, newBuilder, newEtran);
+              CheckFrameWellFormed(newOptions, reads, locals, newBuilder, comprehensionEtran);
               // new options now contains the delayed reads checks
               newOptions.ProcessSavedReadsChecks(locals, builder, newBuilder);
 
@@ -7932,13 +7938,13 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu
             Bpl.Expr guard = null;
             if (e.Range != null) {
               var range = Substitute(e.Range, null, substMap);
-              CheckWellformed(range, newOptions, locals, newBuilder, newEtran);
-              guard = etran.TrExpr(range);
+              CheckWellformed(range, newOptions, locals, newBuilder, comprehensionEtran);
+              guard = comprehensionEtran.TrExpr(range);
             }
 
             if (mc != null) {
               Contract.Assert(bodyLeft != null);
-              BplIfIf(e.tok, guard != null, guard, newBuilder, b => { CheckWellformed(bodyLeft, newOptions, locals, b, newEtran); });
+              BplIfIf(e.tok, guard != null, guard, newBuilder, b => { CheckWellformed(bodyLeft, newOptions, locals, b, comprehensionEtran); });
             }
             BplIfIf(e.tok, guard != null, guard, newBuilder, b => {
               Bpl.Expr resultIe = null;
@@ -7950,7 +7956,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu
                 resultIe = new Bpl.IdentifierExpr(body.tok, resultVar);
                 rangeType = lam.Type.AsArrowType.Result;
               }
-              CheckWellformedWithResult(body, newOptions, resultIe, rangeType, locals, b, newEtran);
+              CheckWellformedWithResult(body, newOptions, resultIe, rangeType, locals, b, comprehensionEtran);
             });
 
             if (mc != null) {
@@ -7961,12 +7967,12 @@ void CheckWellformedWithResult(Expression expr, WFOptions options, Bpl.Expr resu
               if (guard != null) {
                 Contract.Assert(e.Range != null);
                 var rangePrime = Substitute(e.Range, null, substMapPrime);
-                guardPrime = etran.TrExpr(rangePrime);
+                guardPrime = comprehensionEtran.TrExpr(rangePrime);
               }
               BplIfIf(e.tok, guard != null, BplAnd(guard, guardPrime), newBuilder, b => {
                 var different = BplOr(
-                  Bpl.Expr.Neq(etran.TrExpr(bodyLeft), etran.TrExpr(bodyLeftPrime)),
-                  Bpl.Expr.Eq(etran.TrExpr(body), etran.TrExpr(bodyPrime)));
+                  Bpl.Expr.Neq(comprehensionEtran.TrExpr(bodyLeft), comprehensionEtran.TrExpr(bodyLeftPrime)),
+                  Bpl.Expr.Eq(comprehensionEtran.TrExpr(body), comprehensionEtran.TrExpr(bodyPrime)));
                 b.Add(Assert(mc.TermLeft.tok, different, "key expressions may be referring to the same value"));
               });
             }
@@ -12584,7 +12590,7 @@ Dictionary<IVariable, Expression> SetupBoundVarsAsLocals(List<BoundVar> boundVar
         locals.Add(bvar);
         var bIe = new Bpl.IdentifierExpr(bvar.tok, bvar);
         builder.Add(new Bpl.HavocCmd(bv.tok, new List<Bpl.IdentifierExpr> { bIe }));
-        Bpl.Expr wh = GetWhereClause(bv.tok, bIe, local.Type, etran, NOALLOC);
+        Bpl.Expr wh = GetWhereClause(bv.tok, bIe, local.Type, etran, CommonHeapUse ? IsAllocType.ISALLOC : IsAllocType.NOALLOC);
         if (wh != null) {
           typeAntecedent = BplAnd(typeAntecedent, wh);
         }

Test/allocated1/dafny0/Comprehensions.dfy.expect

@@ -33,6 +33,7 @@ Comprehensions.dfy(115,40): Error: insufficient reads clause to read field
 Execution trace:
     (0,0): anon0
     (0,0): anon10_Else
+    (0,0): anon11_Then
     (0,0): anon12_Then
     (0,0): anon13_Else
 Comprehensions.dfy(118,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor
@@ -73,12 +74,14 @@ Comprehensions.dfy(180,38): Error: value does not satisfy the subset constraints
 Execution trace:
     (0,0): anon0
     (0,0): anon10_Else
+    (0,0): anon11_Then
     (0,0): anon12_Then
     (0,0): anon13_Else
 Comprehensions.dfy(186,30): Error: value does not satisfy the subset constraints of 'nat'
 Execution trace:
     (0,0): anon0
     (0,0): anon10_Else
+    (0,0): anon11_Then
     (0,0): anon12_Then
     (0,0): anon13_Then
 Comprehensions.dfy(189,16): Error: value does not satisfy the subset constraints of 'nat'

Test/dafny0/ArrayElementInit.dfy.expect

@@ -1,6 +1,7 @@
 ArrayElementInit.dfy(13,31): Error: possible division by zero
 Execution trace:
     (0,0): anon0
+    (0,0): anon5_Then
     (0,0): anon6_Then
 ArrayElementInit.dfy(19,11): Error: all array indices must be in the domain of the initialization function
 Execution trace:

Test/dafny0/ArrayElementInitERR.dfy.expect

@@ -1,6 +1,7 @@
 ArrayElementInitERR.dfy(13,31): Error: possible division by zero
 Execution trace:
     (0,0): anon0
+    (0,0): anon5_Then
     (0,0): anon6_Then
 ArrayElementInitERR.dfy(19,11): Error: all array indices must be in the domain of the initialization function
 Execution trace:

Test/dafny0/Comprehensions.dfy.expect

@@ -16,6 +16,7 @@ Comprehensions.dfy(115,40): Error: insufficient reads clause to read field
 Execution trace:
     (0,0): anon0
     (0,0): anon10_Else
+    (0,0): anon11_Then
     (0,0): anon12_Then
     (0,0): anon13_Else
 Comprehensions.dfy(118,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor
@@ -56,12 +57,14 @@ Comprehensions.dfy(180,38): Error: value does not satisfy the subset constraints
 Execution trace:
     (0,0): anon0
     (0,0): anon10_Else
+    (0,0): anon11_Then
     (0,0): anon12_Then
     (0,0): anon13_Else
 Comprehensions.dfy(186,30): Error: value does not satisfy the subset constraints of 'nat'
 Execution trace:
     (0,0): anon0
     (0,0): anon10_Else
+    (0,0): anon11_Then
     (0,0): anon12_Then
     (0,0): anon13_Then
 Comprehensions.dfy(189,16): Error: value does not satisfy the subset constraints of 'nat'

Test/dafny4/ExpandedGuardednessNeg.dfy.expect

@@ -2,23 +2,27 @@ ExpandedGuardednessNeg.dfy(8,17): Error: cannot prove termination; try supplying
 Execution trace:
     (0,0): anon0
     (0,0): anon8_Else
+    (0,0): anon9_Then
     (0,0): anon10_Then
 ExpandedGuardednessNeg.dfy(8,17): Error: decreases expression must be bounded below by 0
 ExpandedGuardednessNeg.dfy(6,27): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon8_Else
+    (0,0): anon9_Then
     (0,0): anon10_Then
 ExpandedGuardednessNeg.dfy(13,16): Error: cannot prove termination; try supplying a decreases clause
 Execution trace:
     (0,0): anon0
     (0,0): anon8_Else
+    (0,0): anon9_Then
     (0,0): anon10_Then
 ExpandedGuardednessNeg.dfy(13,16): Error: decreases expression must be bounded below by 0
 ExpandedGuardednessNeg.dfy(11,21): Related location
 Execution trace:
     (0,0): anon0
     (0,0): anon8_Else
+    (0,0): anon9_Then
     (0,0): anon10_Then
 
 Dafny program verifier finished with 0 verified, 4 errors

Test/dafny4/regression-calc.dfy.expect

@@ -0,0 +1,11 @@
+regression-calc.dfy(8,16): Error: A postcondition might not hold on this return path.
+regression-calc.dfy(8,10): Related location: This is the postcondition that might not hold.
+Execution trace:
+    (0,0): anon0
+    regression-calc.dfy(9,5): anon2_Else
+regression-calc.dfy(15,16): Error: A postcondition might not hold on this return path.
+regression-calc.dfy(15,10): Related location: This is the postcondition that might not hold.
+Execution trace:
+    (0,0): anon0
+
+Dafny program verifier finished with 0 verified, 2 errors

Test/git-issues/git-issue-1163.dfy

@@ -0,0 +1,66 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function F(i: int): int
+
+method M() {
+  ghost var f := old(i => F(i));  // the translation of this once had crashed the verifier
+}
+
+class MyClass {
+  var y: int
+
+  method N()
+    modifies this
+  {
+    y := 8;
+    label L:
+    var p := new MyClass;
+    label K:
+    if * {
+      ghost var g := old@L((x: int) reads p.R(this) => x);  // error, because p is not allocated in L
+    } else if * {
+      ghost var g := old@L((x: int) reads R(p) => x);  // error, because p is not allocated in L
+    } else if * {
+      ghost var g := old@K((x: int) reads p.R(p) => x);
+    } else {
+      ghost var g := old((x: int) reads p.R(p) => x);  // error, because p is not allocated in old state
+    }
+  }
+
+  method O()
+    modifies this
+  {
+    y := 8;
+    label L:
+    ghost var h :=
+      old@L(
+        (p: MyClass) requires p.y == 10 reads p =>
+        assert p.y == 10; 5  // this assert once didn't work, because of a mismatch of heap variables in the translator
+      );
+  }
+
+  method Q()
+    modifies this
+  {
+    // The following uses of p in R(p) should be allowed. In particular, they should not
+    // produce "p not allocated in function state" errors.
+    if * {
+      ghost var h := old((p: MyClass) reads R(p) => 5);
+    } else if * {
+      ghost var s := old(iset p: MyClass | R(p) == p);
+    } else if * {
+      ghost var m := old(imap p: MyClass | R(p) == p :: 12);
+    } else if * {
+      ghost var m := old(var p: MyClass :| R(p) == p; p.y);
+    } else {
+      ghost var m := old(forall p: MyClass :: R(p) == p);
+    }
+  }
+
+  function R(c: MyClass): MyClass
+    reads this
+  {
+    this
+  }
+}

Test/git-issues/git-issue-1163.dfy.expect

@@ -0,0 +1,20 @@
+git-issue-1163.dfy(21,42): Error: receiver argument must be allocated in the state in which the function is invoked
+Execution trace:
+    (0,0): anon0
+    (0,0): anon23_Then
+    (0,0): anon24_Then
+    (0,0): anon25_Then
+git-issue-1163.dfy(23,44): Error: argument must be allocated in the state in which the function is invoked
+Execution trace:
+    (0,0): anon0
+    (0,0): anon26_Then
+    (0,0): anon27_Then
+    (0,0): anon28_Then
+git-issue-1163.dfy(27,40): Error: receiver argument must be allocated in the state in which the function is invoked
+Execution trace:
+    (0,0): anon0
+    (0,0): anon29_Else
+    (0,0): anon32_Then
+    (0,0): anon33_Then
+
+Dafny program verifier finished with 3 verified, 3 errors

Test/git-issues/git-issue-334.dfy.expect

@@ -2,6 +2,7 @@ git-issue-334.dfy(6,17): Error: index out of range
 Execution trace:
     (0,0): anon0
     (0,0): anon8_Else
+    (0,0): anon9_Then
     (0,0): anon10_Then
 
 Dafny program verifier finished with 1 verified, 1 error

Test/git-issues/git-issue-405.dfy.expect

@@ -1,6 +1,7 @@
 git-issue-405.dfy(19,22): Error: insufficient reads clause to read field
 Execution trace:
     (0,0): anon0
+    (0,0): anon7_Then
     (0,0): anon8_Then
 
 Dafny program verifier finished with 6 verified, 1 error

Test/git-issues/git-issue-503.dfy.expect

@@ -1,6 +1,7 @@
 git-issue-503.dfy(18,4): Error: missing case in match expression: Input(None)
 Execution trace:
     (0,0): anon0
+    (0,0): anon10_Then
     (0,0): anon11_Then
     (0,0): anon12_Then
     (0,0): anon13_Else

Test/hofs/FnRef.dfy.expect

@@ -2,6 +2,7 @@ FnRef.dfy(17,44): Error: possible violation of function precondition
 Execution trace:
     (0,0): anon0
     FnRef.dfy(15,12): anon9_Else
+    (0,0): anon11_Then
     (0,0): anon12_Then
 FnRef.dfy(32,7): Error: possible violation of function precondition
 Execution trace:

Test/hofs/Frame.dfy.expect

@@ -18,11 +18,13 @@ Frame.dfy(66,18): Error: insufficient reads clause to read array element
 Execution trace:
     (0,0): anon0
     (0,0): anon23_Then
+    (0,0): anon24_Then
     (0,0): anon25_Then
 Frame.dfy(68,27): Error: insufficient reads clause to read array element
 Execution trace:
     (0,0): anon0
     (0,0): anon23_Else
+    (0,0): anon26_Then
     (0,0): anon27_Then
 Frame.dfy(123,13): Error: possible violation of function precondition
 Execution trace:

Test/hofs/Simple.dfy.expect

@@ -2,11 +2,13 @@ Simple.dfy(14,9): Error: possible division by zero
 Execution trace:
     (0,0): anon0
     (0,0): anon8_Else
+    (0,0): anon9_Then
     (0,0): anon10_Then
 Simple.dfy(27,9): Error: possible division by zero
 Execution trace:
     (0,0): anon0
     (0,0): anon8_Else
+    (0,0): anon9_Then
     (0,0): anon10_Then
 Simple.dfy(37,8): Error: possible violation of function precondition
 Execution trace:

Test/hofs/Twice.dfy.expect

@@ -6,6 +6,7 @@ Twice.dfy(34,31): Error: possible violation of function precondition
 Execution trace:
     (0,0): anon0
     (0,0): anon11_Else
+    (0,0): anon12_Then
     (0,0): anon13_Then
 
 Dafny program verifier finished with 2 verified, 2 errors