len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-10-15 17:27:46 -04:00
Code Issues Projects Releases Packages Wiki Activity

List proofs and signoff (#194)

Browse source
This commit is contained in:
Nathan Chong 2020-08-27 14:59:12 -04:00 • committed by GitHub
parent 6d35a38bdd
commit 669084ee8f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
16 changed files with 1737 additions and 59 deletions
Download patch file Download diff file Expand all files Collapse all files

56
FreeRTOS/Test/VeriFast/Makefile
View file

@ -14,28 +14,37 @@ check_coverage = perl -pe \
$$status=/$1 statements verified/ ? 0 : 1;'
endif
all: queue
all: queue list
.PHONY: queue
queue:
@$(VERIFAST) $(VERIFAST_ARGS) queue/create.c | $(call check_coverage,317)
@$(VERIFAST) $(VERIFAST_ARGS) queue/prvCopyDataFromQueue.c | $(call check_coverage,301)
@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/prvCopyDataToQueue.c | $(call check_coverage,329)
@$(VERIFAST) $(VERIFAST_ARGS) queue/prvIsQueueEmpty.c | $(call check_coverage,282)
@$(VERIFAST) $(VERIFAST_ARGS) queue/prvIsQueueFull.c | $(call check_coverage,282)
@$(VERIFAST) $(VERIFAST_ARGS) queue/prvLockQueue.c | $(call check_coverage,283)
@$(VERIFAST) $(VERIFAST_ARGS) queue/prvUnlockQueue.c | $(call check_coverage,297)
@$(VERIFAST) $(VERIFAST_ARGS) queue/uxQueueMessagesWaiting.c | $(call check_coverage,285)
@$(VERIFAST) $(VERIFAST_ARGS) queue/uxQueueSpacesAvailable.c | $(call check_coverage,283)
@$(VERIFAST) $(VERIFAST_ARGS) queue/vQueueDelete.c | $(call check_coverage,280)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueGenericSend.c | $(call check_coverage,328)
@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueGenericSendFromISR.c | $(call check_coverage,310)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueIsQueueEmptyFromISR.c | $(call check_coverage,280)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueIsQueueFullFromISR.c | $(call check_coverage,280)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueuePeek.c | $(call check_coverage,328)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueuePeekFromISR.c | $(call check_coverage,293)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueReceive.c | $(call check_coverage,330)
@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueReceiveFromISR.c | $(call check_coverage,307)
@$(VERIFAST) $(VERIFAST_ARGS) queue/create.c | $(call check_coverage,324)
@$(VERIFAST) $(VERIFAST_ARGS) queue/prvCopyDataFromQueue.c | $(call check_coverage,308)
@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/prvCopyDataToQueue.c | $(call check_coverage,336)
@$(VERIFAST) $(VERIFAST_ARGS) queue/prvIsQueueEmpty.c | $(call check_coverage,289)
@$(VERIFAST) $(VERIFAST_ARGS) queue/prvIsQueueFull.c | $(call check_coverage,289)
@$(VERIFAST) $(VERIFAST_ARGS) queue/prvLockQueue.c | $(call check_coverage,290)
@$(VERIFAST) $(VERIFAST_ARGS) queue/prvUnlockQueue.c | $(call check_coverage,304)
@$(VERIFAST) $(VERIFAST_ARGS) queue/uxQueueMessagesWaiting.c | $(call check_coverage,292)
@$(VERIFAST) $(VERIFAST_ARGS) queue/uxQueueSpacesAvailable.c | $(call check_coverage,290)
@$(VERIFAST) $(VERIFAST_ARGS) queue/vQueueDelete.c | $(call check_coverage,287)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueGenericSend.c | $(call check_coverage,335)
@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueGenericSendFromISR.c | $(call check_coverage,317)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueIsQueueEmptyFromISR.c | $(call check_coverage,287)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueIsQueueFullFromISR.c | $(call check_coverage,287)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueuePeek.c | $(call check_coverage,335)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueuePeekFromISR.c | $(call check_coverage,300)
@$(VERIFAST) $(VERIFAST_ARGS) queue/xQueueReceive.c | $(call check_coverage,337)
@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check queue/xQueueReceiveFromISR.c | $(call check_coverage,314)
.PHONY: list
list:
@$(VERIFAST) $(VERIFAST_ARGS) list/listLIST_IS_EMPTY.c | $(call check_coverage,314)
@$(VERIFAST) $(VERIFAST_ARGS) list/uxListRemove.c | $(call check_coverage,440)
@$(VERIFAST) $(VERIFAST_ARGS) list/vListInitialise.c | $(call check_coverage,325)
@$(VERIFAST) $(VERIFAST_ARGS) list/vListInitialiseItem.c | $(call check_coverage,316)
@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check list/vListInsertEnd.c | $(call check_coverage,410)
@$(VERIFAST) $(VERIFAST_ARGS) -disable_overflow_check list/vListInsert.c | $(call check_coverage,456)
.PHONY: proof_changes
proof_changes:
@ -43,10 +52,13 @@ proof_changes:
GIT?=git
NO_CHANGE_CHECKOUT_DIR=no-change-check-freertos-kernel
NO_CHANGE_EXPECTED_HASH=587a83d6476
NO_CHANGE_EXPECTED_HASH_QUEUE=587a83d6476
NO_CHANGE_EXPECTED_HASH_LIST=bb1c4293787
.PHONY: synced_with_source_check
synced_with_source_check:
@rm -rf $(NO_CHANGE_CHECKOUT_DIR)
@$(GIT) clone https://github.com/FreeRTOS/FreeRTOS-Kernel.git $(NO_CHANGE_CHECKOUT_DIR)
@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH) queue.c
@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH) include/queue.h
@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_QUEUE) queue.c
@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_QUEUE) include/queue.h
@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_LIST) list.c
@cd $(NO_CHANGE_CHECKOUT_DIR) && $(GIT) diff --quiet $(NO_CHANGE_EXPECTED_HASH_LIST) include/list.h

44
FreeRTOS/Test/VeriFast/README.md
View file

