search

dafny-lang / dafny

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

IDE does not provide feedback if the solver can not be started #5131

Open Timmmm opened 7 months ago

Timmmm commented 7 months ago

Failing code

method MaxSum(x: int, y: int) returns (s: int, m: int)
  ensures m >= x && m >= y
  ensures m == x || m == y
  ensures s == x + y
{
    s := x + y;
    m := if x > y then x else y;
}

method Main() {
    var s, m := MaxSum(1928, 1);
    assert s == 1929;
    assert m == 1928;
}

Steps to reproduce the issue

Expected behavior

It proves or disproves something.

Actual behavior

It just looks like this forever:

image

I'm not even sure how to debug this. There's nothing printed at all in the Dafny VSCode output log. The Dafny Language Server log just says:

[Error - 12:53:58] Server process exited with code 0.
Timmmm commented 7 months ago

Oh I should say this is on RHEL 8.

keyboardDrummer commented 7 months ago

I haven't been able to reproduce this on macOS. Could you look in the Dafny VSCode output channel?

image

It should say which Dafny binary it's launching, like this:

Language server: {"command":"/usr/local/share/dotnet/dotnet","args":["/Users/rwillems/.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/nightly-2024-02-15-73fcdf3/github/dafny/Dafny.dll","server","--verify-on:Save","--verification-time-limit:30","--cache-verification=0","--cores:6","--notify-ghostness:true","--notify-line-verification-status:false","--log-level=Debug","--log-location=/Users/rwillems/Documents/Sync/Temp"]}
Dafny is ready

Could you try running that Dafny binary yourself, using dotnet pathToDafny.dll verify pathToDafnyFile.dfy, and see what the output is?

Timmmm commented 7 months ago

Yep I get

Language server: {"command":"/usr/bin/dotnet","args":["/home/.../.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/4.4.0/github/dafny/Dafny.dll","server","--verify-on:Change","--verification-time-limit:20","--cache-verification=0","--cores:7","--notify-ghostness:true","--notify-line-verification-status:true"]}
Dafny is ready

If I run that command it just sits there with a blinking cursor (maybe that's correct)

❯ /usr/bin/dotnet ~/.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/4.4.0/github/dafny/Dafny.dll server --verify-on:Change --verification-time-limit:20 --cache-verification=0 --cores:7 --notify-ghostness:true --notify-line-verification-status:true

If I try running it, aha, as usual it's bloody glibc. Bane of reliability. I have a copy of Z3 installed already - is there a way to tell it to use the system version (assuming it doesn't depend on the exact version)?

❯ /usr/bin/dotnet ~/.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/4.4.0/github/dafny/Dafny.dll verify ~/workspace/dafny_playground/main.dfy 
Prover error: /home/../.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/4.4.0/github/dafny/z3/bin/z3-4.12.1: /lib64/libstdc++.so.6: version `GLIBCXX_3.4.26' not found (required by /home/../.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/4.4.0/github/dafny/z3/bin/z3-4.12.1)

Prover error: /home/../.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/4.4.0/github/dafny/z3/bin/z3-4.12.1: /lib64/libstdc++.so.6: version `GLIBCXX_3.4.26' not found (required by /home/../.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/4.4.0/github/dafny/z3/bin/z3-4.12.1)

Prover error: /home/../.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/4.4.0/github/dafny/z3/bin/z3-4.12.1: /lib64/libm.so.6: version `GLIBC_2.29' not found (required by /home/../.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/4.4.0/github/dafny/z3/bin/z3-4.12.1)

Prover error: /home/../.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/4.4.0/github/dafny/z3/bin/z3-4.12.1: /lib64/libm.so.6: version `GLIBC_2.29' not found (required by /home/../.vscode/extensions/dafny-lang.ide-vscode-3.2.2/out/resources/4.4.0/github/dafny/z3/bin/z3-4.12.1)

