On Wed, 10 Dec 2025, Richard Biener wrote:
The problem is that in GIMPLE, a pointer does not need to be in bounds. The caller
could call the function with a value of i such that p + i happens to be equal to
&a. So, as I understand it, the GIMPLE semantics do not allow the pass to conclude
that p + i == &a is false, unless p + i is dereferenced (because dereferencing a
through p + i would be UB due to provenance).
GIMPLE adopts most of the C pointer restrictions here thus we can (and do)
conclude that pointers stay within an object when advanced. This is used by
the PTA pass which results are used when we optimize your example. You have to
divert to integer arithmetic to circumvent this and the PTA pass, while
tracking provenance through integers as well, does the right thing with this.
Great, that is much better for smtgcc than the semantics I have currently
implemented!
But it is not completely clear to me what "most of the C pointer
restrictions" implies. Is the following a correct interpretation?
1. A pointer must contain a value that points into (or one past) an object
corresponding to its provenance (where a pointer may have multiple
provenances). Otherwise it invokes undefined behavior.
2. The provenance used for the result of POINTER_PLUS is the union of the
provenances for the two arguments.
3. The POINTER_PLUS operation is UB if the calculation overflows and
TYPE_OVERFLOW_WRAPS(ptr_type) is false.
4. The rules are the same for the calculations done in MEM_REF and
TARGET_MEM_REF as for POINTER_PLUS.
Question: For the TARGET_MEM_REF calculation:
BASE + STEP * INDEX + INDEX2 + OFFSET
Is it treated as one POINTER_PLUS, i.e.
BASE + (STEP * INDEX + INDEX2 + OFFSET)
or as two (i.e. do we care about overflow and OOB between the two index
calculations)?
FWIW, the vectorizer and ivopts do introduce pointers that are outside the
object (which is why I allowed it in my current semantics)...
/Krister
