Analysis of longjmp/setjmp

[michael-schwarz]

PR to document the ongoing progress towards sound handling of longjmp/setjmp.

Corresponding draft for those with access to versioncontrolseidl: https://versioncontrolseidl.in.tum.de/schwarz/longjmp-and-setjmp

Issues that need to be handled:

• Non-unique jump buffers
• Jumping from several functions deep
• Jumping in recursive calls
• Returning a value that is potentially zero in longjmp call
• Warn for longjmps that propagate out of the current thread
• ...?
• Detecting misuse
  • Jumping from different thread
  • Accessing non-volatile local variable that has been potentially modified since call
  • setjmp in invalid place (not directly used for branching) (deemed out of scope)
  • sigsetjmp

Closes #887

[michael-schwarz]

I'll also start a testrun of this with the benchmarks we used for SOAP.

[michael-schwarz]

The changes increase the runtime for libpng by ~ 10%. I could not inspect warnings, as they now are in the behavior category, so I restarted a run where I increased the level of output again.

[sim642]

Interesting, I'm not sure what might've caused it but I have a few ideas from my changes in #1015:

1. Replace context hashes with ControlSpecC (1f7424f). This makes things more reliable but such elements in sets are also more expensive to compare, etc than just ints.
2. I also changed the normal combine (7e70553). Previously it changed local without adapting ask.
3. Using Access events (ba3437a, d7708d3, f2eb6e0) might be making things more expensive while in single-threaded mode. Normally those events are not emitted, but with these new analyses they are.

[michael-schwarz]

I was able to verify that the output is still as expected. W.r.t. the slowdown, I don't think it is critical for this PR, I think it can be addressed in a separate PR.

[sim642]

For some reason marshaling tests on the new test group fail across the board: https://github.com/goblint/analyzer/actions/runs/4516943406.

[michael-schwarz]

Maybe it's because contexts are not relifted inside domain values?

[michael-schwarz]

After relifting the contents of jumpbuffers, it works if done manually:

./regtest.sh 68 02 --set save_run save
./regtest.sh 68 02 --set load_run save

For some reason, it still fails when invoked via the script.

[sim642]

Interesting, I'm not sure what might've caused it but I have a few ideas from my changes in #1015:

2. I also changed the normal combine 7e70553. Previously it changed local without adapting ask.

I benchmarked this just this change on sv-benchmarks with master and there wasn't a performance difference.
So at least this change, which affects Goblint even without longjmp analyses, doesn't hurt us in general.

[sim642]

After relifting the contents of jumpbuffers, it works if done manually:

./regtest.sh 68 02 --set save_run save
./regtest.sh 68 02 --set load_run save

For some reason, it still fails when invoked via the script.

That's not how marshaling tests do it though. The second run uses --conf save/config.json --set save_run '' --set load_run save.
Exactly using the full commands used by update_suite.rb, I can reproduce the fixpoint error still.

[michael-schwarz]

For some reason, there are two paths when the incremental analysis checks if the fixpoint is reached, but only one in the marshalled result.

[sim642]

I've started looking into this myself already. We have quite many relifts missing, but that's hidden by the default one. Making the default one in Printable.Std fail allows tracking down any missing ones that we've been too lazy to add. I've done that for everything in this particular example, but there's still an issue, but it's now inside base's jmpbuf domain.

[michael-schwarz]

I didn't know you already started looking into it. I added some of these relifts directly on master (fae675b), these are probably superseded by your changes.