feat: Generate a warning when 'old' has no effect (#2610)

Fixes #1989

If the argument to `old` has no dereferences of the mutable heap, generate a warning saying that the `old` has no effect. This has been a common source of errors and confusion.

RELEASE_NOTES.md

@@ -2,6 +2,7 @@
 
 - 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)
+- feat: generate warning when 'old' has no effect
 
 # 3.8.1
 
@@ -15,7 +16,6 @@
 - fix: Better messages on hovering failing postconditions in IDE (https://github.com/dafny-lang/dafny/pull/2654)
 - fix: Better error reporting on counter-examples if an option is not provided (https://github.com/dafny-lang/dafny/pull/2650)
 
-
 # 3.8.0
 
 - fix: Use the right bitvector comparison in decrease checks

Source/Dafny/AST/DafnyAst.cs

@@ -6723,6 +6723,24 @@ public Statement(IToken tok, IToken endTok)
       Contract.Requires(endTok != null);
     }
 
+    /// <summary>
+    /// Returns the non-null expressions of this statement proper (that is, do not include the expressions of substatements).
+    /// Filters all sub expressions that are not part of specifications
+    /// </summary>
+    public IEnumerable<Expression> SubExpressionsIncludingTransitiveSubStatements {
+      get {
+        foreach (var e in SubExpressions) {
+          yield return e;
+        }
+
+        foreach (var s in SubStatements) {
+          foreach (var e in s.SubExpressionsIncludingTransitiveSubStatements) {
+            yield return e;
+          }
+        }
+      }
+    }
+
     /// <summary>
     /// Returns the non-null substatements of the Statements.
     /// </summary>
@@ -8759,7 +8777,7 @@ public TryRecoverStatement(Statement tryBody, IVariable haltMessageVar, Statemen
   // ------------------------------------------------------------------------------------------------------
 
   public abstract class TokenWrapper : IToken {
-    protected readonly IToken WrappedToken;
+    public readonly IToken WrappedToken;
     protected TokenWrapper(IToken wrappedToken) {
       Contract.Requires(wrappedToken != null);
       WrappedToken = wrappedToken;

Source/Dafny/AST/FreeVariablesUtil.cs

@@ -35,17 +35,20 @@ public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs) {
       bool dontCare0 = false, dontCare1 = false;
       Type dontCareT = null;
       var dontCareHeapAt = new HashSet<Label>();
-      ComputeFreeVariables(expr, fvs, ref dontCare0, ref dontCare1, dontCareHeapAt, ref dontCareT);
+      ComputeFreeVariables(expr, fvs, ref dontCare0, ref dontCare1, dontCareHeapAt, ref dontCareT, false);
     }
-    public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, ref bool usesHeap) {
+    public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, ref bool usesHeap, bool includeStatements = false) {
       Contract.Requires(expr != null);
       Contract.Requires(fvs != null);
       bool dontCare1 = false;
       Type dontCareT = null;
       var dontCareHeapAt = new HashSet<Label>();
-      ComputeFreeVariables(expr, fvs, ref usesHeap, ref dontCare1, dontCareHeapAt, ref dontCareT);
+      ComputeFreeVariables(expr, fvs, ref usesHeap, ref dontCare1, dontCareHeapAt, ref dontCareT, includeStatements);
     }
-    public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, ref bool usesHeap, ref bool usesOldHeap, ISet<Label> freeHeapAtVariables, ref Type usesThis) {
+    public static void ComputeFreeVariables(Expression expr,
+      ISet<IVariable> fvs,
+      ref bool usesHeap, ref bool usesOldHeap, ISet<Label> freeHeapAtVariables, ref Type usesThis,
+      bool includeStatements) {
       Contract.Requires(expr != null);
 
       if (expr is ThisExpr) {
@@ -113,8 +116,13 @@ public static void ComputeFreeVariables(Expression expr, ISet<IVariable> fvs, re
       // visit subexpressions
       bool uHeap = false, uOldHeap = false;
       Type uThis = null;
+      if (expr is StmtExpr stmtExpr && includeStatements) {
+        foreach (var subExpression in stmtExpr.S.SubExpressionsIncludingTransitiveSubStatements) {
+          ComputeFreeVariables(subExpression, fvs, ref uHeap, ref uOldHeap, freeHeapAtVariables, ref uThis, includeStatements);
+        }
+      }
       foreach (var subExpression in expr.SubExpressions) {
-        ComputeFreeVariables(subExpression, fvs, ref uHeap, ref uOldHeap, freeHeapAtVariables, ref uThis);
+        ComputeFreeVariables(subExpression, fvs, ref uHeap, ref uOldHeap, freeHeapAtVariables, ref uThis, includeStatements);
       }
       Contract.Assert(usesThis == null || uThis == null || usesThis.Equals(uThis));
       usesThis = usesThis ?? uThis;

Source/Dafny/Resolver.cs

@@ -441,6 +441,8 @@ public void ResolveProgram(Program prog) {
         rewriters.Add(new ConstructorWarning(reporter));
       }
 
+      rewriters.Add(new UselessOldLinter(reporter));
+
       foreach (var plugin in DafnyOptions.O.Plugins) {
         rewriters.AddRange(plugin.GetRewriters(reporter));
       }
@@ -10622,6 +10624,8 @@ void ResolveIterator(IteratorDecl iter) {
     void CreateIteratorMethodSpecs(IteratorDecl iter) {
       Contract.Requires(iter != null);
 
+      var tok = new AutoGeneratedToken(iter.tok);
+
       // ---------- here comes the constructor ----------
       // same requires clause as the iterator itself
       iter.Member_Init.Req.AddRange(iter.Requires);
@@ -10653,7 +10657,7 @@ void CreateIteratorMethodSpecs(IteratorDecl iter) {
       }
       ens.Add(new AttributedExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
         new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_reads"),
-        new OldExpr(iter.tok, frameSet))));
+        new OldExpr(tok, frameSet))));
       // ensures this._modifies == old(ModifiesClause);
       modSetSingletons = new List<Expression>();
       frameSet = new SetDisplayExpr(iter.tok, true, modSetSingletons);
@@ -10668,7 +10672,7 @@ void CreateIteratorMethodSpecs(IteratorDecl iter) {
       }
       ens.Add(new AttributedExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
         new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_modifies"),
-        new OldExpr(iter.tok, frameSet))));
+        new OldExpr(tok, frameSet))));
       // ensures this._new == {};
       ens.Add(new AttributedExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
         new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"),
@@ -10679,7 +10683,7 @@ void CreateIteratorMethodSpecs(IteratorDecl iter) {
         var p = iter.Decreases.Expressions[i];
         ens.Add(new AttributedExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq,
           new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), iter.DecreasesFields[i].Name),
-          new OldExpr(iter.tok, p))));
+          new OldExpr(tok, p))));
       }
 
       // ---------- here comes predicate Valid() ----------
