Use vSocketCloseNextTime instead of FreeRTOS_closesocket

[bernd-edlinger]

This avoids problems with calling FreeRTOS_closesocket
from the IP task.

This is an alternative to #229

---

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[bernd-edlinger]

@htibosch
Actually this does not address the select anomaly in !HANG_PROTECTION build,
I will create a separate PR for this.

[htibosch]

For the readers: FreeRTOS_closesocket() writes to a queue which is read by the IP-task. This writing can fail in case the queue is full. This means that the IP-task better not uses mentioned function.
This PR introduces vSocketCloseNextTime() which can be used by the IP-task only.
@bernd-edlinger : thank you for this PR, I prefer it above the earlier drafts for closesocket().

[bernd-edlinger]

Hmm, the CBMC Proofs fail over the configASSERT( xIsCallingFromIPTask() != pdFALSE ); which I added in the
last update.
I'll try to fix that.

[bernd-edlinger]

Hmm, that is a bit unfair,
the trace for the failing proofs are show that xIsCallingFromIPTask returns first true, and then false:

State 255 file test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c function harness line 49 thread 0
----------------------------------------------------
  socketSize=400u (00000000 00000000 00000001 10010000)

Assumption:
  file TCPHandleState_harness.c line 57 function harness
  (unsigned int)byte_extract_little_endian(pxSocket->u, 0, IPTCPSocket_t).xTCPWindow.ucOptionLength == (sizeof(uint32_t) /*4u*/  * 16u) / sizeof(uint32_t) /*4u*/ 

Assumption:
  file TCPHandleState_harness.c line 59 function harness
  tmp_if_expr

Assumption:
  file TCPHandleState_harness.c line 61 function harness
  (unsigned int)byte_extract_little_endian(pxSocket->u, 0, IPTCPSocket_t).usInitMSS == sizeof(uint16_t) /*2u*/ 

State 281 file FreeRTOS_IP.c function xIsCallingFromIPTask line 638 thread 0
----------------------------------------------------
  xReturn=-1 (11111111 11111111 11111111 11111111)

State 288 file FreeRTOS_IP.c function xIsCallingFromIPTask line 642 thread 0
----------------------------------------------------
  xReturn=1 (00000000 00000000 00000000 00000001)

[...]

State 967 file FreeRTOS_IP.c function xIsCallingFromIPTask line 638 thread 0
----------------------------------------------------
  xReturn=-1 (11111111 11111111 11111111 11111111)

State 974 file FreeRTOS_IP.c function xIsCallingFromIPTask line 646 thread 0
----------------------------------------------------
  xReturn=0 (00000000 00000000 00000000 00000000)

Violated property:
  file FreeRTOS_TCP_IP.c function vTCPStateChange line 1864 thread 0
  Assertion Error
  return_value_xIsCallingFromIPTask != (BaseType_t)0

[AniruddhaKanhere]

Hello @bernd-edlinger,

the CBMC proofs try to cover every possible scenario. They return an indeterministic value (meaning anything can be returned - I hesitate to say randomly because that would not be correct but can make the nature of the return value clearer).
Since the function xIsCallingFromIPTask is not defined in the proof, the signature defaults to something like this:

BaseType_t xIsCallingFromIPTask(void)
{
    BaseType_t xReturn;

    /* Return a non-deterministic value. */
    return xReturn;
}

I have been busy with other tasks at hand. I'll try and fix the proofs which are broken in this PR.

Regards,
Aniruddha

[bernd-edlinger]

Thanks @AniruddhaKanhere for clarifying.

Now I understand a lot better.
Likely the problem is xTaskGetCurrentTaskHandle() needs to be added to the test.

[bernd-edlinger]

CBMC proofs do now pass.
@AniruddhaKanhere I've added this to the failing tests:

/* Abstraction of xTaskGetCurrentTaskHandle */
TaskHandle_t xTaskGetCurrentTaskHandle( void )
{
    static int xIsInit = 0;
    static TaskHandle_t pxCurrentTCB;
    TaskHandle_t xRandomTaskHandle; /* not initialized on purpose */

    if( xIsInit == 0 )
    {
        pxCurrentTCB = xRandomTaskHandle;
        xIsInit = 1;
    }

    return pxCurrentTCB;
}

do you agree with my approach?

[gkwicker]

One question, see comments.

[htibosch]

Although merged, this PR was still on my list to do a real-life test.

I just took one example: a client wants to connect but it sends the wrong TCP flags (e.g. SYN + FIN).
The server will complain about the flags and call vTCPStateChange():

    /* In case pxSocket is not yet owned by the application, a closure
     * of the socket will be scheduled for the next cycle. */
    vTCPStateChange( pxSocket, eCLOSE_WAIT );

vTCPStateChange() sees that the socket is not yet owned by the application and so it calls vSocketCloseNextTime(). A few µs later, the socket is closed and deleted.

Bernd, thank you for this PR, and also for your patience and flexibility.