Interactive analysis

[sim642]

This draft PR serves as a place to list the changes on the interactive branch, which have been combined there for better experimentation.

Changes

1. Incremental TD3: restart destabilized side-effected variables #363
2. (Incremental) TD3: restart detected wpoints #366
3. Incremental postsolve in TD3 #372
4. Refactor race warnings (accesses) to use global invariant #397
5. TD3: optimize destabilization by aborting transfer function when unchanged #364 Reverted, because not used for interactive paper and modifies TD3 too much.
6. Use nodes for messages instead of locations #533
7. Use global invariant for dead branch detection #525
8. Collect constraint unknown sets in global invariant, use them for TD3 incremental load #549
9. Add option for manual restarting of globals #573
10. Incremental analysis: Eagerly analyze functions in force-reanalyze, even when reluctant is on #600
11. Fix unnecessary initial double parsing in server mode with reparse #625
12. Incremental TD3: optimize write-only unknown restarting #634
13. Exclude functions with changed header from reluctant destabilization #663
14. Fix incremental warnings with reluctant destabilization #709
15. Incremental: (Cheap!) Full Reachability to Prune  #713
16. Minimal write-only restarting is insufficient: add ana.malloc.include-node #647 (parts cherry-picked)
17. Interactive: fix expression locations #717
18. Option to only destabilize access globals (instead of following all side-effects) after re-setting them to bottom #721
19. Rename incremental.reluctant.on → incremental.reluctant.enabled for consistency.
20. Interactive: improvements for chrony story #724
21. Interactive: improvements for smtprc story #729
22. Incremental TD3: limit side-effected restarting using fuel #629
23. Add server command pre_files #740

TODO

• Hack incremental accesses to only restart during postsolving #633
• Revert Option to only destabilize access globals (instead of following all side-effects) after re-setting them to bottom #721, which was just done to allow some benchmarking? If kept, at least address TODOs from there.
• Reorder tests to keep order from master and have all interactive tests come after. Currently they've all been chaotically renamed when tests with same numbers have been added on both branches simultaneously while trying to fix duplicate ID errors.
• Rename solver and do git merge trick to preserve both histories? Just merge.
• Benchmark before vs after on SQLite.

[sim642]

For good measure, I did a sv-benchmarks comparison run with this entire PR: results. Luckily all these additions to the solver and analyses to track extra information (which we theoretically could disable for batch analysis if we're careful) don't come with a notable penalty. Most of the comparison plot is just noise around the ECA tasks.

[jerhard]

Looks good!

I only had some remarks about some test files.

[jerhard]

I let goblint in the current master and the interactive version run on sqlite.

Goblint Command line

./goblint ../../benchmarks/sqlite-amalgamation-3370200/sqlite3.c ../../benchmarks/sqlite-amalgamation-3370200/sqlite3.h ../../benchmarks/sqlite-amalga
mation-3370200/sqlite3ext.h ../../benchmarks/sqlite-amalgamation-3370200/shell.c -v --set pre.cppflags[+] -DSQLITE_DEBUG --disable ana.base.context.non-ptr --disable ana.int.def_exc --disable sem.unknown_functio
n.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --s
et ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper

The runtime of the master version was 444 minutes, compared to the interactive version with a runtime of 461 minutes. The interactive version is thus 3,8% slower on this benchmark. I think that this is should not be a blocker from merging it.

[sim642]

@michael-schwarz Do you also wish to go over this monster PR once more or can I pull the trigger?

[michael-schwarz]

No, I think it's fine! Feel free to merge!