path: root/FreeRTOS-Plus/Test/CBMC/stubs/freertos_api.c

/* Standard includes. */
#include <stdint.h>
#include <stdio.h>

/* FreeRTOS includes. */
#include "FreeRTOS.h"
#include "task.h"
#include "queue.h"
#include "semphr.h"

/* FreeRTOS+TCP includes. */
#include "FreeRTOS_UDP_IP.h"
#include "FreeRTOS_IP.h"
#include "FreeRTOS_Sockets.h"
#include "FreeRTOS_IP_Private.h"
#include "FreeRTOS_DNS.h"
#include "NetworkBufferManagement.h"

#include "cbmc.h"

/****************************************************************
 * This is a collection of abstractions of methods in the FreeRTOS TCP
 * API.  The abstractions simply perform minimal validation of
 * function arguments, and return unconstrained values of the
 * appropriate type.
 ****************************************************************/

/****************************************************************
 * Abstract FreeRTOS_socket.
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/socket.html
 *
 * We stub out this function to do nothing but allocate space for a
 * socket containing unconstrained data or return an error.
 ****************************************************************/

Socket_t FreeRTOS_socket( BaseType_t xDomain,
                          BaseType_t xType,
                          BaseType_t xProtocol )
{
    return nondet_bool() ?
           FREERTOS_INVALID_SOCKET : malloc( sizeof( Socket_t ) );
}

/****************************************************************
 * Abstract FreeRTOS_setsockopt.
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/setsockopt.html
 ****************************************************************/

BaseType_t FreeRTOS_setsockopt( Socket_t xSocket,
                                int32_t lLevel,
                                int32_t lOptionName,
                                const void * pvOptionValue,
                                size_t uxOptionLength )
{
    __CPROVER_assert( xSocket != NULL,
                      "FreeRTOS precondition: xSocket != NULL" );
    __CPROVER_assert( pvOptionValue != NULL,
                      "FreeRTOS precondition: pvOptionValue != NULL" );
    return nondet_BaseType();
}

/****************************************************************
 * Abstract FreeRTOS_closesocket.
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/close.html
 ****************************************************************/

BaseType_t FreeRTOS_closesocket( Socket_t xSocket )
{
    __CPROVER_assert( xSocket != NULL,
                      "FreeRTOS precondition: xSocket != NULL" );
    return nondet_BaseType();
}

/****************************************************************
 * Abstract FreeRTOS_bind.
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/bind.html
 ****************************************************************/

BaseType_t FreeRTOS_bind( Socket_t xSocket,
                          struct freertos_sockaddr * pxAddress,
                          socklen_t xAddressLength )
{
    __CPROVER_assert( xSocket != NULL,
                      "FreeRTOS precondition: xSocket != NULL" );
    __CPROVER_assert( pxAddress != NULL,
                      "FreeRTOS precondition: pxAddress != NULL" );
    return nondet_BaseType();
}

/****************************************************************
 * Abstract FreeRTOS_inet_addr.
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/inet_addr.html
 ****************************************************************/

uint32_t FreeRTOS_inet_addr( const char * pcIPAddress )
{
    __CPROVER_assert( pcIPAddress != NULL,
                      "FreeRTOS precondition: pcIPAddress != NULL" );
    return nondet_uint32();
}

/****************************************************************
 * Abstract FreeRTOS_recvfrom.
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/recvfrom.html
 *
 * We stub out this function to do nothing but allocate a buffer of
 * unconstrained size containing unconstrained data and return the
 * size (or return the size 0 if the allocation fails).
 ****************************************************************/

int32_t FreeRTOS_recvfrom( Socket_t xSocket,
                           void * pvBuffer,
                           size_t uxBufferLength,
                           BaseType_t xFlags,
                           struct freertos_sockaddr * pxSourceAddress,
                           socklen_t * pxSourceAddressLength )

