Skip to content

Commit 676693c

Browse files
AniruddhaKanhereAniruddhaKanhere
authored
Remove extra MSS field from TCP sockets (#288)
* Remove extra MSS field * Update proof to work with new field
1 parent 1a24f31 commit 676693c

File tree

4 files changed

+31
-35
lines changed

4 files changed

+31
-35
lines changed

‎FreeRTOS_Sockets.c‎

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -470,8 +470,7 @@ Socket_t FreeRTOS_socket( BaseType_t xDomain,
470470
{
471471
/* StreamSize is expressed in number of bytes */
472472
/* Round up buffer sizes to nearest multiple of MSS */
473-
pxSocket->u.xTCP.usCurMSS = ( uint16_t ) ipconfigTCP_MSS;
474-
pxSocket->u.xTCP.usInitMSS = ( uint16_t ) ipconfigTCP_MSS;
473+
pxSocket->u.xTCP.usMSS = ( uint16_t ) ipconfigTCP_MSS;
475474
pxSocket->u.xTCP.uxRxStreamSize = ( size_t ) ipconfigTCP_RX_BUFFER_LENGTH;
476475
pxSocket->u.xTCP.uxTxStreamSize = ( size_t ) FreeRTOS_round_up( ipconfigTCP_TX_BUFFER_LENGTH, ipconfigTCP_MSS );
477476
/* Use half of the buffer size of the TCP windows */
@@ -1697,7 +1696,7 @@ void * vSocketClose( FreeRTOS_Socket_t * pxSocket )
16971696
if( lOptionName == FREERTOS_SO_SNDBUF )
16981697
{
16991698
/* Round up to nearest MSS size */
1700-
ulNewValue = FreeRTOS_round_up( ulNewValue, ( uint32_t ) pxSocket->u.xTCP.usInitMSS );
1699+
ulNewValue = FreeRTOS_round_up( ulNewValue, ( uint32_t ) pxSocket->u.xTCP.usMSS );
17011700
pxSocket->u.xTCP.uxTxStreamSize = ulNewValue;
17021701
}
17031702
else
@@ -1988,8 +1987,8 @@ BaseType_t FreeRTOS_setsockopt( Socket_t xSocket,
19881987
* adapt the window size parameters */
19891988
if( pxSocket->u.xTCP.xTCPWindow.u.bits.bHasInit != pdFALSE_UNSIGNED )
19901989
{
1991-
pxSocket->u.xTCP.xTCPWindow.xSize.ulRxWindowLength = pxSocket->u.xTCP.uxRxWinSize * pxSocket->u.xTCP.usInitMSS;
1992-
pxSocket->u.xTCP.xTCPWindow.xSize.ulTxWindowLength = pxSocket->u.xTCP.uxTxWinSize * pxSocket->u.xTCP.usInitMSS;
1990+
pxSocket->u.xTCP.xTCPWindow.xSize.ulRxWindowLength = pxSocket->u.xTCP.uxRxWinSize * pxSocket->u.xTCP.usMSS;
1991+
pxSocket->u.xTCP.xTCPWindow.xSize.ulTxWindowLength = pxSocket->u.xTCP.uxTxWinSize * pxSocket->u.xTCP.usMSS;
19931992
}
19941993
}
19951994

@@ -4319,10 +4318,10 @@ void vSocketWakeUpUser( FreeRTOS_Socket_t * pxSocket )
43194318
}
43204319
else
43214320
{
4322-
/* usCurMSS is declared as uint16_t to save space. FreeRTOS_mss()
4321+
/* usMSS is declared as uint16_t to save space. FreeRTOS_mss()
43234322
* will often be used in signed native-size expressions cast it to
43244323
* BaseType_t. */
4325-
xReturn = ( BaseType_t ) ( pxSocket->u.xTCP.usCurMSS );
4324+
xReturn = ( BaseType_t ) ( pxSocket->u.xTCP.usMSS );
43264325
}
43274326

43284327
return xReturn;

‎FreeRTOS_TCP_IP.c‎

Lines changed: 23 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -878,9 +878,9 @@
878878
/* If possible, advertise an RX window size of at least 1 MSS, otherwise
879879
* the peer might start 'zero window probing', i.e. sending small packets
880880
* (1, 2, 4, 8... bytes). */
881-
if( ( ulSpace < pxSocket->u.xTCP.usCurMSS ) && ( ulFrontSpace >= pxSocket->u.xTCP.usCurMSS ) )
881+
if( ( ulSpace < pxSocket->u.xTCP.usMSS ) && ( ulFrontSpace >= pxSocket->u.xTCP.usMSS ) )
882882
{
883-
ulSpace = pxSocket->u.xTCP.usCurMSS;
883+
ulSpace = pxSocket->u.xTCP.usMSS;
884884
}
885885

886886
/* Avoid overflow of the 16-bit win field. */
@@ -1085,7 +1085,7 @@
10851085
ipconfigTCP_MSS * pxSocket->u.xTCP.uxTxWinSize,
10861086
pxSocket->u.xTCP.xTCPWindow.rx.ulCurrentSequenceNumber,
10871087
pxSocket->u.xTCP.xTCPWindow.ulOurSequenceNumber,
1088-
( uint32_t ) pxSocket->u.xTCP.usInitMSS );
1088+
( uint32_t ) pxSocket->u.xTCP.usMSS );
10891089
}
10901090
/*-----------------------------------------------------------*/
10911091

