问题描述
您好，自动扣款和验证黑客！
为了更深入地了解 WhyML 如何为 ACSL 注释的 C 程序提供证明，我尝试手动重现"Why3 对WhyML 程序所做的工作，同时将其转换为SMT 逻辑并将其提供给Z3 证明器.
假设我们有以下 C 片段:
const int L = 3;int a[L] = {0};int i = 0;而 (i < L) {a[i] = i;我++;}断言 (a[1] == 1);我正在尝试将其编码为这样的 SMT 逻辑:
(设置逻辑 AUFNIRA)(define-sort _array() (Array Int Int))(声明-const ar _array)(declare-fun set_a_i (_array Int Int) _array)(断言(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) )))(断言(=(选择(set_a_i ar 0 3)1)1))(检查周六)Z3 给出未知".
这可能是因为在指定 set_a_i 函数时使用了量化.但我看不到其他方法可以指定它.
我知道以下声明:
- SMT 求解器通常无法(或以糟糕的方式)处理阵列上的量化.
- WhyML 能够证明这样的程序，如果我提供 pre &后置条件和循环不变.
- 即使后端设置为 Z3，WhyML 也能够证明此类程序，因此 SMT 求解器本身不是问题.
- WhyML 可以生成 z3 smt 文件，但要理解它是一项艰巨的任务，部分原因是为什么WhyML->smt 翻译的自动性质(例如它不保留变量名称)
我阅读了几乎所有为 WhyML、Frama-C WP 插件和 Z3 提供的材料.我还阅读了几篇关于验证 C 代码的论文，但没有发现关于 C --> SMT 翻译技术的任何内容.
我应该学习哪些材料才能获得这种理解?您能否提供有关将命令式代码转换为多排序一阶逻辑的机制的论文的见解和/或链接.
我将不胜感激任何评论.谢谢！
祝你好运埃夫根尼.
WP 0.8 插件手册和论文Why3: Shepherd Your Herd of Provers" 提供有关如何将带注释的 C 代码转换为 Why 逻辑，以及如何将Why 逻辑转换为定理证明器的输入逻辑的高级概述.
如 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}的情况为例.根据霍尔微积分的赋值规则，我们知道 {x + 1 > 0} x = x + 1 {x > 0} 成立.{x + 1 > 0} 实际上是 x = x + 1 和 {x > 0} 的最弱前提.
更一般地说，可以确定任何语句和任何后置条件的最弱前置条件.
现在假设您有一个函数 f 注释了前置条件 P 和后置条件 Q:
{P} f {Q}
定义 W = wp(f, Q).根据 wp 的定义，我们知道以下 Hoare 三元组成立:
{W} f {Q}
如果我们能够证明P ⇒ W(这是提交给定理证明者的)，那么属性的有效性Pem> 和 Q 为 f 建立.
WP 插件生成 Why 逻辑.正如Why3:Shepherd Your Herd of Provers"论文的第 4 节所述，Why3 的操作被描述为处理证明任务，这是一系列以目标结尾的声明.这就是为什么将逻辑转换为特定定理证明器的输入逻辑的方式.
举一个具体的例子，本文概述了将Why逻辑转换为Z3.不仅输入语言不同(Z3使用SMT-LIB2语法)，逻辑上也有显着差异为什么和Z3.论文给出了Z3不支持多态或归纳谓词的例子.
为了将Why逻辑转换为定理证明器的输入逻辑，Why3使用了一系列的转换，逐渐将Why逻辑转换为目标输入逻辑.Why3 使用称为驱动程序的配置文件来定义所有转换、输出证明者的本机输入格式的漂亮打印机以及用于解释证明者输出的正则表达式.
假设您已经运行了 why3config，您可以查看主目录中自动生成的 .why3.conf 配置文件，以确定 Why3 使用的驱动程序特定的证明者.例如，在我的系统上，Why3 在使用 Z3 时使用 ~/.opam/system/share/why3/drivers/z3_432.drv.z3_432.drv 导入 smt-libv2.drv 驱动程序作为 SMT-LIB2 兼容证明器的基础驱动程序.
我知道您知道检查生成的 SMT2，但我想我会为感兴趣的任何人提及如何执行此操作.如果您将 -wp-out DIR 和 -wp-proof-trace 选项传递给 frama-c，那么 WP 将保存从在单个属性上运行证明器.然后，您可以为感兴趣的属性找到相应的 .err 文件.就我而言，它是 main_assert_final_a_Why3_z3.err.在文本编辑器中打开该文件，您将看到如下内容:
这个.smt2文件包含Why3生成的Z3的SMT-LIB2输入.
如果您愿意，可以运行该命令.就我而言，我看到:
警告:模式确实包含任何变量.警告:模式确实包含任何变量.警告:模式确实包含任何变量.警告:模式确实包含任何变量.未满足为什么3cpulimit时间:0.020000秒虽然有点违反直觉，unsat 意味着属性的有效性已经建立.
Good day, auto deduction and verification hackers!
In order to gain a deeper understanding of how exactly WhyML provides proofs for ACSL-annotated C programs I am trying to manually "reproduce" the job Why3 does with WhyML program while translating it into SMT logic and feeding it into Z3 prover.
Lets say we have the following C fragment:
const int L = 3;
int a[L] = {0};
int i = 0;
while (i < L) {
a[i] = i;
i++;
}
assert (a[1] == 1);
I am trying to encode it into SMT logic like this:
(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 gives "unknown".
This is probably because of quantification used in specifing set_a_i function. But I see no other ways to specify it.
I am aware of the following statements:
- SMT solvers in general are not able to (or do it in a bad way) handle quantifications over arrays.
- WhyML is able to prove such programs if I supply pre & post condition and loop invariant.
- WhyML is able to prove such programs even when backend is set to Z3, so SMT solver itself is not an issue.
- WhyML can produce z3 smt file, but to understand it is a great toil partly because of the automatic nature of whyML->smt translation (it doest not preserve variable names for example)
I read nearly all supplied materials for WhyML, Frama-C WP plugin and Z3. I also read several papers on verifing C code but found nothing regarding C --> SMT translation techniques.
Which materials should I study to gain this understanding? Could you please provide insights and/or links to papers describing this machinery of translating imperative code into multi-sorted first order logic.
I will appreciate any comments. Thanks!
Good luck,Evgeniy.
The WP 0.8 plugin manual and the paper "Why3: Shepherd Your Herd of Provers" provide a high-level overview of how annotated C code is transformed into Why logic, and how the Why logic is then transformed into the input logic of a theorem prover.
As described in section 1.3 of the WP plugin manual, start by considering Hoare's triples:
{P} stmt {Q}
which is read: whenever preconditions P hold, then after running stmt, the postconditions Q hold. The WP plugin considers the weakest precondition as a function over stmt and the postconditions such that the following Hoare triple holds:
{wp(stmt, Q)} stmt {Q}
The weakest precondition is, in a sense, the simplest property that must hold before the execution of stmt such that Q holds after the execution of stmt.
As an example, consider the case where stmt is x = x + 1 and {Q} is {x > 0}. By the assignment rule of Hoare calculus, we know that {x + 1 > 0} x = x + 1 {x > 0} holds. {x + 1 > 0} is, in fact, the weakest precondition of x = x + 1 and {x > 0}.
More generally, it is possible to determine the weakest precondition for any statement and any postcondition.
Now suppose that you have a function f annotated with preconditions P and postconditions Q:
{P} f {Q}
Define W = wp(f, Q). We know by definition of wp that the following Hoare triple holds:
{W} f {Q}
If we are able to prove that P ⇒ W (this is what is submitted to the theorem prover), then the validity of properties P and Q for f is established.
The WP plugin generates Why logic. As described in section 4 of the "Why3: Shepherd Your Herd of Provers" paper, the operation of Why3 is described as processing proof tasks, which are a sequence of declarations ending with a goal. This is how the Why logic is converted to the input logic of a particular theorem prover.
For a concrete example, the paper gives an overview of transforming Why logic to Z3. Not only is the input language different (Z3 uses SMT-LIB2 syntax), there are significant differences in the logic of Why and Z3. The paper gives the examples that Z3 does not support polymorphism or inductive predicates.
In order to transform Why logic into the input logic of a theorem prover, Why3 uses a series of transformations that gradually transform the Why logic into the target input logic. Why3 uses configuration files known as drivers to define all of the transformations, a pretty printer which outputs the prover's native input format, and regular expressions for interpreting the output of the prover.
Assuming you have run why3config, you can take a look at the automatically-generated .why3.conf config file in your home directory to determine which driver Why3 uses for a particular prover. For example, on my system Why3 uses ~/.opam/system/share/why3/drivers/z3_432.drv when using Z3. z3_432.drv imports the smt-libv2.drv driver as a base driver for SMT-LIB2-compatible provers.
I know that you are aware of examining the generated SMT2, but I figured that I would mention how to do this for anyone who is interested. If you pass the -wp-out DIR and -wp-proof-trace options to frama-c, then WP will save the output from running the prover on individual properties. You can then locate the corresponding .err file for the property of interest. In my case, it's main_assert_final_a_Why3_z3.err. Opening that file in a text editor, you will see something like:
Call_provers: command is: /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
This .smt2 file contains the SMT-LIB2 input to Z3 that Why3 generated.
You can run the command if you would like. In my case, I see:
WARNING: pattern does contain any variable. WARNING: pattern does contain any variable. WARNING: pattern does contain any variable. WARNING: pattern does contain any variable. unsat why3cpulimit time : 0.020000 s
Although slightly counterintuitive, unsat means that the validity of the property is established.
这篇关于将WhyML映射到SMT逻辑的确切机制的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！