A few months ago I saw a talk on buildit, https://buildit.so/ a really neat project that achieves staged metaprogramming as a C++ library. I love the

Symbolic Execution by Overloading `__bool__`

submited by
Style Pass
2024-12-24 04:00:03

A few months ago I saw a talk on buildit, https://buildit.so/ a really neat project that achieves staged metaprogramming as a C++ library. I love the central tenets of being in a mainstream language and not requiring a modified compiler. Right on, brother. One thing I came away with was a neat trick for getting non-overloadable syntax to be overloadable.

The interesting observation, which seems clear in hindsight (the best observations are), is that bool conversion is overloadable by writing a __bool__ function on the Z3 class. With a little hackery, you can record all the paths through a piece of fairly pure python code. In this way you can simply achieve symbolic execution of python code without the usual expected rigamarole, or symbolically reflect python code as pure z3 expressions.

I have noted for a while after tinkering with MetaOCaml that metaprogramming z3 in python has a lot of the flavor of staged metaprogramming (big surprise? Maybe there’s not much content to the observation).

Leave a Comment