Copying CBMC proofs from aws/amazon-freertos repo ./tools/cbmc to this repo ./FreeRTOS/Test/CBMC as is.

The commit ID in aws/amazon-freertos is 0c8e0217f2a43bdeb364b58ae01c6c259e03ef1b.

FreeRTOS/Test/CBMC/include/README.md

@@ -0,0 +1,2 @@
+This directory contains include files used by the CBMC proofs:
+* cbmc.h defines some macros used in the proof test harnesses

FreeRTOS/Test/CBMC/include/aws_freertos_ip_verification_access_ip_define.h

@@ -0,0 +1,3 @@
+eFrameProcessingResult_t publicProcessIPPacket( IPPacket_t * const pxIPPacket, NetworkBufferDescriptor_t * const pxNetworkBuffer ) {
+	prvProcessIPPacket(pxIPPacket, pxNetworkBuffer);
+}

FreeRTOS/Test/CBMC/include/aws_freertos_tcp_verification_access_tcp_define.h

@@ -0,0 +1,12 @@
+int32_t publicTCPPrepareSend( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer, UBaseType_t uxOptionsLength ) {
+	prvTCPPrepareSend( pxSocket, ppxNetworkBuffer, uxOptionsLength );
+}
+
+BaseType_t publicTCPHandleState( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t **ppxNetworkBuffer ) {
+	prvTCPHandleState(pxSocket, ppxNetworkBuffer);
+}
+
+void publicTCPReturnPacket( FreeRTOS_Socket_t *pxSocket, NetworkBufferDescriptor_t *pxNetworkBuffer,
+	uint32_t ulLen, BaseType_t xReleaseAfterSend ) {
+	prvTCPReturnPacket(pxSocket, pxNetworkBuffer, ulLen, xReleaseAfterSend );
+}

FreeRTOS/Test/CBMC/include/cbmc.h

@@ -0,0 +1,67 @@
+/*
+ * CBMC models a pointer as an object id and an offset into that
+ * object.  The top bits of a pointer encode the object id and the
+ * remaining bits encode the offset.  This means there is a bound on
+ * the maximum offset into an object in CBMC, and hence a bound on the
+ * size of objects in CBMC.
+ */
+#define CBMC_BITS 7
+#define CBMC_MAX_OBJECT_SIZE (0xFFFFFFFF >> CBMC_BITS)
+
+enum CBMC_LOOP_CONDITION { CBMC_LOOP_BREAK, CBMC_LOOP_CONTINUE, CBMC_LOOP_RETURN };
+
+// CBMC specification: capture old value for precondition /
+// postcondition checking
+
+#define OLDVAL(var) _old_ ## var
+#define SAVE_OLDVAL(var,typ) const typ OLDVAL(var) = var
+
+// CBMC specification: capture old value for values passed by
+// reference in function abstractions
+
+#define OBJ(var) (*var)
+#define OLDOBJ(var) _oldobj_ ## var
+#define SAVE_OLDOBJ(var,typ) const typ OLDOBJ(var) = OBJ(var)
+
+// CBMC debugging: printfs for expressions
+
+#define __CPROVER_printf(var) { uint32_t ValueOf_ ## var = (uint32_t) var; }
+#define __CPROVER_printf2(str,exp) { uint32_t ValueOf_ ## str = (uint32_t) (exp); }
+
+// CBMC debugging: printfs for pointer expressions
+
+#define __CPROVER_printf_ptr(var) { uint8_t *ValueOf_ ## var = (uint8_t *) var; }
+#define __CPROVER_printf2_ptr(str,exp) { uint8_t *ValueOf_ ## str = (uint8_t *) (exp); }
+
+/*
+ * An assertion that pvPortMalloc returns NULL when asked to allocate 0 bytes.
+ * This assertion is used in some of the Task proofs.
+ */
+#define __CPROVER_assert_zero_allocation() \
+        __CPROVER_assert( pvPortMalloc(0) == NULL, \
+			  "pvPortMalloc allows zero-allocated memory.")
+
+/*
+ * A stub for pvPortMalloc that nondeterministically chooses to return
+ * either NULL or an allocation of the requested space.  The stub is
+ * guaranteed to return NULL when asked to allocate 0 bytes.
+ * This stub is used in some of the Task proofs.
+ */
+void *pvPortMalloc( size_t xWantedSize )
+{
+	if ( xWantedSize == 0 )
+	{
+		return NULL;
+	}
+	return nondet_bool() ? malloc( xWantedSize ) : NULL;
+}
+
+void vPortFree( void *pv )
+{
+	(void)pv;
+	free(pv);
+}
+
+BaseType_t nondet_basetype();
+UBaseType_t nondet_ubasetype();
+TickType_t nondet_ticktype();

