search

viperproject / viperserver

HTTP server that manages verification requests to different tools from the Viper tool stack.
Other
10 stars 17 forks source link

Carbon doesn't seem to initialise correctly if paths contain whitespace #103

Closed alexanderjsummers closed 1 year ago

alexanderjsummers commented 1 year ago

Using either Stable or Nightly from the VSCode extension I can't run carbon on a new Windows machine. The ViperServer output includes:

2:14:52.876 The command `carbon --z3Exe c:\Users\Alex Summers\AppData\Roaming\Code\User\globalStorage\viper-admin.viper\Nightly\ViperTools\z3\bin\z3.exe --boogieExe c:\Users\Alex Summers\AppData\Roaming\Code\User\globalStorage\viper-admin.viper\Nightly\ViperTools\boogie\Binaries\Boogie.exe` resulted in an exception.

I can't see the exception, but it looks to me as though the space in "Alex Summers" (which is unfortunate as a user name) might be tripping this up; at least if the printed command is accurate this seems unlikely to work as is.

ArquintL commented 1 year ago

The path on macOS always contains white spaces and Silicon & Carbon work fine there. It's however correct that the path is not correctly escaped in the log output (each command argument is a string and they simply get concatenated).

About 3 weeks ago, I've extended the logging slightly and when you get the "... resulted in an exception" error, ViperServer should have entered this branch here, which also prints the stack trace (in a somewhat ugly way).

Could you please check whether you get this additional output (first switch to the Nightly build channel and then update the ViperTools) and what it says?

marcoeilers commented 1 year ago

@alexanderjsummers It would be great if you could have a look at the logged stack trace so we can figure out if this is a blocker for the release or not.

alexanderjsummers commented 1 year ago

Thanks for the help! I looked into it some more and it seems I was just unlucky in that the examples I was trying illustrated a different problem (an actual crash in Carbon). I think this is unrelated to the paths (it would be nice to print those differently I guess, but that seems like a minor improvement). I'll close this issue and open others :)

alexanderjsummers commented 1 year ago

By the way @ArquintL I am on Nightly with the latest tools, I believe - unfortunately I don't see the stack trace. Should that show up in the "Viper Server" output?

marcoeilers commented 1 year ago

Great, thanks!

alexanderjsummers commented 1 year ago

No problem - thanks for pinging. From my perspective the new issues aren't blocking (and also aren't new in this release, as far as I know).

ArquintL commented 1 year ago

By the way @ArquintL I am on Nightly with the latest tools, I believe - unfortunately I don't see the stack trace. Should that show up in the "Viper Server" output?

Yes, 3-5 lines above the line stating that the command resulted in an exception. It could be that you've missed the stack trace because it's printed in a funny way: We print each stack trace entry as a line consisting of the class and method name and the line number