z3 - 将 IR 转换为 Z3 公式？

Question

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

1. 是否有任何技术论文详细解释了如何将 SSA IR 转换为 SMT 公式？我四处寻找，无济于事。

2. 对于那些计算指令，转换为 Z3 公式没有太大问题。但是，我仍在为无条件和有条件的分支指令而苦苦挣扎。关于如何将这些指令转换为 Z3 公式的任何建议？

非常感谢！！！

Answer 1

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

• Fuzzer 和 Bug 查找器。这些工具本质上是将程序的一个执行路径编码为 SMT 公式。这些工具使用 SMT 来检查特定的执行路径是否可行。示例或此类工具有：Pex、EXE、Sage。根据您的问题，您似乎已经知道如何将一条路径编码为 SMT。

• 扩展静态检查器和验证编译器。这些工具通常将程序简化为中间形式。然后，生成几个验证条件 (VC) 并将其发送到 SMT 求解器。他们中的大多数（全部？）尝试进行模块化验证，因为将整个程序验证为单个 SMT 问题的成本太高。Boogie-PL 是一种非常流行的中间格式。如果您将 IR 映射到 Boogie-PL，则可以使用Boogie生成 SMT 格式的 VC。文章“非结构化程序的最弱前提条件”描述了 Boogie-PL 如何编码为公式。请注意，Boogie 是开源的，代码可读性很强。因此，您还可以浏览代码以阐明详细信息。鲁斯坦·莱诺还有一堆幻灯片解释了如何将 Boogie VC 编码为公式。其他相关项目是ESC/Java 2、Why3、VeriFast。

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

循环不变示例：duplet此Why3 验证示例中的函数。

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