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
I think that the only way to have the assertion proved is to put an axiomatic block of the form
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 globalconst
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 asshift(global(0),0xnnnn)
. As can be seen in e.g.$FRAMAC_SHARE/wp/ergo/Memory.mlw
,global(0)
has abase
of0
, and so has theshift
(which modifies only theoffset
). The definition ofvalid_rw
imposes a strictly positivebase
, 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:
\valid
by\valid_read
in the axiomatic. Definition of\valid_read
in the model does not have thebase>0
requirement, hence the axiom will not lead to a contradiction.dev
anextern
declaration (or definedev
as being equal to anextern
declarationabstract_dev
), and use the abstract constant in the axiom: in this way, you won't have the equalitydev.base==0
in the logic model, removing the contradiction.$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 makeglobal
rely on an abstract base, as in:(Note of course that this answer does in no way guarantee that this does not introduce other issues in the model).