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

Question

我找到的最接近的答案可能与 Eva 插件的 -absolute-valid-range 有关，但真的是这样吗？我是否必须想出 read/write ACSL 谓词来做虚拟 read/write？

示例代码：

#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

The fact that the proof fails is related to two independent issues, but none of them is related to using absolute addresses.

First, as the argument of mmio_read32 is marked as volatile, WP consider that its value can be anything. In particular, none of the hypotheses that are made on offset are known to hold when evaluating addr. You can see that in the GUI by looking at the generated goal (go in the WP Goals tab at the bottom and double click in the Script colon and the line of the failed proof attempt):

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 and w_1 correspond to two read accesses to the volatile content of addr. I'm not sure if you really intended the addr parameter to be volatile (as opposed to a non-volatile pointer to a volatile location), as this would require a pretty weird execution environment.

Assuming that the volatile qualifier should not present in the declaration of addr, a remaining issue is that the constraint on offset in read32 is too weak: it should read offset < 0x1000 with a strict inequality (or the precondition of mmio_read32 be made non-strict, but again this would be quite uncommon).

Regarding the initial question about physical adressing and volatile, in ACSL (see section 2.12.1 of the manual), you have a specific volatile clause that allows you to specify (C, usually ghost) functions to represent read and write accesses to volatile locations. Unfortunately, support for these clauses is currently only accessible through a non-publicly distributed plug-in.

I'm afraid that if you want to use WP on code with physical adressing, you need indeed to use an encoding (e.g. with a ghost array of appropriate size), and/or model volatile accesses with appropriate functions.

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

How to validate code that read/write to hardware memory mapped registers (mmio) with frama-c Eva plugin or WP-RTE?

frama-c