@@ -10705,7 +10709,7 @@ void CreateIteratorMethodSpecs(IteratorDecl iter) {
       ens.Add(new AttributedExpression(new FreshExpr(iter.tok,
         new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub,
           new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"),
-          new OldExpr(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"))))));
+          new OldExpr(tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), "_new"))))));
       // ensures null !in _new
       ens.Add(new AttributedExpression(new BinaryExpr(iter.tok, BinaryExpr.Opcode.NotIn,
         new LiteralExpr(iter.tok),
@@ -10722,9 +10726,9 @@ void CreateIteratorMethodSpecs(IteratorDecl iter) {
         var ys = iter.OutsHistoryFields[i];
         var ite = new ITEExpr(iter.tok, false, new IdentifierExpr(iter.tok, "more"),
           new BinaryExpr(iter.tok, BinaryExpr.Opcode.Add,
-            new OldExpr(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)),
+            new OldExpr(tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)),
             new SeqDisplayExpr(iter.tok, new List<Expression>() { new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), y.Name) })),
-          new OldExpr(iter.tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)));
+          new OldExpr(tok, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name)));
         var eq = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Eq, new MemberSelectExpr(iter.tok, new ThisExpr(iter.tok), ys.Name), ite);
         ens.Add(new AttributedExpression(eq));
       }

Source/Dafny/Rewriter.cs

@@ -122,6 +122,16 @@ public AutoGeneratedToken(IToken wrappedToken)
       : base(wrappedToken) {
       Contract.Requires(wrappedToken != null);
     }
