几个月前，我看到一个关于buildit（https://buildit.so/）的演讲，这是一个非常棒的项目，它实现了作为C++库的分阶段元编程。我喜欢它在主流语言中并且不需要修改编译器的核心原则。
一个有趣的观察结果是，可以通过在Z3类上编写__bool__函数来重载布尔转换。通过一些技巧，你可以记录相当纯净的Python代码中的所有路径。通过这种方式，你可以简单地实现Python代码的符号执行，而无需通常的繁琐操作，或者将Python代码符号化地反映为纯Z3表达式。
## 部分求值和元编程Z3
我在使用MetaOCaml后就注意到，在Python中进行Z3元编程有很多分阶段元编程的味道（有什么大惊小怪的？也许这个观察结果没有多少内容）。
一些元编程框架或风格看起来与非分阶段代码非常不同。你明确地调用各种奇怪的函数来构建代码对象。
一种非常酷的分阶段元编程风格采用非分阶段代码并添加一些注释以获得分阶段代码。分阶段代码与原始代码越相似越好。它可能需要某种语言级别的特性，例如引用、重载或内省才能实现这一点。
分阶段元编程的一个典型示例是展开幂函数（Ershov）。这是一个简单的非分阶段递归幂函数示例，它作用于常规的Python整数。
```python
def mypow(x: int, n: int):
if n == 0:
return 1
else:
return x * mypow(x, n - 1)
assert mypow(2, 3) == 8
mypow(2, 3)
```
相反，你可以使用看起来非常相似的代码来生成代码字符串。Python的f-字符串功能（正在不断改进，我希望有带标签的字符串）提供了一些不错的引用机制。非常可爱的是，以下内容看起来就像上面一样。我们将参数n解释为已知为“编译时”/静态，并将参数x解释为已知为“运行时”/动态。
```python
def Code(t): return str
def mypow(x: Code(int), n: int) -> Code(int):
if n == 0:
return "1"
else:
return f"{x} * {mypow(x, n - 1)}"
assert mypow("x", 3) == "x * x * x * 1"
mypow("x", 3)
```
如果我们将Z3表达式视为“代码”，则会发生非常相似但更具结构化的事情。这实际上为我们提供了一个可以处理的树形结构。
```python
import z3
def code(typ):
if typ == int:
return z3.IntSort()
def mypow(x: Code(int), n: int) -> Code(int):
if n == 0:
return 1
else:
return x * mypow(x, n - 1)
x = z3.Int("x")
assert mypow(x, 3).eq(x * (x * (x * 1)))
mypow(x, 3)
```
“静态”编译时由常规Python值扮演，而“动态”由Z3表达式扮演。你可以在编译时和运行时之间混合使用，在求解器中或多或少地执行操作。例如展开循环对应于展开量词。由于Z3使用Python的重载，因此相同的代码可以通过轻微的注释以不同的方式使用。
我认为符号执行有两个值得注意的设计点。你是将所有分支都扔进求解器，还是将单个路径/轨迹扔进求解器进行多次查询？这些方法之间的区别可以被视为阶段混合。分支条件的返回值是静态布尔值还是动态布尔值？
不过，Python中的一些东西确实无法重载。if-then-else块、while循环、链式比较以及and、or、not运算符都无法重载。因此，你需要更改某些内容以使用z3.If。这有点令人沮丧。
## 重载__bool__
但实际上，你可以间接地重载这些功能。当条件不是布尔值时，会调用类上的可重载__bool__函数。你可以在Z3中对其进行修补。
这本身并不能让你达到目的，你需要多次运行相关函数以探索所有路径。这是一种符号执行的版本，本身就很有意义。
你可能可以使用C++ Z3绑定做同样的事情。
我发现这对于将Python代码用作DSL特别有趣。例如，我试图使用Python的“应用”子集作为逻辑，类似于ACL2如何使用Common Lisp的一个子集（https://www.philipzucker.com/applicative_python/），但我当时正在遍历Python AST，这是一种丑陋且冗长的操作。
我在张量编译或MLIR领域也看到了类似的问题。人们至少想要Python语法来进行试验。不过，要获得一个可维护的系统非常困难。
```python
import random
from z3 import *
def symexec(*vs, limit=100):
def wrapper(f):
trace = []
traces = []
# 共享求解器被推送和弹出可能效率更高
s = Solver()
def branch(self):
# branch在每个分支上都被调用（每次要求将Z3表达式转换为具体布尔值时）
s.push()
s.add(And(trace)) # TODO: 我可以将push和pop移动到周围以避免此完整推送
# 掷硬币。可能意味着任何单个运行都将结束。
# 如果没有循环，那么更加确定性是可以的。
if random.random() < 0.5:
take = True
else:
take = False
# 是否可以执行分支？
s.add(self == take)
res = s.check()
s.pop()
if res == sat:
# 可以执行分支
trace.append(self == take)
return take
else:
# 不可能执行分支
trace.append(self == (not take))
return not take
BoolRef.__bool__ = branch # 将__bool__重载修补到其中
for i in range(limit):
if s.check() == unsat: # 如果没有更多可能的路径，则停止
break
trace = [] # 重置轨迹
res = f(*vs) # 运行函数
# res = z3.simplify(res) # 可能不错。
traces.append((trace, res)) # 记录运行结果
s.add(Not(And(trace))) # 再次不允许完全相同的轨迹
BoolRef.__bool__ = None
return traces
return wrapper
@symexec(z3.Int("x"))
def foo(x):
if x > 3:
if x == 4:
return x
else:
return x - 2
else:
return x * 3
foo
```
我们还可以获得诸如比较器链之类的便利功能：
```python
@symexec(Int("x"), Int("y"))
def comparison_example(x, y):
return y - 3 < x < y + 4 or x > 3
comparison_example
```
或者match语句：
```python
@symexec(Int("x"))
def matcher(x):
match x:
case 0:
return 1
case 2:
return x + 14
case _:
return x * 2
matcher
```
或者有界while循环：
```python
@symexec(Int("x"))
def bwhile(x):
if x > 0 and x < 10:
acc = 0
while x > 0:
x -= 2
acc += x
return acc
bwhile
```
我们还可以寻求无界while循环，但输出将不完整。
```python
@symexec(Int("x"), limit=5)
def bfor(x):
acc = 0
while x > 0:
x -= 1
acc += x
return acc
bfor
```
## 细枝末节
如果我想谨慎一些，我应该确保没有达到限制，并且如果结果曾经是None，则忘记返回。
可以将此技术与hypothesis结合使用以获得并发测试。
我可能可以通过检查调用__bool__的堆栈来注意到我们已返回到先前看到的位置来重新捕获循环。但这会很笨拙。也许还可以通过在重载中记录更多信息来做到这一点，但这需要更多工作。
一些关于MLIR和其他使用DSL的Python语法的想法。
这可能对Z3重新表示很有用。重写AST + 重写字节码 + 重载。
exocompiler等。
可以将ifthenelse转换为x if c else。
chococpy
codon
mypyc
buildit风格
温度计延续
dialectica和探测。
通过重载bool进行符号执行
实际上，以这种方式使用C++可能会在考虑范围内。对C++进行符号执行并不容易。当然有Klee。但Klee需要很大的努力。
Symcc具有一种部分求值的感觉
使用相同的思想进行部分求值？轨迹从设置一些变量开始。并发
实际上检测循环似乎很难，因为我们不是用相同的表达式再次到达循环。
通过使用hypothesis进行并发。装饰器“部分求值”
Rosette与Python + Z3相比到底提供了什么？我从未清楚这一点（https://docs.racket-lang.org/rosette-guide/index.html）。如果你喜欢的话，它确实在Racket上创建了一个DSL。
可以切换到基于Not的形式。
用其他元数据标记代码字符串可能非常有用。你希望它在类型没有意义时尽早失败。但这让你无法使用f字符串。:(
一些关于压缩使输出更漂亮的想法。
我们可能希望编译成if then else树，那么我们如何安排事物会有很大的不同。