Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Autotuning of Configuration #772

Merged
merged 44 commits into from
Oct 10, 2022
Merged

Autotuning of Configuration #772

merged 44 commits into from
Oct 10, 2022

Conversation

leunam99
Copy link
Contributor

Adds an option that tries choosing some configurations automatically based on the file that is analyzed.
Already implemented:

  • Enable Congruence domain only in functions that use modulo and related ones
  • new widening thresholds
  • focus analysis depending on sv-comp specification
  • disable thread analyses if program is single threaded
  • disable interval contexts in recursive functions
    This is part of my bachelor thesis and still work in progress.

@sim642 sim642 self-requested a review July 1, 2022 05:05
@sim642 sim642 added feature student-job sv-comp SV-COMP (analyses, results), witnesses precision performance Analysis time, memory usage labels Jul 1, 2022
@sim642 sim642 added this to the SV-COMP 2023 milestone Jul 1, 2022
sim642
sim642 reviewed Jul 1, 2022
View reviewed changes
Copy link
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

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

Thanks for the contribution!
Given that you've touched the SV-COMP files here already, I suppose you've already tried this on sv-benchmarks? If so, then does this already show some improvement there?

@leunam99
Copy link
Contributor Author

leunam99 commented Jul 1, 2022

I am testing with the sv-comp tests and there are some improvements.
For example, in the NoOverflow category Goblint is correct 104 instead of 81 times and uses a bit less time and memory (on my machine at least)
In the other categories there are also improvements, but I currently don't know the numbers

leunam99 added 6 commits July 11, 2022 13:58
@leunam99
Added selective loop unrolling
71e65ca 
Active if the loop uses malloc/threads/locks
Moved the creation of the CFG to seperate file to break dependency cycle
@leunam99
Enum detection
508efb9 
Comment cleanup
@leunam99
Added Collection of factors to predict complexity
60e58d4 
fixed handling of __builtin functions when setting congruence attributes
@leunam99
New loop unrolling heuristic: detect dimple loops with fixed iteratio…
b9112e4 
…n count
@leunam99
Enable different tuning options
5576e21 
rename to autotune
find malloc wrappers
@leunam99
Array domain can individually be configured
bab6914 
by variable, type attributes
Small fixes to loopheuristic
@sim642 sim642 mentioned this pull request Jul 27, 2022
Merged
sim642
sim642 requested changes Sep 19, 2022
View reviewed changes
Copy link
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

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

It would be good to have complete SV-COMP before vs after runs with this to see how well this ad-hoc stuff works.

@michael-schwarz @sim642
Cleanup indentation
5ad7a14 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@leunam99
Copy link
Contributor Author

leunam99 commented Sep 19, 2022 •
edited
Loading

It would be good to have complete SV-COMP before vs after runs with this to see how well this ad-hoc stuff works.

I did this in my bachelor's thesis: pages 19 and 20 contain tables with the results of the different features and some further configurations. In the text surrounding it I describe a bit further what changed.

@sim642
Copy link
Member

sim642 commented Sep 23, 2022

Besides the couple of unresolved comments, the test group 58-array_annotations needs to be renumbered to 60-array_annotations to avoid conflict on master.

@michael-schwarz
Copy link
Member

@sim642 Any more comments here or are we good to merge?

@michael-schwarz michael-schwarz merged commit 9f677d7 into goblint:master Oct 10, 2022
sim642 added a commit that referenced this pull request Oct 10, 2022
@sim642
Fix autotune indentation (PR #772)
f91c892
sim642 added a commit that referenced this pull request Oct 11, 2022
@sim642
Fix autotune compilation on OCaml < 4.13 (PR #772)
7f84b27
sim642 added a commit that referenced this pull request Oct 11, 2022
@sim642
Fix autotune compilation on OCaml < 4.12 (PR #772)
b4c0057
@michael-schwarz michael-schwarz mentioned this pull request Nov 1, 2022
Closed
3 tasks
@sim642 sim642 mentioned this pull request Nov 25, 2022
Merged
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 25, 2022
@sim642
[new release] goblint (2.1.0)
93889f4 
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2023.

* Add automatic configuration tuning (goblint/analyzer#772).
* Add many library function specifications (goblint/analyzer#865, goblint/analyzer#868, goblint/analyzer#878, goblint/analyzer#884, goblint/analyzer#886).
* Reorganize library stubs (goblint/analyzer#814, goblint/analyzer#845).
* Add Trace Event Format output to timing (goblint/analyzer#844).
* Optimize domains for address and path sets (goblint/analyzer#803, goblint/analyzer#809).
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 approved these changes

@sim642 sim642 sim642 approved these changes

Assignees
No one assigned
Labels
feature performance Analysis time, memory usage precision student-job sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Milestone
SV-COMP 2023
Development

Successfully merging this pull request may close these issues.
3 participants
@leunam99 @sim642 @michael-schwarz