Abstract debugging

[FeldrinH]

This pull request adds abstract debugging support. It also includes some tweaks and additions that are helpful for debugging and/or using abstract debugging. Some changes are accompanied by refactoring of surrounding/related code.

Changes:

• Added abstract debugging (all files under abstractdebugging package)
• Added description of abstract debugging to readme.
• Added some example C programms for demonstrating abstract debugging to folder adb_examples.
• Changed and refactored main to include abstract debugging
• Removed duplicate definitions of Goblint location type. Moved all usages to GoblintLocation.
• Retrofitted CFG HTTP handler to serve ARG instead if the function name is <arg>.
• Added show arg code lens to main function. (retrofitted to GoblintCFGAnalysisResult to avoid duplicate code)
• Added lots of new methods to GoblintService and renamed some existing ones for consistency.
• Tweaked JSON-RPC handler debug logging.
• Added Goblint version to debug output (version is checked using goblint --version; command is executed only if debug logging is enabled).

Changes made based on review comments:

• Added and documented config option to enable/disable abstract debugging.
• Improved HTTP handler error handling (this is necessary to ensure that clicking 'show arg' when ARG generation is disabled shows an error to the user)
• Moved debugger socket file to OS temp directory.

TODO

• [x] GobPie option to disable abstract debugging, in particular the --enable exp.arg for all analyses.

[sim642]

For some reason this doesn't work for me with the current Goblint version (b592c3c6157ec94198254b0d85bbf6903f949751). If I set a breakpoint into thesis_example.c, then it initially shows the state and call stack, but after clicking any stepping operation nothing happens. All the stepping buttons become disabled and the variables/call stack views become empty. There's nothing in the GobPie log either:

10:59:45.810 INFO  - Goblint run with command: goblint --enable exp.arg --enable server.enabled --enable server.reparse --set server.mode unix --set server.unix-socket /home/simmo/dev/GobPie/adb_examples/goblint.sock
10:59:45.940 INFO  - Goblint client connected
10:59:45.965 INFO  - HTTP server started on: http://localhost:33563/
10:59:45.996 INFO  - MagpieBridge server launched.
10:59:46.016 INFO  - Abstract debugging server launched.
10:59:46.123 INFO  - ---------------------- Analysis started ----------------------
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 24
  dead: 0
  total lines: 24
10:59:46.273 INFO  - --------------------- Analysis finished ----------------------
11:00:00.763 INFO  - Accepted new connection to abstract debugging server.
11:00:00.811 INFO  - Debug adapter initialized, waiting for configuration
11:00:00.817 INFO  - Setting breakpoints for /home/simmo/dev/GobPie/adb_examples/thesis_example.c (thesis_example.c)
11:00:00.829 INFO  - Debug adapter configuration done
11:00:00.829 INFO  - Debug adapter launched
11:00:00.842 INFO  - Stopped on breakpoint 0 (thesis_example.c 21:9-21:15)

[sim642]

Apparently VSCode 1.78 broke DAP:

• https://github.com/microsoft/vscode/issues/181485
• https://github.com/microsoft/vscode/issues/181825
• https://github.com/microsoft/AL/issues/7388
• https://github.com/microsoft/AL/issues/7404

The supposed fix (https://github.com/microsoft/vscode/issues/181966) doesn't really work though. Downgrading to VSCode 1.77 seems to make this work again...

[FeldrinH]

It is worth noting that the abstract debugger technically violates the spec when it comes to the timing of stop events, but several other debuggers do this as well. (See comment in AbstractDebuggingServer.onThreadsStopped)

Edit: I found out that Microsoft's Mock Debug actually has fixed the stop event timing issue and I simply failed to notice the fix last time I looked at it. Unfortunately the fix depends on JavaScripts single-threaded nature and cannot be used in Java.

[FeldrinH]

At least according to the DAP spec the problem is on my end. The fact that it worked before could technically be considered a bug in VSCode's DAP client that has now been fixed. I will try to fix this on the abstract debugger side as soon as possible.

[FeldrinH]

The problem should now be fixed. The fix isn't particularly nice and there are some pitfalls to correctly using the queueing API where calls to other methods can cause events to be sent prematurely. However, it avoids depending on Java API-s that are explicitly marked as not reliable for synchronization use, so I consider it better than the alternative proposed in https://github.com/eclipse-lsp4j/lsp4j/issues/229.

[FeldrinH]

I have made changes based on the comments.