Fix address set meet

[jerhard]

The meet of addresses is currently unsound when different integer domains may be activated within an analysis run. This is demonstrated by this example. Here, the abstract representation of the address pointed to by slotvec0.val contains an offset where all int domains are active, as all int domains are activated for global variables with the annotation.int.enabled setting. At the point of the comparison however, only def_exc is active. Therefore the abstract addresses are kept in different buckets and the meet that is performed yields bottom.

This issue also appears on sv-comp when the congruence auto-tuning is enabled, and for some functions the congruence domain is activated, and for others not.

This PR fixes this issue by not keeping the index information in the representative that is used to split address sets.

(Closes #925)

[michael-schwarz]

I'll start a run of this together with #911.

[sim642]

This PR fixes this issue by not keeping the index information in the representative that is used to split address sets.

But that is already the case:

analyzer/src/cdomains/lval.ml

Lines 389 to 399 in 00bfa7f

	(** Representatives for lvalue sublattices as defined by {!NormalLat}. *)
	module R: DisjointDomain.Representative with type elt = t =
	struct
	include Normal (Idx)
	type elt = t
	let rec of_elt_offset: Offs.t -> Offs.t =
	function
	| `NoOffset -> `NoOffset
	| `Field (f,o) -> `Field (f, of_elt_offset o)
	| `Index (_,o) -> `Index (Idx.top (), of_elt_offset o) (* all indices to same bucket *)

Isn't this just another instance of #822?

[michael-schwarz]

The issue is Idx.top () that depends on the activated int domains.
In the example the two address values for which the meet is \bot are identical except for the number of activated int domains.

[sim642]

The issue is Idx.top () that depends on the activated int domains.

That seems like a problem in itself because it's supposed to be a real top, not top_of. Having multiple incomparable "tops" defies the definition of top.

Also, this is the index domain, which is a separate thing from the intdomain that's actually used for integer values.

In the example the two address values for which the meet is \bot are identical except for the number of activated int domains.

It still seems to me that something deeper is wrong here that such situation can arise at all. Aren't the intdomain projections that are used for converting integer abstractions between different precisions supposed to ensure that we don't have such mixture?
There might be a projection missing somewhere. If it's a problem here, it's a problem elsewhere as well because AFAIK our intdomain operations aren't meant to be used between tuples with different precisions. The fact that such mismatches arise at all is the bug.
If integers with mismatching precisions coexist, then other operations on them could break precisely in the same way.

[jerhard]

@michael-schwarz started a run with a version of this PR, so I would suggest that if the results for that run are well, we merge this hot-fix PR for the sv-comp version. We would implement a follow-up PR that addresses your remark, @sim642, to be merged after submission for sv-comp.