满足 memcpy 的证明义务？ [Frama-C]

Question

我们一直在使用 Frama-C 对商业项目进行 'experimental' 静态分析（集成到我们的 CI 中，很少在整个代码库的一小部分进行选择性阻塞检查。

出现的障碍之一与满足 wp 插件在遇到 memcpy 调用时生成的证明义务有关。具体包括以下三项义务：

从 'goal' 注释看来，Frama-C 试图证明目标内存和源内存是有效的，.

我试过添加 requires \valid() 前提条件，但这似乎没有帮助。在这些情况下，被测函数内的 memcpy 调用将数据从输入参数复制到函数，并将该数据放入局部变量（在函数范围内）。

更复杂的是，复制数据的局部变量是打包结构中的一个属性。

具体来说，我希望有人能够分享一些 memcpy 使用的真实示例，这些示例可以满足 wp 引入的目标（例如，我必须添加哪些先决条件使其可证明？）

如果重要的话，我是运行 Frama-C Magnesium-20151002（根据 apt-get 在 Ubuntu 16 上的说法，这是 'up to date'），并使用以下参数调用：

frama-c -wp -wp-split -wp-dynamic -lib-entry -wp-proof alt-ergo -wp-report

也相关，但缺少一个清晰的工作示例：

Answer 1

正如您在评论中提到的，正确的解决方案是使用 -wp-model "Typed+Cast" 让 WP 接受强制转换 to/from void*（更准确地说，它会认为 p和(void*)p对于任何指针都是一样的，这足以证明memcpy的requires）。现在，正如中提到的你链接到的问题，这个内存模型的主要问题（以及它不是默认的原因）是它 本质上不安全 ：它依赖于根据定义无法由 WP 本身评估的假设。这是一个强调此问题的小示例：

int x;
char* c;

/*@ assigns c;
    ensures c == ((char *)&x);
*/
void g(void) {
  c = &x;
}

/*@ assigns \nothing;
    ensures \separated(&x,c);
*/
void f() {
}

void main () {
g();
f();
//@ assert \false;
}

基本上，默认的 Typed 内存模型确保了 c 和 x 指向的位置之间的分离（即 [=20 的 post 条件） =]), 因为 int 和 char 是不同的，你既不能证明 g 的 post 条件，也不能将其作为假设来推导 \false 在 main 中，因为模型中根本无法表达等式。

现在，如果您使用 Typed+Cast，g 的 post 条件现在已被正确理解，并且证明起来完全微不足道。 WP 不会让你同时证明 &x 和 c 是分开的，因为它们一起参与一个赋值。然而，在 f 中不存在这样的分配，并且 post 条件也很容易证明，导致在 main 中证明 \false 因为我们有两个关于 &x 和 c。更一般地说，WP 依赖于本地别名分析来跟踪不同类型的指针之间的潜在别名（全局分析会破坏拥有模块化分析器的目的）。因此，传递选项 -wp-model +Cast 可以被视为告诉 WP "Trust me, the program won't create miss-typed aliases" 的方式。然而，可以手动传递别名信息（或借助例如尚未编写的全局别名检测插件）。例如，使用选项 -wp-alias-vars x,c，f 的 post 条件变为 Unknown（即 &x 和 c 之间的分隔不是假设不再，甚至 f).

满足 memcpy 的证明义务？ [Frama-C]

Satisfying Proof Obligations for memcpy? [Frama-C]

frama-c