Как заставить область памяти быть действительной в ACSL?

Я определяю доступ к устройству следующим образом

volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS;

Я смоделировал доступ с помощью

@ volatile dev->somereg reads somereg_read writes somereg_write;

Теперь проблема в том, что когда я включаю проверки RTE, сгенерированные проверки достоверности не могут быть доказаны

/*@ assert rte: mem_access: \valid(dev->somereg); */

Есть ли способ аннотировать мой код так, чтобы MY_DEVICE_ADDRESS вплоть до MY_DEVICE_ADDRESS+sizeof(struct mydevice) считался действительным?

РЕДАКТИРОВАТЬ: Вот попытка, которая не работает

#include <stdint.h>

#define MY_DEVICE_ADDRESS (0x80000000)

struct mydevice {
  uint32_t somereg;
  uint32_t someotherreg;
};

volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS;

/*@ axiomatic Physical_Memory {
     axiom Dev: \valid((struct mydevice*)MY_DEVICE_ADDRESS);
  } */

int main(int argc, const char *argv[]) {
  //@ assert \valid(dev);
  //@ assert \false;
  return 0;
}

Бежать с

frama-c-wp -wp-rte -wp-init-const -wp-model Typed test.c

Источник

2 ответа

Решение

Я думаю, что единственный способ доказать утверждение - это поставить аксиоматический блок вида

/*@ axiomatic Physical_Memory {
     axiom Dev: \valid((struct mydevice*)MY_DEVICE_ADDRESS);
     // add more if you have other physical memory accesses
  } */

Есть опция в ядре -absolute-valid-range <min-max> чтобы указать, что разыменование указателя в данном интервале - это нормально, но только EVA может воспользоваться этим (боюсь, это слишком низкий уровень для моделей памяти WP).

Обратите внимание, что вы можете передать опцию -wp-init-const WP, чтобы указать, что он должен добавить в своем контексте тот факт, что глобальный const переменные всегда равны их начальному значению.

редактировать

Как уже упоминалось в комментариях, предложенная аксиома действительно несовместима с моделью памяти WP. Основная проблема заключается в том, что в указанной модели числовой адрес 0xnnnn по-видимому, определяется как shift(global(0),0xnnnn), Как видно на примере $FRAMAC_SHARE/wp/ergo/Memory.mlw, global(0) имеет base из 0и так shift (который изменяет только offset). Определение valid_rw накладывает строго положительный baseотсюда и противоречие.

Это должно быть исправлено на уровне WP. Тем не менее, есть несколько обходных путей в ожидании новой версии Frama-C:

  • если вам не нужно писать в физическое местоположение, вы можете заменить \valid от \valid_read в аксиоматическом. Значение \valid_read в модели нет base>0 требование, следовательно, аксиома не приведет к противоречию.
  • если вы можете позволить себе изменение источников, сделайте dev extern декларация (или определение dev как равный extern декларация abstract_dev), и используйте абстрактную константу в аксиоме: таким образом, у вас не будет равенства dev.base==0 в логической модели, устраняя противоречие.
  • наконец, вы можете исправить модель памяти в $FRAMAC_SHARE/wp/ergo/Memory.mlw (а также $FRAMAC_SHARE/wp/why3/Memory.why а также $FRAMAC_SHARE/wp/coq/Memory.v в зависимости от вашего выбора пруверов). Самый простой способ сделать это, вероятно, сделать global полагаться на абстрактную базу, как в:
логика global_base: int

функция global(b: int): addr = { base = global_base + b; смещение = 0}

(Обратите внимание, что этот ответ никоим образом не гарантирует, что это не приведет к появлению других проблем в модели).

Источник

Не то чтобы я знал (я тоже много пробовал).

Единственный обходной путь, который я нашел:

struct mydevice MY_DEVICE_STRUCT;
volatile struct mydevice * const dev = & MY_DEVICE_STRUCT;

Вам нужно "создать экземпляр" памяти, потому что именно этого ожидает базовый LLVM. Наверняка было бы неплохо форсировать это через нотацию ACSL.

Источник
Другие вопросы по тегам