Closed sim642 closed 4 months ago
Debugging this revealed that the autotuning option octagon
was manually switched off in the command used to generate the incorrect witness. By removing --set 'ana.autotune.activated[-]' octagon
, the interval seems to be correctly calculated (interval_sets:[[-2147483648, 2147483647]]
).
In the svcomp-ghost.json
, the ana.autotune.wideningThresholds
is still activated, making autotune set option ana.int.interval_threshold_widening_constants
to comparisons
, which is then used in intDomain.IntervalSetFunctior.widen
:
where the list ts
gets the value [-281474976710656 -4294967296; -65536; -256; -16; -4; -1; 0; 1; 4; 12; 16; 256; 65536; 4294967296; 281474976710656]
I am not entirely sure what this WideningThresholds.upper_thresholds
does, but in conditional_widening_thresholds
there is a variable called octagon
, so I guess that either in the autotune, wideningOption
assumes that octagon
should also be activated and thus this should be enforced, or the implementation of WideningThresholds.upper_thresholds
is flawed.
Looks like interval set widening up to the next threshold (above 65536) chooses 4294967296, but it should not go higher than max_ik
(2147483647 in this case). The map_default
only uses max_ik
if no upper threshold could be found.
The condition for find_opt
should maybe be Z.compare u x <= 0 && Z.compare x max_ik <= 0
to prevent it from going over. Non-set intervals use very similar logic and somehow avoid this problem, so it's worth looking to see how it does that. And maybe interval sets should just delegate to intervals at this point.
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 (#1472):With some additional tracing and CIL warnings, it becomes clear that interval sets are at fault:
Namely, interval sets somehow have an interval which is larger than the corresponding type. This itself breaks many internal assumptions.
The internal inconsistency is only revealed via witnesses, where conversion of
Z.t
intoCil.exp
goes through some CIL functions that truncate to type. Because the interval is bigger than the type, it gets bit-truncated to 0 (because all 32 bits are zero).