@ -1,8 +1,19 @@
# FreeRTOS VeriFast proofs
This directory contains automated functional correctness proofs of the FreeRTOS
kernel queue data structure. These properties are proven with the
[VeriFast](https://github.com/verifast/verifast) verifier.
This directory contains unbounded proofs of the FreeRTOS kernel queue and list
data structures. Unbounded proofs mean that these results hold independent of
the length of the queue or list.
Informally, the queue proofs demonstrate that the queue implementation is
memory safe (does not access invalid memory), thread safe (properly
synchronizes accesses) and functionally correct (behaves like a queue) under
any arbitrary number of tasks or ISRs. The list proofs demonstrate that the
list implementation is memory safe and functionally correct.
These properties are proven with the
[VeriFast](https://github.com/verifast/verifast) verifier. See the proof
[signoff](docs/signoff.md) document for more on the proof properties,
assumptions, and simplifications.
## Proof directory structure
@ -14,6 +25,7 @@ predicates, functions and lemmas used by all proofs is maintained in the
`include/proof` directory.
- `queue`: proofs for the FreeRTOS queue data structure
- `list`: proofs for the FreeRTOS list data structure
The following figure gives the callgraph of the queue proofs. Green=Proven
functions, Blue=Functions modeled by lock invariants (underlying implementation
@ -49,7 +61,7 @@ and uncheck `Check arithmetic overflow`).
- `queue/xQueueReceiveFromISR.c`
A successful proof results in the top banner turning green with a statement
similar to: `0 errors found (328 statements verified)`.
similar to: `0 errors found (335 statements verified)`.
## Proof checking a single proof at the command-line
@ -65,7 +77,7 @@ A successful proof results in output similar to:
```
queue/xQueueGenericSend.c
0 errors found (328 statements verified)
0 errors found (335 statements verified)
```
## Running proof regression
@ -87,7 +99,8 @@ $ VERIFAST=/path/to/verifast NO_COVERAGE=1 make
## Annotation burden
VeriFast can emit statistics about the number of source code lines and
annotations. These range from .3-2x annotations per line of source code.
annotations. These range from .3-2x annotations per line of source code for the
queue proofs and up to 7x for the list proofs.
```
$ VERIFAST=/path/to/verifast ./scripts/annotation_overhead.sh
@ -96,15 +109,12 @@ $ VERIFAST=/path/to/verifast ./scripts/annotation_overhead.sh
## Reading a VeriFast proof
VeriFast is a modular deductive verifier using separation logic. A quick
introduction is given by [Jacobs and
Piessens](https://people.cs.kuleuven.be/~bart.jacobs/verifast/verifast.pdf).
In particular, Section 1 Introduction, gives a high-level overview of the proof
technique, which uses forward symbolic execution over a symbolic heap.
introduction is given by [Jacobs and Piessens][1]. In particular, Section 1
Introduction, gives a high-level overview of the proof technique, which uses
forward symbolic execution over a symbolic heap.
Learning how to use VeriFast will help you read and understand the proofs.
The VeriFast
[tutorial](https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf) is
a good guide. You will need to understand:
Learning how to use VeriFast will help you read and understand the proofs. The
VeriFast [tutorial][2] is a good guide. You will need to understand:
- Sec 4. Functions and Contracts
- Sec 5. Patterns
@ -115,8 +125,12 @@ a good guide. You will need to understand:
- Sec 10. Inductive Datatypes
- Sec 11. Lemmas
[1]: https://people.cs.kuleuven.be/~bart.jacobs/verifast/verifast.pdf
[2]: https://people.cs.kuleuven.be/~bart.jacobs/verifast/tutorial.pdf
## Contributors
We acknowledge and thank the following contributors, listed alphabetically:
We acknowledge and thank the following contributors:
- Bart Jacobs, KU Leuven, https://people.cs.kuleuven.be/~bart.jacobs/
- Aalok Thakkar, University of Pennsylvania, https://aalok-thakkar.github.io/

144
FreeRTOS/Test/VeriFast/docs/signoff.md Normal file
View file

@ -0,0 +1,144 @@
# FreeRTOS VeriFast Proof Signoff
Verification tool: VeriFast (code-level proof)
Proofs: `queue/` and `list`
Implementation: Kernel queue data structure (`queue.c`) and list data structure (`list.c`)
Specification / Properties:
- *Memory safety*: the implementation only accesses valid memory. In the case
of the queue, this is true under any arbitrary number of tasks or ISRs.
- *Thread safety*: in the case of the queue, tasks and ISRs only update
objects that they own via proper synchronization.
- *Functional correctness*: the queue and list implementations behave like an
abstract queue and list. In the case of the queue, this is true under any
arbitrary number of tasks or ISRs.
## Queue proof assumptions
Generally, we assume well-behaved clients; the correctness of underlying
primitives (memory allocation, task scheduling, scheduler suspension); and
assumptions about the system.
- Well-behaved client: all client tasks and ISRs use the queue API in a
manner that adheres to the specification. A badly-behaved client can
invalidate the proven properties. For example, a client that reads or
writes to the queue storage directly, without masking interrupts, is racy
and no longer thread safe. The specification forbids this behavior by
the definition of `queuehandle`, which is a handle to acquire ownership of
the queue through interrupt masking, but we cannot, in general, enforce
this behavior since we do not verify client code.
- Memory safety, thread safety and function contracts for the following
primitives. For the list and task functions we give a contract that is
maximal in terms of the queue objects that can be updated, but we do not
model their function effect (e.g., task blocking and the moving of task
control blocks between scheduler lists).
pvPortMalloc
vPortFree
memcpy
vListInitialise
xTaskRemoveFromEventList
vTaskMissedYield
xTaskCheckForTimeOut
vTaskInternalSetTimeOutState
vTaskPlaceOnEventList
- We assume interrupt masking gives strong isolation between tasks and ISRs.
See Appendix. We further assume the system is configured as required by
`configASSERT`. For example, interrupts with a priority greater than the
maximum system call priority must not call queue API functions, otherwise
the strong isolation guarantee is not maintained.
## List proof assumptions
The list proofs are sequential. We assume the caller of the list API functions
has taken appropriate synchronization steps to avoid races.
## Simplifications
A list of changes to the source code required for the proofs can be generated:
```
make proof_changes
```
A side-by-side diff with respect to the source code can be generated. See
![`scripts/diff_files.md`](../scripts/diff_files.md).
The main queue changes are:
- merge cTxLock and cRxLock critical regions: under approximate queue
unlock behavior to atomically set `cTxLock` and `cRxLock` to unlocked in a
single critical region instead of two separate critical regions. In
practice, this is not an issue since no ISR function reads-from both
cTxLock and cRxLock.
- model single malloc of struct and buffer: split the single malloc of the
queue struct and storage into two separate mallocs.
- xQueueGenericReset happens-before concurrent behavior: assume that queue
initialisation is not concurrent.
- do not model pxIndex and xListEnd of xLIST struct: ignore these fields in
the list structs of the queue implementation
The main list changes are:
- change `MiniList_t` to `ListItem_t`: simplifying assumption on the list
structure.
- over-approximate list insert loop: replace a loop in the insert function
that finds the insertion point with an over-approximating function call.
The following minor changes due to the stricter typing and parser of VeriFast:
- replacing a union declaration with a struct
- const pointer declaration
- stricter casting
- void cast of unused return value
- void cast of unused var
The following minor changes due to the modeling of interrupts and scheduler
suspension in the proofs as ghost state.
- ghost action
- leak ghost state on deletion
## Configuration
We do not verify across the full configuration space of FreeRTOS. In
particular, the queue proofs do not apply when the following options are
enabled:
- `configUSE_QUEUE_SETS`
- `configSUPPORT_STATIC_ALLOCATION`
For both the queue and list proofs we assume that coverage and tracing
macros are no-ops.
## Trusted computing base
- Soundness of verification tools: VeriFast, Redux prover
- C Compiler, because the verification is at the C code-level and the
properties proved may not be preserved by compilation.
## References
[N1570] ISO/IEC. Programming languages – C. International standard 9899:201x,
2011
## Appendix
Assumption on strong isolation induced by interrupt masking and scheduler
suspension for queue proofs. Informally, we need the following:
```
// Initially *data == 0
// Task 1
taskENTER_CRITICAL()
*data = 1;
*data = 2;
taskEXIT_CRITICAL()
// ISR or Task 2
r0 = *data; //< guaranteed to read 0 or 2, never 1
```

65
FreeRTOS/Test/VeriFast/include/proof/common.gh
View file

@ -191,6 +191,45 @@ lemma_auto void mod_range(int x, int n)
div_rem_nonneg(x, n);
}
lemma void head_append<t>(list<t> xs, list<t> ys)
requires 0 < length(xs);
ensures head(append(xs, ys)) == head(xs);
{
switch(xs)
{
case cons(c, cs):
case nil:
}
}
lemma void drop_take_singleton<t>(int i, list<t> xs)
requires 0 < i && i < length(xs);
ensures drop(i-1, take(i, xs)) == singleton(nth(i-1, xs));
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (i == 1) {
} else {
drop_take_singleton(i-1, xs0);
}
}
}
lemma void take_singleton<t>(int i, list<t> xs)
requires 0 <= i && i < length(xs);
ensures append(take(i, xs), singleton(nth(i, xs))) == take(i+1, xs);
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (i == 0) {
} else {
take_singleton(i-1, xs0);
}
}
}
lemma void drop_update_le<t>(int i, int j, t x, list<t> xs)
requires 0 <= i && i <= j && j < length(xs);
ensures drop(i, update(j, x, xs)) == update(j - i, x, drop(i, xs));
@ -298,21 +337,17 @@ lemma void take_take<t>(int m, int n, list<t> xs)
}
}
lemma void index_of_distinct<t>(list<t> xs, t x1, t x2)
requires mem(x1, xs) == true &*& mem(x2, xs) == true &*& x1 != x2;
ensures index_of(x1, xs) != index_of(x2, xs);
lemma_auto void take_head<t>(list<t> xs)
requires 0 < length(xs);
ensures take(1, xs) == singleton(head(xs));
{
switch(xs) {
case nil:
case cons(h, tl):
if (h == x1 || h == x2) {
/* trivial */
} else {
index_of_distinct(tl, x1, x2);
}
case cons(x0, xs0):
}
}
/* Following lemma from `verifast/bin/rt/_list.java` */
lemma void remove_remove_nth<t>(list<t> xs, t x)
requires mem(x, xs) == true;
ensures remove(x, xs) == remove_nth(index_of(x, xs), xs);
@ -328,6 +363,18 @@ lemma void remove_remove_nth<t>(list<t> xs, t x)
}
}
lemma void mem_take_false<t>(t x, int n, list<t> xs)
requires mem(x, xs) == false;
ensures mem(x, take(n, xs)) == false;
{
switch (xs) {
case nil:
case cons(x0, xs0):
if (x0 != x && n != 0)
mem_take_false(x, n - 1, xs0);
}
}
/* Following lemma from `verifast/bin/rt/_list.java`. Renamed to
avoid clash with listex.c's nth_drop lemma. */
lemma void nth_drop2<t>(list<t> vs, int i)

368
FreeRTOS/Test/VeriFast/include/proof/list.h Normal file
View file

@ -0,0 +1,368 @@
/*
* FreeRTOS VeriFast Proofs
* Copyright (C) Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
#ifndef LIST_H
#define LIST_H
#define VERIFAST
#include <stdlib.h>
#include <stdint.h>
//@#include "common.gh"
typedef size_t TickType_t;
typedef size_t UBaseType_t;
typedef ssize_t BaseType_t;
#define pdTRUE 1
#define pdFALSE 0
/* Empty/no-op macros */
#define mtCOVERAGE_TEST_MARKER()
#define mtCOVERAGE_TEST_DELAY()
#define listSET_LIST_INTEGRITY_CHECK_1_VALUE( pxList )
#define listSET_LIST_INTEGRITY_CHECK_2_VALUE( pxList )
#define listTEST_LIST_INTEGRITY( pxList )
#define listTEST_LIST_ITEM_INTEGRITY( pxListItem )
#define listSET_FIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxListItem )
#define listSET_SECOND_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxListItem )
/* Max value stored in sentinel xListEnd element */
#define portMAX_DELAY UINT_MAX
struct xLIST;
struct xLIST_ITEM {
TickType_t xItemValue;
struct xLIST_ITEM * pxNext;
struct xLIST_ITEM * pxPrevious;
void * pvOwner;
struct xLIST *pxContainer;
};
typedef struct xLIST_ITEM ListItem_t;
typedef struct xLIST {
UBaseType_t uxNumberOfItems;
struct xLIST_ITEM *pxIndex;
#ifdef VERIFAST /*< ***change MiniList_t to ListItem_t*** */
struct xLIST_ITEM xListEnd;
#else
MiniListItem_t xListEnd;
#endif
} List_t;
/*@
predicate xLIST_ITEM(
struct xLIST_ITEM *n,
TickType_t xItemValue,
struct xLIST_ITEM *pxNext,
struct xLIST_ITEM *pxPrevious,
struct xLIST *pxContainer;) =
n->xItemValue |-> xItemValue &*&
n->pxNext |-> pxNext &*&
n->pxPrevious |-> pxPrevious &*&
n->pvOwner |-> _ &*&
n->pxContainer |-> pxContainer;
@*/
/* Ferreira et al. (STTT'14) doubly-linked list segment (DLS). */
/*@
predicate DLS(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
list<TickType_t > vals,
struct xLIST *pxContainer) =
n == m
? cells == cons(n, nil) &*&
vals == cons(?v, nil) &*&
xLIST_ITEM(n, v, mnext, nprev, pxContainer)
: cells == cons(n, ?cells0) &*&
vals == cons(?v, ?vals0) &*&
xLIST_ITEM(n, v, ?o, nprev, pxContainer) &*& DLS(o, n, mnext, m, cells0, vals0, pxContainer);
lemma void dls_star_item(
struct xLIST_ITEM *n,
struct xLIST_ITEM *m,
struct xLIST_ITEM *o)
requires DLS(n, ?nprev, ?mnext, m, ?cells, ?vals, ?l) &*& xLIST_ITEM(o, ?v, ?onext, ?oprev, ?l2);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& xLIST_ITEM(o, v, onext, oprev, l2) &*& mem(o, cells) == false;
{
open DLS(n, nprev, mnext, m, cells, vals, l);
if (n == m) {
assert xLIST_ITEM(n, _, _, _, _);
open xLIST_ITEM(n, _, _, _, _);
open xLIST_ITEM(o, _, _, _, _);
assert n != o;
close xLIST_ITEM(o, _, _, _, _);
close xLIST_ITEM(n, _, _, _, _);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
else {
assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l);
dls_star_item(nnext, m, o);
open xLIST_ITEM(n, _, _, _, _);
open xLIST_ITEM(o, _, _, _, _);
assert n != o;
close xLIST_ITEM(o, _, _, _, _);
close xLIST_ITEM(n, _, _, _, _);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
}
lemma void dls_distinct(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& distinct(cells) == true;
{
if (n == m) {
open DLS(n, nprev, mnext, m, cells, vals, l);
close DLS(n, nprev, mnext, m, cells, vals, l);
} else {
open DLS(n, nprev, mnext, m, cells, vals, l);
assert DLS(?nnext, n, mnext, m, tail(cells), tail(vals), l);
dls_distinct(nnext, n, mnext, m, tail(cells));
dls_star_item(nnext, m, n);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
}
predicate xLIST(
struct xLIST *l,
int uxNumberOfItems,
struct xLIST_ITEM *pxIndex,
struct xLIST_ITEM *xListEnd,
list<struct xLIST_ITEM *>cells,
list<TickType_t >vals) =
l->uxNumberOfItems |-> uxNumberOfItems &*&
l->pxIndex |-> pxIndex &*&
mem(pxIndex, cells) == true &*&
xListEnd == &(l->xListEnd) &*&
xListEnd == head(cells) &*&
portMAX_DELAY == head(vals) &*&
struct_xLIST_ITEM_padding(&l->xListEnd) &*&
length(cells) == length(vals) &*&
uxNumberOfItems + 1 == length(cells) &*&
DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l);
lemma void xLIST_distinct_cells(struct xLIST *l)
requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals);
ensures xLIST(l, n, idx, end, cells, vals) &*& distinct(cells) == true;
{
open xLIST(l, n, idx, end, cells, vals);
assert DLS(end, ?endprev, end, _, cells, vals, l);
dls_distinct(end, endprev, end, endprev, cells);
close xLIST(l, n, idx, end, cells, vals);
}
lemma void xLIST_star_item(struct xLIST *l, struct xLIST_ITEM *x)
requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals) &*& xLIST_ITEM(x, ?v, ?xnext, ?xprev, ?l2);
ensures xLIST(l, n, idx, end, cells, vals) &*& xLIST_ITEM(x, v, xnext, xprev, l2) &*& mem(x, cells) == false;
{
open xLIST(l, n, idx, end, cells, vals);
assert DLS(end, ?endprev, end, _, cells, vals, l);
dls_distinct(end, endprev, end, endprev, cells);
dls_star_item(end, endprev, x);
close xLIST(l, n, idx, end, cells, vals);
}
lemma void dls_first_mem(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(n, cells) == true &*& index_of(n, cells) == 0;
{
open DLS(n, nprev, mnext, m, cells, vals, l);
if (n == m) {
assert cells == cons(n, nil);
close DLS(n, nprev, mnext, m, cells, vals, l);
} else {
assert cells == cons(n, ?tail);
close DLS(n, nprev, mnext, m, cells, vals, l);
}
}
lemma void dls_not_empty(
struct xLIST_ITEM *n,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
struct xLIST_ITEM *x)
requires DLS(n, m, n, m, cells, ?vals, ?l) &*& mem(x, cells) == true &*& x != n;
ensures DLS(n, m, n, m, cells, vals, l) &*& n != m;
{
open DLS(n, m, n, m, cells, vals, l);
close DLS(n, m, n, m, cells, vals, l);
}
lemma void dls_last_mem(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells)
requires DLS(n, nprev, mnext, m, cells, ?vals, ?l);
ensures DLS(n, nprev, mnext, m, cells, vals, l) &*& mem(m, cells) == true &*& index_of(m, cells) == length(cells) - 1;
{
open DLS(n, nprev, mnext, m, cells, vals, l);
if (n == m) {
// trivial
} else {
open xLIST_ITEM(n, _, ?nnext, _, l);
assert DLS(?o, n, mnext, m, tail(cells), tail(vals), l);
dls_last_mem(o, n, mnext, m, tail(cells));
close xLIST_ITEM(n, _, nnext, _, l);
}
close DLS(n, nprev, mnext, m, cells, vals, l);
}
lemma void split(
struct xLIST_ITEM *n,
struct xLIST_ITEM *nprev,
struct xLIST_ITEM *mnext,
struct xLIST_ITEM *m,
list<struct xLIST_ITEM * > cells,
list<TickType_t > vals,
struct xLIST_ITEM *x,
int i)
requires DLS(n, nprev, mnext, m, cells, vals, ?l) &*& x != n &*& mem(x, cells) == true &*& index_of(x,cells) == i;
ensures DLS(n, nprev, x, ?xprev, take(i, cells), take(i, vals), l) &*& DLS(x, xprev, mnext, m, drop(i, cells), drop(i, vals), l) &*& xprev == nth(i-1, cells);
{
open DLS(n, nprev, mnext, m, cells, vals, l);
assert n != m;
assert xLIST_ITEM(n, ?v, ?nnext, _, _);
assert DLS(nnext, n, mnext, m, tail(cells), tail(vals), l);
if (nnext == x) {
close DLS(n, nprev, x, n, singleton(n), singleton(v), l);
open DLS(x, n, mnext, m, tail(cells), tail(vals), l);
open xLIST_ITEM(x, _, ?xnext, ?xprev, l);
close xLIST_ITEM(x, _, xnext, xprev, l);
close DLS(x, n, mnext, m, tail(cells), tail(vals), l);
} else {
assert nnext != x;
split(nnext, n, mnext, m, tail(cells), tail(vals), x, i - 1);
assert DLS(nnext, n, x, ?xprev, take(i-1, tail(cells)), take(i-1, tail(vals)), l);
dls_distinct(nnext, n, x, xprev, take(i-1, tail(cells)));
dls_star_item(nnext, xprev, n);
dls_last_mem(nnext, n, x, xprev, take(i-1, tail(cells)));
assert n != xprev;
close DLS(n, nprev, x, xprev, take(i, cells), take(i, vals), l);
}
}
lemma void join(
struct xLIST_ITEM *n1,
struct xLIST_ITEM *nprev1,
struct xLIST_ITEM *mnext1,
struct xLIST_ITEM *m1,
list<struct xLIST_ITEM * > cells1,
list<TickType_t > vals1,
struct xLIST_ITEM *n2,
struct xLIST_ITEM *nprev2,
struct xLIST_ITEM *mnext2,
struct xLIST_ITEM *m2,
list<struct xLIST_ITEM * > cells2,
list<TickType_t > vals2)
requires
DLS(n1, nprev1, mnext1, m1, cells1, vals1, ?l) &*&
DLS(n2, nprev2, mnext2, m2, cells2, vals2, l) &*&
mnext1 == n2 &*& m1 == nprev2;
ensures DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
{
if (n1 == m1) {
dls_first_mem(n1, nprev1, mnext1, m1, cells1);
dls_last_mem(n2, nprev2, mnext2, m2, cells2);
open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
dls_star_item(n2, m2, n1);
close DLS(n1, nprev1, mnext2, m2, append(singleton(n1), cells2), append(vals1, vals2), l);
} else {
open DLS(n1, nprev1, mnext1, m1, cells1, vals1, l);
assert DLS(?o, n1, mnext1, m1, ?cells1_tail, ?vals1_tail, l);
join(o, n1, mnext1, m1, cells1_tail, vals1_tail,
n2, nprev2, mnext2, m2, cells2, vals2);
assert DLS(o, n1, mnext2, m2, append(cells1_tail, cells2), append(vals1_tail, vals2), l);
dls_last_mem(o, n1, mnext2, m2, append(cells1_tail, cells2));
dls_star_item(o, m2, n1);
close DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
}
}
lemma void idx_remains_in_list<t>(
list<t> cells,
t idx,
t x,
int ix)
requires
idx != x &*&
mem(idx, cells) == true &*&
mem(x, cells) == true &*&
index_of(x, cells) == ix;
ensures mem(idx, remove_nth(ix, cells)) == true;
{
neq_mem_remove(idx, x, cells);
remove_remove_nth(cells, x);
}
@*/
/* Following lemma from `verifast/examples/shared_boxes/concurrentqueue.c`.
Used in the uxListRemove proof to show that the item to remove `x` must
have value `nth(i, vals)` where `i == index_of(x, cells)`. */
/*@
lemma void drop_nth_index_of<t>(list<t> vs, int i)
requires
0 <= i && i < length(vs);
ensures
head(drop(i , vs)) == nth(i, vs);
{
switch(vs) {
case nil:
case cons(h, t):
if (i == 0) {
// trivial
} else {
drop_nth_index_of(t, i - 1);
}
}
}
@*/
/*@
lemma void remove_append<t>(t x, list<t> l1, list<t> l2)
requires mem(x, l1) == false;
ensures remove(x, append(l1, l2)) == append(l1, remove(x, l2));
{
switch(l1) {
case nil:
case cons(h1, t1):
remove_append(x, t1, l2);
}
}
@*/
#endif /* LIST_H */

1
FreeRTOS/Test/VeriFast/include/proof/queue.h
View file

@ -305,7 +305,6 @@ ensures
}
drop_drop(1, j, elements);
nth_drop2(elements, i);
open buffer(buffer + (i+1) * M, (N-1-i), M, _);
}
}

69
FreeRTOS/Test/VeriFast/list/README.md Normal file
View file

@ -0,0 +1,69 @@
# FreeRTOS list proofs
The list predicates and proofs are inspired by and based on the work from
Ferreira et al. (STTT'14).
The main shape predicate is a doubly-linked list segment (DLS), as defined
by Ferreira et al. in Fig 15. A DLS is defined by two `xLIST_ITEM` struct
pointers `n` and `m` (possibly pointing to the same item) which are the start
and end of the segment. We track the item pointers and values within the DLS in
the lists `cells` and `vals`, respectively. Therefore `n` and `m` are the first
and last items of `cells`.
```
+--+ +--+
-----n-> |*n| ... |*m| -mnext->
<-nprev- | | | | <-m-----
+--+ +--+
^-----------^
DLS(n, nprev, mnext, m)
```
With base case: `n == m` (single item case)
```
+--+
-----n-> |*n| -mnext->
<-nprev- | | <-n-----
+--+
^--^
xLIST_ITEM
DLS(n, nprev, mnext, n)
```
Cons case:
```
+--+ +--+ +--+
-----n-> |*n| -o-> |*o| ... |*m| -mnext->
<-nprev- | | <-n- | | | | <-m-----
+--+ +--+ +--+
^--^ ^-----------^
xLIST_ITEM DLS(o, n, mnext, m)
^---------------------^
DLS(n, nprev, mnext, m)
```
A DLS can be made into a well-formed list by joining `n` and `m` into a cycle.
Note that unlike Ferreira et al.'s list shape predicate, we always start with
the sentinel end item to avoid a top-level case-split. So in the following
diagram the start and end of the DLS are `end` and the item-before-end
`endprev`.
```
.-----------------------------------.
| +--------+ +--------+ |
`--> |*end | ... |*endprev| ----'
.---- | | | | <---.
| +--------+ +--------+ |
`----------------------------------'
^-----------------------^
DLS(end, endprev, end, endprev)
```
## References
- Automated Verification of the FreeRTOS Scheduler in HIP/SLEEK\
João F. Ferreira, Cristian Gherghina, Guanhua He, Shengchao Qin, Wei-Ngan Chin\
https://joaoff.com/publication/2014/sttt/

36
FreeRTOS/Test/VeriFast/list/listLIST_IS_EMPTY.c Normal file
View file

@ -0,0 +1,36 @@
/*
* FreeRTOS VeriFast Proofs
* Copyright (C) Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
#include "proof/list.h"
/* Wrap the macro in a function call so we can give a function contract */
#define listLIST_IS_EMPTY( pxList ) ( ( ( pxList )->uxNumberOfItems == ( UBaseType_t ) 0 ) ? pdTRUE : pdFALSE )
BaseType_t wrapper_listLIST_IS_EMPTY( List_t * pxList )
/*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals);@*/
/*@ensures xLIST(pxList, len, idx, end, cells, vals) &*&
result == ((len == 0) ? pdTRUE : pdFALSE); @*/
{
/*@open xLIST(pxList, len, _, _, _, _);@*/
return listLIST_IS_EMPTY( pxList );
/*@close xLIST(pxList, len, _, _, cells, vals);@*/
}

306
FreeRTOS/Test/VeriFast/list/uxListRemove.c Normal file
View file

@ -0,0 +1,306 @@
/*
* FreeRTOS VeriFast Proofs
* Copyright (C) Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
#include "proof/list.h"
UBaseType_t uxListRemove( ListItem_t * const pxItemToRemove )
/*@requires
exists<struct xLIST * >(?l) &*&
xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
end != pxItemToRemove &*&
mem(pxItemToRemove, cells) == true;@*/
/*@ensures
result == len-1 &*&
xLIST_ITEM(pxItemToRemove, nth(index_of(pxItemToRemove, cells), vals), _, ?pxItemToRemovePrevious, NULL) &*&
pxItemToRemovePrevious == nth(index_of(pxItemToRemove, cells)-1, cells) &*&
xLIST(l, result, idx == pxItemToRemove ? pxItemToRemovePrevious : idx, end, remove(pxItemToRemove, cells), remove_nth(index_of(pxItemToRemove, cells), vals));@*/
{
/* For brevity we alias x to pxItemToRemove */
/*@struct xLIST_ITEM *x = pxItemToRemove;@*/
/* Start by establishing that the list must be non-empty since x != end */
/*@open xLIST(l, len, idx, end, cells, vals);@*/
/*@assert DLS(end, ?endprev, end, _, cells, vals, l);@*/
/*@assert vals == cons(portMAX_DELAY, _);@*/
/*@dls_not_empty(end, endprev, cells, x);@*/
/* We know the xLIST is a DLS: end...endprev
Split this into DLS1:end...xprev and DLS2:x...endprev */
/*@int i = index_of(x, cells);@*/
/*@split(end, endprev, end, endprev, cells, vals, x, i);@*/
/*@list<struct xLIST_ITEM *> ys = take(i, cells);@*/
/*@list<struct xLIST_ITEM *> zs = drop(i, cells);@*/
/*@list<TickType_t> vs = take(i, vals);@*/
/*@list<TickType_t> ws = drop(i, vals);@*/
/*@assert length(ys) == length(vs);@*/
/*@assert length(zs) == length(ws);@*/
/*@assert DLS(end, endprev, x, ?xprev, ys, vs, l);@*/ /*< DLS1 (ys, vs) */
/*@assert DLS(x, xprev, end, endprev, zs, ws, l);@*/ /*< DLS2 (zs, ws) */
/* Now case split to open DLS1 and DLS2 appropriately */
/*@
if (end == xprev)
{
if (x == endprev)
{
//Case A
//DLS1: extract end=prev=next
open DLS(end, endprev, x, xprev, ys, vs, l);
open xLIST_ITEM(end, portMAX_DELAY, x, endprev, l);
//DLS2: extract x
open DLS(x, xprev, end, endprev, zs, ws, l);
//Lengths
assert length(ys) == 1;
assert length(zs) == 1;
}
else
{
//Case B
//DLS1: extract end=prev
open DLS(end, endprev, x, xprev, ys, vs, l);
open xLIST_ITEM(end, portMAX_DELAY, x, endprev, l);
//DLS2: extract next and x
open DLS(x, end, end, endprev, zs, ws, l);
assert DLS(?xnext, x, end, endprev, tail(zs), tail(ws), l);
open DLS(xnext, x, end, endprev, tail(zs), tail(ws), l);
open xLIST_ITEM(xnext, _, _, x, l);
//Lengths
assert length(ys) == 1;
}
}
else
{
if (x == endprev)
{
//Case C
//DLS1: extract end=next and prev
dls_last_mem(end, endprev, x, xprev, ys);
assert mem(xprev, ys) == true;
open DLS(end, endprev, x, xprev, ys, vs, l);
open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, l);
if (endnext == xprev)
{
open DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
open xLIST_ITEM(xprev, _, x, _, l);
}
else
{
assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
int k = index_of(xprev, tail(ys));
dls_last_mem(endnext, end, x, xprev, tail(ys));
split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k);
open DLS(xprev, _, x, xprev, _, _, l);
open xLIST_ITEM(xprev, _, x, _, l);
}
//DLS2: extract x
open DLS(x, xprev, end, endprev, zs, ws, l);
//Lengths
assert length(zs) == 1;
}
else
{
//Case D
//DLS1: extract prev
dls_last_mem(end, endprev, x, xprev, ys);
int j = index_of(xprev, ys);
open DLS(end, endprev, x, xprev, ys, vs, l);
open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, l);
if (endnext == xprev)
{
open DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
assert tail(ys) == singleton(xprev);
open xLIST_ITEM(xprev, _, x, _, l);
}
else
{
assert DLS(endnext, end, x, xprev, tail(ys), tail(vs), l);
int k = index_of(xprev, tail(ys));
dls_last_mem(endnext, end, x, xprev, tail(ys));
split(endnext, end, x, xprev, tail(ys), tail(vs), xprev, k);
open DLS(xprev, _, x, xprev, _, _, l);
open xLIST_ITEM(xprev, _, x, _, l);
}
//DLS2: extract next and x
open DLS(x, xprev, end, endprev, zs, ws, l);
assert xLIST_ITEM(x, _, ?xnext, _, l);
open DLS(xnext, x, end, endprev, tail(zs), tail(ws), l);
open xLIST_ITEM(xnext, _, _, x, l);
}
}
@*/
/*@drop_nth_index_of(vals, i);@*/
/*@open xLIST_ITEM(x, nth(i, vals), ?xnext, xprev, l);@*/
/* The list item knows which list it is in. Obtain the list from the list
* item. */
#ifdef VERIFAST /*< const pointer declaration */
List_t * pxList = pxItemToRemove->pxContainer;
#else
List_t * const pxList = pxItemToRemove->pxContainer;
#endif
pxItemToRemove->pxNext->pxPrevious = pxItemToRemove->pxPrevious;
pxItemToRemove->pxPrevious->pxNext = pxItemToRemove->pxNext;
/* Only used during decision coverage testing. */
mtCOVERAGE_TEST_DELAY();
/* Make sure the index is left pointing to a valid item. */
if( pxList->pxIndex == pxItemToRemove )
{
pxList->pxIndex = pxItemToRemove->pxPrevious;
}
else
{
mtCOVERAGE_TEST_MARKER();
}
pxItemToRemove->pxContainer = NULL;
( pxList->uxNumberOfItems )--;
return pxList->uxNumberOfItems;
/*@
// Reassemble DLS1 and a modified DLS2, which no longer includes x
if (end == xprev)
{
if (x == endprev)
{
//Case A
close xLIST_ITEM(end, portMAX_DELAY, _, _, _);
close DLS(end, end, end, end, singleton(end), singleton(portMAX_DELAY), l);
}
else
{
//Case B
close xLIST_ITEM(xprev, _, xnext, endprev, l);
close DLS(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY), l);
close xLIST_ITEM(xnext, _, _, xprev, l);
close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), l);
join(end, endprev, xnext, xprev, singleton(end), singleton(portMAX_DELAY),
xnext, xprev, end, endprev, tail(zs), tail(ws));
}
}
else
{
if (x == endprev)
{
//Case C
close xLIST_ITEM(end, _, ?endnext, xprev, l);
close xLIST_ITEM(xprev, ?xprev_val, end, _, l);
if (endnext == xprev)
{
close DLS(xprev, end, end, xprev, singleton(xprev), singleton(xprev_val), l);
close DLS(end, xprev, end, xprev, cons(end, singleton(xprev)), cons(portMAX_DELAY, singleton(xprev_val)), l);
}
else
{
close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, l);
join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev,
xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val));
close DLS(end, xprev, end, xprev, ys, vs, l);
}
}
else
{
//Case D
close xLIST_ITEM(xnext, _, ?xnextnext, xprev, l);
close DLS(xnext, xprev, end, endprev, tail(zs), tail(ws), l);
close xLIST_ITEM(end, _, ?endnext, endprev, l);
close xLIST_ITEM(xprev, ?xprev_val, xnext, _, l);
if (endnext == xprev)
{
close DLS(xprev, _, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
close DLS(end, endprev, xnext, xprev, ys, vs, l);
join(end, endprev, xnext, xprev, ys, vs,
xnext, xprev, end, endprev, tail(zs), tail(ws));
}
else
{
close DLS(xprev, ?xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val), l);
assert DLS(endnext, end, xprev, xprevprev, ?cells_endnext_to_xprevprev, ?vals_endnext_to_xprevprev, l);
join(endnext, end, xprev, xprevprev, cells_endnext_to_xprevprev, vals_endnext_to_xprevprev,
xprev, xprevprev, xnext, xprev, singleton(xprev), singleton(xprev_val));
close DLS(end, endprev, xnext, xprev, ys, vs, l);
join(end, endprev, xnext, xprev, ys, vs,
xnext, xprev, end, endprev, tail(zs), tail(ws));
}
}
}
@*/
/*@remove_remove_nth(cells, x);@*/
/*@
if (idx == x)
{
close xLIST(l, len-1, xprev, end, append(ys, tail(zs)), append(vs, tail(ws)));
}
else
{
idx_remains_in_list(cells, idx, x, i);
close xLIST(l, len-1, idx, end, append(ys, tail(zs)), append(vs, tail(ws)));
}
@*/
/*@close xLIST_ITEM(x, nth(i, vals), xnext, xprev, NULL);@*/
}
ListItem_t * client_example( List_t * l )
/*@requires
xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
idx != end &*&
cells == cons(end, cons(idx, ?cells_tl)) &*&
vals == cons(portMAX_DELAY, cons(42, ?vals_tl));@*/
/*@ensures
xLIST(l, len - 1, _, end, cons(end, cells_tl), cons(portMAX_DELAY, vals_tl)) &*&
xLIST_ITEM(result, 42, _, _, NULL);@*/
{
/*@open xLIST(l, len, idx, end, cells, vals);@*/
ListItem_t *index = l->pxIndex;
/*@close xLIST(l, len, idx, end, cells, vals);@*/
/*@close exists(l);@*/
uxListRemove( index );
return index;
}
void client_example2( List_t * l )
/*@requires
xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
cells == cons(end, cons(?x1, cons(?x2, ?cells_tl))) &*&
idx == x2 &*&
vals == cons(portMAX_DELAY, cons(1, cons(2, ?vals_tl)));@*/
/*@ensures
xLIST(l, len-2, end, end, cons(end, cells_tl), cons(portMAX_DELAY, vals_tl)) &*&
xLIST_ITEM(_, 1, _, _, NULL) &*&
xLIST_ITEM(_, 2, _, _, NULL);@*/
{
/*@xLIST_distinct_cells(l);@*/
/*@open xLIST(l, len, idx, end, cells, vals);@*/
ListItem_t *index = l->pxIndex;
/*@close xLIST(l, len, idx, end, cells, vals);@*/
/*@close exists(l);@*/
uxListRemove( index );
/*@open xLIST(l, len-1, x1, end, cons(end, cons(x1, cells_tl)), cons(portMAX_DELAY, cons(1, vals_tl)));@*/
index = l->pxIndex;
/*@close xLIST(l, len-1, x1, end, cons(end, cons(x1, cells_tl)), cons(portMAX_DELAY, cons(1, vals_tl)));@*/
/*@close exists(l);@*/
uxListRemove( index );
}

71
FreeRTOS/Test/VeriFast/list/vListInitialise.c Normal file
View file

@ -0,0 +1,71 @@
/*
* FreeRTOS VeriFast Proofs
* Copyright (C) Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
#include "proof/list.h"
/*@
predicate xLIST_uninitialised(struct xLIST *l) =
l->uxNumberOfItems |-> _ &*&
l->pxIndex |-> _ &*&
l->xListEnd.xItemValue |-> _ &*&
l->xListEnd.pxNext |-> _ &*&
l->xListEnd.pxPrevious |-> _ &*&
l->xListEnd.pvOwner |-> _ &*&
l->xListEnd.pxContainer |-> _ &*&
struct_xLIST_ITEM_padding(&l->xListEnd);
@*/
void vListInitialise( List_t * const pxList )
/*@requires xLIST_uninitialised(pxList);@*/
/*@ensures xLIST(pxList, 0, ?end, end, singleton(end), singleton(portMAX_DELAY));@*/
{
/*@open xLIST_uninitialised(pxList);@*/
/* The list structure contains a list item which is used to mark the
* end of the list. To initialise the list the list end is inserted
* as the only list entry. */
pxList->pxIndex = ( ListItem_t * ) &( pxList->xListEnd ); /*lint !e826 !e740 !e9087 The mini list structure is used as the list end to save RAM. This is checked and valid. */
/* The list end value is the highest possible value in the list to
* ensure it remains at the end of the list. */
pxList->xListEnd.xItemValue = portMAX_DELAY;
/* The list end next and previous pointers point to itself so we know
* when the list is empty. */
pxList->xListEnd.pxNext = ( ListItem_t * ) &( pxList->xListEnd ); /*lint !e826 !e740 !e9087 The mini list structure is used as the list end to save RAM. This is checked and valid. */
pxList->xListEnd.pxPrevious = ( ListItem_t * ) &( pxList->xListEnd ); /*lint !e826 !e740 !e9087 The mini list structure is used as the list end to save RAM. This is checked and valid. */
pxList->uxNumberOfItems = ( UBaseType_t ) 0U;
/* Write known values into the list if
* configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */
listSET_LIST_INTEGRITY_CHECK_1_VALUE( pxList );
listSET_LIST_INTEGRITY_CHECK_2_VALUE( pxList );
#ifdef VERIFAST /*< ***change MiniList_t to ListItem_t*** */
pxList->xListEnd.pxContainer = pxList;
#endif
/*@ListItem_t *end = &(pxList->xListEnd);@*/
/*@close xLIST_ITEM(end, portMAX_DELAY, _, _, pxList);@*/
/*@close DLS(end, end, end, end, singleton(end), singleton(portMAX_DELAY), pxList);@*/
/*@close xLIST(pxList, 0, end, end, singleton(end), singleton(portMAX_DELAY));@*/
}

37
FreeRTOS/Test/VeriFast/list/vListInitialiseItem.c Normal file
View file

@ -0,0 +1,37 @@
/*
* FreeRTOS VeriFast Proofs
* Copyright (C) Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
#include "proof/list.h"
void vListInitialiseItem( ListItem_t * const pxItem )
/*@requires xLIST_ITEM(pxItem, _, _, _, _);@*/
/*@ensures xLIST_ITEM(pxItem, _, _, _, NULL);@*/
{
/* Make sure the list item is not recorded as being on a list. */
pxItem->pxContainer = NULL;
/* Write known values into the list item if
* configUSE_LIST_DATA_INTEGRITY_CHECK_BYTES is set to 1. */
listSET_FIRST_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxItem );
listSET_SECOND_LIST_ITEM_INTEGRITY_CHECK_VALUE( pxItem );
/*@close xLIST_ITEM(pxItem, _, _, _, NULL);@*/
}

316
FreeRTOS/Test/VeriFast/list/vListInsert.c Normal file
View file

@ -0,0 +1,316 @@
/*
* FreeRTOS VeriFast Proofs
* Copyright (C) Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
#include "proof/list.h"
ListItem_t * choose(List_t * list);
/*@ requires DLS(&(list->xListEnd), ?endprev, &(list->xListEnd), endprev, ?cells, ?vals, ?container);@*/
/*@ ensures DLS(&(list->xListEnd), endprev, &(list->xListEnd), endprev, cells, vals, container) &*&
mem(result, cells) == true;@*/
void vListInsert( List_t * const pxList,
ListItem_t * const pxNewListItem )
/*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals) &*&
xLIST_ITEM(pxNewListItem, ?val, _, _, _);@*/
/*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals) &*&
remove(pxNewListItem, new_cells) == cells
;@*/
{
/*@xLIST_star_item(pxList, pxNewListItem);@*/
/*@open xLIST_ITEM(pxNewListItem, _, _, _, _);@*/
/*@open xLIST(pxList, len, idx, end, cells, vals);@*/
/*@assert DLS(end, ?endprev, end, endprev, cells, vals, pxList);@*/
ListItem_t * pxIterator;
const TickType_t xValueOfInsertion = pxNewListItem->xItemValue;
/* Only effective when configASSERT() is also defined, these tests may catch
* the list data structures being overwritten in memory. They will not catch
* data errors caused by incorrect configuration or use of FreeRTOS. */
listTEST_LIST_INTEGRITY( pxList );
listTEST_LIST_ITEM_INTEGRITY( pxNewListItem );
/* Insert the new list item into the list, sorted in xItemValue order.
*
* If the list already contains a list item with the same item value then the
* new list item should be placed after it. This ensures that TCBs which are
* stored in ready lists (all of which have the same xItemValue value) get a
* share of the CPU. However, if the xItemValue is the same as the back marker
* the iteration loop below will not end. Therefore the value is checked
* first, and the algorithm slightly modified if necessary. */
if( xValueOfInsertion == portMAX_DELAY )
{
/*@open DLS(end, endprev, end, endprev, cells, vals, pxList);@*/
/*@open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList);@*/
/*@
if (end != endprev)
{
assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList);
if (endnext == endprev)
{
// done
}
else
{
dls_last_mem(endnext, end, end, endprev, tail(cells));
split(endnext, end, end, endprev, tail(cells), tail(vals), endprev, index_of(endprev, tail(cells)));
}
open DLS(endprev, _, _, _, _, _, _);
open xLIST_ITEM(endprev, _, _, _, _);
}
@*/
pxIterator = pxList->xListEnd.pxPrevious;
}
else
{
/* *** NOTE ***********************************************************
* If you find your application is crashing here then likely causes are
* listed below. In addition see https://www.freertos.org/FAQHelp.html for
* more tips, and ensure configASSERT() is defined!
* https://www.freertos.org/a00110.html#configASSERT
*
* 1) Stack overflow -
* see https://www.freertos.org/Stacks-and-stack-overflow-checking.html
* 2) Incorrect interrupt priority assignment, especially on Cortex-M
* parts where numerically high priority values denote low actual
* interrupt priorities, which can seem counter intuitive. See
* https://www.freertos.org/RTOS-Cortex-M3-M4.html and the definition
* of configMAX_SYSCALL_INTERRUPT_PRIORITY on
* https://www.freertos.org/a00110.html
* 3) Calling an API function from within a critical section or when
* the scheduler is suspended, or calling an API function that does
* not end in "FromISR" from an interrupt.
* 4) Using a queue or semaphore before it has been initialised or
* before the scheduler has been started (are interrupts firing
* before vTaskStartScheduler() has been called?).
**********************************************************************/
#ifdef VERIFAST /*< ***over-approximate list insert loop*** */
pxIterator = choose(pxList);
#else
for( pxIterator = ( ListItem_t * ) &( pxList->xListEnd ); pxIterator->pxNext->xItemValue <= xValueOfInsertion; pxIterator = pxIterator->pxNext ) /*lint !e826 !e740 !e9087 The mini list structure is used as the list end to save RAM. This is checked and valid. *//*lint !e440 The iterator moves to a different value, not xValueOfInsertion. */
{
/* There is nothing to do here, just iterating to the wanted
* insertion position. */
}
#endif
/*@int i = index_of(pxIterator, cells);@*/
/*@
if (pxIterator == end)
{
open DLS(end, endprev, end, endprev, cells, vals, pxList);
open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList);
if (end != endprev)
{
assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList);
open DLS(endnext, _, _, _, _, _, _);
open xLIST_ITEM(endnext, _, _, _, _);
}
}
else
{
assert DLS(end, endprev, end, endprev, cells, vals, pxList);
dls_first_mem(end, endprev, end, endprev, cells);
assert pxIterator != end;
assert index_of(end, cells) == 0;
split(end, endprev, end, endprev, cells, vals, pxIterator, i);
assert DLS(end, endprev, pxIterator, ?iterprev, take(i, cells), take(i, vals), pxList);
assert DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList);
open DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList);
open xLIST_ITEM(pxIterator, _, ?iternext, iterprev, pxList);
if (pxIterator == endprev)
{
open DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
take_take(1, i, vals);
assert xLIST_ITEM(end, portMAX_DELAY, _, _, _);
open xLIST_ITEM(iternext, _, _, pxIterator, _);
}
else
{
open DLS(iternext, pxIterator, end, endprev, _, _, _);
open xLIST_ITEM(iternext, _, _, pxIterator, _);
}
}@*/
}
pxNewListItem->pxNext = pxIterator->pxNext;
pxNewListItem->pxNext->pxPrevious = pxNewListItem;
pxNewListItem->pxPrevious = pxIterator;
pxIterator->pxNext = pxNewListItem;
/* Remember which list the item is in. This allows fast removal of the
* item later. */
pxNewListItem->pxContainer = pxList;
( pxList->uxNumberOfItems )++;
/*@close xLIST_ITEM(pxNewListItem, val, ?iternext, pxIterator, pxList);@*/
/*@close xLIST_ITEM(pxIterator, ?iterval, pxNewListItem, ?iterprev, pxList);@*/
/*@
if( xValueOfInsertion == portMAX_DELAY )
{
assert iternext == end;
assert pxIterator == endprev;
if (end == endprev)
{
close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList);
close DLS(pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
join(end, pxNewListItem, pxNewListItem, end, cells, vals,
pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
}
else
{
close xLIST_ITEM(end, portMAX_DELAY, ?endnext, pxNewListItem, pxList);
close DLS(pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
if (endnext == endprev)
{
assert xLIST_ITEM(endnext, ?endnextval, pxNewListItem, end, pxList);
close DLS(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY), pxList);
close DLS(endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval), pxList);
join(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY),
endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval));
assert DLS(end, pxNewListItem, pxNewListItem, endnext, cells, vals, pxList);
}
else
{
assert DLS(endnext, end, endprev, ?endprevprev, ?cells_endnext_to_endprevprev, ?vals_endnext_to_endprevprev, pxList);
assert cells_endnext_to_endprevprev == take(index_of(endprev, tail(cells)), tail(cells));
assert index_of(endprev, tail(cells)) == length(tail(cells)) - 1;
assert cells_endnext_to_endprevprev == take(length(tail(cells)) - 1, tail(cells));
assert xLIST_ITEM(endprev, ?endprevval, pxNewListItem, endprevprev, pxList);
close DLS(endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList);
dls_last_mem(endnext, end, endprev, endprevprev, cells_endnext_to_endprevprev);
dls_star_item(endnext, endprevprev, end);
close DLS(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev), pxList);
join(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev),
endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval));
assert DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList);
}
join(end, pxNewListItem, pxNewListItem, endprev, cells, vals,
pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
remove_append(pxNewListItem, cells, singleton(pxNewListItem));
close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
}
}
else
{
if (pxIterator == end)
{
if (iternext == end)
{
close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList);
close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
join(end, pxNewListItem, pxNewListItem, end, cells, vals,
pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
}
else
{
close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList);
if (iternext == endprev)
{
close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList);
dls_last_mem(iternext, pxNewListItem, end, endprev, singleton(iternext));
}
else
{
assert DLS(?iternextnext, iternext, end, endprev, ?cells_iternextnext_to_endprev, ?vals_iternextnext_to_endprev, pxList);
close DLS(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev), cons(iternextval, vals_iternextnext_to_endprev), pxList);
dls_last_mem(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev));
}
close DLS(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), pxList);
assert DLS(iternext, pxNewListItem, end, endprev, ?cells_iternext_to_endprev, ?vals_iternext_to_endprev, pxList);
dls_star_item(iternext, endprev, pxNewListItem);
close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev), pxList);
join(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY),
pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev));
close xLIST(pxList, len+1, idx, end, cons(end, cons(pxNewListItem, cells_iternext_to_endprev)), cons(portMAX_DELAY, cons(val, vals_iternext_to_endprev)));
}
}
else
{
close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList);
if (pxIterator == endprev)
{
if (iterprev == end)
{
close DLS(end, pxNewListItem, pxIterator, end, singleton(end), singleton(portMAX_DELAY), pxList);
}
else
{
assert DLS(_, iternext, pxIterator, iterprev, ?cells1, ?vals1, _);
close DLS(end, pxNewListItem, pxIterator, iterprev, cons(end, cells1), cons(portMAX_DELAY, vals1), pxList);
}
int i = index_of(pxIterator, cells);
assert DLS(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
close DLS(pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals), pxList);
close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
join(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals),
pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals));
join(end, pxNewListItem, pxNewListItem, pxIterator, cells, vals,
pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
remove_append(pxNewListItem, cells, singleton(pxNewListItem));
}
else
{
int i = index_of(pxIterator, cells);
if (iternext == endprev)
{
close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList);
}
else
{
assert DLS(_, iternext, end, endprev, ?cells0, ?vals0, pxList);
dls_star_item(end, iterprev, iternext);
close DLS(iternext, pxNewListItem, end, endprev, tail(drop(i, cells)), tail(drop(i, vals)), pxList);
}
drop_drop(1, i, cells);
drop_drop(1, i, vals);
assert DLS(iternext, pxNewListItem, end, endprev, drop(i+1, cells), drop(i+1, vals), pxList);
assert DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList);
dls_star_item(iternext, endprev, pxNewListItem);
dls_last_mem(iternext, pxNewListItem, end, endprev, drop(i+1, cells));
close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, drop(i+1, cells)), cons(val, drop(i+1, vals)), pxList);
close DLS(pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals))), pxList);
join(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals),
pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals))));
list<struct xLIST_ITEM * >new_cells = append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
list<TickType_t >new_vals = append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals))));
head_append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
take_head(take(i, cells));
take_take(1, i, cells);
assert( end == head(new_cells) );
head_append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals))));
take_head(take(i, vals));
take_take(1, i, vals);
assert( portMAX_DELAY == head(new_vals) );
append_take_drop_n(cells, index_of(pxIterator, cells));
close xLIST(pxList, len+1, idx, end, append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells)))), append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals)))));
mem_take_false(pxNewListItem, i, cells);
remove_append(pxNewListItem, take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))));
}
}
}@*/
}

234
FreeRTOS/Test/VeriFast/list/vListInsertEnd.c Normal file
View file

@ -0,0 +1,234 @@
/*
* FreeRTOS VeriFast Proofs
* Copyright (C) Amazon.com, Inc. or its affiliates. All Rights Reserved.
*
* Permission is hereby granted, free of charge, to any person obtaining a copy of
* this software and associated documentation files (the "Software"), to deal in
* the Software without restriction, including without limitation the rights to
* use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
* the Software, and to permit persons to whom the Software is furnished to do so,
* subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
* FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
* COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
* IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
* CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
*/
#include "proof/list.h"
void vListInsertEnd( List_t * const pxList,
ListItem_t * const pxNewListItem )
/*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals) &*&
xLIST_ITEM(pxNewListItem, ?val, _, _, _);@*/
/*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals) &*&
idx == end
? (new_cells == append(cells, singleton(pxNewListItem)) &*&
new_vals == append(vals, singleton(val)))
: (new_cells == append(take(index_of(idx, cells), cells), append(singleton(pxNewListItem), drop(index_of(idx, cells), cells))) &*&
new_vals == append(take(index_of(idx, cells), vals), append(singleton(val), drop(index_of(idx, cells), vals))));@*/
{
/*@xLIST_star_item(pxList, pxNewListItem);@*/
/*@assert mem(pxNewListItem, cells) == false;@*/
/*@open xLIST(pxList, len, idx, end, cells, vals);@*/
#ifdef VERIFAST /*< const pointer declaration */
ListItem_t * pxIndex = pxList->pxIndex;
#else
ListItem_t * const pxIndex = pxList->pxIndex;
/* Only effective when configASSERT() is also defined, these tests may catch
* the list data structures being overwritten in memory. They will not catch
* data errors caused by incorrect configuration or use of FreeRTOS. */
listTEST_LIST_INTEGRITY( pxList );
listTEST_LIST_ITEM_INTEGRITY( pxNewListItem );
#endif
/*@open xLIST_ITEM(pxNewListItem, _, _, _, _);@*/
/*@assert DLS(end, ?endprev, end, _, cells, vals, pxList);@*/
/*@dls_first_mem(end, endprev, end, endprev, cells);@*/
/*@dls_last_mem(end, endprev, end, endprev, cells);@*/
/*@
if (end == idx)
{
open DLS(end, endprev, end, endprev, cells, vals, pxList);
open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList);
if (end == endprev)
{
// Case A (singleton): idx==end==endprev
}
else
{
assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList);
if (endnext == endprev)
{
// Case B (two): idx==end and endnext==endprev
open DLS(endnext, end, end, endnext, _, _, _);
open xLIST_ITEM(endnext, _, _, _, _);
}
else
{
// Case C: idx==end and DLS:endnext...endprev
split(endnext, end, end, endprev, tail(cells), tail(vals), endprev, index_of(endprev, tail(cells)));
open DLS(endprev, _, _, _, _, _, _);
open xLIST_ITEM(endprev, _, _, _, _);
}
}
}
else
{
int i = index_of(idx, cells);
split(end, endprev, end, endprev, cells, vals, idx, i);
assert DLS(end, endprev, idx, ?idxprev, take(i, cells), take(i, vals), pxList);
assert DLS(idx, idxprev, end, endprev, drop(i, cells), drop(i, vals), pxList);
open DLS(idx, idxprev, end, endprev, _, _, _);
open xLIST_ITEM(idx, _, _, _, _);
if (end == idxprev)
{
// Case D: end==idxprev and DLS:idx...endprev
take_take(1, i, vals);
take_head(vals);
open DLS(end, endprev, idx, idxprev, take(i, cells), take(i, vals), pxList);
open xLIST_ITEM(end, portMAX_DELAY, _, _, _);
assert length(take(i, cells)) == 1;
}
else
{
// Case E: DLS:end...idxprev and DLS:idx...endprev
dls_last_mem(end, endprev, idx, idxprev, take(i, cells));
split(end, endprev, idx, idxprev, take(i, cells), take(i, vals), idxprev, index_of(idxprev, take(i, cells)));
open DLS(idxprev, _, _, idxprev, _, _, _);
length_take(i, cells);
drop_take_singleton(i, vals);
open xLIST_ITEM(idxprev, nth(i-1, vals), _, _, _);
}
}
@*/
/* Insert a new list item into pxList, but rather than sort the list,
* makes the new list item the last item to be removed by a call to
* listGET_OWNER_OF_NEXT_ENTRY(). */
pxNewListItem->pxNext = pxIndex;
pxNewListItem->pxPrevious = pxIndex->pxPrevious;
/* Only used during decision coverage testing. */
mtCOVERAGE_TEST_DELAY();
pxIndex->pxPrevious->pxNext = pxNewListItem;
pxIndex->pxPrevious = pxNewListItem;
/* Remember which list the item is in. */
pxNewListItem->pxContainer = pxList;
( pxList->uxNumberOfItems )++;
/*@
if (end == idx)
{
close xLIST_ITEM(pxNewListItem, val, end, endprev, pxList);
close DLS(pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList);
close xLIST_ITEM(end, portMAX_DELAY, ?endnext, pxNewListItem, pxList);
if (end == endprev)
{
// Case A (singleton): idx==end==endprev
close DLS(end, pxNewListItem, endnext, end, cells, vals, pxList);
join(end, pxNewListItem, endnext, end, cells, vals,
pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
}
else
{
close xLIST_ITEM(endprev, ?endprevval, pxNewListItem, ?endprevprev, _);
if (endnext == endprev)
{
// Case B (two): idx==end and endnext==endprev
close DLS(endprev, end, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList);
close DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList);
join(end, pxNewListItem, pxNewListItem, endprev, cells, vals,
pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
}
else
{
// Case C: idx==end and DLS:endnext...endprev
close DLS(endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList);
assert DLS(endnext, end, endprev, endprevprev, ?cells_endnext_to_endprevprev, ?vals_endnext_to_endprevprev, pxList);
join(endnext, end, endprev, endprevprev, cells_endnext_to_endprevprev, vals_endnext_to_endprevprev,
endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval));
close DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList);
join(end, pxNewListItem, pxNewListItem, endprev, cells, vals,
pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val));
close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val)));
}
}
}
else
{
// Case D: end==idxprev and DLS:idx...endprev
// Case E: DLS:end...idxprev and DLS:idx...endprev
int i = index_of(idx, cells);
close xLIST_ITEM(pxNewListItem, val, idx, ?idxprev, pxList);
close xLIST_ITEM(idx, ?idxval, ?idxnext, pxNewListItem, pxList);
nth_drop2(vals, i);
assert idxval == nth(i, vals);
close xLIST_ITEM(idxprev, ?idxprevval, pxNewListItem, ?idxprevprev, pxList);
if (end == idxprev)
{
close DLS(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), pxList);
}
else
{
length_take(i, cells);
take_take(i-1, i, vals);
take_singleton(i-1, vals);
take_singleton(i, vals);
assert DLS(end, endprev, idxprev, idxprevprev, ?cells_end_to_idxprevprev, take(i-1, vals), pxList);
close DLS(idxprev, idxprevprev, pxNewListItem, idxprev, singleton(idxprev), singleton(idxprevval), pxList);
join(end, endprev, idxprev, idxprevprev, cells_end_to_idxprevprev, take(i-1, vals),
idxprev, idxprevprev, pxNewListItem, idxprev, singleton(idxprev), singleton(idxprevval));
}
if (idx == endprev)
{
close DLS(idx, pxNewListItem, end, idx, singleton(idx), singleton(idxval), pxList);
}
else
{
assert DLS(end, endprev, pxNewListItem, idxprev, ?cells_end_to_idxprev, ?vals_end_to_idxprev, pxList);
close DLS(idx, pxNewListItem, end, endprev, drop(i, cells), drop(i, vals), pxList);
}
assert DLS(end, endprev, pxNewListItem, idxprev, take(i, cells), take(i, vals), pxList);
assert DLS(idx, pxNewListItem, end, endprev, drop(i, cells), drop(i, vals), pxList);
assert xLIST_ITEM(pxNewListItem, val, idx, idxprev, pxList);
dls_star_item(idx, endprev, pxNewListItem);
close DLS(pxNewListItem, idxprev, end, endprev, cons(pxNewListItem, drop(i, cells)), cons(val, drop(i, vals)), pxList);
join(end, endprev, pxNewListItem, idxprev, take(i, cells), take(i, vals),
pxNewListItem, idxprev, end, endprev, cons(pxNewListItem, drop(i, cells)), cons(val, drop(i, vals)));
assert DLS(end, endprev, end, endprev, ?cells_new, ?vals_new, pxList);
assert cells_new == append(take(i, cells), append(singleton(pxNewListItem), drop(i, cells)));
assert vals_new == append(take(i, vals) , append(singleton(val), drop(i, vals)));
head_append(take(i, cells), append(singleton(pxNewListItem), drop(i, cells)));
take_take(1, i, cells);
head_append(take(i, vals), append(singleton(val), drop(i, vals)));
take_take(1, i, vals);
close xLIST(pxList, len+1, idx, end, cells_new, vals_new);
}
@*/
}
void client_example1( List_t * const l, ListItem_t * const pxNewListItem )
/*@requires
xLIST(l, ?len, ?idx, ?end, ?cells, ?vals) &*&
xLIST_ITEM(pxNewListItem, ?val, _, _, _) &*&
idx == end;@*/
/*@ensures
xLIST(l, len + 1, idx, end, _, append(vals, singleton(val)));@*/
{
vListInsertEnd(l, pxNewListItem);
}

2
FreeRTOS/Test/VeriFast/scripts/annotation_overhead.sh
View file

@ -1,3 +1,3 @@
#!/bin/bash -eu
NO_COVERAGE=1 EXTRA_VERIFAST_ARGS=-stats make queue | grep overhead: | sort | uniq
NO_COVERAGE=1 EXTRA_VERIFAST_ARGS=-stats make queue list | grep overhead: | sort | uniq

4
FreeRTOS/Test/VeriFast/scripts/diff_files.md
View file

@ -16,7 +16,7 @@ implementation and the proof directory.
```
cd scripts
./generate_diff_files.sh
# will extract to ./FreeRTOS-Kernel/generated and ./queue/generated
# will extract to ./FreeRTOS-Kernel/generated and ./queue/generated and ./list/generated
```
Then use `diff` for a side-by-side comparison. Note that the `--color=always`
@ -24,12 +24,14 @@ flag needs v3.4+:
```
diff --color=always --width=$COLUMNS --suppress-common-lines --side-by-side FreeRTOS-Kernel/generated queue/generated | less -r
diff --color=always --width=$COLUMNS --suppress-common-lines --side-by-side FreeRTOS-Kernel/generated list/generated | less -r
```
Or generate a html report using `diff2html`:
```
diff -u FreeRTOS-Kernel/generated queue/generated | diff2html -i stdin
diff -u FreeRTOS-Kernel/generated list/generated | diff2html -i stdin
```
The expectation is that the proofs make minimal changes to the original source

29
FreeRTOS/Test/VeriFast/scripts/generate_diff_files.sh
View file

@ -1,6 +1,6 @@
#!/bin/bash -eu
FUNCS=(
QUEUE_FUNCS=(
prvCopyDataFromQueue
prvCopyDataToQueue
prvInitialiseNewQueue
@ -22,6 +22,14 @@ FUNCS=(
xQueueReceiveFromISR
)
LIST_FUNCS=(
uxListRemove
vListInitialise
vListInitialiseItem
vListInsertEnd
vListInsert
)
if [ ! -d "FreeRTOS-Kernel" ]; then
git clone https://github.com/FreeRTOS/FreeRTOS-Kernel.git
fi
@ -29,7 +37,11 @@ pushd FreeRTOS-Kernel > /dev/null
rm -rf tags generated
ctags --excmd=number queue.c
mkdir generated
for f in ${FUNCS[@]}; do
for f in ${QUEUE_FUNCS[@]}; do
../extract.py tags $f > generated/$f.c
done
ctags --excmd=number list.c
for f in ${LIST_FUNCS[@]}; do
../extract.py tags $f > generated/$f.c
done
popd > /dev/null
@ -40,8 +52,19 @@ pushd queue > /dev/null
rm -rf tags generated
ctags --excmd=number *.c
mkdir generated
for f in ${FUNCS[@]}; do
for f in ${QUEUE_FUNCS[@]}; do
../scripts/extract.py tags $f > generated/$f.c
done
popd > /dev/null
echo "created: queue/generated"
ln -fs ../list .
pushd list > /dev/null
rm -rf tags generated
ctags --excmd=number *.c
mkdir generated
for f in ${LIST_FUNCS[@]}; do
../scripts/extract.py tags $f > generated/$f.c
done
popd > /dev/null
echo "created: list/generated"