具有Frama-C和Eva的动态阵列 [英] Dynamic array with Frama-C and Eva

问题描述

在 https://stackoverflow.com/a/57116260/946226 中，我学习了如何验证功能 foo 在缓冲区上运行（由开始和结束指针给定）实际上只能读取它，但是会创建一个代表性的 main 调用它的函数：

In https://stackoverflow.com/a/57116260/946226 I learned how to verify that a function foo that operates on a buffer (given by a begin and end pointer) really only reads form it, but creating a representative main function that calls it:

#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);
}

但这不会捕获仅在缓冲区很短时出现的错误。

but this does not catch bugs that only appear when the buffer is very short.

我尝试了以下操作：

#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);

我可以使其工作吗？

推荐答案

正如anol的评论中所述，Eva中没有可用的抽象域能够跟踪 n 与长度之间的关系 malloc 返回的内存块的大小。因此，从所有实际目的出发，在这种情况下都不可能摆脱对现实生活分析的警告。一般而言，准备一个初始状态很重要，该初始状态会导致整个程序所操纵的缓冲区的精确边界（而内容可以保持更抽象）。

As mentioned in anol's comment, none of the abstract domains available within Eva is capable of keeping track of the relation between n and the length of the memory block returned by malloc. Hence, for all practical purposes, it will not be possible to get rid of the warning in such circumstances for a real-life analysis. Generally speaking, it is important to prepare an initial state which leads to precise bounds for the buffer that are manipulated throughout the program (while the content can stay much more abstract).

也就是说，用于较小的实验，如果您不介意浪费（很多）CPU周期，则可以通过基本指示Eva考虑每个可能的长度来作弊一些分别。这是通过一些注释和命令行选项完成的（仅Frama-C 19.0 Potassium）

That said, for smaller experiments, and if you don't mind wasting (quite a lot of) CPU cycles, it is possible to cheat a little bit, by basically instructing Eva to consider each possible length separately. This is done by a few annotations and command-line options (Frama-C 19.0 Potassium only)

#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);
  }
}

使用$ $ b启动Frama-C
$ b

Launch Frama-C with

  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不会拆分）。 // @循环展开n 要求展开循环 n 次，而不是合并所有步骤的结果。

In the code, //@ split n indicates that Eva should consider separately each possible value of n at this point. It goes along with the -eva-split-limit 256 (by default, Eva won't split if the expression can have more than 100 values). //@ loop unroll n ask to unroll the loop n times instead of merging results for all steps.

对于其他命令行选项， -eva-precision 7 将控制Eva精度的各种参数设置为合理的值。它的范围从 0 （精确度低于默认值）到 11 （最大精度-请勿在任何情况下尝试使用）十几行）。 -eva-builtin malloc：Frama_C_malloc_fresh 指示Eva为遇到的对 malloc 的任何调用创建一个新的基地址。否则，您将获得所有长度的单一基数，从而打败了首先在 n 上进行拆分的目的。

For the other command-line options, -eva-precision 7 sets the various parameters controlling Eva precision to sensible values. It goes from 0 (less precise than default) up to 11 (maximal precision - don't try it on anything more than a dozen of lines). -eva-builtin malloc:Frama_C_malloc_fresh instructs Eva to create a fresh base address for any call to malloc it encounters. Otherwise, you'd get a single base for all lengths, defeating the purpose of splitting on n in the first place.

这篇关于具有Frama-C和Eva的动态阵列的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！