Make meet in AddressDomain more precise

[michael-schwarz]

Currently, in the address domain inside the buckets, for the meets we use ProjectiveSetPairwiseMeet

analyzer/src/domain/disjointDomain.ml

Lines 190 to 205 in bffc5e3

	let meet m1 m2 =
	let meet_buckets b1 b2 acc =
	B.fold (fun e1 acc ->
	B.fold (fun e2 acc ->
	if B.may_be_equal e1 e2 then
	add e1 (add e2 acc)
	else
	acc
	) b2 acc
	) b1 acc
	in
	fold_buckets (fun _ b1 acc ->
	fold_buckets (fun _ b2 acc ->
	meet_buckets b1 b2 acc
	) m2 acc
	) m1 (empty ())

where B.may_be_equal delegates to

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

Line 180 in bffc5e3

let may_be_equal a b = Option.value (Addr.semantic_equal a b) ~default:true

Addr.semantic_equal given by

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

Lines 102 to 111 in bffc5e3

	let semantic_equal x y = match x, y with
	| Addr x, Addr y -> Mval.semantic_equal x y
	| StrPtr s1, StrPtr s2 -> SD.semantic_equal s1 s2
	| NullPtr, NullPtr -> Some true
	| UnknownPtr, UnknownPtr
	| UnknownPtr, Addr _
	| Addr _, UnknownPtr
	| UnknownPtr, StrPtr _
	| StrPtr _, UnknownPtr -> None
	| _, _ -> Some false

which calls SD.sematic_equal

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

Lines 77 to 81 in bffc5e3

	let semantic_equal x y =
	match x, y with
	| None, _
	| _, None -> Some true
	| Some a, Some b -> if a = b then None else Some false

this is needed to handle all sorts of different offsets that may be semantically equal, i.e., evaluate to the same physical address. In this case it keeps both elements.

After some discussion with @jerhard and @hseidl, we reached the following insights:

This behavior is overly conservative, as the mess of the address lattice contains some sub-lattices where the meet operation is semantically correct.

This now checks via a new predicate amenable_to_meet whether for the two addresses a and b this relationship between values and the meet holds. If this is the case, a meet is performed and the element added to the resulting set only if it is distinct from bot.

Currently, we answer amenable_to_meetby true whenever both arguments are strings, or when the both are addresses that differ in the numeric(!) offsets only.

This PR also adds two tests where this yields additional precision.

Closes #1467

[sim642]

Don't the address set buckets already guarantee this to only be called in such cases because Mval.top_indices are the representatives?

[michael-schwarz]

Even if the buckets guarantee this already, this function can be called with two arbitrary addresses, so we can not just return true.

[sim642]

That's true, although it could just be an implementation detail (like the buckets themselves are), which isn't exposed to the outside by the interface. Then such misuse would be impossible.

[michael-schwarz]

I followed this assumption now to just assume that things placed into the same bucket are amenable to meet, which seems to be the case in our implementation and I think also makes sense semantically.

This largely simplifies the implementation and makes all sorts of extra considerations obsolete.

[michael-schwarz]

Sorry for being MIA, I will take this up and hopefully get it mergeable before the holidays.