FreeRTOS/Test/CBMC/include/queue_init.h

@@ -0,0 +1,141 @@
+#include "FreeRTOS.h"
+#include "queue.h"
+#include "queue_datastructure.h"
+
+#ifndef CBMC_OBJECT_BITS
+#define CBMC_OBJECT_BITS 7
+#endif
+
+#ifndef CBMC_OBJECT_MAX_SIZE
+#define CBMC_OBJECT_MAX_SIZE (UINT32_MAX>>(CBMC_OBJECT_BITS+1))
+#endif
+
+/* Using prvCopyDataToQueue together with prvNotifyQueueSetContainer
+   leads to a problem space explosion. Therefore, we use this stub
+   and a sepearted proof on prvCopyDataToQueue to deal with it.
+   As prvNotifyQueueSetContainer is disabled if configUSE_QUEUE_SETS != 1,
+   in other cases the original implementation should be used. */
+#if( configUSE_QUEUE_SETS == 1 )
+	BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition )
+	{
+		if(pxQueue->uxItemSize > ( UBaseType_t ) 0)
+		{
+			__CPROVER_assert(__CPROVER_r_ok(pvItemToQueue, ( size_t ) pxQueue->uxItemSize), "pvItemToQueue region must be readable");
+			if(xPosition == queueSEND_TO_BACK){
+				__CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->pcWriteTo, ( size_t ) pxQueue->uxItemSize), "pxQueue->pcWriteTo region must be writable");
+			}else{
+				__CPROVER_assert(__CPROVER_w_ok(( void * ) pxQueue->u.xQueue.pcReadFrom, ( size_t ) pxQueue->uxItemSize), "pxQueue->u.xQueue.pcReadFrom region must be writable");
+			}
+			return pdFALSE;
+		}else
+		{
+			return nondet_BaseType_t();
+		}
+	}
+#endif
+
+/* xQueueCreateSet is compiled out if configUSE_QUEUE_SETS != 1.*/
+#if( configUSE_QUEUE_SETS == 1 )
+	QueueSetHandle_t xUnconstrainedQueueSet()
+	{
+		UBaseType_t uxEventQueueLength = 2;
+		QueueSetHandle_t xSet = xQueueCreateSet(uxEventQueueLength);
+		if( xSet )
+		{
+			xSet->cTxLock = nondet_int8_t();
+			xSet->cRxLock = nondet_int8_t();
+			xSet->uxMessagesWaiting = nondet_UBaseType_t();
+			xSet->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
+			/* This is an invariant checked with a couple of asserts in the code base.
+			   If it is false from the beginning, the CBMC proofs are not able to succeed*/
+			__CPROVER_assume(xSet->uxMessagesWaiting < xSet->uxLength);
+			xSet->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
+		}
+		return xSet;
+	}
+#endif
+
+/* Create a mostly unconstrained Queue but bound the max item size.
+   This is required for performance reasons in CBMC at the moment. */
+QueueHandle_t xUnconstrainedQueueBoundedItemSize( UBaseType_t uxItemSizeBound ) {
+	UBaseType_t uxQueueLength;
+	UBaseType_t uxItemSize;
+	uint8_t ucQueueType;
+	__CPROVER_assume(uxQueueLength > 0);
+	__CPROVER_assume(uxItemSize < uxItemSizeBound);
+
+	// QueueGenericCreate method does not check for multiplication overflow
+	size_t uxQueueStorageSize;
+	__CPROVER_assume(uxQueueStorageSize < CBMC_OBJECT_MAX_SIZE);
+	__CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength);
+
+	QueueHandle_t xQueue =
+		xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType);
+	if(xQueue){
+		xQueue->cTxLock = nondet_int8_t();
+		xQueue->cRxLock = nondet_int8_t();
+		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
+		/* This is an invariant checked with a couple of asserts in the code base.
+		   If it is false from the beginning, the CBMC proofs are not able to succeed*/
+		__CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength);
+		xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
+		xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
+		#if( configUSE_QUEUE_SETS == 1)
+			xQueueAddToSet(xQueue, xUnconstrainedQueueSet());
+		#endif
+	}
+	return xQueue;
+}
+
+/* Create a mostly unconstrained Queue */
+QueueHandle_t xUnconstrainedQueue( void ) {
+	UBaseType_t uxQueueLength;
+	UBaseType_t uxItemSize;
+	uint8_t ucQueueType;
+
+	__CPROVER_assume(uxQueueLength > 0);
+
+	// QueueGenericCreate method does not check for multiplication overflow
+	size_t uxQueueStorageSize;
+	__CPROVER_assume(uxQueueStorageSize < CBMC_OBJECT_MAX_SIZE);
+	__CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength);
+
+	QueueHandle_t xQueue =
+		xQueueGenericCreate(uxQueueLength, uxItemSize, ucQueueType);
+
+	if(xQueue){
+		xQueue->cTxLock = nondet_int8_t();
+		xQueue->cRxLock = nondet_int8_t();
+		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
+		/* This is an invariant checked with a couple of asserts in the code base.
+		   If it is false from the beginning, the CBMC proofs are not able to succeed*/
+		__CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength);
+		xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
+		xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
+		#if( configUSE_QUEUE_SETS == 1)
+			xQueueAddToSet(xQueue, xUnconstrainedQueueSet());
+		#endif
+	}
+	return xQueue;
+}
+
+/* Create a mostly unconstrained Mutex */
+QueueHandle_t xUnconstrainedMutex( void ) {
+	uint8_t ucQueueType;
+	QueueHandle_t xQueue =
+		xQueueCreateMutex(ucQueueType);
+	if(xQueue){
+		xQueue->cTxLock = nondet_int8_t();
+		xQueue->cRxLock = nondet_int8_t();
+		xQueue->uxMessagesWaiting = nondet_UBaseType_t();
+		/* This is an invariant checked with a couple of asserts in the code base.
+		   If it is false from the beginning, the CBMC proofs are not able to succeed*/
+		__CPROVER_assume(xQueue->uxMessagesWaiting < xQueue->uxLength);
+		xQueue->xTasksWaitingToReceive.uxNumberOfItems = nondet_UBaseType_t();
+		xQueue->xTasksWaitingToSend.uxNumberOfItems = nondet_UBaseType_t();
+		#if( configUSE_QUEUE_SETS == 1)
+			xQueueAddToSet(xQueue, xUnconstrainedQueueSet());
+		#endif
+	}
+	return xQueue;
+}

FreeRTOS/Test/CBMC/include/tasksStubs.h

@@ -0,0 +1,10 @@
+#ifndef INC_TASK_STUBS_H
+#define INC_TASK_STUBS_H
+
+#include "FreeRTOS.h"
+#include "task.h"
+
+BaseType_t xState;
+void vInitTaskCheckForTimeOut(BaseType_t maxCounter, BaseType_t maxCounter_limit);
+
+#endif /* INC_TASK_STUBS_H */