Autotuner only enables relational analysis for at most 2 globals

[sim642]

While checking https://github.com/goblint/analyzer/pull/1821#issuecomment-3342492386, I found out the following surprising thing: the autotuner only enables relational analysis for at most 2 globals: https://github.com/goblint/analyzer/blob/529013137ad4de9d020b47dcfc7a553d1e677766/src/autoTune.ml#L435-L447

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.