mirror of
https://github.com/FreeRTOS/FreeRTOS-Kernel.git
synced 2025-10-17 02:07:48 -04:00
Update VeriFast proofs (#836)
* Undo syntax changes preventing VeriFast parsing * Update proofs inline with source changes Outstanding: - xQueueGenericReset return code - Not using prvIncrementQueueTxLock or prvIncrementQueueRxLock macros * Remove git hash check * Document new changes between proven code and implementation * Update copyright header * VeriFast proofs: turn off uncrustify checks Uncrustify requires formatting of comments that is at odds with VeriFast's proof annotations, which are contained within comments. * Update ci.yml Co-authored-by: Joseph Julicher <jjulicher@mac.com> Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com>
This commit is contained in:
Nathan Chong
GitHub
parent
4e0fecaadd
commit
4f87f485d5
32 changed files with 1877 additions and 1864 deletions
|
|
@ -24,27 +24,27 @@
|
|||
*
|
||||
*/
|
||||
|
||||
/* *INDENT-OFF* */
|
||||
|
||||
#include "proof/queue.h"
|
||||
|
||||
static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
|
||||
const void * pvItemToQueue,
|
||||
const BaseType_t xPosition )
|
||||
|
||||
/*@requires queue(pxQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
|
||||
* (K < N || xPosition == queueOVERWRITE) &*&
|
||||
* chars(pvItemToQueue, M, ?x) &*&
|
||||
* (xPosition == queueSEND_TO_BACK || xPosition == queueSEND_TO_FRONT || (xPosition == queueOVERWRITE && N == 1));@*/
|
||||
|
||||
(K < N || xPosition == queueOVERWRITE) &*&
|
||||
chars(pvItemToQueue, M, ?x) &*&
|
||||
(xPosition == queueSEND_TO_BACK || xPosition == queueSEND_TO_FRONT || (xPosition == queueOVERWRITE && N == 1));@*/
|
||||
/*@ensures
|
||||
* (xPosition == queueSEND_TO_BACK
|
||||
* ? queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x)))
|
||||
* : (xPosition == queueSEND_TO_FRONT
|
||||
* ? (R == 0
|
||||
* ? queue(pxQueue, Storage, N, M, W, (N-1), (K+1), is_locked, cons(x, abs))
|
||||
* : queue(pxQueue, Storage, N, M, W, (R-1), (K+1), is_locked, cons(x, abs)))
|
||||
* : xPosition == queueOVERWRITE &*& queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x)))
|
||||
* ) &*&
|
||||
* chars(pvItemToQueue, M, x);@*/
|
||||
(xPosition == queueSEND_TO_BACK
|
||||
? queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x)))
|
||||
: (xPosition == queueSEND_TO_FRONT
|
||||
? (R == 0
|
||||
? queue(pxQueue, Storage, N, M, W, (N-1), (K+1), is_locked, cons(x, abs))
|
||||
: queue(pxQueue, Storage, N, M, W, (R-1), (K+1), is_locked, cons(x, abs)))
|
||||
: xPosition == queueOVERWRITE &*& queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x)))
|
||||
) &*&
|
||||
chars(pvItemToQueue, M, x);@*/
|
||||
{
|
||||
BaseType_t xReturn = pdFALSE;
|
||||
UBaseType_t uxMessagesWaiting;
|
||||
|
|
@ -76,29 +76,27 @@ static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
|
|||
}
|
||||
else if( xPosition == queueSEND_TO_BACK )
|
||||
{
|
||||
#ifdef VERIFAST /*< void cast of unused return value */
|
||||
|
||||
/* Now we focus the proof on the logical element of the buffer that
|
||||
* will be updated using the following lemma to split the buffer into 3
|
||||
* parts: a prefix, the element we want to update, and the suffix. This
|
||||
* enables the subsequent memcpy to verify. */
|
||||
/*@split_element(Storage, N, M, W);@*/
|
||||
|
||||
/*@assert
|
||||
* buffer(Storage, W, M, ?prefix) &*&
|
||||
* chars(Storage + W * M, M, _) &*&
|
||||
* buffer(Storage + (W + 1) * M, (N-1-W), M, ?suffix);@*/
|
||||
memcpy( ( void * ) pxQueue->pcWriteTo, pvItemToQueue, ( size_t ) pxQueue->uxItemSize );
|
||||
/* After the update we stitch the buffer back together */
|
||||
/*@join_element(Storage, N, M, W);@*/
|
||||
/*@combine_list_update(prefix, x, suffix, W, contents);@*/
|
||||
#else
|
||||
( void ) memcpy( ( void * ) pxQueue->pcWriteTo, pvItemToQueue, ( size_t ) pxQueue->uxItemSize ); /*lint !e961 !e418 !e9087 MISRA exception as the casts are only redundant for some ports, plus previous logic ensures a null pointer can only be passed to memcpy() if the copy size is 0. Cast to void required by function signature and safe as no alignment requirement and copy length specified in bytes. */
|
||||
#endif /* ifdef VERIFAST */
|
||||
#ifdef VERIFAST /*< void cast of unused return value */
|
||||
/* Now we focus the proof on the logical element of the buffer that
|
||||
* will be updated using the following lemma to split the buffer into 3
|
||||
* parts: a prefix, the element we want to update, and the suffix. This
|
||||
* enables the subsequent memcpy to verify. */
|
||||
/*@split_element(Storage, N, M, W);@*/
|
||||
/*@assert
|
||||
buffer(Storage, W, M, ?prefix) &*&
|
||||
chars(Storage + W * M, M, _) &*&
|
||||
buffer(Storage + (W + 1) * M, (N-1-W), M, ?suffix);@*/
|
||||
memcpy( ( void * ) pxQueue->pcWriteTo, pvItemToQueue, ( size_t ) pxQueue->uxItemSize );
|
||||
/* After the update we stitch the buffer back together */
|
||||
/*@join_element(Storage, N, M, W);@*/
|
||||
/*@combine_list_update(prefix, x, suffix, W, contents);@*/
|
||||
#else
|
||||
( void ) memcpy( ( void * ) pxQueue->pcWriteTo, pvItemToQueue, ( size_t ) pxQueue->uxItemSize ); /*lint !e961 !e418 !e9087 MISRA exception as the casts are only redundant for some ports, plus previous logic ensures a null pointer can only be passed to memcpy() if the copy size is 0. Cast to void required by function signature and safe as no alignment requirement and copy length specified in bytes. */
|
||||
#endif
|
||||
/*@mul_mono_l(W, N-1, M);@*/
|
||||
pxQueue->pcWriteTo += pxQueue->uxItemSize; /*lint !e9016 Pointer arithmetic on char types ok, especially in this use case where it is the clearest way of conveying intent. */
|
||||
pxQueue->pcWriteTo += pxQueue->uxItemSize; /*lint !e9016 Pointer arithmetic on char types ok, especially in this use case where it is the clearest way of conveying intent. */
|
||||
|
||||
if( pxQueue->pcWriteTo >= pxQueue->u.xQueue.pcTail ) /*lint !e946 MISRA exception justified as comparison of pointers is the cleanest solution. */
|
||||
if( pxQueue->pcWriteTo >= pxQueue->u.xQueue.pcTail ) /*lint !e946 MISRA exception justified as comparison of pointers is the cleanest solution. */
|
||||
{
|
||||
/*@div_leq(N, W+1, M);@*/ /* now we know W == N-1 so (W+1)%N == 0 */
|
||||
pxQueue->pcWriteTo = pxQueue->pcHead;
|
||||
|
|
@ -106,29 +104,28 @@ static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
|
|||
else
|
||||
{
|
||||
/*@{
|
||||
* div_lt(W+1, N, M); // now we know W+1 < N
|
||||
* mod_lt(W+1, N); // so, W+1 == (W+1)%N
|
||||
* note(pxQueue->pcWriteTo == Storage + ((W + 1) * M));
|
||||
* note( Storage + ((W + 1) * M) == Storage + (((W + 1) % N) * M));
|
||||
* }@*/
|
||||
div_lt(W+1, N, M); // now we know W+1 < N
|
||||
mod_lt(W+1, N); // so, W+1 == (W+1)%N
|
||||
note(pxQueue->pcWriteTo == Storage + ((W + 1) * M));
|
||||
note( Storage + ((W + 1) * M) == Storage + (((W + 1) % N) * M));
|
||||
}@*/
|
||||
mtCOVERAGE_TEST_MARKER();
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
#ifdef VERIFAST /*< void cast of unused return value */
|
||||
/*@split_element(Storage, N, M, R);@*/
|
||||
|
||||
/*@assert
|
||||
* buffer(Storage, R, M, ?prefix) &*&
|
||||
* chars(Storage + R * M, M, _) &*&
|
||||
* buffer(Storage + (R + 1) * M, (N-1-R), M, ?suffix);@*/
|
||||
memcpy( ( void * ) pxQueue->u.xQueue.pcReadFrom, pvItemToQueue, ( size_t ) pxQueue->uxItemSize );
|
||||
/*@join_element(Storage, N, M, R);@*/
|
||||
/*@combine_list_update(prefix, x, suffix, R, contents);@*/
|
||||
#else
|
||||
( void ) memcpy( ( void * ) pxQueue->u.xQueue.pcReadFrom, pvItemToQueue, ( size_t ) pxQueue->uxItemSize ); /*lint !e961 !e9087 !e418 MISRA exception as the casts are only redundant for some ports. Cast to void required by function signature and safe as no alignment requirement and copy length specified in bytes. Assert checks null pointer only used when length is 0. */
|
||||
#endif
|
||||
#ifdef VERIFAST /*< void cast of unused return value */
|
||||
/*@split_element(Storage, N, M, R);@*/
|
||||
/*@assert
|
||||
buffer(Storage, R, M, ?prefix) &*&
|
||||
chars(Storage + R * M, M, _) &*&
|
||||
buffer(Storage + (R + 1) * M, (N-1-R), M, ?suffix);@*/
|
||||
memcpy( ( void * ) pxQueue->u.xQueue.pcReadFrom, pvItemToQueue, ( size_t ) pxQueue->uxItemSize );
|
||||
/*@join_element(Storage, N, M, R);@*/
|
||||
/*@combine_list_update(prefix, x, suffix, R, contents);@*/
|
||||
#else
|
||||
( void ) memcpy( ( void * ) pxQueue->u.xQueue.pcReadFrom, pvItemToQueue, ( size_t ) pxQueue->uxItemSize ); /*lint !e961 !e9087 !e418 MISRA exception as the casts are only redundant for some ports. Cast to void required by function signature and safe as no alignment requirement and copy length specified in bytes. Assert checks null pointer only used when length is 0. */
|
||||
#endif
|
||||
pxQueue->u.xQueue.pcReadFrom -= pxQueue->uxItemSize;
|
||||
|
||||
if( pxQueue->u.xQueue.pcReadFrom < pxQueue->pcHead ) /*lint !e946 MISRA exception justified as comparison of pointers is the cleanest solution. */
|
||||
|
|
@ -146,12 +143,12 @@ static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
|
|||
}
|
||||
|
||||
/*@
|
||||
* if (R == 0)
|
||||
* {
|
||||
* mod_plus(N, (K+1), N); mod_same(N); mod_mod(K+1, N);
|
||||
* assert W == ((N-1) + 1 + (K+1)) % N;
|
||||
* }
|
||||
* @*/
|
||||
if (R == 0)
|
||||
{
|
||||
mod_plus(N, (K+1), N); mod_same(N); mod_mod(K+1, N);
|
||||
assert W == ((N-1) + 1 + (K+1)) % N;
|
||||
}
|
||||
@*/
|
||||
if( xPosition == queueOVERWRITE )
|
||||
{
|
||||
if( uxMessagesWaiting > ( UBaseType_t ) 0 )
|
||||
|
|
@ -176,20 +173,22 @@ static BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
|
|||
pxQueue->uxMessagesWaiting = uxMessagesWaiting + ( UBaseType_t ) 1;
|
||||
|
||||
/*@
|
||||
* if (xPosition == queueSEND_TO_BACK)
|
||||
* {
|
||||
* enq_lemma(K, (R+1)%N, contents, abs, x);
|
||||
* mod_plus_one(W, R + 1 + K, N);
|
||||
* mod_plus_distr(R+1, K, N);
|
||||
* }
|
||||
* else if (xPosition == queueSEND_TO_FRONT)
|
||||
* {
|
||||
* front_enq_lemma(K, R, contents, abs, x);
|
||||
* if (0 < R)
|
||||
* {
|
||||
* mod_lt(R, N);
|
||||
* }
|
||||
* }
|
||||
* @*/
|
||||
if (xPosition == queueSEND_TO_BACK)
|
||||
{
|
||||
enq_lemma(K, (R+1)%N, contents, abs, x);
|
||||
mod_plus_one(W, R + 1 + K, N);
|
||||
mod_plus_distr(R+1, K, N);
|
||||
}
|
||||
else if (xPosition == queueSEND_TO_FRONT)
|
||||
{
|
||||
front_enq_lemma(K, R, contents, abs, x);
|
||||
if (0 < R)
|
||||
{
|
||||
mod_lt(R, N);
|
||||
}
|
||||
}
|
||||
@*/
|
||||
return xReturn;
|
||||
}
|
||||
|
||||
/* *INDENT-ON* */
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue