dafny
dafny copied to clipboard
Published
20 hours ago •
dafny-lang
dafny-lang
Resolver crash when using language server
Resolver crash
Program:
trait Computation<T> {
function run(): T
}
class Stop<T> extends Computation<T> {
var value: T;
constructor(value: T) {
this.value := value;
}
function run(): T { value }
}
class Stop<T> extends Computation<T> {
var value: T;
constructor(value: T) {
this.value := value;
}
function run(): T { value }
}
Stacktrace:
[Trace - 5:21:28 AM] Received response 'textDocument/documentSymbol - (204)' in 7ms. Request failed: Internal Error - System.Collections.Generic.KeyNotFoundException: The given key 'T' was not present in the dictionary.
at System.Collections.Generic.Dictionary`2.get_Item(TKey key)
at Microsoft.Dafny.Type.<>c__DisplayClass82_0.<AsParentType>b__0(TypeParameter tp) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/AST/DafnyAst.cs:line 1175
at System.Collections.Generic.List`1.ConvertAll[TOutput](Converter`2 converter)
at Microsoft.Dafny.Type.AsParentType(TopLevelDecl parent) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/AST/DafnyAst.cs:line 1176
at Microsoft.Dafny.Resolver.ResolveExprDotCall(IToken tok, Expression receiver, Type receiverTypeBound, MemberDecl member, List`1 args, List`1 optTypeArguments, ResolveOpts opts, Boolean allowMethodCall) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 16528
at Microsoft.Dafny.Resolver.ResolveNameSegment(NameSegment expr, Boolean isLastNameSegment, List`1 args, ResolveOpts opts, Boolean allowMethodCall, Boolean complain) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 15992
at Microsoft.Dafny.Resolver.ResolveExpression(Expression expr, ResolveOpts opts) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 14676
at Microsoft.Dafny.Resolver.ResolveFunction(Function f) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 10156
at Microsoft.Dafny.Resolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 9559
at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 2811
at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 1024
at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 497
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(TextDocumentItem document, Program program) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs:line 54
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(TextDocumentItem textDocument, Program program, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs:line 44
at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadInternal(LoadRequest loadRequest) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs:line 130
at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.Run() in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs:line 100
--- End of stack trace from previous location ---
at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadAsync(TextDocumentItem textDocument, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs:line 90
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.GetDocumentAsync(TextDocumentIdentifier documentId) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 212
at Microsoft.Dafny.LanguageServer.Handlers.DafnyDocumentSymbolHandler.Handle(DocumentSymbolParams request, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs:line 44
at OmniSharp.Extensions.LanguageServer.Server.Pipelines.SemanticTokensDeltaPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at OmniSharp.Extensions.LanguageServer.Server.Pipelines.ResolveCommandPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestPreProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestPostProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.<RouteRequest>g__InnerRoute|7_0(IServiceScopeFactory serviceScopeFactory, Request request, TDescriptor descriptor, Object params, CancellationToken token, ILogger logger)
at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.RouteRequest(IRequestDescriptor`1 descriptors, Request request, CancellationToken token)
at OmniSharp.Extensions.JsonRpc.DefaultRequestInvoker.<>c__DisplayClass10_0.<<RouteRequest>b__5>d.MoveNext() (-32603).
[Error - 5:21:28 AM] Request textDocument/documentSymbol failed.
Message: Internal Error - System.Collections.Generic.KeyNotFoundException: The given key 'T' was not present in the dictionary.
at System.Collections.Generic.Dictionary`2.get_Item(TKey key)
at Microsoft.Dafny.Type.<>c__DisplayClass82_0.<AsParentType>b__0(TypeParameter tp) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/AST/DafnyAst.cs:line 1175
at System.Collections.Generic.List`1.ConvertAll[TOutput](Converter`2 converter)
at Microsoft.Dafny.Type.AsParentType(TopLevelDecl parent) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/AST/DafnyAst.cs:line 1176
at Microsoft.Dafny.Resolver.ResolveExprDotCall(IToken tok, Expression receiver, Type receiverTypeBound, MemberDecl member, List`1 args, List`1 optTypeArguments, ResolveOpts opts, Boolean allowMethodCall) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 16528
at Microsoft.Dafny.Resolver.ResolveNameSegment(NameSegment expr, Boolean isLastNameSegment, List`1 args, ResolveOpts opts, Boolean allowMethodCall, Boolean complain) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 15992
at Microsoft.Dafny.Resolver.ResolveExpression(Expression expr, ResolveOpts opts) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 14676
at Microsoft.Dafny.Resolver.ResolveFunction(Function f) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 10156
at Microsoft.Dafny.Resolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 9559
at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 2811
at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 1024
at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/Dafny/Resolver.cs:line 497
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(TextDocumentItem document, Program program) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs:line 54
at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(TextDocumentItem textDocument, Program program, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs:line 44
at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadInternal(LoadRequest loadRequest) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs:line 130
at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.Run() in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs:line 100
--- End of stack trace from previous location ---
at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadAsync(TextDocumentItem textDocument, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs:line 90
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.ApplyChangesAsync(Task`1 oldDocumentTask, DidChangeTextDocumentParams documentChange, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 172
at Microsoft.Dafny.LanguageServer.Workspace.DocumentDatabase.GetDocumentAsync(TextDocumentIdentifier documentId) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs:line 212
at Microsoft.Dafny.LanguageServer.Handlers.DafnyDocumentSymbolHandler.Handle(DocumentSymbolParams request, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/release-dafny/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs:line 44
at OmniSharp.Extensions.LanguageServer.Server.Pipelines.SemanticTokensDeltaPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at OmniSharp.Extensions.LanguageServer.Server.Pipelines.ResolveCommandPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestPreProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestPostProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.<RouteRequest>g__InnerRoute|7_0(IServiceScopeFactory serviceScopeFactory, Request request, TDescriptor descriptor, Object params, CancellationToken token, ILogger logger)
at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.RouteRequest(IRequestDescriptor`1 descriptors, Request request, CancellationToken token)
at OmniSharp.Extensions.JsonRpc.DefaultRequestInvoker.<>c__DisplayClass10_0.<<RouteRequest>b__5>d.MoveNext()
Code: -32603
