Handling arrays inside structs.

[isubasinghe]

Hey, just had a quick question because I've been failing to verify this.
To me the obvious perm here is to just add Perm(&tx_queue_clients[client],size, read) but VerCors doesn't currently accept this.

What can I do to get this code verified?

Thanks

#include <stdint.h>
#define DRIVER 0
#define CLIENT_CH 1
#define NUM_CLIENTS 3
#define NET_BUFFER_SIZE 2048

struct net_buff_desc {
    /* offset of buffer within buffer memory region or io address of buffer */
    uint64_t io_or_offset;
    /* length of data inside buffer */
    uint16_t len;
};

struct net_queue {
    /* index to insert at */
    uint16_t tail;
    /* index to remove from */
    uint16_t head;
    /* flag to indicate whether consumer requires signalling */
    uint32_t consumer_signalled;
    /* buffer descripter array */
    struct net_buff_desc buffers[];
};

struct net_queue_handle {
     /* available buffers */
    struct net_queue *free;
     /* filled buffers */
    struct net_queue *active;
    /* size of the queues */
    uint32_t size;
};


uintptr_t tx_free_drv;
uintptr_t tx_active_drv;
uintptr_t tx_free_arp;
uintptr_t tx_active_arp;
uintptr_t tx_free_cli0;
uintptr_t tx_active_cli0;
uintptr_t tx_free_cli1;
uintptr_t tx_active_cli1;

uintptr_t buffer_data_region_arp_vaddr;
uintptr_t buffer_data_region_cli0_vaddr;
uintptr_t buffer_data_region_cli1_vaddr;

uintptr_t buffer_data_region_arp_paddr;
uintptr_t buffer_data_region_cli0_paddr;
uintptr_t buffer_data_region_cli1_paddr;

struct state {
    struct net_queue_handle tx_queue_drv;
    struct net_queue_handle tx_queue_clients[NUM_CLIENTS];
    uintptr_t buffer_region_vaddrs[NUM_CLIENTS];
    uintptr_t buffer_region_paddrs[NUM_CLIENTS];
};

/*@
  context phys != NULL ** Perm(phys, read);
  context gstate != NULL ** Perm(gstate, read);
  context Perm(gstate->buffer_region_paddrs, read);
  context Perm(gstate->buffer_region_vaddrs, read);
  context Perm(gstate->tx_queue_clients, read);
  context \pointer(gstate->buffer_region_paddrs, 3, read);
  context \pointer(gstate->buffer_region_vaddrs, 3, read);
  context \pointer(gstate->tx_queue_clients, 3, read);
 @*/
int extract_offset(uintptr_t *phys, struct state *gstate)
{

    int myphys = *phys;
    uintptr_t *paddrs = gstate->buffer_region_paddrs;
    uintptr_t *vaddrs = gstate->buffer_region_vaddrs;
    struct net_queue_handle *tx_queue_clients = gstate->tx_queue_clients;
    for (int client = 0; client < NUM_CLIENTS; client++) 
    /*@
     context paddrs != NULL;
     context Perm(&paddrs[client], read);
     context Perm(&vaddrs[client], read);
     context Perm(&tx_queue_clients[client], read);
    @*/
    {
        if (myphys >= paddrs[client] &&
            myphys <  paddrs[client] + tx_queue_clients[client].size * NET_BUFFER_SIZE) {
            return client;
        }
    }

    return -1;
}

void init() {
}

[superaxander]

Yes this is a bit of a confusing thing but what you actually need is Perm(tx_queue_clients[client].size, read) without the &.

