Remove or rework assumptions in queue proofs (#603)

This commit is paired with another to queue.c in the kernel. To accomodate changes in newer versions of CBMC, the --pointer-overflow-check is removed.
2025-12-15 16:15:08 -05:00 · 2021-06-04 15:42:14 -04:00 · 2021-06-04 15:42:14 -04:00 · b6624fa44d
commit b6624fa44d
parent d9ddcc0134
33 changed files with 57 additions and 124 deletions
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/Makefile.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/QueueCreateCountingSemaphore_harness.c
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphore/QueueCreateCountingSemaphore_harness.c
@ -32,13 +32,10 @@
 #include "cbmc.h"


-void harness(){
+void harness()
+{
    UBaseType_t uxMaxCount;
    UBaseType_t uxInitialCount;

-    __CPROVER_assume(uxMaxCount != 0);
-    __CPROVER_assume(uxInitialCount <= uxMaxCount);
-
    xQueueCreateCountingSemaphore( uxMaxCount, uxInitialCount );
 }
-
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/Makefile.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/QueueCreateCountingSemaphoreStatic_harness.c
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateCountingSemaphoreStatic/QueueCreateCountingSemaphoreStatic_harness.c
@ -31,15 +31,12 @@
 #include "cbmc.h"


-void harness(){
+void harness()
+{
    UBaseType_t uxMaxCount;
    UBaseType_t uxInitialCount;
+    StaticQueue_t * pxStaticQueue = ( StaticQueue_t * ) pvPortMalloc( sizeof( StaticQueue_t ) );

-    //xStaticQueue is required to be not null
-    StaticQueue_t xStaticQueue;

-    //Checked invariant
-    __CPROVER_assume(uxMaxCount != 0);
-    __CPROVER_assume(uxInitialCount <= uxMaxCount);
-    xQueueCreateCountingSemaphoreStatic( uxMaxCount, uxInitialCount, &xStaticQueue );
+    xQueueCreateCountingSemaphoreStatic( uxMaxCount, uxInitialCount, pxStaticQueue );
 }
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutex/Makefile.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/Makefile.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/QueueCreateMutexStatic_harness.c
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueCreateMutexStatic/QueueCreateMutexStatic_harness.c
@ -31,11 +31,10 @@
 #include "cbmc.h"


-void harness(){
+void harness()
+{
    uint8_t ucQueueType;
+    StaticQueue_t * pxStaticQueue = ( StaticQueue_t * ) pvPortMalloc( sizeof( StaticQueue_t ) );

-    //The mutex storage is assumed to be not null.
-    StaticQueue_t xStaticQueue;
-
-    xQueueCreateMutexStatic( ucQueueType, &xStaticQueue );
+    xQueueCreateMutexStatic( ucQueueType, pxStaticQueue );
 }
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/Configurations.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/Configurations.json
@ -38,7 +38,6 @@
  [
      "--unwind 1",
      "--signed-overflow-check",
-      "--pointer-overflow-check",
      "--unsigned-overflow-check"

  ],
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/QueueGenericCreate_harness.c
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreate/QueueGenericCreate_harness.c
@ -32,19 +32,14 @@
 #include "cbmc.h"


-void harness(){
-	UBaseType_t uxQueueLength;
-	UBaseType_t uxItemSize;
-	uint8_t ucQueueType;
+void harness()
+{
+    UBaseType_t uxQueueLength;
+    UBaseType_t uxItemSize;
+    uint8_t ucQueueType;

-	size_t uxQueueStorageSize;
-	__CPROVER_assume(uxQueueStorageSize < (UINT32_MAX>>8));
+    /* Allow CBMC to run in a reasonable amount of time. */
+    __CPROVER_assume( ( uxQueueLength == QUEUE_LENGTH ) || ( uxItemSize == QUEUE_ITEM_SIZE ) );

-	// QueueGenericCreate does not check for multiplication overflow
-	__CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength);
-
-	// QueueGenericCreate asserts positive queue length
-	__CPROVER_assume(uxQueueLength > ( UBaseType_t ) 0);
-
-	xQueueGenericCreate( uxQueueLength, uxItemSize, ucQueueType );
+    xQueueGenericCreate( uxQueueLength, uxItemSize, ucQueueType );
 }
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/Configurations.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/Configurations.json
@ -37,7 +37,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
@ -48,8 +47,8 @@
  "DEF": [
    {
      "QeueuGenericCreateStatic_DynamicAllocation": [
-	"CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}",
-	"CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}",
+        "CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}",
+        "CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}",
        "configUSE_TRACE_FACILITY=0",
        "configGENERATE_RUN_TIME_STATS=0",
        "configSUPPORT_STATIC_ALLOCATION=1",
@ -58,8 +57,8 @@
    },
    {
      "QeueuGenericCreateStatic_NoDynamicAllocation": [
-	"CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}",
-	"CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}",
+        "CBMC_OBJECT_BITS={CBMC_OBJECT_BITS}",
+        "CBMC_OBJECT_MAX_SIZE={CBMC_OBJECT_MAX_SIZE}",
        "configUSE_TRACE_FACILITY=0",
        "configGENERATE_RUN_TIME_STATS=0",
        "configSUPPORT_STATIC_ALLOCATION=1",
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/QueueGenericCreateStatic_harness.c
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericCreateStatic/QueueGenericCreateStatic_harness.c
@ -31,32 +31,22 @@
 #include "queue_datastructure.h"
 #include "cbmc.h"

-void harness(){
+void harness()
+{
    UBaseType_t uxQueueLength;
    UBaseType_t uxItemSize;
-
-    size_t uxQueueStorageSize;
-    uint8_t *pucQueueStorage = (uint8_t *) pvPortMalloc(uxQueueStorageSize);
-
-    StaticQueue_t *pxStaticQueue =
-      (StaticQueue_t *) pvPortMalloc(sizeof(StaticQueue_t));
-
    uint8_t ucQueueType;
+    size_t storageSize;

-    __CPROVER_assume(uxQueueStorageSize < (UINT32_MAX>>8));
+    /* Allow CBMC to run in a reasonable amount of time. */
+    __CPROVER_assume( ( uxQueueLength == QUEUE_LENGTH ) || ( uxItemSize == QUEUE_ITEM_SIZE ) );

-    // QueueGenericReset does not check for multiplication overflow
-    __CPROVER_assume(uxItemSize < uxQueueStorageSize/uxQueueLength);
+    /* Prevent overflow in this harness. */
+    __CPROVER_assume( ( uxQueueLength > 0 ) && ( ( storageSize / uxQueueLength ) == uxItemSize ) );

-    // QueueGenericCreateStatic asserts positive queue length
-    __CPROVER_assume(uxQueueLength > ( UBaseType_t ) 0);
+    uint8_t * pucQueueStorage = ( uint8_t * ) pvPortMalloc( storageSize );

-    // QueueGenericCreateStatic asserts the following equivalence
-    __CPROVER_assume( ( pucQueueStorage && uxItemSize ) ||
-                      ( !pucQueueStorage && !uxItemSize ) );
-
-    // QueueGenericCreateStatic asserts nonnull pointer
-    __CPROVER_assume(pxStaticQueue);
+    StaticQueue_t * pxStaticQueue = ( StaticQueue_t * ) pvPortMalloc( sizeof( StaticQueue_t ) );

    xQueueGenericCreateStatic( uxQueueLength, uxItemSize, pucQueueStorage, pxStaticQueue, ucQueueType );
 }
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/Makefile.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/QueueGenericReset_harness.c
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericReset/QueueGenericReset_harness.c
@ -34,12 +34,11 @@

 struct QueueDefinition;

-void harness() {
-	BaseType_t xNewQueue;
+void harness()
+{
+    BaseType_t xNewQueue;

-	QueueHandle_t xQueue = xUnconstrainedQueue();
-	if(xQueue != NULL)
-	{
-		xQueueGenericReset(xQueue, xNewQueue);
-	}
+    QueueHandle_t xQueue = xUnconstrainedQueue();
+
+    xQueueGenericReset( xQueue, xNewQueue );
 }
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/Configurations.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSend/Configurations.json
@ -33,7 +33,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check",
    "--unwindset xQueueGenericSend.0:{QUEUE_SEND_BOUND},prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}",
    "--nondet-static"
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/Configurations.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGenericSendFromISR/Configurations.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check",
    "--nondet-static"
  ],
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolder/Makefile.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGetMutexHolderFromISR/Makefile.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/Configurations.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveFromISR/Configurations.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check",
    "--nondet-static"
  ],
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueGiveMutexRecursive/Makefile.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueMessagesWaiting/Makefile.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueuePeek/Makefile.json
@ -33,7 +33,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check",
    "--unwindset prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND},xQueuePeek.0:{QUEUE_PEEK_BOUND}",
    "--nondet-static"
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceive/Makefile.json
@ -33,7 +33,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check",
    "--unwindset xQueueReceive.0:{QUEUE_RECEIVE_BOUND},prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}",
    "--nondet-static"
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueReceiveFromISR/Makefile.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSemaphoreTake/Makefile.json
@ -35,7 +35,6 @@
  "CBMCFLAGS": [
    "--unwind 2",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check",
    "--nondet-static",
    "--unwindset prvUnlockQueue.0:{QUEUE_BOUND},prvUnlockQueue.1:{QUEUE_BOUND},xQueueSemaphoreTake.0:3"
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueSpacesAvailable/Makefile.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/Makefile.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/QueueTakeMutexRecursive/Makefile.json
@ -38,7 +38,6 @@
    "--unwind {QueueSemaphoreTake_BOUND}",
    "--unwindset prvUnlockQueue.0:{PRV_UNLOCK_UNWINDING_BOUND},prvUnlockQueue.1:{PRV_UNLOCK_UNWINDING_BOUND}",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/Configurations.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvCopyDataToQueue/Configurations.json
@ -31,7 +31,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check"
  ],
  "OBJS": [
--- a/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/Configurations.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvNotifyQueueSetContainer/Configurations.json
@ -32,7 +32,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check",
    "--unwindset prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}"
  ],
--- a/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/Configurations.json
+++ b/FreeRTOS/Test/CBMC/proofs/Queue/prvUnlockQueue/Configurations.json
@ -32,7 +32,6 @@
  "CBMCFLAGS": [
    "--unwind 1",
    "--signed-overflow-check",
-    "--pointer-overflow-check",
    "--unsigned-overflow-check",
    "--unwindset prvUnlockQueue.0:{LOCK_BOUND},prvUnlockQueue.1:{LOCK_BOUND}"
  ],