2

美好的一天，自动扣款和验证黑客！

为了更深入地了解WhyML 究竟如何为 ACSL 注释的 C 程序提供证明，我试图手动“重现”Why3 对 WhyML 程序所做的工作，同时将其转换为 SMT 逻辑并将其输入 Z3 证明程序。

假设我们有以下 C 片段：

const int L = 3;
int a[L] = {0};
int i = 0;
while (i < L) {
  a[i] = i;
  i++;
}
assert (a[1] == 1);

我正在尝试将其编码为 SMT 逻辑，如下所示：

(set-logic AUFNIRA)
(define-sort _array () (Array Int Int))
(declare-const ar _array)
(declare-fun set_a_i (_array Int Int) _array)
(assert (forall ((ar0 _array) (i Int) (j Int)) 
    (ite (< i j)   
                 (= (set_a_i ar0 i j) 
                    (set_a_i (store ar0 i i) (+ i 1) j))
                 (= (set_a_i ar0 i i) ar0) ))) 

(assert (= (select (set_a_i ar 0 3) 1) 1))
(check-sat)

Z3 给出“未知”。

这可能是因为在指定 set_a_i 函数时使用了量化。但我看不到其他方法来指定它。

我知道以下陈述：

  • SMT 求解器通常不能（或以不好的方式）处理数组上的量化。
  • 如果我提供前后条件和循环不变量，WhyML 能够证明这样的程序。
  • 即使后端设置为 Z3，WhyML 也能够证明此类程序，因此 SMT 求解器本身不是问题。
  • WhyML 可以生成 z3 smt 文件，但要理解它是一件很辛苦的事情，部分原因是由于 whyML->smt 翻译的自动性质（例如，它不保留变量名）

我阅读了几乎所有为 WhyML、Frama-C WP 插件和 Z3 提供的材料。我还阅读了几篇关于验证 C 代码的论文，但没有发现任何关于 C --> SMT 翻译技术的文章。

我应该学习哪些材料来获得这种理解？您能否提供见解和/或链接到描述这种将命令式代码转换为多排序一阶逻辑的机制的论文。

我将不胜感激任何评论。谢谢！

祝你好运，叶夫根尼。

4

1 回答 1

3

WP 0.8 插件手册和论文“ Why3 : Shepherd Your Herd of Provers ”提供了带注释的 C 代码如何转换为为什么逻辑以及为什么逻辑随后如何转换为定理证明器的输入逻辑的高级概述.

如 WP 插件手册第 1.3 节所述，首先考虑 Hoare 的三元组：

{ P } stmt { Q }

读作：只要先决条件P成立，然后在运行stmt后，后置条件Q成立。WP 插件将最弱的前置条件视为stmt上的函数和后置条件，因此以下 Hoare 三元组成立：

{ wp ( stmt , Q )} stmt { Q }

从某种意义上说，最弱的前提条件是在 stmt 执行之前必须保持的最简单的属性，这样 Q 在 stmt执行之后保持不变。

例如，考虑stmt为x = x + 1且 { Q } 为 {x > 0} 的情况。根据 Hoare 演算的赋值规则，我们知道 {x + 1 > 0} x = x + 1{x > 0} 成立。{x + 1 > 0} 实际上是x = x + 1和 {x > 0} 的最弱前提。

更一般地说，可以确定任何语句和任何后置条件的最弱前置条件。

现在假设您有一个用前置条件P和后置条件Q注释的函数f：

{ P } f { Q }

定义W = wp ( f , Q )。根据wp的定义，我们知道以下 Hoare 三元组成立：

{ W } f { Q }

如果我们能够证明P ⇒ W（这是提交给定理证明者的内容），那么属性P和Q对于f的有效性就成立了。

WP 插件生成为什么逻辑。正如“Why3: Shepherd Your Herd of Provers”论文的第 4 节所述，Why3 的​​操作被描述为处理证明任务，这是一系列以目标结尾的声明。这就是为什么逻辑转换为特定定理证明器的输入逻辑的方式。

对于一个具体的例子，论文给出了将Why logic 转换为 Z3 的概述。不仅输入语言不同（Z3使用SMT-LIB2语法），Why和Z3的逻辑也有显着差异。论文给出了 Z3 不支持多态和归纳谓词的例子。

为了将 Why 逻辑转换为定理证明器的输入逻辑，Why3 使用了一系列转换，逐渐将 Why 逻辑转换为目标输入逻辑。Why3 使用称为驱动程序的配置文件来定义所有转换，一个漂亮的打印机输出证明者的本机输入格式，以及用于解释证明者输出的正则表达式。

假设您已经运行why3config，您可以查看.why3.conf主目录中自动生成的配置文件，以确定Why3 用于特定证明者的驱动程序。例如，在我的系统上，Why3~/.opam/system/share/why3/drivers/z3_432.drv在使用 Z3 时使用。 z3_432.drv将smt-libv2.drv驱动程序作为 SMT-LIB2 兼容证明器的基本驱动程序导入。

我知道您知道检查生成的 SMT2，但我想我会提到如何为任何感兴趣的人执行此操作。如果您将-wp-out DIRand-wp-proof-trace选项传递给frama-c，则 WP 将保存在单个属性上运行证明者的输出。然后，您可以找到.err感兴趣的属性的相应文件。在我的情况下，它是main_assert_final_a_Why3_z3.err. 在文本编辑器中打开该文件，您将看到如下内容：

call_provers：命令是：/Users/dtrebbien/.opam/system/lib/why3/why3-cpulimit
  10 1000 -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false
  smt.random_seed=42
  /var/folders/1v/2nkqhkgx0qnfwd75h0p3fcsc0000gn/T/why_9f8a52_main_Why3_ide-T-WP.smt2

此.smt2文件包含Why3 生成的 Z3 的 SMT-LIB2 输入。

如果您愿意，可以运行该命令。就我而言，我看到：

警告：模式确实包含任何变量。
警告：模式确实包含任何变量。
警告：模式确实包含任何变量。
警告：模式确实包含任何变量。
不饱和
为什么3cpulimit时间：0.020000 s

虽然有点违反直觉，但unsat意味着该属性的有效性已建立。

于 2015-07-22T11:57:52.057 回答