Динамический массив с Frama-C и Eva

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

Могу ли я заставить его работать?


c static-analysis dynamic-memory-allocation memory-access frama-c
person Joachim Breitner    schedule 23.07.2019    source источник
comment
Мне придется перепроверить это позже, но я боюсь, что вам нужен реляционный инвариант между значением n, используемым в вызове malloc, и циклом. Без возможности сохранить этот инвариант Ева не может сделать вывод, что размер, используемый для выделения динамического массива, совпадает с размером цикла. В настоящее время в Eva есть несколько слабых реляционных доменов, но я боюсь, что они не в состоянии поддерживать эту информацию.   -  person anol    schedule 23.07.2019

Ответы (1)


arrow_upward
1
arrow_downward

Как упоминалось в комментарии anol, ни один из абстрактных доменов, доступных в Eva, не способен отслеживать отношение между n и длиной блока памяти, возвращаемого malloc. Следовательно, для всех практических целей избавиться от предупреждения в таких обстоятельствах для реального анализа будет невозможно. Вообще говоря, важно подготовить начальное состояние, которое приводит к точным границам для буфера, которым манипулируют на протяжении всей программы (в то время как содержимое может оставаться гораздо более абстрактным).

Тем не менее, для небольших экспериментов, и если вы не возражаете тратить (довольно много) процессорных циклов, можно немного схитрить, в основном инструктируя Еву рассматривать каждую возможную длину отдельно . Это делается с помощью нескольких аннотаций и параметров командной строки (только для 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 указывает, что Ева должна рассмотреть отдельно каждое возможное значение n на данном этапе. Это соответствует -eva-split-limit 256 (по умолчанию Eva не будет разделяться, если выражение может иметь более 100 значений). //@ loop unroll n попросите развернуть цикл n раз вместо объединения результатов для всех шагов.

Для других параметров командной строки -eva-precision 7 устанавливает различные параметры, контролирующие точность Eva, в разумные значения. Она изменяется от 0 (менее точная, чем по умолчанию) до 11 (максимальная точность — не пытайтесь использовать ее более чем на дюжине строк). -eva-builtin malloc:Frama_C_malloc_fresh инструктирует Eva создавать новый базовый адрес для любого обращения к malloc, которое она встречает. В противном случае вы получите единую базу для всех длин, что в первую очередь сведет на нет цель разделения на n.

person Virgile    schedule 24.07.2019
comment
Спасибо, это разблокирует меня. Я могу бегать на длинах от 1 до 10 100, что неплохо для начала. - person Joachim Breitner; 24.07.2019