Frama-c：无法理解 WP 内存模型

Question

我正在寻找可以让我证明基本的 C 内存操作的 WP options/model，例如：

memcpy : 我试图证明这个简单的代码 :

struct header_src{
  char t1;
  char t2;
  char t3;
  char t4;
};

struct header_dest{
  short t1;
  short t2;
};

/*@ requires 0<=n<=UINT_MAX;
  @ requires \valid(dest);
  @ requires \valid_read(src);
  @ assigns (dest)[0..n-1] \from (src)[0..n-1];
  @ assigns \result \from dest; 
  @ ensures dest[0..n] == src[0..n];
  @ ensures \result == dest;
*/
void* Frama_C_memcpy(char *dest, const char *src, uint32_t n);

int main(void)
{
  struct header_src p_header_src;
  struct header_dest p_header_dest;
  p_header_src.t1 = 'e';
  p_header_src.t2 = 'b';
  p_header_src.t3 = 'c';
  p_header_src.t4 = 'd';

  p_header_dest.t1 = 0x0000;
  p_header_dest.t2 = 0x0000;

  //@ assert \valid(&p_header_dest);

  Frama_C_memcpy((char*)&p_header_dest, (char*)&p_header_src, sizeof(struct header_src));
  //@ assert p_header_dest.t1 == 0x6265;
  //@ assert p_header_dest.t2 == 0x6463;
}

但是最后两个断言没有被 WP 验证（使用默认证明 Alt-Ergo）。它可以通过值分析来证明，但我更希望能够不使用抽象解释来证明代码。

Cast pointer to int ：因为我正在编写嵌入式代码，所以我希望能够指定如下内容：

#define MEMORY_ADDR 0x08000000
#define SOME_SIZE 10
struct some_struct {
    uint8_t field1[SOME_SIZE];
    uint32_t field2[SOME_SIZE];
}
// [...]
// some function body {
    struct some_struct *p = (some_struct*)MEMORY_ADDR;
    if(p == NULL) {
        // Handle error
    } else {
        // Do something
    }
// } body end

我稍微看了看 WP 的文档，我使用的 frama-c 版本 (Magnesium-20151002) 似乎有几种内存模型（Hoare、Typed、+cast、+ref、.. .) 但给定示例的 none 已通过上述任何模型得到证明。文档中明确指出 Typed 模型不处理指向 int 的指针转换。我很难理解每个 wp-model 背后到底发生了什么。如果我能够验证至少 post-memcpy 函数的条件，那将对我有很大帮助。

此外，我已经看到 this 关于 void 指针的问题，至少在 Magnesium 版本中，WP 显然没有很好地处理这些问题。我还没有尝试过其他版本的 frama-c，但我认为较新的版本可以更好地处理 void 指针。

非常感谢您的建议！

Answer 1

我在最新版的Frama-C中试过这个例子（当然格式稍微修改了一下）

对于 `memcpy` 案例

断言 2 失败但断言 3 被成功证明（主要是因为断言 2 的失败导致错误假设，这证明了一切）。

所以其实这两个说法都无法证明，和你的问题一样。

这个结论是合理的，因为 wp 插件中使用的内存模型（据我所知）没有假设结构中字段之间的关系，即在 header_src 中第一个两个字段是 8 位字符，但它们可能不会像 char[2] 那样在物理内存中嵌套组织。相反，它们之间可能有填充（有关详细说明，请参阅 wiki）。因此，当您尝试将此类结构中的位复制到另一个结构时，Frama-C 变得完全混乱并且不知道您在做什么。

就我而言，Frama-C 不支持任何精确控制内存布局的方法，例如gcc 的 PACKED 强制编译器删除填充。

我面临同样的问题，（一点也不优雅）解决方案是，改用数组。数组总是嵌套的，所以如果你试图将一个char[4]复制到一个short[2]，我认为这个断言是可以证明的。

对于 `Cast pointer to int` 案例

使用内存模型 Typed+cast，我使用的当前版本 (Chlorine-20180501) 支持指针和 uint64_t 之间的转换。您可能想试试这个版本。

另外，强烈建议通过why3调用Z3和CVC4，性能肯定比Alt-Ergo好

Answer 2

memcpy

推理memcpy（或Frama_C_memcpy）的结果超出了当前WP插件的范围。唯一适用于您的情况的内存模型是 Bytes（氯手册第 13 页），但未实现。

请注意，Frama_C_memcpy 中的后置条件不是您在这里想要的。您断言集合 dest[0..n] 和 src[0..n] 相等。首先，您应该停在 n-1。其次，更重要的是，这太弱了，实际上不足以证明调用者的两个断言。你想要的是对所有字节的量化。参见例如Frama-C 的标准库中的谓词 memcmp，或变体 \forall int i; 0 <= i < n -> dest[i] == src[i];

顺便说一句，只有当 dest 和 src 正确分开时，此后置条件才成立，而您的函数不需要这样做。否则，你应该写dest[i] == \at (src[i], Pre)。而且你的 requires 也因为另一个原因太弱了，因为你只要求第一个字符有效，而不是 n 第一个字符。
将指针转换为 int

基本上，当前在 WP 中实现的所有模型都无法推理使用多个不兼容类型（通过使用联合或指针转换）访问内存的代码。在某些情况下，比如Typed，会在语法上检测到强制转换，并发出警告，警告无法分析代码。 Typed+Cast 模型是 Typed 的变体，其中一些类型转换被接受。如果指针在使用前被重新转换为它的原始类型，分析是正确的只有。这个想法是允许使用一些需要转换为 void* 的 libc 函数，但仅此而已。

你的例子又有点不同，因为 MEMORY_ADDR 很可能总是用类型 some_stuct 来寻址。稍微更改代码并将您的函数更改为采用指向此类型的指针是否可以接受？这样，您将在一个尚未证明的函数中 "hide" 转换为 MEMORY_ADDR。

Frama-c：无法理解 WP 内存模型

Frama-c : Trouble understanding WP memory models

frama-c

对于 memcpy 案例

对于 Cast pointer to int 案例

对于 `memcpy` 案例

对于 `Cast pointer to int` 案例