Inequalities between pointers do not work

[karoliineh]

Looking further through SV-COMP tasks, I stumbled upon an imprecision due to inequalities between pointers.

In task loops/veris.c_NetBSD-libc_loop.i:

...
typedef int Char;
Char *tmp;

int glob2 (Char *pathbuf, Char *pathlim) {
  Char *p;
  for (p = pathbuf; p <= pathlim; p++) {
    __VERIFIER_assert(p<=tmp);
    *p = 1;
  }
  return 0;
}

int main () {
  Char pathbuf[1 +1];
  Char *bound = pathbuf + sizeof(pathbuf)/sizeof(*pathbuf) - 1;
  tmp = pathbuf + sizeof(pathbuf)/sizeof(*pathbuf) - 1;
  glob2 (pathbuf, bound);
  return 0;
}

In function glob2, the loop bound pathlim is pathbuf[1], but p runs past it; and with unrolling, the loop body where p → pathbuf[2] is not dead.

The length of pathbuf is 2, and the loop should stop at index 1. However, since this is unknown due to the pointer inequality not working, we fail to verify memsafety.

The following minimization can be used as a regression test when solving this issue:

typedef int Char;

int main () {
  Char pathbuf[1 +1];
  Char *ptr = pathbuf;
  Char *bound = pathbuf + 1;
  __goblint_check(ptr < bound); // SUCCESS

  return 0;
}

[michael-schwarz]

I guess the problem is that we have turned things into IntDomain elements when the comparison gets called, and we return top when getting an int domain representation of an pointer.

[sim642]

Stripping the casts like we do for Eq/Ne is the easy part. The hard part is that evalbinop_base simply doesn't have cases for Lt/... on the address domain at all.
For Eq/Ne those are implemented via AD.meet which has special behavior via semantic_equal of addresses and offsets. There's no easy way to get inequalities out of that. The many layers from address sets to offsets need new semantic comparison operators. Eventually it should boil down to Offset.MakeLattice.to_index like semantic_equal, but the intermediate layers need to handle ambiguous points-to-sets (like the special AD.meet) and all pairs of Addr/NullPtr/UnknownPtr/StrPtr.