diff --git a/config.def b/config.def index c6281c8..1bf893c 100644 --- a/config.def +++ b/config.def @@ -1,2 +1,11 @@ -- Number of sockets that can be opened simultaneously SOCKET_MAX_COUNT := 10 + +-- Default buffer size for reception +TCP_DEFAULT_RX_BUFFER_SIZE := 2860 + +-- Default buffer size for transmission +TCP_DEFAULT_TX_BUFFER_SIZE := 2860 + +-- Default SYN queue size for listening sockets +TCP_DEFAULT_SYN_QUEUE_SIZE := 4 diff --git a/options.md b/options.md index 7d7376b..e345387 100644 --- a/options.md +++ b/options.md @@ -3,6 +3,21 @@ List of Options The following table lists all the options allowed in the configuration file. -| **Option** | **Description** | **Range** | -|--------------------|-----------------------------------------------------|------------| -| `SOCKET_MAX_COUNT` | Number of sockets that can be opened simultaneously | `Positive` | +Socket Options +-------------- + +| **Option** | **Description** | **Range** | **Default** | +|--------------------|-----------------------------------------------------|------------|-------------| +| `SOCKET_MAX_COUNT` | Number of sockets that can be opened simultaneously | `Positive` | 16 | + +TCP Options +----------- + +| **Option** | **Description** | **Range** | **Default** | +|--------------------------|-----------------------------------------------------|------------------------|-------------| +| `TCP_MAX_RX_BUFFER_SIZE` | Maximum acceptable size for the receive buffer | 536 .. `Positive'Last` | 22_880 | +| `TCP_DEFAULT_RX_BUFFER_SIZE` | Default buffer size for reception | 536 .. `TCP_MAX_RX_BUFFER_SIZE` | 2_860 | +| `TCP_MAX_TX_BUFFER_SIZE` | Maximum acceptable size for the send buffer | 536 .. `Positive'Last` | 22_880 | +| `TCP_DEFAULT_TX_BUFFER_SIZE` | Default buffer size for transmission | 536 .. `TCP_MAX_TX_BUFFER_SIZE` | 2_860 | +| `TCP_MAX_SYN_QUEUE_SIZE` | Maximum SYN queue size for listening sockets | 1 .. `Positive'Last` | 16 | +| `TCP_DEFAULT_SYN_QUEUE_SIZE` | Default SYN queue size for listening sockets | 1 .. `TCP_MAX_SYN_QUEUE_SIZE` | 4 | \ No newline at end of file diff --git a/prove.gpr b/prove.gpr index 8bf0e94..c3f1223 100644 --- a/prove.gpr +++ b/prove.gpr @@ -1,6 +1,9 @@ project Prove is - for Source_Dirs use ("src/**"); + for Source_Dirs use (".", "src/**"); Package Compiler is - for default_switches ("Ada") use ("-gnat2020"); + for default_switches ("Ada") use + ("-gnat2020", + "-I" & Prove'Project_Dir, + "-gnatep=" & Prove'Project_Dir & "prep.data"); end Compiler; end Prove; diff --git a/src/ada/socket_interface.adb b/src/ada/socket_interface.adb index eee83c0..b229319 100644 --- a/src/ada/socket_interface.adb +++ b/src/ada/socket_interface.adb @@ -128,15 +128,16 @@ is Sock.n := 0; Sock.recover := 0; Sock.txBuffer.chunkCount := 0; - Sock.txBufferSize := 2_860; + Sock.txBufferSize := TCP_DEFAULT_TX_BUFFER_SIZE; Sock.rxBuffer.chunkCount := 0; - Sock.rxBufferSize := 2_860; + Sock.rxBufferSize := TCP_DEFAULT_RX_BUFFER_SIZE; Sock.retransmitQueue := System.Null_Address; Sock.retransmitCount := 0; Sock.synQueue := null; pragma Annotate (GNATprove, False_Positive, "memory leak might occur", "Memory should already be free"); - Sock.synQueueSize := 0; + -- Limit the number of pending connections + Sock.synQueueSize := TCP_DEFAULT_SYN_QUEUE_SIZE; Sock.wndProbeCount := 0; Sock.wndProbeInterval := 0; Sock.sackPermitted := False; diff --git a/src/ada/socket_types.ads b/src/ada/socket_types.ads index 30ba364..c742e6c 100644 --- a/src/ada/socket_types.ads +++ b/src/ada/socket_types.ads @@ -166,7 +166,7 @@ is retransmitCount : unsigned; synQueue : Tcp_Syn_Queue_Item_Acc;-- Tcp_Syn_Queue_Item_Acc; - synQueueSize : unsigned; + synQueueSize : Syn_Queue_Size; wndProbeCount : unsigned; wndProbeInterval : Systime; diff --git a/src/ada/tcp_interface.adb b/src/ada/tcp_interface.adb index f219b7b..aa41c14 100644 --- a/src/ada/tcp_interface.adb +++ b/src/ada/tcp_interface.adb @@ -186,10 +186,11 @@ is -- Set the size of the SYN queue Limit the number of pending connections if Backlog > 0 then - Sock.synQueueSize := unsigned'Min (Backlog, TCP_MAX_SYN_QUEUE_SIZE); - else Sock.synQueueSize := - unsigned'Min (TCP_DEFAULT_SYN_QUEUE_SIZE, TCP_MAX_SYN_QUEUE_SIZE); + Syn_Queue_Size( + unsigned'Min (Backlog, unsigned(TCP_MAX_SYN_QUEUE_SIZE))); + else + Sock.synQueueSize := TCP_DEFAULT_SYN_QUEUE_SIZE; end if; -- Place the socket in the listening state diff --git a/src/ada/tcp_type.ads b/src/ada/tcp_type.ads index 48288de..71139f8 100644 --- a/src/ada/tcp_type.ads +++ b/src/ada/tcp_type.ads @@ -6,11 +6,58 @@ with System; use System; package Tcp_Type with SPARK_Mode is - TCP_MAX_SYN_QUEUE_SIZE : constant unsigned := 16; - TCP_DEFAULT_SYN_QUEUE_SIZE : constant unsigned := 4; + type Syn_Queue_Size_Max is range 1 .. Natural'Last + with Size => unsigned'Size; - TCP_MAX_RX_BUFFER_SIZE : constant unsigned_long := 22_880; - TCP_MAX_TX_BUFFER_SIZE : constant unsigned_long := 22_880; + -- Maximum SYN queue size for listening sockets +#if TCP_MAX_SYN_QUEUE_SIZE'Defined then + TCP_MAX_SYN_QUEUE_SIZE : constant Syn_Queue_Size_Max := $TCP_MAX_SYN_QUEUE_SIZE; +#else + TCP_MAX_SYN_QUEUE_SIZE : constant Syn_Queue_Size_Max := 16; +#end if; + + type Syn_Queue_Size is range 1 .. TCP_MAX_SYN_QUEUE_SIZE + with Size => unsigned'Size; + + -- Default SYN queue size for listening sockets +#if TCP_DEFAULT_SYN_QUEUE_SIZE'Defined then + TCP_DEFAULT_SYN_QUEUE_SIZE : constant Syn_Queue_Size := $TCP_DEFAULT_SYN_QUEUE_SIZE; +#else + TCP_DEFAULT_SYN_QUEUE_SIZE : constant Syn_Queue_Size := 4; +#end if; + + subtype Buffer_Size is Natural range 536 .. Natural'Last; + + -- Maximum acceptable size for the receive buffer +#if TCP_MAX_RX_BUFFER_SIZE'Defined then + TCP_MAX_RX_BUFFER_SIZE : constant Buffer_Size := $TCP_MAX_RX_BUFFER_SIZE; +#else + TCP_MAX_RX_BUFFER_SIZE : constant Buffer_Size := 22_880; +#end if; + + -- Maximum acceptable size for the send buffer +#if TCP_MAX_TX_BUFFER_SIZE'Defined then + TCP_MAX_TX_BUFFER_SIZE : constant Buffer_Size := $TCP_MAX_TX_BUFFER_SIZE; +#else + TCP_MAX_TX_BUFFER_SIZE : constant Buffer_Size := 22_880; +#end if; + + type Tx_Buffer_Size is range 1 .. TCP_MAX_TX_BUFFER_SIZE; + type Rx_Buffer_Size is range 1 .. TCP_MAX_RX_BUFFER_SIZE; + + -- Default buffer size for reception +#if TCP_DEFAULT_RX_BUFFER_SIZE'Defined then + TCP_DEFAULT_RX_BUFFER_SIZE : constant Rx_Buffer_Size := $TCP_DEFAULT_RX_BUFFER_SIZE; +#else + TCP_DEFAULT_RX_BUFFER_SIZE : constant Rx_Buffer_Size := 2_860; +#end if; + + -- Default buffer size for transmission +#if TCP_DEFAULT_TX_BUFFER_SIZE'Defined then + TCP_DEFAULT_TX_BUFFER_SIZE : constant Tx_Buffer_Size := $TCP_DEFAULT_TX_BUFFER_SIZE; +#else + TCP_DEFAULT_TX_BUFFER_SIZE : constant Tx_Buffer_Size := 2_860; +#end if; TCP_DEFAULT_MSS : constant unsigned_short := 536; TCP_MAX_MSS : constant unsigned_short := 1_430; @@ -82,9 +129,6 @@ package Tcp_Type with SPARK_Mode is type Chunk_Desc_Array is array (0 .. 14) of Chunk_Desc with Object_Size => 15 * (32 + System.Word_Size); - type Tx_Buffer_Size is range 1 .. TCP_MAX_TX_BUFFER_SIZE; - type Rx_Buffer_Size is range 1 .. TCP_MAX_RX_BUFFER_SIZE; - type Tcp_Tx_Buffer is record chunkCount : unsigned; maxChunkCound : unsigned; diff --git a/src/net_config.h b/src/net_config.h index 2ffdad7..aac2e64 100644 --- a/src/net_config.h +++ b/src/net_config.h @@ -123,12 +123,6 @@ //TCP support #define TCP_SUPPORT ENABLED -//Default buffer size for transmission -#define TCP_DEFAULT_TX_BUFFER_SIZE (1430*2) -//Default buffer size for reception -#define TCP_DEFAULT_RX_BUFFER_SIZE (1430*2) -//Default SYN queue size for listening sockets -#define TCP_DEFAULT_SYN_QUEUE_SIZE 4 //Maximum number of retransmissions #define TCP_MAX_RETRIES 5 //Selective acknowledgment support