将 IR 转换为 Z3 公式？答案

【问题标题】：converting IR to Z3 formula?将 IR 转换为 Z3 公式？
【发布时间】：2012-12-21 01:08:05
【问题描述】：

我在 IR 中有一些代码，并且该代码已经采用 SSA 形式。现在我正在尝试将此代码转换为 SMT 公式，然后将其提供给 Z3 进行一些验证。我有一些问题：

有没有技术论文详细解释了如何将SSA IR转换为SMT公式？我四处寻找，无济于事。
对于那些计算指令，转换为Z3公式没有太大问题。但是，我仍在为无条件和有条件的分支指令而苦苦挣扎。关于如何将这些指令转换为 Z3 公式的任何建议？

非常感谢！！！

【问题讨论】：

标签： z3

【解决方案1】：

我认为将基于 SMT 的程序验证工具分为两大类是公平的：

模糊器和错误查找器。这些工具本质上是将程序的一个执行路径编码为 SMT 公式。这些工具使用 SMT 来检查特定的执行路径是否可行。示例或此类工具有：Pex、EXE、Sage。根据您的问题，您似乎已经知道如何将一条路径编码为 SMT。
扩展的静态检查器和验证编译器。这些工具通常将程序简化为中间形式。然后，生成几个验证条件 (VC) 并将其发送到 SMT 求解器。他们中的大多数（全部？）尝试进行模块化验证，因为将整个程序验证为单个 SMT 问题的成本太高。 Boogie-PL 是一种非常流行的中间格式。如果您将 IR 映射到 Boogie-PL，则可以使用 Boogie 生成 SMT 格式的 VC。文章“Weakest-Precondition of Unstructured Programs”描述了如何将 Boogie-PL 编码为公式。请注意，Boogie 是开源的，代码可读性很强。因此，您还可以浏览代码以阐明详细信息。 Rustan Leino 还有一堆幻灯片，解释如何将 Boogie VC 编码为公式。其他相关项目有ESC/Java 2、Why3、VeriFast。

EDIT（处理循环）：处理循环的最简单技术只是将它们展开给定次数。当我们这样做时，我们的验证工具就变成了“错误查找器”，因为我们基本上放弃了分析所有可能的路径。在工具（如 ESC/Java、Why3、VeriFast）中，使用了loop invariants。 Rustan 有一个很好的video and lectures notes 关于循环不变量。循环不变量可以由用户提供，也可以自动计算。关于“循环不变综合”的论文很多。

循环不变示例：Why3 verification example 中的函数 duplet。

另一种可能性是将您的 IR 编码为muZ。 muZ 是 Z3 中可用的定点引擎。在这种方法中，可以直接对循环进行编码（参见 muZ 页面上的文章），无需提供循环不变量。然而，像 muZ 这样的引擎作为最先进的 SMT 求解器尚未成熟。

【讨论】：

与往常一样，Leo，您的回答很棒！但是，我还有一个问题：我看了上面提到的论文“Weakest precondition of Unstructured Programs”，不明白为什么在生成公式之前必须要有一个无循环的代码？（作者删除了循环的所有后边缘）。这个问题与我有关，因为我的 IR 代码有条件分支和无条件分支，我仍然不确定如何处理它们。非常感谢，狮子座！
我添加了关于循环的附加注释。