将IR转换为Z3公式? [英] converting IR to Z3 formula?
问题描述
我在 IR 中有一些代码，并且此代码已采用 SSA 形式.现在我正在尝试将此代码转换为 SMT 公式，然后将其提供给 Z3 进行一些验证.我有几个问题:
I have some code in IR, and this code is already in SSA form. Now I am trying to convert this code to SMT formula, then feed it to Z3 to do some verification. I have some questions:
是否有技术论文详细解释了如何将 SSA IR 转换为 SMT 公式?我四处寻找，无济于事.
Is there any technical paper explains in detail how to convert SSA IR to SMT formula? I searched around, to no avail.
对于那些计算指令，转换为Z3公式没有太大问题.但是，我仍在为无条件和条件分支指令而苦苦挣扎.关于如何将这些指令转换为 Z3 公式的任何建议?
For those computational instructions, there is not much problems converting to Z3 formula. However, I am still struggling with unconditional and conditional branch instructions. Any suggestion on how to convert these instructions to Z3 formula?
非常感谢！！！
推荐答案
我认为将基于 SMT 的程序验证工具分为两大类是公平的:
I think it is fair to divide the SMT based program verification tools in two main groups:
模糊器和错误查找器.这些工具基本上将程序的一个执行路径编码为 SMT 公式.这些工具使用 SMT 来检查特定的执行路径是否可行.示例或此类工具有:Pex、EXE, 圣人.根据您的问题，您似乎已经知道如何将一条路径编码为 SMT.
Fuzzers and Bug finders. These tools essentially encode one execution path of the program into a SMT formula. These tools use SMT to check whether a particular execution path is feasible or not. Examples or such tools are: Pex, EXE, Sage. Based on your question, it seems you already know how to encode one path into SMT.
扩展静态检查器和验证编译器.这些工具通常将程序简化为中间形式.然后，生成多个验证条件 (VC) 并将其发送到 SMT 求解器.他们中的大多数(全部?)尝试进行模块化验证，因为将整个程序验证为单个 SMT 问题的成本太高了.Boogie-PL 是一种非常流行的中间格式.如果您将 IR 映射到 Boogie-PL，则可以使用 Boogie 生成 SMT 格式的 VC.文章非结构化程序的最弱先决条件" 描述了 Boogie-PL 如何编码到公式中.请注意，Boogie 是开源的，代码可读性很强.因此，您也可以浏览代码以澄清细节.Rustan Leino 也有一堆幻灯片解释了如何对 Boogie VC 进行编码成公式.其他相关项目有 ESC/Java 2、Why3, VeriFast.
Extended Static Checkers and Verifying Compilers. These tools usually reduce the program to an intermediate form. Then, several verification conditions (VCs) are produced and sent to a SMT solver. Most of them (all?) try to do modular verification, since it is too expensive to verify the whole program as a single SMT problem. Boogie-PL is a very popular intermediate format. If you map your IR into Boogie-PL, you can then use Boogie to generate the VCs in SMT format. The article "Weakest-Precondition of Unstructured Programs" describes how Boogie-PL is encoded into formulas. Note that, Boogie is open-source, and the code is very readable. So, you may also browse the code to clarify details. Rustan Leino also has a bunch of slides explaining how to encode Boogie VCs into formulas. Other relevant projects are ESC/Java 2, Why3, VeriFast.
EDIT(处理循环):处理循环的最简单技术就是将它们展开给定的次数.当我们这样做时，我们的验证工具就变成了错误查找器"，因为我们基本上放弃了分析所有可能的路径.在工具(如 ESC/Java、Why3、VeriFast)中，使用了循环不变量.Rustan 有一个关于循环不变量的很好的视频和讲义.循环不变量可由用户提供，或自动计算.关于循环不变综合"的论文很多.
EDIT (handling loops): the simplest technique for handling loops just unfold them for a given number of times. When we do that, our verification tool becomes a "bug finder" since we are essentially giving up on analyzing all possible paths. In tools (such as ESC/Java, Why3, VeriFast), loop invariants are used. Rustan has a nice video and lectures notes about loop invariants. The loop invariants may be provided by the user, or automatically computed. There are many papers on "loop invariant synthesis".
循环不变的例子:这个Why3验证中的函数duplet例子.
Loop invariant example: the function duplet in this Why3 verification example.
另一种可能性是将您的 IR 编码为 muZ.muZ 是 Z3 中可用的定点引擎.在这种方法中，可以直接对循环进行编码(参见 muZ 页面上的文章)，并且不需要提供循环不变量.然而，像 muZ 这样的引擎作为最先进的 SMT 求解器还没有成熟.
Yet another possibility is to encode your IR into muZ. muZ is the fixedpoint engine available in Z3. In this approach, loops can be directly encoded (see the articles on the muZ page), and no loop invariants need to be provided. However, engines like muZ are not yet mature as state-of-the-art SMT solvers.
这篇关于将IR转换为Z3公式?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
