Skip to content

Commit 6db4337

Browse files
mgrojomgrojo
committed
Better contracts in Channel and clean-up
The socket initialization is again done outside of the main loop and it takes the passed port into account.
1 parent ba15359 commit 6db4337

4 files changed

Lines changed: 25 additions & 87 deletions

File tree

‎src/coap_spark-channel.adb‎

Lines changed: 3 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -129,7 +129,7 @@ is
129129
Option => Option);
130130

131131
if Result /= SPARK_Sockets.Success then
132-
Finalize (Socket);
132+
SPARK_Sockets.Close_Socket (Socket => Socket.Attached_Socket);
133133
return;
134134
end if;
135135

@@ -143,7 +143,7 @@ is
143143
Port => SPARK_Sockets.Port_Type (Port)));
144144

145145
if Result /= SPARK_Sockets.Success then
146-
Finalize (Socket);
146+
SPARK_Sockets.Close_Socket (Socket => Socket.Attached_Socket);
147147
return;
148148
end if;
149149

@@ -156,7 +156,7 @@ is
156156
Socket.Result := WolfSSL.Initialize;
157157

158158
if Socket.Result /= WolfSSL.Success then
159-
Finalize (Socket);
159+
SPARK_Sockets.Close_Socket (Socket => Socket.Attached_Socket);
160160
return;
161161
end if;
162162

@@ -330,17 +330,6 @@ is
330330
end if;
331331
end Send;
332332

