Fix: Enhanced "insufficient reads clause to read field"

[MikaelMayer]

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 thisx'` is added for discoverability.
For scopes without a possible resolution, the following error message is now emitted:

Error: insufficient reads clause to read field; Mutable fields
cannot be accessed within certain scopes, such as default
values or the right-hand side of constants

For a function by method, the scope is the function and not the method body.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[RustanLeino]

Thanks for doing this work! It will help our users.

I'm wondering if we should suggest the field-specific forms of the reads clauses. In my experience, the object-specific form is almost always enough, so the more specific form may clutter up reads clauses (plus, users may get stuck if they then want to try to add these field-specific clauses to a Dafny set). If you think the field-specific version is better, then how about we mention both, like "try reads obj or reads obj`x"?

[RustanLeino]

Thank you for taking such care in crafting these error messages so that they are highly useful to users.

I have a few more comments along those lines:

function F(a: array<int>): int
  requires a.Length > 0
{
  a[0] // this gives no suggestion, but it could suggest "reads 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))
}

[RustanLeino]

Bravo!