JIT 整数优化窥孔规则 DSL¶

对于 JIT 中的整数窥孔优化，我们使用了一种基于模式匹配的领域特定语言，它指定了如何简化（一系列）整数运算。它在 jit/metainterp/optimizeopt 目录中实现。此目录包含 optimizeopt 中整数重写 DSL 的实现。然后将这些规则编译成 RPython 代码，该代码在 optimizeopt 中执行转换。重写规则在构建过程中会自动使用 Z3 证明其正确性。此页面介绍了该 DSL 的工作原理以及如何使用它。

简单的转换规则¶

DSL 中的规则指定了整数运算如何转换为更便宜的其他整数运算。规则始终由名称、模式和目标组成。这是一个简单的规则

add_zero: int_add(x, 0)
    => x

规则的名称是 add_zero。它匹配跟踪中 int_add(x, 0) 形式的运算，其中 x 将匹配任何内容，而 0 将仅匹配常量零。在 => 箭头之后是重写的目标，即运算被重写成的内容，在本例中为 x。

规则语言知道哪些运算满足交换律，因此 add_zero 也将优化 int_add(0, x) 为 x。

模式中的变量可以重复

sub_x_x: int_sub(x, x)
    => 0

此规则匹配 int_sub 运算，其中两个参数相同（要么是同一个盒，要么是同一个常量）。

这是一个具有更复杂模式的规则

sub_add: int_sub(int_add(x, y), y)
    => x

此模式匹配 int_sub 运算，其中第一个参数由 int_add 运算产生。此外，加法的其中一个参数必须与减法的第二个参数相同。

常量 MININT、MAXINT 和 LONG_BIT（为 32 或 64）可以在规则中使用，它们的行为类似于编写数字，但允许使用与位宽无关的公式

is_true_and_minint: int_is_true(int_and(x, MININT))
    => int_lt(x, 0)

也可以有一个模式，其中某些参数需要是常量，而不指定哪个常量。这些模式如下所示

sub_add_consts: int_sub(int_add(x, C1), C2) # incomplete
    # more goes here
    => int_sub(x, C)

以 C 开头的模式中的变量仅匹配常量。但是，在此当前形式下，规则是不完整的，因为目标运算中使用的变量 C 在任何地方都没有定义。我们将在下一节中了解如何计算它。

计算常量和其他中间结果¶

有时需要计算目标运算中使用的中间结果。为此，可以在规则头和规则目标之间进行额外的赋值。

sub_add_consts: int_sub(int_add(x, C1), C2) # incomplete
    C = C1 + C1
    => int_sub(x, C)

此类赋值的右侧是 Python 语法的子集，支持使用 +、-、* 的算术运算以及某些辅助函数。但是，语法允许您明确某些运算的无符号性。例如，>>u 用于无符号右移（我计划为比较添加 >u、>=u、<u、<=u）。

检查¶

某些重写仅在某些条件下才成立。例如，int_eq(x, 1) 可以重写为 x，如果已知 x 存储布尔值。这可以使用检查来表达

eq_one: int_eq(x, 1)
    check x.is_bool()
    => x

检查后跟一个布尔表达式。模式中的变量可以用作检查中的 IntBound 实例（以及赋值中），以了解抽象解释对跟踪变量值的了解。

这是一个例子

mul_lshift: int_mul(x, int_lshift(1, y))
    check y.known_ge_const(0) and y.known_le_const(LONG_BIT)
    => int_lshift(x, y)

它表示 x * (1 << y) 可以重写为 x << y，但检查 y 是否已知介于 0 和 LONG_BIT 之间。

检查和赋值可以重复并相互组合

mul_pow2_const: int_mul(x, C)
    check C > 0 and C & (C - 1) == 0
    shift = highest_bit(C)
    => int_lshift(x, shift)

除了调用 IntBound 实例上的方法之外，还可以访问它们的属性，例如在此规则中

and_x_c_in_range: int_and(x, C)
    check x.lower >= 0 and x.upper <= C & ~(C + 1)
    => x

规则排序和活跃性¶

生成的优化器代码将优先应用将常量或变量作为重写结果的规则。只有在这些规则都不匹配的情况下，才会应用生成新结果运算的规则。例如，规则 sub_x_x 和 sub_add 在尝试 sub_add_consts 之前进行尝试，因为前两个规则分别优化为常量和变量，而后者则生成新的运算作为结果。

规则 sub_add_consts 存在一个潜在的问题，即如果规则头中 int_add 运算的中间结果被其他一些运算使用，则 sub_add_consts 规则实际上并没有减少运算的数量（并且由于寄存器压力增加，实际上可能会使情况略微恶化）。但是，目前在 JIT 的优化过程中考虑此类信息将极其困难，因此我们仍然乐观地应用这些规则。

检查规则覆盖率¶

每个重写规则都应该至少有一个单元测试来触发它。为了确保这一点，test_optimizeintbound.py 文件中的测试在测试运行结束时都有一个断言，即每个规则至少触发一次（此检查有时会触发误报，例如当使用 -k 运行单个测试时）。

