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 )
{
    if( nondet_bool() )
    {
        return FREERTOS_INVALID_SOCKET;
    }
    else
    {
        void * ptr = malloc( sizeof( struct xSOCKET ) );
        __CPROVER_assume( ptr != NULL );
        return ptr;
    }
}

/****************************************************************
* 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 ulFlags
    * 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_Multi( size_t uxRequestedSizeBytes,
                                           TickType_t uxBlockTimeTicks,
                                           uint8_t ucIPType )
{
    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_ReleaseUDPPayloadBuffer
* 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";
}

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


/****************************************************************
* Abstract xNetworkInterfaceOutput
* https://www.freertos.org/FreeRTOS-Plus/FreeRTOS_Plus_TCP/Embedded_Ethernet_Porting.html#xNetworkInterfaceOutput
****************************************************************/
BaseType_t xNetworkInterfaceOutput( NetworkBufferDescriptor_t * const pxNetworkBuffer,
                                    BaseType_t bReleaseAfterSend )
{
    __CPROVER_assert( pxNetworkBuffer != NULL, "The networkbuffer cannot be NULL" );

    BaseType_t xReturn;

    /* Return some random value. */
    return xReturn;
}

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