ada/Http_Cyclone
0
0
Fork 0
mirror of https://github.com/AdaCore/Http_Cyclone.git synced 2026-02-12 13:07:39 -08:00
Code Issues Packages Projects Releases Wiki Activity

Add support for all the preprocessed constants of the C code in the SPARK code

Browse Source
This commit is contained in:
Guillaume Cluzel
2020-08-04 15:48:13 +02:00
parent f051aa400e
commit ea17ad063e
9 changed files with 93 additions and 24 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
Makefile
View File

@@ -428,6 +428,7 @@ clean:
rm -f $(RESULT).hex
rm -f $(RESULT).lst
rm -f $(OBJ_DIR)/*.o
rm -r ./src/spark_config.h
.PHONY: prove
prove: prove.gpr $(wildcard ./src/ada/*.adb) $(wildcard ./src/ada/*.ads)

9
options.md
View File

@@ -20,4 +20,11 @@ TCP Options
| `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 |
| `TCP_DEFAULT_SYN_QUEUE_SIZE` | Default SYN queue size for listening sockets | 1 .. `TCP_MAX_SYN_QUEUE_SIZE` | 4 |
| `TCP_MAX_MSS` | Maximum segment size | 536 .. `Short_Integer'Last` | 1430 |
| `TCP_MIN_MSS` | Mimimum acceptable segment size | 1 .. `Short_Integer'Last` | 64 |
| `TCP_DEFAULT_MSS` | Default SYN queue size for listening sockets | 1 .. `TCP_MAX_MSS` | 536 |
| `TCP_MAX_RTO` | Maximum retransmission timeout | 1000 .. `unsigned'Last` | 536 |
| `TCP_MIN_RTO` | Minimum retransmission timeout | 100 .. `TCP_MAX_RTO` | 536 |
| `TCP_DEFAULT_MSS` | Initial retransmission timeout | 1 .. `TCP_MAX_RTO` | 536 |
| `TCP_INITIAL_WINDOW` | Size of the congestion window after the three-way handshake is completed | 1 .. 20 | 3 |

7
src/ada/net_mem.ads
View File

@@ -3,6 +3,13 @@ with System;
package Net_Mem is
-- Size of the buffers
#if NET_MEM_POOL_BUFFER_SIZE'Defined then
NET_MEM_POOL_BUFFER_SIZE : constant Positive := $NET_MEM_POOL_BUFFER_SIZE;
#else
NET_MEM_POOL_BUFFER_SIZE : constant Positive := 1536;
#end if;
type Chunk_Desc is record
address : System.Address;
length : unsigned_short;

2
src/ada/net_mem_interface.ads
View File

@@ -31,7 +31,7 @@ is
Convention => C,
External_Name => "memPoolFree",
Global => null;
procedure Mem_Pool_Free
(Queue_Item : in out Tcp_Syn_Queue_Item_Acc)
with

2
src/ada/os_types.ads
View File

@@ -7,7 +7,7 @@ package Os_Types is
end record
with
Convention => C;
type Os_Event_Acc is access Os_Event;
-- This record type is consistant with the OsMutex type for freertos

4
src/ada/socket_interface.adb
View File

@@ -101,8 +101,8 @@ is
Sock.owned_Flag := False;
Sock.closed_Flag := False;
Sock.reset_Flag := False;
Sock.smss := 0;
Sock.rmss := 0;
Sock.smss := TCP_DEFAULT_MSS;
Sock.rmss := TCP_DEFAULT_MSS;
Sock.iss := 0;
Sock.irs := 0;
Sock.sndUna := 0;

12
src/ada/socket_types.ads
View File

@@ -80,7 +80,7 @@ is
SOCKET_IP_PROTO_TCP => 6,
SOCKET_IP_PROTO_UDP => 17,
SOCKET_IP_PROTO_ICMPV6 => 58);
------------------------
-- Receive queue item --
------------------------
@@ -125,8 +125,8 @@ is
closed_Flag : Bool;
reset_Flag : Bool;
smss : unsigned_short;
rmss : unsigned_short;
smss : Mss_Size;
rmss : Mss_Size;
iss : unsigned;
irs : unsigned;
@@ -183,7 +183,7 @@ is
-- UDP specific variables
receiveQueue : Socket_Queue_Item_Acc;
end record
with
with
Convention => C,
Predicate =>
Socket_Struct.S_Event_Mask = SOCKET_EVENT_TIMEOUT or else
@@ -212,7 +212,7 @@ is
SOCKET_FLAG_DELAY : constant Socket_Flags := 16#8000#;
-- Number of sockets that can be opened simultaneously
#if SOCKET_MAX_COUNT'Defined then
SOCKET_MAX_COUNT : constant Positive := $SOCKET_MAX_COUNT;
#else
@@ -301,7 +301,7 @@ is
S_Remote_Port => Sock.S_Remote_Port
))
with Ghost;
-- The transition relation function is used to compute all the transitions
-- that can happen when a message is received.

10
src/ada/tcp_interface.adb
View File

@@ -107,9 +107,9 @@ is
end if;
-- The SMSS is the size of the largest segment that the sender can transmit
Sock.smss := unsigned_short'Min (TCP_DEFAULT_MSS, TCP_MAX_MSS);
Sock.smss := Mss_Size'Min (TCP_DEFAULT_MSS, Mss_Size(TCP_MAX_MSS));
-- The RMSS is the size of the largest segment the receiver is willing to accept
Sock.rmss := unsigned_short(unsigned_long'Min
Sock.rmss := Mss_Size(unsigned_long'Min
(unsigned_long(Sock.rxBufferSize),
unsigned_long(TCP_MAX_MSS)));
@@ -328,9 +328,9 @@ is
-- The RMSS is the size of the largest segment the receiver is
-- willing to accept
Client_Socket.rmss := unsigned_short'Min
Client_Socket.rmss := Mss_Size(unsigned_short'Min
(unsigned_short(Client_Socket.rxBufferSize),
TCP_MAX_MSS);
unsigned_short(TCP_MAX_MSS)));
-- Initialize TCP control block
Client_Socket.iss := netGetRand;
@@ -348,7 +348,7 @@ is
Sock.congestState := TCP_CONGEST_STATE_IDLE;
-- Initial congestion window
Client_Socket.cwnd := unsigned_short(unsigned_long'Min
(unsigned_long(TCP_INITIAL_WINDOW * Client_Socket.smss),
(unsigned_long(TCP_INITIAL_WINDOW * unsigned_short(Client_Socket.smss)),
unsigned_long(Client_Socket.txBufferSize)));
-- Slow start threshold should be set arbitrarily high
Client_Socket.ssthresh := unsigned_short'Last;

70
src/ada/tcp_type.ads
View File

@@ -59,12 +59,62 @@ package Tcp_Type with SPARK_Mode is
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;
type Mss_Lower_Bound is range 1 .. unsigned_short'Last;
type Mss_Upper_Bound is range 536 .. unsigned_short'Last;
TCP_INITIAL_RTO : constant Systime := 1_000;
-- Mimimum acceptable segment size
#if TCP_MIN_MSS'Defined then
TCP_MIN_MSS : constant Mss_Lower_Bound := $TCP_MIN_MSS;
#else
TCP_MIN_MSS : constant Mss_Lower_Bound := 64;
#end if;
-- Maximum segment size
#if TCP_MAX_MSS'Defined then
TCP_MAX_MSS : constant Mss_Upper_Bound := $TCP_MAX_MSS;
#else
TCP_MAX_MSS : constant Mss_Upper_Bound := 1_430;
#end if;
type Mss_Size is range 1 .. TCP_MAX_MSS
with Size => unsigned_short'Size;
-- Default maximum segment size
#if TCP_DEFAULT_MSS'Defined then
TCP_DEFAULT_MSS : constant Mss_Size := $TCP_DEFAULT_MSS;
#else
TCP_DEFAULT_MSS : constant Mss_Size := 536;
#end if;
subtype Rto_Systime_Max is Systime range 1000 .. Systime'Last;
-- Maximum retransmission timeout
#if TCP_MAX_RTO'Defined then
TCP_MAX_RTO : constant Rto_Systime_Max := $TCP_MAX_RTO;
#else
TCP_MAX_RTO : constant Rto_Systime_Max := 60000;
#end if;
subtype Rto_Systime is Systime range 100 .. TCP_MAX_RTO;
-- Initial retransmission timeout
#if TCP_INITIAL_RTO'Defined then
TCP_INITIAL_RTO : constant Rto_Systime := $TCP_INITIAL_RTO;
#else
TCP_INITIAL_RTO : constant Rto_Systime := 1000;
#end if;
-- Minimum retransmission timeout
#if TCP_MIN_RTO'Defined then
TCP_MIN_RTO : constant Rto_Systime := $TCP_MIN_RTO;
#else
TCP_MIN_RTO : constant Rto_Systime := 1000;
#end if;
-- Size of the congestion window after the three-way handshake is completed
#if TCP_INITIAL_WINDOW'Defined then
TCP_INITIAL_WINDOW : constant unsigned_short := $TCP_INITIAL_WINDOW;
#else
TCP_INITIAL_WINDOW : constant unsigned_short := 3;
#end if;
-- Override timeout (should be in the range 0.1 to 1 seconds)
TCP_OVERRIDE_TIMEOUT : constant Systime := 500;
@@ -125,9 +175,11 @@ package Tcp_Type with SPARK_Mode is
TCP_FLAG_ACK : constant Tcp_Flags := 16;
TCP_FLAG_URG : constant Tcp_Flags := 32;
-- TODO: use preprocessing instead of 14 to be coherent with the C code.
type Chunk_Desc_Array is array (0 .. 14) of Chunk_Desc
with Object_Size => 15 * (32 + System.Word_Size);
type Chunk_Desc_Array_Index is range 0 .. ((TCP_MAX_TX_BUFFER_SIZE + NET_MEM_POOL_BUFFER_SIZE - 1) / NET_MEM_POOL_BUFFER_SIZE);
type Chunk_Desc_Array is array (Chunk_Desc_Array_Index) of Chunk_Desc
with
Object_Size =>
(((TCP_MAX_TX_BUFFER_SIZE + NET_MEM_POOL_BUFFER_SIZE - 1) / NET_MEM_POOL_BUFFER_SIZE) + 1) * (32 + System.Word_Size);
type Tcp_Tx_Buffer is record
chunkCount : unsigned;
@@ -135,7 +187,9 @@ package Tcp_Type with SPARK_Mode is
chunk : Chunk_Desc_Array;
end record
with
Convention => C, Object_Size => 64 + 15 * (32 + System.Word_Size);
Convention => C,
Object_Size =>
64 + (((TCP_MAX_TX_BUFFER_SIZE + NET_MEM_POOL_BUFFER_SIZE - 1) / NET_MEM_POOL_BUFFER_SIZE) + 1) * (32 + System.Word_Size);
type Tcp_Rx_Buffer is record
chunkCount : unsigned;
@@ -178,7 +232,7 @@ package Tcp_Type with SPARK_Mode is
Src_Port : Port;
Dest_Addr : IpAddr;
Isn : unsigned;
Mss : unsigned_short;
Mss : Mss_Size;
end record
with Convention => C;