Solution to issue 2265 related to erroneous substitution under bindin…

RELEASE_NOTES.md

@@ -1,11 +1,11 @@
 # Upcoming
 
 - feat: Command-line arguments are now available from `Main` in Dafny programs, using `Main(args: seq<string>)` (https://github.com/dafny-lang/dafny/pull/2594)
-- feat: generate warning when 'old' has no effect (https://github.com/dafny-lang/dafny/pull/2610)
+- feat: Generate warning when 'old' has no effect (https://github.com/dafny-lang/dafny/pull/2610)
 - fix: Missing related position in failing precondition (https://github.com/dafny-lang/dafny/pull/2658)
 - fix: No more IDE crashing on the elephant operator (https://github.com/dafny-lang/dafny/pull/2668)
-- fix: retain non-method-body block statements when cloning abstract signatures (https://github.com/dafny-lang/dafny/pull/2731)
-
+- fix: Retain non-method-body block statements when cloning abstract signatures (https://github.com/dafny-lang/dafny/pull/2731)
+- fix: Correctly substitute variables introduced by a binding guard (https://github.com/dafny-lang/dafny/pull/2745)
 
 # 3.8.1
 

Source/DafnyCore/Substituter.cs

@@ -277,43 +277,8 @@ public virtual Expression Substitute(Expression expr) {
         }
 
       } else if (expr is ComprehensionExpr) {
-        var e = (ComprehensionExpr)expr;
-        // For quantifiers and setComprehesion we want to make sure that we don't introduce name clashes with
-        // the enclosing scopes.
 
-        var q = e as QuantifierExpr;
-        if (q != null && q.SplitQuantifier != null) {
-          return Substitute(q.SplitQuantifierExpression);
-        }
-
-        var newBoundVars = CreateBoundVarSubstitutions(e.BoundVars, expr is ForallExpr || expr is ExistsExpr || expr is SetComprehension);
-        var newRange = e.Range == null ? null : Substitute(e.Range);
-        var newTerm = Substitute(e.Term);
-        var newAttrs = SubstAttributes(e.Attributes);
-        var newBounds = SubstituteBoundedPoolList(e.Bounds);
-        if (newBoundVars != e.BoundVars || newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes || newBounds != e.Bounds) {
-          if (e is SetComprehension) {
-            newExpr = new SetComprehension(e.BodyStartTok, e.BodyEndTok, ((SetComprehension)e).Finite, newBoundVars, newRange, newTerm, newAttrs);
-          } else if (e is MapComprehension) {
-            var mc = (MapComprehension)e;
-            var newTermLeft = mc.IsGeneralMapComprehension ? Substitute(mc.TermLeft) : null;
-            newExpr = new MapComprehension(e.BodyStartTok, e.BodyEndTok, mc.Finite, newBoundVars, newRange, newTermLeft, newTerm, newAttrs);
-          } else if (expr is ForallExpr forallExpr) {
-            newExpr = new ForallExpr(expr.tok, e.BodyEndTok, newBoundVars, newRange, newTerm, newAttrs);
-          } else if (expr is ExistsExpr existsExpr) {
-            newExpr = new ExistsExpr(expr.tok, e.BodyEndTok, newBoundVars, newRange, newTerm, newAttrs);
-          } else if (expr is LambdaExpr) {
-            var l = (LambdaExpr)expr;
-            newExpr = new LambdaExpr(e.BodyStartTok, e.BodyEndTok, newBoundVars, newRange, l.Reads.ConvertAll(SubstFrameExpr), newTerm);
-          } else {
-            Contract.Assert(false);  // unexpected ComprehensionExpr
-          }
-          ((ComprehensionExpr)newExpr).Bounds = newBounds;
-        }
-        // undo any changes to substMap (could be optimized to do this only if newBoundVars != e.BoundVars)
-        foreach (var bv in e.BoundVars) {
-          substMap.Remove(bv);
-        }
+        newExpr = SubstituteComprehensionExpr((ComprehensionExpr)expr, true);
 
       } else if (expr is StmtExpr) {
         var e = (StmtExpr)expr;
@@ -713,7 +678,8 @@ protected virtual Statement SubstStmt(Statement stmt) {
         r = SubstBlockStmt((BlockStmt)stmt);
       } else if (stmt is IfStmt) {
         var s = (IfStmt)stmt;
-        r = new IfStmt(s.Tok, s.EndTok, s.IsBindingGuard, Substitute(s.Guard), SubstBlockStmt(s.Thn), SubstStmt(s.Els));
+        var guard = s.IsBindingGuard ? SubstituteComprehensionExpr((ExistsExpr)s.Guard, false) : Substitute(s.Guard);
+        r = new IfStmt(s.Tok, s.EndTok, s.IsBindingGuard, guard, SubstBlockStmt(s.Thn), SubstStmt(s.Els));
       } else if (stmt is AlternativeStmt) {
         var s = (AlternativeStmt)stmt;
         r = new AlternativeStmt(s.Tok, s.EndTok, s.Alternatives.ConvertAll(SubstGuardedAlternative), s.UsesOptionalBraces);
@@ -932,5 +898,68 @@ public Attributes SubstAttributes(Attributes attrs) {
       }
       return attrs;
     }
+
+    /// <summary>
+    /// Substitution in a comprehension expression. 
+    /// Parameter 'forceSubstituteOfBoundVars' should be set to false if and only if
+    /// the expression is a binding guard, in which case a bound variable is introduced.
+    /// Such a variable must not be substituted. 
+    /// </summary>
+    protected Expression SubstituteComprehensionExpr(ComprehensionExpr expr, bool forceSubstituteOfBoundVars) {
+
+      Expression newExpr = null;
+
+      var e = (ComprehensionExpr)expr;
+      // For quantifiers and setComprehesion we want to make sure that we don't introduce name clashes with
+      // the enclosing scopes.
+
+      var q = e as QuantifierExpr;
+      if (q != null && q.SplitQuantifier != null) {
+        if (forceSubstituteOfBoundVars) {
+          return Substitute(q.SplitQuantifierExpression);
+        } else {
+          return SubstituteComprehensionExpr((ComprehensionExpr)q.SplitQuantifierExpression, false);
+        }
+      }
+
+      var newBoundVars = CreateBoundVarSubstitutions(e.BoundVars, forceSubstituteOfBoundVars && (expr is ForallExpr || expr is ExistsExpr || expr is SetComprehension));
+      var newRange = e.Range == null ? null : Substitute(e.Range);
+      var newTerm = Substitute(e.Term);
+      var newAttrs = SubstAttributes(e.Attributes);
+      var newBounds = SubstituteBoundedPoolList(e.Bounds);
+      if (newBoundVars != e.BoundVars || newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes ||
+          newBounds != e.Bounds || !forceSubstituteOfBoundVars) {
+        if (e is SetComprehension) {
+          newExpr = new SetComprehension(e.BodyStartTok, e.BodyEndTok, ((SetComprehension)e).Finite, newBoundVars,
+            newRange, newTerm, newAttrs);
+        } else if (e is MapComprehension) {
+          var mc = (MapComprehension)e;
+          var newTermLeft = mc.IsGeneralMapComprehension ? Substitute(mc.TermLeft) : null;
+          newExpr = new MapComprehension(e.BodyStartTok, e.BodyEndTok, mc.Finite, newBoundVars, newRange, newTermLeft, newTerm, newAttrs);
+        } else if (expr is ForallExpr forallExpr) {
+          newExpr = new ForallExpr(expr.tok, e.BodyEndTok, newBoundVars, newRange, newTerm, newAttrs);
+        } else if (expr is ExistsExpr existsExpr) {
+          newExpr = new ExistsExpr(expr.tok, e.BodyEndTok, newBoundVars, newRange, newTerm, newAttrs);
+        } else if (expr is LambdaExpr) {
+          var l = (LambdaExpr)expr;
+          newExpr = new LambdaExpr(e.BodyStartTok, e.BodyEndTok, newBoundVars, newRange,
+            l.Reads.ConvertAll(SubstFrameExpr), newTerm);
+        } else {
+          Contract.Assert(false); // unexpected ComprehensionExpr
+        }
+
+        ((ComprehensionExpr)newExpr).Bounds = newBounds;
+      }
+
+      // undo any changes to substMap (could be optimized to do this only if newBoundVars != e.BoundVars)
+      foreach (var bv in e.BoundVars) {
+        substMap.Remove(bv);
+      }
+
+      return newExpr;
+
+    }
+
   }
 }
+

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

@@ -0,0 +1,18 @@
+// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module DefaultModule {
+  class DefaultClass {
+    static function BrokenFunction(): nat {
+      var y := 0;
+      assert true by {
+        if foobarquux: bool :| true {
+          assert true || foobarquux;
+        }
+      }
+      0
+    }
+  }
+}
+
+

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

@@ -0,0 +1,3 @@
+git-issue-2265.dfy(9,11): Warning: /!\ No terms found to trigger on.
+
+Dafny program verifier finished with 1 verified, 0 errors