RFR: 8346664: C2: Optimize mask check with constant offset [v22]

[Quan Anh Mai]

On Sat, 8 Feb 2025 18:30:56 GMT, Matthias Ernst <duke at openjdk.org> wrote:

>> Fixes [JDK-8346664](https://bugs.openjdk.org/browse/JDK-8346664): extends the optimization of masked sums introduced in #6697 to cover constant values, which currently break the optimization.
>> 
>> Such constant values arise in an expression of the following form, for example from `MemorySegmentImpl#isAlignedForElement`:
>> 
>> 
>> (base + (index + 1) << 8) & 255
>> => MulNode
>> (base + (index << 8 + 256)) & 255
>> => AddNode
>> ((base + index << 8) + 256) & 255
>> 
>> 
>> Currently, `256` is not being recognized as a shifted value. This PR enables further reduction:
>> 
>> 
>> ((base + index << 8) + 256) & 255
>> => MulNode (this PR)
>> (base + index << 8) & 255
>> => MulNode (PR #6697)
>> base & 255 (loop invariant)
>> 
>> 
>> Implementation notes:
>> * I verified that the originating issue "scaled varhandle indexed with i+1"  (https://mail.openjdk.org/pipermail/panama-dev/2024-December/020835.html) is resolved with this PR.
>> * ~in order to stay with the flow of the current implementation, I refrained from solving general (const & mask)==0 cases, but only those where const == _ << shift.~
>> * ~I modified existing test cases adding/subtracting from the index var (which would fail with current C2). Let me know if would like to see separate cases for these.~
>
> Matthias Ernst has updated the pull request incrementally with one additional commit since the last revision:
> 
>   Reword correctness (fixes).

src/hotspot/share/opto/mulnode.cpp line 2113:

> 2111: //
> 2112: //    expr % mod == 0                             (multiple of power of two)
> 2113: // => (a + expr) % mod         == a % mod         (zero element in modular arithmetic)

The use of the `%` operator here is pretty misleading, what we want is the unsigned remainder (a.k.a the floor remainder or the mathematical congruent notation). You also need the modular of the int or long arithmetic to be divisible by `mod` for this to work. I suggest writing it in pure mathematical form like this. Better formatting is encouraged:

    This section is concerned with pure mathematics values, not programming arithmetic values. For unsigned integers x, y; let's denote x mod y be the unsigned remainder of x when divided by y. It satisfies:
    - (x mod y) < y
    - There exists integer q such that x == q * y + (x mod y)
    According to the basic properties of division, this value is unique
    We then have:
    1. a mod 2**w == (a mod 2**W) mod 2**w
      Proof: Call a mod 2**w = r1 and a mod 2**W = r2, we have:
        a == q1 * 2**w + r1
        a == q2 * 2**W + r2
        -> q1 * 2**w + r1 == q2 * 2**W + r2
        -> r2 == (q1 - q2 * 2**(W - w)) * 2**w + r1
        -> r2 mod 2**w == r1
        -> (a mod 2**W) mod 2**w == a mod 2**w (qed)
    2. expr mod 2**w == 0 -> ((a + expr) mod 2**W) mod 2**w == a mod 2**w
      Proof: Since expr mod 2**w == 0, we have expr == q1 * 2**w
      Call a mod 2**w == r, we have a == q2 * 2**w + r
      We have a + expr == q2 * 2**w + r + q1 * 2**w == (q2 + q1) * 2**w + r
      Which means that (a + expr) mod 2**w == a mod 2**w
      Furthermore, since (a + expr) mod 2**w == ((a + expr) mod 2**W) mod 2**w (according to 1)
      We have ((a + expr) mod 2**W) mod 2**w == a mod 2**w (qed)

    Back to the programming arithmetic domain, ((a + expr) mod 2**W) is the sum of a and expr in the int/long domain, a mod 2**w == a & (2**w - 1). This leads to us having:
    (a + expr) & (2**w - 1) == a & (2**w - 1)
    Furthermore, mask & (2**w - 1) == mask
    (a + expr) & (2**w - 1) & mask == a & (2**w - 1) & mask
    -> (a + expr) & mask == a & mask (qed)

-------------

PR Review Comment: https://git.openjdk.org/jdk/pull/22856#discussion_r1952057285