@@ -1225,7 +1225,7 @@
12251225
/* Only set the SYN flag. */
12261226
pxTCPPacket->xTCPHeader.ucTCPFlags = tcpTCP_FLAG_SYN;
12271227

1228-
/* Set the values of usInitMSS / usCurMSS for this socket. */
1228+
/* Set the value of usMSS for this socket. */
12291229
prvSocketSetMSS( pxSocket );
12301230

12311231
/* The initial sequence numbers at our side are known. Later
@@ -1429,7 +1429,7 @@
14291429
* endian number. */
14301430
uxNewMSS = usChar2u16( &( pucPtr[ 2 ] ) );
14311431

1432-
if( pxSocket->u.xTCP.usInitMSS != uxNewMSS )
1432+
if( pxSocket->u.xTCP.usMSS != uxNewMSS )
14331433
{
14341434
/* Perform a basic check on the the new MSS. */
14351435
if( uxNewMSS == 0U )
@@ -1441,31 +1441,30 @@
14411441
}
14421442
else
14431443
{
1444-
FreeRTOS_debug_printf( ( "MSS change %u -> %lu\n", pxSocket->u.xTCP.usInitMSS, uxNewMSS ) );
1444+
FreeRTOS_debug_printf( ( "MSS change %u -> %lu\n", pxSocket->u.xTCP.usMSS, uxNewMSS ) );
14451445
}
14461446
}
14471447

