search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.85k stars 256 forks source link

internal error on match with static const of newtype #5405

Open erniecohen opened 2 months ago

erniecohen commented 2 months ago

Failing code

newtype T = nat {
    static const C := 0 as T
    const V:bool := match this case C => true
}

Steps to reproduce the issue

Expected behavior

not crashing

Actual behavior

Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues. System.NullReferenceException: Object reference not set to an instance of an object. at Microsoft.Dafny.MatchFlattener.LetBind(IdPattern var, Expression genExpr, PatternPath bodyPath) at Microsoft.Dafny.MatchFlattener.LetBindNonWildCard(IdPattern idPattern, Expression expr, PatternPath bodyPath) at Microsoft.Dafny.MatchFlattener.<>cDisplayClass14_0.b4(PatternPath path) at System.Linq.Enumerable.SelectListIterator2.ToList() at Microsoft.Dafny.MatchFlattener.CompilePatternPathsForMatchee(MatchCompilationState state, MatchingContext context, List1 paths, Cons1 consMatchees) at Microsoft.Dafny.MatchFlattener.CompilePatternPaths(MatchCompilationState state, MatchingContext context, SinglyLinkedList1 matchees, List`1 paths) at Microsoft.Dafny.MatchFlattener.CompileNestedMatchExpr(NestedMatchExpr nestedMatchExpr) at Microsoft.Dafny.MatchFlattener.<>cDisplayClass5_0.b0(INode node) at Microsoft.Dafny.Node.Visit(Func2 beforeChildren, Action1 afterChildren, Action`1 reportError) at Microsoft.Dafny.MatchFlattener.FlattenNode(Node root) at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation) at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) at Microsoft.Dafny.LanguageServer.Language.CachingResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>cDisplayClass5_0.b0() at Microsoft.Dafny.LanguageServer.Language.CachingResolver.Resolve(CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken) at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken) at Microsoft.Dafny.TextDocumentLoader.<>cDisplayClass5_0.<b0>d.MoveNext() --- End of stack trace from previous location --- at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken) at Microsoft.Dafny.Compilation.ResolveAsync()

erniecohen commented 2 months ago

no crash when match is replaced with conditionals

keyboardDrummer commented 2 months ago

Moved to dafny-lang/dafny since this does not seem IDE related.