How to touch global struct array?

[Kiwamu Okabe]

Dear all,

How to touch global struct array?

Now I'm trying to verify FreeRTOS code using VeriFast.
https://github.com/metasepi/amazon-freertos/

It can be verify with following command:
```
$ vfide -I verifast_inc lib/FreeRTOS/tasks.c
```

I know that function can touch global value such like following manner:
```
static volatile UBaseType_t uxCurrentNumberOfTasks = ( UBaseType_t ) 0U;
// --snip--
static void prvAddNewTaskToReadyList( TCB_t *pxNewTCB )
//@ requires u_integer(&uxCurrentNumberOfTasks, _) &*&
pointer(&pxCurrentTCB, _) &*& u_integer(&uxTaskNumber, _) &*&
u_integer(&uxTopReadyPriority, _) &*& TCB_t_pred(pxNewTCB);
//@ ensures u_integer(&uxCurrentNumberOfTasks, _) &*&
pointer(&pxCurrentTCB, _) &*& u_integer(&uxTaskNumber, _) &*&
u_integer(&uxTopReadyPriority, _);
{
/* Ensure interrupts don't access the task lists while the lists are being
updated. */
taskENTER_CRITICAL();
{
uxCurrentNumberOfTasks++;
```

But, how to touch following `pxReadyTasksLists` array on function?
```
typedef struct xLIST
{
} List_t;
// --snip--
static List_t pxReadyTasksLists[ configMAX_PRIORITIES ];
// --snip--
#define prvAddTaskToReadyList( pxTCB )
\
traceMOVED_TASK_TO_READY_STATE( pxTCB );
\
taskRECORD_READY_PRIORITY( ( pxTCB )->uxPriority );
\
vListInsertEnd( &( pxReadyTasksLists[ ( pxTCB )->uxPriority ] ),
&( ( pxTCB )->xStateListItem ) ); \
tracePOST_MOVED_TASK_TO_READY_STATE( pxTCB )
```

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[Bart Jacobs]

Put this in your precondition: `pxReadyTasksLists[..configMAX_PRIORITIES] |-> _`.

Note: instead of writing `u_integer(&uxCurrentNumberOfTasks, _)` or `pointer(&pxCurrentTCB, _)`, it is better to write `uxCurrentNumberOfTasks |-> _` and `pxCurrentTCB |-> _`. Not only is this easier to read, it also eliminates the assumption that `uxCurrentNumberOfTasks` is of type `unsigned int`.

[Kiwamu Okabe]

On Fri, Sep 7, 2018 at 5:51 PM Bart Jacobs <bart....@cs.kuleuven.be> wrote:
> Put this in your precondition: `pxReadyTasksLists[..configMAX_PRIORITIES] |-> _`.

It say:

```
$ verifast -c -I verifast_inc lib/FreeRTOS/tasks.c
lib/FreeRTOS/tasks.c
lib/FreeRTOS/tasks.c(1071,202-205): Array points-to notation is not
supported for element type 'struct xLIST'
```

I need to define some predicate for `struct xLIST`?

> Note: instead of writing `u_integer(&uxCurrentNumberOfTasks, _)` or `pointer(&pxCurrentTCB, _)`, it is better to write `uxCurrentNumberOfTasks |-> _` and `pxCurrentTCB |-> _`. Not only is this easier to read, it also eliminates the assumption that `uxCurrentNumberOfTasks` is of type `unsigned int`.

Thanks. I should read your tutorial with more caution.

[Bart Jacobs]

On 07/09/18 11:33, Kiwamu Okabe wrote:
> On Fri, Sep 7, 2018 at 5:51 PM Bart Jacobs <bart....@cs.kuleuven.be> wrote:
>> Put this in your precondition: `pxReadyTasksLists[..configMAX_PRIORITIES] |-> _`.
> It say:
>
> ```
> $ verifast -c -I verifast_inc lib/FreeRTOS/tasks.c
> lib/FreeRTOS/tasks.c
> lib/FreeRTOS/tasks.c(1071,202-205): Array points-to notation is not
> supported for element type 'struct xLIST'
> ```

