Как проверить код, который считывает / записывает в регистры отображения аппаратной памяти (mmio) с помощью плагина Eva frama-c или WP-RTE? - PullRequest
Новая
       30

Как проверить код, который считывает / записывает в регистры отображения аппаратной памяти (mmio) с помощью плагина Eva frama-c или WP-RTE?

0 голосов
/ 08 октября 2018

Ближайший ответ, который я нашел, может быть связан с -absolute-valid-range для плагина Eva, но так ли это?Нужно ли придумывать предикаты ACSL для чтения / записи, чтобы сделать фиктивное чтение / запись?

Пример кода: 

#include <stdint.h>

#define BASE_ADDR 0x0e000000
#define BASE_LIMIT 0x0e001000
#define TEST_REG 0x10

/*@ requires BASE_ADDR <= addr < BASE_LIMIT;
  @ assigns \nothing;
 */
static inline uint32_t mmio_read32(volatile uintptr_t addr)
{
    volatile uint32_t *ptr = (volatile uint32_t *)addr;
    return *ptr;
}
/*@
  @ requires 0 <= offset <= 0x1000;
  @ assigns \nothing;
 */
static inline uint32_t read32(uintptr_t offset)
{
    return mmio_read32((uintptr_t)BASE_ADDR + offset);
}

void main(){
    uint32_t test;
    test = read32(TEST_REG);
    return;
}

Команда Frama-c и вывод: 

[frama -absolute-valid-range 0x0e000000-0x0e001000 -wp mmio2.c
[kernel] Parsing mmio2.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_read32_call_mmio_read32_pre : Unknown (Qed:4ms) (51ms)
[wp] Proved goals:    5 / 6
   Qed:             5
   Alt-Ergo:        0  (unknown: 1)][1]

Как выполнить цель "typed_read32_call_mmio_read32_pre" или это ожидается?

1 Ответ

0 голосов
/ 15 октября 2018

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

Во-первых, аргумент mmio_read32 помечен как volatile, WPУчтите, что его значением может быть что угодно.В частности, известно, что ни одна из гипотез, выдвинутых на offset, не выполняется при оценке addr.Вы можете увидеть это в графическом интерфейсе, посмотрев на сгенерированную цель (перейдите на вкладку WP Goals внизу и дважды щелкните двоеточие Script и строку неудачной попытки доказательства): 

Goal Instance of 'Pre-condition'
 (call 'mmio_read32'):
Assume {
  Type: is_uint32(offset_0).
  (* Pre-condition *)
  Have: (0 <= offset_0) /\ (offset_0 <= 4095).
}
Prove: (234881024 <= w) /\ (w_1 <= 234885119).

w и w_1 соответствуют двум доступам чтения к изменчивому содержимому addr.Я не уверен, действительно ли вы предполагали, что параметр addr будет volatile (в отличие от не volatile указателя на местоположение volatile), поскольку для этого потребуется довольно странная среда выполнения.

Предполагая, что квалификатор volatile не должен присутствовать в объявлении addr, остается проблема в том, что ограничение на offset в read32 слишком слабое: оно должно читать offset < 0x1000 со строгимнеравенство (или предварительное условие mmio_read32 должно быть сделано нестрогим, но, опять же, это было бы довольно редко).

Относительно первоначального вопроса о физической адресации и энергозависимости в ACSL (см. раздел 2.12.1 *)1028 * руководство ), у вас есть специальное предложение volatile, которое позволяет вам задавать (C, обычно призрачные) функции для представления доступа для чтения и записи в volatile местоположениях.К сожалению, поддержка этих предложений в настоящее время доступна только через не публично распространяемый плагин.

Боюсь, что если вы хотите использовать WP в коде с физической адресацией, вам действительно нужно использовать кодировку(например, с массивом-призраком соответствующего размера) и / или изменяемым доступом модели с соответствующими функциями.

...