begriffs open source - cmsis-freertos/blob - Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/prvNotifyQueueSetContainer_harness.c

   1 /*
   2  * FreeRTOS memory safety proofs with CBMC.
   3  * Copyright (C) 2019 Amazon.com, Inc. or its affiliates.  All Rights Reserved.
   4  *
   5  * Permission is hereby granted, free of charge, to any person
   6  * obtaining a copy of this software and associated documentation
   7  * files (the "Software"), to deal in the Software without
   8  * restriction, including without limitation the rights to use, copy,
   9  * modify, merge, publish, distribute, sublicense, and/or sell copies
  10  * of the Software, and to permit persons to whom the Software is
  11  * furnished to do so, subject to the following conditions:
  12  *
  13  * The above copyright notice and this permission notice shall be
  14  * included in all copies or substantial portions of the Software.
  15  *
  16  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
  17  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
  18  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  19  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS
  20  * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN
  21  * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
  22  * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
  23  * SOFTWARE.
  24  *
  25  * http://aws.amazon.com/freertos
  26  * http://www.FreeRTOS.org
  27  */
  28
  29 #include "FreeRTOS.h"
  30 #include "queue.h"
  31 #include "queue_datastructure.h"
  32 #include "cbmc.h"
  33
  34 #ifndef LOCK_BOUND
  35     #define LOCK_BOUND    4
  36 #endif
  37
  38 BaseType_t prvNotifyQueueSetContainer( const Queue_t * const pxQueue,
  39                                        const BaseType_t xCopyPosition );
  40
  41 BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue,
  42                                const void * pvItemToQueue,
  43                                const BaseType_t xPosition )
  44 {
  45     if( pxQueue->uxItemSize > ( UBaseType_t ) 0 )
  46     {
  47         __CPROVER_assert( __CPROVER_r_ok( pvItemToQueue, ( size_t ) pxQueue->uxItemSize ), "pvItemToQueue region must be readable" );
  48
  49         if( xPosition == queueSEND_TO_BACK )
  50         {
  51             __CPROVER_assert( __CPROVER_w_ok( ( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize ), "pxQueue->pcWriteTo region must be writable" );
  52         }
  53         else
  54         {
  55             __CPROVER_assert( __CPROVER_w_ok( ( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize ), "pxQueue->u.xQueue.pcReadFrom region must be writable" );
  56         }
  57
  58         return pdFALSE;
  59     }
  60     else
  61     {
  62         return nondet_BaseType_t();
  63     }
  64 }
  65
  66 QueueSetHandle_t xUnconstrainedQueueSet()
  67 {
  68     UBaseType_t uxEventQueueLength = 2;
  69     QueueSetHandle_t xSet = xQueueCreateSet( uxEventQueueLength );
  70
  71     if( xSet )
  72     {
  73         xSet->cTxLock = nondet_int8_t();
  74         __CPROVER_assume( xSet->cTxLock != 127 );
  75         xSet->cRxLock = nondet_int8_t();
  76         xSet->uxMessagesWaiting = nondet_UBaseType_t();
  77         xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
  78         xSet->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
  79     }
  80
  81     return xSet;
  82 }
  83
  84 void harness()
  85 {
  86     UBaseType_t uxQueueLength;
  87     UBaseType_t uxItemSize;
  88     uint8_t ucQueueType;
  89
  90     __CPROVER_assume( uxQueueLength > 0 );
  91     __CPROVER_assume( uxItemSize < 10 );
  92
  93     /* The implicit assumption for the QueueGenericCreate method is,
  94      * that there are no overflows in the computation and the inputs are safe.
  95      * There is no check for this in the code base */
  96     UBaseType_t upper_bound = portMAX_DELAY - sizeof( Queue_t );
  97     __CPROVER_assume( uxItemSize < ( upper_bound ) / uxQueueLength );
  98     QueueHandle_t xQueue =
  99         xQueueGenericCreate( uxQueueLength, uxItemSize, ucQueueType );
 100
 101     if( xQueue )
 102     {
 103         xQueueAddToSet( xQueue, xUnconstrainedQueueSet() );
 104
 105         if( xQueue->pxQueueSetContainer )
 106         {
 107             __CPROVER_assume( xQueue->pxQueueSetContainer->uxMessagesWaiting < xQueue->pxQueueSetContainer->uxLength );
 108             BaseType_t xCopyPosition = nondet_BaseType_t();
 109             prvNotifyQueueSetContainer( xQueue, xCopyPosition );
 110         }
 111     }
 112 }