Right. What I suggested works only for arrays whose element type is an
integer or a pointer.

>
> I need to define some predicate for `struct xLIST`?

Yes. Furthermore, you need to define a predicate for arrays of struct
xLIST. For example:
```
predicate xLISTs(struct xLIST *p, int count;) = count == 0 ? emp :
xLIST(p) &*& xLISTs(p + 1, count - 1);
```
where `xLIST` is the predicate you defined for `struct xLIST`.

Then, just write `xLISTs(pxReadyTaskLists, configMAX_PRIORITIES)` (or,
equivalently, `xLISTs(&pxReadyTaskLists, configMAX_PRIORITIES)`) in your
precondition.

[Kiwamu Okabe]

On Fri, Sep 7, 2018 at 6:42 PM Bart Jacobs <bart....@cs.kuleuven.be> wrote:
> > I need to define some predicate for `struct xLIST`?
>
> Yes. Furthermore, you need to define a predicate for arrays of struct
> xLIST. For example:
> ```
> predicate xLISTs(struct xLIST *p, int count;) = count == 0 ? emp :
> xLIST(p) &*& xLISTs(p + 1, count - 1);
> ```
> where `xLIST` is the predicate you defined for `struct xLIST`.

Umm... I think it doesn't make sense.
Following patch occurs error:

```
$ pwd
/home/kiwamu/src/amazon-freertos-metasepi
$ git diff | cat
diff --git a/lib/FreeRTOS/tasks.c b/lib/FreeRTOS/tasks.c
index 6962b04..e6d6d3b 100644
--- a/lib/FreeRTOS/tasks.c
+++ b/lib/FreeRTOS/tasks.c
@@ -1068,8 +1068,8 @@ UBaseType_t x;
/*-----------------------------------------------------------*/

static void prvAddNewTaskToReadyList( TCB_t *pxNewTCB )

- //@ requires u_integer(&uxCurrentNumberOfTasks, _) &*&

pointer(&pxCurrentTCB, _) &*& u_integer(&uxTaskNumber, _) &*&
u_integer(&uxTopReadyPriority, _) &*& TCB_t_pred(pxNewTCB);

- //@ ensures u_integer(&uxCurrentNumberOfTasks, _) &*&

pointer(&pxCurrentTCB, _) &*& u_integer(&uxTaskNumber, _) &*&
u_integer(&uxTopReadyPriority, _);

+ //@ requires u_integer(&uxCurrentNumberOfTasks, _) &*&

pointer(&pxCurrentTCB, _) &*& u_integer(&uxTaskNumber, _) &*&
u_integer(&uxTopReadyPriority, _) &*&

pxReadyTasksLists[..configMAX_PRIORITIES] |-> _ &*&
TCB_t_pred(pxNewTCB);
+ //@ ensures u_integer(&uxCurrentNumberOfTasks, _) &*&

pointer(&pxCurrentTCB, _) &*& u_integer(&uxTaskNumber, _) &*&

u_integer(&uxTopReadyPriority, _) &*&
pxReadyTasksLists[..configMAX_PRIORITIES] |-> _;

{
/* Ensure interrupts don't access the task lists while the
lists are being
updated. */

diff --git a/verifast_inc/list.h b/verifast_inc/list.h
index d949694..c089947 100644
--- a/verifast_inc/list.h
+++ b/verifast_inc/list.h
@@ -14,8 +14,20 @@ typedef struct xLIST_ITEM ListItem_t;

typedef struct xLIST
{
+ int dummy;
} List_t;

+/*@
+predicate xLIST(struct xLIST *p) =
+ p->dummy |-> _;
+
+predicate xLISTs(struct xLIST *p, int count;) =
+ count == 0 ?
+ emp
+ :
+ xLIST(p) &*& xLISTs(p + 1, count - 1);
+@*/
+
#define listSET_LIST_ITEM_OWNER( pxListItem, pxOwner ) ( (
pxListItem )->pvOwner = ( void * ) ( pxOwner ) )

#define listSET_LIST_ITEM_VALUE( pxListItem, xValue ) ( ( pxListItem
)->xItemValue = ( xValue ) )

$ verifast -c -I verifast_inc lib/FreeRTOS/tasks.c
lib/FreeRTOS/tasks.c

verifast_inc/list.h(28,9-14): Preciseness check failure: callee is not precise.
```