333-
procedure Send_To
334-
(Socket : in out Socket_Type;
335-
Buffer : RFLX.RFLX_Builtin_Types.Bytes;
336-
To : Address_Type)
337-
is
338-
Data : constant Ada.Streams.Stream_Element_Array :=
339-
To_Ada_Stream (Buffer);
340-
begin
341-
Send_Socket (Socket => Socket, Item => Data, To => To);
342-
end Send_To;
343-
344333
procedure Receive_Socket
345334
(Socket : Socket_Type;
346335
Item : out Ada.Streams.Stream_Element_Array;
@@ -439,27 +428,6 @@ is
439428
end if;
440429
end Receive;
441430

442-
procedure Receive
443-
(Socket : in out Socket_Type;
444-
Buffer : out RFLX.RFLX_Builtin_Types.Bytes;
445-
Length : out RFLX.RFLX_Builtin_Types.Length;
446-
From : out Address_Type)
447-
is
448-
Data : Ada.Streams.Stream_Element_Array (1 .. Buffer'Length)
449-
with Relaxed_Initialization;
450-
Last : Ada.Streams.Stream_Element_Offset;
451-
begin
452-
453-
Receive_Socket
454-
(Socket => Socket, Item => Data, Last => Last, From => From);
455-
456-
pragma Assert (Data'Length = Buffer'Length);
457-
Buffer (Buffer'First .. RFLX.RFLX_Builtin_Types.Index'Base (Last)) :=
458-
To_RFLX_Bytes (Data (Data'First .. Last));
459-
Length := RFLX.RFLX_Builtin_Types.Length (Last);
460-
461-
end Receive;
462-
463431
procedure Accept_Connection (Socket : in out Socket_Type) is
464432
begin
465433
if Socket.Is_Secure then

‎src/coap_spark-channel.ads‎

Lines changed: 19 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -32,75 +32,51 @@ is
3232
xor (Server and then PSK_Server_Callback not in null)
3333
else
3434
(PSK_Client_Callback not in null xor PSK_Server_Callback not in null)),
35-
Relaxed_Initialization => Socket,
36-
Global => null;
35+
Relaxed_Initialization => Socket;
3736

37+
-- Accept client connections on a server socket.
3838
procedure Accept_Connection
3939
(Socket : in out Socket_Type)
4040
with
41-
-- Pre => Is_Valid (Socket),
42-
Global =>
43-
null;
41+
Pre => Is_Valid (Socket);
4442

4543
procedure Shutdown
4644
(Socket : in out Socket_Type)
4745
with
48-
Pre => Is_Valid (Socket),
49-
Global => null;
46+
Pre => Is_Valid (Socket);
5047

48+
-- When the socket is valid, it means that it has been correctly initialized.
5149
function Is_Valid (Socket : Socket_Type) return Boolean with
5250
Global =>
5351
null;
5452

53+
-- Is ready to send or receive data. Is ready to connect, when it is a client socket.
54+
function Is_Ready (Socket : Socket_Type) return Boolean with
55+
Global =>
56+
null;
57+
58+
-- Connect to a server.
5559
procedure Connect (Socket : in out Socket_Type;
5660
Server : String;
5761
Port : Port_Type := Default_Port) with
58-
Pre => Is_Valid (Socket),
59-
Global =>
60-
null;
62+
Pre => Is_Ready (Socket);
6163

6264
use type RFLX.RFLX_Builtin_Types.Index;
6365

6466
procedure Send (Socket : in out Socket_Type;
6567
Buffer : RFLX.RFLX_Builtin_Types.Bytes) with
66-
Pre => Is_Valid (Socket) and then Buffer'First = 1,
67-
Global =>
68-
null;
69-
70-
procedure Send_To (Socket : in out Socket_Type;
71-
Buffer : RFLX.RFLX_Builtin_Types.Bytes;
72-
To : Address_Type) with
73-
Pre => Is_Valid (Socket) and then
74-
Buffer'First = 1 and then
75-
Is_Valid (To),
76-
Global =>
77-
null;
68+
Pre => Is_Ready (Socket) and then Buffer'First = 1;
7869

7970
use type RFLX.RFLX_Builtin_Types.Length;
8071

8172
procedure Receive (Socket : in out Socket_Type;
8273
Buffer : out RFLX.RFLX_Builtin_Types.Bytes;
8374
Length : out RFLX.RFLX_Builtin_Types.Length) with
8475
Relaxed_Initialization => (Buffer),
85-
Pre => Is_Valid (Socket) and then Buffer'First = 1,
76+
Pre => Is_Ready (Socket) and then Buffer'First = 1,
8677
Post =>
8778
Length <= Buffer'Length and then
88-
Buffer (Buffer'First .. RFLX.RFLX_Builtin_Types.Index'Base (Length))'Initialized,
89-
Global =>
90-
null;
91-
92-
procedure Receive (Socket : in out Socket_Type;
93-
Buffer : out RFLX.RFLX_Builtin_Types.Bytes;
94-
Length : out RFLX.RFLX_Builtin_Types.Length;
95-
From : out Address_Type) with
96-
Relaxed_Initialization => (Buffer),
97-
Pre => Is_Valid (Socket) and then Buffer'First = 1,
98-
Post =>
99-
Length <= Buffer'Length and then
100-
Buffer (Buffer'First .. RFLX.RFLX_Builtin_Types.Index'Base (Length))'Initialized and then
101-
Is_Valid (From),
102-
Global =>
103-
null;
79+
Buffer (Buffer'First .. RFLX.RFLX_Builtin_Types.Index'Base (Length))'Initialized;
10480

10581
function Has_Attached_Socket (Socket : Socket_Type) return Boolean;
10682

@@ -141,7 +117,10 @@ private
141117
(Has_Attached_Socket (Socket)
142118
and then
143119
(if Socket.Is_Secure then Socket.Result = WolfSSL.Success and then
144-
-- WolfSSL.Is_Valid (Socket.Ssl) and then
145120
WolfSSL.Is_Valid (Socket.Ctx)));
146121

122+
function Is_Ready (Socket : Socket_Type) return Boolean
123+
is (Is_Valid (Socket)
124+
and then (if Socket.Is_Secure then WolfSSL.Is_Valid (Socket.Ssl)));
125+
147126
end CoAP_SPARK.Channel;

‎src/coap_spark-server_session.adb‎

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -74,20 +74,14 @@ is
7474

7575
procedure Run_Session_Loop
7676
(Ctx : in out FSM.Context;
77-
PSK_Server_Callback : WolfSSL.PSK_Server_Callback;
7877
Skt : in out CoAP_SPARK.Channel.Socket_Type)
7978
is
8079
use type FSM.State;
8180
function C_wolfSSL_Debugging_ON return Interfaces.C.int;
8281
pragma Import (C, C_wolfSSL_Debugging_ON, "wolfSSL_Debugging_ON");
8382
Result : Interfaces.C.int;
8483
begin
85-
CoAP_SPARK.Channel.Initialize
86-
(Socket => Skt,
87-
Port =>
88-
(if Skt.Is_Secure then Secure_Port else Default_Port),
89-
Server => True,
90-
PSK_Server_Callback => PSK_Server_Callback);
84+
9185
Result := C_wolfSSL_Debugging_ON;
9286

9387
while FSM.Active (Ctx) loop
@@ -108,13 +102,13 @@ is
108102
end if;
109103
Write (Ctx, Skt);
110104
end if;
111-
exit when not CoAP_SPARK.Channel.Is_Valid (Skt);
105+
exit when not CoAP_SPARK.Channel.Is_Ready (Skt);
112106
if FSM.Has_Data (Ctx, C) then
113107
Read (Ctx, Skt);
114108
end if;
115109
exit when not CoAP_SPARK.Channel.Is_Valid (Skt);
116110
end loop;
117-
exit when not CoAP_SPARK.Channel.Is_Valid (Skt);
111+
exit when not CoAP_SPARK.Channel.Is_Ready (Skt);
118112
FSM.Run (Ctx);
119113
if FSM.Next_State (Ctx) = FSM.S_Receive_Request then
120114
CoAP_SPARK.Channel.Shutdown (Skt);

‎src/coap_spark-server_session.ads‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,6 @@ with CoAP_SPARK.Channel;
22

33
with RFLX.CoAP_Server.Main_Loop.FSM;
44

5-
with WolfSSL;
6-
75
package CoAP_SPARK.Server_Session
86
with SPARK_Mode
97
is
@@ -12,7 +10,6 @@ is
1210

1311
procedure Run_Session_Loop
1412
(Ctx : in out FSM.Context;
15-
PSK_Server_Callback : WolfSSL.PSK_Server_Callback;
1613
Skt : in out CoAP_SPARK.Channel.Socket_Type)
1714
with
1815
Pre =>

0 commit comments

Comments
 (0)