len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-07 13:45:00 -05:00
Code Issues Projects Releases Packages Wiki Activity

CBMC: Add proof for vSocketBind (#202)

Browse source 
* Add proof

* Update

* Update MakefileCommon.json

* Undo changes

* Undo changes in MakefileCommon.json

* Update Makefile.json

* Update Makefile.json

* Update Makefile.json

* Change v1

* Change v2
This commit is contained in:
Aniruddha Kanhere 2020-08-24 11:35:48 -07:00 • committed by GitHub
parent 1ae6eda77a
commit 6eba275f89
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
6 changed files with 286 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

31
FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/Makefile.json Normal file
View file

@ -0,0 +1,31 @@
{
"ENTRY": "vSocketBind",
"ALLOW_SEND_WITHOUT_BIND":"1",
"ALLOW_ETHERNET_DRIVER_FILTER":"1",
"ALLOW_TCP":"1",
"CBMCFLAGS":
[
"--unwind 1"
],
"OBJS":
[
"$(FREERTOS)/Source/list.goto",
"$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Sockets.goto",
"$(ENTRY)_harness.goto"
],
"INSTFLAGS":
[
],
"DEF":
[
"ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND={ALLOW_SEND_WITHOUT_BIND}",
"ipconfigUSE_TCP={ALLOW_TCP}",
"ipconfigETHERNET_DRIVER_FILTERS_PACKETS={ALLOW_ETHERNET_DRIVER_FILTER}"
],
"INC":
[
"$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/include",
"$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/proofs/utility"
]
}

68
FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_ETHERNET_DRIVER_FILTERS_PACKETS/vSocketBind_harness.c Normal file
View file

@ -0,0 +1,68 @@
/* Standard includes. */
#include <stdint.h>
#include <stdio.h>
/* FreeRTOS includes. */
#include "FreeRTOS.h"
#include "list.h"
/* FreeRTOS+TCP includes. */
#include "FreeRTOS_IP.h"
#include "FreeRTOS_IP_Private.h"
#include "FreeRTOS_Sockets.h"
#include "memory_assignments.c"
uint16_t prvGetPrivatePortNumber( BaseType_t xProtocol );
uint16_t prvGetPrivatePortNumber( BaseType_t xProtocol )
{
uint16_t usResult;
return usResult;
}
BaseType_t xIPIsNetworkTaskReady( void )
{
/* Return true saying that the task is ready. */
return pdTRUE;
}
/* Random number generator provided by the application. In our case, CBMC provides
* an indeterministic value. */
BaseType_t xApplicationGetRandomNumber( uint32_t *pulNumber )
{
__CPROVER_assert( pulNumber != NULL, "Argument to xApplicationGetRandomNumber cannot be NULL" );
if( nondet_bool() )
{
*pulNumber = nondet_uint32_t();
return 1;
}
else
{
*pulNumber = NULL;
return 0;
}
}
void harness()
{
FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
__CPROVER_assume( pxSocket != NULL );
__CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );
struct freertos_sockaddr * pxBindAddress = safeMalloc( sizeof( struct freertos_sockaddr ) );
/* uxAddressLength is not used in this implementation. */
size_t uxAddressLength;
BaseType_t xInternal;
/* Call to init the socket list. */
vNetworkSocketsInit();
vSocketBind( pxSocket, pxBindAddress, uxAddressLength, xInternal );
}

28
FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_SOCKET_SEND_WITHOUT_BIND/Makefile.json Normal file
View file

@ -0,0 +1,28 @@
{
"ENTRY": "vSocketBind",
"ALLOW_SEND_WITHOUT_BIND":"1",
"CBMCFLAGS":
[
"--unwind 1"
],
"OBJS":
[
"$(FREERTOS)/Source/list.goto",
"$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Sockets.goto",
"$(ENTRY)_harness.goto"
],
"INSTFLAGS":
[
],
"DEF":
[
"ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND={ALLOW_SEND_WITHOUT_BIND}",
"ipconfigUSE_TCP=1"
],
"INC":
[
"$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/include",
"$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/proofs/utility"
]
}

65
FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c Normal file
View file

