SV-COMP autotuner spuriously enables all integer domains

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

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]

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]

analyzer/src/analyses/base.ml

Lines 1610 to 1612 in bffc5e3

	let update_offset old_value =
	(* Projection globals to highest Precision *)
	let projected_value = project_val (Queries.to_value_domain_ask ask) None None value (is_global ask x) in

[michael-schwarz]

analyzer/src/analyses/base.ml

Lines 128 to 136 in bffc5e3

	let project_val ask array_attr p_opt value is_glob =
	let p = if GobConfig.get_bool "annotation.int.enabled" then (
	if is_glob then
	Some PU.max_int_precision
	else p_opt
	) else None
	in
	let a = if GobConfig.get_bool "annotation.goblint_array_domain" then array_attr else None in
	VD.project ask p a value

[sim642]

This doesn't seem intentional to me:

analyzer/src/autoTune.ml

Lines 139 to 142 in bffc5e3

	let addModAttributes file =
	set_bool "annotation.int.enabled" true;
	let thisVisitor = new modFunctionAnnotatorVisitor in
	ignore (visitCilFileSameGlobals thisVisitor file)

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]

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.