Autotuner only enables relational analysis for at most 2 globals

[sim642]

While checking #1821 (comment), I found out the following surprising thing: the autotuner only enables relational analysis for at most 2 globals:

analyzer/src/autoTune.ml

Lines 435 to 447 in 5290131

	in let globals = 2 in
	let selectedLocals =
	let list = ref [] in
	let visitor = new octagonFunctionVisitor(list, locals) in
	visitCilFileSameGlobals visitor file;
	List.concat !list
	in
	let selectedGlobals =
	let varMap = ref VariableMap.empty in
	let visitor = new octagonVariableVisitor(varMap, true) in
	visitCilFileSameGlobals visitor file;
	topVars globals !varMap
	in

We should really look into this because we could be shooting ourselves in the foot with such a low limit. SV-COMP benchmarks often use global variables for no good reason (over locals) because code quality doesn't matter.
This also makes relational Mutex-Meet mostly useless.

[michael-schwarz]

Wow, that's an incredible find!

[sim642]

I tried just hard-coding it to 100 to see what happens, but just doing that loses points. It seems that by allowing more globals to be picked, the cost in autotuner goes up and the autotuner doesn't activate relational analysis at all.
So improving our results requires more careful tuning.

[michael-schwarz]

Might be worth to do a run where it's always on for globals and those are free? Then we see if it makes sense before investing effort into tuning.

[sim642]

Yeah, that's a good idea. I now did that and the diff table is here: https://goblint.cs.ut.ee/results/275-all-autotune-globals-100-2/table-generator-cmp.diff.html#/. The summary is:

1. 13 trues turned into TIMEOUT/OUT OF MEMORY: some LDV ones and some pthread-wmm ones.
2. 118 unknowns turned into true: many of them are eca-rers2012, hardness-nfm22 and product-lines, but surprisingly a couple of goblint-regression ones as well!

So there is something to gain!

Randomly looking into one, we also seem to do some weird things because the list includes (even builtin) function names:

[Info] Enabled octagon domain ONLY for:
[Info] pthread_mutex_lock, pthread_mutex_unlock, __VERIFIER_assert, pthread_create, g, h, abort, __assert_fail, reach_error, [...]

I don't think the attribute does anything on functions: the autotuner specifically looks for locals inside functions to annotate.
I'll try a small fix to filter functions because it might also be hurting us to pick a function over an actual global.

[karoliineh]

Looking into this now, some of these benchmarks have been removed from SV-COMP, but for the ones remaining:

1. 13 trues turned into TIMEOUT/OUT OF MEMORY: some LDV ones and some pthread-wmm ones.

All of these are solved by the level 00 conf that does not even have octagon autotune turned on.

2. 118 unknowns turned into true: many of them are eca-rers2012, hardness-nfm22 and product-lines, but surprisingly a couple of goblint-regression ones as well!

hardness-nfm22 tasks are not there anymore, but most (if not all) of the eca-rers2012 and product-lines tasks are now solved by level 02 conf (level 01 turns on octagon autotune, whereas 02 does not, but turns on apron analysis).

Thus, figuring out a good bound for the globals needs new experiments and a new assessment.