c - 采用 Frama-C 和 Eva 的动态阵列

Question

在 https://stackoverflow.com/a/57116260/946226我学习了如何验证在缓冲区(由开始和结束指针给出)上操作的函数 foo 确实只读取它，但创建一个代表性的 main 函数称之为:

#include <stddef.h>

#define N 100
char test[N];

extern char *foo(char *, char *);

int main() {
  char* beg, *end;
  beg = &test[0];
  end = &test[0] + N;
  foo(beg, end);
}

但这并不能捕获仅在缓冲区非常短时出现的错误。

我尝试了以下方法:

#include <stddef.h>
#include <stdlib.h>
#include "__fc_builtin.h"

extern char *foo(char *, char *);

int main() {
  int n = Frama_C_interval(0, 255);
  uint8_t *test = malloc(n);
  if (test != NULL) {
    for (int i=0; i<n; i++) test[i]=Frama_C_interval(0, 255);

    char* beg, *end;
    beg = &test[0];
    end = &test[0] + n;
    foo(beg, end);
  }
}

但这不起作用:

[eva:alarm] frama-main.c:14: Warning: 
  out of bounds write. assert \valid(test + i);

我可以让它工作吗？

Answer 1

正如 anol 的评论中提到的，Eva 中可用的抽象域都无法跟踪 n 与 malloc 返回的内存块的长度之间的关系>。因此，出于所有实际目的，在这种情况下进行现实分析时不可能消除警告。一般来说，准备一个初始状态非常重要，它可以为整个程序中操作的缓冲区提供精确的边界(同时内容可以保持更加抽象)。

也就是说，对于较小的实验，如果您不介意浪费(相当多的)CPU 周期，则可以通过基本上指示 Eva 考虑每个可能的长度分开。这是通过一些注释和命令行选项完成的(仅限 Frama-C 19.0 Potassium)

#include <stdint.h>
#include <stddef.h>
#include <stdlib.h>
#include "__fc_builtin.h"

extern char *foo(char *, char *);

int main() {
  int n = Frama_C_interval(0, 255);
  //@ split n;
  uint8_t *test = malloc(n);
  if (test != NULL) {
    //@ loop unroll n;
    for (int i=0; i<n; i++) {
      Frama_C_show_each_test(n, i, test);
      test[i]=Frama_C_interval(0, 255);
    }
    char* beg, *end;
    beg = &test[0];
    end = &test[0] + n;
    foo(beg, end);
  }
}

启动 Frama-C

  frama-c -eva file.c \
          -eva-precision 7 \
          -eva-split-limit 256 \
          -eva-builtin malloc:Frama_C_malloc_fresh

代码中，//@ split n表示此时Eva应该单独考虑n的每个可能值。它与 -eva-split-limit 256 一起使用(默认情况下，如果表达式可以有超过 100 个值，Eva 不会拆分)。 //@loop unroll n 要求展开循环 n 次，而不是合并所有步骤的结果。

对于其他命令行选项，-eva- precision 7 将控制 Eva 精度的各种参数设置为合理值。它的范围从 0 (低于默认值)到 11 (最大精度 - 不要在超过十几行的情况下尝试)。 -eva-builtin malloc:Frama_C_malloc_fresh 指示 Eva 为它遇到的任何对 malloc 的调用创建一个新的基地址。否则，您将得到所有长度的单一碱基，从而违背了在 n 上拆分的目的。