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

Boogie crash due to decreases clause in trait #4969

Closed
ssomayyajula opened this issue Jan 10, 2024 · 0 comments · Fixed by #5087
Closed

Boogie crash due to decreases clause in trait #4969

ssomayyajula opened this issue Jan 10, 2024 · 0 comments · Fixed by #5087
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: boogie Happens after passing the program to Boogie priority: next Will consider working on this after in progress work is done

Comments

@ssomayyajula
Copy link
Contributor

Dafny version

4.4.0

Code to produce this issue

// Trampoline.dfy

trait ProgramTrait {
  function Rank(): nat

  method Compute() returns (r: Result)
    decreases Rank()
}

datatype Result =
| Bounce(next: ProgramTrait)
| Done()

datatype Trivial extends ProgramTrait =
  Trivial()
{
  function Rank(): nat { 0 }
  
  method Compute() returns (r: Result)
    decreases Rank()
  {
    return Done();
  }
}

Command to run and resulting output

$ dafny verify --type-system-refresh --general-traits:datatype Trampoline.dfy

Trampoline.dfy(5,14): Error: internal error, shallow-type assignment was done incorrectly, this:Box != DatatypeType
Unhandled exception: cce+UnreachableException: Exception of type 'cce+UnreachableException' was thrown.
   at Microsoft.Boogie.IdentifierExpr.Typecheck(TypecheckingContext tc)
   at Microsoft.Boogie.NAryExpr.Typecheck(TypecheckingContext tc)
   at Microsoft.Boogie.NAryExpr.Typecheck(TypecheckingContext tc)
   at Microsoft.Boogie.NAryExpr.Typecheck(TypecheckingContext tc)
   at Microsoft.Boogie.AssertCmd.Typecheck(TypecheckingContext tc)
   at Microsoft.Boogie.Block.Typecheck(TypecheckingContext tc)
   at Microsoft.Boogie.Implementation.Typecheck(TypecheckingContext tc)
   at Microsoft.Boogie.Program.Typecheck(TypecheckingContext tc)
   at Microsoft.Boogie.Program.Typecheck(CoreOptions options, IErrorSink errorSink)
   at Microsoft.Boogie.Program.Typecheck(CoreOptions options)
   at Microsoft.Boogie.ExecutionEngine.ResolveAndTypecheck(Program program, String bplFileName, CivlTypeChecker& civlTypeChecker)
   at Microsoft.Dafny.DafnyMain.BoogiePipelineWithRerun(DafnyOptions options, TextWriter output, ExecutionEngine engine, Program program, String bplFileName, String programId) in /com.docker.devenvironments.code/Source/DafnyCore/DafnyMain.cs:line 168
   at Microsoft.Dafny.DafnyMain.BoogieOnce(DafnyOptions options, TextWriter output, ExecutionEngine engine, String baseFile, String moduleName, Program boogieProgram, String programId) in /com.docker.devenvironments.code/Source/DafnyCore/DafnyMain.cs:line 130
   at Microsoft.Dafny.CompilerDriver.BoogieOnceWithTimerAsync(TextWriter output, DafnyOptions options, String baseName, String programId, String moduleName, Program program) in /com.docker.devenvironments.code/Source/DafnyDriver/CompilerDriver.cs:line 428
   at Microsoft.Dafny.CompilerDriver.<>c__DisplayClass10_0.<<BoogieAsync>b__0>d.MoveNext() in /com.docker.devenvironments.code/Source/DafnyDriver/CompilerDriver.cs:line 400
--- End of stack trace from previous location ---
   at Microsoft.Dafny.CompilerDriver.<>c__DisplayClass10_0.<<BoogieAsync>b__0>d.MoveNext() in /com.docker.devenvironments.code/Source/DafnyDriver/CompilerDriver.cs:line 403
--- End of stack trace from previous location ---
   at Microsoft.Dafny.CompilerDriver.BoogieAsync(DafnyOptions options, String baseName, IEnumerable`1 boogiePrograms, String programId) in /com.docker.devenvironments.code/Source/DafnyDriver/CompilerDriver.cs:line 406
   at Microsoft.Dafny.CompilerDriver.ProcessFilesAsync(IReadOnlyList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, DafnyOptions options, ProofDependencyManager depManager, Boolean lookForSnapshots, String programId) in /com.docker.devenvironments.code/Source/DafnyDriver/CompilerDriver.cs:line 307
   at Microsoft.Dafny.CompilerDriver.Run(DafnyOptions options) in /com.docker.devenvironments.code/Source/DafnyDriver/CompilerDriver.cs:line 67
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass5_0.<<SetHandlerUsingDafnyOptionsContinuation>g__Handle|0>d.MoveNext() in /com.docker.devenvironments.code/Source/DafnyDriver/DafnyNewCli.cs:line 114
--- End of stack trace from previous location ---
   at System.CommandLine.Invocation.AnonymousCommandHandler.InvokeAsync(InvocationContext context)
   at System.CommandLine.Invocation.InvocationPipeline.<>c__DisplayClass4_0.<<BuildInvocationChain>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass17_0.<<UseParseErrorReporting>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass12_0.<<UseHelp>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass16_0.<<AddDeveloperHelp>b__0>d.MoveNext() in /com.docker.devenvironments.code/Source/DafnyDriver/DafnyNewCli.cs:line 264
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass22_0.<<UseVersionOption>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass19_0.<<UseTypoCorrections>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<UseSuggestDirective>b__18_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass16_0.<<UseParseDirective>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<RegisterWithDotnetSuggest>b__5_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass8_0.<<UseExceptionHandler>b__0>d.MoveNext()

What happened?

This should verify as-is; I wonder if the datatype extending a trait is the culprit.

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

Mac
@ssomayyajula ssomayyajula added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label part: boogie Happens after passing the program to Boogie labels Jan 10, 2024
@ssomayyajula ssomayyajula changed the title Verifier crash due to decreases clause in trait Boogie crash due to decreases clause in trait Jan 10, 2024
@ssomayyajula ssomayyajula added the crash Dafny crashes on this input, or generates malformed code that can not be executed label Jan 10, 2024
@ssomayyajula ssomayyajula mentioned this issue Jan 12, 2024
Closed
@keyboardDrummer keyboardDrummer added during 2: compilation of correct program Dafny rejects a valid program during compilation priority: next Will consider working on this after in progress work is done labels Feb 7, 2024
@RustanLeino RustanLeino mentioned this issue Feb 14, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
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: boogie Happens after passing the program to Boogie priority: next Will consider working on this after in progress work is done
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Termination override check for certain non-reference trait implementations fabiomadge/dafny
2 participants
@keyboardDrummer @ssomayyajula