学术嵌入式形式验证并非能让计算机系统瞬间变好的神奇魔法它和其他系统级工作一样涉及大量艰难、繁琐且复杂的工程任务。而且验证工具本身也很难做到万无一失存在各种缺陷调试起来比其他软件更困难。若要信任这些工具就必须对其进行严格测试。Alive2翻译验证工具Alive2 是一款翻译验证工具给定 LLVM IR 中的两个版本的函数通常对应某个函数在优化前后的代码它会尝试证明该优化是否正确。在实际应用中编译器工程师会使用 Alive2超过 600 个 LLVM 问题都链接到了在线 Alive2 实例。Alive2 的缺陷分类抛开崩溃等问题Alive2 的缺陷大致可分为两类误报和漏报。误报是指实际没有错误时Alive2 却发出了错误信号漏报则是实际存在错误时Alive2 未能发出错误信号。第一类错误相对容易测试只需让 Alive2 验证大量优化并仔细查看它发出的错误信号。而第二类错误难测得多因为缺少可能触发漏报错误的测试用例。每个这样的测试都需要一对 LLVM IR 函数它们具有相同的签名但对于至少一组输入其行为明显不同。而且不能依赖编译器的错误来创建这些测试用例因为 LLVM 本身并不是一个容易出错的编译器它执行的绝大多数优化都是正确的。寻找漏报错误的方法一使用 YARPGen为了找到漏报错误尝试使用了 YARPGen这是一个随机程序生成器已被用于发现大量编译器错误。YARPGen 的关键优势在于它生成的 C 或 C 函数不会出现未定义行为。不过仅这一点还不足以发现漏报错误所以对 YARPGen 进行了修改。修改后的版本会生成一个随机函数然后在保证新函数同样没有未定义行为的前提下对该函数进行轻微的随机修改。有了两个非常相似且都没有未定义行为的函数后还需要确保这两个函数在执行时至少对于一组输入会产生不同的结果。为此将这对函数进行编译和运行舍弃那些修改后行为没有明显变化的函数对。最后将这对函数编译成 LLVM IR然后让 Alive2 检查其中一个函数是否能细化另一个函数。如果 Alive2 没有发出错误信号那么就找到了漏报错误。寻找漏报错误的方法二借助 Minotaur寻找漏报错误的另一种方法是偶然发现的。意识到 Zhengyang Liu 的 LLVM 超级优化器 Minotaur 在每次使用时实际上都在被动地寻找漏报错误。对于正在优化的程序中的每个 LLVM 指令Minotaur 都会尝试找到一种更高效的计算方法。它会提取该指令及其部分反向数据、控制和内存依赖项生成一个新的 LLVM 函数该函数返回目标指令计算的值。这个新函数作为程序综合问题的 规范目标是找到一种更高效的方法来计算该规范。Minotaur 使用 Alive2 来确保新函数能细化旧函数并使用 llvm - mca 来确保新函数的计算成本更低。综合过程通过枚举大量 部分符号化 的候选方案来实现其中指令用具体形式表示而字面常量用符号表示。Zhengyang 对 Alive2 进行了修改当候选方案中至少包含一个符号常量时它会发出一个存在 - 全称求解器查询。由于候选方案数量众多其中绝大多数都无法细化规范这就给了 Alive2 很多漏报的机会。如果 Alive2 在被 Minotaur 调用时漏报了错误由于漏报意味着 Alive2 声称某个候选方案能细化规范但实际上并不存在这种细化关系而细化是优化器的正确性标准从定义上来说这些失败会导致编译错误。因为经常使用 Minotaur 来编译大型开源程序然后运行它们的测试套件所以有很大机会发现它引入的任何编译错误。目前的发现与疑问研究了两种不同的方法来寻找 Alive2 中的漏报错误一种是使用随机搜索另一种是使用小规模的穷举搜索。到目前为止收获甚微看起来 Alive2 和 Z3 不太容易出现漏报情况这意味着它达到了其顶层设计目标这是好事因为在实际应用中人们确实依赖 Alive2。但现在能确定 Alive2 不会漏报错误了吗可惜还不能确定。怀疑如果真的想找到漏报错误应该关注 Alive2 对函数属性和类似结构的支持而 YARPGen 和 Minotaur 在这方面的测试都不够深入。评论关于工具探索状态空间的思考BCS 提出疑问关于像 YARPGen 和 大型开源程序集合 这样的工具实际探索了多少完整状态空间有多少相关研究呢甚至不知道该如何描述完整状态空间的范围但猜测任何单一的方法都可能会遗漏 几乎所有从数学意义上来说的状态空间。不过只要实际应用中使用的部分得到覆盖将资源用于探索新方法可能比扩大现有方法的覆盖范围更有价值。