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

Use of 'const' in pattern matching results in error (unhandled exception) #5776

Open
seebees opened this issue Sep 17, 2024 · 4 comments
Open

Use of 'const' in pattern matching results in error (unhandled exception) #5776

seebees opened this issue Sep 17, 2024 · 4 comments
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@seebees
Copy link

seebees commented Sep 17, 2024

Dafny version

4.8.0

Code to produce this issue

const BB := false 

function test(a: bool): bool 
{
    match a 
        case BB => false 
        case _ => true
}

Command to run and resulting output

dafny verify

What happened?

Unhandled exception: System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.EmitNestedMatchStmtCaseConstructor(String sourceName, Type sourceType, IdPattern idPattern, ConcreteSyntaxTree result, Boolean lastCase) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs:line 671
at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.EmitNestedMatchCaseConditions(String sourceName, Type sourceType, ExtendedPattern pattern, ConcreteSyntaxTree writer, Boolean lastCase) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs:line 636
at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.EmitNestedMatchGeneric(INestedMatch match, Boolean preventCaseFallThrough, Action2 emitBody, Boolean inLetExprBody, ConcreteSyntaxTree output) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs:line 604 at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.TrOptNestedMatchExpr(NestedMatchExpr match, Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts, Boolean inLetExprBody, IVariable accumulatorVar, OptimizedExpressionContinuation continuation) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs:line 728 at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.EmitNestedMatchExpr(NestedMatchExpr match, Boolean inLetExprBody, ConcreteSyntaxTree output, ConcreteSyntaxTree wStmts) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs:line 720 at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.EmitExpr(Expression expr, Boolean inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs:line 381 at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.Expr(Expression expr, Boolean inLetExprBody, ConcreteSyntaxTree wStmts) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs:line 4730 at Microsoft.Dafny.Compilers.CsharpCodeGenerator.EmitMapBuilder_Add(MapType mt, IToken tok, String collName, Expression term, Boolean inLetExprBody, ConcreteSyntaxTree wr) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs:line 3428 at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.EmitExpr(Expression expr, Boolean inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs:line 526 at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.TrExprOpt(Expression expr, Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts, Boolean inLetExprBody, IVariable accumulatorVar, OptimizedExpressionContinuation continuation) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs:line 2932 at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.CompileReturnBody(Expression body, Type resultType, ConcreteSyntaxTree wr, IVariable accumulatorVar) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs:line 3096 at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.CompileFunction(Function f, IClassWriter cw, Boolean lookasideBody) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs:line 2744 at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWriter classWriter) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs:line 2303 at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleDefinition module) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs:line 1649 at Microsoft.Dafny.Compilers.SinglePassCodeGenerator.Compile(Program program, ConcreteSyntaxTree wrx) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs:line 1520 at Microsoft.Dafny.ExecutableBackend.Compile(Program dafnyProgram, String dafnyProgramName, ConcreteSyntaxTree output) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyCore/Backends/ExecutableBackend.cs:line 35 at Microsoft.Dafny.SynchronousCliCompilation.<>c__DisplayClass20_1.<CompileDafnyProgram>b__1() in /Users/runner/work/dafny/dafny/dafny/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs:line 676 at System.Threading.Tasks.Task.InnerInvoke() at System.Threading.Tasks.Task.<>c.<.cctor>b__272_0(Object obj) at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state) --- End of stack trace from previous location --- at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state) at System.Threading.Tasks.Task.ExecuteWithThreadLocal(Task& currentTaskSlot, Thread threadPoolThread) --- End of stack trace from previous location --- at Microsoft.Dafny.SynchronousCliCompilation.CompileDafnyProgram(Program dafnyProgram, String dafnyProgramName, ReadOnlyCollection1 otherFileNames, Boolean invokeCompiler) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs:line 676
at Microsoft.Dafny.SynchronousCliCompilation.Compile(String fileName, ReadOnlyCollection1 otherFileNames, Program dafnyProgram, PipelineOutcome oc, IDictionary2 moduleStats, Boolean verified) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs:line 533
at Microsoft.Dafny.SynchronousCliCompilation.ProcessFilesAsync(IReadOnlyList1 dafnyFiles, ReadOnlyCollection1 otherFileNames, DafnyOptions options, ProofDependencyManager depManager, Boolean lookForSnapshots, String programId) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs:line 306
at Microsoft.Dafny.SynchronousCliCompilation.Run(DafnyOptions options) in /Users/runner/work/dafny/dafny/dafny/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs:line 61
at Microsoft.Dafny.TranslateCommand.<>c__DisplayClass3_0.<b__0>d.MoveNext() in /Users/runner/work/dafny/dafny/dafny/Source/DafnyDriver/Commands/TranslateCommand.cs:line 48
--- End of stack trace from previous location ---
at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass5_0.<g__Handle|0>d.MoveNext() in /Users/runner/work/dafny/dafny/dafny/Source/DafnyDriver/DafnyNewCli.cs:line 140
--- End of stack trace from previous location ---
at System.CommandLine.Invocation.AnonymousCommandHandler.InvokeAsync(InvocationContext context)
at System.CommandLine.Invocation.InvocationPipeline.<>c__DisplayClass4_0.<b__0>d.MoveNext()
--- End of stack trace from previous location ---
at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass17_0.<b__0>d.MoveNext()
--- End of stack trace from previous location ---
at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass12_0.<b__0>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass17_0.<b__0>d.MoveNext() in /Users/runner/work/dafny/dafny/dafny/Source/DafnyDriver/DafnyNewCli.cs:line 268
--- End of stack trace from previous location ---
at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass22_0.<b__0>d.MoveNext()
--- End of stack trace from previous location ---
at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass19_0.<b__0>d.MoveNext()
--- End of stack trace from previous location ---
at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<b__18_0>d.MoveNext()
--- End of stack trace from previous location ---
at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass16_0.<b__0>d.MoveNext()
--- End of stack trace from previous location ---
at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<b__5_0>d.MoveNext()
--- End of stack trace from previous location ---
at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass8_0.<b__0>d.MoveNext()

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

Linux
@seebees seebees added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Sep 17, 2024
@seebees
Copy link
Author

seebees commented Sep 17, 2024

I think that this is a regression of #4214.

You can see this in my CI: https://github.com/aws/aws-cryptographic-material-providers-library/actions/runs/10835523115/job/30067278531?pr=594#step:11:586

For: aws/aws-cryptographic-material-providers-library#594
specifically:
https://github.com/aws/aws-cryptographic-material-providers-library/pull/594/files#diff-9b50a2e65e8f0bca0deb62c50446bbbf810faaf194355a8a78bbef2baf9c880cR150

Here is a link to the original code:
https://github.com/aws/aws-cryptographic-material-providers-library/blob/f3a0a5269e611afd254425226d32eaaed1f3d99b/AwsCryptographicMaterialProviders/dafny/AwsCryptographyKeyStore/src/Structure.dfy#L125-L137

@keyboardDrummer
Copy link
Member

Might be caused by: #5528

@seebees seebees mentioned this issue Oct 4, 2024
Open
@keyboardDrummer
Copy link
Member

The description of this issue says to run dafny verify but based on the stack-trace it seems you're running the C# code generator.

@keyboardDrummer
Copy link
Member

I can't reproduce this issue with the provided code sample

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@seebees @keyboardDrummer