几个月前看到关于 buildit 的演讲，它是一个用 C++库实现分阶段元编程的项目，喜欢其在主流语言中且无需修改编译器的核心原则。得出一个技巧可让不可重载语法变为可重载。
有趣观察是通过在 Z3 类上写__bool__函数可重载布尔转换，通过一些技巧可记录纯 Python 代码的所有路径，实现 Python 代码的符号执行或将 Python 代码符号化表示为纯 Z3 表达式。
用 Python 元编程 Z3 有分阶段元编程的味道，分阶段元编程有多种风格，一种是给未分阶段代码添加注释得到分阶段代码，使其更像原始代码，可能需要语言级特性如引用、重载或内省来实现。
以展开幂函数为例展示未分阶段递归幂函数和生成代码字符串的相似代码，还展示了将 Z3 表达式视为“代码”的类似情况，“静态”编译时由常规 Python 值扮演，“动态”由 Z3 表达式扮演，可在编译和运行时之间处理事情。
Python 中一些东西不可重载，如if-then-else块、while、链式比较、and or not运算符，需用z3.If改变，可间接重载这些特性，需多次运行函数以探索所有路径，这是符号执行的一种版本，可使用 C++Z3 绑定实现同样的事情。
将 Python 代码用作领域特定语言很有趣，如用“应用式”Python 子集作为逻辑，之前遍历 Python AST 很丑陋，在张量编译或 MLIR 世界也有类似问题，人们希望有 Python 语法。
定义symexec装饰器用于符号执行，可处理各种情况如比较器链、匹配语句、有界while循环、无界while循环等，还提到可结合假设进行测试，可通过检查调用__bool__的栈来重新捕获循环，但较复杂。
还提到相关项目如 CrossHair 等，python 的预处理器、jupyter 中的特殊操作等，以及其他相关的编译器如 exocompiler 等，讨论了不同的编程风格和技术，如 buildit 风格、温度计延续、dialectica 和探测等，思考在 C++中以这种方式进行符号执行的可能性及相关问题。