Reveal label inside match case causes crash #6268
Description
Dafny version
4.10.0
Code to produce this issue
datatype Color = Red | Blue
method Test(color: Color)
{
match color
case Red =>
assert L: true;
reveal L;
case Blue =>
}Command to run and resulting output
$ dafny verify dfyconfig.toml
Encountered internal compilation exception: Object reference not set to an instance of an object.
Verifier/Verifier.dfy(7,10): Error: Internal error occurred during verification: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<<VerifyUnverifiedSymbol>b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed)
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed)
at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable`1 randomSeed)+MoveNext()
|
7 | newtype Incarnations = map<Variable, Var>
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Unhandled exception. System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Boogie.PredicateCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.AssumeCmd.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Block.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Implementation.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(ResolutionContext rc)
at Microsoft.Boogie.Program.Resolve(CoreOptions options, IErrorSink errorSink)
at Microsoft.Boogie.ExecutionEngine.GetVerificationTasks(Program program, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.DafnyProgramVerifier.GetVerificationTasksAsync(ExecutionEngine engine, ResolutionResult resolution, ModuleDefinition moduleDefinition, CancellationToken cancellationToken)
at Microsoft.Dafny.Compilation.<>c__DisplayClass58_0.<<VerifyUnverifiedSymbol>b__1>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed)
at Microsoft.Dafny.Compilation.VerifyUnverifiedSymbol(Boolean onlyPrepareVerificationForGutterTests, ICanVerify canVerify, ResolutionResult resolution, Func`2 taskFilter, Nullable`1 randomSeed)
at DafnyDriver.Commands.CliCompilation.VerifyAllLazily(Nullable`1 randomSeed)+System.Threading.Tasks.Sources.IValueTaskSource<System.Boolean>.GetResult()
at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 50
--- End of stack trace from previous location ---
at System.Reactive.PlatformServices.ExceptionServicesImpl.Rethrow(Exception exception) in /_/Rx.NET/Source/src/System.Reactive/Internal/ExceptionServicesImpl.cs:line 16
at System.Reactive.ExceptionHelpers.Throw(Exception exception) in /_/Rx.NET/Source/src/System.Reactive/Internal/ExceptionServices.cs:line 14
at System.Reactive.Stubs.<>c.<.cctor>b__2_1(Exception ex) in /_/Rx.NET/Source/src/System.Reactive/Internal/Stubs.cs:line 16
at System.Reactive.AnonymousObserver`1.OnErrorCore(Exception error) in /_/Rx.NET/Source/src/System.Reactive/AnonymousObserver.cs:line 73
at System.Reactive.ObserverBase`1.OnError(Exception error) in /_/Rx.NET/Source/src/System.Reactive/ObserverBase.cs:line 59
at System.Reactive.Subjects.Subject`1.OnError(Exception error) in /_/Rx.NET/Source/src/System.Reactive/Subjects/Subject.cs:line 103
at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 60
--- End of stack trace from previous location ---
at System.Linq.AsyncEnumerable.ToObservableObservable`1.<>c__DisplayClass2_0.<<Subscribe>g__Core|0>d.MoveNext() in /_/Ix.NET/Source/System.Linq.Async/System/Linq/Operators/ToObservable.cs:line 74
--- End of stack trace from previous location ---
at System.Threading.Tasks.Task.<>c.<ThrowAsync>b__128_1(Object state)
at System.Threading.ThreadPoolWorkQueue.Dispatch()
at System.Threading.PortableThreadPool.WorkerThread.WorkerThreadStart()
at System.Threading.Thread.StartCallback()
What happened?
Dafny crashes. It's generating malformed Boogie from the reveal L; statement. (I'm guessing the problem has to do with the rewriting of match earlier in the Dafny pipeline.)
Note: The crash also occurs if the assert L: true; is moved before the match.
What type of operating system are you experiencing the problem on?
Mac