形式化验证(Formal Verification)常被误解为一种「魔法粉末」,只要洒在系统上就能保证万无一失。然而,真正的形式化验证工作并非如此简单。它涉及大量复杂的工程挑战,与其他系统级软件开发一样,需要面对艰难的调试和验证过程。更为关键的是,形式化验证工具本身也极易出现缺陷,甚至比普通软件更难以调试。这些工具必须经过严格测试,才能被开发者和研究人员所信任。在编译器优化领域,形式化验证工具扮演着至关重要的角色。
以 Alive2 为例,这是一个专门用于 LLVM IR(中间表示)的翻译验证工具。它通过比较优化前后的函数版本,判断编译器优化是否正确。Alive2 不仅在理论研究中具有价值,更在实际工程中得到广泛应用 - - 超过 600 个 LLVM 问题报告直接关联到 Alive2 的在线实例,证明其在编译器开发中的重要性。然而,Alive2 这样的工具也面临着两大类缺陷:1. **误报(False Alarm)**:当优化实际上是正确的,但 Alive2 却错误地认为存在问题。2. **漏报(Missed Alarm)**:当优化实际上存在问题,但 Alive2 却未能检测到。误报虽然令人烦恼,但相对容易发现 - - 只需运行大量优化测试,检查 Alive2 报告的错误即可。
每个误报背后可能隐藏着 LLVM 或 Alive2 自身的缺陷。相比之下,漏报则更为隐蔽和危险。因为漏报意味着 Alive2 未能发现一个实际存在的错误优化,这可能导致编译器生成错误的机器码,进而引发程序运行时的严重问题。寻找漏报缺陷的挑战在于:我们需要构造一对 LLVM IR 函数,它们在语法上相似,但在某些输入下行为不同。这种测试用例的构造极其困难,因为大多数编译器优化都是正确的,LLVM 很少出现明显的错误。因此,传统的随机测试方法难以覆盖这类缺陷。
为了解决这一难题,研究人员尝试了两种截然不同的方法。第一种方法基于随机程序生成器 YARPGen,第二种则是通过超级优化器 Minotaur 的协同验证。这两种方法虽然出发点不同,但都为发现 Alive2 的漏报缺陷提供了新的思路。---### **方法一:随机变异生成测试用例**YARPGen 是一个广泛用于发现编译器错误的随机程序生成器。它能够生成无未定义行为(Undefined Behavior, UB)的 C 或 C++ 函数,确保生成的代码在语义上是安全的。然而,仅仅生成无 UB 的代码并不足以发现漏报缺陷。
因此,研究人员对 YARPGen 进行了改进,使其能够生成一对非常相似但行为不同的函数。具体步骤如下:1. **生成原始函数**:YARPGen 首先生成一个随机函数,确保其无未定义行为。2. **随机变异**:对原始函数进行轻微变异(如修改常量、调整运算顺序等),同时保证变异后的函数仍然无未定义行为。3. **行为差异验证**:将变异后的函数与原始函数编译并执行,检查是否存在输入使得两者行为不同。如果行为相同,则丢弃该测试用例。4. **Alive2 验证**:将生成的函数对编译为 LLVM IR,并交由 Alive2 验证。
由于两者在某些输入下行为不同,Alive2 应当检测到优化错误。如果 Alive2 未能报告错误,则说明发现了漏报缺陷。这种方法的核心在于构造「几乎相同但行为不同」的函数对。通过随机变异,研究人员能够在大规模测试中覆盖更多边界情况,从而提高发现漏报的概率。然而,由于 LLVM 的优化通常是正确的,这种方法的成功率仍然有限。尽管如此,它为形式化验证工具的测试提供了新的思路。
---### **方法二:超级优化器协同验证**第二种方法的灵感来自于 Minotaur - - 一个 LLVM 超级优化器。超级优化器的目标是为每个 LLVM 指令寻找更廉价的计算方式,从而提升程序性能。Minotaur 的工作流程如下:1. **提取指令依赖**:对于程序中的每个指令,Minotaur 提取该指令及其数据、控制和内存依赖,构建一个新的 LLVM 函数。2. **规范化验证**:该新函数作为规范(Specification),用于验证是否存在更廉价的实现方式。3. **程序合成**:Minotaur 通过枚举大量候选实现(部分符号化表示),并使用 Alive2 验证这些候选是否满足规范(即是否「精炼」原始指令)。4. **性能验证**:同时,Minotaur 使用 llvm-mca 工具验证候选实现是否在性能上更优。
在 Minotaur 的验证过程中,Alive2 扮演着关键角色。然而,由于候选实现数量庞大,且大多数候选并不满足精炼关系,Alive2 需要频繁处理「不精炼」的情况。如果 Alive2 在某些情况下未能检测到不精炼关系,即发生漏报,那么 Minotaur 可能会选择一个错误的优化方案,导致编译器生成错误的代码。研究人员发现,Minotaur 在实际使用中(如编译大型开源项目并运行其测试套件)能够被动地暴露 Alive2 的漏报缺陷。如果 Alive2 发生漏报,Minotaur 可能会生成一个错误的优化方案,进而在运行时触发程序错误。通过这种方式,研究人员能够间接验证 Alive2 的正确性。
---### **实践结果与反思**经过上述两种方法的大规模测试,研究人员发现 Alive2 和其底层求解器 Z3 在漏报方面表现良好。这意味着 Alive2 基本实现了其设计目标 - - 在实际应用中可靠地验证编译器优化的正确性。然而,这并不意味着形式化验证工具的问题已经完全解决。研究人员指出,当前的测试方法(如 YARPGen 和 Minotaur)主要关注基础指令和简单优化场景,而对更复杂的语言特性(如函数属性、内存模型等)涉及较少。这些特性在实际编译器优化中扮演着重要角色,但往往被现有测试方法所忽略。因此,未来的工作可能需要更深入地探索这些边界情况,以确保形式化验证工具在所有场景下的正确性。
---### **形式化验证工具的未来:挑战与机遇**形式化验证工具的发展面临着双重挑战:一方面,工具本身的复杂性和可靠性要求不断提升;另一方面,编译器优化技术的快速演进(如机器学习驱动的优化、自动向量化等)为验证工具带来了新的挑战。1. **工具可靠性**:形式化验证工具必须能够处理现代编译器中的复杂优化,包括跨模块优化、链接时优化(LTO)等。这要求验证工具具备更强的表达能力和更高的性能。2. **新兴优化技术**:随着机器学习和自动化工具在编译器中的应用,形式化验证工具需要适应这些新技术带来的变化。例如,如何验证机器学习驱动的优化方案的正确性,仍是一个开放问题。3. **工业级应用**:在工业界,形式化验证工具(如 Alive2)的应用正在逐步普及。
然而,如何将这些工具集成到现有的开发流程中,并确保其在大规模代码库中的可扩展性,仍是一个需要解决的问题。---### **结论:从理论到实践的持续探索**形式化验证工具的漏报缺陷检测是一个极具挑战性的问题。通过随机变异生成和超级优化器协同验证,研究人员为这一问题提供了创新的解决方案。尽管当前的测试方法已经取得了一定的成功,但仍然存在局限性。未来的工作需要更深入地探索形式化验证工具的边界,特别是在处理复杂语言特性和新兴优化技术方面。对于开发者和研究人员而言,形式化验证工具的可靠性不仅关乎理论上的正确性,更关乎实际工程中的安全性和效率。
因此,持续投入资源改进这些工具,并探索新的验证方法,将是推动编译器技术发展的重要方向。 。
