On Thu, Apr 3, 2025 at 2:23 AM Krister Walfridsson via Gcc
<gcc@gcc.gnu.org> wrote:
>
> I have more questions about GIMPLE memory semantics for smtgcc.
>
> As before, each section starts with a description of the semantics I've
> implemented (or plan to implement), followed by concrete questions if
> relevant. Let me know if the described semantics are incorrect or
> incomplete.
>
>
> Accessing memory
> ----------------
> Memory access in GIMPLE is done using GIMPLE_ASSIGN statements where the
> lhs and/or rhs is a memory reference expression (such as MEM_REF). When
> both lhs and rhs access memory, one of the following must hold --
> otherwise the access is UB:
> 1. There is no overlap between lhs and rhs
> 2. lhs and rhs represent the same address
>
> A memory access is also UB in the following cases:
> * Any accessed byte is outside valid memory
> * The pointer violates the alignment requirements
> * The pointer provenance doesn't match the object
> * The type is incorrect from a TBAA perspective
> * It's a store to constant memory
correct.
Note that GIMPLE_CALL and GIMPLE_ASM can also access memory.
> smtgcc requires -fno-strict-aliasing for now, so I'll ignore TBAA in this
> mail. Provenance has its own issues, which I'll come back to in a separate
> mail.
>
>
> Checking memory access is within bounds
> ---------------------------------------
> A memory access may be represented by a chain of memory reference
> expressions such as MEM_REF, ARRAY_REF, COMPONENT_REF, etc. For example,
> accessing a structure:
>
> struct s {
> int x, y;
> };
>
> as:
>
> int foo (struct s * p)
> {
> int _3;
>
> <bb 2> :
> _3 = p_1(D)->x;
> return _3;
> }
>
> involves a MEM_REF for the whole object and a COMPONENT_REF to select the
> field. Conceptually, we load the entire structure and then pick out the
> element -- so all bytes of the structure must be in valid memory.
>
> We could also do the access as:
>
> int foo (struct s * p)
> {
> int * q;
> int _3;
>
> <bb 2> :
> q_2 = &p_1(D)->x;
> _3 = *q_2;
> return _3;
> }
>
> This calculates the address of the element, and then reads it as an
> integer, so only the four bytes of x must be in valid memory.
>
> In other words, the compiler is not allowed to optimize:
> q_2 = &p_1(D)->x;
> _3 = *q_2;
> to
> _3 = p_1(D)->x;
Correct. The reason that p_1(D)->x is considered accessing the whole
object is because of TBAA, so with -fno-strict-aliasing there is no UB
when the whole object isn't accessible (but the subsetted piece is).
> Question: Describing the first case as conceptually reading the whole
> structure makes sense for loads. But I assume the same requirement -- that
> the entire object must be in valid memory -- also applies for stores. Is
> that correct?
Yes. Like for loads this is for the purpose of TBAA.
>
>
> Allowed out-of-bounds read?
> ---------------------------
> Compile the function below for x86_64 with "-O3 -march=x86-64-v2":
>
> int f(int *a)
> {
> for (int i = 0; i < 100; i++)
> if (a[i])
> return 1;
> return 0;
> }
>
> The vectorizer transforms this into code that processes one scalar element
> at a time until the pointer is 16-byte aligned, then switches to vector
> loads.
>
> The original code is well-defined when called like this:
>
> int a[2] __attribute__((aligned(16))) = {1, 0};
> f(a);
>
> But the vectorized version ends up reading 8 bytes out of bounds.
>
> This out-of-bounds read is harmless in practice -- it stays within the
> same memory page, so the extra bytes are accessable. But it's invalid
> under the smtgcc memory model.
>
> Question: Is this considered a valid access in GIMPLE? If so, what are the
> rules for allowed out-of-bounds memory reads?
The "out-of-bound memory reads" thing is used for
a) TBAA
b) possibly range analysis for access indexes (the 'i' in a[i])
For TBAA vector(T) is the same as T. For index analysis, unless
the vector(T)[i'] access is fully outside of the contained object, it
should not be inferred that i' is an invalid index.
Validity at runtime is then determined by whether the difference can
be observed which to my understanding is about traps from unmapped
pages in case of reads (and of course bogus values written to unrelated
memory for writes). (similarly 'volatile' accesses are considered to be
exactly observable)
So the "GIMPLE abstract machine" (to introduce that term...) would
consider aligned, partly out-of-bound accesses as valid, fully
out-of-bound accesses as invalid. Complementary to that, TBAA
restrictions apply (which for vector vs. component accesses are waived).
>
>
> Alignment check
> ---------------
> Question: smtgcc currently gets the alignment requirements by calling
> get_object_alignment on the tree expression returned from
> gimple_assign_lhs (for stores) or gimple_assign_rhs1 (for loads). Is that
> the correct way to get the required alignment?
That's the conservative alignment the compiler may assume, so yes. Note
that this function derives the alignment from the access, so if a pass
does emit a wrongly aligned access the function will then report a bigger
alignment. Of course it can also happen that there's just more knowledge
and we can give a less conservative answer, like (*p).a vs. b.a after
propagating &b into p. So ultimatively the abstract machine knows
the alignment of objects from their declaration (DECL_ALIGN) or the
allocation (malloc, etc.) and that of pointers by tracking their provenance.
So in the end alignment checking is similarly difficult as verifying actual
TBAA constraints (tracking the active dynamic type of every memory location)
Richard.
>
>
> /Krister
