如何使用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 认为它的值可以是任何值。特别是，在评估addr 时，已知对offset 所做的假设都不成立。您可以通过查看生成的目标在 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 的声明中，剩下的问题是read32 中对offset 的约束太弱：它应该读作offset < 0x1000 并具有严格的不等式（或者 mmio_read32 的前提条件是非严格的，但这又是很不常见的）。

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

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