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

Exception when generating doo file with --no-verify flag #5143

Closed
ShubhamChaturvedi7 opened this issue Mar 4, 2024 · 1 comment · Fixed by #5152
Closed

Exception when generating doo file with --no-verify flag #5143

ShubhamChaturvedi7 opened this issue Mar 4, 2024 · 1 comment · Fixed by #5152
Assignees
@robin-aws
Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: next Will consider working on this after in progress work is done release-blocker Must be resolved before the next release

Comments

@ShubhamChaturvedi7
Copy link
Collaborator

Dafny version

master branch

Code to produce this issue

Commit id: f2d6e5cab8d478ee5aed5991114f80ddb01af38e

Command to run and resulting output

dafny build -t:lib --no-verify dafny_go.dfy

What happened?

I get a NPE:

Dafny program verifier did not attempt verification
Unhandled exception: System.NullReferenceException: Object reference not set to an instance of an object.
   at DafnyCore.DooFile.ManifestData..ctor(DafnyOptions options) in /Users/scchatur/workspace/DafnyLang/dafny/Source/DafnyCore/DooFile.cs:line 42
   at DafnyCore.DooFile..ctor(Program dafnyProgram) in /Users/scchatur/workspace/DafnyLang/dafny/Source/DafnyCore/DooFile.cs:line 113
   at Microsoft.Dafny.Compilers.LibraryBackend.Compile(Program dafnyProgram, ConcreteSyntaxTree output) in /Users/scchatur/workspace/DafnyLang/dafny/Source/DafnyCore/Backends/Library/LibraryBackend.cs:line 82
   at Microsoft.Dafny.SynchronousCliCompilation.<>c__DisplayClass20_1.<CompileDafnyProgram>b__1() in /Users/scchatur/workspace/DafnyLang/dafny/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs:line 668
   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, ReadOnlyCollection`1 otherFileNames, Boolean invokeCompiler) in /Users/scchatur/workspace/DafnyLang/dafny/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs:line 668
   at Microsoft.Dafny.SynchronousCliCompilation.Compile(String fileName, ReadOnlyCollection`1 otherFileNames, Program dafnyProgram, PipelineOutcome oc, IDictionary`2 moduleStats, Boolean verified) in /Users/scchatur/workspace/DafnyLang/dafny/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs:line 525
   at Microsoft.Dafny.SynchronousCliCompilation.ProcessFilesAsync(IReadOnlyList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, DafnyOptions options, ProofDependencyManager depManager, Boolean lookForSnapshots, String programId) in /Users/scchatur/workspace/DafnyLang/dafny/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs:line 300
   at Microsoft.Dafny.SynchronousCliCompilation.Run(DafnyOptions options) in /Users/scchatur/workspace/DafnyLang/dafny/Source/DafnyDriver/Legacy/SynchronousCliCompilation.cs:line 62
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass5_0.<<SetHandlerUsingDafnyOptionsContinuation>g__Handle|0>d.MoveNext() in /Users/scchatur/workspace/DafnyLang/dafny/Source/DafnyDriver/DafnyNewCli.cs:line 116
--- 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__DisplayClass17_0.<<AddDeveloperHelp>b__0>d.MoveNext() in /Users/scchatur/workspace/DafnyLang/dafny/Source/DafnyDriver/DafnyNewCli.cs:line 270
--- 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()

Process finished with exit code 1.

The stable released version 4.4 generates a doo with no-verify=true in the manifest. This seems like a regression related to how we set SolverVersion in the DooFile.cs .

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

Mac
@ShubhamChaturvedi7 ShubhamChaturvedi7 added the kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label label Mar 4, 2024
@robin-aws robin-aws added the release-blocker Must be resolved before the next release label Mar 4, 2024
@robin-aws
Copy link
Member

Note this regression should likely have been caught by the separate-verification/assumptions.dfy test case, but the ! operator accepts the non-zero exit code (and I'm not clear why that command is expected to fail), and the extra stderr output doesn't automatically make the test fail. It would be a great idea to tighten that up.

@robin-aws robin-aws added the priority: next Will consider working on this after in progress work is done label Mar 4, 2024
@robin-aws robin-aws self-assigned this Mar 5, 2024
@robin-aws robin-aws mentioned this issue Mar 6, 2024
Merged
robin-aws added a commit that referenced this issue Mar 6, 2024
@robin-aws
fix: Avoid NPE when building a doo file with —no-verify (#5152)
5ece05f 
### Description
Fixes #5143.

### How has this been tested?
Added this case to `separate-verification/app.dfy`.

`separate-verification/assumptions.dfy` SHOULD have caught this
regression, but unfortunately the command that triggers the exception
uses `!` to expect a non-zero exit code, and LIT test commands usually
only redirect stdout to a file to diff against the expected output, so
the extra stderr output with the exception trace is lost.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@robin-aws robin-aws

Labels
kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label priority: next Will consider working on this after in progress work is done release-blocker Must be resolved before the next release
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: Avoid NPE when building a doo file with —no-verify robin-aws/dafny
2 participants
@ShubhamChaturvedi7 @robin-aws