Autotuning of Configuration by manuel-pietsch · Pull Request #772 · goblint/analyzer

manuel-pietsch · 2022-06-30T21:18:38Z

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.

Added scripts for overflow category

sim642

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?

conf/svcomp22.json

goblint.opam

sv-comp/my-bench-sv-comp/goblint-all-fast.sh

src/util/wideningThresholds.mli

src/cdomains/apron/apronDomain.apron.ml

src/AutoSelect.ml

manuel-pietsch · 2022-07-01T15:24:54Z

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

Active if the loop uses malloc/threads/locks Moved the creation of the CFG to seperate file to break dependency cycle

Comment cleanup

fixed handling of __builtin functions when setting congruence attributes

…n count

rename to autotune find malloc wrappers

by variable, type attributes Small fixes to loopheuristic

loop unrolling now seperately activateable over ana.autotune.activated

small fixes annotationg variables for tracking with apron choosing options annotate arrays

…stimate

sim642

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

src/analyses/apron/apronAnalysis.apron.ml

src/cdomains/apron/apronDomain.apron.ml

tests/regression/58-array_annotations/01-var_array_annotation.c

tests/regression/58-array_annotations/03-change_domain_array_annotation.c

src/util/options.schema.json

src/analyses/base.ml

src/autoTune.ml

src/util/cilfacade.ml

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>

manuel-pietsch · 2022-09-19T23:34:38Z

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.

Changes for pull request

docs/user-guide/annotating.md

src/analyses/base.ml

sim642 · 2022-09-23T07:26:36Z

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 · 2022-10-07T14:34:05Z

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

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).

manuel-pietsch added 4 commits June 22, 2022 12:43

autoselect beginning, new wideningThresholds

543b954

Merge branch 'master' of https://github.com/leunam99/analyzer

9718bfe

Added Analysis Focus

dea75d7

Added scripts for overflow category

Use LibraryFunction for detecting ThreadCreation

9b39f58

sim642 self-requested a review July 1, 2022 05:05

sim642 added feature student-job sv-comp SV-COMP (analyses, results), witnesses precision performance Analysis time, memory usage labels Jul 1, 2022

sim642 added this to the SV-COMP 2023 milestone Jul 1, 2022

sim642 reviewed Jul 1, 2022

View reviewed changes

manuel-pietsch added 2 commits July 1, 2022 16:32

revert personal changes

011cd17

Suggested Changes for Pull request

1c41250

manuel-pietsch added 6 commits July 11, 2022 13:58

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

Enum detection

508efb9

Comment cleanup

Added Collection of factors to predict complexity

60e58d4

fixed handling of __builtin functions when setting congruence attributes

New loop unrolling heuristic: detect dimple loops with fixed iteratio…

b9112e4

…n count

Enable different tuning options

5576e21

rename to autotune find malloc wrappers

Array domain can individually be configured

bab6914

by variable, type attributes Small fixes to loopheuristic

sim642 mentioned this pull request Jul 27, 2022

Malloc uniqueness #722

Merged

manuel-pietsch added 8 commits July 28, 2022 23:42

support for choosing options based on estimates

9b95b6c

Indentation fixes, uncomment loopunrolling

5c91440

loop unrolling now seperately activateable over ana.autotune.activated

project arrays to different domains when calling functions

fbef34b

activate loopunrolling correctly

ac1097b

array domain can actually project arguments

050225d

Changed options

c926829

small fixes annotationg variables for tracking with apron choosing options annotate arrays

regression tests, small fixes

d775b43

changed widening thresholds because of logic error, different apron e…

8b2bd2c

…stimate

michael-schwarz added 4 commits September 19, 2022 14:27

Fix names

3b7b825

Cleanup wideningThresholds.ml

c6cc2dd

Typos in options scheme

627c982

Minimize changes to array domain

c102005

michael-schwarz approved these changes Sep 19, 2022

View reviewed changes

michael-schwarz requested a review from sim642 September 19, 2022 13:13

sim642 requested changes Sep 19, 2022

View reviewed changes

Cleanup indentation

5ad7a14

Co-authored-by: Simmo Saan <simmo.saan@gmail.com>

manuel-pietsch added 3 commits September 22, 2022 11:13

Changed attribute option names

ff6662b

Moved loop unrolling to it's own file

fbd888c

Changes for pull request

Dokumentaton

aeee3d8

michael-schwarz reviewed Sep 22, 2022

View reviewed changes

docs/user-guide/annotating.md Outdated Show resolved Hide resolved

michael-schwarz reviewed Sep 22, 2022

View reviewed changes

docs/user-guide/annotating.md Outdated Show resolved Hide resolved

michael-schwarz reviewed Sep 22, 2022

View reviewed changes

src/analyses/base.ml Outdated Show resolved Hide resolved

michael-schwarz requested a review from sim642 September 22, 2022 14:10

manuel-pietsch and others added 4 commits September 24, 2022 01:11

More small fixes

07d1aff

Merge branch 'master' into autotune

423631c

Merge branch 'master' of github.com:leunam99/analyzer into autotune

e247378

Remove polymorphic hash table

b6b7cde

sim642 approved these changes Oct 10, 2022

View reviewed changes

michael-schwarz merged commit 9f677d7 into goblint:master Oct 10, 2022

sim642 added a commit that referenced this pull request Oct 10, 2022

Fix autotune indentation (PR #772)

f91c892

sim642 added a commit that referenced this pull request Oct 11, 2022

Fix autotune compilation on OCaml < 4.13 (PR #772)

7f84b27

sim642 added a commit that referenced this pull request Oct 11, 2022

Fix autotune compilation on OCaml < 4.12 (PR #772)

b4c0057

michael-schwarz mentioned this pull request Nov 1, 2022

Limit unrolling to specific loops and arrays to make it applicable to larger programs #643

Closed

3 tasks

sim642 mentioned this pull request Nov 25, 2022

[new release] goblint (2.1.0) ocaml/opam-repository#22565

Merged

Conversation

manuel-pietsch commented Jun 30, 2022

Uh oh!

sim642 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

manuel-pietsch commented Jul 1, 2022

Uh oh!

sim642 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

manuel-pietsch commented Sep 19, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sim642 commented Sep 23, 2022

Uh oh!

michael-schwarz commented Oct 7, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

manuel-pietsch commented Sep 19, 2022 •

edited

Loading