Conversation
Co-authored-by: Benjamin Bott<bottbenj@users.noreply.github.com>
Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
Refactor `setjmp`/`longjmp` analysis
|
I'll also start a testrun of this with the benchmarks we used for SOAP. |
|
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. |
|
Interesting, I'm not sure what might've caused it but I have a few ideas from my changes in #1015:
|
|
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. |
|
For some reason marshaling tests on the new test group fail across the board: https://github.com/goblint/analyzer/actions/runs/4516943406. |
|
Maybe it's because contexts are not relifted inside domain values? |
|
After relifting the contents of jumpbuffers, it works if done manually:
For some reason, it still fails when invoked via the script. |
I benchmarked this just this change on sv-benchmarks with master and there wasn't a performance difference. |
That's not how marshaling tests do it though. The second run uses |
|
For some reason, there are two paths when the incremental analysis checks if the fixpoint is reached, but only one in the marshalled result. |
|
I've started looking into this myself already. We have quite many |
|
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. |
CHANGES: * Add `setjmp`/`longjmp` analysis (goblint/analyzer#887, goblint/analyzer#970, goblint/analyzer#1015, goblint/analyzer#1019). * Refactor race analysis to lazy distribution (goblint/analyzer#1084, goblint/analyzer#1089, goblint/analyzer#1136, goblint/analyzer#1016). * Add thread-unsafe library function call analysis (goblint/analyzer#723, goblint/analyzer#1082). * Add mutex type analysis and mutex API analysis (goblint/analyzer#800, goblint/analyzer#839, goblint/analyzer#1073). * Add interval set domain and string literals domain (goblint/analyzer#901, goblint/analyzer#966, goblint/analyzer#994, goblint/analyzer#1048). * Add affine equalities analysis (goblint/analyzer#592). * Add use-after-free analysis (goblint/analyzer#1050, goblint/analyzer#1114). * Add dead code elimination transformation (goblint/analyzer#850, goblint/analyzer#979). * Add taint analysis for partial contexts (goblint/analyzer#553, goblint/analyzer#952). * Add YAML witness validation via unassume (goblint/analyzer#796, goblint/analyzer#977, goblint/analyzer#1044, goblint/analyzer#1045, goblint/analyzer#1124). * Add incremental analysis rename detection (goblint/analyzer#774, goblint/analyzer#777). * Fix address sets unsoundness (goblint/analyzer#822, goblint/analyzer#967, goblint/analyzer#564, goblint/analyzer#1032, goblint/analyzer#998, goblint/analyzer#1031). * Fix thread escape analysis unsoundness (goblint/analyzer#939, goblint/analyzer#984, goblint/analyzer#1074, goblint/analyzer#1078). * Fix many incremental analysis issues (goblint/analyzer#627, goblint/analyzer#836, goblint/analyzer#835, goblint/analyzer#841, goblint/analyzer#932, goblint/analyzer#678, goblint/analyzer#942, goblint/analyzer#949, goblint/analyzer#950, goblint/analyzer#957, goblint/analyzer#955, goblint/analyzer#954, goblint/analyzer#960, goblint/analyzer#959, goblint/analyzer#1004, goblint/analyzer#558, goblint/analyzer#1010, goblint/analyzer#1091). * Fix server mode for abstract debugging (goblint/analyzer#983, goblint/analyzer#990, goblint/analyzer#997, goblint/analyzer#1000, goblint/analyzer#1001, goblint/analyzer#1013, goblint/analyzer#1018, goblint/analyzer#1017, goblint/analyzer#1026, goblint/analyzer#1027). * Add documentation for configuration JSON schema and OCaml API (goblint/analyzer#999, goblint/analyzer#1054, goblint/analyzer#1055, goblint/analyzer#1053). * Add many library function specifications (goblint/analyzer#962, goblint/analyzer#996, goblint/analyzer#1028, goblint/analyzer#1079, goblint/analyzer#1121, goblint/analyzer#1135, goblint/analyzer#1138). * Add OCaml 5.0 support (goblint/analyzer#1003, goblint/analyzer#945, goblint/analyzer#1162).
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:
longjmpcall(deemed out of scope)setjmpin invalid place (not directly used for branching)sigsetjmpCloses #887