Unsound address set equality with mismatching offsets

[sim642]

Program

Consider the following program:

#include <assert.h>

typedef struct {
  int x;
} a;

int main() {
  a z;
  a *y = &z;

  int *m = &y->x; // {&z.x}
  a *n = &y[0]; // {&z[def_exc:0]}

  int b = m == n;
  assert(b);
  return 0;
}

In concrete the assertion actually holds, but Goblint unsoundly reports FAIL.

Reason

Base analysis implements address set equality as follows:

analyzer/src/analyses/base.ml

Lines 299 to 300 in 0080994

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

AD.meet applies meet to the offsets as follows:

analyzer/src/cdomains/lval.ml

Lines 105 to 116 in 0080994

	let rec merge cop x y =
	let op = match cop with `Join -> Idx.join | `Meet -> Idx.meet | `Widen -> Idx.widen | `Narrow -> Idx.narrow in
	match x, y with
	| `NoOffset, `NoOffset -> `NoOffset
	| `NoOffset, x
	| x, `NoOffset -> (match cop, cmp_zero_offset x with
	| (`Join | `Widen), (`MustZero | `MayZero) -> x
	| (`Meet | `Narrow), (`MustZero | `MayZero) -> `NoOffset
	| _ -> raise Lattice.Uncomparable)
	| `Field (x1,y1), `Field (x2,y2) when CilType.Fieldinfo.equal x1 x2 -> `Field (x1, merge cop y1 y2)
	| `Index (x1,y1), `Index (x2,y2) -> `Index (op x1 x2, merge cop y1 y2)
	| _ -> raise Lattice.Uncomparable

Since one is Field and the other Index, it raises Uncomparable, which in HoarePO results in an empty address set. Hence base analysis considers the address sets disjoint, concludes that they cannot equal and returns 0.

Problem

Our operations on mismatching offset constructors are sketchy and the behavior isn't well-defined, as already pointed out in #559. There's some special logic for equating no offset with [0] and the first field, but there are also inconsistencies in this handling. Moreover, the logic for this is already quite involved, as seen from the above snippet.

Even if the zero index and first field handling worked perfectly, there are still cases where there's no obvious answer. For example, what should be the meet of [5] and .g (not first field)? It should not be Uncomparable or empty, because that leads to the unsound address sets. To be sound, it should be something because we don't know for sure that they cannot alias. But it also cannot be an unknown offset (index), because that would be their join. So join and meet would be equal, which is nonsense.

[jerhard]

As discussed at GobCon, we would like to fix this issue by modifying the implementation of the address set as follows:

• do not split addresses with same lval but different offset into separate buckets. Addresses with different offsets should be kept separate, but in the same bucket.
• in the meet, for adresses with the same lval, check whether their offset may have the same integer value. Do this by translating the offset into an intdomain value. If two addresses may have the same offset, retain both in the result of the meet

[sim642]

Wow, this issue is essentially just an earlier instance of #822, which I didn't notice when finding those other broken combinations.