一个简单的运行时不变量挖掘器

# 一个简单的运行时不变式挖掘器 来源: http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/ TLDR: 本文完整实现了一个 Daikon 风格的运行时不变式挖掘器，涵盖插桩、轨迹收集、候选不变式检查以及基于蕴含的抑制。 ## Oracle 问题与似然不变式 软件测试中的一个核心挑战是 **Oracle 问题**：如何通过编程方式判断测试输出是否正确？手动编写断言（即“Oracle”）既繁琐又常常不完整。 Daikon 风格的挖掘提供了一种 **近似 Oracle**。通过观察程序的 *gold* 运行，我们可以将由此产生的不变式视为正确行为的规约。 需要牢记两个关键区别： 1. **似然性，而非保证性**：由于这些不变式是通过观察归纳得出的，它们只是假设。如果你的输入只包含正整数，挖掘器可能会报告 `x > 0` 为一个不变式，即使该函数本应处理负数。 2. **描述性 vs. 规范性**：挖掘出的不变式描述的是代码*当前*的行为，而不一定是程序员*意图*的行为。如果 “gold” 版本的代码存在 bug，挖掘器会忠实地将该 bug 提升为一个需求。 尽管是近似的，这些 Oracle 在**回归测试**中极其有效。如果一次重构导致以前稳定的不变式失效，那么你的“自动化 Oracle”就标记出了一个人类可能遗漏的破坏性变更。 *运行时不变式挖掘*的概念如下：给定一个程序和一组输入，我们在一个追踪器下运行程序，该追踪器会在执行的关键点（如函数入口、函数出口等）记录所有变量的值。然后我们生成一大组候选不变式（例如 `x >= 0`、`x == y`、`len(a) == n`），并针对每个记录的状态检查每个候选不变式。能够存活在所有观测中的候选不变式被报告为一个似然不变式。这一思想由 Ernst 等人在 Daikon 系统中提出 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#fn:ernst2001daikon)。Daikon 已被用于发现真实 bug、生成测试 Oracle 以及自动记录程序行为。与我们的 grammar miner (http://rahul.gopinath.org/post/2019/11/26/simpleminer-01/) 类似，本文通过 `sys.settrace` 进行挂钩，并在程序运行时收集观测。区别在于，我们不再恢复输入字符串的结构，而是恢复程序变量的逻辑性质。 ## 概要 `` results = mine_invariants(triangle, triangle_inputs) for point, invs in results.items(): print(point) for inv in invs: print(' ', inv) `` ## 定义 - **程序点**是程序执行中的一个命名位置，在此处观察变量值。典型的程序点包括函数入口 (`ENTER`) 和函数出口 (`EXIT`)。按惯例，名称格式为 `function_name:::POINT_TYPE`。 - **轨迹**是程序在单个输入的一次运行中收集的（程序点，变量状态）对序列。 - **变量状态**是在给定程序点处所有作用域内变量绑定的快照。对于 `EXIT` 点，还包括绑定在键 `'return'` 上的返回值。 - **候选不变式**是一个关于变量状态的谓词，我们希望检查它是否成立。例如 `x >= 0` 或 `x == y`。 - 如果一个不变式对于某个状态成立，则称它在该状态下**存活**。一个不变式在第一次对任何观测状态失败时就被**证伪**，此后便被丢弃。 - **似然不变式**是一个在其程序点处的所有观测状态中都存活的候选不变式。之所以称为“似然”，是因为我们只检查了有限的一组输入。 - **抑制**是移除冗余不变式的过程。如果 `x == y` 成立，那么 `x <= y` 和 `x >= y` 都蕴含于它，无需单独报告。 ## 目录 1. Oracle 问题与似然不变式 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#the-oracle-problem-and-likely-invariants) 2. 概要 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#synopsis) 3. 定义 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#definitions) 4. 前置条件 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#prerequisites) 5. 程序点 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#program-points) 6. TraceStore (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#tracestore) 7. 插桩 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#instrumentation)1. 上下文 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#context) 2. 插桩器 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#instrumentor) 3. 收集多个输入的轨迹 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#collecting-traces-over-multiple-inputs) 8. 候选不变式 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#candidate-invariants)1. 一元模板 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#unary-templates) 2. 二元模板 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#binary-templates) 9. 不变式引擎 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#invariant-engine)1. 为一个点生成候选 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#generating-candidates-for-a-point) 2. 针对观测检查候选 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#checking-candidates-against-observations) 3. 运行完整分析 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#running-the-full-analysis) 10. 抑制 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#suppression) 11. 完整流水线 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#full-pipeline) 12. 作用域程序点 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#scoped-program-points) 13. 前置/后置关系 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#prepost-relations)1. PairedTraceStore (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#pairedtracestore) 2. PairedInstrumentor (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#pairedinstrumentor) 3. collect_pairs (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#collect_pairs) 4. 关系不变式模板 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#relational-invariant-templates) 5. RelationalEngine (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#relationalengine) 6. 完整关系流水线 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#full-relational-pipeline) 14. 扩展示例：牛顿法 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#extended-example-newtons-method) 15. 工具函数 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#utilities) 16. 性能 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#performance) 17. 结论：“足够好”的 Oracle 的价值 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#conclusion-the-value-of-good-enough-oracles) 18. 参考文献 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#references) 19. 制品 (http://rahul.gopinath.org/post/2026/05/09/simple-invariant-miner/#artifacts) **重要:** Pyodide (https://pyodide.readthedocs.io/en/latest/) 初始化需要时间。初始化完成时，“Run all”按钮会显示红色边框。 ## 前置条件 本文只需要 Python 标准库。 我们将使用以下简单的函数作为贯穿全文的运行示例。它们足够小，我们可以通过检查来预测其不变式，从而验证挖掘器是否正确工作。 ## 程序点 Daikon 最重要的设计决策是将不变式附加到程序中称为**程序点**的特定位置。这意味着 `foo:::ENTER` 处的 `x >= 0` 和 `foo:::EXIT` 处的 `x >= 0` 是两个不同的不变式。这种区分很重要：一个变量可能在入口处满足某个性质，但在出口处不满足，反之亦然。 我们将程序点表示为一个小的具名对象。按惯例，名称格式为 `function_name:::POINT_TYPE`。我们为其提供 `__eq__` 和 `__hash__` 方法，以便它可以用作字典键。 两个具有相同名称的 `ProgramPoint` 对象必须比较相等且哈希值相同，这样在不同地方创建的相同点将指向相同的字典条目。 ## TraceStore `TraceStore` 按程序点名称收集观测到的变量状态。每个条目是一个状态字典列表，每个观测一个，跨所有输入累积。 验证观测是否正确累积，并且 `get` 方法按插入顺序返回它们。 ## 插桩 为了收集轨迹，我们利用 Python 的 `sys.settrace` 机制。我们需要两个基础设施：一个 `Context` 类，用于从原始 Python 帧中解包我们需要的信息；一个 `Instrumentor` 类，用于管理 `sys.settrace` 的生命周期并累积事件。 ### 上下文 Python 的追踪回调接收一个原始的 `frame` 对象。`Context` 解包我们关心的字段：方法名、其声明的参数名、源文件以及当前行号。 `extract_vars` 返回帧中所有可见的局部绑定。`parameters` 将其过滤为仅声明的参数——这在 `call` 时刻很有用，此时我们只希望获取调用者传入的参数，而不是函数体可能已创建的任何局部变量。 我们在此直接验证 `Context`，然后再转向 `Instrumentor`，这样读者可以确切地看到帧被解包后的样子。我们安装一个最小的一次性回调，作为一个闭包，它会在第一个 `call` 事件时捕获帧并立即移除自身。这样所有机制都局限在测试块内。 ### 插桩器 `Instrumentor` 管理 `sys.settrace` 回调并驱动整个观测过程。 哪些变量值值得记录是一个策略决策，而非插桩的固定部分。默认的 `default_interesting` 接受一个变量名及其值，如果两者都值得记录则返回 `True`。默认情况下，它排除以 `_` 开头的名称（Python 内部变量）以及类型无法被我们的不变式模板推理的值。如果库用户希望包含私有变量、跟踪其他类型或排除特定名称，可以传入自己的 `interesting=my_predicate` 给任何插桩器或收集函数，而无需子类化任何东西。 `_tracer` 是注册到 `sys.settrace` 的原始回调。Python 会在每次 `call`、`return`、`line` 和 `exception` 事件时调用它；我们仅响应 `call` 和 `return` 以保持低开销。在 `call` 时，我们构建一个 `Context`，检查方法名不以 `_` 开头（以排除 Python 内部函数），收集被 `interesting` 接受的变量，并将其存储为 `ENTER` 状态。在 `return` 时，我们收集所有被接受的局部变量加上返回值，并将其存储为 `EXIT` 状态。回调总是返回自身，以便 Python 继续为嵌套帧调用它。 `run` 方法安装 `_tracer`，调用函数，并始终在 `finally` 块中拆除钩子，这样即使函数抛出异常，我们也永远不会留下过时的回调。 验证一次 `run` 调用是否同时产生 `ENTER` 和 `EXIT` 观测，`ENTER` 是否仅包含声明的参数，`EXIT` 是否包含返回值。 库用户可以通过传入自定义的 `interesting` 谓词来限制或扩展记录的内容。这里我们传入一个只接受整数的谓词，这意味着字符串返回值和非常量局部变量将被排除。注意谓词同时接收名称和值。例如，用户可以通过完全忽略名称过滤器来包含私有变量。 ### 收集多个输入的轨迹 我们每个输入运行一次函数，并将所有观测累积到同一个 store 中。`inputs` 的每个元素是一个参数元组。单参数函数将其参数包装在一个单元素元组中：`([1, 2, 3],)`。`interesting` 谓词会传递给 `Instrumentor`，以便调用者控制记录内容，而无需接触收集循环。 收集一组三角形输入的轨迹。 所有五个输入共享相同的两个程序点：`triangle:::ENTER` 和 `triangle:::EXIT`。它们的观测被合并，因此存活的不变式将是那些在所有输入中都成立的不变式。 ## 候选不变式 `Invariant` 对象封装了一个谓词并跟踪它是否已被证伪。一旦被证伪，它就会保持死亡——我们永远不会复活它。谓词接收一个状态字典，应返回一个 bool。评估期间的任何异常都算作证伪，这处理了类型不匹配（例如，将字符串与数字比较）而无需特殊处理。 ### 一元模板 一元不变式涉及单个变量。我们为观测到的每个变量生成一个小的固定模板集。不适用于该变量类型的模板（例如，对字符串应用 `>= 0`）将在第一次观测时被证伪，并安静地消失。 验证一个数值状态会杀死字符串模板但保留数值模板，而一个负值会杀死 `>= 0`。 ### 二元模板 二元不变式涉及两个变量。我们为至少在一个状态中同时出现的每一对变量生成模板。 验证相等的状态会保持 `==` 存活，而不同的状态会杀死它但保留 `<=` 存活。 ## 不变式引擎 引擎接收一个 `TraceStore`，为每个程序点生成候选不变式，并针对该点的所有观测检查它们。在每次观测中都存活的候选不变式就是一个似然不变式。 ### 为一个点生成候选 我们收集该点任何状态中出现的所有变量名，然后在这些名称上生成所有一元和二元候选。候选的数量随变量数量呈二次方增长，但对于典型的程序点，变量数量很小。 验证候选生成产生我们期望的模板。 ### 针对观测检查候选 我们针对每个观测状态测试每个候选。在所有观测后仍存活的候选就是似然不变式。迭代顺序无关紧要，因为证伪是单调的：一旦死亡，永远死亡。 ### 运行完整分析 `analyze` 遍历 store 中的每个程序点，为每个点生成全新的候选，针对该点的观测检查它们，并将幸存者收集到一个以点名为键的结果字典中。每个点都会重新生成候选，这样一点的证伪不会影响另一点。 在三角形轨迹上运行引擎。 在 `triangle:::ENTER` 处，我们看到 `a >= 0`、`b >= 0`、`c >= 0` 和 `type(a) is int`，因为我们所有的输入都使用了正整数。在 `triangle:::EXIT` 处，我们看到 `type(return) is str`。注意，合并所有五个输入意味着 `a == b` 不会存活——它对 `(3,3,3)` 和 `(5,5,5)` 成立，但对 `(3,4,5)` 不成立。我们将在下面的作用域程序点部分解决这个问题。 ## 抑制 引擎会产生许多冗余的不变式。如果 `x == y` 成立，那么 `x <= y` 和 `x >= y` 都不会增加信息。抑制步骤会移除那些被更强不变式蕴含的较弱不变式。 我们维护一个简单的蕴含表：如果匹配*强*模式的不变式存活，我们就移除任何涉及相同变量且匹配*弱*模式的共存活不变式。`_vars` 通过对不变式的名称字符串进行分词（并保留字母数字标记）来提取变量名。