Finding JIT Optimizer Bugs using SMT Solvers and Fuzzing

In this blog post I want to describe a recent bug finding technique that I've added to the PyPy JIT testing infrastructure. This technique uses the Z3 theorem prover to find bugs in the optimizer of P