基于 Rust 和 Z3 的无循环程序综合（2020）

# 使用 Rust 和 Z3 合成无循环程序 来源：https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html 自动寻找实现给定规范的程序称为*程序合成*。其主要难点在于搜索空间庞大：规模为 \\\(n\\\) 的程序数量呈指数级增长。朴素地枚举所有规模为 \\\(n\\\) 的程序，逐一检查它们是否满足规范，然后再处理规模为 \\\(n\+1\\\) 的程序——这种方法无法扩展。然而，该领域通过采用更智能的搜索技术来修剪搜索空间、利用 SMT 求解器的性能提升，以及有时限制问题范围来取得进展。 在本文中，我将介绍一种现代程序合成方法：基于组件的无循环程序的反例引导迭代合成，正如 Gulwani 等人所著的《无循环程序的合成》(https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/pldi11-loopfree-synthesis.pdf) 中所述。我们将详细解释每个术语的含义，并还将介绍一个使用 Z3 求解器 (https://github.com/Z3Prover/z3) 编写的 Rust 实现。 我对本文的期望有两方面： 1. 我希望那些不熟悉程序合成的人——就像不久前的我一样——能变得不那么陌生，并学到一些关于这个主题的新知识。我提供了许多例子，并将论文中密集的逻辑公式分解成更小、更易理解的部分。 2. 我希望那些已经熟悉这类程序合成的人能帮助我诊断实现中的一些性能问题，我无法重现文献中报告的合成结果。对于一些较难的基准问题，综合器甚至无法在我的耐心耗尽之前找到解决方案。 ## 目录 - 动机 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#motivation) - 任务概述 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#an-overview-of-our-task) - 问题形式化 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#formalizing-the-problem) - SMT 求解器简介 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#a-brief-introduction-to-smt-solvers) - 反例引导迭代合成 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#counterexample-guided-iterative-synthesis) - 带组件的 CEGIS (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#cegis-with-components) - 验证基于组件的程序 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#verifying-a-component-based-program) - 基于组件程序的有限合成 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#finite-synthesis-of-a-component-based-program) - 实现 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#implementation) - 程序表示 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#program-representation) - 构建程序 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#building-programs) - 定义组件 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#defining-components) - 规范 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#specifications) - 综合器 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#the-synthesizer) - 位置映射 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#location-mappings) - 验证 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#verification) - 有限合成 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#finite-synthesis) - CEGIS 循环 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#the-cegis-loop) - 结果 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#results) - 结论 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#conclusion) - 参考文献 (https://fitzgen.com/2020/01/13/synthesizing-loop-free-programs.html#references) ## 动机 为什么要编写一个为我编写其他程序的程序？我是不是只是太懒了，不想自己写程序？当然是的。然而，即使不像我这么懒的人，也有很多合理的理由想要合成程序。有些程序手动编写正确颇为棘手，而程序综合器可能在你我可能失败的地方取得成功。 快！如何仅用三条位操作指令隔离一个字中最右边的零位？ ``` ,--- 最右边的零位。 V 输入: 011010011 输出: 000000100 ^ | '--- 只有该位被设置。 ``` 你得到了吗？... 好的，答案是： ``` isolate_rightmost_zero_bit(x): // x = 011010011 a ← not x // a = 100101100 b ← add 1, x // b = 011010100 c ← and a, b // c = 000000100 return c ``` 我们的程序综合器将在不到一秒内找到*一个*解决方案，并在大约一分钟内找到*最短长度*的解决方案。我手动完成同样的事情需要更长的时间。我们将在本文其余部分回到这个问题，并将其作为一个持续使用的例子。 使用程序综合器的另一个原因可能是我们需要编写的程序数量远多于我们手动编写的时间。以编译器的窥孔优化器 (https://en.wikipedia.org/wiki/Peephole_optimization) 为例：它考虑一个滑动指令序列窗口，对于每个序列，它检查是否知道一个等效但更快或更小的指令序列。当它知道一个更好的指令序列时，它会将原始指令替换为更好的指令。 窥孔优化器通常由模式匹配规则构建，这些规则识别次优的指令序列并配对用于替换匹配的改进指令序列： ``` new PeepholeOptimizer( pattern0 → replacement0 pattern1 → replacement1 pattern2 → replacement2 // ... patternn → replacementn ) ``` 每个`replacementi`都是一个小巧的、优化的微型程序。如果我们从头开始手动编写一个新的窥孔优化器，我们将必须自己编写 \\\(n\\\) 个优化的微型程序。而 \\\(n\\\) 可能很大：LLVM 的`InstCombine`窥孔优化器有超过 1,000 个模式与替换对。即使只有一半的数量也远多于我想自己编写的数量。 与其手动编写那些优化的微型程序，我们可以将每个原始指令序列作为规范，将其输入程序综合器，并看看综合器是否能找到执行相同功能的最佳指令序列。最后，我们可以使用所有这些原始指令序列及其合成的、优化的指令序列作为模式与替换对，自动构建一个窥孔优化器！ 这个想法最早由 Bansal 等人在《自动超级窥孔优化器的生成》(https://theory.stanford.edu/~aiken/publications/papers/asplos06.pdf) 中提出。 > ***编辑：**John Regehr (https://twitter.com/johnregehr)向我指出，这个想法在 Bansal 等人论文于 2006 年发表之前就早已出现。他向我指出了 Davidson 等人在 1980 年发表的《可重定向窥孔优化器的设计与应用》(https://dl.acm.org/doi/10.1145/357094.357098) 作为一个例子，但指出即使这也不是它第一次出现。* ## 任务概述 程序合成是根据规范，自动寻找满足它的程序的行为。为了使问题更容易处理，我们通过两种方式限制其范围： 1. **无循环：**我们只合成没有循环的程序。 2. **基于组件：**我们只合成可以表示为给定组件库组合的程序。 无循环的限制对于许多用例来说限制不大。例如，窥孔优化器通常不考虑跨越循环边界的指令序列。 基于组件的合成意味着，综合器不是使用目标语言的任何数量的任何组合来合成程序，而是被提供一个组件库，并合成每个组件恰好使用一次的程序。综合器重新排列组件，重新连接它们的输入和输出，直到找到满足规范的配置。 也就是说，给定一个包含 \\\(N\\\) 个组件的库，它构建如下形式的程序： ``` synthesized_program(inputs...): temp0 ← component0(params0...) temp1 ← component1(params1...) // ... tempN-1 ← componentN-1(paramsN-1...) return tempN-1 ``` 其中，`paramsi`中的每个参数要么是程序中前面定义的`tempj`变量，要么是原始的`inputs`之一。 例如，给定两个组件： - `f(a)` - `g(a, b)` 以及一个输入参数`x`，综合器可以构建以下任何候选程序（隐式返回最后定义的变量）： ``` a ← g(x, x) b ← f(x) ``` 或 ``` a ← g(x, x) b ← f(a) ``` 或 ``` a ← f(x) b ← g(x, x) ``` 或 ``` a ← f(x) b ← g(a, x) ``` 或 ``` a ← f(x) b ← g(x, a) ``` 或 ``` a ← f(x) b ← g(a, a) ``` 就是这样。这就是给定这两个组件，它可能构建的*所有*程序。综合器*不能*构建以下程序，因为它没有使用每个组件： ``` a ← f(x) ``` 综合器*不能*构建这个程序，因为它使用了`f`组件超过一次： ``` a ← f(x) b ← f(a) c ← g(b, b) ``` 最后，它*不能*构建这最后一个程序，因为这最后一个程序使用了一个不在我们给定库中的函数`h`： ``` a ← f(x) b ← h(a, x) ``` 下表通过将基于组件的合成与完全通用的程序合成进行比较，描述了基于组件合成的一些属性： | 通用合成 | 基于组件的合成 | | :--- | :--- | | **合成程序的形状** | 使用目标语言的任何数量的任何表达式 | 仅使用库中的组件 | | **合成程序的大小** | 可变 | 恰好是库的大小，因为库中的每个组件恰好使用一次 | 在我们的综合器中，组件将是固定位宽整数上的函数（在 SMT 求解器术语中也称为“位向量”），它们将对应于我们虚拟指令集中的单条指令：`add`、`and`、`xor` 等。但原则上它们也可以是更高级的函数或任何我们可以在 SMT 查询中编码的东西。更多关于 SMT 查询的内容稍后介绍。 虽然基于组件的合成使合成问题更容易，但它在每次调用综合器时都迫使我们做出一个决定：我们必须选择可用组件的库。每个组件在合成的程序中恰好使用一次，但如果我们想合成一个执行多次加法的程序，我们可以在库中包含多个`add`组件的实例。 组件太少，综合器可能找不到解决方案。组件太多会减慢综合器的速度，并让它生成可能包含死代码的非最优程序。 总结来说，在无循环程序的基于组件的合成中，我们综合器的输入是 - 一个规范，以及 - 一个组件库。 它的输出是一个满足规范的程序（用给定的组件表示），或者如果找不到这样的程序则返回一个错误。 ## 问题形式化 为了合成一个程序，我们需要一个描述所需程序行为的规范。规范是一个逻辑表达式，描述当程序给定这些输入时的输出。我们用以下方式定义规范： - \\\(\\vec\{I\}\\\) 作为程序输入， - \\\(O\\\) 作为程序输出， - \\\(\\phi\_\\mathrm\{spec\}\(\\vec\{I\}, O\)\\\) 作为关联输入和输出的表达式。当 \\\(O\\\) 是在输入 \\\(\\vec\{I\}\\\) 上运行程序所需的输出时，此表达式应为真。 我们给定的组件库是一个描述每个组件行为的规范多重集。每个组件规范附带它需要的输入数量（例如，一个`add(a, b)`组件需要两个输入，一个`not(a)`组件需要一个输入），以及一个将组件输入与其输出关联起来的逻辑公式。 组件输入、输出和表达式的符号与程序规范相似，但带有一个下标： - \\\(\\vec\{I\}\_i\\\) 是第 \\\(i^\\mathrm\{th\}\\\) 个组件的输入变量， - \\\(O\_i\\\) 是第 \\\(i^\\mathrm\{th\}\\\) 个组件的输出变量， - \\\(\\phi\_i\(\\vec\{I\}\_i, O\_i\)\\\) 是将第 \\\(i^\\mathrm\{th\}\\\) 个组件的输入与其输出关联起来的逻辑表达式。 我们定义 \\\(N\\\) 为库中的组件数量。 对于我们的隔离最右边零位的例子，我们可以给综合器的最小组件库是什么，同时仍然保留其找到所需解决方案的能力？它应该是一个恰好包含与解决方案程序中每条指令对应的组件的库：一个`not`、一个`add1`和一个`and`组件。 | 组件定义 | 描述 | \\\( \\phi\_0(I\_0, O\_0) \\\) | \\\( O\_0 = \\texttt\{bvadd\}\(1, I\_0\) \\\) | | :--- | :--- | :--- | :--- | | \\( \\phi\_1(I\_1, I\_2, O\_1) \\\) | \\( O\_1 = \\texttt\{bvand\}\(I\_1, I\_2\) \\\) | 位向量上的按位与操作。 | | \\( \\phi\_2(I\_3, O\_2) \\\) | \\( O\_0 = \\texttt\{bvnot\}\(I\_3\) \\\) | 位向量上的按位非操作。 | 程序合成可以表达为一个*存在-全称*问题：我们想要找到是否存在某个程序 \\\(P\\\)，使得*对于所有*给定的输入和其返回的输出，该程序满足规范。 > \\\( \\begin\{align\} & \\exists P: \\\\ & \\quad \\forall \\vec\{I\},O: \\\\ & \\quad \\quad P\(\\vec\{I\}\) = O \\implies \\phi\_\\mathrm\{spec\}\(\\vec\{I\}, O\) \\end\{align\} \\\) 让我们分解一下，并将其翻译成英文： \\( \\exists P \\\) 存在某个程序 \\\(P\\\)，使得 \\( \\forall \\vec\{I\},O \\\) 对于所有输入 \\\(\\vec\{I\}\\\) 和输出 \\\(O\\\)， \\( P\(\\vec\{I\}\) = O \\\) 如果我们在输入 \\\(\\vec\{I\}\\\) 上运行程序得到输出 \\\(O\\\)， \\( \\implies \\\) 那么 \\( \\phi\_\\mathrm\{spec\}\(\\vec\{I\}, O\) \\\) 我们的规范 \\\(\\phi\_\\mathrm\{spec\}\) 得到满足。 理解这种*存在-全称*形式化很重要，因为我们的最终实现将使用几乎相同的公式向 SMT 求解器（本例中为 Z3）进行查询。它不会*完全*相同： - \\\(P\\\) 是一个抽象，隐藏了有关组件的一些细节， - 我们将执行一些代数变换， - 我们不会在单个查询中一次性将整个问题提交给求解器。 尽管如此，实现正是基于这种形式化，如果我们不掌握这一点，我们将走不远。 ## SMT 求解器简介 在简要讨论 SMT 求解器及其能力之前，我们无法继续。像 Z3 这样的 SMT 求解器接受一个逻辑公式（可能包含未绑定变量），并返回该公式是： - *可满足的：* 存在对未绑定变量的赋值使得断言为真，并且这里有一个描述这些赋值的模型。 - *不可满足的：* 公式的断言为假；没有对未绑定变量的赋值能使它们为真。 SMT 求解器以一种类似 Lisp 的输入语言接受它们的断言，称为 SMT-LIB2 (http://smtlib.cs.uiowa.edu/)。 这是一个可满足的 SMT 查询示例： ``` ;; `x` 是某个整数。