14481448
/* If a 'return' condition has not been found. */
14491449
if( xReturn == pdFALSE )
14501450
{
1451-
if( pxSocket->u.xTCP.usInitMSS > uxNewMSS )
1451+
if( pxSocket->u.xTCP.usMSS > uxNewMSS )
14521452
{
14531453
/* our MSS was bigger than the MSS of the other party: adapt it. */
14541454
pxSocket->u.xTCP.bits.bMssChange = pdTRUE_UNSIGNED;
14551455

1456-
if( pxSocket->u.xTCP.usCurMSS > uxNewMSS )
1456+
if( pxSocket->u.xTCP.usMSS > uxNewMSS )
14571457
{
14581458
/* The peer advertises a smaller MSS than this socket was
14591459
* using. Use that as well. */
1460-
FreeRTOS_debug_printf( ( "Change mss %d => %lu\n", pxSocket->u.xTCP.usCurMSS, uxNewMSS ) );
1461-
pxSocket->u.xTCP.usCurMSS = ( uint16_t ) uxNewMSS;
1460+
FreeRTOS_debug_printf( ( "Change mss %d => %lu\n", pxSocket->u.xTCP.usMSS, uxNewMSS ) );
1461+
pxSocket->u.xTCP.usMSS = ( uint16_t ) uxNewMSS;
14621462
}
14631463

14641464
pxTCPWindow->xSize.ulRxWindowLength = ( ( uint32_t ) uxNewMSS ) * ( pxTCPWindow->xSize.ulRxWindowLength / ( ( uint32_t ) uxNewMSS ) );
14651465
pxTCPWindow->usMSSInit = ( uint16_t ) uxNewMSS;
14661466
pxTCPWindow->usMSS = ( uint16_t ) uxNewMSS;
1467-
pxSocket->u.xTCP.usInitMSS = ( uint16_t ) uxNewMSS;
1468-
pxSocket->u.xTCP.usCurMSS = ( uint16_t ) uxNewMSS;
1467+
pxSocket->u.xTCP.usMSS = ( uint16_t ) uxNewMSS;
14691468
}
14701469

14711470
uxIndex = tcpTCP_OPT_MSS_LEN;
@@ -1595,7 +1594,7 @@
15951594

15961595

15971596
/* 'xTCP.uxRxWinSize' is the size of the reception window in units of MSS. */
1598-
uxWinSize = pxSocket->u.xTCP.uxRxWinSize * ( size_t ) pxSocket->u.xTCP.usInitMSS;
1597+
uxWinSize = pxSocket->u.xTCP.uxRxWinSize * ( size_t ) pxSocket->u.xTCP.usMSS;
15991598
ucFactor = 0U;
16001599

16011600
while( uxWinSize > 0xffffUL )
@@ -1607,7 +1606,7 @@
16071606

16081607
FreeRTOS_debug_printf( ( "prvWinScaleFactor: uxRxWinSize %u MSS %u Factor %u\n",
16091608
( unsigned ) pxSocket->u.xTCP.uxRxWinSize,
1610-
( unsigned ) pxSocket->u.xTCP.usInitMSS,
1609+
( unsigned ) pxSocket->u.xTCP.usMSS,
16111610
ucFactor ) );
16121611

16131612
return ucFactor;
@@ -1634,7 +1633,7 @@
16341633
static UBaseType_t prvSetSynAckOptions( FreeRTOS_Socket_t * pxSocket,
16351634
TCPHeader_t * pxTCPHeader )
16361635
{
1637-
uint16_t usMSS = pxSocket->u.xTCP.usInitMSS;
1636+
uint16_t usMSS = pxSocket->u.xTCP.usMSS;
16381637
UBaseType_t uxOptionsLength;
16391638

16401639
/* We send out the TCP Maximum Segment Size option with our SYN[+ACK]. */
@@ -2047,7 +2046,7 @@
20472046
* along with the position in the txStream.
20482047
* Why check for MSS > 1 ?
20492048
* Because some TCP-stacks (like uIP) use it for flow-control. */
2050-
if( pxSocket->u.xTCP.usCurMSS > 1U )
2049+
if( pxSocket->u.xTCP.usMSS > 1U )
20512050
{
20522051
lDataLen = ( int32_t ) ulTCPWindowTxGet( pxTCPWindow, pxSocket->u.xTCP.ulWindowSize, &lStreamPos );
20532052
}
@@ -2663,13 +2662,13 @@
26632662

26642663
if( xTCPWindowLoggingLevel >= 0 )
26652664
{
2666-
FreeRTOS_debug_printf( ( "MSS: sending %d\n", pxSocket->u.xTCP.usCurMSS ) );
2665+
FreeRTOS_debug_printf( ( "MSS: sending %d\n", pxSocket->u.xTCP.usMSS ) );
26672666
}
26682667

26692668
pxTCPHeader->ucOptdata[ 0 ] = tcpTCP_OPT_MSS;
26702669
pxTCPHeader->ucOptdata[ 1 ] = tcpTCP_OPT_MSS_LEN;
2671-
pxTCPHeader->ucOptdata[ 2 ] = ( uint8_t ) ( ( pxSocket->u.xTCP.usCurMSS ) >> 8 );
2672-
pxTCPHeader->ucOptdata[ 3 ] = ( uint8_t ) ( ( pxSocket->u.xTCP.usCurMSS ) & 0xffU );
2670+
pxTCPHeader->ucOptdata[ 2 ] = ( uint8_t ) ( ( pxSocket->u.xTCP.usMSS ) >> 8 );
2671+
pxTCPHeader->ucOptdata[ 3 ] = ( uint8_t ) ( ( pxSocket->u.xTCP.usMSS ) & 0xffU );
26732672
uxOptionsLength = 4U;
26742673
pxTCPHeader->ucTCPOffset = ( uint8_t ) ( ( ipSIZE_OF_TCP_HEADER + uxOptionsLength ) << 2 );
26752674
}
@@ -2761,7 +2760,7 @@
27612760
/* This socket was the one connecting actively so now perform the
27622761
* synchronisation. */
27632762
vTCPWindowInit( &pxSocket->u.xTCP.xTCPWindow,
2764-
ulSequenceNumber, pxSocket->u.xTCP.xTCPWindow.ulOurSequenceNumber, ( uint32_t ) pxSocket->u.xTCP.usCurMSS );
2763+
ulSequenceNumber, pxSocket->u.xTCP.xTCPWindow.ulOurSequenceNumber, ( uint32_t ) pxSocket->u.xTCP.usMSS );
27652764
pxTCPWindow->rx.ulHighestSequenceNumber = ulSequenceNumber + 1U;
27662765
pxTCPWindow->rx.ulCurrentSequenceNumber = ulSequenceNumber + 1U;
27672766
pxTCPWindow->tx.ulCurrentSequenceNumber++; /* because we send a TCP_SYN [ | TCP_ACK ]; */
@@ -3040,7 +3039,7 @@
30403039

