A DSL for Peephole Transformation Rules of Integer Operations in the PyPy JIT | PyPy

[utterances-bot]

A DSL for Peephole Transformation Rules of Integer Operations in the PyPy JIT | PyPy

https://www.pypy.org/posts/2024/10/jit-peephole-dsl.html

[squenson1]

In the section "Computing constants and other intermediate results", should not C = C1 + C1 be C = C1 + C2?

[arigo]

In mul_lshift: int_mul(x, int_lshift(1, y)), it's unclear why you need to add the rule check y.known_ge_const(0) and y.known_le_const(LONG_BIT). I think that if that check is not satisfied, then we can look at it in two ways:

• either the int_lshift(1, y) would give undefined results anyway, and adding the check doesn't change the fact that the incoming instruction was already undefined;
• or we say that int_lshift is well-defined and in practice works by considering only the lower bits of y, and in that case, then the replacement is valid even without the check.

[cfbolz]

In the section "Computing constants and other intermediate results", should not C = C1 + C1 be C = C1 + C2?

absolutely, fix is on the way.

[cfbolz]

it's unclear why you need to add the rule check y.known_ge_const(0) and y.known_le_const(LONG_BIT)

Yeah, that's a good point. I cargo-culted the check y.known_ge_const(0) and y.known_le_const(LONG_BIT) part from the non-dsl version of the code. The metainterp/blackhole consider it undefined to shift by something negative or large and raise an assertion. But I don't model a result being undefined in the Z3 proofs yet, so I'll have to think a bit more carefully about the whole area (also because I would like to move some of the int_add_ovf rules to the DSL). Right now I inherit the semantics of int_lshift from Z3 in the proofs, and that returns 0 if the shift amount is outside of the 0...63 range.