Skip to content
This repository was archived by the owner on May 22, 2023. It is now read-only.

Commit 791fe08

Browse files
jklmnnsenier
jklmnn
authored and
senier
committedSep 24, 2019
prove block server test
ref #80
·
v0.2.0v0.1.0
1 parent 8539f06 commit 791fe08

File tree

2 files changed

+122
-55
lines changed

2 files changed

+122
-55
lines changed
 

‎test/block_server/component.adb

+108-52
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,18 @@
11

22
with Componolit.Interfaces.Log.Client;
33

4-
package body Component is
4+
package body Component with
5+
SPARK_Mode
6+
is
7+
use type Block.Id;
8+
use type Block.Request_Status;
9+
use type Block.Request_Kind;
510

611
Log : Componolit.Interfaces.Log.Client_Session := Componolit.Interfaces.Log.Client.Create;
712
Dispatcher : Block.Dispatcher_Session := Block_Dispatcher.Create;
813
Server : Block.Server_Session := Block_Server.Create;
914

10-
subtype Block_Buffer is Buffer (1 .. 512);
11-
type Disk is array (Block.Id range 0 .. 1023) of Block_Buffer;
15+
subtype Disk is Buffer (0 .. 524287); -- Disk_Block_Size * Disk_Block_Count - 1
1216

1317
Ram_Disk : Disk;
1418

@@ -23,18 +27,26 @@ package body Component is
2327
Handled => False,
2428
Success => False));
2529

26-
use all type Block.Id;
27-
use all type Block.Count;
28-
use all type Block.Request_Kind;
29-
use all type Block.Request_Status;
30-
3130
procedure Construct (Cap : Componolit.Interfaces.Types.Capability)
3231
is
3332
begin
34-
Componolit.Interfaces.Log.Client.Initialize (Log, Cap, "Ada_Block_Server");
35-
Block_Dispatcher.Initialize (Dispatcher, Cap);
36-
Block_Dispatcher.Register (Dispatcher);
37-
Componolit.Interfaces.Log.Client.Info (Log, "Dispatcher initialized");
33+
if not Componolit.Interfaces.Log.Client.Initialized (Log) then
34+
Componolit.Interfaces.Log.Client.Initialize (Log, Cap, "Ada_Block_Server");
35+
end if;
36+
if Componolit.Interfaces.Log.Client.Initialized (Log) then
37+
if not Block_Dispatcher.Initialized (Dispatcher) then
38+
Block_Dispatcher.Initialize (Dispatcher, Cap);
39+
end if;
40+
if Block_Dispatcher.Initialized (Dispatcher) then
41+
Block_Dispatcher.Register (Dispatcher);
42+
Componolit.Interfaces.Log.Client.Info (Log, "Dispatcher initialized");
43+
else
44+
Componolit.Interfaces.Log.Client.Error (Log, "Failed to initialize dispatcher");
45+
Main.Vacate (Cap, Main.Failure);
46+
end if;
47+
else
48+
Main.Vacate (Cap, Main.Failure);
49+
end if;
3850
end Construct;
3951

4052
procedure Destruct
@@ -48,47 +60,59 @@ package body Component is
4860
end if;
4961
end Destruct;
5062

