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.

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

Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs

@@ -3,7 +3,7 @@
 
 namespace Microsoft.Dafny;
 
-public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr> {
+public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr>, 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";
 }

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) {

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -65,4 +65,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
  AutoRevealFunctionDependencies.GenerateMessage(addedReveals.ToList()));
  }
  }
+ public string Designator => WhatKind;
 }

Source/DafnyCore/AST/Members/Function.cs

@@ -564,4 +564,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
  AutoRevealFunctionDependencies.GenerateMessage(addedReveals, autoRevealDepth));
  }
  }
+ public string Designator => WhatKind;
 }

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -50,7 +50,7 @@ public static ICodeContext Unwrap(ICodeContext codeContext) {
 /// <summary>
 /// An ICallable is a Function, Method, IteratorDecl, or (less fitting for the name ICallable) RedirectingTypeDecl or DatatypeDecl.
 /// </summary>
-public interface ICallable : ICodeContext, ISymbol {
+public interface ICallable : ICodeContext, ISymbol, IFrameScope {
  string WhatKind { get; }
  string NameRelativeToModule { get; }
  Specification<Expression> 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<INode> GetConcreteChildren() {
  public string GetDescription(DafnyOptions options) {
  throw new cce.UnreachableException();
  }
+ public string Designator => WhatKind;
 }
 
 /// <summary>

Source/DafnyCore/AST/Members/Method.cs

@@ -472,4 +472,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
  AutoRevealFunctionDependencies.GenerateMessage(addedReveals, autoRevealDepth));
  }
  }
+ public string Designator => WhatKind;
 }

Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs

@@ -196,4 +196,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
  }
  }
  }
+ public string Designator => WhatKind;
 }

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;
 }

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 {

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;
 }

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);

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<Bpl.Expr> args = arguments.Select(arg => etran.TrExpr(arg)).ToList();
  var formals = MkTyParamBinders(GetTypeParams(method), out var tyargs);
  if (method.FunctionFromWhichThisIsByMethodDecl.ReadsHeap) {

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.
  /// </summary>
  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<ExpressionTranslator>() != 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;
  }