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

Question

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

• 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）。可以通过值分析来证明，但我最希望能够不使用抽象解释来证明代码。

• 将指针转换为 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, ...)但是上面的任何模型都没有证明给定的例子。文档中明确指出 Typed 模型不处理指向 int 的指针转换。我很难理解每个 wp 模型的引擎盖下到底发生了什么。如果我能够至少验证 memcpy 函数的后置条件，那真的会对我有所帮助。

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

非常感谢您的建议！

Answer 1

• memcpy

  推理memcpy（或Frama_C_memcpy）的结果超出了当前WP插件的范围。唯一适用于您的情况的内存模型是 Bytes（Chlorine 手册的第 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 的变体，其中接受 some 演员表。 仅在指针在使用之前被重新转换为其原始类型时分析是正确的。这个想法是允许使用一些需要转换为 void* 的 libc 函数，但仅此而已。

  您的示例再次有点不同，因为MEMORY_ADDR 很可能总是使用some_stuct 类型寻址。稍微更改代码并将函数更改为指向此类型的指针是否可以接受？这样，您将“隐藏”到 MEMORY_ADDR 的演员表在一个尚未得到证实的函数中。

Answer 2

我在最新版本的 Frama-C 中尝试过这个例子（当然格式稍作修改）。

对于memcpy 案例

断言 2 失败但断言 3 被成功证明（基本上是因为断言 2 失败导致 False 假设，这证明了一切）。

所以事实上这两个断言都不能被证明，就像你的问题一样。

这个结论是合理的，因为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。