cubedos-file_server-api.ads

1--------------------------------------------------------------------------------
2-- FILE : cubedos-file_server-api.ads
3-- SUBJECT: Specification of a package that simplifies use of the file server.
4-- AUTHOR : (C) Copyright 2018 by Vermont Technical College
5--
6-- All the subprograms in this package must be task safe. They can be simultaneously called
7-- from multiple tasks. If possible, make every subprogram here a pure function.
8--
9--------------------------------------------------------------------------------
10pragma SPARK_Mode(On);
11
12with CubedOS.Lib;
13with Message_Manager;
14with System;
15with Name_Resolver;
16use Message_Manager;
17
18package CubedOS.File_Server.API is
19
20 type Message_Type is
21 (Open_Request,
22 Open_Reply,
23 Read_Request,
24 Read_Reply,
25 Write_Request,
26 Write_Reply,
27 Close_Request);
28
29 type Mode_Type is (Read, Write);
30 type File_Handle_Type is range 0 .. 64;
31 subtype Valid_File_Handle_Type is File_Handle_Type range 1 .. File_Handle_Type'Last;
32
33 Invalid_Handle : constant File_Handle_Type := 0;
34 Maximum_Read_Size : constant := 256;
35 Maximum_Write_Size : constant := 256;
36
37 -- Attempted reads and writes must be for at least one octet. The reply messages contain the
38 -- number of octets successfully read or written and must allow for zero to handle the error
39 -- or end-of-file case.
40 --
41 subtype Read_Result_Size_Type is Natural range 0 .. Maximum_Read_Size;
42 subtype Read_Size_Type is Natural range 1 .. Read_Result_Size_Type'Last;
43 subtype Write_Result_Size_Type is Natural range 0 .. Maximum_Write_Size;
44 subtype Write_Size_Type is Natural range 1 .. Write_Result_Size_Type'Last;
45
46 function Open_Request_Encode
47 (Sender_Address : in Message_Address;
48 Request_ID : in Request_ID_Type;
49 Mode : in Mode_Type;
50 Name : in String;
51 Priority : in System.Priority := System.Default_Priority) return Message_Record
52 with
53 Global => null,
54 Pre => (0 < Name'Length and Name'Length <= Data_Size_Type'Last - 12);
55
56 function Open_Reply_Encode
57 (Receiver_Address : in Message_Address;
58 Request_ID : in Request_ID_Type;
59 Handle : in File_Handle_Type;
60 Priority : in System.Priority := System.Default_Priority) return Message_Record
61 with
62 Global => null;
63
64 function Read_Request_Encode
65 (Sender_Address : in Message_Address;
66 Request_ID : in Request_ID_Type;
67 Handle : in Valid_File_Handle_Type;
68 Amount : in Read_Size_Type;
69 Priority : in System.Priority := System.Default_Priority) return Message_Record
70 with Global => null;
71
72 function Read_Reply_Encode
73 (Receiver_Address : in Message_Address;
74 Request_ID : in Request_ID_Type;
75 Handle : in Valid_File_Handle_Type;
76 Amount : in Read_Result_Size_Type;
77 Data : in CubedOS.Lib.Octet_Array;
78 Priority : in System.Priority := System.Default_Priority) return Message_Record
79 with
80 Global => null,
81 Pre => Amount <= Data'Length;
82
83 function Write_Request_Encode
84 (Sender_Address : in Message_Address;
85 Request_ID : in Request_ID_Type;
86 Handle : in Valid_File_Handle_Type;
87 Amount : in Write_Size_Type;
88 Data : in CubedOS.Lib.Octet_Array;
89 Priority : in System.Priority := System.Default_Priority) return Message_Record
90 with
91 Global => null,
92 Pre => Amount <= Data'Length;
93
94 function Write_Reply_Encode
95 (Receiver_Address : in Message_Address;
96 Request_ID : in Request_ID_Type;
97 Handle : in Valid_File_Handle_Type;
98 Amount : in Write_Result_Size_Type;
99 Priority : in System.Priority := System.Default_Priority) return Message_Record
100 with Global => null;
101
102 function Close_Request_Encode
103 (Sender_Address : in Message_Address;
104 Request_ID : in Request_ID_Type;
105 Handle : in Valid_File_Handle_Type;
106 Priority : in System.Priority := System.Default_Priority) return Message_Record
107 with Global => null;
108
109
110 function Is_Open_Request(Message : in Message_Record) return Boolean is
111 (Message.Receiver_Address = Name_Resolver.File_Server and
112 Message.Message_ID = Message_Type'Pos(Open_Request));
113
114 function Is_Open_Reply(Message : in Message_Record) return Boolean is
115 (Message.Sender_Address = Name_Resolver.File_Server and
116 Message.Message_ID = Message_Type'Pos(Open_Reply));
117
118 function Is_Read_Request(Message : in Message_Record) return Boolean is
119 (Message.Receiver_Address = Name_Resolver.File_Server and
120 Message.Message_ID = Message_Type'Pos(Read_Request));
121
122 function Is_Read_Reply(Message : in Message_Record) return Boolean is
123 (Message.Sender_Address = Name_Resolver.File_Server and
124 Message.Message_ID = Message_Type'Pos(Read_Reply));
125
126 function Is_Write_Request(Message : in Message_Record) return Boolean is
127 (Message.Receiver_Address = Name_Resolver.File_Server and
128 Message.Message_ID = Message_Type'Pos(Write_Request));
129
130 function Is_Write_Reply(Message : in Message_Record) return Boolean is
131 (Message.Sender_Address = Name_Resolver.File_Server and
132 Message.Message_ID = Message_Type'Pos(Write_Reply));
133
134 function Is_Close_Request(Message : in Message_Record) return Boolean is
135 (Message.Receiver_Address = Name_Resolver.File_Server and
136 Message.Message_ID = Message_Type'Pos(Close_Request));
137
138
139 procedure Open_Request_Decode
140 (Message : in Message_Record;
141 Mode : out Mode_Type;
142 Name : out String;
143 Name_Size : out Natural;
144 Decode_Status : out Message_Status_Type)
145 with
146 Global => null,
147 Pre => Is_Open_Request(Message),
148 Depends => ((Mode, Name_Size, Decode_Status) => Message, Name =>+ Message);
149
150 procedure Open_Reply_Decode
151 (Message : in Message_Record;
152 Handle : out File_Handle_Type;
153 Decode_Status : out Message_Status_Type)
154 with
155 Global => null,
156 Pre => Is_Open_Reply(Message),
157 Depends => ((Handle, Decode_Status) => Message);
158
159 procedure Read_Request_Decode
160 (Message : in Message_Record;
161 Handle : out Valid_File_Handle_Type;
162 Amount : out Read_Size_Type;
163 Decode_Status : out Message_Status_Type)
164 with
165 Global => null,
166 Pre => Is_Read_Request(Message),
167 Depends => ((Handle, Amount, Decode_Status) => Message);
168
169 procedure Read_Reply_Decode
170 (Message : in Message_Record;
171 Handle : out Valid_File_Handle_Type;
172 Amount : out Read_Result_Size_Type;
173 Data : out CubedOS.Lib.Octet_Array;
174 Decode_Status : out Message_Status_Type)
175 with
176 Global => null,
177 Pre => Is_Read_Reply(Message) and Data'Length = Read_Result_Size_Type'Last,
178 Depends => ((Handle, Amount, Decode_Status) => Message, Data =>+ Message);
179
180 procedure Write_Request_Decode
181 (Message : in Message_Record;
182 Handle : out Valid_File_Handle_Type;
183 Amount : out Write_Size_Type;
184 Data : out CubedOS.Lib.Octet_Array;
185 Decode_Status : out Message_Status_Type)
186 with
187 Global => null,
188 Pre => Is_Write_Request(Message) and Data'Length = Read_Result_Size_Type'Last,
189 Depends => ((Handle, Amount, Decode_Status) => Message, Data =>+ Message);
190
191 procedure Write_Reply_Decode
192 (Message : in Message_Record;
193 Handle : out Valid_File_Handle_Type;
194 Amount : out Write_Result_Size_Type;
195 Decode_Status : out Message_Status_Type)
196 with
197 Global => null,
198 Pre => Is_Write_Reply(Message),
199 Depends => ((Handle, Amount, Decode_Status) => Message);
200
201 procedure Close_Request_Decode
202 (Message : in Message_Record;
203 Handle : out Valid_File_Handle_Type;
204 Decode_Status : out Message_Status_Type)
205 with
206 Global => null,
207 Pre => Is_Close_Request(Message),
208 Depends => ((Handle, Decode_Status) => Message);
209
210
211end CubedOS.File_Server.API;