1 /* FreeRTOS includes. */
2 #include "FreeRTOS.h"
3 #include "queue.h"
4
5 /* FreeRTOS+TCP includes. */
6 #include "FreeRTOS_IP.h"
7 #include "FreeRTOS_IP_Private.h"
8 #include "FreeRTOS_TCP_IP.h"
9 #include "FreeRTOS_Stream_Buffer.h"
10
11 /* This proof assumes FreeRTOS_socket, pxTCPSocketLookup and
12 * pxGetNetworkBufferWithDescriptor are implemented correctly.
13 *
14 * It also assumes prvSingleStepTCPHeaderOptions, prvCheckOptions, prvTCPPrepareSend,
15 * prvTCPHandleState and prvTCPReturnPacket are correct. These functions are
16 * proved to be correct separately. */
17
18 /* Implementation of safe malloc */
safeMalloc(size_t xWantedSize)19 void * safeMalloc( size_t xWantedSize )
20 {
21 if( xWantedSize == 0 )
22 {
23 return NULL;
24 }
25
26 uint8_t byte;
27
28 return byte ? malloc( xWantedSize ) : NULL;
29 }
30
31 /* Abstraction of FreeRTOS_socket */
FreeRTOS_socket(BaseType_t xDomain,BaseType_t xType,BaseType_t xProtocol)32 Socket_t FreeRTOS_socket( BaseType_t xDomain,
33 BaseType_t xType,
34 BaseType_t xProtocol )
35 {
36 return safeMalloc( sizeof( FreeRTOS_Socket_t ) );
37 }
38
39 /* Abstraction of xTaskGetCurrentTaskHandle */
xTaskGetCurrentTaskHandle(void)40 TaskHandle_t xTaskGetCurrentTaskHandle( void )
41 {
42 static int xIsInit = 0;
43 static TaskHandle_t pxCurrentTCB;
44 TaskHandle_t xRandomTaskHandle; /* not initialized on purpose */
45
46 if( xIsInit == 0 )
47 {
48 pxCurrentTCB = xRandomTaskHandle;
49 xIsInit = 1;
50 }
51
52 return pxCurrentTCB;
53 }
54
55 /* Abstraction of pxTCPSocketLookup */
pxTCPSocketLookup(uint32_t ulLocalIP,UBaseType_t uxLocalPort,uint32_t ulRemoteIP,UBaseType_t uxRemotePort)56 FreeRTOS_Socket_t * pxTCPSocketLookup( uint32_t ulLocalIP,
57 UBaseType_t uxLocalPort,
58 uint32_t ulRemoteIP,
59 UBaseType_t uxRemotePort )
60 {
61 FreeRTOS_Socket_t * xRetSocket = safeMalloc( sizeof( FreeRTOS_Socket_t ) );
62
63 if( xRetSocket )
64 {
65 xRetSocket->u.xTCP.txStream = safeMalloc( sizeof( StreamBuffer_t ) );
66 xRetSocket->u.xTCP.pxPeerSocket = safeMalloc( sizeof( StreamBuffer_t ) );
67
68 /* This bit depicts whether the socket was supposed to be reused or not. */
69 if( xRetSocket->u.xTCP.pxPeerSocket == NULL )
70 {
71 xRetSocket->u.xTCP.bits.bReuseSocket = pdTRUE_UNSIGNED;
72 }
73 else
74 {
75 xRetSocket->u.xTCP.bits.bReuseSocket = pdFALSE_UNSIGNED;
76 }
77
78 if( xIsCallingFromIPTask() == pdFALSE )
79 {
80 xRetSocket->u.xTCP.bits.bPassQueued = pdFALSE_UNSIGNED;
81 xRetSocket->u.xTCP.bits.bPassAccept = pdFALSE_UNSIGNED;
82 }
83 }
84
85 return xRetSocket;
86 }
87
88 /* Abstraction of pxGetNetworkBufferWithDescriptor */
pxGetNetworkBufferWithDescriptor(size_t xRequestedSizeBytes,TickType_t xBlockTimeTicks)89 NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
90 TickType_t xBlockTimeTicks )
91 {
92 NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
93
94 if( pxNetworkBuffer )
95 {
96 pxNetworkBuffer->pucEthernetBuffer = safeMalloc( xRequestedSizeBytes );
97 __CPROVER_assume( pxNetworkBuffer->xDataLength == ipSIZE_OF_ETH_HEADER + sizeof( int32_t ) );
98 }
99
100 return pxNetworkBuffer;
101 }
102
harness()103 void harness()
104 {
105 NetworkBufferDescriptor_t * pxNetworkBuffer = safeMalloc( sizeof( NetworkBufferDescriptor_t ) );
106
107 /* To avoid asserting on the network buffer being NULL. */
108 __CPROVER_assume( pxNetworkBuffer != NULL );
109
110 pxNetworkBuffer->pucEthernetBuffer = safeMalloc( sizeof( TCPPacket_t ) );
111
112 /* To avoid asserting on the ethernet buffer being NULL. */
113 __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
114
115 xProcessReceivedTCPPacket( pxNetworkBuffer );
116 }
117
