Fix: Optional pre-type won't cause a crash anymore

[MikaelMayer]

This PR fixes #5369
I added the corresponding test.

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

[keyboardDrummer]

Can you add a comment to the class UnusedPreType ?

[keyboardDrummer]

What do you mean by MemberSelect not being considered an expression? It inherits from Expression

[MikaelMayer]

It weirdly is an Expression, but not a true Dafny expression: you cannot use it in a regular Dafny expression. Consider the following:

class A {
  method Test() {
  }
}
method Main() {
  var a := new A();
  var f := a.Test; // Error, expected a Dafny expression on the RHS
  f();
}

[keyboardDrummer]

It is also used for fields, in which case it is an expression, right?

[keyboardDrummer]

It seems nice to conceptually consider a MemberSelectExpr that references a method still an expression, even if we don't allow it in an expression context. If we do that, then I would expect to assign some sort of callable type to it. Could we rename UnusedPreType to Method[Pre]Type?

[MikaelMayer]

Yes, it's used for fields and in that case it's indeed an expression.

I did the renaming, hoping it won't break any future development.

[keyboardDrummer]

Can you add a comment to ConfirmConstraint, or update its signature (parameter names) to make it clear what it does? I don't understand the meaning of the parameters or return value by looking at just its signature and comment.

[MikaelMayer]

I can't, as I don't understand the code at a level high enough to do that. I don't have a mental model of what ConfirmConstraint does, nor about what code context it was called with. I'll leave it for @RustanLeino to comment on it.

[keyboardDrummer]

I don't think this is the right fix. Looking at the input program:

predicate IsSmallest(s: set<nat>, item: nat) 
  requires item in s {
  m in s && forall y: nat :: y in s ==> m <= y
}

method m(items: set<nat>) returns (r:nat)
requires |items| > 0 {
    var item :| item in items;
    return item;
}

I think the expect file should be:

git-issue-5369.dfy(20,2): name of method (m) is used as a variable
git-issue-5369.dfy(20,40): name of method (m) is used as a variable

and nothing else.

I think these errors some come from the pretype resolution phase and leave a preTypeProxy assigned as the type of m, so that no further errors are generated based on usages of m.

I've pushed a commit to this PR that almost achieves what I describe above. The errors are now:

git-issue-5369.dfy(20,2): Error: expression is not allowed to invoke a method (m)
git-issue-5369.dfy(20,40): Error: expression is not allowed to invoke a method (m)

and nothing else from predicate IsSmallest

[MikaelMayer]

I don't think this is the right fix. Looking at the input program:

Thank you very much for this more precise fix ! Looks great.