Advisory: MaxSum (correctness) SKIPPED due to I/O exception: Broken pipe
Advisory: Main (correctness) SKIPPED due to I/O exception: Broken pipe
Unhandled exception: System.ArgumentNullException: Value cannot be null. (Parameter 'source')
   at System.Linq.ThrowHelper.ThrowArgumentNullException(ExceptionArgument argument)
   at System.Linq.Enumerable.Select[TSource,TResult](IEnumerable`1 source, Func`2 selector)
   at Microsoft.Dafny.DafnyConsolePrinter.DistillVerificationResult(VerificationResult verificationResult)
   at Microsoft.Dafny.DafnyConsolePrinter.ReportEndVerifyImplementation(Implementation implementation, VerificationResult result)
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass48_0.<VerifyImplementation>b__0(IVerificationStatus status)
   at System.Reactive.Linq.ObservableImpl.Do`1.OnNext._.OnNext(TSource value) in /_/Rx.NET/Source/src/System.Reactive/Linq/Observable/Do.cs:line 38
--- End of stack trace from previous location ---
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass41_0.<<VerifyEachImplementation>b__1>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass41_0.<<VerifyEachImplementation>b__1>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Boogie.ExecutionEngine.VerifyEachImplementation(TextWriter output, ProcessedProgram processedProgram, PipelineStatistics stats, String programId, ErrorReporterDelegate er, String requestId, Implementation[] stablePrioritizedImpls)
   at Microsoft.Boogie.ExecutionEngine.InferAndVerify(TextWriter output, Program program, PipelineStatistics stats, String programId, ErrorReporterDelegate er, String requestId)
   at Microsoft.Dafny.DafnyMain.BoogiePipelineWithRerun(DafnyOptions options, TextWriter output, ExecutionEngine engine, Program program, String bplFileName, String programId)
   at Microsoft.Dafny.DafnyMain.BoogieOnce(DafnyOptions options, TextWriter output, ExecutionEngine engine, String baseFile, String moduleName, Program boogieProgram, String programId)
   at Microsoft.Dafny.CompilerDriver.BoogieOnceWithTimerAsync(TextWriter output, DafnyOptions options, String baseName, String programId, String moduleName, Program program)
   at Microsoft.Dafny.CompilerDriver.<>c__DisplayClass8_0.<<BoogieAsync>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.CompilerDriver.<>c__DisplayClass8_0.<<BoogieAsync>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.CompilerDriver.BoogieAsync(DafnyOptions options, String baseName, IEnumerable`1 boogiePrograms, String programId)
   at Microsoft.Dafny.CompilerDriver.ProcessFilesAsync(IReadOnlyList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, DafnyOptions options, ProofDependencyManager depManager, Boolean lookForSnapshots, String programId)
   at Microsoft.Dafny.CompilerDriver.RunCompiler(DafnyOptions options)
   at Microsoft.Dafny.DafnyCli.<>c__DisplayClass9_0.<<SetHandlerUsingDafnyOptionsContinuation>g__Handle|0>d.MoveNext()
--- 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.DafnyCli.<>c__DisplayClass20_0.<<AddDeveloperHelp>b__0>d.MoveNext()
--- 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()

I'm surprised that error doesn't get surfaced anywhere in VSCode's logs. That should probably be fixed at least.

keyboardDrummer commented 7 months ago

I have a copy of Z3 installed already - is there a way to tell it to use the system version

You can use the --solver-path=pathToYourZ3binary option to specify a path to a different solver, such as your own Z3 installation.

I suggest first testing it with dafny verify until it verifies correctly.

Then, if you want to use this with the IDE, you can specify the option in the Dafny preferences of VSCode, as part of the server launch arguments

image

(assuming it doesn't depend on the exact version)

Yes and no. It can use a range of versions, but the verification performance will be different for different versions.

I'm surprised that error doesn't get surfaced anywhere in VSCode's logs. That should probably be fixed at least.

I agree. I've marked this issue as a bug, and moved it to the repo where the fix should occur.

Timmmm commented 6 months ago

Thanks!

Adding --solver-path=/usr/bin/z3 worked perfectly and adding it in the Language Server Launch Args also worked.

Perhaps z3 could be compiled on an older version of Linux. It's pretty much the only way to get good binary compatibility with binaries that link with glibc.

Kind of a pain in the arse. The GNU people don't care about the issue because of course everything should be built from source according to them... Mac has a similar issue but people generally run very recent versions of MacOS whereas with Linux it's very common to be using an ancient distro with decades-old libraries.

The other option is statically linking with musl.