From b43f9489e0d00ceadce81ee1b8ab216ebb74a474 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 24 Jun 2022 16:42:25 -0700 Subject: [PATCH 1/5] fix: Substitute for heap labels in TrSplitExpr Fixes #2299 --- Source/Dafny/Substituter.cs | 34 +++--- Source/Dafny/Verifier/Translator.cs | 7 +- Test/git-issues/git-issue-2299.dfy | 123 ++++++++++++++++++++++ Test/git-issues/git-issue-2299.dfy.expect | 19 ++++ 4 files changed, 164 insertions(+), 19 deletions(-) create mode 100644 Test/git-issues/git-issue-2299.dfy create mode 100644 Test/git-issues/git-issue-2299.dfy.expect diff --git a/Source/Dafny/Substituter.cs b/Source/Dafny/Substituter.cs index bae836842dc..888d4b0be58 100644 --- a/Source/Dafny/Substituter.cs +++ b/Source/Dafny/Substituter.cs @@ -9,18 +9,20 @@ namespace Microsoft.Dafny { /// particular, the substituter does not copy parts of an expression that are used only for well-formedness checks. /// public class Substituter { - public readonly Expression receiverReplacement; - public readonly Dictionary/*!*/ substMap; - public readonly Dictionary/*!*/ typeMap; + protected readonly Expression receiverReplacement; + protected readonly Dictionary substMap; + protected readonly Dictionary typeMap; + protected readonly Label oldLabel; public static readonly Substituter EMPTY = new Substituter(null, new Dictionary(), new Dictionary()); - public Substituter(Expression receiverReplacement, Dictionary/*!*/ substMap, Dictionary typeMap) { + public Substituter(Expression receiverReplacement, Dictionary substMap, Dictionary typeMap, Label oldLabel = null) { Contract.Requires(substMap != null); Contract.Requires(typeMap != null); this.receiverReplacement = receiverReplacement; this.substMap = substMap; this.typeMap = typeMap; + this.oldLabel = oldLabel; } public virtual Expression Substitute(Expression expr) { Contract.Requires(expr != null); @@ -84,13 +86,13 @@ public virtual Expression Substitute(Expression expr) { newExpr = new MapDisplayExpr(expr.tok, e.Finite, elmts); } } else if (expr is MemberSelectExpr) { - MemberSelectExpr fse = (MemberSelectExpr)expr; - Expression substE = Substitute(fse.Obj); - MemberSelectExpr fseNew = new MemberSelectExpr(fse.tok, substE, fse.MemberName); - fseNew.Member = fse.Member; - fseNew.TypeApplication_AtEnclosingClass = fse.TypeApplication_AtEnclosingClass.ConvertAll(t => Resolver.SubstType(t, typeMap)); - fseNew.TypeApplication_JustMember = fse.TypeApplication_JustMember.ConvertAll(t => Resolver.SubstType(t, typeMap)); - fseNew.AtLabel = fse.AtLabel; + var mse = (MemberSelectExpr)expr; + Expression substE = Substitute(mse.Obj); + MemberSelectExpr fseNew = new MemberSelectExpr(mse.tok, substE, mse.MemberName); + fseNew.Member = mse.Member; + fseNew.TypeApplication_AtEnclosingClass = mse.TypeApplication_AtEnclosingClass.ConvertAll(t => Resolver.SubstType(t, typeMap)); + fseNew.TypeApplication_JustMember = mse.TypeApplication_JustMember.ConvertAll(t => Resolver.SubstType(t, typeMap)); + fseNew.AtLabel = mse.AtLabel ?? oldLabel; newExpr = fseNew; } else if (expr is SeqSelectExpr) { SeqSelectExpr sse = (SeqSelectExpr)expr; @@ -118,7 +120,7 @@ public virtual Expression Substitute(Expression expr) { } } else if (expr is FunctionCallExpr) { - FunctionCallExpr e = (FunctionCallExpr)expr; + var e = (FunctionCallExpr)expr; Expression receiver = Substitute(e.Receiver); List newArgs = SubstituteExprList(e.Args); var newTypeApplicationAtEnclosingClass = SubstituteTypeList(e.TypeApplication_AtEnclosingClass); @@ -126,7 +128,7 @@ public virtual Expression Substitute(Expression expr) { if (receiver != e.Receiver || newArgs != e.Args || newTypeApplicationAtEnclosingClass != e.TypeApplication_AtEnclosingClass || newTypeApplicationJustFunction != e.TypeApplication_JustFunction) { - FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs, e.AtLabel); + FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs, e.AtLabel ?? oldLabel); newFce.Function = e.Function; // resolve on the fly (and set newFce.Type below, at end) newFce.CoCall = e.CoCall; // also copy the co-call status newFce.CoCallHint = e.CoCallHint; // and any co-call hint @@ -161,7 +163,7 @@ public virtual Expression Substitute(Expression expr) { // BoogieWrapper before calling Substitute. Expression se = Substitute(e.E); if (se != e.E) { - newExpr = new OldExpr(expr.tok, se, e.At) { AtLabel = e.AtLabel }; + newExpr = new OldExpr(expr.tok, se, e.At) { AtLabel = e.AtLabel ?? oldLabel }; } } else if (expr is UnchangedExpr) { var e = (UnchangedExpr)expr; @@ -175,7 +177,7 @@ public virtual Expression Substitute(Expression expr) { fr.Add(fefe); } if (anythingChanged) { - newExpr = new UnchangedExpr(e.tok, fr, e.At) { AtLabel = e.AtLabel }; + newExpr = new UnchangedExpr(e.tok, fr, e.At) { AtLabel = e.AtLabel ?? oldLabel }; } } else if (expr is SeqConstructionExpr) { var e = (SeqConstructionExpr)expr; @@ -202,7 +204,7 @@ public virtual Expression Substitute(Expression expr) { if (se != e.E) { if (e is FreshExpr) { var ee = (FreshExpr)e; - newExpr = new FreshExpr(expr.tok, se, ee.At) { AtLabel = ee.AtLabel }; + newExpr = new FreshExpr(expr.tok, se, ee.At) { AtLabel = ee.AtLabel ?? oldLabel }; } else if (e is UnaryOpExpr) { var ee = (UnaryOpExpr)e; newExpr = new UnaryOpExpr(expr.tok, ee.Op, se); diff --git a/Source/Dafny/Verifier/Translator.cs b/Source/Dafny/Verifier/Translator.cs index 3b2dde5e23e..536a6c73f45 100644 --- a/Source/Dafny/Verifier/Translator.cs +++ b/Source/Dafny/Verifier/Translator.cs @@ -11668,7 +11668,7 @@ private Expression GetSubstitutedBody(FunctionCallExpr fexp, Function f) { var pp = (PrefixPredicate)f; body = PrefixSubstitution(pp, body); } - body = Substitute(body, fexp.Receiver, substMap, fexp.GetTypeArgumentSubstitutions()); + body = Substitute(body, fexp.Receiver, substMap, fexp.GetTypeArgumentSubstitutions(), fexp.AtLabel); return body; } @@ -11815,11 +11815,12 @@ public static Expression Substitute(Expression expr, IVariable v, Expression e) return Substitute(expr, null, substMap); } - public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary/*!*/ substMap, Dictionary/*?*/ typeMap = null) { + public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary/*!*/ substMap, + Dictionary typeMap = null, Label oldLabel = null) { Contract.Requires(expr != null); Contract.Requires(cce.NonNullDictionaryAndValues(substMap)); Contract.Ensures(Contract.Result() != null); - var s = new Substituter(receiverReplacement, substMap, typeMap ?? new Dictionary()); + var s = new Substituter(receiverReplacement, substMap, typeMap ?? new Dictionary(), oldLabel); return s.Substitute(expr); } diff --git a/Test/git-issues/git-issue-2299.dfy b/Test/git-issues/git-issue-2299.dfy new file mode 100644 index 00000000000..b8fa3d63d8b --- /dev/null +++ b/Test/git-issues/git-issue-2299.dfy @@ -0,0 +1,123 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +class Twostate { + var z: int + + twostate predicate Increase() + reads this + { + old(z) <= z + } + + twostate predicate NoChange() + reads this + { + unchanged(this) + } + + static twostate predicate IsFresh(new c: Twostate) + { + fresh(c) + } + + twostate predicate All(new c: Twostate) + reads this + { + Increase() && NoChange() && IsFresh(c) + } + + method Test0() + modifies this + { + z := z + 1; + label L: + z := z - 1; + // the following line was once translated incorrectly without the @L + assert Increase@L(); // error: does not hold + assert false; + } + + method Test1() + modifies this + { + z := z + 1; + label L: + z := z - 1; + // the following line was once translated incorrectly without the @L + assert NoChange@L(); // error: does not hold + } + + method Test2() + modifies this + { + z := z + 1; + label L: + z := z - 1; + // the following line was once translated incorrectly without the @L + assert IsFresh@L(this); // error: does not hold + } + + method Test3() + { + var c := new Twostate; + label L: + if * { + // the following line was once translated incorrectly without the @L + assert IsFresh@L(c); // error: does not hold + } else { + assert IsFresh(c); + } + } + + method Test4() + modifies this + { + var c := new Twostate; + z := z + 1; + label L: + z := z - 1; + // the following line was once translated incorrectly without the @L + assert All@L(c); // error: does not hold + } + + method Test5(k: nat) + modifies this + { + z := z + k; + label L: + var c := new Twostate; + + assert Increase@L(); + assert NoChange@L(); + assert IsFresh@L(c); + + assert Increase(); + if k == 0 { + assert NoChange(); + } + assert IsFresh(c); + } + + method Test6() + modifies this + { + z := z + 1; + var c := new Twostate; + label L: + z := z - 1; + + assert Increase(); + assert NoChange(); + assert IsFresh(c); + } + + method Test7() + modifies this + { + z := z + 1; + label L: + var c := new Twostate; + assert All@L(c); + } +} diff --git a/Test/git-issues/git-issue-2299.dfy.expect b/Test/git-issues/git-issue-2299.dfy.expect new file mode 100644 index 00000000000..62c78b453ca --- /dev/null +++ b/Test/git-issues/git-issue-2299.dfy.expect @@ -0,0 +1,19 @@ +git-issue-2299.dfy(37,11): Error: assertion might not hold +git-issue-2299.dfy(10,11): Related location +git-issue-2299.dfy(48,11): Error: assertion might not hold +git-issue-2299.dfy(16,4): Related location +git-issue-2299.dfy(58,11): Error: assertion might not hold +git-issue-2299.dfy(21,4): Related location +git-issue-2299.dfy(67,13): Error: assertion might not hold +git-issue-2299.dfy(21,4): Related location +git-issue-2299.dfy(81,11): Error: assertion might not hold +git-issue-2299.dfy(27,4): Related location +git-issue-2299.dfy(10,11): Related location +git-issue-2299.dfy(81,11): Error: assertion might not hold +git-issue-2299.dfy(27,18): Related location +git-issue-2299.dfy(16,4): Related location +git-issue-2299.dfy(81,11): Error: assertion might not hold +git-issue-2299.dfy(27,32): Related location +git-issue-2299.dfy(21,4): Related location + +Dafny program verifier finished with 6 verified, 7 errors From db6294c192d1934000024008fda5062bdf59fd6f Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 24 Jun 2022 16:44:39 -0700 Subject: [PATCH 2/5] fix: Recognize heap labels as free vars (MultiSelectExpr and FunctionCallExpr) --- Source/Dafny/AST/FreeVariablesUtil.cs | 10 ++++++++-- Test/git-issues/git-issue-2299.dfy | 12 ++++++++++++ Test/git-issues/git-issue-2299.dfy.expect | 2 +- 3 files changed, 21 insertions(+), 3 deletions(-) diff --git a/Source/Dafny/AST/FreeVariablesUtil.cs b/Source/Dafny/AST/FreeVariablesUtil.cs index a259cbd42da..bc0a4ef9229 100644 --- a/Source/Dafny/AST/FreeVariablesUtil.cs +++ b/Source/Dafny/AST/FreeVariablesUtil.cs @@ -61,6 +61,9 @@ public static void ComputeFreeVariables(Expression expr, ISet fvs, re if (e.Obj.Type.IsRefType && !(e.Member is ConstantField)) { usesHeap = true; } + if (e.AtLabel != null) { + freeHeapAtVariables.Add(e.AtLabel); + } } else if (expr is SeqSelectExpr) { var e = (SeqSelectExpr)expr; if (e.Seq.Type.IsArrayType) { @@ -74,10 +77,13 @@ public static void ComputeFreeVariables(Expression expr, ISet fvs, re } else if (expr is MultiSelectExpr) { usesHeap = true; } else if (expr is FunctionCallExpr) { - Function f = ((FunctionCallExpr)expr).Function; - if (Translator.AlwaysUseHeap || f == null || f.ReadsHeap) { + var e = (FunctionCallExpr)expr; + if (Translator.AlwaysUseHeap || e.Function == null || e.Function.ReadsHeap) { usesHeap = true; } + if (e.AtLabel != null) { + freeHeapAtVariables.Add(e.AtLabel); + } } else if (expr is UnchangedExpr) { var e = (UnchangedExpr)expr; // Note, we don't have to look out for const fields here, because const fields diff --git a/Test/git-issues/git-issue-2299.dfy b/Test/git-issues/git-issue-2299.dfy index b8fa3d63d8b..02394dd32f3 100644 --- a/Test/git-issues/git-issue-2299.dfy +++ b/Test/git-issues/git-issue-2299.dfy @@ -120,4 +120,16 @@ class Twostate { var c := new Twostate; assert All@L(c); } + + method FreeHeapAtVariables() + modifies this + { + z := z + 1; + label L: + z := z - 1; + ghost var x; + // regression: the following line once led to malformed Boogie + x := var u :| u == Increase@L(); !u; + assert x; + } } diff --git a/Test/git-issues/git-issue-2299.dfy.expect b/Test/git-issues/git-issue-2299.dfy.expect index 62c78b453ca..42594dbd7f1 100644 --- a/Test/git-issues/git-issue-2299.dfy.expect +++ b/Test/git-issues/git-issue-2299.dfy.expect @@ -16,4 +16,4 @@ git-issue-2299.dfy(81,11): Error: assertion might not hold git-issue-2299.dfy(27,32): Related location git-issue-2299.dfy(21,4): Related location -Dafny program verifier finished with 6 verified, 7 errors +Dafny program verifier finished with 7 verified, 7 errors From 5588e02db627f04e1825479c85f2d62dcdabb772 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 24 Jun 2022 16:58:24 -0700 Subject: [PATCH 3/5] Use newfangled way to call dafny from test file --- Test/git-issues/git-issue-2299.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/git-issues/git-issue-2299.dfy b/Test/git-issues/git-issue-2299.dfy index 02394dd32f3..5573f2f0daa 100644 --- a/Test/git-issues/git-issue-2299.dfy +++ b/Test/git-issues/git-issue-2299.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny_0 /compile:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class Twostate { From b19543a3229cdd6c49aee46a1551c417a2009564 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 24 Jun 2022 17:01:46 -0700 Subject: [PATCH 4/5] Add release notes --- RELEASE_NOTES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 8e267decbd4..226b5f7a581 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,5 +1,7 @@ # Upcoming +- fix: Fix bug in translation of two-state predicates with heap labels. (https://github.com/dafny-lang/dafny/pull/2300) + # 3.7.1 - fix: The Dafny runtime library for C# is now compatible with .NET Standard 2.1, as it was before 3.7.0. Its version has been updated to 1.2.0 to reflect this. (https://github.com/dafny-lang/dafny/pull/2277) From e08509d09a5f57004e1b3986234a69605491edeb Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 27 Jun 2022 16:14:28 -0700 Subject: [PATCH 5/5] Improve name of variable --- Source/Dafny/Substituter.cs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Source/Dafny/Substituter.cs b/Source/Dafny/Substituter.cs index 888d4b0be58..6eb317166c7 100644 --- a/Source/Dafny/Substituter.cs +++ b/Source/Dafny/Substituter.cs @@ -12,17 +12,17 @@ public class Substituter { protected readonly Expression receiverReplacement; protected readonly Dictionary substMap; protected readonly Dictionary typeMap; - protected readonly Label oldLabel; + protected readonly Label oldHeapLabel; public static readonly Substituter EMPTY = new Substituter(null, new Dictionary(), new Dictionary()); - public Substituter(Expression receiverReplacement, Dictionary substMap, Dictionary typeMap, Label oldLabel = null) { + public Substituter(Expression receiverReplacement, Dictionary substMap, Dictionary typeMap, Label oldHeapLabel = null) { Contract.Requires(substMap != null); Contract.Requires(typeMap != null); this.receiverReplacement = receiverReplacement; this.substMap = substMap; this.typeMap = typeMap; - this.oldLabel = oldLabel; + this.oldHeapLabel = oldHeapLabel; } public virtual Expression Substitute(Expression expr) { Contract.Requires(expr != null); @@ -92,7 +92,7 @@ public virtual Expression Substitute(Expression expr) { fseNew.Member = mse.Member; fseNew.TypeApplication_AtEnclosingClass = mse.TypeApplication_AtEnclosingClass.ConvertAll(t => Resolver.SubstType(t, typeMap)); fseNew.TypeApplication_JustMember = mse.TypeApplication_JustMember.ConvertAll(t => Resolver.SubstType(t, typeMap)); - fseNew.AtLabel = mse.AtLabel ?? oldLabel; + fseNew.AtLabel = mse.AtLabel ?? oldHeapLabel; newExpr = fseNew; } else if (expr is SeqSelectExpr) { SeqSelectExpr sse = (SeqSelectExpr)expr; @@ -128,7 +128,7 @@ public virtual Expression Substitute(Expression expr) { if (receiver != e.Receiver || newArgs != e.Args || newTypeApplicationAtEnclosingClass != e.TypeApplication_AtEnclosingClass || newTypeApplicationJustFunction != e.TypeApplication_JustFunction) { - FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs, e.AtLabel ?? oldLabel); + FunctionCallExpr newFce = new FunctionCallExpr(expr.tok, e.Name, receiver, e.OpenParen, newArgs, e.AtLabel ?? oldHeapLabel); newFce.Function = e.Function; // resolve on the fly (and set newFce.Type below, at end) newFce.CoCall = e.CoCall; // also copy the co-call status newFce.CoCallHint = e.CoCallHint; // and any co-call hint @@ -163,7 +163,7 @@ public virtual Expression Substitute(Expression expr) { // BoogieWrapper before calling Substitute. Expression se = Substitute(e.E); if (se != e.E) { - newExpr = new OldExpr(expr.tok, se, e.At) { AtLabel = e.AtLabel ?? oldLabel }; + newExpr = new OldExpr(expr.tok, se, e.At) { AtLabel = e.AtLabel ?? oldHeapLabel }; } } else if (expr is UnchangedExpr) { var e = (UnchangedExpr)expr; @@ -177,7 +177,7 @@ public virtual Expression Substitute(Expression expr) { fr.Add(fefe); } if (anythingChanged) { - newExpr = new UnchangedExpr(e.tok, fr, e.At) { AtLabel = e.AtLabel ?? oldLabel }; + newExpr = new UnchangedExpr(e.tok, fr, e.At) { AtLabel = e.AtLabel ?? oldHeapLabel }; } } else if (expr is SeqConstructionExpr) { var e = (SeqConstructionExpr)expr; @@ -204,7 +204,7 @@ public virtual Expression Substitute(Expression expr) { if (se != e.E) { if (e is FreshExpr) { var ee = (FreshExpr)e; - newExpr = new FreshExpr(expr.tok, se, ee.At) { AtLabel = ee.AtLabel ?? oldLabel }; + newExpr = new FreshExpr(expr.tok, se, ee.At) { AtLabel = ee.AtLabel ?? oldHeapLabel }; } else if (e is UnaryOpExpr) { var ee = (UnaryOpExpr)e; newExpr = new UnaryOpExpr(expr.tok, ee.Op, se);