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.

Sign up for GitHub

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

Jump to bottom

datatype doesn't correctly compute equality-support #1427

Open
tjhance opened this issue Sep 10, 2021 · 3 comments
Open

datatype doesn't correctly compute equality-support #1427

tjhance opened this issue Sep 10, 2021 · 3 comments
Labels
during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec introduced: pre-2012 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work

Comments

@tjhance
Copy link

tjhance commented Sep 10, 2021

In the following, T doesn't have equality support, so X shouldn't either:

type T

method m(t1: T, t2: T) {
  var x := t1 == t2; // correctly gives error
}

datatype X = X(t: T)

method m2(x1: X, x2: X) {
  var y := x1 == x2; // doesn't error but should
}

As far as I can tell, it only seems to apply to opaque types (e.g., if T is a datatype with a ghost field or something, then X will correctly compute that it doesn't have equality support).
@tjhance tjhance mentioned this issue Sep 11, 2021
Closed
@tjhance
Copy link
Author

tjhance commented Sep 13, 2021

I should probably provide a little more context: the reason this came up is that I have an extern type (defined via C++) with no operator== defined. In the C++ backend, this results in compile errors. (Because when generating code for type X, it tries to call out to T's operator== which does not exit.) I think in the C# backend it falls back to object equality ("pointer equality") so fails silently.

This is inconsistent across the backends, and we should think about which is the desired behavior. Personally I'd argue that failing to compile makes more sense - I can't really think of any reason why falling back to pointer equality would make sense.

@robin-aws robin-aws added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) labels Sep 21, 2021
cpitclaudel added a commit that referenced this issue Apr 25, 2022
@cpitclaudel
Fix computation of equality support for datatypes (fixes #1427)
52e6e7d
cpitclaudel added a commit that referenced this issue Apr 26, 2022
@cpitclaudel
Fix computation of equality support for datatypes (fixes #1427)
949439f 
* Source/Dafny/Resolver.cs (DetermineEqualitySupport):

  Change early-exit criterion: use general `Type.SupportsEquality` instead of
  special-casing codatatypes and arrow types.  Separately check for datatypes to
  avoid infinite recursion.
@cpitclaudel cpitclaudel mentioned this issue Apr 26, 2022
Closed
cpitclaudel added a commit that referenced this issue Apr 26, 2022
@cpitclaudel
Fix computation of equality support for datatypes (fixes #1427)
e150887 
* Source/Dafny/Resolver.cs (DetermineEqualitySupport):

  Change early-exit criterion: use general `Type.SupportsEquality` instead of
  special-casing codatatypes and arrow types.  Separately check for datatypes to
  avoid infinite recursion.
@cpitclaudel
Copy link
Member

The issue here is that the test in

dafny/Source/Dafny/Resolver.cs

Line 9683 in b5ad10a

if (arg.IsGhost ||
is to weak: it only eliminates codatatypes, function types, and datatypes that are never equatable (e.g. those that contain ghost fields. It does not check that datatypes that may support equality depending on their parameters indeed do support equality, and it doesn't check for other types, like opaque types.

@cpitclaudel cpitclaudel mentioned this issue Apr 27, 2022
Closed
cpitclaudel added a commit that referenced this issue Apr 27, 2022
@cpitclaudel
wip: Fix computation of equality support for datatypes (fixes #1427)
53aa358 
* Source/Dafny/Resolver.cs (DetermineEqualitySupport):

  Change early-exit criterion: use general `Type.SupportsEquality` instead of
  special-casing codatatypes and arrow types.  Separately check for datatypes to
  avoid infinite recursion.
@cpitclaudel cpitclaudel added during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec and removed logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) labels Sep 2, 2022
@jtristan jtristan self-assigned this Sep 20, 2022
@jtristan jtristan mentioned this issue Sep 20, 2022
Closed
@cpitclaudel
Copy link
Member

I will merge #1429 and #2070 with this issue. There's no obvious way to fix any one of these without fixing the two others, so it's much better to fix all three at once and have the discussion in a single place.

@jtristan jtristan removed their assignment Oct 24, 2022
@keyboardDrummer keyboardDrummer mentioned this issue Nov 29, 2022
Closed
@keyboardDrummer keyboardDrummer added the priority: not yet Will reconsider working on this when we're looking for work label Feb 21, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
during 3: execution of incorrect program An bug in the verifier that allows Dafny to run a program that does not correctly implement its spec introduced: pre-2012 kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking priority: not yet Will reconsider working on this when we're looking for work
Projects
None yet
Milestone
No milestone
6 participants
@atomb @tjhance @jtristan @keyboardDrummer @cpitclaudel @robin-aws