1 /* Standard includes. */
2 #include <stdint.h>
3 #include <stdio.h>
4 
5 /* FreeRTOS includes. */
6 #include "FreeRTOS.h"
7 #include "task.h"
8 #include "queue.h"
9 #include "list.h"
10 #include "semphr.h"
11 
12 /* FreeRTOS+TCP includes. */
13 #include "FreeRTOS_IP.h"
14 #include "FreeRTOS_ND.h"
15 #include "FreeRTOS_UDP_IP.h"
16 #include "FreeRTOS_IP_Private.h"
17 
18 /* Include the stubs for APIs. */
19 #include "memory_assignments.c"
20 #include "freertos_api.c"
21 
22 /* We do not need to calculate the actual checksum for the proof to be complete.
23  * Neither does the checksum matter for completeness. */
usGenerateChecksum(uint16_t usSum,const uint8_t * pucNextData,size_t uxByteCount)24 uint16_t usGenerateChecksum( uint16_t usSum,
25                              const uint8_t * pucNextData,
26                              size_t uxByteCount )
27 {
28     uint16_t usChecksum;
29 
30     __CPROVER_assert( pucNextData != NULL, "Next data in GenerateChecksum cannot be NULL" );
31     /* Return any random value of checksum since it does not matter for CBMC checks. */
32     return usChecksum;
33 }
34 
35 
36 /* We do not need to calculate the actual checksum for the proof to be complete.
37  * Neither does the checksum matter for completeness. */
usGenerateProtocolChecksum(const uint8_t * const pucEthernetBuffer,size_t uxBufferLength,BaseType_t xOutgoingPacket)38 uint16_t usGenerateProtocolChecksum( const uint8_t * const pucEthernetBuffer,
39                                      size_t uxBufferLength,
40                                      BaseType_t xOutgoingPacket )
41 {
42     uint16_t usProtocolChecksum;
43 
44     __CPROVER_assert( pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL while generating Protocol Checksum" );
45 
46     /* Return random value of checksum since it does not matter for CBMC checks. */
47     return usProtocolChecksum;
48 }
49 
50 /* This function has been tested separately. Therefore, we assume that the implementation is correct. */
eNDGetCacheEntry(IPv6_Address_t * pxIPAddress,MACAddress_t * const pxMACAddress,struct xNetworkEndPoint ** ppxEndPoint)51 eARPLookupResult_t eNDGetCacheEntry( IPv6_Address_t * pxIPAddress,
52                                      MACAddress_t * const pxMACAddress,
53                                      struct xNetworkEndPoint ** ppxEndPoint )
54 {
55     eARPLookupResult_t eResult;
56 
57     __CPROVER_assert( pxIPAddress != NULL, "pxIPAddress cannot be NULL" );
58     __CPROVER_assert( pxMACAddress != NULL, "pxMACAddress cannot be NULL" );
59 
60     return eResult;
61 }
62 
63 /* This function has been tested separately. Therefore, we assume that the implementation is correct. */
vNDSendNeighbourSolicitation(NetworkBufferDescriptor_t * pxNetworkBuffer,const IPv6_Address_t * pxIPAddress)64 void vNDSendNeighbourSolicitation( NetworkBufferDescriptor_t * pxNetworkBuffer,
65                                    const IPv6_Address_t * pxIPAddress )
66 {
67     __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
68     __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL." );
69     __CPROVER_assert( pxIPAddress != NULL, "pxIPAddress cannot be NULL." );
70 }
71 
NetworkInterfaceOutputFunction_Stub(struct xNetworkInterface * pxDescriptor,NetworkBufferDescriptor_t * const pxNetworkBuffer,BaseType_t xReleaseAfterSend)72 BaseType_t NetworkInterfaceOutputFunction_Stub( struct xNetworkInterface * pxDescriptor,
73                                                 NetworkBufferDescriptor_t * const pxNetworkBuffer,
74                                                 BaseType_t xReleaseAfterSend )
75 {
76     BaseType_t ret;
77 
78     __CPROVER_assert( pxDescriptor != NULL, "The network interface cannot be NULL." );
79     __CPROVER_assert( pxNetworkBuffer != NULL, "The network buffer descriptor cannot be NULL." );
80     __CPROVER_assert( pxNetworkBuffer->pucEthernetBuffer != NULL, "The Ethernet buffer cannot be NULL." );
81 
82     return ret;
83 }
84 
85 
harness()86 void harness()
87 {
88     size_t xRequestedSizeBytes;
89 
90     /* Assume that the size of packet must be greater than that of UDP-Packet and less than
91      * that of the Ethernet Frame Size. */
92     __CPROVER_assume( xRequestedSizeBytes >= sizeof( UDPPacket_IPv6_t ) && xRequestedSizeBytes <= ipTOTAL_ETHERNET_FRAME_SIZE );
93 
94     /* Second parameter is not used from CBMC's perspective. */
95     NetworkBufferDescriptor_t * const pxNetworkBuffer = pxGetNetworkBufferWithDescriptor( xRequestedSizeBytes, 0 );
96 
97     /* The buffer cannot be NULL for the function call. */
98     __CPROVER_assume( pxNetworkBuffer != NULL );
99     __CPROVER_assume( pxNetworkBuffer->pucEthernetBuffer != NULL );
100 
101     /*
102      * Add an end point to the network buffer present. Its assumed that the
103      * network interface layer correctly assigns the end point to the generated buffer.
104      */
105     pxNetworkBuffer->pxEndPoint = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
106     __CPROVER_assume( pxNetworkBuffer->pxEndPoint != NULL );
107     pxNetworkBuffer->pxEndPoint->pxNext = NULL;
108 
109     /* Add an interface */
110     pxNetworkBuffer->pxEndPoint->pxNetworkInterface = ( NetworkInterface_t * ) safeMalloc( sizeof( NetworkInterface_t ) );
111     __CPROVER_assume( pxNetworkBuffer->pxEndPoint->pxNetworkInterface != NULL );
112 
113     /* Add few endpoints to global pxNetworkEndPoints */
114     pxNetworkEndPoints = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
115     __CPROVER_assume( pxNetworkEndPoints != NULL );
116 
117     pxNetworkEndPoints->pxNetworkInterface = pxNetworkBuffer->pxEndPoint->pxNetworkInterface;
118 
119     if( nondet_bool() )
120     {
121         pxNetworkEndPoints->pxNext = ( NetworkEndPoint_t * ) safeMalloc( sizeof( NetworkEndPoint_t ) );
122         __CPROVER_assume( pxNetworkEndPoints->pxNext != NULL );
123         pxNetworkEndPoints->pxNext->pxNetworkInterface = pxNetworkBuffer->pxEndPoint->pxNetworkInterface;
124         pxNetworkEndPoints->pxNext->pxNext = NULL;
125     }
126     else
127     {
128         pxNetworkEndPoints->pxNext = NULL;
129     }
130 
131     pxNetworkBuffer->pxEndPoint->pxNetworkInterface->pfOutput = &NetworkInterfaceOutputFunction_Stub;
132 
133     vProcessGeneratedUDPPacket_IPv6( pxNetworkBuffer );
134 }
135