Jelvis Uses Z3 Solver to Replace Manual Rules in Compiler Optimization

Jelvis利用Z3求解器取代编译器优化中的手动规则 将代码转化为有界SMT逻辑公式，让求解器直接验证等价性并合成更快的指令，从而无需手工编写优化遍。 Tikhon Jelvis阐述了如何通过将一种极简语言（IMP）编译为由Z3评估的声明式SMT约束，来消除命令式编程与形式逻辑之间的隔阂。通过内联函数、将循环展开至有限边界，并将其转换为带有符号化if-then-else phi节点的静态单赋值（SSA）形式，程序可以作为符号执行轨迹进行双向分析。Jelvis说明了有界模型检测如何将时序性质转化为简单的布尔逻辑，展示了反向可满足性如何验证程序等价性，并探讨了反例引导的归纳合成（CEGIS）如何为超级优化、程序草图绘制以及自定义DSL工具提供支持。 将命令式代码编译为声明式SMT公式需要内联函数、将循环展开至指定边界，并将变量更新转换为静态单赋值（SSA）形式。 (14:05) 由于编译后的SMT公式没有方向偏差，因此求解器可以作为常规解释器进行正向查询，作为非确定性逆向解释器进行反向查询，或为了有界不变量验证进行双向查询。 (8:48) 反例引导的归纳合成（CEGIS）将基于求解器的合成器与验证器配对，利用具体的边缘情况反例来迭代优化代码并剪枝庞大的搜索空间。 (32:27) SMT程序验证采用反向可满足性模型：断言输出存在分歧意味着SAT结果是测试失败并产生反例，而UNSAT则形式化证明了在展开边界内的等价性。 (31:52)

Tikhon Jelvis argues that compiling imperative programs into SMT logic formulas enables automated verification, bidirectional execution, and program synthesis by turning execution traces into declarative constraints. By bounding loops and relying on fixed-width bit-vector theories in solvers like Z3, developers can bypass the undecidability of general software analysis and build practical formal tooling. Compiling Imperative Execution into Declarative Logic (6:22) Analyzing software through an SMT solver requires compiling imperative source code into a static, unordered logical formula. Using a minimal imperative toy language called Imp, Jelvis models program execution as a symbolic trace partitioned into inputs, intermediate states, and outputs. Translating sequential mutation into mathematical logic requires three distinct steps: hygienic function inlining, bounded loop unrolling, and Single Static Assignment (SSA) conversion. In SSA, every variable assignment generates a distinct immutable symbol, such as x₁ = x₀ + a₀, removing chronological time from the representation. While an ordinary interpreter executes only the active branch of an if statement, a symbolic formula compiler must translate both branches unconditionally. Merging these diverged variable states mirrors SSA phi functions, which Jelvis implements directly through Z3's native if-then-else (ite) expressions. Rather than relying on high-level mathematical abstractions like unbounded integers or reals, the compiler explicitly encodes numeric values as 32-bit bit vectors. Jelvis emphasizes that fixed-width representations match physical hardware behavior and prevent solvers from slipping into undecidable reasoning. Bidirectional Execution and Inverted Verification Logic (8:48) Because SMT formulas express declarative relationships rather than fixed operational steps, they exhibit no inherent directionality. Fixing input variables and solving for outputs causes the solver to act as a forward interpreter. Conversely, fixing terminal outputs and requesting valid inputs runs the program in reverse, yielding input counter-images or generating test payloads. In bounded model checking, developers can express temporal properties across unrolled execution slices, translating invariant 'always' checks into conjunctions and 'eventually' assertions into disjunctions across state versions. When verifying a program against a reference specification, the satisfiability outcome is inverted compared to standard test suites. The compiler asserts that both programs share identical inputs while asserting that their outputs differ. If the solver reports SAT, verification has failed because the solver discovered a concrete counterexample where the outputs diverge. Conversely, an UNSAT result formally proves that the implementations produce identical outputs for every possible input within the loop iteration bound. Synthesis, Superoptimization, and Scope Boundaries (32:27) Verifying code against a reference model extends naturally into program synthesis via Counterexample-Guided Inductive Synthesis (CEGIS). A synthesizer proposes a candidate program satisfying an initial input-output pair, which a verifier tests to discover diverging edge cases. Feeding these counterexamples back into the synthesizer eliminates large portions of the search space in relatively few iterations. Jelvis notes that this loop enables superoptimization without requiring developers to hand-craft fragile compiler optimization rules, as demonstrated in his work generating optimized code for a low-level Forth architecture. Because SMT synthesis becomes computationally expensive on large codebases, Jelvis recommends applying it across sliding peephole windows or using program sketching, where solvers fill in specific holes within a programmer-defined skeleton. Furthermore, while general-purpose languages introduce messy semantic overhead, domain-specific languages (DSLs) represent the primary sweet spot for SMT tooling. DSLs typically feature tightly constrained operational semantics and bounded loops, allowing SMT verification to deliver practical guarantees without unmanageable performance bottlenecks. SMT performance remains largely a black box, as formula size does not reliably predict solver solving times. While proving the total absence of counterexamples can trigger long compute times, Jelvis notes that practical workflows—such as automated exploit detection or offline test-suite generation—can successfully manage solver limitations using bounded iteration thresholds and execution timeouts.

Tikhon Jelvis 在 Compose Conference 演讲中阐述，通过将命令式程序经由循环展开与静态单赋值（SSA）形式编译为 SMT 逻辑公式，开发者可借助 Z3 等求解器实现双向执行、时序不变量验证以及基于反例引导的程序合成。 从 SAT 到 SMT 与程序逻辑编译 (0:12) SMT（可满足性模理论）在经典布尔可满足性（SAT）的基础上引入了数字、数组等高阶领域理论。例如，Z3 支持超过 30 种不同理论，能够将机器字建模为位向量理论，并支持精确到具体位模式的形式化浮点理论。虽然微软研究院最初对 Z3 采用了限制性学术许可，但随后将其以 MIT 许可开源，并提供了跨 OCaml、.NET、Haskell 等语言的 API 接口。 分析软件时，编译器将源代码映射为逻辑公式，公式变量划分为输入、各执行步骤的中间状态以及最终输出三组。为应对图灵完备性与赖斯定理所带来的停机问题与无界路径挑战，分析采用有界验证策略：将循环强制展开至预设上限（如 1000 或 10000 次），从而将无界计算降维为 SMT 求解器可完全穷举分析的有界公式。 SSA 转换与公式编译器架构 (11:44) Jelvis 选用学术界经典的玩具命令式语言 IMP 作为演示，该语言将语义严格划分为无副作用的值表达式（布尔与 32 位整数）以及改变状态但不返回值的命令（赋值、分支、循环与顺序执行）。编译到一阶逻辑的核心难题在于消除程序的时间序列概念：逻辑公式本身是无方向且静态的，必须通过静态单赋值（SSA）技术，在变量每次被赋值时生成带版本号的新变量（如 x1 = x0 + a0）。 该编译器结构与传统解释器高度平行，但纯表达式返回的是未绑定的 SMT 抽象语法树（AST）片段而非具体数值；命令执行则直接向 Z3 推送逻辑断言（在 Haskell 中表现为 Z3 () Monad），并利用 Z3 原生的增量求解特性叠加约束。针对分支合并，传统编译器的 phi 函数在 SMT 中直接映射为原生条件选择表达式 ite（if-then-else）。对于分支内修改的变量，编译器生成新变量并断言其等于 ite(条件, then分支值, else分支值)，从而无条件同时编译两条路径。 双向执行、时序不变量与反向求解 (29:33) 编译生成的 SMT 公式因其声明式本质而完全丧失了固有的执行方向性。固定输入求解输出即为正向解释器；而固定输出反求有效输入则构成反向解释器。反向执行在本质上是非确定性的，求解器能逐一枚举或给出所有可能的原像输入。在安全分析领域，反向解释器可用于根据漏洞接收点的有效载荷反推能绕过过滤器的上游输入字符串。 在程序验证中，求解器的判定逻辑呈现出“反转的可满足性”。验证两个程序等价时，系统断言两者输入相同且输出不相等：若求解器返回 SAT，说明找到了输出发生分歧的反例，验证失败；若返回 UNSAT，则证明两者在展开界限内完全等价。此外，将循环切片为离散步长后，时序逻辑可直接映射为布尔操作，例如“总是（Always）”不变量对应所有步长断言的合取，而“最终（Eventually）”属性则对应各步长断言的析取。 程序合成、超优化与特定领域语言 (32:27) 通过将指令选择、寄存器索引或 AST 节点编码为符号变量，验证机制可自然延伸为程序合成。反例引导的归纳合成（CEGIS）构建了合成器与验证器之间的反馈循环：合成器先生成满足有限测试样例的候选程序，验证器寻找反例并将其回传给合成器以进一步修剪搜索空间。Jelvis 指出，利用 SMT 构建窥孔超优化器，相比为复杂或小众硬件手写 GCC 式优化规则要简单得多，只需构建语义公式编译器即可。 面对通用全功能语言的极端复杂性，Jelvis 认为特定领域语言（DSL）是 SMT 工具链落地的最佳场景。DSL 通常缺乏无界循环或图灵完备特性，有界验证足以覆盖其完整语义，且设计者能完全掌控其规约。对于更广泛的辅助开发场景，程序草图（Sketching，如 Synquid 系统）允许开发者仅编写框架并由求解器填补代码“空洞”，同时位向量理论能确保在规避无界实数求解不可判定性风险的同时实现有限时间终止。 SMT 技术通过将程序执行轨迹符号化，为验证、反向分析和指令级优化提供了严密的自动化数学手段。然而，通用语言中无界循环与复杂控制流导致的求解器性能黑盒问题依然存在，当前最具可行性的工业级应用仍主要集中在滑动窗口超优化、带超时的反例搜索以及语义受限的 DSL 验证之中。