51-
procedure Read (R : in out Cache_Element);
63+
procedure Read (R : in out Cache_Element) with
64+
Pre => Block_Server.Initialized (Server)
65+
and then Block_Server.Status (R.Req) = Block.Pending
66+
and then Block_Server.Kind (R.Req) = Block.Read
67+
and then Block_Server.Start (R.Req) <= Block.Id (Ram_Disk'Length / Disk_Block_Size)
68+
and then Block_Server.Length (R.Req) > 0
69+
and then Block_Server.Length (R.Req) <= Block.Count (Ram_Disk'Length / Disk_Block_Size),
70+
Post => Block_Server.Initialized (Server);
5271

5372
procedure Read (R : in out Cache_Element)
5473
is
55-
Start : constant Block.Id := Block_Server.Start (R.Req);
74+
Start : constant Block.Count := Block.Count (Block_Server.Start (R.Req));
5675
Length : constant Block.Count := Block_Server.Length (R.Req);
57-
Buf : Buffer (1 .. Length * Block_Size (Block_Server.Instance (Server)));
5876
begin
59-
if Buf'Length mod Block_Buffer'Length = 0 and then
60-
Start in Ram_Disk'Range and then
61-
Start + (Length - 1) in Ram_Disk'Range
77+
if
78+
Start * Disk_Block_Size in Ram_Disk'Range
79+
and then (Start + Length) * Disk_Block_Size - 1 in Ram_Disk'Range
6280
then
63-
for I in Block.Id range Start .. Start + (Length - 1) loop
64-
Buf (Buf'First + (I - Start) * Block_Buffer'Length ..
65-
Buf'First + (I - Start + 1) * Block_Buffer'Length - 1) := Ram_Disk (I);
66-
end loop;
67-
Block_Server.Read (Server, R.Req, Buf);
81+
Block_Server.Read
82+
(Server,
83+
R.Req,
84+
Ram_Disk (Start * Disk_Block_Size .. (Start + Length) * Disk_Block_Size - 1));
6885
R.Success := True;
86+
else
87+
R.Success := False;
6988
end if;
7089
end Read;
7190

72-
procedure Write (R : in out Cache_Element);
91+
procedure Write (R : in out Cache_Element) with
92+
Pre => Block_Server.Initialized (Server)
93+
and then Block_Server.Status (R.Req) = Block.Pending
94+
and then Block_Server.Kind (R.Req) = Block.Write
95+
and then Block_Server.Start (R.Req) <= Block.Id (Ram_Disk'Length / Disk_Block_Size)
96+
and then Block_Server.Length (R.Req) > 0
97+
and then Block_Server.Length (R.Req) <= Block.Count (Ram_Disk'Length / Disk_Block_Size),
98+
Post => Block_Server.Initialized (Server);
7399

74100
procedure Write (R : in out Cache_Element)
75101
is
76-
Start : constant Block.Id := Block_Server.Start (R.Req);
102+
Start : constant Block.Count := Block.Count (Block_Server.Start (R.Req));
77103
Length : constant Block.Count := Block_Server.Length (R.Req);
78-
B : Buffer (1 .. Length * Block_Size (Block_Server.Instance (Server)));
79104
begin
80105
if
81-
B'Length mod Block_Buffer'Length = 0 and then
82-
Start in Ram_Disk'Range and then
83-
Start + (Length - 1) in Ram_Disk'Range
106+
Start * Disk_Block_Size in Ram_Disk'Range
107+
and then (Start + Length) * Disk_Block_Size - 1 in Ram_Disk'Range
84108
then
85-
Block_Server.Write (Server, R.Req, B);
86-
for I in Block.Id range Start .. Start + (Length - 1) loop
87-
Ram_Disk (I) :=
88-
B (B'First + (I - Start) * Block_Buffer'Length ..
89-
B'First + ((I - Start) + 1) * Block_Buffer'Length - 1);
90-
end loop;
109+
Block_Server.Write
110+
(Server,
111+
R.Req,
112+
Ram_Disk (Start * Disk_Block_Size .. (Start + Length) * Disk_Block_Size - 1));
91113
R.Success := True;
114+
else
115+
R.Success := False;
92116
end if;
93117
end Write;
94118

@@ -107,13 +131,22 @@ package body Component is
107131
and then not Request_Cache (I).Handled
108132
then
109133
Request_Cache (I).Handled := True;
110-
case Block_Server.Kind (Request_Cache (I).Req) is
111-
when Block.Read =>
112-
Read (Request_Cache (I));
113-
when Block.Write =>
114-
Write (Request_Cache (I));
115-
when others => null;
116-
end case;
134+
if
135+
Block_Server.Start (Request_Cache (I).Req) <= Block.Id (Ram_Disk'Length / Disk_Block_Size)
136+
and then Block_Server.Length (Request_Cache (I).Req) > 0
137+
and then Block_Server.Length (Request_Cache (I).Req) <=
138+
Block.Count (Ram_Disk'Length / Disk_Block_Size)
139+
then
140+
case Block_Server.Kind (Request_Cache (I).Req) is
141+
when Block.Read =>
142+
Read (Request_Cache (I));
143+
when Block.Write =>
144+
Write (Request_Cache (I));
145+
when others => null;
146+
end case;
147+
else
148+
Request_Cache (I).Success := False;
149+
end if;
117150
end if;
118151
if
119152
Block_Server.Status (Request_Cache (I).Req) = Block.Pending
@@ -131,14 +164,14 @@ package body Component is
131164
is
132165
pragma Unreferenced (S);
133166
begin
134-
return Block.Count (Ram_Disk'Length);
167+
return Disk_Block_Count;
135168
end Block_Count;
136169

137170
function Block_Size (S : Block.Server_Instance) return Block.Size
138171
is
139172
pragma Unreferenced (S);
140173
begin
141-
return Block.Size (Block_Buffer'Length);
174+
return Disk_Block_Size;
142175
end Block_Size;
143176

144177
function Writable (S : Block.Server_Instance) return Boolean
@@ -159,10 +192,28 @@ package body Component is
159192
is
160193
pragma Unreferenced (S);
161194
pragma Unreferenced (B);
195+
Max : Natural;
162196
begin
163-
Componolit.Interfaces.Log.Client.Info (Log, "Server initialize with label: " & L);
164-
Ram_Disk := (others => (others => 0));
165-
Componolit.Interfaces.Log.Client.Info (Log, "Initialized");
197+
if Componolit.Interfaces.Log.Client.Initialized (Log) then
198+
Max := Componolit.Interfaces.Log.Client.Maximum_Message_Length (Log);
199+
Componolit.Interfaces.Log.Client.Info (Log, "Server initialize with label: ");
200+
if L'Length <= Max then
201+
Componolit.Interfaces.Log.Client.Info (Log, L);
202+
else
203+
for I in Natural range 0 .. Natural'Last / Max - L'First - 1 loop
204+
pragma Loop_Invariant (Componolit.Interfaces.Log.Client.Initialized (Log));
205+
pragma Loop_Invariant (Max = Componolit.Interfaces.Log.Client.Maximum_Message_Length (Log));
206+
if L'First + (I + 1) * Max <= L'Last then
207+
Componolit.Interfaces.Log.Client.Info (Log, L (L'First + I * Max .. L'First + (I + 1) * Max - 1));
208+
else
209+
Componolit.Interfaces.Log.Client.Info (Log, L (L'First + I * Max .. L'Last));
210+
exit;
211+
end if;
212+
end loop;
213+
end if;
214+
Componolit.Interfaces.Log.Client.Info (Log, "Initialized");
215+
end if;
216+
Ram_Disk := (others => 0);
166217
end Initialize;
167218

168219
procedure Finalize (S : Block.Server_Instance)
@@ -175,13 +226,18 @@ package body Component is
175226
procedure Request (C : Block.Dispatcher_Capability)
176227
is
177228
begin
178-
if Block_Dispatcher.Valid_Session_Request (Dispatcher, C) and not Block_Server.Initialized (Server) then
179-
Block_Dispatcher.Session_Initialize (Dispatcher, C, Server);
180-
if Block_Server.Initialized (Server) then
181-
Block_Dispatcher.Session_Accept (Dispatcher, C, Server);
229+
if Block_Dispatcher.Initialized (Dispatcher) then
230+
if
231+
Block_Dispatcher.Valid_Session_Request (Dispatcher, C)
232+
and then not Block_Server.Initialized (Server)
233+
then
234+
Block_Dispatcher.Session_Initialize (Dispatcher, C, Server);
235+
if Block_Server.Initialized (Server) then
236+
Block_Dispatcher.Session_Accept (Dispatcher, C, Server);
237+
end if;
182238
end if;
239+
Block_Dispatcher.Session_Cleanup (Dispatcher, C, Server);
183240
end if;
184-
Block_Dispatcher.Session_Cleanup (Dispatcher, C, Server);
185241
end Request;
186242

187243
end Component;

‎test/block_server/component.ads

+14-3
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,9 @@ with Componolit.Interfaces.Block;
55
with Componolit.Interfaces.Block.Server;
66
with Componolit.Interfaces.Block.Dispatcher;
77

8-
package Component is
8+
package Component with
9+
SPARK_Mode
10+
is
911

1012
procedure Construct (Cap : Componolit.Interfaces.Types.Capability);
1113
procedure Destruct;
@@ -18,9 +20,18 @@ package Component is
1820

1921
package Block is new Componolit.Interfaces.Block (Byte, Unsigned_Long, Buffer);
2022

23+
use type Block.Count;
24+
use type Block.Size;
25+
26+
Disk_Block_Size : constant Block.Size := 512;
27+
Disk_Block_Count : constant Block.Count := 1024;
28+
2129
procedure Event;
22-
function Block_Count (S : Block.Server_Instance) return Block.Count;
23-
function Block_Size (S : Block.Server_Instance) return Block.Size;
30+
function Block_Count (S : Block.Server_Instance) return Block.Count with
31+
Post => Block_Count'Result = Disk_Block_Count;
32+
function Block_Size (S : Block.Server_Instance) return Block.Size with
33+
Post => Block_Size'Result = Disk_Block_Size,
34+
Annotate => (GNATprove, Terminating);
2435
function Writable (S : Block.Server_Instance) return Boolean;
2536
function Initialized (S : Block.Server_Instance) return Boolean;
2637
procedure Initialize (S : Block.Server_Instance; L : String; B : Block.Byte_Length);

0 commit comments

Comments
 (0)
This repository has been archived.