A DSL for peephole transformation rules of integer operations in the PyPy JIT

Re:A DSL for peephole transformation rules of integer operat... by westurner on Wednesday October 23, 2024 @02:02PM (#41927655)

math.fma fused multiply add is in Python 3.13. Are there already rules to transform expressions to math.fma?

And does Z3 verification indicate differences in output due to minimizing float-rounding error?

https://docs.python.org/3/library/math.html#math.fma :

> math.fma(x, y, z)

> Fused multiply-add operation. Return (x * y) + z, computed as though with infinite precision and range followed by a single round to the float format. This operation often provides better accuracy than the direct expression (x * y) + z.

> This function follows the specification of the fusedMultiplyAdd operation described in the IEEE 754 standard.

[ Parent | on HN ]

Re:A DSL for peephole transformation rules of integer operat... by cfbolztereick on Wednesday October 23, 2024 @02:53PM (#41928178)

I only support integer operations in the DSL so far.

(but yes, turning the python expression x*y+z into an fma call would not be a legal optimization for the jit anyway. And Z3 would rightfully complain. The results must be bitwise identical before and after optimization)

[ Parent | on HN ]

Re:A DSL for peephole transformation rules of integer operat... by westurner on Friday October 25, 2024 @06:54AM (#41944043)

Does Z3 distinguish between x*y+z and z+y*x, in terms of floating point output?

math.fma() would be a different function call with the same or similar output.

(deal-solver is a tool for verifying formal implementations in Python with Z3.)

[ Parent | on HN ]