Autotuning of Configuration: First Steps

[leunam99]

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.

[leunam99]

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]

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]

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]

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