Появляется плагин для фрагментирования c, который отбрасывает используемые значения - PullRequest
Новая
       69

Появляется плагин для фрагментирования c, который отбрасывает используемые значения

2 голосов
/ 04 мая 2020

Описание проблемы

Я разрабатываю плагин frama- c, который использует плагин для нарезки в виде библиотеки для удаления неиспользуемых битов автоматически сгенерированного кода. К сожалению, плагин слайсинга сбрасывает кучу значений стека, которые фактически используются. Они используются, поскольку их адреса содержатся в структурах, предназначенных для абстрактных внешних функций.

Простой пример

Это более простой пример, который моделирует ту же общую структуру, что и я. 

/* Abstract external function */
void some_function(int* ints[]);

int main() {
  int i;
  int *p = &i;
  int *a[] = { &p };
  some_function(a);
  return 0;
}

При нарезке этого примера с помощью frama-c-gui -slice-calls some_function experiment_slicing.c (я не понимаю, как увидеть результат среза при вызове командной строки без gui), он отбрасывает все, кроме объявления int *a[]; и вызов some_function.

Попытки исправить

Я попытался исправить это, добавив аннотации ACSL. Однако то, что я считал разумной спецификацией (см. Ниже), не сработало 

/*@ requires \valid(ints) && \valid(ints[0]);
 */
void some_function(int* ints[]);

Затем я попытался с заданием (см. Ниже), которое имеет желаемое поведение. однако это не правильная спецификация, так как функция никогда не записывает указатель, а должна прочитать ее для корректной работы. Я обеспокоен тем, что, если я продвинусь с такой неправильной спецификацией, это приведет к странным проблемам в будущем. 

/*@ requires \valid(ints) && \valid(ints[0]);
   assigns  *ints;
*/
void some_function(int* ints[]);

1 Ответ

1 голос
/ 05 мая 2020

Вы на правильном пути: это пункт assigns, который вы должны использовать здесь: он будет указывать, какие части состояния памяти связаны с вызовом неопределенной функции. Однако необходимо предоставить полное предложение assigns с его частью \from (которая указывает, какая ячейка памяти считывается для вычисления нового значения ячейки памяти, записанной в).

Я добавил int переменная для вашего примера, так как ваша функция не возвращает результат (void тип возврата). Для функции, которая возвращает что-то, вы также должны иметь предложение assigns \result \from ...;: 

int x;

/*@ assigns x \from indirect:ints[..], *(ints[..]); */
void some_function(int* ints[]);

int main() {
  int i;
  int*p = &i;
  int *a[] = { &p };
  some_function(a);
  return 0;
}

Предложение assigns указывает, что some_function может изменить значение x, и что новый значение будет вычислено из адресов, сохраненных в ints[..] (метка indirect говорит о том, что мы не используем их значение напрямую, это более подробно описано в разделе 8.2 руководства Евы ), и их содержимое.

с использованием frama-c -slice-calls some_function file.c -then-last -print (здесь приведены последние аргументы для печати результирующего файла на стандартном выводе: -then-last указывает, что следующие опции должны работать с последним созданным проектом Frama- C, в этом случае тот, который получен в результате нарезки, и -print печатает код C указанного проекта. Вы также можете использовать -ocode output.c для перенаправления симпатичной печати кода в output.c.) дает следующий результат : 

* Generated by Frama-C */
void some_function(int **ints);

void main(void)
{
  int i;
  int *p = & i;
  int *a[1] = {(int *)(& p)};
  some_function(a);
  return;
}

Кроме того, обратите внимание, что ваш пример напечатан неправильно: &p является указателем на указатель на int и, следовательно, должен храниться в массиве int**, а не * 10 31 * массив. Но я предполагаю, что это связано только с уменьшением вашего исходного примера и не имеет большого значения для нарезки.

...