Skip to content

Interactive analysis#391

Merged
sim642 merged 500 commits intomasterfrom
interactive
Aug 12, 2022
Merged

Interactive analysis#391
sim642 merged 500 commits intomasterfrom
interactive

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Oct 13, 2021 •
edited
Loading

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

@sim642 sim642 mentioned this pull request Oct 13, 2021
Closed
@sim642 sim642 mentioned this pull request Dec 1, 2021
Merged
4 tasks
@sim642 sim642 added this to the v2.0.0 milestone Dec 2, 2021
@sim642 sim642 mentioned this pull request Dec 8, 2021
Merged
2 tasks
@sim642 sim642 mentioned this pull request Jan 6, 2022
Merged
@michael-schwarz michael-schwarz mentioned this pull request Jan 6, 2022
Merged
This was referenced Jan 7, 2022
Closed
Merged
michael-schwarz
michael-schwarz reviewed Jan 18, 2022
View reviewed changes
michael-schwarz
michael-schwarz reviewed Jan 18, 2022
View reviewed changes
michael-schwarz
michael-schwarz reviewed Jan 18, 2022
View reviewed changes
michael-schwarz
michael-schwarz reviewed Jan 18, 2022
View reviewed changes
michael-schwarz
michael-schwarz reviewed Jan 18, 2022
View reviewed changes
michael-schwarz
michael-schwarz reviewed Jan 18, 2022
View reviewed changes
michael-schwarz
michael-schwarz reviewed Jan 18, 2022
View reviewed changes
michael-schwarz
michael-schwarz reviewed Jan 18, 2022
View reviewed changes
This was referenced Jan 19, 2022
Open
Merged
sim642 and others added 8 commits January 26, 2022 15:05
@sim642 sim642 self-assigned this Aug 3, 2022
@sim642 sim642 mentioned this pull request Aug 4, 2022
Closed
sim642 added 2 commits August 4, 2022 12:46
@sim642
Remove broken incremental.restart.sided.destab-with-sides option
7aa89e9 
#703 (comment)
@sim642
Add option incremental.restart.sided.vars
4ec572b 
This simplifies the should_restart logic and makes the combination of both "only" options unrepresentable.
@sim642 sim642 marked this pull request as ready for review August 4, 2022 11:18
@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Aug 5, 2022

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
jerhard reviewed Aug 9, 2022
View reviewed changes
Copy link
Copy Markdown
Member

@jerhard jerhard left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good!

I only had some remarks about some test files.

@jerhard
Copy link
Copy Markdown
Member

jerhard commented Aug 11, 2022

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
Copy link
Copy Markdown
Member Author

sim642 commented Aug 11, 2022

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

@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Aug 11, 2022

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

@sim642 sim642 merged commit fa83790 into master Aug 12, 2022
sim642 added a commit that referenced this pull request Aug 12, 2022
@sim642
Fix interactive indentation (PR #391)
e3ebbdf
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
@sim642
[new release] goblint (2.0.0)
6efdfdf 
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
@sim642 sim642 mentioned this pull request Aug 18, 2022
Merged
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 18, 2022
@sim642
[new release] goblint (2.0.0)
1c281d5 
CHANGES:

Goblint "lean" release after a lot of cleanup.

* Remove unmaintained analyses: OSEK, ARINC, shapes, containment, deadlocksByRaces (goblint/analyzer#460, goblint/analyzer#736, goblint/analyzer#812, goblint/analyzer#474).
* Add interactive analysis (goblint/analyzer#391).
* Add server mode (goblint/analyzer#522).
* Add Compilation Database support (goblint/analyzer#406, goblint/analyzer#448).
* Add floating point domain, unrolled array domain and improved struct domains (goblint/analyzer#734, goblint/analyzer#761, goblint/analyzer#577, goblint/analyzer#419).
* Add static loop unrolling and heap variable unrolling (goblint/analyzer#563, goblint/analyzer#722).
* Improve race detection with may-happen-in-parallel analysis (goblint/analyzer#529, goblint/analyzer#518, goblint/analyzer#595).
* Reimplement lockset and deadlock analyses (goblint/analyzer#659, goblint/analyzer#662, goblint/analyzer#650, goblint/analyzer#655).
* Add pthread extraction to Promela (goblint/analyzer#220).
* Add location spans to output (goblint/analyzer#428, goblint/analyzer#449).
* Improve race reporting (goblint/analyzer#550, goblint/analyzer#551).
* Improve dead code reporting (goblint/analyzer#94, goblint/analyzer#353, goblint/analyzer#785).
* Refactor warnings (goblint/analyzer#55, goblint/analyzer#783).
* Add JSON schema for configuration (goblint/analyzer#476, goblint/analyzer#499).
* Refactor option names (goblint/analyzer#28, goblint/analyzer#192, goblint/analyzer#516, goblint/analyzer#675).
* Add bash completion (goblint/analyzer#669).
* Add OCaml 4.13 and 4.14 support, remove OCaml 4.09 support (goblint/analyzer#503, goblint/analyzer#672).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@michael-schwarz michael-schwarz michael-schwarz left review comments

@jerhard jerhard jerhard approved these changes

Assignees

@sim642 sim642

Labels

feature in progress performance Analysis time, memory usage precision

Projects

None yet

Milestone

v2.0.0

Development

Successfully merging this pull request may close these issues.

5 participants

@sim642 @jerhard @michael-schwarz @vesalvojdani @stilscher