What does `precise` mean?

[Bart Jacobs]

See the section on precise predicates in the VeriFast tutorial. Or
remove the semicolon from the parameter list of predicate xLISTs.

[Kiwamu Okabe]

On Mon, Sep 10, 2018 at 4:24 PM Bart Jacobs <bart....@cs.kuleuven.be> wrote:
> See the section on precise predicates in the VeriFast tutorial.

I'll try to read it again.

> Or remove the semicolon from the parameter list of predicate xLISTs.

Unfortunately, it causes error:

```
$ cat tasklist.c
#include "stdlib.h"

#define configMAX_PRIORITIES 7

typedef struct xLIST
{
int dummy;
} List_t;

/*@
predicate xLIST(struct xLIST *p) =
p->dummy |-> _;

predicate xLISTs(struct xLIST *p, int count) =

count == 0 ?
emp
:
xLIST(p) &*& xLISTs(p + 1, count - 1);

@*/

static List_t pxReadyTasksLists[ configMAX_PRIORITIES ];

int entry()
//@ requires pxReadyTasksLists[..configMAX_PRIORITIES] |-> _;
//@ ensures pxReadyTasksLists[..configMAX_PRIORITIES] |-> _;
{
return 0;
}
$ verifast -c tasklist.c
tasklist.c
tasklist.c(24,60-63): Array points-to notation is not supported for
element type 'struct xLIST'
```

[Bart Jacobs]

The spec for `entry` should be:

```
int entry()
//@ requires xLISTs(pxReadyTaskLists, configMAX_PRIORITIES);
//@ ensures xLISTs(pxReadyTaskLists, configMAX_PRIORITIES);
```

[Kiwamu Okabe]

On Tue, Sep 11, 2018 at 3:42 PM Bart Jacobs <bart....@cs.kuleuven.be> wrote:
> The spec for `entry` should be:

Thanks. Following works:

```
$ cat tasklist.c
#include "stdlib.h"

#define configMAX_PRIORITIES 7

typedef struct xLIST
{
int dummy;
} List_t;

/*@
predicate xLIST(struct xLIST *p) =
p->dummy |-> _;

predicate xLISTs(struct xLIST *p, int count) =
count == 0 ?
emp
:
xLIST(p) &*& xLISTs(p + 1, count - 1);
@*/

static List_t pxReadyTasksLists[ configMAX_PRIORITIES ];

int entry()

//@ requires xLISTs(pxReadyTasksLists, configMAX_PRIORITIES);
//@ ensures xLISTs(pxReadyTasksLists, configMAX_PRIORITIES);

{
return 0;
}
$ verifast -c tasklist.c
tasklist.c

0 errors found (0 statements verified)
```

I'm confusing.

* When should we use generic chunk syntax?
* When should we use field chunk-specific syntax?

[Bart Jacobs]

On 11/09/2018 9:10, Kiwamu Okabe wrote:
>
> * When should we use generic chunk syntax?
> * When should we use field chunk-specific syntax?
>

`bin/prelude.h` defines array predicates (`chars`, `ints`, `integers_`,
etc.) for arrays whose elements are integers or pointers. The points-to
syntax is supported only for arrays whose elements are integers or
pointers, and is syntactic sugar for the predicates defined in
`bin/prelude.h`. For all other arrays, you need to define your own array
predicates, and use the generic chunk syntax to refer to them.

[Kiwamu Okabe]

On Tue, Sep 11, 2018 at 4:31 PM Bart Jacobs <bart....@cs.kuleuven.be> wrote:
> `bin/prelude.h` defines array predicates (`chars`, `ints`, `integers_`,
> etc.) for arrays whose elements are integers or pointers. The points-to
> syntax is supported only for arrays whose elements are integers or
> pointers, and is syntactic sugar for the predicates defined in
> `bin/prelude.h`. For all other arrays, you need to define your own array
> predicates, and use the generic chunk syntax to refer to them.

Thanks. It's clear for me.