Unsound address set must-not-equality check in base

[sim642]

The use of AD.meet to check address set must-not-equality:

analyzer/src/analyses/base.ml

Lines 331 to 334 in 3a189a9

	| Eq ->
	`Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.zero else match eq p1 p2 with Some x when x -> ID.of_int ik BI.one | _ -> bool_top ik)
	| Ne ->
	`Int (if AD.is_bot (AD.meet p1 p2) then ID.of_int ik BI.one else match eq p1 p2 with Some x when x -> ID.of_int ik BI.zero | _ -> bool_top ik)

is unsound in at least the following cases:

• First struct field and zero index:

  analyzer/tests/regression/02-base/91-ad-meet.c

  Lines 6 to 16 in 3a189a9

  	struct s {
  	int fst;
  	};
  	int main() {
  	struct s a;
  	void *p = &a.fst;
  	void *q = ((int(*)[1]) (&a))[0];
  	assert(p == q);
  	return 0;
  	}

• Union fields:

  analyzer/tests/regression/02-base/92-ad-union-fields.c

  Lines 6 to 17 in 3a189a9

  	union u {
  	int fst;
  	float snd;
  	};
  	int main() {
  	union u a;
  	void *p = &a.fst;
  	void *q = &a.snd;
  	assert(p == q);
  	return 0;
  	}

• Non-first struct field and non-zero index with alignment: Unsound address set must-not-equality check in base #822 (comment).

For both programs we report that the assert definitely fails, but when compiled and run, it succeeds.

Using meet would only work if addresses were represented in their canonical form using a byte offset from the variable.

[jerhard]

The unsoundness of comparing addresses with a struct field and an index as offsets is also exhibited for non-zero offsets:

analyzer/tests/regression/02-base/93-ad-struct-offset.c

Lines 9 to 27 in 712c6ce

	struct str a;
	char* ca = (char*) &a;
	void *ptr = &ca[4];
	void *ptr2 = &a.c;
	int z = 1;
	// Alginment of struct fields, and thus result of the equality check here is implementation defined.
	if(ptr == ptr2){
	z = 1;
	} else {
	z = 2;
	}
	// Aaccording to the C standard (section 6.2.8 in the C11 standard),
	// the alignment of fields in structs is implementation defined.
	// When compiling with GCC, the following check as an assert happens to hold.
	__goblint_check(z==1); //UNKNOWN!

The alignment of fields within objects is implementation defined, thus one generally cannot produce definite answers when comparing integer offsets with field offsets on structs.

[sim642]

Since #809 makes this problem even more urgent, we probably need a quicker fix than completely refactoring lvalue representations to carry a canonical form or whatnot. A simpler implementation for just AD.may_equal a1 a2 would be to pairwise check all lvalues from a1 and a2, and check their may equality. That could be implemented by calculating the canonical offset numerically, a la Cil.bitsOffset and checking those integers for may equality. The only problem is that Cil.bitsOffset works only with constant indices, but we'll have abstract ones, so it'll have to be partially reimplemented in Goblint. However, CIL can still provide us with the byte/bit offsets of struct fields (using Machdep), so it shouldn't be too difficult.

[sim642]

A remark from Zulip on optimizing the pairwise may alias checking. Checking all pairs is overly wasteful because addresses may only alias if their varinfos (without offsets) are equal, so it suffices to do pairwise checking within each varinfo.

The projective bucketing from #809 doesn't directly allow that because the ProjectiveSet buckets are per varinfo and representative offset. However, that could be replaced with a two nested ProjectiveSets: outer split by varinfo only and inner split by representative offset in each varinfo. Then may alias checking can be performed pairwise within each outer bucket, but over all the elements in the corresponding inner buckets.
Currently ProjectiveSet completely abstracts away the map structure, so an additional special function (maybe bucket_exists2?) would have to be implemented to do that.