{
    /****************************************************************
     * "If the zero copy calling semantics are used (the ulFlasg
     * parameter does not have the FREERTOS_ZERO_COPY bit set) then
     * pvBuffer does not point to a buffer and xBufferLength is not
     * used."  This is from the documentation.
     ****************************************************************/
    __CPROVER_assert( xFlags & FREERTOS_ZERO_COPY, "I can only do ZERO_COPY" );

    __CPROVER_assert( pvBuffer != NULL,
                      "FreeRTOS precondition: pvBuffer != NULL" );

    /****************************************************************
     * TODO: We need to check this out.
     *
     * The code calls recvfrom with these parameters NULL, it is not
     * clear from the documentation that this is allowed.
     ****************************************************************/
    #if 0
        __CPROVER_assert( pxSourceAddress != NULL,
                          "FreeRTOS precondition: pxSourceAddress != NULL" );
        __CPROVER_assert( pxSourceAddressLength != NULL,
                          "FreeRTOS precondition: pxSourceAddress != NULL" );
    #endif

    size_t payload_size;
    __CPROVER_assume( payload_size + sizeof( UDPPacket_t )
		      < CBMC_MAX_OBJECT_SIZE );

    /****************************************************************
     * TODO: We need to make this lower bound explicit in the Makefile.json
     *
     * DNSMessage_t is a typedef in FreeRTOS_DNS.c
     * sizeof(DNSMessage_t) = 6 * sizeof(uint16_t)
     ****************************************************************/
    __CPROVER_assume( payload_size >= 6 * sizeof( uint16_t ) );

    #ifdef CBMC_FREERTOS_RECVFROM_BUFFER_BOUND
        __CPROVER_assume( payload_size <= CBMC_FREERTOS_RECVFROM_BUFFER_BOUND );
    #endif

    uint32_t buffer_size = payload_size + sizeof( UDPPacket_t );
    uint8_t *buffer = safeMalloc( buffer_size );
	
    if ( buffer == NULL ) {
      buffer_size = 0;
    }
    else
    {
      buffer = buffer + sizeof( UDPPacket_t );
      buffer_size = buffer_size - sizeof( UDPPacket_t );
    }
    
    *( ( uint8_t ** ) pvBuffer ) = buffer;
    return buffer_size;
}

/****************************************************************
 * Abstract FreeRTOS_recvfrom.
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/sendto.html
 ****************************************************************/

int32_t FreeRTOS_sendto( Socket_t xSocket,
                         const void * pvBuffer,
                         size_t uxTotalDataLength,
                         BaseType_t xFlags,
                         const struct freertos_sockaddr * pxDestinationAddress,
                         socklen_t xDestinationAddressLength )
{
    __CPROVER_assert( xSocket != NULL,
                      "FreeRTOS precondition: xSocket != NULL" );
    __CPROVER_assert( pvBuffer != NULL,
                      "FreeRTOS precondition: pvBuffer != NULL" );
    __CPROVER_assert( pxDestinationAddress != NULL,
                      "FreeRTOS precondition: pxDestinationAddress != NULL" );
    return nondet_int32();
}

/****************************************************************
 * Abstract FreeRTOS_GetUDPPayloadBuffer
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_UDP/API/FreeRTOS_GetUDPPayloadBuffer.html
 *
 * We stub out this function to do nothing but allocate a buffer of
 * unconstrained size containing unconstrained data and return a
 * pointer to the buffer (or NULL).
 ****************************************************************/

void * FreeRTOS_GetUDPPayloadBuffer( size_t xRequestedSizeBytes,
                                     TickType_t xBlockTimeTicks )
{
    size_t size;

    __CPROVER_assume( size < CBMC_MAX_OBJECT_SIZE );
    __CPROVER_assume( size >= sizeof( UDPPacket_t ) );

    uint8_t *buffer = safeMalloc( size );
    return buffer == NULL ? buffer : buffer + sizeof( UDPPacket_t );
}

/****************************************************************
 * Abstract FreeRTOS_GetUDPPayloadBuffer
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/FreeRTOS_ReleaseUDPPayloadBuffer.html
 ****************************************************************/

void FreeRTOS_ReleaseUDPPayloadBuffer( void * pvBuffer )
{
    __CPROVER_assert( pvBuffer != NULL,
                      "FreeRTOS precondition: pvBuffer != NULL" );
    __CPROVER_assert( __CPROVER_POINTER_OFFSET( pvBuffer )
		      == sizeof( UDPPacket_t ),
                      "FreeRTOS precondition: pvBuffer offset" );

    free( pvBuffer - sizeof( UDPPacket_t ) );
}

/****************************************************************
 * Abstract pxGetNetworkBufferWithDescriptor.
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/pxGetNetworkBufferWithDescriptor.html
 *
 * The real allocator take buffers off a list.
 ****************************************************************/

uint32_t GetNetworkBuffer_failure_count;

