Idea: leverage PyPy

[Rik-de-Kort]

Given that

• The PyPy interpreter is built upon RPython which is a subset of Python
• CrossHair essentially reimplements the Python interpreter in z3 and derives useful results from that

It might be possible to implement CrossHair only for RPython, and then leverage the PyPy interpreter for any other code. crosshair check would proceed by first using the PyPy interpreter to turn Python code into RPython code, which would be implemented in symbolics. Then we check the model to potentially generate a counterexample.

Questions arising from that process:

• I'm not sure the counterexample is immediately translatable to a user-level counterexample, since it has to go back through the PyPy interpreter.
• Introducing the PyPy interpreter as a translation step might complicate the z3 models so they become harder to check

Nevertheless, thought it was an interesting idea, so I put it out there.

[pschanely]

Very much an interesting idea. So far, I've mostly only been thinking about selectively pulling in PyPy implementations. See #104 if you haven't noticed it already. That discussion brings up an open question in my mind about different kinds of implementations having different objectives. IIRC, I remember being surprised that opcode dispatch in PyPy is a giant if/else (not a hash lookup!). That's because the compiler is optimized to detect if/else chains that can be implemented as case statements, so it's quite efficient in practice.

I think there is very much an open question about the feasibility of a "real" symbolic interpreter instead of the kind of wacky approach we have now, and RPython might be a very convenient level to target. My hunch is that this kind of solution will also have problems and "sweet spots." It would be really interesting to see a proof of concept here. If it looks promising, I'd love to help integrate that kind of system into CrossHair: ensemble approaches are our best chance of making something useful today.

The discussion in #86 sort of went off the rails, but the core of it is talking about the feasibility of a more pure symbolic approach, so might also be of interest.