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: https://github.com/goblint/analyzer/blob/00809949512925a6ecf1b04d531f3c739667ce87/src/analyses/base.ml#L299-L300 AD.meet applies meet to the offsets as follows: https://github.com/goblint/analyzer/blob/00809949512925a6ecf1b04d531f3c739667ce87/src/cdomains/lval.ml#L105-L116 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.