Re:Mining JIT traces for missing optimizations with Z3
by cfbolztereick on Sunday July 21, 2024 @05:12PM
(#41028161)
PyPy has formally verified the integer abstract domain using Z3, a quite important part of our jit optimizer (will write about that in the coming weeks).
We also run a fuzzer regularly to find optimization bugs, using Z3 as a correctness check:
The peephole optimizations aren't themselves formally verified completely yet. We've verified the very simplest rules, and some of the newer complicated ones, but not systematically all of them. I plan to work on fully and automatically verifying all integer optimizations in the next year or so. But we'll see, I'll need to find students and/or money.
We also run a fuzzer regularly to find optimization bugs, using Z3 as a correctness check:
https://pypy.org/posts/2022/12/jit-bug-finding-smt-fuzzing.h...
The peephole optimizations aren't themselves formally verified completely yet. We've verified the very simplest rules, and some of the newer complicated ones, but not systematically all of them. I plan to work on fully and automatically verifying all integer optimizations in the next year or so. But we'll see, I'll need to find students and/or money.