Frama-c: проблемы с пониманием моделей памяти WP

Question

Я ищу опции / модель WP, которые позволили бы мне доказать основные манипуляции с памятью C, такие как:

• 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.Кроме того, я видел эту проблему с указателем на пустоту, которая, по-видимому, не очень хорошо обрабатывается WP, по крайней мере, в версии Magnesium.Я еще не пробовал другую версию frama-c, но я думаю, что более новая версия лучше обрабатывает пустые указатели.

Большое спасибо заранее за ваши предложения!

Answer 1

• memcpy

  Рассуждение о результате memcpy (или Frama_C_memcpy) выходит за пределы диапазона текущего плагина WP.Единственная модель памяти, которая будет работать в вашем случае - это Bytes (стр. 13 руководства по хлору), но она не реализована.

  Независимо, обратите внимание, что ваше постусловие из Frama_C_memcpy равно не что вы хотите здесь.Вы утверждаете равенство множеств dest[0..n] и src[0..n].Во-первых, вы должны остановиться на n-1.Во-вторых, и что еще более важно, это слишком слабо и фактически недостаточно для доказательства двух утверждений в вызывающей стороне.То, что вы хотите, это количественное определение всех байтов.См., Например, предикат memcmp в stdlib Frama-C, или вариант \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, в котором допускается несколько приведений.Анализ корректен только , если перед использованием указатель приведен к исходному типу.Идея состоит в том, чтобы разрешить использование некоторых функций libc, которые требуют приведения к void*, но не намного.

  Ваш пример снова немного отличается, потому что вполне вероятно, что MEMORY_ADDR всегда адресуется с типом some_stuct.Было бы приемлемо немного изменить код и изменить свою функцию, используя указатель на этот тип?Таким образом, вы «спрячете» приведение к MEMORY_ADDR внутри функции, которая останется бездоказательной.

Answer 2

Я попробовал этот пример в последней версии Frama-C (конечно, формат немного изменен).

для случая memcpy

Утверждение 2 не выполняется, но утверждение3 успешно доказано (в основном потому, что провал утверждения 2 приводит к ложному предположению, которое доказывает все).

Таким образом, на самом деле оба утверждения не могут быть доказаны, так же как и ваша проблема.

ЭтоВывод обоснован, потому что модели памяти, используемые в плагине wp (насколько я знаю), не предполагают отношения между полями в структуре, т.е. в header_src первые два поля являются 8-битными символами, но они могутне быть вложенным в физическую память, подобную char[2].Вместо этого между ними могут быть отступы (подробное описание см. wiki ).Поэтому, когда вы пытаетесь скопировать биты в такой структуре в другую структуру, Frama-C становится полностью сбитым с толку и понятия не имеет, что вы делаете.

Насколько мне известно, Frama-C не поддерживает какие-либоподход для точного управления макетом памяти, например, gcc PACKED, который вынуждает компилятор удалять отступы.

Я сталкиваюсь с той же проблемой, и решение (совсем не элегантное) - использовать вместо этого массивы.Массивы всегда вложены, поэтому, если вы попытаетесь скопировать char[4] в short[2], я думаю, что утверждение можно доказать.

для Cast pointer to int case

С моделью памятиTyped+cast, текущая версия, которую я использую (Chlorine-20180501), поддерживает приведение между указателями и uint64_t.Возможно, вы захотите попробовать эту версию.

Более того, настоятельно рекомендуется вызывать Z3 и CVC4 через Why3, производительность которого, безусловно, лучше, чем у Alt-Ergo.