Interval sets are unsound due to larger-than-type ranges

[sim642]

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):

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

With some additional tracing and CIL warnings, it becomes clear that interval sets are at fault:

%%% priv: (:-1)  invariant_global unprotected:cur
  %%% priv: getg unprotected:cur -> (Unknown int([-31,31]),[0,2147483647],not {} ([-31,31]),ℤ,[[-4294967296, 4294967296]])
  %%% priv: interval invariant [-4294967296,4294967296]
lib/libc/stub/src/stdlib.c:38: Warning: Truncating integer 4294967296 to 0
  %%% priv: -> exp:0 <= cur && cur <= 0
  %%% priv: interval invariant [0,2147483647]
  %%% priv: -> exp:0 <= cur
  %%% priv: -> exp:0 <= cur && (0 <= cur && cur <= 0)

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 into Cil.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).

[karoliineh]

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:

analyzer/src/cdomain/value/cdomains/intDomain.ml

Lines 1397 to 1401 in ede09b8

	let upper_threshold (_,u) =
	let ts = if GobConfig.get_string "ana.int.interval_threshold_widening_constants" = "comparisons" then WideningThresholds.upper_thresholds () else ResettableLazy.force widening_thresholds in
	let u = Ints_t.to_bigint u in
	let t = List.find_opt (fun x -> Z.compare u x <= 0) ts in
	BatOption.map_default Ints_t.of_bigint max_ik t

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.

[sim642]

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.