From 04e763541aac414b48a2e3a8a567937b909efa57 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Fri, 29 Mar 2024 16:20:10 -0500 Subject: [PATCH 1/2] Chore: More precise documentation about export set names (#5230) Just documentation update on non-checked code. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- docs/DafnyRef/Modules.md | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/docs/DafnyRef/Modules.md b/docs/DafnyRef/Modules.md index ab757469ce9..31ee26bbfe1 100644 --- a/docs/DafnyRef/Modules.md +++ b/docs/DafnyRef/Modules.md @@ -352,9 +352,8 @@ Examples: ```dafny export E extends F reveals f,g provides g,h export E reveals * -export reveals f +export reveals f,g provides g,h export E -export export E ... reveals f ``` @@ -375,15 +374,16 @@ module using the `import` mechanism. An _export set_ enables a module to disallow the use of some declarations outside the module. -Export sets have names; those names are used in `import` statements to -designate which export set of a module is being imported. -If a module `M` has export sets -`E1` and `E2`, we can write ``import A = M`E1`` to create a module alias -`A` that contains only the -names in `E1`. Or we can write ``import A = M`{E1,E2}`` to import the union +An export set has an optional name used to disambiguate +in case of multiple export sets; +If specified, such names are used in `import` statements +to designate which export set of a module is being imported. +If a module `M` has export sets `E1` and `E2`, +we can write ``import A = M`E1`` to create a module alias +`A` that contains only the names in `E1`. +Or we can write ``import A = M`{E1,E2}`` to import the union of names in `E1` and `E2` as module alias `A`. -As before, ``import M`E1`` is an -abbreviation of ``import M = M`E1``. +As before, ``import M`E1`` is an abbreviation of ``import M = M`E1``. If no export set is given in an import statement, the default export set of the module is used. From 4a3aace168a23b930a3b7a073d39387b3b947986 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Fri, 29 Mar 2024 18:52:36 -0500 Subject: [PATCH 2/2] Fix: Enhanced "insufficient reads clause to read field" (#5265) This PR enhances the error message, giving more context. Fixes #5262 For example, in the context of a method where `x` is a field, x := 5; f := () => if 5 / x == 1 then 2 else 3; ^ Error here Instead of saying git-issue-405.dfy(19,22): Error: insufficient reads clause to read field the new message is more helpful: git-issue-405.dfy(19,22): Error: insufficient reads clause to read field; Consider extracting this.x to a local variable, or adding 'reads this' in the enclosing lambda specification for resolution The first part of this message is added only for lambda expressions, the second part is always present for scope tolerating a reads clause. For scopes such as functions or methods, where the reads clause can sometimes be more fine-grained, the hint `or 'reads this`x'` is added for discoverability. For scopes without a possible resolution, the following error message is now emitted: Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values or the right-hand side of constants For a function by method, the scope is the function and not the method body. By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../Expressions/Comprehensions/LambdaExpr.cs | 4 +- Source/DafnyCore/AST/IHasUsages.cs | 4 + Source/DafnyCore/AST/Members/ConstantField.cs | 1 + Source/DafnyCore/AST/Members/Function.cs | 1 + Source/DafnyCore/AST/Members/ICodeContext.cs | 5 +- Source/DafnyCore/AST/Members/Method.cs | 1 + .../AST/TypeDeclarations/DatatypeDecl.cs | 1 + .../AST/TypeDeclarations/IteratorDecl.cs | 1 + .../AST/TypeDeclarations/NewtypeDecl.cs | 1 + .../TypeDeclarations/TypeSynonymDeclBase.cs | 1 + .../Verifier/BoogieGenerator.BoogieFactory.cs | 2 +- .../BoogieGenerator.DefiniteAssignment.cs | 2 +- .../BoogieGenerator.ExpressionTranslator.cs | 40 ++++++---- .../BoogieGenerator.ExpressionWellformed.cs | 24 +++--- .../Verifier/BoogieGenerator.Extremes.cs | 2 +- .../Verifier/BoogieGenerator.Fields.cs | 4 +- .../Verifier/BoogieGenerator.Functions.cs | 24 +++--- .../Verifier/BoogieGenerator.Iterators.cs | 10 +-- .../Verifier/BoogieGenerator.LetExpr.cs | 4 +- .../Verifier/BoogieGenerator.Methods.cs | 24 +++--- .../Verifier/BoogieGenerator.TrStatement.cs | 20 ++--- .../Verifier/BoogieGenerator.Types.cs | 4 +- Source/DafnyCore/Verifier/BoogieGenerator.cs | 8 +- .../Verifier/ProofObligationDescription.cs | 79 ++++++++++++++++--- .../LitTests/LitTest/dafny0/Array.dfy.expect | 12 +-- .../LitTest/dafny0/Comprehensions.dfy.expect | 2 +- .../dafny0/ComprehensionsNewSyntax.dfy.expect | 2 +- .../dafny0/DefaultParameters.dfy.expect | 18 ++--- .../LitTests/LitTest/dafny0/Reads.dfy.expect | 16 ++-- .../LitTest/dafny0/ReadsOnMethods.dfy | 14 ++-- .../LitTest/dafny0/ReadsOnMethods.dfy.expect | 34 ++++---- .../dafny0/Twostate-Functions.dfy.expect | 2 +- .../LitTests/LitTest/dafny4/Bug146.dfy.expect | 2 +- .../git-issues/git-issue-405.dfy.expect | 2 +- .../LitTest/git-issues/git-issue-5262.dfy | 38 +++++++++ .../git-issues/git-issue-5262.dfy.expect | 6 ++ .../LitTests/LitTest/hofs/Frame.dfy.expect | 4 +- docs/OnlineTutorial/guide.20.expect | 2 +- docs/dev/news/5262.fix | 1 + 39 files changed, 274 insertions(+), 148 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5262.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5262.dfy.expect create mode 100644 docs/dev/news/5262.fix diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs index ce4eccd027d..add5306ab3a 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs @@ -3,7 +3,7 @@ namespace Microsoft.Dafny; -public class LambdaExpr : ComprehensionExpr, ICloneable { +public class LambdaExpr : ComprehensionExpr, ICloneable, IFrameScope { public override string WhatKind => Reads.Expressions.Count != 0 ? "lambda" : Range != null ? "partial lambda" : "total lambda"; public Expression Body => Term; @@ -84,4 +84,6 @@ public override bool SetIndent(int indentBefore, TokenNewIndentCollector formatt return true; } + + public string Designator => "lambda"; } \ No newline at end of file diff --git a/Source/DafnyCore/AST/IHasUsages.cs b/Source/DafnyCore/AST/IHasUsages.cs index 47905ba13a6..31c31f280a0 100644 --- a/Source/DafnyCore/AST/IHasUsages.cs +++ b/Source/DafnyCore/AST/IHasUsages.cs @@ -28,6 +28,10 @@ public interface ICanVerify : ISymbol { string FullDafnyName { get; } } +public interface IFrameScope { + string Designator { get; } // "lambda expression", "method", "function"... +} + public static class AstExtensions { public static string GetMemberQualification(MemberDecl memberDecl) { diff --git a/Source/DafnyCore/AST/Members/ConstantField.cs b/Source/DafnyCore/AST/Members/ConstantField.cs index efc8668ad24..7ec15279603 100644 --- a/Source/DafnyCore/AST/Members/ConstantField.cs +++ b/Source/DafnyCore/AST/Members/ConstantField.cs @@ -65,4 +65,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn AutoRevealFunctionDependencies.GenerateMessage(addedReveals.ToList())); } } + public string Designator => WhatKind; } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs index 52521ec1fe7..84cc33ba36a 100644 --- a/Source/DafnyCore/AST/Members/Function.cs +++ b/Source/DafnyCore/AST/Members/Function.cs @@ -564,4 +564,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn AutoRevealFunctionDependencies.GenerateMessage(addedReveals, autoRevealDepth)); } } + public string Designator => WhatKind; } diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs index 4d850ab5b88..b314efc9bd0 100644 --- a/Source/DafnyCore/AST/Members/ICodeContext.cs +++ b/Source/DafnyCore/AST/Members/ICodeContext.cs @@ -50,7 +50,7 @@ public static ICodeContext Unwrap(ICodeContext codeContext) { /// /// An ICallable is a Function, Method, IteratorDecl, or (less fitting for the name ICallable) RedirectingTypeDecl or DatatypeDecl. /// -public interface ICallable : ICodeContext, ISymbol { +public interface ICallable : ICodeContext, ISymbol, IFrameScope { string WhatKind { get; } string NameRelativeToModule { get; } Specification Decreases { get; } @@ -98,6 +98,8 @@ public bool InferredDecreases { public string GetDescription(DafnyOptions options) { return CwInner.GetDescription(options); } + + public string Designator => WhatKind; } @@ -132,6 +134,7 @@ public IEnumerable GetConcreteChildren() { public string GetDescription(DafnyOptions options) { throw new cce.UnreachableException(); } + public string Designator => WhatKind; } /// diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs index cb4134beeef..c4937dc3aca 100644 --- a/Source/DafnyCore/AST/Members/Method.cs +++ b/Source/DafnyCore/AST/Members/Method.cs @@ -472,4 +472,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn AutoRevealFunctionDependencies.GenerateMessage(addedReveals, autoRevealDepth)); } } + public string Designator => WhatKind; } diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs index 9a8cd46bb68..b12e70ee970 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs @@ -196,4 +196,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn } } } + public string Designator => WhatKind; } \ No newline at end of file diff --git a/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs index 6898b4b380b..93b51ee07c5 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs @@ -513,4 +513,5 @@ public override string GetTriviaContainingDocstring() { } public bool ShouldVerify => true; // This could be made more accurate public ModuleDefinition ContainingModule => EnclosingModuleDefinition; + public string Designator => WhatKind; } diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs index b7fa0f74b73..8d9e9b7414a 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs @@ -166,6 +166,7 @@ public string GetTriviaContainingDocstring() { public ModuleDefinition ContainingModule => EnclosingModuleDefinition; public bool ShouldVerify => true; // This could be made more accurate + public string Designator => WhatKind; } public class NativeType { diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs index 4bb05afb283..8ce7193f41b 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs @@ -125,4 +125,5 @@ public string GetTriviaContainingDocstring() { public abstract SymbolKind Kind { get; } public abstract string GetDescription(DafnyOptions options); + public string Designator => WhatKind; } \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs index 36638c1bb9f..f595f0413d3 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs @@ -39,7 +39,7 @@ internal Bpl.Expr BplBvLiteralExpr(Bpl.IToken tok, BaseTypes.BigNum n, int width // Bpl.LiteralExpr for a bitvector. var zero = new Bpl.LiteralExpr(tok, BaseTypes.BigNum.ZERO, width); var absN = new Bpl.LiteralExpr(tok, -n, width); - var etran = new ExpressionTranslator(this, predef, tok); + var etran = new ExpressionTranslator(this, predef, tok, null); return etran.TrToFunctionCall(tok, "sub_bv" + width, BplBvType(width), zero, absN, false); } else { return new Bpl.LiteralExpr(tok, n, width); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs index c6ab0be08f4..cdb1eb62d12 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs @@ -202,7 +202,7 @@ void AssumeCanCallForByMethodDecl(Method method, BoogieStmtListBuilder builder) // fn == new FunctionCallExpr(tok, f.Name, receiver, tok, tok, f.Formals.ConvertAll(Expression.CreateIdentExpr)); Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(method.tok, method.FullSanitizedName + "#canCall", Bpl.Type.Bool); - var etran = new ExpressionTranslator(this, predef, method.tok); + var etran = new ExpressionTranslator(this, predef, method.tok, method); List args = arguments.Select(arg => etran.TrExpr(arg)).ToList(); var formals = MkTyParamBinders(GetTypeParams(method), out var tyargs); if (method.FunctionFromWhichThisIsByMethodDecl.ReadsHeap) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index 774c86a7b3d..28213727d32 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -38,6 +38,7 @@ public Boogie.IdentifierExpr HeapCastToIdentifierExpr { public readonly string This; public readonly string readsFrame; // the name of the context's frame variable for reading state. // May be null to indicate the context's reads frame is * and doesn't require any reads checks. + public readonly IFrameScope scope; // lambda, function or predicate public readonly string modifiesFrame; // the name of the context's frame variable for writing state. readonly Function applyLimited_CurrentFunction; internal readonly FuelSetting layerInterCluster; @@ -64,7 +65,8 @@ void ObjectInvariant() { /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in. /// ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, string thisVar, - Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, string readsFrame, string modifiesFrame, bool stripLits) { + Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, IFrameScope scope, + string readsFrame, string modifiesFrame, bool stripLits) { Contract.Requires(boogieGenerator != null); Contract.Requires(predef != null); @@ -84,6 +86,7 @@ void ObjectInvariant() { this.layerIntraCluster = layerIntraCluster; } + this.scope = scope; this.readsFrame = readsFrame; this.modifiesFrame = modifiesFrame; this.stripLits = stripLits; @@ -94,48 +97,51 @@ public static Boogie.IdentifierExpr HeapIdentifierExpr(PredefinedDecls predef, B return new Boogie.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType); } - public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.IToken heapToken) - : this(boogieGenerator, predef, HeapIdentifierExpr(predef, heapToken)) { + public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.IToken heapToken, IFrameScope scope) + : this(boogieGenerator, predef, HeapIdentifierExpr(predef, heapToken), scope) { Contract.Requires(boogieGenerator != null); Contract.Requires(predef != null); Contract.Requires(heapToken != null); } - public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap) - : this(boogieGenerator, predef, heap, "this") { + public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, IFrameScope scope) + : this(boogieGenerator, predef, heap, scope, "this") { Contract.Requires(boogieGenerator != null); Contract.Requires(predef != null); } - public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, Boogie.Expr oldHeap) - : this(boogieGenerator, predef, heap, "this") { + public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, Boogie.Expr oldHeap, IFrameScope scope) + : this(boogieGenerator, predef, heap, scope, "this") { Contract.Requires(boogieGenerator != null); Contract.Requires(predef != null); Contract.Requires(oldHeap != null); - var old = new ExpressionTranslator(boogieGenerator, predef, oldHeap); + var old = new ExpressionTranslator(boogieGenerator, predef, oldHeap, scope); old.oldEtran = old; this.oldEtran = old; } - public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, string thisVar) - : this(boogieGenerator, predef, heap, thisVar, null, new FuelSetting(boogieGenerator, 1), null, "$_ReadsFrame", "$_ModifiesFrame", false) { + public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, IFrameScope scope, string thisVar) + : this(boogieGenerator, predef, heap, thisVar, null, new FuelSetting(boogieGenerator, 1), null, scope, "$_ReadsFrame", "$_ModifiesFrame", false) { Contract.Requires(boogieGenerator != null); Contract.Requires(predef != null); Contract.Requires(thisVar != null); } public ExpressionTranslator(ExpressionTranslator etran, Boogie.Expr heap) - : this(etran.BoogieGenerator, etran.predef, heap, etran.This, etran.applyLimited_CurrentFunction, etran.layerInterCluster, etran.layerIntraCluster, etran.readsFrame, etran.modifiesFrame, etran.stripLits) { + : this(etran.BoogieGenerator, etran.predef, heap, etran.This, etran.applyLimited_CurrentFunction, etran.layerInterCluster, etran.layerIntraCluster, etran.scope, etran.readsFrame, etran.modifiesFrame, etran.stripLits) { Contract.Requires(etran != null); } + public ExpressionTranslator WithReadsFrame(string newReadsFrame, IFrameScope frameScope) { + return new ExpressionTranslator(BoogieGenerator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, frameScope, newReadsFrame, modifiesFrame, stripLits); + } public ExpressionTranslator WithReadsFrame(string newReadsFrame) { - return new ExpressionTranslator(BoogieGenerator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, newReadsFrame, modifiesFrame, stripLits); + return new ExpressionTranslator(BoogieGenerator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, scope, newReadsFrame, modifiesFrame, stripLits); } public ExpressionTranslator WithModifiesFrame(string newModifiesFrame) { - return new ExpressionTranslator(BoogieGenerator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, newModifiesFrame, stripLits); + return new ExpressionTranslator(BoogieGenerator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, scope, readsFrame, newModifiesFrame, stripLits); } internal IToken GetToken(Expression expression) { @@ -148,7 +154,7 @@ public ExpressionTranslator Old { Contract.Ensures(Contract.Result() != null); if (oldEtran == null) { - oldEtran = new ExpressionTranslator(BoogieGenerator, predef, new Boogie.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits); + oldEtran = new ExpressionTranslator(BoogieGenerator, predef, new Boogie.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, scope, readsFrame, modifiesFrame, stripLits); oldEtran.oldEtran = oldEtran; } return oldEtran; @@ -161,7 +167,7 @@ public ExpressionTranslator OldAt(Label/*?*/ label) { return Old; } var heapAt = new Boogie.IdentifierExpr(Token.NoToken, "$Heap_at_" + label.AssignUniqueId(BoogieGenerator.CurrentIdGenerator), predef.HeapType); - return new ExpressionTranslator(BoogieGenerator, predef, heapAt, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits); + return new ExpressionTranslator(BoogieGenerator, predef, heapAt, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, scope, readsFrame, modifiesFrame, stripLits); } public bool UsesOldHeap { @@ -224,9 +230,9 @@ public ExpressionTranslator DecreaseFuel(int offset) { private static ExpressionTranslator CloneExpressionTranslator(ExpressionTranslator orig, BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, string thisVar, Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, string readsFrame, string modifiesFrame, bool stripLits) { - var et = new ExpressionTranslator(boogieGenerator, predef, heap, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits); + var et = new ExpressionTranslator(boogieGenerator, predef, heap, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, orig.scope, readsFrame, modifiesFrame, stripLits); if (orig.oldEtran != null) { - var etOld = new ExpressionTranslator(boogieGenerator, predef, orig.Old.HeapExpr, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits); + var etOld = new ExpressionTranslator(boogieGenerator, predef, orig.Old.HeapExpr, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, orig.scope, readsFrame, modifiesFrame, stripLits); etOld.oldEtran = etOld; et.oldEtran = etOld; } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index e7a4fa61120..54520c2f5a3 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -373,9 +373,9 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re } } } - if (!origOptions.LValueContext && wfOptions.DoReadsChecks && e.Member is Field && ((Field)e.Member).IsMutable) { + if (!origOptions.LValueContext && wfOptions.DoReadsChecks && e.Member is Field { IsMutable: true } f) { wfOptions.AssertSink(this, builder)(selectExpr.tok, Bpl.Expr.SelectTok(selectExpr.tok, etran.ReadsFrame(selectExpr.tok), etran.TrExpr(e.Obj), GetField(e)), - new PODesc.FrameSubset("read field", false), wfOptions.AssertKv); + new PODesc.ReadFrameSubset("read field", selectExpr, etran.scope), wfOptions.AssertKv); } break; @@ -430,7 +430,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re i = ConvertExpression(selectExpr.tok, i, e.E0.Type, Type.Int); Bpl.Expr fieldName = FunctionCall(selectExpr.tok, BuiltinFunction.IndexField, null, i); wfOptions.AssertSink(this, builder)(selectExpr.tok, Bpl.Expr.SelectTok(selectExpr.tok, etran.ReadsFrame(selectExpr.tok), seq, fieldName), - new PODesc.FrameSubset("read array element", false), wfOptions.AssertKv); + new PODesc.ReadFrameSubset("read array element", e, etran.scope), wfOptions.AssertKv); } else { Bpl.Expr lowerBound = e.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(e.E0); Contract.Assert(eSeqType.AsArrayType.Dims == 1); @@ -444,7 +444,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re var trigger = BplTrigger(allowedToRead); // Note, the assertion we're about to produce only seems useful in the check-only mode (that is, with subsumption 0), but if it were to be assumed, we'll use this entire RHS as the trigger var qq = new Bpl.ForallExpr(e.tok, new List { iVar }, trigger, BplImp(range, allowedToRead)); wfOptions.AssertSink(this, builder)(selectExpr.tok, qq, - new PODesc.FrameSubset("read the indicated range of array elements", false), + new PODesc.ReadFrameSubset("read the indicated range of array elements", e, etran.scope), wfOptions.AssertKv); } } @@ -479,7 +479,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re if (wfOptions.DoReadsChecks) { Bpl.Expr fieldName = etran.GetArrayIndexFieldName(e.tok, e.Indices); wfOptions.AssertSink(this, builder)(selectExpr.tok, Bpl.Expr.SelectTok(selectExpr.tok, etran.ReadsFrame(selectExpr.tok), array, fieldName), - new PODesc.FrameSubset("read array element", false), wfOptions.AssertKv); + new PODesc.ReadFrameSubset("read array element", selectExpr, etran.scope), wfOptions.AssertKv); } break; @@ -600,7 +600,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re objset); var reads = new FrameExpression(e.tok, wrap, null); CheckFrameSubset(applyExpr.tok, new List { reads }, null, null, - etran, etran.ReadsFrame(applyExpr.tok), wfOptions.AssertSink(this, builder), new PODesc.FrameSubset("invoke function", false), wfOptions.AssertKv); + etran, etran.ReadsFrame(applyExpr.tok), wfOptions.AssertSink(this, builder), new PODesc.ReadFrameSubset("invoke function"), wfOptions.AssertKv); } break; @@ -736,7 +736,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re objset); var reads = new FrameExpression(expr.tok, wrap, null); CheckFrameSubset(expr.tok, new List { reads }, null, null, - etran, etran.ReadsFrame(expr.tok), wfOptions.AssertSink(this, builder), new PODesc.FrameSubset("invoke function", false), wfOptions.AssertKv); + etran, etran.ReadsFrame(expr.tok), wfOptions.AssertSink(this, builder), new PODesc.ReadFrameSubset("invoke function"), wfOptions.AssertKv); } } else { @@ -766,7 +766,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re var s = new Substituter(null, new Dictionary(), e.GetTypeArgumentSubstitutions()); CheckFrameSubset(callExpr.tok, e.Function.Reads.Expressions.ConvertAll(s.SubstFrameExpr), - e.Receiver, substMap, etran, etran.ReadsFrame(callExpr.tok), wfOptions.AssertSink(this, builder), new PODesc.FrameSubset("invoke function", false), wfOptions.AssertKv); + e.Receiver, substMap, etran, etran.ReadsFrame(callExpr.tok), wfOptions.AssertSink(this, builder), new PODesc.ReadFrameSubset("invoke function"), wfOptions.AssertKv); } } Bpl.Expr allowance = null; @@ -892,7 +892,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re CheckFrameSubset(fe.E.tok, new List() { fe }, null, new Dictionary(), etran, etran.ReadsFrame(fe.E.tok), wfOptions.AssertSink(this, builder), - new PODesc.FrameSubset($"read state of 'unchanged' {description}", false), wfOptions.AssertKv); + new PODesc.ReadFrameSubset($"read state of 'unchanged' {description}"), wfOptions.AssertKv); } } @@ -1098,7 +1098,7 @@ void CheckOperand(Expression operand) { // Set up a new frame var frameName = CurrentIdGenerator.FreshId("$_Frame#l"); reads = lam.Reads.Expressions.ConvertAll(s.SubstFrameExpr); - comprehensionEtran = comprehensionEtran.WithReadsFrame(frameName); + comprehensionEtran = comprehensionEtran.WithReadsFrame(frameName, lam); DefineFrame(e.tok, comprehensionEtran.ReadsFrame(e.tok), reads, newBuilder, locals, frameName, comprehensionEtran); // Check frame WF and that it read covers itself @@ -1343,7 +1343,7 @@ void BuildWithHeapAs(IToken token, Bpl.Expr temporaryHeap, string heapVarSuffix, var tmpHeapVar = new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "Heap$" + suffix, predef.HeapType)); locals.Add(tmpHeapVar); var tmpHeap = new Bpl.IdentifierExpr(token, tmpHeapVar); - var generalEtran = new ExpressionTranslator(this, predef, token); + var generalEtran = new ExpressionTranslator(this, predef, token, null); var theHeap = generalEtran.HeapCastToIdentifierExpr; // tmpHeap := $Heap; @@ -1549,7 +1549,7 @@ private void CheckElementInit(IToken tok, bool forArray, List dims, }; CheckFrameSubset(tok, new List { reads }, null, null, etran, etran.ReadsFrame(tok), maker, - new PODesc.FrameSubset("invoke the function passed as an argument to the sequence constructor", false), + new PODesc.ReadFrameSubset("invoke the function passed as an argument to the sequence constructor"), options.AssertKv); } // Check that the values coming out of the function satisfy any appropriate subset-type constraints diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs index 8670f4a46e4..6c280073674 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs @@ -53,7 +53,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) { Contract.Requires(predef != null); var co = pp.ExtremePred; var tok = pp.tok; - var etran = new ExpressionTranslator(this, predef, tok); + var etran = new ExpressionTranslator(this, predef, tok, pp); var tyvars = MkTyParamBinders(GetTypeParams(pp), out var tyexprs); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs index 7ee312b18ff..fab22d0f323 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs @@ -117,7 +117,7 @@ Bpl.Function GetReadonlyField(Field f) { // function QQ():int { 3 } var cf = (ConstantField)f; if (cf.Rhs != null && RevealedInScope(cf)) { - var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(f.tok)); + var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(f.tok), null); if (!IsOpaque(cf)) { sink.AddTopLevelDeclaration(ff.CreateDefinitionAxiom(etran.TrExpr(cf.Rhs))); } @@ -167,7 +167,7 @@ void AddWellformednessCheck(ConstantField decl) { currentModule = decl.EnclosingModule; codeContext = decl; fuelContext = FuelSetting.NewFuelContext(decl); - var etran = new ExpressionTranslator(this, predef, decl.tok); + var etran = new ExpressionTranslator(this, predef, decl.tok, null); // parameters of the procedure List inParams = MkTyParamFormals(GetTypeParams(decl.EnclosingClass), true); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs index 0b7db48a7e3..b41b0f8c813 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs @@ -28,7 +28,7 @@ void AddWellformednessCheck(Function f) { Bpl.Expr prevHeap = null; Bpl.Expr currHeap = null; - var ordinaryEtran = new ExpressionTranslator(this, predef, f.tok); + var ordinaryEtran = new ExpressionTranslator(this, predef, f.tok, f); ExpressionTranslator etran; var inParams_Heap = new List(); if (f is TwoStateFunction) { @@ -38,7 +38,7 @@ void AddWellformednessCheck(Function f) { inParams_Heap.Add(currHeapVar); prevHeap = new Bpl.IdentifierExpr(f.tok, prevHeapVar); currHeap = new Bpl.IdentifierExpr(f.tok, currHeapVar); - etran = new ExpressionTranslator(this, predef, currHeap, prevHeap); + etran = new ExpressionTranslator(this, predef, currHeap, prevHeap, f); } else { etran = ordinaryEtran; } @@ -133,7 +133,7 @@ void AddWellformednessCheck(Function f) { delayer.DoWithDelayedReadsChecks(true, wfo => { foreach (var formal in f.Formals.Where(formal => formal.DefaultValue != null)) { var e = formal.DefaultValue; - CheckWellformed(e, wfo, locals, builder, etran); + CheckWellformed(e, wfo, locals, builder, etran.WithReadsFrame(etran.readsFrame, null)); // No frame scope for default values builder.Add(new Bpl.AssumeCmd(e.tok, etran.CanCallAssumption(e))); CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, builder); @@ -360,11 +360,11 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis bvPrevHeap = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", predef.HeapType)); etran = new ExpressionTranslator(this, predef, f.ReadsHeap ? new Bpl.IdentifierExpr(f.tok, predef.HeapVarName, predef.HeapType) : null, - new Bpl.IdentifierExpr(f.tok, bvPrevHeap)); + new Bpl.IdentifierExpr(f.tok, bvPrevHeap), f); etranHeap = etran; } else { - etranHeap = new ExpressionTranslator(this, predef, f.tok); - etran = readsHeap ? etranHeap : new ExpressionTranslator(this, predef, (Bpl.Expr)null); + etranHeap = new ExpressionTranslator(this, predef, f.tok, f); + etran = readsHeap ? etranHeap : new ExpressionTranslator(this, predef, (Bpl.Expr)null, f); } // This method generate the Consequence Axiom, which has information about the function's @@ -646,11 +646,11 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { bvPrevHeap = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", predef.HeapType)); etran = new ExpressionTranslator(this, predef, f.ReadsHeap ? new Bpl.IdentifierExpr(f.tok, predef.HeapVarName, predef.HeapType) : null, - new Bpl.IdentifierExpr(f.tok, bvPrevHeap)); + new Bpl.IdentifierExpr(f.tok, bvPrevHeap), f); } else { etran = readsHeap - ? new ExpressionTranslator(this, predef, f.tok) - : new ExpressionTranslator(this, predef, (Bpl.Expr)null); + ? new ExpressionTranslator(this, predef, f.tok, f) + : new ExpressionTranslator(this, predef, (Bpl.Expr)null, f); } // quantify over the type arguments, and add them first to the arguments @@ -1106,7 +1106,7 @@ public string FunctionHandle(Function f) { Bpl.Expr unboxBx = FunctionCall(f.tok, BuiltinFunction.Unbox, predef.RefType, bx); Bpl.Expr lhs = Bpl.Expr.SelectTok(f.tok, lhs_inner, bx); - var et = new ExpressionTranslator(this, predef, h); + var et = new ExpressionTranslator(this, predef, h, f); var rhs = InRWClause_Aux(f.tok, unboxBx, bx, null, f.Reads.Expressions, false, et, selfExpr, rhs_dict); if (f.EnclosingClass is ArrowTypeDecl) { @@ -1182,8 +1182,8 @@ void AddFrameAxiom(Function f) { Bpl.Expr h0; var h0Var = BplBoundVar("$h0", predef.HeapType, out h0); Bpl.Expr h1; var h1Var = BplBoundVar("$h1", predef.HeapType, out h1); - var etran0 = new ExpressionTranslator(this, predef, h0); - var etran1 = new ExpressionTranslator(this, predef, h1); + var etran0 = new ExpressionTranslator(this, predef, h0, f); + var etran1 = new ExpressionTranslator(this, predef, h1, f); Bpl.Expr wellFormed = Bpl.Expr.And( FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr), diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs index 84cc98bacab..cb4dcf07015 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs @@ -69,7 +69,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { currentModule = iter.EnclosingModuleDefinition; codeContext = iter; - var etran = new ExpressionTranslator(this, predef, iter.tok); + var etran = new ExpressionTranslator(this, predef, iter.tok, iter); var inParams = new List(); List outParams; @@ -146,7 +146,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { Contract.Assert(proc.OutParams.Count == 0); var builder = new BoogieStmtListBuilder(this, options); - var etran = new ExpressionTranslator(this, predef, iter.tok); + var etran = new ExpressionTranslator(this, predef, iter.tok, iter); // Don't do reads checks since iterator reads clauses mean something else. // See comment inside GenerateIteratorImplPrelude(). etran = etran.WithReadsFrame(null); @@ -156,7 +156,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { // check well-formedness of any default-value expressions (before assuming preconditions) foreach (var formal in iter.Ins.Where(formal => formal.DefaultValue != null)) { var e = formal.DefaultValue; - CheckWellformed(e, new WFOptions(null, false, false, true), localVariables, builder, etran); + CheckWellformed(e, new WFOptions(null, false, false, true), localVariables, builder, etran.WithReadsFrame(etran.readsFrame, null)); builder.Add(new Bpl.AssumeCmd(e.tok, etran.CanCallAssumption(e))); CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, builder); } @@ -210,7 +210,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { new List())); // assume the implicit postconditions promised by MoveNext: // assume fresh(_new - old(_new)); - var yeEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType)); + var yeEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType), iter); var old_nw = new OldExpr(iter.tok, nw); old_nw.Type = nw.Type; // resolve here var setDiff = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub, nw, old_nw); @@ -279,7 +279,7 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { Contract.Assert(proc.OutParams.Count == 0); var builder = new BoogieStmtListBuilder(this, options); - var etran = new ExpressionTranslator(this, predef, iter.tok); + var etran = new ExpressionTranslator(this, predef, iter.tok, iter); // Don't do reads checks since iterator reads clauses mean something else. // See comment inside GenerateIteratorImplPrelude(). etran = etran.WithReadsFrame(null); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs b/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs index 7d5e846c113..647afb39d4d 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs @@ -103,7 +103,7 @@ Expression LetDesugaring(LetExpr e) { // now that we've declared the functions and axioms, let's prepare the let-such-that desugaring { - var etran = new ExpressionTranslator(this, predef, e.tok); + var etran = new ExpressionTranslator(this, predef, e.tok, null); var rhss = new List(); foreach (var bv in e.BoundVars) { var args = info.SkolemFunctionArgs(bv, this, etran); @@ -135,7 +135,7 @@ private Bpl.Function AddLetSuchThatCanCallFunction(LetExpr e, LetSuchThatExprInf } private void AddLetSuchThenCanCallAxiom(LetExpr e, LetSuchThatExprInfo info, Bpl.Function canCallFunction) { - var etranCC = new ExpressionTranslator(this, predef, info.HeapExpr(this, false), info.HeapExpr(this, true)); + var etranCC = new ExpressionTranslator(this, predef, info.HeapExpr(this, false), info.HeapExpr(this, true), null); Bpl.Expr typeAntecedents; // later ignored List gg = info.GAsVars(this, false, out typeAntecedents, etranCC); var gExprs = new List(); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index d5a46ab2890..d9031f585ac 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -223,7 +223,7 @@ private void AddAllocationAxiom(Boogie.Declaration fieldDeclaration, Field f, To var cf = (ConstantField)f; AddWellformednessCheck(cf); if (InVerificationScope(cf)) { - var etran = new ExpressionTranslator(this, predef, f.tok); + var etran = new ExpressionTranslator(this, predef, f.tok, null); heightAntecedent = Bpl.Expr.Lt(Bpl.Expr.Literal(cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf)), etran.FunctionContextHeight()); } } @@ -541,7 +541,8 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP var builder = new BoogieStmtListBuilder(this, options); var builderInitializationArea = new BoogieStmtListBuilder(this, options); builder.Add(new CommentCmd("AddMethodImpl: " + m + ", " + proc)); - var etran = new ExpressionTranslator(this, predef, m.tok); + var etran = new ExpressionTranslator(this, predef, m.tok, + m.IsByMethod ? m.FunctionFromWhichThisIsByMethodDecl : m); // Only do reads checks for methods, not lemmas // (which aren't allowed to declare frames and don't check reads and writes against them). // Also don't do any reads checks if the reads clause is *, @@ -681,7 +682,7 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP readsCheckDelayer.DoWithDelayedReadsChecks(true, wfo => { foreach (var formal in m.Ins.Where(formal => formal.DefaultValue != null)) { var e = formal.DefaultValue; - CheckWellformed(e, wfo, localVariables, builder, etran); + CheckWellformed(e, wfo, localVariables, builder, etran.WithReadsFrame(etran.readsFrame, null)); // No scope for default parameters builder.Add(new Boogie.AssumeCmd(e.tok, etran.CanCallAssumption(e))); CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, builder); @@ -808,7 +809,7 @@ private void AddMethodOverrideCheckImpl(Method m, Boogie.Procedure proc) { List outParams = Boogie.Formal.StripWhereClauses(proc.OutParams); var builder = new BoogieStmtListBuilder(this, options); - var etran = new ExpressionTranslator(this, predef, m.tok); + var etran = new ExpressionTranslator(this, predef, m.tok, m); var localVariables = new List(); InitializeFuelConstant(m.tok, builder, etran); @@ -906,7 +907,7 @@ private void AddFunctionOverrideCheckImpl(Function f) { Boogie.Expr prevHeap = null; Boogie.Expr currHeap = null; - var ordinaryEtran = new ExpressionTranslator(this, predef, f.tok); + var ordinaryEtran = new ExpressionTranslator(this, predef, f.tok, f); ExpressionTranslator etran; var inParams_Heap = new List(); if (f is TwoStateFunction) { @@ -918,7 +919,7 @@ private void AddFunctionOverrideCheckImpl(Function f) { inParams_Heap.Add(currHeapVar); currHeap = new Boogie.IdentifierExpr(f.tok, currHeapVar); } - etran = new ExpressionTranslator(this, predef, currHeap, prevHeap); + etran = new ExpressionTranslator(this, predef, currHeap, prevHeap, f); } else { etran = ordinaryEtran; } @@ -1220,11 +1221,12 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti bvPrevHeap = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, "$prevHeap", predef.HeapType)); etran = new ExpressionTranslator(this, predef, f.ReadsHeap ? new Boogie.IdentifierExpr(f.tok, predef.HeapVarName, predef.HeapType) : null, - new Boogie.IdentifierExpr(f.tok, bvPrevHeap)); + new Boogie.IdentifierExpr(f.tok, bvPrevHeap), + f); } else if (readsHeap) { - etran = new ExpressionTranslator(this, predef, f.tok); + etran = new ExpressionTranslator(this, predef, f.tok, f); } else { - etran = new ExpressionTranslator(this, predef, (Boogie.Expr)null); + etran = new ExpressionTranslator(this, predef, (Boogie.Expr)null, f); } // "forallFormals" is built to hold the bound variables of the quantification @@ -1629,7 +1631,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { isAllocContext = new IsAllocContext(options, m.IsGhost); Boogie.Expr prevHeap = null; Boogie.Expr currHeap = null; - var ordinaryEtran = new ExpressionTranslator(this, predef, m.tok); + var ordinaryEtran = new ExpressionTranslator(this, predef, m.tok, m); ExpressionTranslator etran; var inParams = new List(); if (m is TwoStateLemma) { @@ -1639,7 +1641,7 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { inParams.Add(currHeapVar); prevHeap = new Boogie.IdentifierExpr(m.tok, prevHeapVar); currHeap = new Boogie.IdentifierExpr(m.tok, currHeapVar); - etran = new ExpressionTranslator(this, predef, currHeap, prevHeap); + etran = new ExpressionTranslator(this, predef, currHeap, prevHeap, m); } else { etran = ordinaryEtran; } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs index b7cf77f1ace..df1cb7bee48 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.TrStatement.cs @@ -102,7 +102,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List { etran.HeapCastToIdentifierExpr })); updater.Add(TrAssumeCmd(s.Tok, HeapSucc(prevHeap, etran.HeapExpr))); @@ -1389,7 +1389,7 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, Bpl.LocalVariable preLoopHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$PreLoopHeap$" + suffix, predef.HeapType)); locals.Add(preLoopHeapVar); Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(s.Tok, preLoopHeapVar); - ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap); + ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap, etran.scope); ExpressionTranslator updatedFrameEtran; string loopFrameName = "$Frame$" + suffix; if (s.Mod.Expressions != null) { @@ -1400,7 +1400,7 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, if (s.Mod.Expressions != null) { // check well-formedness and that the modifies is a subset CheckFrameWellFormed(new WFOptions(), s.Mod.Expressions, locals, builder, etran); - CheckFrameSubset(s.Tok, s.Mod.Expressions, null, null, etran, etran.ModifiesFrame(s.Tok), builder, new PODesc.FrameSubset("loop modifies clause", true), null); + CheckFrameSubset(s.Tok, s.Mod.Expressions, null, null, etran, etran.ModifiesFrame(s.Tok), builder, new PODesc.ModifyFrameSubset("loop modifies clause"), null); DefineFrame(s.Tok, etran.ModifiesFrame(s.Tok), s.Mod.Expressions, builder, locals, loopFrameName); } builder.Add(Bpl.Cmd.SimpleAssign(s.Tok, preLoopHeap, etran.HeapExpr)); @@ -1918,14 +1918,14 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E if (etran.readsFrame != null) { var readsSubst = new Substituter(null, new Dictionary(), tySubst); CheckFrameSubset(tok, callee.Reads.Expressions.ConvertAll(readsSubst.SubstFrameExpr), - receiver, substMap, etran, etran.ReadsFrame(tok), builder, new PODesc.FrameSubset("call", false), null); + receiver, substMap, etran, etran.ReadsFrame(tok), builder, new PODesc.ReadFrameSubset("call"), null); } // Check that the modifies clause of a subcall is a subset of the current modifies frame, // but only if we're in a context that defines a modifies frame. if (codeContext is IMethodCodeContext) { var modifiesSubst = new Substituter(null, new Dictionary(), tySubst); CheckFrameSubset(tok, callee.Mod.Expressions.ConvertAll(modifiesSubst.SubstFrameExpr), - receiver, substMap, etran, etran.ModifiesFrame(tok), builder, new PODesc.FrameSubset("call", true), null); + receiver, substMap, etran, etran.ModifiesFrame(tok), builder, new PODesc.ModifyFrameSubset("call"), null); } // Check termination @@ -2068,7 +2068,7 @@ void TrForallStmtCall(IToken tok, List boundVars, List bo var initHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, CurrentIdGenerator.FreshId("$initHeapForallStmt#"), predef.HeapType)); locals.Add(initHeapVar); var initHeap = new Bpl.IdentifierExpr(tok, initHeapVar); - var initEtran = new ExpressionTranslator(this, predef, initHeap, etran.Old.HeapExpr); + var initEtran = new ExpressionTranslator(this, predef, initHeap, etran.Old.HeapExpr, etran.scope); // initHeap := $Heap; exporter.Add(Bpl.Cmd.SimpleAssign(tok, initHeap, etran.HeapExpr)); var heapIdExpr = etran.HeapCastToIdentifierExpr; @@ -2095,7 +2095,7 @@ void TrForallStmtCall(IToken tok, List boundVars, List bo Bpl.Expr ante; var argsSubstMap = new Dictionary(); // maps formal arguments to actuals Contract.Assert(s0.Method.Ins.Count == s0.Args.Count); - var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap); + var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap, etran.scope); Bpl.Expr post = Bpl.Expr.True; Bpl.Trigger tr; if (forallExpressions != null) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs index 210f45c8c30..c1c8951ab14 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs @@ -998,7 +998,7 @@ void AddRedirectingTypeDeclAxioms(bool is_alloc, T dd, string fullName) comment = $"$Is axiom for {dd.WhatKind} {fullName}"; // $Is(o, ..) is_o = MkIs(o, o_ty, ModeledAsBoxType(baseType)); - var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(dd.tok)); + var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(dd.tok), null); Bpl.Expr parentConstraint, constraint; if (baseType.IsNumericBased() || baseType.IsBitVectorType || baseType.IsBoolType || baseType.IsCharType) { // optimize this to only use the numeric/bitvector constraint, not the whole $Is thing on the base type @@ -1397,7 +1397,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { currentModule = decl.Module; codeContext = new CallableWrapper(decl, true); - var etran = new ExpressionTranslator(this, predef, decl.tok); + var etran = new ExpressionTranslator(this, predef, decl.tok, null); // parameters of the procedure var inParams = MkTyParamFormals(decl.TypeArgs, true); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 52788f3f800..843d2b0f08a 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -1167,7 +1167,7 @@ public Expr TypeSpecificEqual(IToken tok, Dafny.Type type, Expr e0, Expr e1) { Contract.Requires(B != null); Contract.Requires(l != null); Contract.Requires(predef != null); - var etran = new ExpressionTranslator(this, predef, dt.tok); + var etran = new ExpressionTranslator(this, predef, dt.tok, dt); // For example, for possibly infinite lists: // codatatype SList = Nil | SCons(head: T, tail: SList); // produce with conjucts=false (default): @@ -1509,7 +1509,7 @@ public Specialization(IVariable formal, MatchCase mc, Specialization prev, Boogi // IsGoodHeap(h) && OlderTag(h) && F(x, y) && IsAlloc(y, Y, h) // ==> IsAlloc(x, X, h)) var heapVar = BplBoundVar("$olderHeap", predef.HeapType, out var heap); - var etran = new ExpressionTranslator(this, predef, heap); + var etran = new ExpressionTranslator(this, predef, heap, f); var isGoodHeap = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, heap); var olderTag = FunctionCall(f.tok, "$OlderTag", Bpl.Type.Bool, heap); @@ -2050,7 +2050,7 @@ void DefineFrame(IToken/*!*/ tok, Boogie.IdentifierExpr frameIdentifier, List inParams = MkTyParamFormals(GetTypeParams(ctor.EnclosingDatatype), true); diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs index 4cff0ae159c..6c0c5460d5b 100644 --- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs +++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs @@ -1,3 +1,4 @@ +using System; using System.Collections.Generic; using System.Diagnostics.Contracts; using System.Linq; @@ -526,25 +527,81 @@ public TraitDecreases(string whatKind) { } } -public class FrameSubset : ProofObligationDescription { +public class ReadFrameSubset : ProofObligationDescription { public override string SuccessDescription => - isWrite - ? $"{whatKind} is allowed by context's modifies clause" - : $"sufficient reads clause to {whatKind}"; + $"sufficient reads clause to {whatKind}"; public override string FailureDescription => - isWrite - ? $"{whatKind} might violate context's modifies clause" - : $"insufficient reads clause to {whatKind}"; + $"insufficient reads clause to {whatKind}" + ExtendedFailureHint(); - public override string ShortDescription => "frame subset"; + public string ExtendedFailureHint() { + if (readExpression is null) { + return ""; + } + if (scope is { Designator: var designator }) { + var lambdaScope = scope as LambdaExpr; + var extraHint = ""; + var obj = "object"; + if (readExpression is MemberSelectExpr e) { + obj = Printer.ExprToString(DafnyOptions.DefaultImmutableOptions, e.Obj, new PrintFlags(UseOriginalDafnyNames: true)); + } else if (readExpression is SeqSelectExpr s) { + obj = Printer.ExprToString(DafnyOptions.DefaultImmutableOptions, s.Seq, new PrintFlags(UseOriginalDafnyNames: true)); + } else if (readExpression is MultiSelectExpr m) { + obj = Printer.ExprToString(DafnyOptions.DefaultImmutableOptions, m.Array, + new PrintFlags(UseOriginalDafnyNames: true)); + } + + if (scope is Function { CoClusterTarget: var x } && x != Function.CoCallClusterInvolvement.None) { + } else { + if (lambdaScope == null && readExpression is MemberSelectExpr { MemberName: var field }) { + extraHint = $" or 'reads {obj}`{field}'"; + } + var hint = $"adding 'reads {obj}'{extraHint} in the enclosing {designator} specification for resolution"; + if (lambdaScope != null && lambdaScope.Reads.Expressions.Count == 0) { + hint = $"extracting {readExpression} to a local variable before the lambda expression, or {hint}"; + } + + return $"; Consider {hint}"; + } + } + + string whyNotWhat = "Memory locations"; + + if (whatKind == "read field") { + whyNotWhat = "Mutable fields"; + } else if (whatKind is "read array element" or "read the indicated range of array elements") { + whyNotWhat = "Array elements"; + } + return $"; {whyNotWhat} cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls"; + + } + + public override string ShortDescription => "read frame subset"; + + private readonly string whatKind; + private readonly Expression readExpression; + [CanBeNull] private readonly IFrameScope scope; + + public ReadFrameSubset(string whatKind, Expression readExpression = null, [CanBeNull] IFrameScope scope = null) { + this.whatKind = whatKind; + this.readExpression = readExpression; + this.scope = scope; + } +} + +public class ModifyFrameSubset : ProofObligationDescription { + public override string SuccessDescription => + $"{whatKind} is allowed by context's modifies clause"; + + public override string FailureDescription => + $"{whatKind} might violate context's modifies clause"; + + public override string ShortDescription => "modify frame subset"; private readonly string whatKind; - private readonly bool isWrite; - public FrameSubset(string whatKind, bool isWrite) { + public ModifyFrameSubset(string whatKind) { this.whatKind = whatKind; - this.isWrite = isWrite; } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Array.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Array.dfy.expect index 8e5a6429467..5f3db8228c6 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Array.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Array.dfy.expect @@ -9,12 +9,12 @@ Array.dfy(50,19): Error: assertion might not hold Array.dfy(58,7): Error: assignment might update an array element not in the enclosing context's modifies clause Array.dfy(65,7): Error: assignment might update an array element not in the enclosing context's modifies clause Array.dfy(108,20): Error: upper bound below lower bound or above length of array -Array.dfy(118,7): Error: insufficient reads clause to read the indicated range of array elements -Array.dfy(120,7): Error: insufficient reads clause to read the indicated range of array elements -Array.dfy(121,7): Error: insufficient reads clause to read the indicated range of array elements -Array.dfy(122,7): Error: insufficient reads clause to read the indicated range of array elements -Array.dfy(160,5): Error: insufficient reads clause to read array element -Array.dfy(168,5): Error: insufficient reads clause to read array element +Array.dfy(118,7): Error: insufficient reads clause to read the indicated range of array elements; Consider adding 'reads a' in the enclosing function specification for resolution +Array.dfy(120,7): Error: insufficient reads clause to read the indicated range of array elements; Consider adding 'reads a' in the enclosing function specification for resolution +Array.dfy(121,7): Error: insufficient reads clause to read the indicated range of array elements; Consider adding 'reads a' in the enclosing function specification for resolution +Array.dfy(122,7): Error: insufficient reads clause to read the indicated range of array elements; Consider adding 'reads a' in the enclosing function specification for resolution +Array.dfy(160,5): Error: insufficient reads clause to read array element; Consider adding 'reads a' in the enclosing function specification for resolution +Array.dfy(168,5): Error: insufficient reads clause to read array element; Consider adding 'reads b' in the enclosing function specification for resolution Array.dfy(184,5): Error: assignment might update an array element not in the enclosing context's modifies clause Array.dfy(191,5): Error: assignment might update an array element not in the enclosing context's modifies clause Array.dfy(216,0): Error: a postcondition could not be proved on this return path diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Comprehensions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Comprehensions.dfy.expect index 5a5ad58161d..35d8b095abc 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Comprehensions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Comprehensions.dfy.expect @@ -8,7 +8,7 @@ Comprehensions.dfy(12,13): Error: assertion might not hold Comprehensions.dfy(78,22): Error: assertion might not hold Comprehensions.dfy(99,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor Comprehensions.dfy(107,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -Comprehensions.dfy(115,40): Error: insufficient reads clause to read field +Comprehensions.dfy(115,40): Error: insufficient reads clause to read field; Consider extracting x to a local variable before the lambda expression, or adding 'reads this' in the enclosing lambda specification for resolution Comprehensions.dfy(118,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor Comprehensions.dfy(126,4): Error: all sequence indices must be in the domain of the initialization function Comprehensions.dfy(132,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ComprehensionsNewSyntax.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ComprehensionsNewSyntax.dfy.expect index bc8699851c7..6b0a32f79f3 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ComprehensionsNewSyntax.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ComprehensionsNewSyntax.dfy.expect @@ -8,7 +8,7 @@ ComprehensionsNewSyntax.dfy(12,13): Error: assertion might not hold ComprehensionsNewSyntax.dfy(78,22): Error: assertion might not hold ComprehensionsNewSyntax.dfy(99,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor ComprehensionsNewSyntax.dfy(107,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor -ComprehensionsNewSyntax.dfy(115,40): Error: insufficient reads clause to read field +ComprehensionsNewSyntax.dfy(115,40): Error: insufficient reads clause to read field; Consider extracting x to a local variable before the lambda expression, or adding 'reads this' in the enclosing lambda specification for resolution ComprehensionsNewSyntax.dfy(118,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor ComprehensionsNewSyntax.dfy(126,4): Error: all sequence indices must be in the domain of the initialization function ComprehensionsNewSyntax.dfy(132,4): Error: insufficient reads clause to invoke the function passed as an argument to the sequence constructor diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect index ca00b3beab3..374679dc3f9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy.expect @@ -5,8 +5,8 @@ DefaultParameters.dfy(92,2): Error: a postcondition could not be proved on this DefaultParameters.dfy(91,16): Related location: this is the postcondition that could not be proved DefaultParameters.dfy(102,15): Error: assertion might not hold DefaultParameters.dfy(110,15): Error: assertion might not hold -DefaultParameters.dfy(124,37): Error: insufficient reads clause to read field -DefaultParameters.dfy(131,40): Error: insufficient reads clause to read field +DefaultParameters.dfy(124,37): Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls +DefaultParameters.dfy(131,40): Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls DefaultParameters.dfy(135,49): Error: possible division by zero DefaultParameters.dfy(137,43): Error: possible division by zero DefaultParameters.dfy(140,34): Error: possible division by zero @@ -38,13 +38,13 @@ DefaultParameters.dfy(229,8): Error: decreases clause might not decrease DefaultParameters.dfy(235,4): Error: decreases clause might not decrease DefaultParameters.dfy(235,6): Error: decreases clause might not decrease DefaultParameters.dfy(241,4): Error: decreases clause might not decrease -DefaultParameters.dfy(251,31): Error: insufficient reads clause to read field +DefaultParameters.dfy(251,31): Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls DefaultParameters.dfy(258,40): Error: default-value expression is not allowed to involve recursive or mutually recursive calls DefaultParameters.dfy(267,41): Error: possible division by zero DefaultParameters.dfy(320,45): Error: a precondition for this call could not be proved DefaultParameters.dfy(319,15): Related location: this is the precondition that could not be proved -DefaultParameters.dfy(326,36): Error: insufficient reads clause to read array element -DefaultParameters.dfy(327,54): Error: insufficient reads clause to read array element +DefaultParameters.dfy(326,36): Error: insufficient reads clause to read array element; Array elements cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls +DefaultParameters.dfy(327,54): Error: insufficient reads clause to read array element; Array elements cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls DefaultParameters.dfy(360,38): Error: possible division by zero DefaultParameters.dfy(361,40): Error: possible division by zero DefaultParameters.dfy(362,32): Error: possible division by zero @@ -70,10 +70,10 @@ DefaultParameters.dfy(493,18): Error: value does not satisfy the subset constrai DefaultParameters.dfy(494,32): Error: value does not satisfy the subset constraints of 'nat' DefaultParameters.dfy(500,15): Error: a precondition for this call could not be proved DefaultParameters.dfy(503,13): Related location: this is the precondition that could not be proved -DefaultParameters.dfy(520,38): Error: insufficient reads clause to read field -DefaultParameters.dfy(521,40): Error: insufficient reads clause to read field -DefaultParameters.dfy(524,49): Error: insufficient reads clause to read field -DefaultParameters.dfy(548,38): Error: insufficient reads clause to read field +DefaultParameters.dfy(520,38): Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls +DefaultParameters.dfy(521,40): Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls +DefaultParameters.dfy(524,49): Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls +DefaultParameters.dfy(548,38): Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls DefaultParameters.dfy(601,11): Error: assertion might not hold DefaultParameters.dfy(582,18): Related location: this proposition could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Reads.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Reads.dfy.expect index bd68ad79877..f23fdc08228 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Reads.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Reads.dfy.expect @@ -1,14 +1,14 @@ -Reads.dfy(9,16): Error: insufficient reads clause to read field -Reads.dfy(18,29): Error: insufficient reads clause to read field -Reads.dfy(28,32): Error: insufficient reads clause to read field -Reads.dfy(37,29): Error: insufficient reads clause to read field -Reads.dfy(56,29): Error: insufficient reads clause to read field +Reads.dfy(9,16): Error: insufficient reads clause to read field; Consider adding 'reads c' or 'reads c`u' in the enclosing function specification for resolution +Reads.dfy(18,29): Error: insufficient reads clause to read field; Consider adding 'reads c' or 'reads c`u' in the enclosing function specification for resolution +Reads.dfy(28,32): Error: insufficient reads clause to read field; Consider adding 'reads xs[0]' or 'reads xs[0]`u' in the enclosing function specification for resolution +Reads.dfy(37,29): Error: insufficient reads clause to read field; Consider adding 'reads c' or 'reads c`u' in the enclosing function specification for resolution +Reads.dfy(56,29): Error: insufficient reads clause to read field; Consider adding 'reads r' or 'reads r`r' in the enclosing function specification for resolution Reads.dfy(122,35): Error: function precondition could not be proved Reads.dfy(122,35): Error: insufficient reads clause to invoke function Reads.dfy(125,37): Error: insufficient reads clause to invoke function -Reads.dfy(138,10): Error: insufficient reads clause to read field -Reads.dfy(149,25): Error: insufficient reads clause to read field -Reads.dfy(157,18): Error: insufficient reads clause to read field +Reads.dfy(138,10): Error: insufficient reads clause to read field; Consider adding 'reads this' or 'reads this`Repr' in the enclosing predicate specification for resolution +Reads.dfy(149,25): Error: insufficient reads clause to read field; Consider adding 'reads this' or 'reads this`y' in the enclosing function specification for resolution +Reads.dfy(157,18): Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls Reads.dfy(159,18): Error: insufficient reads clause to invoke function Dafny program verifier finished with 19 verified, 12 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy index ac47a4114ea..31dec745852 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy @@ -242,7 +242,7 @@ method GetBoxReadsStar(b: Box) returns (i: int) method GetBoxIncorrectReads(b: Box) returns (i: int) reads {} { - i := b.x; // Error: insufficient reads clause to read field + i := b.x; // Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values or the right-hand side of constants } method GetBoxDefaultReads(b: Box) returns (i: int) @@ -301,7 +301,7 @@ class {:extern} ExternalSequentialMutableMap { } method {:concurrent} MemoizedSquare2(x: int, cache: ExternalSequentialMutableMap) returns (xSquared: int) - requires forall k | k in cache.state :: cache.state[k] == k * k // Error: insufficient reads clause to read field + requires forall k | k in cache.state :: cache.state[k] == k * k // Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values or the right-hand side of constants reads {} ensures xSquared == x * x { @@ -399,7 +399,7 @@ function WeirdAlways42(b: Box): int { 42 } by method { var result := 42; - result := result + b.x; // Error: insufficient reads clause to read field + result := result + b.x; // Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values or the right-hand side of constants result := result - b.x; return 42; } @@ -408,9 +408,9 @@ function WeirdAlways42(b: Box): int { method BadMetaBox(b: Box>) reads {} - modifies b.x // Error: insufficient reads clause to read field + modifies b.x // Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values or the right-hand side of constants { - b.x.x := 42; // Error: insufficient reads clause to read field + b.x.x := 42; // Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values or the right-hand side of constants } method GoodMetaBox(b: Box>) @@ -520,14 +520,14 @@ twostate predicate Was42(b: Box) { // Testing the reads checks on other clauses method OnlySpecReads(b: Box) returns (r: int) - requires b.x == 42 // Error: insufficient reads clause to read field + requires b.x == 42 // Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values or the right-hand side of constants reads {} ensures r == b.x { return 42; } -method DefaultValueReads(b: Box, x: int := b.x) // Error: insufficient reads clause to read field +method DefaultValueReads(b: Box, x: int := b.x) // Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values or the right-hand side of constants returns (r: int) reads {} { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy.expect index 54fb063da86..e41ecaaa551 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ReadsOnMethods.dfy.expect @@ -1,28 +1,28 @@ ReadsOnMethods.dfy(279,8): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. ReadsOnMethods.dfy(280,11): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual. -ReadsOnMethods.dfy(19,16): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(29,29): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(44,32): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(54,29): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(73,29): Error: insufficient reads clause to read field +ReadsOnMethods.dfy(19,16): Error: insufficient reads clause to read field; Consider adding 'reads c' or 'reads c`u' in the enclosing method specification for resolution +ReadsOnMethods.dfy(29,29): Error: insufficient reads clause to read field; Consider adding 'reads c' or 'reads c`u' in the enclosing method specification for resolution +ReadsOnMethods.dfy(44,32): Error: insufficient reads clause to read field; Consider adding 'reads xs[0]' or 'reads xs[0]`u' in the enclosing method specification for resolution +ReadsOnMethods.dfy(54,29): Error: insufficient reads clause to read field; Consider adding 'reads c' or 'reads c`u' in the enclosing method specification for resolution +ReadsOnMethods.dfy(73,29): Error: insufficient reads clause to read field; Consider adding 'reads r' or 'reads r`r' in the enclosing method specification for resolution ReadsOnMethods.dfy(147,35): Error: function precondition could not be proved ReadsOnMethods.dfy(147,35): Error: insufficient reads clause to invoke function ReadsOnMethods.dfy(151,37): Error: insufficient reads clause to invoke function ReadsOnMethods.dfy(162,25): Error: insufficient reads clause to invoke function ReadsOnMethods.dfy(162,43): Error: insufficient reads clause to invoke function -ReadsOnMethods.dfy(169,10): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(172,19): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(183,25): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(245,9): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(304,33): Error: insufficient reads clause to read field +ReadsOnMethods.dfy(169,10): Error: insufficient reads clause to read field; Consider adding 'reads this' or 'reads this`Repr' in the enclosing method specification for resolution +ReadsOnMethods.dfy(172,19): Error: insufficient reads clause to read field; Consider adding 'reads this' or 'reads this`Repr' in the enclosing method specification for resolution +ReadsOnMethods.dfy(183,25): Error: insufficient reads clause to read field; Consider adding 'reads this' or 'reads this`y' in the enclosing method specification for resolution +ReadsOnMethods.dfy(245,9): Error: insufficient reads clause to read field; Consider adding 'reads b' or 'reads b`x' in the enclosing method specification for resolution +ReadsOnMethods.dfy(304,33): Error: insufficient reads clause to read field; Consider adding 'reads cache' or 'reads cache`state' in the enclosing method specification for resolution ReadsOnMethods.dfy(308,22): Error: insufficient reads clause to invoke function ReadsOnMethods.dfy(313,13): Error: insufficient reads clause to call ReadsOnMethods.dfy(360,20): Error: insufficient reads clause to call -ReadsOnMethods.dfy(402,23): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(411,13): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(413,4): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(427,10): Error: insufficient reads clause to read array element -ReadsOnMethods.dfy(436,10): Error: insufficient reads clause to read array element +ReadsOnMethods.dfy(402,23): Error: insufficient reads clause to read field; Consider adding 'reads b' or 'reads b`x' in the enclosing function specification for resolution +ReadsOnMethods.dfy(411,13): Error: insufficient reads clause to read field; Consider adding 'reads b' or 'reads b`x' in the enclosing method specification for resolution +ReadsOnMethods.dfy(413,4): Error: insufficient reads clause to read field; Consider adding 'reads b' or 'reads b`x' in the enclosing method specification for resolution +ReadsOnMethods.dfy(427,10): Error: insufficient reads clause to read array element; Consider adding 'reads a' in the enclosing method specification for resolution +ReadsOnMethods.dfy(436,10): Error: insufficient reads clause to read array element; Consider adding 'reads a' in the enclosing method specification for resolution ReadsOnMethods.dfy(469,2): Error: method might read an object not in the parent trait context's reads clause ReadsOnMethods.dfy(479,26): Error: insufficient reads clause to call ReadsOnMethods.dfy(484,24): Error: insufficient reads clause to call @@ -30,7 +30,7 @@ ReadsOnMethods.dfy(494,35): Error: insufficient reads clause to call ReadsOnMethods.dfy(499,9): Error: insufficient reads clause to invoke function ReadsOnMethods.dfy(505,9): Error: assertion might not hold ReadsOnMethods.dfy(516,11): Related location: this proposition could not be proved -ReadsOnMethods.dfy(523,13): Error: insufficient reads clause to read field -ReadsOnMethods.dfy(530,50): Error: insufficient reads clause to read field +ReadsOnMethods.dfy(523,13): Error: insufficient reads clause to read field; Consider adding 'reads b' or 'reads b`x' in the enclosing method specification for resolution +ReadsOnMethods.dfy(530,50): Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls Dafny program verifier finished with 67 verified, 31 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Functions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Functions.dfy.expect index a7aced49240..6f02395a278 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Functions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Functions.dfy.expect @@ -1,6 +1,6 @@ Twostate-Functions.dfy(11,27): Error: receiver could not be proved to be allocated in the state in which its fields are accessed Twostate-Functions.dfy(18,12): Error: receiver could not be proved to be allocated in the state in which its fields are accessed -Twostate-Functions.dfy(23,8): Error: insufficient reads clause to read field +Twostate-Functions.dfy(23,8): Error: insufficient reads clause to read field; Consider adding 'reads u' or 'reads u`aa' in the enclosing twostate function specification for resolution Twostate-Functions.dfy(66,17): Error: assertion might not hold Twostate-Functions.dfy(54,14): Related location: this proposition could not be proved Twostate-Functions.dfy(68,15): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug146.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug146.dfy.expect index f6322f25f9f..d22e9553311 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug146.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug146.dfy.expect @@ -1,4 +1,4 @@ -Bug146.dfy(6,75): Error: insufficient reads clause to read array element +Bug146.dfy(6,75): Error: insufficient reads clause to read array element; Consider adding 'reads world' in the enclosing function specification for resolution Bug146.dfy(37,15): Error: assertion might not hold Bug146.dfy(26,4): Related location: this proposition could not be proved diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-405.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-405.dfy.expect index 86505e65a93..c489ea4b66b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-405.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-405.dfy.expect @@ -1,3 +1,3 @@ -git-issue-405.dfy(19,22): Error: insufficient reads clause to read field +git-issue-405.dfy(19,22): Error: insufficient reads clause to read field; Consider extracting x to a local variable before the lambda expression, or adding 'reads this' in the enclosing lambda specification for resolution Dafny program verifier finished with 6 verified, 1 error diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5262.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5262.dfy new file mode 100644 index 00000000000..3f84ac81260 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5262.dfy @@ -0,0 +1,38 @@ +// RUN: %exits-with 4 %verify "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function F(a: array): int + requires a.Length > 0 +{ + a[0] // Suggests to "read a" +} + +class C { + var data: int + + function G(): int { + // Amazing! I don't think I've ever thought about that ` has really low binding power, + // so the suggestion "reads var th := this; th`data" in the following line works! + (var th := this; th).data + } + + function H(): int { + var th := this; + // the suggestion here is to use "reads th#Z" (maybe it's better to give up with + // a precise "reads" term if the receiver looks complicated, for some definition + // of complicated) + th.data + } +} + +codatatype Stream = More(int, Stream) + +function Repeat(c: C): Stream { + // Here, it would be better not to give a "reads" suggestion, since functions with + // co-recursive calls aren't allowed to have a reads clause. (The AST contain + // information that says whether or not a call is co-recursive. But I'm not sure if + // the AST remembers which functions are sometimes targets of co-recursive calls. + // You could add this. If so, the place to mark a function as such is right next to + // the ".IsCoCall = true" in ModuleResolver.cs.) + More(c.data, Repeat(c)) +} \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5262.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5262.dfy.expect new file mode 100644 index 00000000000..c3ea26ed538 --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5262.dfy.expect @@ -0,0 +1,6 @@ +git-issue-5262.dfy(7,3): Error: insufficient reads clause to read array element; Consider adding 'reads a' in the enclosing function specification for resolution +git-issue-5262.dfy(16,25): Error: insufficient reads clause to read field; Consider adding 'reads var th: C := this; th' or 'reads var th: C := this; th`data' in the enclosing function specification for resolution +git-issue-5262.dfy(24,7): Error: insufficient reads clause to read field; Consider adding 'reads th' or 'reads th`data' in the enclosing function specification for resolution +git-issue-5262.dfy(37,9): Error: insufficient reads clause to read field; Mutable fields cannot be accessed within certain scopes, such as default values, the right-hand side of constants, or co-recursive calls + +Dafny program verifier finished with 0 verified, 4 errors diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Frame.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Frame.dfy.expect index b39a812b6bf..6d5d58a4d49 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Frame.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Frame.dfy.expect @@ -1,8 +1,8 @@ Frame.dfy(23,15): Error: assertion might not hold Frame.dfy(37,13): Error: assertion might not hold Frame.dfy(63,22): Error: assertion might not hold -Frame.dfy(66,18): Error: insufficient reads clause to read array element -Frame.dfy(68,27): Error: insufficient reads clause to read array element +Frame.dfy(66,18): Error: insufficient reads clause to read array element; Consider extracting a[0] to a local variable before the lambda expression, or adding 'reads a' in the enclosing lambda specification for resolution +Frame.dfy(68,27): Error: insufficient reads clause to read array element; Consider adding 'reads a' in the enclosing lambda specification for resolution Frame.dfy(120,17): Error: function precondition could not be proved Frame.dfy(123,18): Error: assertion might not hold diff --git a/docs/OnlineTutorial/guide.20.expect b/docs/OnlineTutorial/guide.20.expect index 1e4b70abf5d..8cd4f6b8f87 100644 --- a/docs/OnlineTutorial/guide.20.expect +++ b/docs/OnlineTutorial/guide.20.expect @@ -1,3 +1,3 @@ -text.dfy(3,44): Error: insufficient reads clause to read array element +text.dfy(3,44): Error: insufficient reads clause to read array element; Consider adding 'reads a' in the enclosing predicate specification for resolution Dafny program verifier finished with 0 verified, 1 error diff --git a/docs/dev/news/5262.fix b/docs/dev/news/5262.fix new file mode 100644 index 00000000000..07d10bb16fc --- /dev/null +++ b/docs/dev/news/5262.fix @@ -0,0 +1 @@ +More helpful error messages when read fields not mentioned in reads clauses \ No newline at end of file