我在IR中有一些代码,这段代码已经是SSA形式.现在我试图将此代码转换为SMT公式,然后将其提供给Z3进行一些验证.我有一些问题:
有没有技术论文详细解释如何将SSA IR转换为SMT公式？我四处搜索,无济于事.
对于那些计算指令,转换为Z3公式没有太多问题.但是,我仍在努力处理无条件和条件分支指令.有关如何将这些指令转换为Z3公式的任何建议？
非常感谢!!!
我认为将基于SMT的程序验证工具分为两大类是公平的:
Fuzzers和Bug finders.这些工具实质上将程序的一个执行路径编码为SMT公式.这些工具使用SMT来检查特定执行路径是否可行.示例或此类工具是:Pex,EXE,Sage.根据您的问题,您似乎已经知道如何将一条路径编码为SMT.
扩展静态检查器和验证编译器.这些工具通常会将程序缩减为中间形式.然后,产生若干验证条件(VC)并将其发送到SMT求解器.他们中的大多数(全部？)都尝试进行模块化验证,因为将整个程序验证为单个SMT问题太昂贵了.Boogie-PL是一种非常流行的中间格式.如果您将IR映射到Boogie-PL,则可以使用Boogie以SMT格式生成VC.文章" 非结构化程序的最弱前提条件 "描述了如何将Boogie-PL编码为公式.请注意,Boogie是开源的,代码非常易读.因此,您也可以浏览代码以澄清细节.Rustan Leino还有一堆幻灯片,解释了如何将Boogie VC编码成公式.其他相关项目是ESC/Java 2,Why3,VeriFast.
编辑(处理循环):处理循环的最简单技术只展开给定次数.当我们这样做时,我们的验证工具变成了"错误查找器",因为我们基本上放弃了分析所有可能的路径.在工具(例如ESC/Java,Why3,VeriFast)中,使用循环不变量.Rustan有一个很好的视频和关于循环不变量的讲义.循环不变量可以由用户提供,或者自动计算.关于"循环不变合成"的论文很多.
循环不变的示例:duplet此Why3验证示例中的函数.
另一种可能性是将您的IR编码为muZ.muZ是Z3中提供的定点引擎.在这种方法中,循环可以直接编码(参见muZ页面上的文章),并且不需要提供循环不变量.然而,像muZ这样的引擎尚未成熟,成为最先进的SMT解决方案.