How to force a memory location to be valid in ACSL?

Question

I define device accesses as thus

volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS;

I've modeled the accesses using

@ volatile dev->somereg reads somereg_read writes somereg_write;

Now the problem is that when I enable RTE checks, the generated validity checks can't be proved

/*@ assert rte: mem_access: \valid(dev->somereg); */

Is there any way to annotate my code such that MY_DEVICE_ADDRESS up to MY_DEVICE_ADDRESS+sizeof(struct mydevice) is considered valid?

EDIT: Here's an attempt that does not work

#include <stdint.h>

#define MY_DEVICE_ADDRESS (0x80000000)

struct mydevice {
  uint32_t somereg;
  uint32_t someotherreg;
};

volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS;

/*@ axiomatic Physical_Memory {
     axiom Dev: \valid((struct mydevice*)MY_DEVICE_ADDRESS);
  } */

int main(int argc, const char *argv[]) {
  //@ assert \valid(dev);
  //@ assert \false;
  return 0;
}

Run with

frama-c-wp -wp-rte -wp-init-const -wp-model Typed test.c

Answer 1

I think that the only way to have the assertion proved is to put an axiomatic block of the form

/*@ axiomatic Physical_Memory {
     axiom Dev: \valid((struct mydevice*)MY_DEVICE_ADDRESS);
     // add more if you have other physical memory accesses
  } */

There is an option in the kernel -absolute-valid-range <min-max> to indicate that dereferencing a pointer within the given interval is OK, but only EVA is able to take advantage of it (I'm afraid this is too low-level for WP's memory models).

Note in addition that you can pass option -wp-init-const to WP to indicate that it should add in its context the fact the global const variables are always equal to their initial value.

Edit

As mentioned in the comments, the proposed axiom is indeed inconsistent with WP's memory model. The bulk of the issue lies in the fact that in said model a numeric address 0xnnnn is apparently defined as shift(global(0),0xnnnn). As can be seen in e.g. $FRAMAC_SHARE/wp/ergo/Memory.mlw, global(0) has a base of 0, and so has the shift (which modifies only the offset). The definition of valid_rw imposes a strictly positive base, hence the contradiction.

This has to be fixed at WP's level. However, there are a few workarounds available while waiting for a new Frama-C release:

• if you don't need to write to the physical location, you can replace \valid by \valid_read in the axiomatic. Definition of \valid_read in the model does not have the base>0 requirement, hence the axiom will not lead to a contradiction.
• if you can afford modifying the sources, make dev an extern declaration (or define dev as being equal to an extern declaration abstract_dev), and use the abstract constant in the axiom: in this way, you won't have the equality dev.base==0 in the logic model, removing the contradiction.
• finally, you can patch the memory model in $FRAMAC_SHARE/wp/ergo/Memory.mlw (and $FRAMAC_SHARE/wp/why3/Memory.why and $FRAMAC_SHARE/wp/coq/Memory.v depending on your choice of provers). The easiest way to do that would probably to make global rely on an abstract base, as in:

logic global_base: int

function global(b: int) : addr = { base = global_base + b; offset = 0 }

(Note of course that this answer does in no way guarantee that this does not introduce other issues in the model).

Answer 2

Not that I know (I've tried a lot too).

The only workaround I found is:

struct mydevice MY_DEVICE_STRUCT;
volatile struct mydevice * const dev = & MY_DEVICE_STRUCT;

You need to "instantiate" the memory because this is what the underlying LLVM expects. For sure it would be nice to force this through an ACSL notation.