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

Question

The closest answer I found maybe related to -absolute-valid-range for the Eva plugin but is that it? Do I have to come up with read/write ACSL predicates to do dummy read/write?

Sample code:

#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 command and output:

[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]

How to discharge goal "typed_read32_call_mmio_read32_pre" or is this expected?

Strictly speaking, -absolute-valid-range is an option of Frama-C's kernel, even though WP is unable to take advantage of this information as far as I know. That said, there are several possible workarounds and the most appropriate course of action is heavily dependent on your code and the properties you want to prove about it: you need to be more specific in your question (i.e. provide us with a mcve) in order for us to provide meaningful answers. — Virgile
Virgile I updated the question to include the mcve. What I also found the unkown status could be related to volatile variable in the code. Do you know if WP plugin can handle volatile variable? — ratt

Virgile Virgile · Accepted Answer · 2018-10-15T08:39:03

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.

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

1 Answers