[CN] VIP: adjust constraints carefully in the presence of non. det. pointer equality

[dc-mak]

It's not clear that VIP w/ non-det. pointer equality is sound with respect to PNVI-ae-udi w/ non-det. pointer equality.

#include <inttypes.h>
int main() {
  int y=2, x=1;
  int *p = (int *)((uintptr_t)&x + sizeof(int));
  int *q = (int *)((uintptr_t)&y + 0);
  return (p==q) ? 0 : 1;
}

If it is, the above example will incorrectly be classed as non-det. in the VIP implementation right now, when it should really return true or 0.

The issue is that a fresh allocation ID is made every time an integer is cast to a pointer, which is essentially an effectful operation.

And I can't constrain it to just be the default<alloc_id> because for non-det. pointer equality I need to be able to prove both provenance _in_equality as well as equality.

I would then need to add constraints in the appropriate place with all other provenances to ensure that the empty provenance is never used to index the allocation history (and maybe even adjust the types in the SMT solver as an extra layer, but this might affect how users can write specs).

[dc-mak]

I think a cleaner solution would be to make any cast from an integer to a pointer which would result in "@empty" provenance as undefined behaviour.

This would mean the "@empty" provenance does not need to be encoded anywhere in CN pointers (may still be needed for memory bytes), and sidestep any extra constraints and questions about indexing the allocation history.

This should also fix any soundness issues by excluding the problematic "PNVI pi ~ VIP @empty" relation from the VIP soundness proof - in the presence of non-det. pointer eq. the statement "@empty leads to strictly more UB" is not true.

It would also need to restrict the "permissive array/member shifts" and forbid calling those on NULL pointers.