/* Standard includes. */ #include #include /* FreeRTOS includes. */ #include "FreeRTOS.h" #include "task.h" #include "queue.h" #include "semphr.h" /* FreeRTOS+TCP includes. */ #include "FreeRTOS_IP.h" #include "FreeRTOS_Sockets.h" #include "FreeRTOS_IP_Private.h" #include "FreeRTOS_UDP_IP.h" #include "FreeRTOS_TCP_IP.h" #include "FreeRTOS_DHCP.h" #include "NetworkInterface.h" #include "NetworkBufferManagement.h" #include "FreeRTOS_ARP.h" #include "FreeRTOS_TCP_WIN.h" #include "cbmc.h" BaseType_t prvSingleStepTCPHeaderOptions( const unsigned char ** const ppucPtr, const unsigned char ** const ppucLast, FreeRTOS_Socket_t ** const ppxSocket, TCPWindow_t ** const ppxTCPWindow); // Given unconstrained values in harness size_t buffer_size; uint8_t *EthernetBuffer; void prvSkipPastRemainingOptions( const unsigned char ** const ppucPtr, FreeRTOS_Socket_t ** const ppxSocket, unsigned char * const pucLen ) { // Preconditions // pucPtr is a valid pointer __CPROVER_assert(EthernetBuffer <= OBJ(ppucPtr) && OBJ(ppucPtr) < EthernetBuffer + buffer_size, "pucPtr is a valid pointer"); // pucPtr + 8 is a valid pointer __CPROVER_assert(EthernetBuffer <= OBJ(ppucPtr) + 8 && OBJ(ppucPtr) + 8 <= EthernetBuffer + buffer_size, "pucPtr+8 is a valid pointer"); // len >= 8 __CPROVER_assert(OBJ(pucLen) >= 8, "len >= 8"); // Record initial values SAVE_OLDOBJ(ppucPtr, unsigned char *); SAVE_OLDOBJ(pucLen, unsigned char); // Model loop body OBJ(ppucPtr) += 8; OBJ(pucLen) -= 8; // Postconditions __CPROVER_assume(OBJ(ppucPtr) == OLDOBJ(ppucPtr) + 8); __CPROVER_assume(OBJ(pucLen) == OLDOBJ(pucLen) - 8); __CPROVER_assume(EthernetBuffer <= OBJ(ppucPtr) && OBJ(ppucPtr) <= EthernetBuffer + buffer_size); } // Proof of CheckOptions outer loop void harness() { // Buffer can be any buffer of size at most BUFFER_SIZE size_t offset; uint8_t buffer[BUFFER_SIZE]; buffer_size = BUFFER_SIZE - offset; EthernetBuffer = buffer + offset; // pucPtr and pucLast can be any pointers into buffer size_t pucPtr_offset; size_t pucLast_offset; unsigned char *pucPtr = EthernetBuffer + pucPtr_offset; unsigned char *pucLast = EthernetBuffer + pucLast_offset; // uxNewMSS can by any byte UBaseType_t uxNewMSS; // pxSocket can be any socket FreeRTOS_Socket_t xSocket; FreeRTOS_Socket_t *pxSocket = &xSocket; // pxTCPWindow can be any window (points into socket) TCPWindow_t *pxTCPWindow = &xSocket.u.xTCP.xTCPWindow; //////////////////////////////////////////////////////////////// // Specification and proof of CheckOptions outer loop // CBMC pointer model (obviously true) __CPROVER_assume(buffer_size < CBMC_MAX_OBJECT_SIZE); // Preconditions // pucPtr is a valid pointer __CPROVER_assume(EthernetBuffer <= pucPtr && pucPtr < EthernetBuffer + buffer_size); // pucLast is a valid pointer (or one past) __CPROVER_assume(EthernetBuffer <= pucLast && pucLast <= EthernetBuffer + buffer_size); // pucPtr is before pucLast __CPROVER_assume(pucPtr < pucLast); // Record initial values SAVE_OLDVAL(pucPtr, uint8_t *); SAVE_OLDVAL(pucLast, uint8_t *); // Loop variables passed by reference // Return value describes loop exit: break or continue BaseType_t rc = prvSingleStepTCPHeaderOptions(&pucPtr, &pucLast, &pxSocket, &pxTCPWindow); // Postconditions __CPROVER_assert(rc == pdFALSE || OLDVAL(pucPtr) < pucPtr, "pucPtr advanced"); __CPROVER_assert(pucLast == OLDVAL(pucLast), "pucLast unchanged"); __CPROVER_assert(pucPtr <= pucLast, "pucPtr <= pucLast"); }