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

New type system refresh issue #4823

Closed
MikaelMayer opened this issue Nov 28, 2023 · 0 comments · Fixed by #4824
Closed

New type system refresh issue #4823

MikaelMayer opened this issue Nov 28, 2023 · 0 comments · Fixed by #4824
Assignees
@RustanLeino
Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking

Comments

@MikaelMayer
Copy link
Member

Dafny version

latest-nightly

Code to produce this issue

trait Test<T> {
  function Cast(t: T): Test<T>
}

datatype Impl extends Test<Impl> = ImplConstructor()
{
  function Cast(t: Impl): Test<Impl> { t }
}

Command to run and resulting output

Run this with

dafny verify --type-system-refresh --general-traits=datatype example.dfy

What happened?

Unhandled exception: System.InvalidCastException: Unable to cast object of type 'Microsoft.Dafny.IndDatatypeDecl' to type 'Microsoft.Dafny.ClassLikeDecl
'.
at Microsoft.Dafny.BoogieGenerator.AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builder, ExpressionTranslator etran, Dictionary2 sub stMap, Dictionary2 typeMap) in dafny\Source\DafnyCore\Verifier\BoogieGenerator.Methods.cs:line 1185

What type of operating system are you experiencing the problem on?

Windows
@MikaelMayer MikaelMayer added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Nov 28, 2023
MikaelMayer added a commit that referenced this issue Nov 28, 2023
@MikaelMayer
Add test for issue #4823
f83131a
@MikaelMayer MikaelMayer mentioned this issue Nov 28, 2023
Merged
@jtristan jtristan added part: resolver Resolution and typechecking crash Dafny crashes on this input, or generates malformed code that can not be executed labels Nov 28, 2023
@keyboardDrummer keyboardDrummer added the during 2: compilation of correct program Dafny rejects a valid program during compilation label Feb 7, 2024
MikaelMayer added a commit that referenced this issue Apr 1, 2024
@MikaelMayer
Fix: Ability to cast a datatype to its trait when overriding functions (
10b59f5 
#4824)

This PR fixes #4823
There were two issues there:
- The function override check was casting to ClassLikeDecl, when it
should now be TopLevelDeclWithMembers as IndDatatypeDecl can also
override trait declarations.
- The generated axiom used to rely on types being unboxed, but since now
we might compare a trait with a datatype value, we need to ensure
correct boxing for Boogie to type-check.
I added the corresponding test.

<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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@RustanLeino RustanLeino

Labels
crash Dafny crashes on this input, or generates malformed code that can not be executed during 2: compilation of correct program Dafny rejects a valid program during compilation kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: resolver Resolution and typechecking
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: Ability to cast a datatype to its trait when overriding functions dafny-lang/dafny
4 participants
@jtristan @keyboardDrummer @MikaelMayer @RustanLeino