Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 9 commits into from
May 17, 2024

Conversation

MikaelMayer
Copy link
Member

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.

@@ -583,6 +583,8 @@ public enum CommonConfirmationBag {
preType = preType.Normalize();
if (preType is PreTypeProxy) {
return false;
} else if (preType is UnusedPreType) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you add a comment to the class UnusedPreType ?

@@ -455,6 +455,9 @@ public class PreTypePlaceholderModule : PreTypePlaceholder {
public class PreTypePlaceholderType : PreTypePlaceholder {
}

/// Currently used exclusively for assigning a pre-type to MemberSelect expressions, such as "obj.method",
/// which is not considered an expression. This indicates that resolution has occurred,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Member

@keyboardDrummer keyboardDrummer May 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@@ -583,6 +583,8 @@ public enum CommonConfirmationBag {
preType = preType.Normalize();
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member Author

@MikaelMayer MikaelMayer May 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Member

keyboardDrummer commented May 17, 2024

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 MikaelMayer enabled auto-merge (squash) May 17, 2024 18:25
@MikaelMayer MikaelMayer merged commit cfc7760 into master May 17, 2024
21 checks passed
@MikaelMayer MikaelMayer deleted the fix-5369-crash-new-resolver branch May 17, 2024 21:25
@MikaelMayer
Copy link
Member Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Crash in new resolver
2 participants