z3 - 将 IR 转换为 Z3 公式？

Question

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

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

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

非常感谢!!!

Answer 1

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

Fuzzer 和 Bug 查找器。这些工具本质上是将程序的一个执行路径编码为 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 .

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

循环不变示例:函数 duplet在这个 Why3 verification example .

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