search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
185 stars 75 forks source link

SV-COMP autotuner spuriously enables all integer domains #1472

Open sim642 opened 6 months ago

sim642 commented 6 months ago

In c/pthread/fib_safe-5.i from #1356, we produce an unsound invariant. Opening the HTML view to see globals reveals that they somehow have all integer domains enabled:

base:priv:unprotected:cur → def_exc:Unknown int([-31,31]); intervals:[0,2147483647]; enums:not {} ([-31,31]); congruences:ℤ; interval_sets:[[-4294967296, 4294967296]]

The autotuner only claims to enable the following:

[Info] Enabled congruence domain.
[Info] Enabled widening thresholds

I'm not even sure how it does because the autotuner has no means for enabling interval sets even... Something is going royally wrong. Disabling congruence and widening threshold autotuners does prevent this from happening though.

This might have massive performance implications for us in SV-COMP if actually we're using all integer domains a lot of the time without even realizing. It only revealed itself now because interval sets produce unsound invariant expressions to the output (#1473). No idea how long this has even been happening.

michael-schwarz commented 6 months ago

Iirc when using selective int precision, we enable all int domains for globals. So this behaves as intended - but maybe it's not the smartest default.

michael-schwarz commented 6 months ago

https://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/analyses/base.ml#L1610-L1612

michael-schwarz commented 6 months ago

https://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/analyses/base.ml#L128-L136

sim642 commented 6 months ago

This doesn't seem intentional to me: https://github.com/goblint/analyzer/blob/bffc5e3cbb1f43bd5c9483a6545802cfba5d3d76/src/autoTune.ml#L139-L142 The autotuner is only enabling this annotation option which again has very surprising implications that are not documented anywhere:

Enable manual annotation of functions with desired precision, i.e., the activated IntDomains.

Moreover, the autotuner only does it to annotate some modulo operations with these annotations. But then it accidentally changes all the global int domains. That's part of "congruence" autotuner...

michael-schwarz commented 6 months ago

I remember discussing this with @jerhard and his student at the time: The idea is that if additional int domains are used inside some functions (via annotations), globals should also use them so precision we have there is not lost spuriously. I think this was probably introduced before we had interval sets.

It's also interesting in light of #1454 that this even does anything meaningful here.