NetworkBufferDescriptor_t * pxGetNetworkBufferWithDescriptor( size_t xRequestedSizeBytes,
                                                              TickType_t xBlockTimeTicks )
{
    __CPROVER_assert(
        xRequestedSizeBytes + ipBUFFER_PADDING < CBMC_MAX_OBJECT_SIZE,
        "pxGetNetworkBufferWithDescriptor: request too big" );

    /*
      * The semantics of this function is to wait until a buffer with
      * at least the requested number of bytes becomes available.  If a
      * timeout occurs before the buffer is available, then return a
      * NULL pointer.
      */

    NetworkBufferDescriptor_t * desc = safeMalloc( sizeof( *desc ) );

    #ifdef CBMC_GETNETWORKBUFFER_FAILURE_BOUND
        /*
          * This interprets the failure bound as being one greater than the
          * actual number of times GetNetworkBuffer should be allowed to
          * fail.
          *
          * This makes it possible to use the same bound for loop unrolling
          * which must be one greater than the actual number of times the
          * loop should be unwound.
          *
          * NOTE: Using this bound with --nondet-static requires setting
          * (or assuming) GetNetworkBuffer_failure_count to a value (like 0)
          * in the proof harness that won't induce an integer overflow.
          */
        GetNetworkBuffer_failure_count++;
        __CPROVER_assume(
	    IMPLIES(
	        GetNetworkBuffer_failure_count >= CBMC_GETNETWORKBUFFER_FAILURE_BOUND,
		desc != NULL ) );
    #endif

    if( desc != NULL )
    {
        /*
          * We may want to experiment with allocating space other than
          * (more than) the exact amount of space requested.
          */

        size_t size = xRequestedSizeBytes;
        __CPROVER_assume( size < CBMC_MAX_OBJECT_SIZE );

        desc->pucEthernetBuffer = safeMalloc( size );
        desc->xDataLength = desc->pucEthernetBuffer == NULL ? 0 : size;

        #ifdef CBMC_REQUIRE_NETWORKBUFFER_ETHERNETBUFFER_NONNULL
            /* This may be implied by the semantics of the function. */
            __CPROVER_assume( desc->pucEthernetBuffer != NULL );
        #endif

	/* Allow method to fail again next time */
	GetNetworkBuffer_failure_count = 0;
    }

    return desc;
}

/****************************************************************
 * Abstract pxGetNetworkBufferWithDescriptor.
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/vReleaseNetworkBufferAndDescriptor.html
 ****************************************************************/

void vReleaseNetworkBufferAndDescriptor( NetworkBufferDescriptor_t * const pxNetworkBuffer )
{
    __CPROVER_assert( pxNetworkBuffer != NULL,
                      "Precondition: pxNetworkBuffer != NULL" );

    if( pxNetworkBuffer->pucEthernetBuffer != NULL )
    {
        free( pxNetworkBuffer->pucEthernetBuffer );
    }

    free( pxNetworkBuffer );
}

/****************************************************************
 * Abstract FreeRTOS_GetAddressConfiguration
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/FreeRTOS_GetAddressConfiguration.html
 ****************************************************************/

void FreeRTOS_GetAddressConfiguration( uint32_t * pulIPAddress,
                                       uint32_t * pulNetMask,
                                       uint32_t * pulGatewayAddress,
                                       uint32_t * pulDNSServerAddress )
{
    if( pulIPAddress != NULL )
    {
        *pulIPAddress = nondet_unint32();
    }

    if( pulNetMask != NULL )
    {
        *pulNetMask = nondet_unint32();
    }

    if( pulGatewayAddress != NULL )
    {
        *pulGatewayAddress = nondet_unint32();
    }

    if( pulDNSServerAddress != NULL )
    {
        *pulDNSServerAddress = nondet_unint32();
    }
}

/****************************************************************/

/****************************************************************
 * This is a collection of methods that are defined by the user
 * application but are invoked by the FreeRTOS API.
 ****************************************************************/

/****************************************************************
 * Abstract FreeRTOS_GetAddressConfiguration
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/API/vApplicationIPNetworkEventHook.html
 ****************************************************************/

void vApplicationIPNetworkEventHook( eIPCallbackEvent_t eNetworkEvent )
{
}

/****************************************************************
 * Abstract pcApplicationHostnameHook
 * https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/TCP_IP_Configuration.html
 ****************************************************************/

const char * pcApplicationHostnameHook( void )
{
    return "hostname";
}

/****************************************************************/