+
+    public static bool Is(IToken tok) {
+      while (tok is TokenWrapper w) {
+        if (w is AutoGeneratedToken) {
+          return true;
+        }
+        tok = w.WrappedToken;
+      }
+      return false;
+    }
   }
 
   public class TriggerGeneratingRewriter : IRewriter {

Source/Dafny/Triggers/TriggerUtils.cs

@@ -286,7 +286,7 @@ internal static IEnumerable<Expression> MaybeWrapInOld(Expression expr, HashSet<
       Contract.Requires(wrap == null || wrap.Count != 0);
       if (wrap != null && !(expr is NameSegment) && !(expr is IdentifierExpr)) {
         foreach (var w in wrap) {
-          var newExpr = new OldExpr(expr.tok, expr, w.At) { AtLabel = w.AtLabel };
+          var newExpr = new OldExpr(new AutoGeneratedToken(expr.tok), expr, w.At) { AtLabel = w.AtLabel };
           newExpr.Type = expr.Type;
           yield return newExpr;
         }

Source/Dafny/UselessOldLinter.cs

@@ -0,0 +1,51 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+//
+//-----------------------------------------------------------------------------
+using System.Collections.Generic;
+using System.Linq;
+using System.Reactive;
+
+namespace Microsoft.Dafny {
+
+  public class UselessOldLinter : IRewriter {
+    internal override void PostResolve(Program program) {
+      base.PostResolve(program);
+      foreach (var moduleDefinition in program.Modules()) {
+        foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType<TopLevelDeclWithMembers>()) {
+          foreach (var callable in topLevelDecl.Members.OfType<ICallable>()) {
+            var visitor = new UselessOldLinterVisitor(this.Reporter);
+            visitor.Visit(callable, Unit.Default);
+          }
+        }
+      }
+    }
+
+    public UselessOldLinter(ErrorReporter reporter) : base(reporter) {
+    }
+  }
+
+  class UselessOldLinterVisitor : TopDownVisitor<Unit> {
+    private readonly ErrorReporter reporter;
+
+    public UselessOldLinterVisitor(ErrorReporter reporter) {
+      this.reporter = reporter;
+    }
+
+    protected override bool VisitOneExpr(Expression expr, ref Unit st) {
+      if (expr is OldExpr oldExpr && !AutoGeneratedToken.Is(oldExpr.tok)) {
+        var fvs = new HashSet<IVariable>();
+        var usesHeap = false;
+        FreeVariablesUtil.ComputeFreeVariables(oldExpr.E, fvs, ref usesHeap, true);
+        if (!usesHeap) {
+          this.reporter.Warning(MessageSource.Rewriter, oldExpr.tok,
+            $"Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect");
+        }
+      }
+      return base.VisitOneExpr(expr, ref st);
+    }
+  }
+}

Source/Dafny/Verifier/Translator.cs

@@ -1968,7 +1968,7 @@ void AddFunctionAxiom(Bpl.Function boogieFunction, Function f, Expression body)
         bool dontCare0 = false, dontCare1 = false;
         var dontCareHeapAt = new HashSet<Label>();
         foreach (var e in f.Decreases.Expressions) {
-          FreeVariablesUtil.ComputeFreeVariables(e, FVs, ref dontCare0, ref dontCare1, dontCareHeapAt, ref usesThis);
+          FreeVariablesUtil.ComputeFreeVariables(e, FVs, ref dontCare0, ref dontCare1, dontCareHeapAt, ref usesThis, false);
         }
 
         var allFormals = new List<Formal>();
@@ -9129,7 +9129,7 @@ Expression LetDesugaring(LetExpr e) {
             bool usesHeap = false, usesOldHeap = false;
             var FVsHeapAt = new HashSet<Label>();
             Type usesThis = null;
-            FreeVariablesUtil.ComputeFreeVariables(e.RHSs[0], FVs, ref usesHeap, ref usesOldHeap, FVsHeapAt, ref usesThis);
+            FreeVariablesUtil.ComputeFreeVariables(e.RHSs[0], FVs, ref usesHeap, ref usesOldHeap, FVsHeapAt, ref usesThis, false);
             var FTVs = new HashSet<TypeParameter>();
             foreach (var bv in e.BoundVars) {
               FVs.Remove(bv);
@@ -10566,7 +10566,7 @@ public static bool UsesHeap(Expression expr) {
       bool usesHeap = false, usesOldHeap = false;
       var FVsHeapAt = new HashSet<Label>();
       Type usesThis = null;
-      FreeVariablesUtil.ComputeFreeVariables(expr, new HashSet<IVariable>(), ref usesHeap, ref usesOldHeap, FVsHeapAt, ref usesThis);
+      FreeVariablesUtil.ComputeFreeVariables(expr, new HashSet<IVariable>(), ref usesHeap, ref usesOldHeap, FVsHeapAt, ref usesThis, false);
       return usesHeap || usesOldHeap || FVsHeapAt.Count != 0;
     }
 

Test/VSComp2010/Problem4-Queens.dfy

@@ -74,7 +74,6 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard:
                   boardSoFar <= B
                   ==>
                   (exists p :: 0 <= p && p < N && !IsConsistent(B, p)));
-  ensures (forall B, p :: IsConsistent(B, p) <==> old(IsConsistent(B, p)));
   decreases N - |boardSoFar|;
 {
   var pos := |boardSoFar|;

Test/allocated1/dafny0/Simple.dfy.expect

@@ -105,5 +105,6 @@ module B refines A {
     ...;
   }
 }
+Simple.dfy(14,12): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 
 Dafny program verifier did not attempt verification

Test/allocated1/dafny0/SmallTests.dfy.expect

@@ -1,4 +1,5 @@
 SmallTests.dfy(548,4): Warning: /!\ No trigger covering all quantified variables found.
+SmallTests.dfy(599,12): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 SmallTests.dfy(34,11): Error: index out of range
 SmallTests.dfy(65,35): Error: possible division by zero
 SmallTests.dfy(66,50): Error: possible division by zero
@@ -52,5 +53,6 @@ SmallTests.dfy(716,8): Error: cannot establish the existence of LHS values that
 
 Dafny program verifier finished with 51 verified, 46 errors
 SmallTests.dfy.tmp.dprint.dfy(450,4): Warning: /!\ No trigger covering all quantified variables found.
+SmallTests.dfy.tmp.dprint.dfy(740,12): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 
 Dafny program verifier did not attempt verification

Test/allocated1/dafny0/Twostate-Verification.dfy.expect

@@ -1,3 +1,4 @@
+Twostate-Verification.dfy(34,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 Twostate-Verification.dfy(39,26): Error: target object might not be allocated
 Twostate-Verification.dfy(44,34): Error: target object might not be allocated
 Twostate-Verification.dfy(60,26): Error: target object might not be allocated

Test/concurrency/12-MutexLifetime-long.dfy

@@ -437,7 +437,6 @@ trait OwnedObject extends Object {
 
   twostate predicate unchangedNonvolatileFields() reads this {
     && old(owner) == owner
-    && old(lifetime) == lifetime
     && unchangedNonvolatileUserFields()
   }
 
@@ -454,7 +453,6 @@ trait OwnedObject extends Object {
 
   twostate predicate localInv2() reads * {
     && (owner != null ==> localUserInv2())
-    && old(lifetime) == lifetime
   }
 
   twostate predicate sequenceInv2() reads * {
@@ -690,16 +688,15 @@ class OutlivesClaim extends OwnedObject {
   function objectUserFields(): set<Object> reads this { { source, target } }
 
   twostate predicate unchangedNonvolatileUserFields() reads this {
-    && old(target) == target
-    && old(source) == source
+    true
   }
 
   predicate localUserInv() reads * {
     && objectGlobalBaseInv()
     && universe.outlives(target, source)
   }
   predicate userInv() reads * ensures userInv() ==> localUserInv() { localUserInv() }
-  twostate predicate localUserInv2() reads * { old(target) == target && old(source) == source }
+  twostate predicate localUserInv2() reads * { true }
   twostate predicate userInv2() reads * ensures userInv2() ==> localUserInv2() { localUserInv2() }
 
   twostate lemma sequenceAdmissibility(running: set<Thread>) requires goodPreAndLegalChangesSequence(running) ensures sequenceInv2() {}

Test/concurrency/12-MutexLifetime-short.dfy

@@ -436,7 +436,6 @@ trait OwnedObject extends Object {
 
   twostate predicate unchangedNonvolatileFields() reads this {
     && old(owner) == owner
-    && old(lifetime) == lifetime
     && unchangedNonvolatileUserFields()
   }
 
@@ -453,7 +452,6 @@ trait OwnedObject extends Object {
 
   twostate predicate localInv2() reads * {
     && (owner != null ==> localUserInv2())
-    && old(lifetime) == lifetime
   }
 
   twostate predicate sequenceInv2() reads * {
@@ -689,16 +687,15 @@ class OutlivesClaim extends OwnedObject {
   function objectUserFields(): set<Object> reads this { { source, target } }
 
   twostate predicate unchangedNonvolatileUserFields() reads this {
-    && old(target) == target
-    && old(source) == source
+    true
   }
 
   predicate localUserInv() reads * {
     && objectGlobalBaseInv()
     && universe.outlives(target, source)
   }
   predicate userInv() reads * ensures userInv() ==> localUserInv() { localUserInv() }
-  twostate predicate localUserInv2() reads * { old(target) == target && old(source) == source }
+  twostate predicate localUserInv2() reads * { true }
   twostate predicate userInv2() reads * ensures userInv2() ==> localUserInv2() { localUserInv2() }
 
   twostate lemma sequenceAdmissibility(running: set<Thread>) requires goodPreAndLegalChangesSequence(running) ensures sequenceInv2() {}

Test/concurrency/12-MutexLifetime-short.dfy.expect

@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 204 verified, 0 errors
+Dafny program verifier finished with 202 verified, 0 errors

Test/dafny0/LabeledAsserts.dfy.expect

@@ -1,3 +1,5 @@
+LabeledAsserts.dfy(63,9): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
+LabeledAsserts.dfy(63,30): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 LabeledAsserts.dfy(25,11): Error: assertion might not hold
 LabeledAsserts.dfy(27,18): Error: assertion might not hold
 LabeledAsserts.dfy(28,18): Error: assertion might not hold

Test/dafny0/LabelsOldAt.dfy.expect

@@ -1,3 +1,4 @@
+LabelsOldAt.dfy(160,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 LabelsOldAt.dfy(34,13): Error: assertion might not hold
 LabelsOldAt.dfy(56,11): Error: assertion might not hold
 LabelsOldAt.dfy(78,13): Error: assertion might not hold