@ -0,0 +1,65 @@
/* Standard includes. */
#include <stdint.h>
#include <stdio.h>
/* FreeRTOS includes. */
#include "FreeRTOS.h"
#include "list.h"
/* FreeRTOS+TCP includes. */
#include "FreeRTOS_IP.h"
#include "FreeRTOS_IP_Private.h"
#include "FreeRTOS_Sockets.h"
#include "memory_assignments.c"
uint16_t prvGetPrivatePortNumber( BaseType_t xProtocol )
{
uint16_t usResult;
return usResult;
}
BaseType_t xIPIsNetworkTaskReady( void )
{
/* Return true saying that the task is ready. */
return pdTRUE;
}
/* Random number generator provided by the application. In our case, CBMC provides
* an indeterministic value. */
BaseType_t xApplicationGetRandomNumber( uint32_t *pulNumber )
{
__CPROVER_assert( pulNumber != NULL, "Argument to xApplicationGetRandomNumber cannot be NULL" );
if( nondet_bool() )
{
*pulNumber = nondet_uint32_t();
return 1;
}
else
{
*pulNumber = NULL;
return 0;
}
}
void harness()
{
FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
__CPROVER_assume( pxSocket != NULL );
__CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );
struct freertos_sockaddr * pxBindAddress = safeMalloc( sizeof( struct freertos_sockaddr ) );
/* uxAddressLength is not used in this implementation. */
size_t uxAddressLength;
BaseType_t xInternal;
/* Call to init the socket list. */
vNetworkSocketsInit();
vSocketBind( pxSocket, pxBindAddress, uxAddressLength, xInternal );
}

28
FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/Makefile.json Normal file
View file

@ -0,0 +1,28 @@
{
"ENTRY": "vSocketBind",
"ALLOW_SEND_WITHOUT_BIND":"0",
"CBMCFLAGS":
[
"--unwind 1"
],
"OBJS":
[
"$(FREERTOS)/Source/list.goto",
"$(FREERTOS)/../FreeRTOS-Plus/Source/FreeRTOS-Plus-TCP/FreeRTOS_Sockets.goto",
"$(ENTRY)_harness.goto"
],
"INSTFLAGS":
[
],
"DEF":
[
"ipconfigALLOW_SOCKET_SEND_WITHOUT_BIND={ALLOW_SEND_WITHOUT_BIND}",
"ipconfigUSE_TCP=1"
],
"INC":
[
"$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/include",
"$(FREERTOS)/../FreeRTOS-Plus/Test/CBMC/proofs/utility"
]
}

66
FreeRTOS-Plus/Test/CBMC/proofs/Socket/vSocketBind/DONT_ALLOW_SOCKET_SEND_WITHOUT_BIND/vSocketBind_harness.c Normal file
View file

@ -0,0 +1,66 @@
/* Standard includes. */
#include <stdint.h>
#include <stdio.h>
/* FreeRTOS includes. */
#include "FreeRTOS.h"
#include "list.h"
/* FreeRTOS+TCP includes. */
#include "FreeRTOS_IP.h"
#include "FreeRTOS_IP_Private.h"
#include "FreeRTOS_Sockets.h"
#include "memory_assignments.c"
uint16_t prvGetPrivatePortNumber( BaseType_t xProtocol )
{
uint16_t usResult;
return usResult;
}
BaseType_t xIPIsNetworkTaskReady( void )
{
/* Return true saying that the task is ready. */
return pdTRUE;
}
/* Random number generator provided by the application. In our case, CBMC provides
* an indeterministic value. */
BaseType_t xApplicationGetRandomNumber( uint32_t *pulNumber )
{
__CPROVER_assert( pulNumber != NULL, "Argument to xApplicationGetRandomNumber cannot be NULL" );
if( nondet_bool() )
{
*pulNumber = nondet_uint32_t();
return 1;
}
else
{
*pulNumber = NULL;
return 0;
}
}
void harness()
{
FreeRTOS_Socket_t *pxSocket = ensure_FreeRTOS_Socket_t_is_allocated();
__CPROVER_assume( pxSocket != NULL );
__CPROVER_assume( pxSocket != FREERTOS_INVALID_SOCKET );
/* malloc instead of safeMalloc since we do not allow socket without binding. */
struct freertos_sockaddr * pxBindAddress = malloc( sizeof( struct freertos_sockaddr ) );
/* uxAddressLength is not used in this implementation. */
size_t uxAddressLength;
BaseType_t xInternal;
/* Call to init the socket list. */
vNetworkSocketsInit();
vSocketBind( pxSocket, pxBindAddress, uxAddressLength, xInternal );
}