The following verifies for me with the flag --no-infer-heap-context-into-frame (needed due to #1101)

#include <stdint.h>
#define DRIVER 0
#define CLIENT_CH 1
#define NUM_CLIENTS 3
#define NET_BUFFER_SIZE 2048

struct net_buff_desc {
    /* offset of buffer within buffer memory region or io address of buffer */
    uint64_t io_or_offset;
    /* length of data inside buffer */
    uint16_t len;
};

struct net_queue {
    /* index to insert at */
    uint16_t tail;
    /* index to remove from */
    uint16_t head;
    /* flag to indicate whether consumer requires signalling */
    uint32_t consumer_signalled;
    /* buffer descripter array */
    struct net_buff_desc buffers[];
};

struct net_queue_handle {
     /* available buffers */
    struct net_queue *free;
     /* filled buffers */
    struct net_queue *active;
    /* size of the queues */
    uint32_t size;
};


uintptr_t tx_free_drv;
uintptr_t tx_active_drv;
uintptr_t tx_free_arp;
uintptr_t tx_active_arp;
uintptr_t tx_free_cli0;
uintptr_t tx_active_cli0;
uintptr_t tx_free_cli1;
uintptr_t tx_active_cli1;

uintptr_t buffer_data_region_arp_vaddr;
uintptr_t buffer_data_region_cli0_vaddr;
uintptr_t buffer_data_region_cli1_vaddr;

uintptr_t buffer_data_region_arp_paddr;
uintptr_t buffer_data_region_cli0_paddr;
uintptr_t buffer_data_region_cli1_paddr;

struct state {
    struct net_queue_handle tx_queue_drv;
    struct net_queue_handle tx_queue_clients[NUM_CLIENTS];
    uintptr_t buffer_region_vaddrs[NUM_CLIENTS];
    uintptr_t buffer_region_paddrs[NUM_CLIENTS];
};

/*@
  context phys != NULL ** Perm(phys, read);
  context gstate != NULL ** Perm(gstate, read);
  context Perm(gstate->buffer_region_paddrs, read);
  context Perm(gstate->buffer_region_vaddrs, read);
  context Perm(gstate->tx_queue_clients, read);
  context \pointer(gstate->buffer_region_paddrs, 3, read);
  context \pointer(gstate->buffer_region_vaddrs, 3, read);
  context \pointer(gstate->tx_queue_clients, 3, read);
  context (\forall int c1=0 .. 3, int c2=0 .. 3; gstate->tx_queue_clients[c1] == gstate->tx_queue_clients[c2] ==> c1 == c2);
  context (\forall int c=0 .. 3; gstate->tx_queue_clients[c] != NULL);
  context (\forall* int c=0 .. 3; Perm(gstate->tx_queue_clients[c].size, read));
 @*/
int extract_offset(uintptr_t *phys, struct state *gstate)
{

    int myphys = *phys;
    uintptr_t *paddrs = gstate->buffer_region_paddrs;
    uintptr_t *vaddrs = gstate->buffer_region_vaddrs;
    struct net_queue_handle *tx_queue_clients = gstate->tx_queue_clients;
    for (int client = 0; client < NUM_CLIENTS; client++)
    /*@
     context paddrs != NULL;
     context Perm(&paddrs[client], read);
     context Perm(&vaddrs[client], read);
     context tx_queue_clients != NULL;
     context Perm(&tx_queue_clients[client], read);
     context tx_queue_clients[client] != NULL;
     context Perm(tx_queue_clients[client].size, read);
    @*/
    {
        if (myphys >= paddrs[client] &&
            myphys <  paddrs[client] + tx_queue_clients[client].size * NET_BUFFER_SIZE) {
            return client;
        }
    }

    return -1;
}

void init() {
}

[isubasinghe]

Thanks a lot @superaxander!!

I would like to know what the level of support for C code is in VerCors as it currently stands, thanks.

I'm asking because we are evaluating alternative tools that could be used for the verification of drivers in LionsOS. I am trying to get a mux verified at the moment.

We have our own toolchain but it suffers from significant scalability issues as a result of working on a lower level of abstraction than the C code (this was done to preserve the binary verification that we do).

We could potentially be interested in collaboration if you share the same interests (SMT based verification with a relatively lower TCB than current methods). I am not speaking for my employer here, just sharing my own opinion, but I don't see why this wouldn't be the case, preserving the binary verification story is an important part of the seL4 verification story and we would want the same properties to be held by LionsOS.

Thanks a lot :)

[superaxander]

Thanks for your interest in VerCors @isubasinghe

Currently we have decent but far from complete support for C code in VerCors. For example, currently there is no support for taking the address of something that is not a struct. (you can still declare functions that take pointers of any type) There is currently work ongoing (for example in #1172) to resolve this and other shortcomings but our support for C is nowhere near that of say Frama-C or VeriFast.

If you want to try to use VerCors for verifying (parts of) your codebase you are welcome to try and to report any bugs and issues you run into along the way. Currently the focus of our C and C++ front-ends have been on the verification of GPU programs but because we are also working on verification on the LLVM-IR level that is necessitating an expansion of the kinds of pointer and struct related operations we support. Therefore I expect that our C support will improve somewhat in the future. We are open to collaborations, contributions and suggestions, but since the support for C is not our main focus I can make no promises for our level of support there.