## Background 该内容由 Tikhon Jelvis 在 2016 年 Compose Conference 上发表，由 Compose Conference 频道发布于 YouTube 平台。视频介绍了 SMT 求解器（如 Z3）在程序分析、验证、以及编译优化中的广泛应用，探讨了如何通过 Haskell 绑定将程序逻辑转换为 SMT 约束公式。 ## TL;DR 本演讲详细阐述了将程序编译为 SMT 公式的技术路径，包括函数内联、循环展开以及 SSA 形式转换。演讲展示了如何利用求解器的符号化能力进行程序有界验证、等价性检查，甚至通过反例引导的归纳合成（CEGIS）实现程序自动优化。Tikhon Jelvis 强调了 SMT 求解器在领域特定语言（DSL）开发中的实用价值，并指出通过设定迭代边界，可以将复杂的验证问题转化为求解器可处理的逻辑断言，从而实现工程化的静态分析。 ## Atmosphere & style 这场演讲展现出浓厚的学术交流氛围，兼具实用工程主义的清晰逻辑与极客式的幽默感。主讲人 Tikhon Jelvis 说话节奏明快，语气既严谨又不失轻松，他经常在复杂的技术原理中穿插对于编程工具（如 Emacs）的小调侃，使观众感到亲切。整个演示风格扎实且注重实战，通过流畅的伪代码分析和逻辑流程图，将高深的理论转化为开发者触手可及的实现范例，听众能感受到一种揭开黑盒技术面纱后的愉悦感。 ## Bulletin - [06:22](https://www.youtube.com/watch?v=ruNFcH-KibY&t=382s) 程序经函数内联、循环展开与静态单赋值（SSA）转换为 SMT 逻辑公式后，可利用 Z3 消除执行方向性，同时胜任正向模拟、逆向输入反推与中间不变量证明。 - [31:52](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1912s) 程序等价性验证并非直接求证输出相同，而是断言输出相异；当求解器判定可满足（SAT）时即可捕获破坏等价性的边缘反例，不可满足（UNSAT）则代表有界范围内数学证明成立。 - [34:15](https://www.youtube.com/watch?v=ruNFcH-KibY&t=2055s) 结合反例引导的归纳合成（CEGIS）与基于位向量的局部窥孔滑动窗口，无需编写复杂的重写规则即可自动化实现面向特殊硬件架构的代码超级优化。 - [36:27](https://www.youtube.com/watch?v=ruNFcH-KibY&t=2187s) 相比通用语言面临的学术研究级复杂度，领域特定语言（DSL）由于语法精简且天然缺乏无界循环需求，成为落地 SMT 形式化分析与程序草图合成（Sketching）的最佳场景。 ## Key takeaways - [00:12](https://www.youtube.com/watch?v=ruNFcH-KibY&t=12s) 现代 SAT 求解器因极高的高效性以及工程问题易于编码映射，成为形式化验证不可或缺的底层基石。 - [02:03](https://www.youtube.com/watch?v=ruNFcH-KibY&t=123s) SMT 求解器在此基础上扩展了位向量、浮点数、数组等高阶领域理论；其中 Z3 凭借 MIT 开源协议与完备的理论支持成为工业界默认选型。 - [06:22](https://www.youtube.com/watch?v=ruNFcH-KibY&t=382s) 面对任意无界循环导致的图灵完备性与不可判定性（莱斯定理），有界验证（Bounded Verification）通过设定上限静态展开循环，换取实用静态分析的可行性。 - [08:48](https://www.youtube.com/watch?v=ruNFcH-KibY&t=528s) 将程序编译为逻辑公式赋予了执行的非确定性与双向性，不仅能当作正向解释器，还能构建寻找生成特定 Payload 的逆向解释器。 - [14:59](https://www.youtube.com/watch?v=ruNFcH-KibY&t=899s) 将 Imp 命令式教学语言编译为公式包含三个核心步骤：函数内联消除调用语义、循环展开压平结构，以及静态单赋值（SSA）消除时间维度。 - [17:27](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1047s) SSA 转换中利用 Φ 函数与 Z3 原生的 ite（If-Then-Else）布尔表达式，将分支汇聚处动态决定的变量取值显式抹平并编码到逻辑公式中。 - [25:00](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1500s) 公式编译器在架构上类似于镜像解释器，但在处理命令时利用增量求解特性逐步生成断言，并通过求解器自动生成全局唯一的同名 Fresh 变量。 - [29:33](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1773s) 在有界模型检验（BMC）中，时态逻辑的“始终为真”（安全属性）与“最终为真”（活性属性）可直接离散化映射为每轮迭代断言的大 AND 与大 OR 运算。 - [31:52](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1912s) 在 CEGIS 循环中，求解器与验证器相互对抗，通过在少量 I/O 样本与边缘反例之间迭代剪枝，能够在几轮搜索内高效率合成满足规范的目标程序。 - [34:15](https://www.youtube.com/watch?v=ruNFcH-KibY&t=2055s) 草图合成（Sketching）允许开发者只保留带有漏洞（holes）的代码骨架与断言规范，由合成引擎（如 Synquid）自动填充函数体实现细节。 - [36:27](https://www.youtube.com/watch?v=ruNFcH-KibY&t=2187s) 对于测试用例生成场景，SMT 求解器的性能耗时并不致命，因为测试用例只需离线耗时生成一次，即可在线支持高吞吐回归测试。 - [39:50](https://www.youtube.com/watch?v=ruNFcH-KibY&t=2390s) 系统全量基于 32 位位向量（Bit-Vectors）而非无界整数或非线性算术建模，主动放弃对全局完备性的追求以换取判定过程的确定性与有界终止保证。 ## Detailed walkthrough ### [00:12](https://www.youtube.com/watch?v=ruNFcH-KibY&t=12s) SMT 求解器与布尔可满足性（SAT）基础 在 Compose Conference 会议当天的最后一场演讲中，主讲人 Tikhon Jelvis 针对 Z3 SMT 求解器及其在程序分析中的应用展开了探讨。他开场提到，许多人已经注意到本届大会存在一条关于 SMT 求解器的“次级主线”（sub-theme），而他的演讲更偏向于入门性质，旨在展示如何将 SMT 求解器落地应用于实际问题。虽然演示代码采用 Haskell 编写并调用 Z3，但其中的核心思想与具体的编程语言或求解器无关，可以无缝迁移至任何语言与主流 SMT 求解器中。 讨论 SMT 求解器必须追溯到它的根基——布尔可满足性问题（Boolean Satisfiability Problem，简称 SAT）。SAT 是计算机科学中经典的 NP 完全问题，但在工程实践中，现代 SAT 求解器的发展使得针对真实世界应用场景的求解速度快得惊人。SAT 之所以极具吸引力，主要在于两点：第一，业界已经拥有性能极高的高效 SAT 求解器；第二，相比于其他 NP 完全问题，将具体的业务与逻辑问题编码映射为 SAT 表达式要容易得多。标准的 SAT 问题公式化描述为：给定一组布尔变量，变量之间通过与（AND）、或（OR）以及非（NOT）进行逻辑组合，求解器的目标是判断是否存在一组布尔真假值赋值，使得整个公式的值为真。求解器最终要么给出一组使公式成立的具体变量赋值（SAT），要么判定该命题无解、不可满足（UNSAT）。 ```mermaid flowchart TD accTitle: SAT 与 SMT 关系流程图 accDescr: 展示从底层 SAT 布尔求解扩展到包含多理论支持的高阶 SMT 求解过程 subgraph SAT_Level["SAT 求解器 (底层比特运算)"] direction TB B_VARS["布尔变量 (True / False)"] LOGIC_OPS["逻辑连接词 (AND, OR, NOT)"] SAT_CORE["SAT 引擎判定: SAT (提供解) / UNSAT"] B_VARS --> LOGIC_OPS --> SAT_CORE end subgraph SMT_Level["SMT 求解器 (高阶领域理论扩展)"] direction TB SMT_THEORIES["丰富理论库: 整数/实数、数组、位向量、浮点数"] SMT_ENGINE["领域特定优化引擎 (如 Z3)"] SMT_THEORIES --> SMT_ENGINE end SAT_Level -->|"扩展高阶类型与领域逻辑"| SMT_Level ``` ### [02:03](https://www.youtube.com/watch?v=ruNFcH-KibY&t=123s) SMT 的高阶理论扩展与 Z3 求解器特性 SMT（Satisfiability Modulo Theories，可满足性模理论）在纯布尔变量的基础上进行了强力扩充。在 SMT 中，变量不再局限于布尔类型，而是可以直接表达针对数值、数组等复杂类型的约束条件。Jelvis 指出，SAT 在某种程度上类似于底层的机器逻辑，开发者必须逐个比特（bit-by-bit）去手工建模；而 SMT 求解器则提供了更高级的抽象，其内置的各种“理论”（Theories）赋予了求解器深入的领域特定洞察力，从而能在更高层面上更快地求解复杂命题。Z3 拥有极为强大的理论支持库，涵盖了三十种以上的理论支持。 在这些理论中，机器字长（位向量，Bit-Vectors）尤其重要。它被建模为一系列比特序列，Z3 不仅能原生处理语言中常见的移位、与或非等按位运算，还能将位向量直接视作数值进行有符号和无符号的加法、乘法与除法。更前沿的进展是建立在位向量之上的浮点数理论（Floating-Point Arithmetic）。以往在分析程序时，人们通常用理想化的实数去近似浮点数，这在关注程序验证的严格正确性时会产生巨大偏差。现今的浮点数理论可以直接用底层的具体比特位来严谨表征浮点数，使得浮点程序的分析与验证能够做到完全精确。 关于工程选型，Z3 是几乎所有人在未遇到特殊限制时的默认首选求解器。它拥有极佳的声誉和极其丰富的理论实现。早期 Z3 受制于微软研究院较为严苛的研究许可协议，主要局限在学术界；但近年来微软已将其完全切换至宽松的 MIT 开源协议，允许免费用于商业应用在内的各类场景。同时，Z3 拥有丰富的多语言 API 绑定，包括 OCaml、C#（以及依托.NET 生态的 F#）和 Haskell。在 Haskell 生态中，主要有两个与 SMT 交互的库： - **SBV**：一个高级领域特定语言（DSL），旨在屏蔽底层差异并支持对接多种不同的 SMT 求解器，适合用于轻量级原型验证与快速实验。 - **Haskell Z3 Bindings**：直接对 Z3 C API 进行了细粒度绑定，暴露了许多 SBV 尚未涵盖的 Z3 原生高阶功能，适合需要与 Z3 紧密集成或构建专业静态分析工具的场景（演讲的配套开源代码也是基于此库构建）。 关于求解器的工业地位，Tikhon Jelvis 明确强调：“Z3 is the specific SMT solver I'm talking about, and it tends to be the default SMT solver everybody goes to first usually unless they have a good reason they're probably going to depend on Z3 because it has a sort of sterling reputation and a lot of different theories.” ### [06:22](https://www.youtube.com/watch?v=ruNFcH-KibY&t=382s) 将程序编译为公式与有界验证技术 演讲的核心主旨在于阐述如何把一段程序编译为一个 SMT 逻辑公式，进而利用求解器来解答关于该程序的各类问题。在公式编码中，变量主要被清晰地划分为三大类： 1. **程序输入变量**：承载程序的起始输入数据。 2. **中间状态变量**：精细追踪程序执行路径中每一步骤所产生的瞬时状态。 3. **程序输出变量**：捕获最终计算所得的结果。 这种将程序执行展开为公式的本质，是构建了一条贯穿整个程序的符号化计算轨迹（Symbolic Computation Trace）。Jelvis 阐述其核心威力在于：“So a good way of thinking about it is that by solving this formula we can make statements about all possible computation traces that your code can take and you can see why this would be very powerful.” ```mermaid flowchart LR accTitle: 程序转 SMT 公式数据流 accDescr: 展示程序输入、执行中间状态到输出转化为一阶逻辑公式并交给求解器的过程 subgraph Program_Execution["符号计算轨迹"] IN["输入变量 (Inputs)"] S1["中间状态 1"] S2["中间状态 2"] OUT["输出变量 (Outputs)"] IN --> S1 --> S2 --> OUT end subgraph SMT_Translation["SMT 求解系统"] FORMULA["SMT 逻辑公式<br>(含路径与分支约束)"] SOLVER["Z3 求解引擎"] FORMULA --> SOLVER end Program_Execution -->|"静态单赋值 / 语义编码"| FORMULA ``` 然而，符号化追踪面临着现实挑战：真实程序往往包含难以穷尽的分支路径与可能陷入死循环的循环结构。SMT 求解器无法在公式中直接表征无限循环。一旦放任任意无限循环，就会不可避免地触及图灵完备性与莱斯定理（Rice's Theorem）的理论边界，导致一系列语义性质在根本上变得不可判定。 为了在工程上解决循环问题，演讲重点介绍了**有界验证（Bounded Verification）**技术： - 主动放弃对任意无界循环的直接分析，强制给循环设定一个确定的人工上限（例如 1,000 次或 10,000 次迭代）。 - 对循环结构进行静态展开（Loop Unrolling），从而将循环彻底扁平化为顺序执行语句。 - 这种妥协通过引入循环边界，换取了自动化静态分析在绝大多数实际程序上的可行性（当然，它也可以与预设的循环不变量相结合，来扩展对特定循环的推理深度）。 ### [08:48](https://www.youtube.com/watch?v=ruNFcH-KibY&t=528s) 多向求解应用：逆向解释、不变量与符号化测试 一旦程序成功被编码为 SMT 约束公式，由于一阶逻辑公式本身不存在天然的“执行方向性”，开发者可以根据分析目的自由固定或求解不同子集的变量： - **正向解释器（Normal Interpreter）**：将输入变量的值固定为常数，要求 SMT 求解输出变量和中间轨迹的值。此时求解器的行为等价于运行一个标准的代码解释器。 - **逆向解释器（Reverse Interpreter）**：固定目标输出变量的值，反向求解能够产生该结果的输入变量及中间状态。逆向执行天然具有非确定性（Non-deterministic）——即多个不同的初始输入可能映射到同一个输出结果。Z3 可以从容应对这种一对多的情况，支持一次性列举所有合法的输入解，或按需逐个生成可行解。 - **中间状态不变量检查（Invariant Verification）**：若开发者期望验证某个不变量（Invariant）在整个生命周期中恒成立，只需将该不变量作为断言约束追加到每一个可能达到的中间状态变量上。求解器随后可以证明该不变量是否永真，或者在不变量失效时精准输出反例路径。 - **程序等价性与有界规范验证**：当存在一个已知正确的高层参考实现（规范程序）与一个待测优化实现时，可以约束两者接收相同的输入，并要求求解器寻找导致两者输出不一致的输入。Jelvis 将其类比为**符号化的 QuickCheck**。在 QuickCheck 等基于属性的测试（PBT）中，框架主要依靠随机生成海量测试用例碰运气来触发 Bug；而借助 SMT 求解器，分析系统是在数学层面对所有可能输入与输出进行符号化的穷尽验证。 为了清晰演示这一整套编译与验证技术，Jelvis 选择了编程语言理论教学中最具代表性的极简命令式语言——**While 语言**（也常称作 Imp 语言）。While 语言拥有最简洁的操作语义（Operational Semantics），实现其解释器极其轻松，因此非常适合作为将语言操作语义编译为 SMT 公式逻辑的教学范例。 ### [11:44](https://www.youtube.com/watch?v=ruNFcH-KibY&t=704s) 简单语言 Imp 的语法设计与类型映射 为了让逻辑求解器能够顺利处理，待分析的语言必须足够简单；编译器越简单，开发工作就越轻松。Tikhon Jelvis 介绍了一种名为 Imp 的典型命令式教学语言。Imp 主要由两部分构成：一部分是没有任何副作用的表达式（Expressions），其计算结果只能是数字或布尔值，且为了简化处理，所有变量都统一定义为 32 位整数（`int`）；另一部分则是命令（Commands），它们不产生返回值，完全依靠修改程序的状态和环境起作用，包括赋值、`while` 循环、`if` 条件分支以及顺序执行（sequence）。 在传统的编程语言理论中，Imp 通常由抽象语法（abstract grammar）定义，涵盖变量、数字字面量以及加减乘除等标准算术运算符。Jelvis 指出，使用 Haskell、OCaml 或 F# 等现代函数式语言的一大优势，在于可以将这些抽象文法极其自然地映射为代数数据类型。在 Haskell 中，开发者甚至可以使用特殊符号定义自定义中缀构造器（infix constructors），使得代码与原本纸面上的语法规则几乎一模一样。 ```mermaid flowchart TD accTitle: Imp 语言的基本构成 accDescr: 展示 Imp 语言中无副作用的表达式与产生副作用的命令的分离架构 subgraph Expressions["表达式 (Expressions: 无副作用，仅求值)"] AExpr["算术表达式 (AExpr) -> 32 位整型"] BExpr["布尔表达式 (BExpr) -> 布尔型"] end subgraph Commands["命令 (Commands: 产生副作用，改变状态)"] C_Assign["变量赋值 (Set)"] C_Seq["顺序执行 (Seq)"] C_If["条件分支 (If)"] C_While["循环语句 (While)"] C_Skip["空操作 (Skip)"] end ``` 针对命令构造器中的 `Skip`，Jelvis 解释其主要用于表达空代码块，比如只有单个分支的 `if` 语句中的空分支。他借用了一个形象的比喻来解释类型系统与后续实现代码之间的关系：“类型就像是一具骨架，而代码则是我们敷在骨架上的一层皮肤，它自然而然地呈现出类型所提供的形态。”将文法拆解为类型后，原本庞大的编译问题被自然拆分成独立的小模块：只需分别解决如何编译 `Skip`、如何编译 `Set`、如何编译 `Seq` 即可，这让整个系统的构建变得格外清晰可控。 - 变量类型一律限定为 32 位整数，杜绝动态类型带来的推断负担。 - 表达式保证纯粹（pure），绝对不包含任何外部副作用。 - 命令不返回任何求值结果，仅负责状态迁移。 - 命令的代数数据类型包含：`Set`（赋值）、`Seq`（顺序结合）、`If`（分支）、`While`（循环）和 `Skip`（空操作）。 --- ### [14:59](https://www.youtube.com/watch?v=ruNFcH-KibY&t=899s) 编译至 SMT 公式的三步走策略：内联、展开与 SSA 转换 将 Imp 代码编译为逻辑公式分为三个关键阶段：函数内联（Inlining）、循环展开（Loop Unrolling）以及转换为静态单赋值形式（Static Single Assignment, SSA）。关于为什么最初的文法中没有提及函数定义，Jelvis 幽默地解释道，函数在第一步就被全部内联展开了，展开后便可以假装系统中根本没有函数。 内联的机制十分简单：生成全新的变量名，然后把函数体直接粘贴到调用处，其行为与 C 语言预处理器类似，但通过生成新变量名避免了作用域冲突。内联的最大好处在于公式层面无需建模函数调用的语义，所有代码都被拉平为直线型代码（straight-line code）。对于潜在的递归问题，处理方式与循环一致——设定一个任意的递归深度上限。第二步则是循环展开，将 `while` 循环机械地拆解为多层嵌套的 `if` 语句。实际工程中，单条循环可能被展开为 100 到 1000 次迭代。虽然展开后的代码量会急剧膨胀，但现代 SMT 求解器的处理吞吐量足以应对这种规模的公式。 谈及求解性能时，Jelvis 坦言 SMT 的求解耗时带有很强的“黑盒”属性。即使是长期使用 SMT 的资深研究者，甚至是求解器本身的开发者，也很难提前准确预测一个公式的求解耗时。“作为一个粗略的经验法则，公式越大耗时越长；但如果两个公式结构差异过大，这个规则就完全不适用了。” ```mermaid flowchart LR accTitle: 程序代码向 SMT 公式的编译流水线 accDescr: 展示从 Imp 代码经过函数内联、循环展开到 SSA 转换的三步流程 P["Imp 原始程序"] --> S1["1. 函数内联 (Inlining)<br/>拉平调用，设定递归上限"] S1 --> S2["2. 循环展开 (Unrolling)<br/>转换为多层嵌套 If 分支"] S2 --> S3["3. SSA 静态单赋值转换<br/>消除时间维度，引入 Φ 函数"] S3 --> Z3F["Z3 SMT 逻辑公式"] ``` --- ### [17:27](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1047s) 静态单赋值（SSA）转换与 Φ 函数的语义消除 第三步是 SSA 转换。命令式程序天然具备时间先后顺序与执行流向（directionality），但底层的逻辑层并不包含时间概念：在求解器眼中，所有逻辑约束是并列且无序的。为了在无方向的纯逻辑世界中保持程序原有的执行时序，必须引入 SSA，为变量的每次更新赋予全新编号。例如变量 $X$ 经过一次修改后，在逻辑公式中会演变为约束 $X_1 = X_0 + A_0$。 在 SSA 转换中，最具挑战性的环节是分支语句（`if` statements）。在程序静态分析阶段，无法预知运行时到底会走哪个分支，这就导致在分支汇聚后，变量的值依赖于不可知的执行路径。编译器的经典解决方案是引入 $\Phi$ 函数（Phi function）。 分支汇聚时会创建一个全新的变量（如 $X_3$），并通过一个类似于“魔法神谕”（magical Oracle function）的选择机制定义其值：如果执行了分支一，则 $X_3 = X_1$；如果执行了分支二，则 $X_3 = X_2$。$\Phi$ 函数成功将条件选择的动态决策逻辑抽离并平铺到 SSA 形式中，为后续将其直接映射为 SMT 条件布尔逻辑铺平了道路。 - 传统的命令式时序通过添加变量版本下标（$X_0, X_1, X_2 \dots$）被彻底消除。 - 逻辑公式本身没有求值顺序，求解器只负责寻找满足全部并列等式赋值的模型。 - $\Phi$ 函数用于连接分支汇聚点，将多条路径的变量版本归一为一个新的单赋值符号。 --- ### [19:38](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1178s) 解释器与 SMT 编译器的镜像设计及位向量约束 在探讨如何用代码实现公式编译器时，Jelvis 指出，只要稍微换个角度观察，公式编译器在架构上几乎就是一个“奇怪的解释器”。为了说明这一点，他将 Imp 解释器的实现与生成 Z3 抽象语法树（AST）及断言的编译器实现进行了逐行对比。两者都划分为三组互相对应的函数（分别处理算术表达式、布尔表达式和命令），并且都维护一个记录变量环境的映射表（scope）。 ```mermaid flowchart TD accTitle: 解释器与 SMT 编译器的结构对照 accDescr: 对比算术/布尔表达式以及命令在解释器与 SMT 编译器中的输出差异 subgraph Interpreter["Imp 解释器"] I_Expr["表达式求值: 读 Scope -> 返回具体值 (Int / Bool)"] I_Cmd["命令执行: 修改 Scope -> 返回更新后的 Scope"] end subgraph SMT_Compiler["SMT 公式编译器"] C_Expr["表达式编译: 读 Scope -> 返回未定值的 Z3 AST 片段"] C_Cmd["命令编译: 更新 SSA Scope -> 直接生成 Z3 Assertion (返回 Z3 Unit)"] end ``` 在解释器中，表达式只能读取环境中的变量，最终算出具体的数值或布尔值；而在 SMT 编译器中，表达式同样只读不写，但它生成的是无法独立求解的 Z3 AST 片段，这些 AST 片段随后会被拼接成完整的逻辑断言。针对命令，解释器执行命令后返回被修改的新环境；而在 Z3 编译器中，处理命令意味着向求解器添加一条全新的全局约束断言（assertion），因此命令编译器的类型签名非常纯粹，就是 `Z3 ()`（Z3 unit）。Jelvis 打趣地补充道，为了演示代码的极简性，他默认所有程序员编写的代码都是完美的，绝不会出现变量未定义的作用域错误。 在实际生成 Z3 的位向量（bit-vector）约束时，底层公式的严格程度往往让人感到繁琐。以编译简单的表达式 `5 + x` 为例，生成的 SMT 表达式必须精确表达为：将一个 32 位宽的位向量字面量 `5` 与同样声明为 32 位宽的位向量变量 `x0` 进行加法操作。SMT 求解器对类型的显式定义要求极高，不仅每一次出现都需要反复声明变量或常量的精确位宽，而且在执行除法或比较等操作时，还必须明确指定究竟是有符号（signed）还是无符号（unsigned）运算。所有的模式匹配代码，正是依托于算术表达式的类型骨架层层展开，逐一转化为这套精密的位向量逻辑断言。 ### [23:14](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1394s) 将 AST 表达式编译为 Z3 公式 在讨论如何把简单的命令式语言翻译成 SMT 公式时，Tikhon Jelvis 将公式编译器的设计与常规解释器进行了对比。在解释器中，如果遇到字面量（Literal），只需直接返回对应的数值；而在 Z3 编译器中，遇到字面量时则需要生成一个指定大小的 32 位位向量（Bit-vector），构造出对应的字面量公式节点。关于作用域（Scope）的处理两者也非常类似：解释器在作用域中保存具体的整数值，而 Z3 编译器的作用域中保存的则是求解器能够识别的“符号变量名”（Symbolic Variable Names），只需通知求解器引用该符号变量即可。 ```mermaid flowchart TD accTitle: Expression Compilation in Z3 accDescr: Flowchart contrasting recursive expression compilation in a normal interpreter versus the monadic Z3 compiler. subgraph Interpreter ["常规解释器模式"] I1["Lit n"] --> I2["直接返回值 n"] I3["Var x"] --> I4["从 Scope 提取具体数值"] I5["Plus e1 e2"] --> I6["直接递归评估: eval e1 + eval e2"] end subgraph Z3Compiler ["Z3 公式编译器模式"] Z1["Lit n"] --> Z2["构造 32-bit 位向量公式节点"] Z3["Var x"] --> Z4["从 Scope 提取对应符号变量"] Z5["Plus e1 e2"] --> Z6["在 Z3 Monad 中显式解构两次递归结果"] Z6 --> Z7["调用 Z3 API 生成加法约束节点"] end ``` 在处理加法（Plus）这类复合表达式时，差异显现出来。解释器可以直接对两个子表达式进行递归调用求和；但在 Z3 绑定中，运算是由 `Z3` Monad 进行管理的，开发者必须显式提取两次递归调用的计算结果，再调用 Z3 接口构造一个加法 AST 节点。Tikhon Jelvis 在这里风趣地提到了代码里使用的 Unicode 下标字符：“这些小小的 Unicode 下标是完全合法的 Haskell 语法，你完全可以在自己的代码里使用这种名字；你可以配置 Emacs 让输入变得非常轻松，虽然所有不用 Emacs 的人都会因此讨厌你，但那是他们自找的（they had it coming）。” 其余的算术和布尔表达式的构造逻辑与加法完全一致：只是将加法节点替换为减法节点，或者将数字字面量替换为布尔字面量，其整体代码结构和递归形态保持不变。 --- ### [25:00](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1500s) 命令语句的翻译、增量求解与变量重命名 与表达式相比，能够改变状态的命令（Commands）更为复杂。编译器的处理机制是将每一条命令转换成独立的断言（Assertion），最后由 Z3 收集所有断言构建一个庞大的复合公式。从概念上讲，这相当于用逻辑“与”（AND）将所有条件连接起来，但分步将断言喂给求解器能让流程更加清晰，并享受到增量求解（Incremental Solving）的好处。 增量求解是一项核心特性：当给求解器输入一定数量的约束并求解完成后，如果后续再追加新的约束，求解器无需推倒重来，而是能够利用其先前的内部状态快速重解。这使得对公式进行逐步求精时不会带来巨大的性能惩罚。 在翻译赋值语句（如 `x:= expr`）时，编译器不会原地修改状态，而是遵循 SSA 规则声明一个全新的变量（例如 $x_1$），并断言 $x_1$ 等于右侧表达式编译得到的结果。在公式编译器内部，一次赋值涉及三个核心动作： ```mermaid flowchart LR accTitle: Assignment Compilation Steps accDescr: Sequence of three operations performed during assignment compilation in Z3. A["1. 生成 Fresh Variable<br/>(保留原名且全局唯一)"] --> B["2. 构造 AST 相等节点<br/>(new_var == rhs_expr)"] B --> C["3. 提交断言至求解器<br/>(z3.assert) 并更新本地 Scope 映射"] ``` - **生成全新变量（Fresh Variable）**：Z3 提供了非常便捷的特性，只要传入变量名，求解器便会自动分配一个同名但全局唯一的全新变量，省去了手写计数器（如手动拼接 $x_1, x_2$）的繁琐状态管理。 - **构建相等断言**：在 AST 中显式生成相等判断节点。 - **提交断言与更新作用域**：调用 `z3.assert` 将断言注册到求解器中，并在本地环境的映射表（Map）中更新变量名，确保源码变量始终指向最新生成的符号变量。 --- ### [27:52](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1672s) 分支语句的编译与 Phi 函数（ITE） 处理条件分支语句（`if-then-else`）是编译过程中的关键难点。在解释器中，程序可以直接判断条件并选择单侧分支执行；但在 Z3 中，所有分支行为必须以符号化（Symbolic）的方式进行，因此**编译器必须同时编译 `then` 和 `else` 两个分支**。 SSA 中的 $\Phi$（Phi）函数在 Z3 中有天然的对应物——`ite`（If-Then-Else）表达式。处理分支语句的具体流程为： 1. 递归编译 `then` 分支与 `else` 分支。 2. 收集两个分支中发生修改的所有变量。 3. 针对每个被修改的变量插入一个 `ite` 函数：断言“若条件为真，则变量取分支 A 的最新版本；若条件为假，则取分支 B 的最新版本”。 4. 将复杂的符号求值逻辑全部交由 SMT 求解器底层去化简。 在控制流转换中，循环语句完全被忽略了。Tikhon Jelvis 解释道，因为在前端已经对循环进行了有限步展开（Unrolling），语言中不再包含循环结构，整个语法被精炼至仅仅两三种基础结构，使得命令编译器变得异常短小纯粹。 --- ### [29:33](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1773s) 有界模型检验（BMC）与时态逻辑不变量验证 在将程序编译为 Z3 公式后，Tikhon Jelvis 探讨了该公式的用途。除了可以充当低效的解释器（用于自检公式正确性）或“反向解释器”（根据输出反推输入，类似于一种小魔术）之外，真正实用的工业级场景是有界模型检验（Bounded Model Checking, BMC）。 在 BMC 中，验证者利用时态逻辑（Temporal Logic）描述程序的状态不变量。时态逻辑的本质是将程序性质关于时间进行量化： - **安全属性（Safety）**：“某个条件在所有时刻都必须始终为真（Always True）”。 - **活性属性（Liveness）**：“某个条件最终必然会变为真（Eventually True）”。 在经过展开的程序模型中，“时间”被离散化为变量的版本切片序列（如 $x_1, x_2, x_3, \dots$）。因此： - 表达“始终为真”（$\square P$），直接编码为对每一轮迭代中该断言的全局逻辑与（Big AND，即 $P(x_1) \land P(x_2) \land \dots$）。 - 表达“最终为真”（$\lozenge P$），则天然对偶地编码为逻辑或（Big OR，即 $P(x_1) \lor P(x_2) \lor \dots$）。 “从本质上讲，这个量词——如果我们说 $X$ 始终为真，就意味着它在循环的每一次迭代中都为真；而既然我们已经把循环展开了，我们只需把这个量词附加到每一个单独的步骤上即可。” --- ### [31:52](https://www.youtube.com/watch?v=ruNFcH-KibY&t=1912s) 等价性验证与反例驱动的程序合成（CEGIS） 基于 SMT 公式，另一个杀手级应用是**程序等价性验证**。要验证优化前后的两个程序是否等价，标准的做法不是证明它们相等，而是**断言它们的输出不相等**（Assert $Output_A \neq Output_B$）并交由求解器求解： - **求解成功（Satisfiable）**：说明存在某组输入使得两个程序的输出不一致，求解器给出的赋值模型直接构成了**反例（Counterexample）**，暴露出程序缺陷。 - **求解失败（Unsatisfiable）**：说明不存在任何使输出相异的输入，即从数学上证明了程序在展开深度内是完全正确的。 Tikhon Jelvis 指出：“坦白说，这在一开始是有点反直觉的，因为通常人们习惯于‘公式可满足’意味着结果是正确的，但在这里情况恰恰相反。” 这种反例生成机制进一步催生了**程序合成（Program Synthesis）**与**超优化（Superoptimization）**。通过对 AST 的指令和表达式进行符号化编码，利用反例引导的归纳合成（CEGIS）技术，可以从规范自动生成最优代码： ```mermaid flowchart TD accTitle: CEGIS Loop accDescr: Counterexample-Guided Inductive Synthesis loop between the synthesizer and the verifier. A["输入规范与当前 I/O 测试用例集"] --> B["SMT 求解器合成候选程序"] B --> C{"验证器检查:<br/>候选程序是否等价于规范?"} C -- "不满足 (SAT): 发现错误" --> D["提取输入反例<br/>(发现新的边缘情况)"] D -->|"加入测试用例集"| B C -- "满足 (UNSAT): 验证通过" --> E["输出最终证明正确的程序"] ``` - **初始生成**：给定极少量的输入输出对（哪怕只有一组），求解器快速合成一个候选程序（此时极有可能存在漏洞）。 - **验证对抗**：将候选程序提交给验证器。验证器通过寻找不相等的解，找出一个导致候选程序崩溃的临界反例（Edge Case）。 - **迭代剪枝**：将新反例加入条件集合，重新触发合成。虽然合成在计算上很繁重，但由于每个反例都精准切中一个边界条件，实际迭代只需极少轮次便能快速剪除绝大部分无效搜索空间。 - **超级优化**：直接向求解器下达指令：“这是原程序，寻找一个指令更少、速度更快的等价程序”，由 SMT 求解器自动挖掘出人类难以察觉的代码极致优化。 ### [34:15](https://www.youtube.com/watch?v=ruNFcH-KibY&t=2055s) 基于 SMT 的程序优化与草图合成（Sketching） Tikhon Jelvis 指出，直接利用求解器进行优化在速度上确实很慢，因此在现实场景中，不可能用它来直接优化大规模程序。但开发者可以采取一种折中方案：利用一个类似于窥孔优化（peephole optimization）的微小滑动窗口（sliding window）来局部优化代码。令人意外的是，以这种方式构建优化器，反而比编写像 GCC 这样经典的优化编译器要简单得多，因为它所要求的领域专长（domain expertise）门槛极低。Tikhon 分享了自己的亲身经历：他曾在一个使用该方法进行优化的编译器项目上工作过，坦言自己绝不可能徒手编写出所有繁琐的优化重写规则；他对目标硬件架构的理解程度仅限于能够编写模拟器，根本不足以手写高效的底层代码。但这完全不是问题，因为在这个体系中，“我们需要的仅仅是一个公式编译器”。 除了程序优化之外，应对“无法处理大规模程序”这一瓶颈的另一个经典策略是“草图合成”（Sketching）。在实际开发中，程序员通常清楚代码的整体骨架——知道哪里需要一个循环、哪里需要一个分支条件、应该调用哪些变量，但往往拿不准边界细节。草图工具允许程序员写下带有“漏洞/挖空”（holes）的代码骨架并附带断言，随后由合成器自动填充剩下的细节，使其满足预设断言。加州大学伯克利分校（UC Berkeley）曾为类 Java 语言开发过类似的编译器草图工具；而 Tikhon 重点提到了一个名为 Synquid 的项目，该项目基于细化类型（refinement types，类似于 Liquid Haskell），允许开发者仅凭函数的细化类型签名就自动合成出函数体实现。 ```mermaid flowchart TD accTitle: Sketching and Synthesis Flow accDescr: 程序员编写带有挖空和断言的程序草图，SMT 求解器在此基础上合成满足断言的具体代码。 subgraph Input["开发者输入"] A["程序骨架 / 草图<br/>(保留 Holes)"] B["规范约束 / 细化类型<br/>(Refinement Types)"] end subgraph Engine["求解与验证"] C["SMT 求解器 / 合成引擎<br/>(如 Z3 / Synquid)"] end subgraph Output["最终产物"] D["填补完整的可执行代码"] end A --> C B --> C C --> D ``` - 经典编译器（如 GCC）依赖大量手工编写的重写规则与深厚的硬件架构经验；基于 SMT 的局部优化仅需硬件的形式化语义规范。 - Synquid 展示了通过类型驱动进行代码合成的前沿方向，用户甚至可以在线试玩其基于细化类型的合成效果。 --- ### [36:27](https://www.youtube.com/watch?v=ruNFcH-KibY&t=2187s) 交互式工具、测试生成与领域特定语言（DSL）的优势 程序合成与 SMT 技术的应用场景远不止于优化。Tikhon 认为最有趣的领域之一是构建辅助日常编码的交互式工具，例如并发建模，或者在开发者还在敲代码的阶段就实时提供执行轨迹（execution trace），这正是“天使式编程”（Angelic Programming）的核心思路。此外，SMT 求解器是极佳的调试辅助器与测试用例生成器。在生成测试用例的场景下，求解器的耗时几乎无足轻重：“你生成测试用例花多长时间根本无所谓，因为你只需要生成一次，之后就能按需运行这套测试套件无数次。”即便跑出完整测试集需要耗费数小时乃至数天，每次改动代码时回归测试能够飞速执行才是最关键的。 然而，Tikhon 强调了一个残酷的现实：如果想为一门完整的通用编程语言（General-Purpose Language）构建上述全套工具，“那几乎等同于一个完整的科研项目，很可能会产出多篇学术论文”。通用语言体量庞大且充满各种历史遗留包袱和边界情况，工程难度极高。相比之下，在领域特定语言（DSL）上构建 SMT 求解工具则可行得多。DSL 通常具备以下关键优势： - **语法与规模小巧**：语言构造精简，极易形式化。 - **天然具备有界性**：许多领域根本不需要无界循环（unbounded looping），也不需要图灵完备性（Turing completeness），使得有界模型检验（bounded verification）能够达到媲美全量证明的实用效果。 - **设计者心智负担低**：DSL 的设计者往往对其语义细节了如指掌，远胜于对复杂通用语言的理解。 Tikhon 提到自己最初是在伯克利的一门程序合成课程上接触这些内容的，尽管授课教授后来调任其他学校，但课程幻灯片和资料依然在线可查。他在个人网站（yelv.is/talks/compose-2016）上也整理了演讲幻灯片与相关论文链接，并邀请周末参加 Unconference 的同行一起上手体验 SMT 求解器。 --- ### [39:50](https://www.youtube.com/watch?v=ruNFcH-KibY&t=2390s) 问答环节：Forth 编译优化、安全利用与非线性算术的边界 在问答环节，有听众首先询问：在讲座中展示的那个通过迭代寻找反例来合成程序的循环机制中，具体输入了什么样的问题或规范？Tikhon 回答道，在他实际参与的一个为奇特硬件架构编写编译器的项目中，规范本身就是用一种底层 Forth 变体语言编写的程序。通常人们认为规范必须是某种高阶逻辑公式，但他们“直接把朴素编译到 Forth（或者该 Forth 的古怪方言）的代码片段当作规范，用来寻找执行速度更快的替代指令”。 随后，一位安全领域的听众提出，逆向解释器（reverse interpreter）在安全漏洞挖掘中大有可为，例如面对复杂的字符串处理逻辑时，已知期望的 Payload 结构，反推输入端应该如何构造。Tikhon 认同其实用价值，但指出这正是求解器性能难以预测（unpredictable performance）的痛点所在：“反向运行程序在本质上显然比正向运行程序要困难得多。”实践中往往存在一种不对称性：如果存在某种输入能够产生指定输出，求解器通常能极其迅速地把它搜出来；但如果想要彻底证明“不存在任何可能的输入”，算法就会陷入泥潭，耗时完全取决于循环展开深度和程序复杂度。不过在工程安全场景下，完全可以退一步放弃 100% 形式化证明：直接设定运行 10 分钟超时，能找到反例就是胜利，找不到反例就暂且默认安全。 针对听众关于代数几何、圆柱代数分解（Cylindrical Algebraic Decomposition）与条件分支的数学讨论，Tikhon 澄清了讲座中代码的技术底座： > “我做的一切都仅仅使用了位向量（bit vectors），这意味着它们只是 32 位的值；虽然求解器确实支持无界整数，但它们求解整数方程的判定过程完全不同，且具有截然不同的性能保证。” 对于位向量公式，在给定边界下通常能够保证在有限时间内给出结论；而一旦引入无界整数和非线性运算，逻辑很快就会滑向不可判定（undecidability）的深渊。因此，系统通过设定最大循环迭代次数 $X$ 来进行有界验证，从设计原则上就已经主动放弃了对绝对完备性（100% promises）的执念。 ## Notable quotes > [39:50](https://www.youtube.com/watch?v=ruNFcH-KibY&t=2390s) 反向运行程序在本质上显然比正向运行程序要困难得多。 — Tikhon Jelvis > [36:27](https://www.youtube.com/watch?v=ruNFcH-KibY&t=2187s) 你生成测试用例花多长时间根本无所谓，因为你只需要生成一次，之后就能按需运行这套测试套件无数次。 — Tikhon Jelvis > [14:59](https://www.youtube.com/watch?v=ruNFcH-KibY&t=899s) 作为一个粗略的经验法则，公式越大耗时越长；但如果两个公式结构差异过大，这个规则就完全不适用了。 — Tikhon Jelvis ## Mentioned Tikhon Jelvis, Z3, Compose Conference, Microsoft Research, Haskell, OCaml, .NET, F#, SBV, Liquid Haskell, While 语言, Imp 语言, QuickCheck, GCC, Synquid, 加州大学伯克利分校, Forth ## Video description Tikhon Jelvis C◦mp◦se :: Conference http://www.composeconference.org/ February 5, 2016 SMT solvers are widely used in research to analyze and verify programs. This lets us check invariants and compare programs against a spec exhaustively, with bounds on the number of loop iterations and the size of the heap. SMT solvers are also useful for other sorts of analysis including sophisticated type checking (like refinement types in Liquid Haskell) and fields other than program analysis (like security research where they can be used to analyze cryptographic algorithms and protocols). I’ll demonstrate how to compile a simple language to an SMT formula and analyze programs using the Haskell Z3 bindings. Z3 has bindings in other languages including OCaml and .NET, so these ideas will be immediately useful to everyone even if the details are slightly different from the Haskell code. The underlying ideas will also help people approach other problems with Z3. [Source](https://www.youtube.com/watch?v=ruNFcH-KibY)

