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/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. 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