frama-c - 如何使用 frama-c Eva 插件或 WP-RTE 验证读取/写入硬件内存映射寄存器 (mmio) 的代码？

Question

我找到的最接近的答案可能与 Eva 插件的 -absolute-valid-range 有关，但真的是这样吗？我是否必须想出读/写 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”或者这是预期的？

Answer 1

证明失败的事实与两个独立的问题有关，但都与使用绝对地址无关。

首先，作为mmio_read32的论证标记为 volatile , WP 认为它的值(value)可以是任何东西。特别是，没有关于 offset 的假设已知在评估 addr 时持有.您可以通过查看生成的目标在 GUI 中看到这一点(进入底部的 WP 目标选项卡并双击 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 的先决条件被设为非严格的，但这同样是非常罕见的)。

关于物理寻址和 volatile 的初始问题，在 ACSL 中(参见 the manual 的第 2.12.1 节)，您有一个特定的 volatile允许您指定(C，通常是 ghost)函数来表示对 volatile 的读写访问的子句位置。不幸的是，目前只能通过非公开分发的插件访问对这些条款的支持。

恐怕如果您想在具有物理地址的代码上使用 WP，您确实需要使用编码(例如，使用适当大小的虚拟数组)和/或使用适当的函数对 volatile 访问进行建模。