[39:50] Tikhon Jelvis: 反向运行程序在本质上显然比正向运行程序要困难得多。 [36:27] Tikhon Jelvis: 你生成测试用例花多长时间根本无所谓，因为你只需要生成一次，之后就能按需运行这套测试套件无数次。 [14:59] Tikhon Jelvis: 作为一个粗略的经验法则，公式越大耗时越长；但如果两个公式结构差异过大，这个规则就完全不适用了。

[0:12] all right everyone we have our last talk [0:15] of the day it's T cons Elvis with some [0:20] information thoughts about the z3 SMT [0:24] solver all right Thank You T Khan right [0:31] okay so as a few people have noticed [0:35] that there's something of a SMD solver [0:37] sub-theme at the conference this year [0:39] and in some sense my talk is maybe one [0:43] of the more introductory ones to how you [0:45] could use an SMD solver and while I have [0:48] some code in Haskell and it uses z3 none [0:52] of the ideas are specific to either and [0:55] you could use them in any language with [0:57] any SMT solver but first let's again [1:00] review what an SMT solver is so it all [1:06] starts with the boolean satisfiability [1:08] problem which is a classic np-complete [1:12] problem which in practice we can solve [1:15] surprisingly fast for real-world [1:18] instances so there are two things that [1:21] make it interesting one of which being [1:23] that you know we have fast as Sat [1:26] solvers and the other one is that it's [1:28] actually relatively easy to encode [1:31] problems in terms of sat as opposed to [1:34] other np-complete problems and the way [1:38] that is formulated is you have some [1:41] number of boolean variables which are [1:43] ANDed or and you know could be negated [1:47] and the solver tells you whether there's [1:50] any assignment of true and false for [1:52] each variable so that the whole thing [1:54] holds true so it either gives you the [1:57] correct assignment or it tells you that [1:59] it's unsatisfiable or unset when an SMT [2:03] solver does is it extends this idea with [2:06] other kinds of variables so we're no [2:09] longer limited to boolean's but instead [2:11] we could have constraints over numbers [2:13] arrays and other things and the [2:17] advantage here is that it's even easier [2:20] to encode interesting things in terms of [2:25] SM [2:25] than it is in terms of sat in some sense [2:28] you could think of sat as being a lower [2:31] level version of this where you have to [2:33] do everything literally bit by bit where [2:36] SMT lets you do things at a higher level [2:37] and also the solvers have more [2:41] domain-specific insights in the kinds of [2:44] variables they provide letting them [2:45] solve certain problems faster so the [2:50] different theories correspond roughly to [2:52] the different kinds of variables and the [2:54] different sorts of constraints that you [2:56] can express and there's a bunch I mean I [2:58] listed the ones that seemed the most [3:02] easy to understand but z3 has I don't [3:06] know 30 maybe more that there's a lot of [3:08] capabilities and one that's worth what [3:12] like seeing in particular are the fixed [3:15] sized words so like machine words [3:18] basically it's just a sequence of bits [3:21] where z3 also knows how to do the common [3:26] bitwise operations including treating [3:29] them as numbers so addition [3:30] multiplication division for both signed [3:34] and unsigned and the normal boob bitwise [3:38] operations you see in languages and one [3:43] thing that's a pretty recent advancement [3:45] is that sort of built on top of bit [3:47] vectors solvers now support theories of [3:50] floating-point numbers so you can [3:52] actually represent a floating-point [3:54] number as the actual set of bits that it [3:56] is as opposed to trying to approximate [3:59] floating numbers with real numbers now [4:01] that might sound kind of weird because [4:03] normally what we do is we approximate [4:04] real numbers with floating-point numbers [4:06] but as soon as we start caring about the [4:09] correctness of programs it's often [4:11] actually easier to go in the opposite [4:12] direction but with these new with the [4:15] new theory of floating-point we can [4:17] actually model programs with [4:20] floating-point numbers [4:21] completely correctly and I mean I won't [4:25] come back to floating-point numbers in [4:26] this example but it should be clear that [4:29] if you just replace every time I use [4:31] integer with floating-point and we use [4:34] the theory of floating-point numbers we [4:35] could analyze programs depending on [4:37] floats the [4:38] we do the ones the depending on you know [4:40] fixed size integers [4:43] okay so z3 is the specific SMT solver [4:46] I'm talking about and it tends to be the [4:50] default SMT solver everybody goes to [4:52] first usually unless they have a good [4:54] reason they're probably going to depend [4:56] on z3 because it has a sort of sterling [4:58] reputation and a lot of different [5:00] theories for a long time it was sort of [5:04] relegated to academic research because [5:07] Microsoft released it under a very [5:09] restrictive license but I think was this [5:12] year or last year they released the [5:15] entire solver under an MIT license which [5:17] means you're free to use it for whatever [5:19] you like including commercial [5:21] applications and it has API bindings [5:24] that are useful too I imagine everybody [5:27] in the room like I'll be using a package [5:30] in Haskell but it also has an O camel [5:32] API as well as one in c-sharp which [5:35] presumably you could just reach out to [5:37] in F sharp as well [5:39] okay so Haskell has well it has multiple [5:43] packages for working with SMT solvers [5:45] but the two that I'm familiar with are [5:47] SBV which is a sort of high-level DSL [5:50] which supports multiple solvers and then [5:52] the Haskell d3 bindings which are z3 [5:55] specific and expose certain capabilities [5:58] that SBT doesn't so if you just want to [6:01] experiment with SMT SBV is a great place [6:04] to look but I think if you're building a [6:06] tool or you need to integrate closely [6:08] with z3 the z3 bindings are more [6:10] interesting so the example code [6:13] I'll have later and the example code I [6:15] haven't github for this talk uses the z3 [6:18] bindings and is specific to z3 okay so [6:22] the main thing I'm going to talk about [6:25] is how we can take a program and compile [6:29] it to an SMT formula then once we've got [6:33] the program as an SMT formula we could [6:36] use the solver to answer all sorts of [6:39] questions about it so the first thing to [6:42] ask in in a formula is what do the [6:45] variables represent and the main are [6:50] encoding separates [6:52] essentially three groups we have one set [6:55] of variables for the inputs to the [6:56] program we have a set of variables for [6:58] the outputs like what the result is and [7:00] also a set of variables for every single [7:02] intermediate state that the program goes [7:04] through so in a sense the formula [7:06] represents a sort of symbolic [7:08] computation trace through the entire [7:11] program so a good way of thinking about [7:14] it is that by solving this formula we [7:17] can make statements about all possible [7:19] computation traces that your code can [7:21] take and you can see why this would be [7:23] very powerful [7:24] unfortunately the downside is that [7:27] actual programs can take a lot of [7:30] different traces and sometimes they can [7:31] loop forever so we can't actually handle [7:35] things like loops directly which means [7:38] that we have to find some way of [7:40] encoding a loop in a way that you know [7:43] that is that an SMT solver can handle [7:48] and the specific technique I'm going to [7:50] describe is bounded so we basically say [7:53] loops are difficult so we're just going [7:55] to arbitrarily max you know bound loops [7:57] at say a thousand iterations or ten [7:59] thousand iterations and then just unroll [8:01] them so in essence we just completely [8:04] skip the question of loops altogether of [8:08] course if you're interested in doing [8:10] something else [8:11] you can mix this approach with say some [8:14] preset loop invariants and have a [8:16] different way of analyzing loops but as [8:18] soon as you get to allowing programs [8:21] that have Arbit you know arbitrary [8:22] looping you hit the limits of sort of [8:26] turing completeness and Rice's theorem [8:28] where there are all these questions [8:30] which you just fundamentally can't [8:33] answer and bounded verification lets you [8:36] trade off the fact that you have this [8:39] arbitrary limit for the fact that you [8:40] can sort of create you know treat any [8:42] sort of program without worrying about [8:44] these things okay and so we have this [8:48] formula and we have our variables that [8:49] are inputs intermediate States and [8:51] outputs and the easiest thing we could [8:53] do is we could fix the outputs and then [8:56] we can solve for the inputs and the [8:57] intermediate races or sorry other way [9:00] around [9:00] we can fix the inputs and solve for the [9:03] outputs which just gives us a normal [9:04] interpreter [9:06] and yet since this is just a normal [9:09] logic formula there's no directionality [9:11] inherent to it and we can solve for any [9:13] set of variables you care about so if we [9:16] fix the outputs and solve for the inputs [9:18] we get a reverse interpreter and it by [9:23] its nature the reverse order has to be [9:25] non-deterministic like there's multiple [9:27] possible input states that give a given [9:29] output and the SMT solver can handle [9:31] this and you can just get either all the [9:35] possible solutions or the solutions one [9:37] at a time and then we can also actually [9:40] look at the intermediate states of the [9:43] program if we have some invariant that [9:46] we want to hold we just add an extra [9:48] constraint and an extra assertion to [9:51] every single state that the program can [9:53] can assume which then lets us solve for [9:58] whether the invariant is always true or [9:59] in which cases it breaks down and we can [10:02] actually use this approach for bounded [10:04] verification where we have some [10:06] specification like say another program [10:09] that we know or believe to be correct [10:11] and we can ensure that it always gives [10:14] the same output for the same input as [10:16] another program and this is another way [10:23] of thinking about this in particular is [10:24] it's sort of like a symbolic quick check [10:26] where with quick check we have our [10:28] little specification and we just [10:30] randomly generate tests and hope to hit [10:32] hit one that fails if there is a failure [10:35] here we have the same idea of having a [10:38] specification as a program but we [10:41] actually use the solver to symbolically [10:42] test every single possible input and [10:44] every single possible output okay so [10:48] I'll go through a sort of slightly [10:52] detailed explanation of how you would [10:55] convert a program to a formula and the [10:58] first question is you know what language [11:01] are you using and obviously the bigger [11:02] the language the more difficult it will [11:04] be to write a formula compiler so I [11:07] chose the smallest language I knew of [11:09] which is it and if anyone's taken a sort [11:13] of programming language Theory course [11:14] this is the language that's classically [11:16] used to teach about operational [11:18] semantics because it [11:19] operational semantics are as simple as [11:21] possible another way to put it is that [11:23] this is an imperative language for which [11:25] it's as easy to write an interpreter as [11:28] possible while still being at least [11:30] somewhat interesting and this makes it a [11:34] good choice for writing a formula [11:36] compiler because in a sense the formula [11:39] compiler compiles the operational [11:42] semantics of a language into a sort of [11:44] logic that's understood by the logic [11:46] solver so the simpler we can make it [11:49] the simpler the formula compiler and the [11:51] easier our job will be okay and so the [11:55] language itself has sort of two pieces [11:56] it has expressions which can be numbers [11:59] or can be boolean's and the expressions [12:02] can't have any side effects all they do [12:04] is they value it to a value and the [12:07] variables for the for simplicity are [12:09] always int and in my case they're always [12:13] 32-bit wide integers and then we we have [12:17] commands which have side-effects but [12:19] don't value to a value so all they ever [12:21] do is change the state and here we have [12:24] assignment we have while loops if [12:26] statements and waste a sequence sequence [12:30] commands together so normally AMP is [12:34] presented defined as a sort of abstract [12:38] grammar so here we have the arithmetic [12:40] expressions and you know we have [12:42] variables we have literal numbers and we [12:45] have all the usual arithmetic operators [12:47] that you're used to but the really nice [12:52] thing with using a language like Haskell [12:54] or oh camel or f-sharp is that it is [12:58] really really straightforward to [13:00] translate these apps our grammars into [13:03] types in fact it's so straightforward [13:05] it's almost pointless to show the two [13:07] except to show that they're kind of [13:09] exactly the same I mean if you were sort [13:12] of you know back in the day when people [13:14] only use ASCII and you have to write out [13:15] this grammar it would look almost [13:18] exactly like this I mean the one weird [13:22] thing for non high schoolers is that the [13:25] last four constructors the plus the [13:27] minus and so on are all in fix so just [13:30] like you can define custom in fix [13:32] operators [13:33] by using special symbols for your [13:35] function names you can define in fixed [13:37] constructors so the Earthmen expressions [13:40] look like this the boolean expressions I [13:43] mean you could figure out what they are [13:45] but they're really not very important [13:46] here and then finally we get the [13:48] commands now the grammar for commands is [13:52] still pretty straightforward it still [13:55] has the four constructs I mentioned as [13:56] well as skip which we use to have you [14:00] know empty blocks so empty if statement [14:02] branches for example and the main reason [14:05] it's useful to look at the type is [14:07] because all the code from here on out is [14:10] going to sort of follow the type at the [14:11] shape of the type here so all the code [14:15] is going to pattern match and do [14:18] different things depending on which [14:20] construct it is and the way I like to [14:23] visualize this is that the type is a [14:25] sort of skeleton and the code is a sort [14:28] of layer of skin which we lay on top of [14:30] the skeleton and it naturally assumes [14:32] that the shape that the types provide [14:34] and this means that our problem is [14:39] immediately broken up into a whole bunch [14:42] of small pieces so instead of trying to [14:44] compile the whole language we now have [14:46] the problem of compiling skip and the [14:48] problem with the compiling set and the [14:50] problem providing seek and so on all [14:52] separately and this actually makes the [14:55] entire effort a lot more tractable ok [14:59] and so to convert to a formula there are [15:01] basically three steps the first one is [15:03] in lining all our functions now I mean I [15:06] didn't talk about functions here and the [15:08] main reason is because after you inline [15:10] them we could just pretend we didn't [15:11] have any then we unroll all our loops [15:14] and we transform it into SSA which is [15:18] single static assignment style I'll go [15:22] into what that means in the next slides [15:23] but so inlining again if we had [15:27] functions basically all we do is we [15:29] create fresh names and then paste the [15:31] function body in to where it was called [15:34] so this is sort of how the C [15:37] preprocessor works except I think it [15:40] doesn't even great fresh names so as you [15:42] can imagine but [15:45] the biggest advantage of inlining of [15:47] course is that our formula doesn't have [15:49] to know anything about functions we can [15:51] forget about function names and it's [15:53] just as if it was all straight line code [15:54] and obviously you could run into the [15:57] problem of recursion but just like we're [16:00] going to have an arbitrary bound on the [16:02] length of our loops we would just have [16:04] an arbitrary bound on like how far we're [16:06] willing to recurse okay yes so that's [16:13] sorry yeah so the second step is [16:15] unrolling loops where basically we take [16:18] a loop in the form of while X something [16:20] and we just turn it into a whole bunch [16:24] of nested if statements and [16:27] realistically you know each loop is [16:30] going to be unrolled to maybe a hundred [16:32] maybe a thousand steps depending on your [16:34] application so if you actually took the [16:36] program and you printed it out it would [16:38] suddenly become very long but luckily [16:41] the SMT solvers are fast enough to [16:45] handle surprisingly large formulas [16:48] although I should make a side note about [16:51] performance is that I mean I've worked [16:53] with SMD solvers for a little while and [16:56] I've worked with people who've spent a [16:57] lot of time years and years using them [16:59] and performance is still a bit of a [17:01] black box I think pretty much for [17:04] anybody who isn't actively implementing [17:05] and SMT solver and maybe even for them [17:08] so it's a bit hard to predict ahead of [17:10] time how long a formula will take as a [17:13] rough heuristic the larger your formula [17:16] the longer but that doesn't actually [17:19] hold if your formulas are too different [17:20] so it's really hard to figure out what [17:24] will run quickly and what won't okay and [17:27] so single static assignment this is the [17:30] part where we really take the sort of [17:34] directionality inherent in executing [17:38] code and transform it translate it to [17:41] the logic layer which has no inherent [17:44] directionality so from the SMT solvers [17:46] perspective the logic formula does not [17:49] happen in any particular order so we [17:53] need some way to structure the formula [17:54] to maintain the order of the program [17:57] and the way we do it is by turning every [18:01] single variable at each time step into a [18:04] new name so if we take X and then we set [18:09] X to something new in the formula we [18:11] would have X 0 and then we would have X [18:14] 1 and we have a constraint that says oh [18:16] X 1 is equal to like X 0 plus a 0 when [18:21] everybody here has taken a compilers [18:23] class you've probably seen SSA before [18:25] because this is an intermediate form [18:27] used by a lot of imperative style [18:31] compilers and it happens to be a really [18:33] good fit for expressing as a formula the [18:37] one tricky part with a single static [18:39] assignment is how to handle if [18:41] statements because here all of a sudden [18:44] we're in a position where depending on [18:46] which branch we take X will have a [18:48] different value and there's no way to [18:51] tell statically which one it will be and [18:54] so at first the solution in real actual [18:58] SSA feels like a bit of a hack but again [19:01] it happens to work well for SMT solving [19:04] but essentially what we do is we after [19:07] we finish with the F statement we create [19:09] a new variable X 3 that basically has a [19:14] magical Oracle function that says oh you [19:16] know if we took the first branch X 3 is [19:19] equal to X 1 and if we took the second [19:21] branch X 3 is equal to X 2 and these are [19:24] traditionally called Phi functions and [19:26] basically let us extract the conditional [19:31] decision part of the if statement into [19:33] our SSA form okay so the next question [19:38] is how do how do we actually compile [19:41] these things and I think especially the [19:43] part with the Phi functions will make [19:47] more sense once we see how they're [19:49] turned into a logic formula for the SMT [19:52] solver but one thing that kind of struck [19:54] me was that the formula compiler looks a [19:57] lot like the interpreter and for most of [20:00] the implementations if you squint it's [20:02] kind of like we're interpreting the code [20:04] in some weird sort of way so for [20:07] comparison I'll just in parallel give [20:10] you [20:11] parts of the interpreter for imp and [20:14] parts of the formula compiler that [20:15] produces the XIII is ast and the set of [20:19] XIII assertions and in both cases just [20:23] like we have three separate types we had [20:25] arithmetic expressions boolean [20:27] expressions and commands we have three [20:29] functions and in both cases we're going [20:33] to keep track of all of our variables in [20:35] in some sort of map a scope and so [20:39] similarly in the interpreter the [20:43] arithmetic expressions and the boolean [20:45] expressions can read variables but they [20:47] can't edit them so all they produce is [20:49] their result which is either you know an [20:51] int or a bool as appropriate and in the [20:54] case of the SMT compiler they actually [20:57] produce fragments of a formula that [20:59] aren't ready to be sent to the solver [21:01] yet they're just sort of like parts of a [21:04] formula which don't necessarily value to [21:07] full constraint so we'll be using these [21:09] ast s to build up a whole constraint [21:12] which you know ultimately can be solved [21:16] and evaluates to you know either true or [21:17] false sat on Sat and the pilot commands [21:20] in the interpreter case all the commands [21:23] can do is they can edit the scope they [21:25] can change variables so we just returned [21:27] the new scope again if this was a more [21:30] complicated language where for example [21:32] commands could have values we'd need a [21:34] lot more plumbing but here for the sake [21:37] of simplicity we just were to always [21:39] return the new scope and similarly for [21:42] the sake of simplicity I'm assuming that [21:43] the programmer is perfect yeah I am so [21:46] fine [21:46] and that nobody ever makes any scope [21:48] errors so I just you know the variable [21:52] is always going to be in scope and so [21:55] finally in the case of z3 once we [21:58] actually run a command we can just [22:00] bundle it as its own assertion and give [22:03] it to the solver so instead of returning [22:05] an ast that needs to be combined with [22:07] other pieces we just assert directly [22:10] which is why the type of the command [22:13] compiler is just a z3 of unit okay so [22:18] the first thing is arithmetic [22:20] expressions so what we want to do is we [22:22] want to compile compile something like [22:24] the expression [22:25] five plus X into an expression which [22:27] says oh you know add two-bit vectors one [22:30] of which is the bit vector literal five [22:32] that's 32 bits wide and one which is the [22:36] variable X 0 32 bits wide and this is [22:40] just one node is that sort of if you [22:42] actually looked at the SMT formula it is [22:44] kind of painfully explicit both about [22:46] what sort of operations you're using I [22:48] mean in this case addition is easy but [22:50] in other cases you have to tell it [22:52] whether it's signed or unsigned and you [22:54] also constantly have to tell it how wide [22:56] literals and variables are and so [23:01] pretend that each of these level [23:06] extracts is part of a large pattern [23:09] matching case statement that matches on [23:12] the structure of an arithmetic [23:14] expression so in the case of an [23:16] interpreter if we see a literal we just [23:18] return that number in the case of the Z [23:23] 3 formula compiler if we see a literal [23:25] we just make a 32-bit bit vector with [23:28] that size so we just produce a literal [23:30] formula similarly in the case of the [23:33] scope it's actually exactly the same [23:35] because we're keeping track of the [23:37] variables in both cases it's just that [23:40] in the original case the scope has Imps [23:42] so we just give it the final value in [23:44] the case of Z 3 the scope has sort of [23:46] symbolic variable names that the solver [23:48] knows about and we just tell it oh use [23:50] this the symbolic variable and then [23:53] finally to do something like plus in the [23:55] interpreter case we just recurse [23:57] directly and in the Z 3 case it's a [24:02] little bit more difficult because [24:03] everything is being managed by the Z 3 [24:06] type which happens to be a monad so we [24:08] have to sort of explicitly extract the [24:11] results of the two recursive calls and [24:13] then make an addition node in our [24:17] formula so also just for a note these [24:25] little unicode subscripts are totally [24:27] valid haskell so you could actually use [24:28] names like this in your code and you can [24:32] configure Emacs to make it easy to type [24:33] and then all non Emacs users will hate [24:35] you but they had it coming [24:39] okay so well I actually have that the [24:43] rest of the expressions both arithmetic [24:45] and boolean's are basically the same [24:47] thing except instead of making an [24:48] addition node you might make a [24:50] subtraction node or you know instead of [24:52] making a literal number you make literal [24:53] boolean but the shape and the structure [24:56] of the code is exactly the same okay so [25:00] the sort of commands are a bit more [25:03] interesting because they're the ones [25:04] that actually change the state and the [25:08] way we do this is by you know extracting [25:11] each command is it into its own [25:12] assertion and at the end d3 gathers up [25:15] all the assertions and makes one big [25:17] formula so conceptually this is the same [25:21] as making a big formula full of and but [25:25] we just let z3 take you know simplify [25:28] the the process a little bit and give it [25:30] the assertions piece by piece I mean [25:33] this is also nice because of a future [25:35] somebody mentioned in the previous talk [25:37] called incremental solving where once [25:40] we've solved the problem with some [25:43] number of constraints we can actually [25:44] add new constraints and the solver can [25:47] resolve it still taking advantage of all [25:50] of its previous internal states and this [25:52] lets us sort of refine our formulas [25:54] without a big performance penalty we can [25:57] take a formula and add constraints [25:58] without having to redo it every single [26:00] time and so in the case of the [26:06] imperative assignment statement were set [26:09] in my type we just now create a new [26:12] variable x1 and assert that it's equal [26:15] to the right hand side and the right [26:17] hand side of course is compiled exactly [26:20] the same way it was in this previous [26:22] previous example okay and so in the [26:27] interpreter all we do is we update the [26:29] scope so the in the formula compiler is [26:37] a little bit more complicated because [26:38] we're only really maintaining the scope [26:40] for our own use so we also have to you [26:43] know create a new variable in d3 and add [26:47] the new assertion so there are actually [26:49] three sort of [26:51] these three operations that we do we [26:53] create a new variable and this is a [26:56] really convenient feature where we just [26:58] give it a name and tell it to make a [27:00] fresh variable which is kind of like a [27:02] new variable with the same name that's [27:04] distinct from all the other ones so this [27:06] keeps us from having to manually keep on [27:09] updating a counter and calling things x1 [27:11] x2 etc and then again for the actual [27:15] Equality assertion so here the he will [27:17] sign we have to make you know explicitly [27:20] make the Equality note in the ast and [27:23] finally we just use Z 3 Z 3 dot assert [27:26] to sort of feed it to the solver and add [27:29] it to the set of assertions that we're [27:31] solving and then finally we update the [27:33] name in our scope so the reason we're [27:36] keeping an explicit map as part of our [27:38] formula compiler is so that all these [27:40] fresh variables are mapped back to a row [27:43] name so by doing this we just let Z 3 [27:45] take care of the ab making variables [27:49] fresh ok and then if statements so these [27:52] are the tricky ones and basically the [27:56] reason the five functions made sense in [27:59] SSA is that Z 3 actually has something [28:02] akin to a Phi function where you give it [28:05] a condition so whatever condition was in [28:07] the if statement goes into the [28:09] expression and then it just you know [28:12] solves to the condition and chooses the [28:14] appropriate one so in a sense this is [28:16] like a symbolic way to do an if [28:18] statement and in the sort of oh so this [28:22] slides a bit different because if [28:24] statements look completely different [28:25] than the interpreter case in the [28:28] interpreter case we just like you know [28:30] branch and do the right thing whereas in [28:32] the Z 3 case we have to compile we [28:33] always compile both branches because all [28:36] the branching happens to Bala Klee and [28:38] so the way we do it is just you know we [28:42] recursively compile both branches and [28:46] then after that we add a sort of a Phi [28:51] function for every single variable that [28:53] got changed and as it happens these [28:56] functions in Z 3 are called itës [28:59] which stands for if-then-else so really [29:02] all this expression is saying is that if [29:04] the condition is true we took [29:05] a if the condition is false we took [29:07] branch B and then the solver handles you [29:09] know all the difficult lifting [29:11] symbolically okay so you'll notice I [29:15] skipped loops and that's because after [29:16] unrolling we don't have any loops so [29:18] we've actually made the language [29:19] significally simpler and went down to [29:21] like what three constructs so that [29:25] really was more or less the whole [29:26] compiler i skipped some some of the [29:30] parts for expressions but the commands [29:31] are all there and now that we have a [29:33] formula for a program the question is [29:35] you know what can we do with it and as I [29:38] mentioned earlier we could use it as an [29:39] interpreter which it's kind of pointless [29:42] because it would just be slower but it's [29:44] nice to be able to test that our formula [29:46] actually makes sense we use is a reverse [29:49] interpreter in a reverse interpreter [29:51] which is something of a parlor trick [29:53] more than being useful but we could also [29:55] start checking invariants and this is a [29:58] technique called bounded model checking [30:01] yeah we're basically we just specify an [30:07] invariant into polar logic so to borrow [30:11] logic lets us take some property of a [30:14] program say or a program state and [30:16] quantify it over time so we can say that [30:19] oh we have this property here and it's [30:21] always true or we have this other [30:22] property and it has to eventually be [30:24] true and I mean depending on the logic [30:26] you use our other operations and among [30:29] other things this is a very natural way [30:31] to encode safety and liveness properties [30:34] for concurrent programs which I won't [30:37] get into and so the main part with [30:40] temporal logic is that the logic itself [30:42] is implicitly quantified over time and [30:45] usually when it's formalized time is [30:48] like a set of natural numbers so in our [30:51] case all the time is is the different [30:53] sort of slices of like X 1 X 2 X 3 X 4 [30:56] so whenever we say that something is [30:58] always true it just means that we run [31:00] the predicate through and we just have a [31:02] big end stage where it says oh this is [31:04] true for x1 and this is true for x2 and [31:06] this is true for x3 and so on I mean [31:09] there's a bit of bookkeeping to deal [31:11] with conditions again but that's the [31:12] core idea and then of course the [31:14] eventually true it's often is like [31:19] just turns it in or so like it was true [31:22] at some point so it's also nice to note [31:25] how these two operators are duals and [31:27] then when we encode them they naturally [31:30] encode as and and/or which are also sort [31:32] of dual in nature yeah right [31:38] but essentially the quantifier like if [31:41] we say that X is always true we're [31:43] saying it's true for every iteration of [31:44] the loop and now that we've unrolled the [31:46] loop we just attack the quantifier to [31:48] every single step okay so the next part [31:52] is that we can actually verify programs [31:53] against each other and basically we take [31:57] the the output and we assert that the [32:00] outputs are not equal and then we solve [32:03] it and if we've solved it that means [32:05] that the programs are different [32:06] something is wrong and we get the input [32:09] that caused the mistake so we get a sort [32:10] of counter example and if you can't [32:12] solve it that means the program is [32:13] correct honestly this is a bit confusing [32:16] at first because normally used you're [32:18] used to the fact that something is [32:20] satisfied means the result was true but [32:23] here it's exactly the opposite okay so [32:27] once we have verification another thing [32:30] we can do and sort of the first place [32:34] that I ended up using an SMT solver was [32:36] to actually synthesize synthesize [32:38] programs so with a bit more clever [32:40] encoding we can actually create [32:42] variables that represent sort of parts [32:44] of the program [32:45] so like expressions or instructions or [32:47] what have you [32:47] and by fixing the inputs and the outputs [32:51] we can have the SMT solver find a [32:53] program that actually satisfies the the [32:55] input/output pair and the way we take [32:59] this from just salt like solving for a [33:02] single pair or multiple pairs to solving [33:04] for a general program is by verifying it [33:06] against some specification and the way [33:09] this works is we take one input output [33:11] pair we solve it we get a program now [33:13] since we only gave it one pair the [33:15] program is probably wrong so we run it [33:17] to the verifier the verifier tells us [33:19] well this is wrong here's a counter [33:21] example so we take the counter example [33:23] and we put it back in the synthesizer [33:24] now we have two points so we synthesize [33:27] that we find the program that works for [33:29] both of those points and then we go back [33:31] to the verifier now [33:32] first it seems like this might take a [33:34] long time and it does take a long time [33:36] but the important part is that it takes [33:40] far fewer steps through the verifier [33:42] than you would think because [33:44] conceptually each time we find a counter [33:46] example we found a new edge case in the [33:49] algorithm and so it turns out that we [33:52] can quickly prove the the search space [33:53] in only a few input-output pairs for [33:56] most programs okay and so one way to use [34:01] this is to just optimize code so we in [34:05] some sense this is like the most direct [34:08] way to optimize something because we say [34:10] well here's a program find a faster one [34:12] and then the solver finds one and so [34:14] this is great [34:15] as I mentioned it's slow so [34:17] realistically you won't be optimizing [34:19] large programs but you could for example [34:22] optimize programs with a little sliding [34:24] window so vaguely similar to peephole [34:26] optimizations and turns out that it's [34:29] actually easier to write an optimizer [34:31] this way than it is to write a classic [34:34] optimizing compiler like GCC because it [34:36] requires a lot less domain expertise and [34:39] I mean I can actually sort of say this [34:42] confidently because I worked on a [34:43] compiler that use this to optimize and [34:45] there's no way I could have written all [34:48] the rules by hand and in fact like I [34:51] understood the architecture we were [34:52] compiling - well enough to like simulate [34:54] it but not well enough to write real [34:56] programs by hand but that was that was [34:58] totally fine because all we need is a [35:00] formula compiler yes exactly [35:06] but of course optimization isn't the [35:09] only thing we could use some business [35:10] for another way to handle the fact that [35:13] we can't deal with large programs is [35:16] this approach called sketching where [35:18] essentially the idea is that a [35:20] programmer often knows most of what they [35:22] want they know the shape of the code [35:24] they know that they'll need a loop here [35:26] a condition here these variables here [35:28] but they don't know all the details and [35:30] but we can actually write tools which [35:33] lets you write a program leave a bunch [35:35] of holes and have you know add some [35:37] assertions and have the synthesizer just [35:39] fill the rest of the program in for you [35:41] in a way that satisfies those assertions [35:43] and so there's an [35:46] existing compiler from Berkeley that [35:47] does it for a Java like language but [35:49] that's not not all that exciting but I [35:51] recently stumbled across a project [35:54] called sync wit which uses refinement [35:57] types so like liquid Haskell but in a [36:01] language that's not quite Haskell and [36:03] then lets you synthesize the [36:05] implementation of functions just based [36:07] on their refinement type so and like you [36:12] can actually go and play around with it [36:14] online so that I'll have a well I don't [36:17] have a look on my slides but it's worth [36:19] just checking it out and at some point [36:21] you know you might expect to see this [36:23] for Haskell se and then there's all [36:27] sorts of other things that you could do [36:29] with this sort of technology one that I [36:33] think is particularly interesting is [36:36] creating interactive tools that can help [36:38] help a programmer as their programming [36:41] so one idea is to use this to you know [36:47] model concurrency perhaps or actually [36:50] like give you execution traces even [36:53] potentially if a program that you're [36:54] sort of in the process of writing which [36:57] is the idea behind this technique called [36:59] angelic programming and in general you [37:01] could use SMT solvers as debugging aids [37:04] you can use them to generate test cases [37:06] and that particular one is a good [37:08] approach because you don't care how long [37:11] it takes you to generate test cases [37:12] because you do that once and then you [37:15] can run the actual test cases as many [37:16] times as you like so even if it takes [37:18] you a few hours or days to generate you [37:20] know that your test suite all that [37:23] really matters is how fast the test [37:24] suite runs you know each time you make a [37:26] change the code and then I imagine [37:29] there's a lot of interesting stuff with [37:31] synthesis powered code completion sake [37:34] actually like infer what the programmer [37:35] wants to do and you know give him and I [37:40] think one of the most important insights [37:43] though is that pretty much everything I [37:45] listed for a full blown language would [37:48] be a research project and likely [37:51] multiple research papers and in fact [37:53] some of these tools exist for languages [37:55] but the problem is real languages are [37:58] big they're kind of messy and [37:59] going to work with but if you have some [38:02] sort of domain-specific language you're [38:04] in a much better position to build tools [38:07] on top of an SMT solver because doing [38:10] specific languages tend to be much [38:12] smaller and they're also often bounded [38:14] by their very nature a lot of domains [38:16] don't need unbounded looping they don't [38:19] need Turing completeness so you might [38:21] actually have domain-specific languages [38:23] where something like bounded [38:25] verification is you know as good as you [38:27] would want it [38:29] and of course presumably you as a [38:31] programmer understand a domain-specific [38:33] language that you designed way more than [38:36] you understand whatever general purpose [38:38] language you're using just because again [38:40] general-purpose languages are really [38:42] really complicated anyway I picked up [38:45] all of the stuff at first by taking a [38:48] program synthesis class at Berkeley and [38:51] while I don't I doubt it'll be offered [38:54] any longer because the professor moved [38:56] to different University all the [38:57] resources are still available online and [39:00] you can see the slides and a lot more [39:02] details on different techniques for [39:05] program synthesis specifically and that [39:07] also I have a links to my slides and a [39:11] whole bunch of papers on my website at [39:14] job that is talks composed 2016 which [39:18] you know if you really want to dive into [39:20] it I will give you a good starting point [39:22] to see different you know different ways [39:25] people use SMT solvers use synthesis do [39:28] bounded verification and so on and you [39:31] know finally I think I'll be at the [39:34] unconference [39:35] this weekend so if anyone's interested [39:36] in you know playing with SMD solvers I'd [39:39] be happy to help or to guide you in the [39:42] right direction okay [39:50] okay I was just wondering when you [39:52] showed that you know have that iterative [39:55] procedure used to generate a program [39:57] started find the case we're on work and [39:59] then several what were some of the [40:01] problems you gave it or specifications [40:04] so like the one project where I use this [40:08] approach was a compiler for a weird [40:11] weird architecture and the [40:14] specifications were programs in this [40:18] sort of low-level force and like we used [40:23] it to optimize them so when like [40:25] normally when you think specification [40:27] you think some sort of high-level logic [40:28] but here we just literally took [40:30] fragments that we naively compiled to [40:33] fourth or this really weird dialect to [40:36] fourth and use them as a specification [40:38] to find faster ones okay somebody else [40:42] or a awesome talk by the way I had so [40:46] when you were talking about reverse [40:48] interpreters not being as useful I an [40:50] example popped into my head for like I [40:53] work in security so actually would be [40:54] really awesome if I could take like a [40:56] string manipulation language and then [40:58] look you know I know what my exploit [41:00] should look like but what should it look [41:02] at like edit the input like that would [41:04] be really cool yeah so I mean perhaps [41:06] they are useful but this is also one of [41:08] the places where the sort of [41:09] unpredictable unpredictable performance [41:10] comes to bite you because obviously [41:13] running a program backwards is [41:15] fundamentally way harder than running [41:16] the program forwards but one of the [41:20] interesting things it turns out is that [41:21] usually what happens is if there is some [41:24] input that gives you an output it's [41:26] really fast but if you want it to fully [41:28] prove that there's no possible input it [41:31] becomes kind of dicey and depends on [41:32] like how far you unroll your program how [41:35] complicated it is and so on but if you [41:38] don't care about having like 100% [41:40] verification you could just say well I'm [41:43] going to run it for ten minutes and if [41:44] it gives me a counter example it's good [41:46] and if it doesn't well you know it's [41:48] probably fine [41:49] and then yeah okay sure [41:55] comments first place thank you um and [41:58] and and and thank goodness this is this [42:01] is coming down the pike right now [42:02] because you know there's a huge movement [42:04] in this country to force children to [42:06] learn how to program in C [42:08] and and I think this what this will deal [42:11] the deathblow I want one more comment [42:13] okay so so suppose there are no ifs in [42:15] your thing it's got plus and times then [42:18] of course we have algebraic geometry and [42:21] we have the general problem of [42:22] interpolation by a polynomial or maybe [42:25] if it's got division or rational [42:26] function so that's well I'm sure it's [42:29] well known in the field as soon as you [42:30] add an F you then get the cylindrical [42:33] decompositions for the reals and stuff [42:35] like that but but thank you yeah I mean [42:37] also like everything I did just use bit [42:40] vectors which means that they're just 32 [42:42] bits and the solvers do support [42:46] unbounded integers but like the decision [42:48] procedure for that like the way they [42:50] solve equations using integers is [42:52] different and has completely different [42:54] performance guarantees and also like [42:56] with this approach you can often [43:00] guarantee that the formula will finish [43:01] in a finite number amount of time but [43:04] with something like integers you know [43:05] you get into undecidability pretty [43:07] quickly but obviously since we're [43:09] willing to do bounded verification where [43:11] we just arbitrarily say you know we're [43:14] just going to stop after X iterations [43:15] you know we're not giving you 100% [43:18] promises pretty much no matter what okay [43:20] all right well thank you very much T [43:25] Khan [43:29] you