打印规则统计信息¶

JIT 可以打印有关哪个规则触发了多少次的统计信息，这些信息位于 jit-intbounds-stats 记录类别中。例如，要将其打印到程序执行结束时的标准输出，请像这样运行 PyPy

PYPYLOG=jit-intbounds-stats:- pypy ...

输出将类似于以下内容

int_add
    add_reassoc_consts 2514
    add_zero 107008
int_sub
    sub_zero 31519
    sub_from_zero 523
    sub_x_x 3153
    sub_add_consts 159
    sub_add 55
    sub_sub_x_c_c 1752
    sub_sub_c_x_c 0
    sub_xor_x_y_y 0
    sub_or_x_y_y 0
int_mul
    mul_zero 0
    mul_one 110
    mul_minus_one 0
    mul_pow2_const 1456
    mul_lshift 0
...

终止和汇合性¶

目前，不幸的是，没有检查规则是否真的将运算重写为“更简单”的形式。没有成本模型，也没有任何东西可以阻止你编写这样的规则

neg_complication: int_neg(x) # leads to infinite rewrites
    => int_mul(-1, x)

如果还有另一个规则将与 -1 的乘法转换为否定，则这样做会导致无限重写。

也没有检查（尚未？）汇合性，即从相同输入跟踪开始的所有重写始终导致相同输出跟踪的属性，无论规则应用的顺序如何。

证明¶

编写在所有极端情况下都不正确的窥孔规则非常容易。因此，默认情况下，所有规则在编译成实际 JIT 代码之前都会使用 Z3 证明其正确性。当证明失败时，会打印一个（希望是最小的）反例。反例包括满足检查的所有输入的值、中间表达式的值，以及源运算和目标运算的两个不同值。

例如，如果我们尝试添加不正确的规则

mul_is_add: int_mul(a, b)
    => int_add(a, b)

我们会得到以下反例作为输出

Could not prove correctness of rule 'mul_is_add'
in line 1
counterexample given by Z3:
counterexample values:
a: 0
b: 1
operation int_mul(a, b) with Z3 formula a*b
has counterexample result vale: 0
BUT
target expression: int_add(a, b) with Z3 formula a + b
has counterexample value: 1

如果我们添加条件，则会考虑这些条件

mul_is_add: int_mul(a, b)
    check a.known_gt_const(1) and b.known_gt_const(2)
    => int_add(a, b)

这将导致以下反例

Could not prove correctness of rule 'mul_is_add'
in line 46
counterexample given by Z3:
counterexample values:
a: 2
b: 3
operation int_mul(a, b) with Z3 formula a*b
has counterexample result vale: 6
BUT
target expression: int_add(a, b) with Z3 formula a + b
has counterexample value: 5

某些 IntBound 方法不能在 Z3 证明中使用，因为它们具有过于复杂的控制流如果出现这种情况，它们可以在 test_z3intbound.Z3IntBound 类中定义 Z3 等效公式（在每种情况下都会这样做，如果 Z3 友好的重构和实际实现彼此不同，则这是一个潜在的证明漏洞，因此需要格外小心以确保它们等效）。

如果这也太难了，可以通过在其主体中添加 SORRY_Z3 来跳过单个规则的证明（但我们应该尽量避免这样做）。

eq_different_knownbits: int_eq(x, y)
    SORRY_Z3
    check x.known_ne(y)
    => 0

检查可满足性¶

除了检查规则是否产生了正确的优化之外，我们还会检查规则是否能够应用。这确保了一些运行时值能够满足规则中所有检查条件。以下是一个违反此规则的示例。

never_applies: int_is_true(x)
    check x.known_lt_const(0) and x.known_gt_const(0) # impossible condition, always False
    => x

目前错误消息不是完全易于理解，我希望以后能够改进这一点。

Rule 'never_applies' cannot ever apply
in line 1
Z3 did not manage to find values for variables x such that the following condition becomes True:
And(x <= x_upper,
    x_lower <= x,
    If(x_upper < 0, x_lower > 0, x_upper < 0))

添加新规则¶

要添加新规则（理想情况下，由实际追踪中观察到的问题推动），应执行以下步骤。

在test_optimizeintbound.py中添加一个失败的测试。
将规则添加到real.rules中。
运行pypy ruleopt/generate.py重新生成Python代码（为此，您需要安装z3-solver和rply包）。
检查test_optimizeintbound.py是否通过，然后运行其他optimizeopt/测试（特别是optimizeopt/test/test_z3checktests.py检查操作和预期输出是否合理）。

DSL 实现说明¶

DSL 的实现采用了一种相对临时的方式。它使用rply进行解析，有一个小型类型检查器试图查找规则编写方式中的常见问题。Z3 通过 Python API 使用。模式匹配 RPython 代码的生成使用受 Luc Maranget 的论文Compiling Pattern Matching to Good Decision Trees启发的方法，参见这篇博文以了解易于理解的介绍。