fix some vlub non monotonic behavior

[monniaux]

Previously, vlub (Ifptr Pbot) (I i) produced Ifptr Ptop if va_strict tt was false, yet vlub (Ifptr Pbot) (Ifptr bot) was Ifptr Pbot.

Not only this was non-monotonic, it also resulted in integer sequences (i=0, 1, …) being over-approximated by Ifptr Ptop, as opposed to Ifptr Pbot. This in turn resulted in e.g. being unable to conclude that t+i was Nonstack if t was Nonstack.

Note: there remain some non-monotonic behaviors in vlub, which I have not fixed.

[xavierleroy]

I agree it would be nice to have fewer irregularities in the value analysis. However, the proposed change (which is actually a revert to what an early version of the value analysis did) is not acceptable because it triggers unwanted optimizations when absolute addresses are used. (For various reasons, authors of embedded systems love to hard-code addresses as integer constants in their code, even though this is completely undefined behavior.) Consider:

int x;

int f(_Bool b)
{
  int * p = b ? &x : (int *) 0x1000;
  x = 42;
  return *p;
}

With the proposed fix, return *p is optimized to return 42, since p is analyzed as an Ifptr to the address of x. It's a valid optimization in CompCert's semantics, and probably valid too in strict ISO C, yet even GCC and Clang at O2 don't do this optimization, since it so clearly violates the intent of the code. That's why the current vlub sets p to top.

It should be possible to improve value analysis while keeping it suitably conservative, but the abstract domain of values, esp. the many roles of Ifptr, probably needs changing.

[monniaux]

Indeed. I had been working on something more ambitious which, as you say, splits the roles of Ifptr by introducing Itop and Ltop. This works, including with respect to your example above, but is more intrusive. Would you be interested in a pull request for this one?

[xavierleroy]

I gave it a try in #490. Also tried to simplify the management of provenance information. vlub remains non-monotonic because of the special case vlub(non-zero integer constant, pointer), but I think this special case is needed to avoid some over-optimizations, so we can live with it.