30413040
#if ipconfigUSE_TCP_WIN == 1
30423041
{
3043-
lMinLength = ( ( int32_t ) 2 ) * ( ( int32_t ) pxSocket->u.xTCP.usCurMSS );
3042+
lMinLength = ( ( int32_t ) 2 ) * ( ( int32_t ) pxSocket->u.xTCP.usMSS );
30443043

30453044
/* In case we're receiving data continuously, we might postpone sending
30463045
* an ACK to gain performance. */
@@ -3063,8 +3062,8 @@
30633062
pxSocket->u.xTCP.pxAckMessage = *ppxNetworkBuffer;
30643063
}
30653064

3066-
if( ( ulReceiveLength < ( uint32_t ) pxSocket->u.xTCP.usCurMSS ) || /* Received a small message. */
3067-
( lRxSpace < ipNUMERIC_CAST( int32_t, 2U * pxSocket->u.xTCP.usCurMSS ) ) ) /* There are less than 2 x MSS space in the Rx buffer. */
3065+
if( ( ulReceiveLength < ( uint32_t ) pxSocket->u.xTCP.usMSS ) || /* Received a small message. */
3066+
( lRxSpace < ipNUMERIC_CAST( int32_t, 2U * pxSocket->u.xTCP.usMSS ) ) ) /* There are less than 2 x MSS space in the Rx buffer. */
30683067
{
30693068
pxSocket->u.xTCP.usTimeout = ( uint16_t ) tcpDELAYED_ACK_SHORT_DELAY_MS;
30703069
}
@@ -3433,8 +3432,7 @@
34333432

34343433
FreeRTOS_debug_printf( ( "prvSocketSetMSS: %lu bytes for %lxip:%u\n", ulMSS, pxSocket->u.xTCP.ulRemoteIP, pxSocket->u.xTCP.usRemotePort ) );
34353434

3436-
pxSocket->u.xTCP.usInitMSS = ( uint16_t ) ulMSS;
3437-
pxSocket->u.xTCP.usCurMSS = ( uint16_t ) ulMSS;
3435+
pxSocket->u.xTCP.usMSS = ( uint16_t ) ulMSS;
34383436
}
34393437
/*-----------------------------------------------------------*/
34403438

‎include/FreeRTOS_IP_Private.h‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -632,8 +632,7 @@
632632
} bits; /**< The bits structure */
633633
uint32_t ulHighestRxAllowed; /**< The highest sequence number that we can receive at any moment */
634634
uint16_t usTimeout; /**< Time (in ticks) after which this socket needs attention */
635-
uint16_t usCurMSS; /**< Current Maximum Segment Size */
636-
uint16_t usInitMSS; /**< Initial maximum segment Size */
635+
uint16_t usMSS; /**< Current Maximum Segment Size */
637636
uint16_t usChildCount; /**< In case of a listening socket: number of connections on this port number */
638637
uint16_t usBacklog; /**< In case of a listening socket: maximum number of concurrent connections on this port number */
639638
uint8_t ucRepCount; /**< Send repeat count, for retransmissions

‎test/cbmc/proofs/TCP/prvTCPHandleState/TCPHandleState_harness.c‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,7 +74,7 @@ void harness()
7474
/* uxRxWinSize is initialized as size_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/
7575
__CPROVER_assume( pxSocket->u.xTCP.uxRxWinSize >= 0 && pxSocket->u.xTCP.uxRxWinSize <= sizeof( size_t ) );
7676
/* uxRxWinSize is initialized as uint16_t. This assumption is required to terminate `while(uxWinSize > 0xfffful)` loop.*/
77-
__CPROVER_assume( pxSocket->u.xTCP.usInitMSS == sizeof( uint16_t ) );
77+
__CPROVER_assume( pxSocket->u.xTCP.usMSS == sizeof( uint16_t ) );
7878

7979
if( xIsCallingFromIPTask() == pdFALSE )
8080
{

0 commit comments

Comments
 (0)