1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
|
-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================
--------------------------------------------------------------------------------
--Synopsis: --
-- --
-- Package containing subprogram bodies to facilitate incremental parsing of a --
-- simplifier log file. --
--------------------------------------------------------------------------------
with Ada.Characters.Latin_1;
package body SLG_Parser is
function First_Three (Line : E_Strings.T) return Key_String is
begin
return Key_String'
(1 => E_Strings.Get_Element (E_Str => Line,
Pos => 1),
2 => E_Strings.Get_Element (E_Str => Line,
Pos => 2),
3 => E_Strings.Get_Element (E_Str => Line,
Pos => 3));
end First_Three;
function Lookup_Key (Line : E_Strings.T) return Log_Key is
Key_Str : Key_String;
Key : Log_Key;
begin
if E_Strings.Get_Length (E_Str => Line) >= 3 then
Key_Str := First_Three (Line);
if Key_Str = "RRS" then
Key := Read_Rulefiles_Header;
elsif Key_Str = "&&&" then
Key := Load_Rulefile;
elsif Key_Str = "STX" then
Key := Syntax_Error_Header;
elsif Key_Str = "!!!" then
Key := Syntax_Error_In_Rulefile;
elsif Key_Str = "SEM" then
Key := No_Semantic_Checks_Header;
elsif Key_Str = "@@@" then
Key := VC_Header;
elsif Key_Str = "%%%" then
Key := Simplified;
elsif Key_Str = ">>>" then
Key := Restructured;
elsif Key_Str = "***" then
Key := Proved;
elsif Key_Str = "###" then
Key := Contradiction;
elsif Key_Str = "---" then
Key := Hyp_Eliminated;
elsif Key_Str = "+++" then
Key := Hyp_Added;
elsif Key_Str = "-S-" then
Key := Substitution;
elsif Key_Str = "<S>" then
Key := New_Hyp_From_Subs;
elsif Key_Str = "VCN" then
Key := VC_Summary_Header;
elsif Key_Str = "FIL" then
Key := Rulefile_Use;
elsif Key_Str = "RUL" then
Key := Rule_Use;
elsif Key_Str = "CON" then
Key := Conclusions;
elsif Key_Str = "HYP" then
Key := Hypotheses;
elsif Key_Str = "OVR" then
Key := Overall_Summary_Header;
elsif Key_Str = "VCS" then
Key := VCs_Using_Rule;
else
Key := Not_A_Recognised_Key;
end if;
else
Key := No_Room_For_Key;
end if;
return Key;
end Lookup_Key;
function Is_White_Space (C : Character) return Boolean is
begin
return C = ' '
or else C = Ada.Characters.Latin_1.HT
or else C = Ada.Characters.Latin_1.LF
or else C = Ada.Characters.Latin_1.CR;
end Is_White_Space;
pragma Inline (Is_White_Space);
function Is_Char_At_Posn (C : Character;
Logfile : Log_Info_T) return Boolean is
begin
return (Logfile.Posn > 0 and then Logfile.Posn <= E_Strings.Get_Length (E_Str => Logfile.Curr_Line))
and then E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => Logfile.Posn) = C;
end Is_Char_At_Posn;
pragma Inline (Is_Char_At_Posn);
function Is_Whitespace_At_Posn (Logfile : Log_Info_T) return Boolean is
begin
return (Logfile.Posn > 0 and then Logfile.Posn <= E_Strings.Get_Length (E_Str => Logfile.Curr_Line))
and then Is_White_Space (C => E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => Logfile.Posn));
end Is_Whitespace_At_Posn;
pragma Inline (Is_Whitespace_At_Posn);
procedure Inc_Posn (Logfile : in out Log_Info_T)
--# derives Logfile from *;
--# pre Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
--# post Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
is
begin
if Logfile.Posn > 0 then
if Logfile.Posn >= E_Strings.Get_Length (E_Str => Logfile.Curr_Line) then
Logfile.Posn := 0;
else
Logfile.Posn := Logfile.Posn + 1;
end if;
end if;
end Inc_Posn;
pragma Inline (Inc_Posn);
procedure Get_Item (Logfile : in out Log_Info_T;
Item : out E_Strings.T)
--# derives Item,
--# Logfile from Logfile;
--# pre Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
--# post Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
is
Start_Posn : E_Strings.Lengths;
End_Posn : E_Strings.Lengths;
begin
Item := E_Strings.Empty_String;
if Logfile.Posn > 0 then
Start_Posn := Logfile.Posn;
End_Posn := Start_Posn;
-- Find the last character position of the item.
-- Items are separated by commas or teminated by an end of line.
while End_Posn < E_Strings.Get_Length (E_Str => Logfile.Curr_Line)
and then E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => End_Posn + 1) /= ',' loop
End_Posn := End_Posn + 1;
--# assert End_Posn <= E_Strings.Get_Length (Logfile.Curr_Line)
--# and Start_Posn > 0;
end loop;
--# assert End_Posn <= E_Strings.Get_Length (Logfile.Curr_Line)
--# and Start_Posn > 0;
-- Update the Logfile Posn to the terminating character or
-- to 0 if the entire current line has been read.
if End_Posn = E_Strings.Get_Length (E_Str => Logfile.Curr_Line) then
Logfile.Posn := 0;
else
Logfile.Posn := End_Posn + 1;
end if;
-- Copy the substring to the Item result string.
for I in E_Strings.Lengths range Start_Posn .. End_Posn loop
--# assert Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line)
--# and Start_Posn > 0;
E_Strings.Append_Char (E_Str => Item,
Ch => E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => I));
end loop;
end if;
end Get_Item;
procedure Get_Next_Keyed_Line (Logfile : in out Log_Info_T)
--# global in out SPARK_IO.File_Sys;
--# derives Logfile,
--# SPARK_IO.File_Sys from Logfile,
--# SPARK_IO.File_Sys;
--# post Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
is
F : SPARK_IO.File_Type;
Found : Boolean := False;
EOF : Boolean := False;
begin
F := Logfile.File_Handle;
while not (Found or EOF) loop
if SPARK_IO.End_Of_File (F) then
Logfile.Key := Reached_EOF;
-- Remove any existing line.
Logfile.Curr_Line := E_Strings.Empty_String;
EOF := True;
else
E_Strings.Get_Line (File => F,
E_Str => Logfile.Curr_Line);
Logfile.Key := Lookup_Key (Logfile.Curr_Line);
Found := (Logfile.Key in Legal_Log_Keys);
end if;
end loop;
if Found then
if E_Strings.Get_Length (E_Str => Logfile.Curr_Line) >= 4 then
Logfile.Posn := 4;
else
Logfile.Posn := 0;
end if;
elsif E_Strings.Get_Length (E_Str => Logfile.Curr_Line) > 0 then
Logfile.Posn := 1;
else
Logfile.Posn := 0;
end if;
end Get_Next_Keyed_Line;
procedure Get_Next_Line (Logfile : in out Log_Info_T)
--# global in out SPARK_IO.File_Sys;
--# derives Logfile,
--# SPARK_IO.File_Sys from Logfile,
--# SPARK_IO.File_Sys;
--# post Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
is
F : SPARK_IO.File_Type;
Found : Boolean;
begin
F := Logfile.File_Handle;
if SPARK_IO.End_Of_File (F) then
Logfile.Key := Reached_EOF;
-- Remove any existing line.
Logfile.Curr_Line := E_Strings.Empty_String;
Found := False;
else
E_Strings.Get_Line (File => F,
E_Str => Logfile.Curr_Line);
Logfile.Key := Lookup_Key (Logfile.Curr_Line);
Found := (Logfile.Key in Legal_Log_Keys);
end if;
if Found then
if E_Strings.Get_Length (E_Str => Logfile.Curr_Line) >= 4 then
Logfile.Posn := 4;
else
Logfile.Posn := 0;
end if;
elsif E_Strings.Get_Length (E_Str => Logfile.Curr_Line) > 0 then
Logfile.Posn := 1;
else
Logfile.Posn := 0;
end if;
end Get_Next_Line;
procedure Get_Next_Item (Logfile : in out Log_Info_T;
Item : out E_Strings.T;
Status : out Log_Status_T)
--# global in out SPARK_IO.File_Sys;
--# derives Item,
--# Logfile,
--# SPARK_IO.File_Sys,
--# Status from Logfile,
--# SPARK_IO.File_Sys;
--# pre Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
--# post Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
is
Continue_Search : Boolean;
Have_Found : Boolean;
Keep_Key : Log_Key;
Keep_Key_Found : Boolean;
begin
-- At start, have not found an item.
Item := E_Strings.Empty_String;
-- Here we try to get an item (a block of text without white space)
-- from the keyed line. Subsequent lines are considered to be part
-- of the keyed line if they match the pattern of wrapped text. This
-- is necessary, as the wrap_utility applies globally to a file.
-- It is not correct to assume that all data will reside on the
-- originating keyed line.
Continue_Search := True;
Have_Found := False;
while (Continue_Search and (not Have_Found)) loop
-- Scan the current keyed line for non-space, non-comma character,
-- or reaching end of line.
loop
--# assert Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
exit when not (Is_Whitespace_At_Posn (Logfile)) and not (Is_Char_At_Posn (',', Logfile));
Inc_Posn (Logfile);
end loop;
--# assert Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
if not (Logfile.Posn = 0) then
-- Found: non-space, non-comma character.
Continue_Search := False;
Have_Found := True;
--# check Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
else
-- Found: end of line.
-- Keep the current key, and consider the next line.
-- It's deemed to be a continuation if it is not the end of
-- the file and it starts with:
-- " [^ ]" (ten spaces, followed by a non-space).
Keep_Key := Logfile.Key;
Keep_Key_Found := Logfile.Key_Found;
Get_Next_Line (Logfile);
--# check Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
if not (Logfile.Key = Reached_EOF)
and then E_Strings.Get_Length (E_Str => Logfile.Curr_Line) >= 11
and then (E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => 1) = ' '
and then E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => 2) = ' '
and then E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => 3) = ' '
and then E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => 4) = ' '
and then E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => 5) = ' '
and then E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => 6) = ' '
and then E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => 7) = ' '
and then E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => 8) = ' '
and then E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => 9) = ' '
and then E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => 10) = ' '
and then not (E_Strings.Get_Element (E_Str => Logfile.Curr_Line,
Pos => 11) = ' ')) then
-- Found: Is a continuation. Set the Key and Key_Found accordingly.
Continue_Search := True;
Logfile.Key := Keep_Key;
Logfile.Key_Found := Keep_Key_Found;
else
-- Found: Is not a continuation. Set Key_Found accordingly.
Continue_Search := False;
Logfile.Key_Found := False;
end if;
end if;
end loop;
--# assert Logfile.Posn <= E_Strings.Get_Length (Logfile.Curr_Line);
-- If found start of a block of text, get the item.
if (Have_Found) then
Get_Item (Logfile, Item);
if E_Strings.Get_Length (E_Str => Item) > 0 then
Status := Success;
else
Status := Not_Found;
end if;
else
Status := Not_Found;
end if;
end Get_Next_Item;
procedure Find_Header (Header : in Log_Key;
Logfile : in out Log_Info_T;
Status : out Log_Status_T)
--# global in out SPARK_IO.File_Sys;
--# derives Logfile,
--# SPARK_IO.File_Sys,
--# Status from Header,
--# Logfile,
--# SPARK_IO.File_Sys;
is
Searching : Boolean;
begin
-- The current line may contain the header desired. Only look at the
-- next line if it does not.
Status := Not_Found;
Searching := True;
while Searching loop
if Logfile.Key = Header then
Status := Success;
Searching := False;
elsif Logfile.Key in Log_Headers and then Logfile.Key > Header then
-- A later section header has been encountered and
-- the given Header is assumed to be not present.
-- Status = Not_Found;
Searching := False;
elsif Logfile.Key = Reached_EOF then
Status := End_Of_File;
Searching := False;
else
Get_Next_Keyed_Line (Logfile);
end if;
end loop;
Logfile.Key_Found := Status = Success;
end Find_Header;
procedure Get_Next_Subsection
(Subsection : in Log_Key;
Logfile : in out Log_Info_T;
Item : out E_Strings.T;
Status : out Log_Status_T)
--# global in out SPARK_IO.File_Sys;
--# derives Item,
--# Logfile,
--# SPARK_IO.File_Sys,
--# Status from Logfile,
--# SPARK_IO.File_Sys,
--# Subsection;
is
begin
-- Three scenarios are possible when we get here:
--
-- 1) Have not looked at any lines. Logfile.Key will be 'Been_Initialised'.
-- So: Want to get the next keyed line.
-- 2) On a keyed line that has been fully processed. Logfile.Key_Found
-- will be true, and Logfile.Key will be in Legal_Log_Keys.
-- So: Want to get the next keyed line.
-- 3) Have looked at the next line, searching for a continuation, but
-- did not find one. Logfile.Key_Found will be false. Logfile.Key may
-- be anything (we may or may not be on a keyed line).
-- So: Only if this is not a keyed line, want to get the next keyed line.
if Logfile.Key_Found or not (Logfile.Key in Legal_Log_Keys) then
Get_Next_Keyed_Line (Logfile);
end if;
if Logfile.Key = Subsection then
Logfile.Key_Found := True;
Get_Next_Item (Logfile, Item, Status);
if Status /= Success then
Status := Unexpected_Text;
end if;
else
Logfile.Key_Found := False;
Status := Not_Found;
Item := E_Strings.Empty_String;
end if;
end Get_Next_Subsection;
procedure Init (Logfile_Name : in E_Strings.T;
Info : out Log_Info_T;
Status : out Log_Status_T) is
Open_Status : SPARK_IO.File_Status;
begin
--# accept F, 23, Info.File_Handle, "The call to open initalises File_Handle";
E_Strings.Open
(File => Info.File_Handle,
Mode_Of_File => SPARK_IO.In_File,
Name_Of_File => Logfile_Name,
Form_Of_File => "",
Status => Open_Status);
--# end accept;
if Open_Status = SPARK_IO.Ok then
Status := Success;
else
Status := Failure;
end if;
Info.Key := Been_Initialised;
Info.Key_Found := False;
Info.Posn := 0;
Info.Curr_Line := E_Strings.Empty_String;
--# accept F, 602, SPARK_IO.File_Sys, Info.File_Handle,
--# "The call to open initalises File_Handle";
--# accept F, 602, Info, Info.File_Handle,
--# "The call to open initalises File_Handle";
--# accept F, 602, Status, Info.File_Handle,
--# "The call to open initalises File_Handle";
end Init;
procedure Find_Rulefiles_Read (Info : in out Log_Info_T;
Status : out Log_Status_T) is
begin
Find_Header (Read_Rulefiles_Header, Info, Status);
end Find_Rulefiles_Read;
procedure Find_Rule_Syntax_Errors (Info : in out Log_Info_T;
Status : out Log_Status_T) is
begin
Find_Header (Syntax_Error_Header, Info, Status);
end Find_Rule_Syntax_Errors;
procedure Get_Next_Rulefile_Syntax_Error (Info : in out Log_Info_T;
Rulefile : out E_Strings.T;
Status : out Log_Status_T) is
begin
Get_Next_Subsection (Syntax_Error_In_Rulefile, Info, Rulefile, Status);
end Get_Next_Rulefile_Syntax_Error;
procedure Find_Rule_Summary (Info : in out Log_Info_T;
Status : out Log_Status_T) is
begin
Find_Header (Overall_Summary_Header, Info, Status);
end Find_Rule_Summary;
procedure Get_Next_Rulefile (Info : in out Log_Info_T;
Rulefile : out E_Strings.T;
Status : out Log_Status_T) is
begin
Get_Next_Subsection (Rulefile_Use, Info, Rulefile, Status);
end Get_Next_Rulefile;
procedure Get_Next_Rule (Info : in out Log_Info_T;
Rule : out E_Strings.T;
Status : out Log_Status_T) is
begin
Get_Next_Subsection (Rule_Use, Info, Rule, Status);
end Get_Next_Rule;
procedure Get_Next_VC (Info : in out Log_Info_T;
VC_Number : out E_Strings.T;
Status : out Log_Status_T) is
begin
if Info.Key = VCs_Using_Rule then
-- A VCs_Using_Rule line is already being parsed.
Get_Next_Item (Info, VC_Number, Status);
else
-- Move to the VCs_Using_Rule line and get first VC number.
Get_Next_Subsection (VCs_Using_Rule, Info, VC_Number, Status);
end if;
end Get_Next_VC;
procedure Finalise (Info : in out Log_Info_T) is
Not_Used : SPARK_IO.File_Status;
begin
--# accept F, 10, Not_Used, "The status returned from Close is not used";
--# accept F, 33, Not_Used, "The status returned from Close is not used";
SPARK_IO.Close (Info.File_Handle, Not_Used);
end Finalise;
end SLG_Parser;
|
