From 0881783917faabf8955e670a09787a5884e505f9 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 15 Aug 2022 16:42:45 -0700 Subject: [PATCH 01/15] snapshot --- Source/Dafny/AST/DafnyAst.cs | 2 +- Source/Dafny/Linter.cs | 51 +++++ Source/Dafny/Resolver.cs | 16 +- Source/Dafny/Rewriter.cs | 10 + Source/Dafny/Triggers/TriggerUtils.cs | 2 +- Test/VSComp2010/Problem4-Queens.dfy | 1 - Test/dafny0/LabeledAsserts.dfy.expect | 2 + Test/dafny0/LabelsOldAt.dfy.expect | 1 + Test/dafny0/OpaqueTypeWithMembers.dfy | 6 +- Test/dafny0/OpaqueTypeWithMembers.dfy.expect | 3 + Test/dafny0/Simple.dfy | 2 +- Test/dafny0/Simple.dfy.expect | 1 + Test/dafny0/SmallTests.dfy.expect | 2 + Test/dafny0/Twostate-Verification.dfy | 46 ++-- Test/dafny0/Twostate-Verification.dfy.expect | 23 ++ Test/git-issues/git-issue-1989.dfy | 225 +++++++++++++++++++ 16 files changed, 357 insertions(+), 36 deletions(-) create mode 100644 Source/Dafny/Linter.cs create mode 100644 Test/git-issues/git-issue-1989.dfy diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 4e621620fc4..e08830d72b5 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -8746,7 +8746,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; diff --git a/Source/Dafny/Linter.cs b/Source/Dafny/Linter.cs new file mode 100644 index 00000000000..e480c16205f --- /dev/null +++ b/Source/Dafny/Linter.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 { + + class Linter : IRewriter { + internal override void PostResolve(Program program) { + base.PostResolve(program); + foreach (var moduleDefinition in program.Modules()) { + foreach (var topLevelDecl in moduleDefinition.TopLevelDecls.OfType()) { + foreach (var callable in topLevelDecl.Members.OfType()) { + var visitor = new LinterVisitor(this.Reporter); + visitor.Visit(callable, Unit.Default); + } + } + } + } + + public Linter(ErrorReporter reporter) : base(reporter) { + } + } + + class LinterVisitor : TopDownVisitor { + private readonly ErrorReporter reporter; + + public LinterVisitor(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(); + var usesHeap = false; + FreeVariablesUtil.ComputeFreeVariables(oldExpr.E, fvs, ref usesHeap); + 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); + } + } +} diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 64b8bf1ed1a..fa6686506eb 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -442,6 +442,8 @@ public void ResolveProgram(Program prog) { rewriters.Add(new ConstructorWarning(reporter)); } + rewriters.Add(new Linter(reporter)); + foreach (var plugin in DafnyOptions.O.Plugins) { rewriters.AddRange(plugin.GetRewriters(reporter)); } @@ -10575,6 +10577,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); @@ -10606,7 +10610,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(); frameSet = new SetDisplayExpr(iter.tok, true, modSetSingletons); @@ -10621,7 +10625,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"), @@ -10632,7 +10636,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() ---------- @@ -10658,7 +10662,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), @@ -10675,9 +10679,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() { 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)); } diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index a549d819b37..6b8350077d7 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -121,6 +121,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 { diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index eb4898378f1..6f0c6f21c2c 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -286,7 +286,7 @@ internal static IEnumerable 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; } diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy index 3d676f06dcc..02dabbcd57f 100644 --- a/Test/VSComp2010/Problem4-Queens.dfy +++ b/Test/VSComp2010/Problem4-Queens.dfy @@ -74,7 +74,6 @@ method SearchAux(N: int, boardSoFar: seq) 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|; diff --git a/Test/dafny0/LabeledAsserts.dfy.expect b/Test/dafny0/LabeledAsserts.dfy.expect index 62dff815b92..508bd8a60ae 100644 --- a/Test/dafny0/LabeledAsserts.dfy.expect +++ b/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 diff --git a/Test/dafny0/LabelsOldAt.dfy.expect b/Test/dafny0/LabelsOldAt.dfy.expect index fdce8098d24..d00a750700a 100644 --- a/Test/dafny0/LabelsOldAt.dfy.expect +++ b/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 diff --git a/Test/dafny0/OpaqueTypeWithMembers.dfy b/Test/dafny0/OpaqueTypeWithMembers.dfy index aec2a4b7e96..4452fcc06c9 100644 --- a/Test/dafny0/OpaqueTypeWithMembers.dfy +++ b/Test/dafny0/OpaqueTypeWithMembers.dfy @@ -23,7 +23,7 @@ type Opaque { ensures old(a[3] + y) == y { u := old(y + a[3]); - var f := old(F()); + var f := old(F()); // warning: old has no effect (since F has no reads clause) var u' := y + a[3]; var f' := F(); } @@ -61,7 +61,7 @@ type StaticOpaque { ensures old(a[3] + y) == y { u := old(y + a[3]); - var f := old(F()); + var f := old(F()); // warning: old has no effect (since F has no reads clause) var u' := y + a[3]; var f' := F(); } @@ -91,7 +91,7 @@ type OpaqueErrors { ensures old(a[3] + y) == y { u := old(y + a[2]); // error: index out of bounds - var f := old(F()); + var f := old(F()); // warning: old has no effect (since F has no reads clause) var u' := y + a[2]; var f' := F(); } diff --git a/Test/dafny0/OpaqueTypeWithMembers.dfy.expect b/Test/dafny0/OpaqueTypeWithMembers.dfy.expect index 8d29e6e1bda..558bacdaaac 100644 --- a/Test/dafny0/OpaqueTypeWithMembers.dfy.expect +++ b/Test/dafny0/OpaqueTypeWithMembers.dfy.expect @@ -1,3 +1,6 @@ +OpaqueTypeWithMembers.dfy(26,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +OpaqueTypeWithMembers.dfy(64,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +OpaqueTypeWithMembers.dfy(94,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect OpaqueTypeWithMembers.dfy(83,36): Error: possible division by zero OpaqueTypeWithMembers.dfy(84,51): Error: possible division by zero OpaqueTypeWithMembers.dfy(87,9): Error: index out of range diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index 6fdd7bc3530..b56282d2370 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -11,7 +11,7 @@ class MyClass { requires s; modifies this, lotsaObjects; ensures t == t; - ensures old(null) != this; + ensures old(null) != this; // warning: old(null) is the same as null { x := 12; while (x < 100) diff --git a/Test/dafny0/Simple.dfy.expect b/Test/dafny0/Simple.dfy.expect index 54a1bc8c277..1e90daa15d3 100644 --- a/Test/dafny0/Simple.dfy.expect +++ b/Test/dafny0/Simple.dfy.expect @@ -105,5 +105,6 @@ greatest lemma M'(x': int) ensures true { } +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 diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index 5f0e952f225..a5be04cf8c8 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/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(909,14): Error: target object might be null SmallTests.dfy(901,14): Error: target object might be null SmallTests.dfy(34,11): Error: index out of range @@ -54,5 +55,6 @@ SmallTests.dfy(716,8): Error: cannot establish the existence of LHS values that Dafny program verifier finished with 56 verified, 48 errors SmallTests.dfy.tmp.dprint.dfy(450,4): Warning: /!\ No trigger covering all quantified variables found. +SmallTests.dfy.tmp.dprint.dfy(803,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 diff --git a/Test/dafny0/Twostate-Verification.dfy b/Test/dafny0/Twostate-Verification.dfy index 357439c7adb..d20cf1dc66e 100644 --- a/Test/dafny0/Twostate-Verification.dfy +++ b/Test/dafny0/Twostate-Verification.dfy @@ -30,7 +30,7 @@ class A { } twostate lemma L2(a: A, b: A) - requires old(a != b) + requires old(a != b) // warning: old has no effect {} twostate lemma L3(a: A, new b: A) @@ -653,33 +653,33 @@ module TwoStateAt { label Label: if * { - ghost var f0 := old(d0.value); - ghost var f1 := old(nt.value); - ghost var f2 := old(ot.value); - ghost var f3 := old(d1.value); // error: receiver is not in old state + ghost var f0 := old(d0.value); // warning: old has no effect + ghost var f1 := old(nt.value); // warning: old has no effect + ghost var f2 := old(ot.value); // warning: old has no effect + ghost var f3 := old(d1.value); // error: receiver is not in old state (warning: old has no effect) } else if * { - ghost var g0 := old(DT.sc); - ghost var g1 := old(NT.sc); - ghost var g2 := old(OT.sc); + ghost var g0 := old(DT.sc); // warning: old has no effect + ghost var g1 := old(NT.sc); // warning: old has no effect + ghost var g2 := old(OT.sc); // warning: old has no effect } else if * { - ghost var h0 := old(d0.sc); - ghost var h1 := old(nt.sc); - ghost var h2 := old(ot.sc); - ghost var h3 := old(d1.sc); // this is also fine + ghost var h0 := old(d0.sc); // warning: old has no effect + ghost var h1 := old(nt.sc); // warning: old has no effect + ghost var h2 := old(ot.sc); // warning: old has no effect + ghost var h3 := old(d1.sc); // this is also fine (warning: old has no effect) } else if * { - ghost var f0 := old@Label(d0.value); - ghost var f1 := old@Label(nt.value); - ghost var f2 := old@Label(ot.value); - ghost var f3 := old@Label(d1.value); // fine + ghost var f0 := old@Label(d0.value); // warning: old has no effect + ghost var f1 := old@Label(nt.value); // warning: old has no effect + ghost var f2 := old@Label(ot.value); // warning: old has no effect + ghost var f3 := old@Label(d1.value); // fine (warning: old has no effect) } else if * { - ghost var g0 := old@Label(DT.sc); - ghost var g1 := old@Label(NT.sc); - ghost var g2 := old@Label(OT.sc); + ghost var g0 := old@Label(DT.sc); // warning: old has no effect + ghost var g1 := old@Label(NT.sc); // warning: old has no effect + ghost var g2 := old@Label(OT.sc); // warning: old has no effect } else if * { - ghost var h0 := old@Label(d0.sc); - ghost var h1 := old@Label(nt.sc); - ghost var h2 := old@Label(ot.sc); - ghost var h3 := old@Label(d1.sc); + ghost var h0 := old@Label(d0.sc); // warning: old has no effect + ghost var h1 := old@Label(nt.sc); // warning: old has no effect + ghost var h2 := old@Label(ot.sc); // warning: old has no effect + ghost var h3 := old@Label(d1.sc); // warning: old has no effect } } } diff --git a/Test/dafny0/Twostate-Verification.dfy.expect b/Test/dafny0/Twostate-Verification.dfy.expect index d627df2ecb2..8815ae6a4e1 100644 --- a/Test/dafny0/Twostate-Verification.dfy.expect +++ b/Test/dafny0/Twostate-Verification.dfy.expect @@ -1,3 +1,26 @@ +Twostate-Verification.dfy(656,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(657,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(658,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(659,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(661,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(662,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(663,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(665,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(666,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(667,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(668,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(670,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(671,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(672,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(673,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(675,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(676,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(677,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(679,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(680,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(681,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(682,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect +Twostate-Verification.dfy(33,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect Twostate-Verification.dfy(271,13): Error: A postcondition might not hold on this return path. Twostate-Verification.dfy(263,24): Related location: This is the postcondition that might not hold. Twostate-Verification.dfy(277,4): Error: A postcondition might not hold on this return path. diff --git a/Test/git-issues/git-issue-1989.dfy b/Test/git-issues/git-issue-1989.dfy new file mode 100644 index 00000000000..afb50686b2a --- /dev/null +++ b/Test/git-issues/git-issue-1989.dfy @@ -0,0 +1,225 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// --------------------------------------- + +module Test { + class C { + } + + function arrSet(a: array): set + reads a + { + set i : int | 0 <= i < a.Length :: a[i] + } + + method test(a: array, i: int, x: C) + modifies a + requires 0 <= i < a.Length + requires x !in arrSet(a) + { + a[i] := x; + assert arrSet(a) == arrSet(old(a)); // warning: old has no effect + } +} + +// --------------------------------------- + +predicate P(s: seq) +predicate Q(a: array) + reads a + +class C { + var x: int + + predicate PInClass(s: seq) + static predicate StaticPInClass(s: seq) + + predicate QInClass(a: array) + reads a + static predicate StaticQInClass(a: array) + reads a + + predicate R(y: int := x) + reads this +} + +method TestsNoReads(c: C, s: seq, a: array) { + ghost var b; + b := old(P(s)); // warning: old has no effect + b := old(c.PInClass(s)); // warning: old has no effect + b := old(C.StaticPInClass(s)); // warning: old has no effect + b := old(c.StaticPInClass(s)); // warning: old has no effect + + b := old(Q(a)); + b := old(c.QInClass(a)); + b := old(C.StaticQInClass(a)); + b := old(c.StaticQInClass(a)); + + b := old(c.R(3)); + b := old(c.R()); +} + +method Trigger() + // The following should generate a warning, but preferably not two. + // That is, if the old expression is copied into the trigger, it + // is preferable that there's not a second warning for the 'old' there. + ensures forall s :: P(s) == old(P(s)) // warning: old has no effect + + // A manually supplied trigger should have its own warning, though: + ensures forall s {:trigger old(P(s))} :: P(s) == old(P(s)) // warning (x2): old has no effect +{ +} + +// An iterator has several auto-generated old expressions. +// These should not generate any warnings. +iterator Iter() +{ +} + +// --------------------------------------- + +class D { + var data: int + const N: int + var arr: array + + method TestFields() + ensures data == old(data) + ensures N == old(N) // warning: old has no effect + { + } + + method TestArrayElements(j: nat, a: array) + requires j < a.Length + ensures a.Length == old(a.Length) // warning: old has no effect + ensures a[j] == old(a[j]) + ensures a[j] == old(a)[j] // warning: old has no effect + ensures a[j] == a[old(j)] // warning: old has no effect + { + } + + method MoreArrays(b: array) + requires 0 <= data && data + 1 < arr.Length == b.Length + requires 1.0 <= arr[data] < arr[data + 1] < 2.0 + requires 4.0 <= b[data] < b[data + 1] < 5.0 + modifies this, arr + ensures arr == b && data == old(data) + 1 + ensures arr[data] != old(arr[data]) + ensures arr[data] != old(arr)[data] + ensures arr[data] != arr[old(data)] + ensures var a, j := arr, data; old(arr[data]) != old(a[j]) + { + forall i | 0 <= i < arr.Length { + arr[i] := 2.0 * arr[i]; + } + arr := b; + data := data + 1; + } + + method TestMatrixElements(i: nat, j: nat, m: array2) + requires i < m.Length0 && j < m.Length1 + ensures m.Length0 == old(m.Length1) // warning: old has no effect + ensures m[i, j] == old(m[i, j]) + ensures m[i, j] == old(m)[i, j] // warning: old has no effect + ensures m[i, j] == m[i, old(j)] // warning: old has no effect + { + } + + lemma Lemma(y: int) + requires data == y + { + } +} + +// --------------------------------------- + +method StmtExpr(d: D) + requires d.data == 3 + modifies d +{ + ghost var a; + d.data := 100; + if { + case true => + a := assert d.data < 5; 10; // error: assertion failure + case true => + a := old(20 + assert d.data < 5; 10); + case true => + a := old(d.Lemma(3); 10); + case true => + a := old(d.Lemma(100); 10); // error: precondition violation + case true => + a := (d.Lemma(old(100)); 10); // warning: old has no effect + } + a := assert d.data < old(105); 0; // warning: old has no effect +} + +method CalcStmtExpr(d: D) + requires d.data == 3 + modifies d +{ + ghost var a; + d.data := 100; + if { + case true => + a := old(calc { } 10); // warning: old has no effect (but this is hard to determine) + case true => + a := old(calc { + 2; + == { assert d.data == 3; } + 2; + } 10); // warning: old has no effect + case true => + a := old(calc { + 2; + == { assert d.data == 100; } // error: assertion violation + 2; + } 10); // warning: old has no effect + case true => + a := old(calc { + 2; + == { d.Lemma(3); } + 2; + } 10); // warning: old has no effect + case true => + a := old(calc { + 2; + == { d.Lemma(100); } // error: precondition violation + 2; + } 10); // warning: old has no effect + } +} + +twostate function CalcStmtExprFunction(d: D, selector: int): int + requires old(d.data) == 3 && d.data == 100 +{ + match selector + case 0 => + old(calc { } 10) // warning: old has no effect (but this is hard to determine) + case 1 => + a := old(calc { + 2; + == { assert d.data == 3; } + 2; + } 10); // warning: old has no effect + case 2 => + a := old(calc { + 2; + == { assert d.data == 100; } // error: assertion violation + 2; + } 10); // warning: old has no effect + case true => + a := old(calc { + 2; + == { d.Lemma(3); } + 2; + } 10); // warning: old has no effect + case true => + a := old(calc { + 2; + == { d.Lemma(100); } // error: precondition violation + 2; + } 10); // warning: old has no effect + } +} From a341eca079f20c033bdb6c237790f747b89b2ea7 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 17 Aug 2022 09:23:02 -0700 Subject: [PATCH 02/15] Enhance two-state detection in resolver --- Source/Dafny/Resolver.cs | 22 ++++-- Test/git-issues/git-issue-2597-resolution.dfy | 69 +++++++++++++++++++ .../git-issue-2597-resolution.dfy.expect | 10 +++ 3 files changed, 95 insertions(+), 6 deletions(-) create mode 100644 Test/git-issues/git-issue-2597-resolution.dfy create mode 100644 Test/git-issues/git-issue-2597-resolution.dfy.expect diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 64b8bf1ed1a..c29bdccdf48 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -9152,8 +9152,11 @@ bool InferRequiredEqualitySupport(TypeParameter tp, Type type) { readonly Scope/*!*/ scope = new Scope(); Scope/*!*/ enclosingStatementLabels = new Scope(); readonly Scope