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 | ------------------------------------------------------------------------------
-- Copyright (C) 2020 by Heisenbug Ltd. (gh+spat@heisenbug.eu)
--
-- This work is free. You can redistribute it and/or modify it under the
-- terms of the Do What The Fuck You Want To Public License, Version 2,
-- as published by Sam Hocevar. See the LICENSE file for more details.
------------------------------------------------------------------------------
pragma License (Unrestricted);
------------------------------------------------------------------------------
--
-- SPARK Proof Analysis Tool
--
-- S.P.A.T. - Main program
--
------------------------------------------------------------------------------
with Ada.Command_Line;
with Ada.Containers.Vectors;
with Ada.Directories;
with GNAT.Regexp;
with GNATCOLL.JSON;
with GNATCOLL.Projects;
with GNATCOLL.VFS;
with SPAT.Command_Line;
with SPAT.GPR_Support;
with SPAT.Log;
with SPAT.Spark_Files;
with SPAT.Spark_Info;
with SPAT.Stop_Watch;
with SPAT.Strings;
with SPAT.Version;
with System;
------------------------------------------------------------------------------
-- Run_SPAT
------------------------------------------------------------------------------
procedure Run_SPAT is
package Reg_Exp_List is new
Ada.Containers.Vectors (Index_Type => Positive,
Element_Type => GNAT.Regexp.Regexp,
"=" => GNAT.Regexp."=");
---------------------------------------------------------------------------
-- Print_Entities
---------------------------------------------------------------------------
procedure Print_Entities
(Info : in SPAT.Spark_Info.T;
Sort_By : in SPAT.Spark_Info.Sorting_Criterion;
Cut_Off : in Duration;
Entity_Filter : in Reg_Exp_List.Vector);
---------------------------------------------------------------------------
-- Print_Suggestion
---------------------------------------------------------------------------
procedure Print_Suggestion
(Info : in SPAT.Spark_Info.T;
File_Map : in SPAT.GPR_Support.SPARK_Source_Maps.Map);
---------------------------------------------------------------------------
-- Print_Summary
---------------------------------------------------------------------------
procedure Print_Summary (Info : in SPAT.Spark_Info.T;
Sort_By : in SPAT.Spark_Info.Sorting_Criterion;
Cut_Off : in Duration);
---------------------------------------------------------------------------
-- Print_Entities
---------------------------------------------------------------------------
procedure Print_Entities
(Info : in SPAT.Spark_Info.T;
Sort_By : in SPAT.Spark_Info.Sorting_Criterion;
Cut_Off : in Duration;
Entity_Filter : in Reg_Exp_List.Vector) is separate;
---------------------------------------------------------------------------
-- Print_Suggestion
---------------------------------------------------------------------------
procedure Print_Suggestion
(Info : in SPAT.Spark_Info.T;
File_Map : in SPAT.GPR_Support.SPARK_Source_Maps.Map) is separate;
---------------------------------------------------------------------------
-- Print_Summary
---------------------------------------------------------------------------
procedure Print_Summary (Info : in SPAT.Spark_Info.T;
Sort_By : in SPAT.Spark_Info.Sorting_Criterion;
Cut_Off : in Duration) is separate;
use type SPAT.Subject_Name;
Entity_Filter : Reg_Exp_List.Vector;
begin
if not SPAT.Command_Line.Parser.Parse then
SPAT.Spark_Files.Shutdown;
Ada.Command_Line.Set_Exit_Status (Code => Ada.Command_Line.Failure);
return;
end if;
if SPAT.Command_Line.Version.Get then
SPAT.Log.Message
(Message =>
"run_spat V" & SPAT.Version.Number &
" (compiled by " & System.System_Name'Image & " " &
SPAT.Version.Compiler & ")");
SPAT.Spark_Files.Shutdown;
Ada.Command_Line.Set_Exit_Status (Code => Ada.Command_Line.Success);
return;
end if;
if SPAT.Command_Line.Project.Get = SPAT.Null_Name then
-- The project file option is mandatory (AFAICS there is no way to
-- require an option argument).
SPAT.Log.Message
(Message => "Argument parsing failed: Missing project file argument");
SPAT.Log.Message (Message => SPAT.Command_Line.Parser.Help);
SPAT.Spark_Files.Shutdown;
Ada.Command_Line.Set_Exit_Status (Code => Ada.Command_Line.Failure);
return;
end if;
-- If there were entity filter options given, try compiling the reg exps.
--
-- for Expression of SPAT.Command_Line.Entity_Filter.Get loop
-- The above triggers a GNAT bug box with GNAT CE 2020.
--
declare
Filter : constant SPAT.Command_Line.Entity_Filter.Result_Array
:= SPAT.Command_Line.Entity_Filter.Get;
begin
for Expression of Filter loop
begin
Entity_Filter.Append
(New_Item =>
GNAT.Regexp.Compile
(Pattern => SPAT.To_String (Expression),
Glob => False,
Case_Sensitive => False));
null;
exception
when GNAT.Regexp.Error_In_Regexp =>
SPAT.Log.Message
(Message =>
"Argument parsing failed: """ &
SPAT.To_String (Source => Expression) &
""" is not a valid regular expression.");
SPAT.Spark_Files.Shutdown;
Ada.Command_Line.Set_Exit_Status
(Code => Ada.Command_Line.Failure);
return;
end;
end loop;
end;
Do_Run_SPAT :
declare
SPARK_Files : SPAT.Spark_Files.T;
Timer : SPAT.Stop_Watch.T := SPAT.Stop_Watch.Create;
Sort_By : constant SPAT.Spark_Info.Sorting_Criterion :=
SPAT.Command_Line.Sort_By.Get;
Cut_Off : constant Duration := SPAT.Command_Line.Cut_Off.Get;
Report_Mode : constant SPAT.Command_Line.Report_Mode :=
SPAT.Command_Line.Report.Get;
Project_File : constant GNATCOLL.VFS.Filesystem_String :=
GNATCOLL.VFS."+" (S => SPAT.To_String (SPAT.Command_Line.Project.Get));
File_List : constant SPAT.GPR_Support.SPARK_Source_Maps.Map :=
SPAT.GPR_Support.Get_SPARK_Files (GPR_File => Project_File);
use type SPAT.Command_Line.Report_Mode;
begin
Collect_And_Parse :
begin
-- Step 2: Parse the files into JSON values.
if not File_List.Is_Empty then
SPAT.Log.Debug
(Message =>
"Using up to" & SPAT.Spark_Files.Num_Workers'Image &
" parsing threads.");
Timer.Start;
declare
File_Names : SPAT.Strings.SPARK_File_Names (Capacity => File_List.Length);
begin
for X in File_List.Iterate loop
File_Names.Append (SPAT.GPR_Support.SPARK_Source_Maps.Key (X));
end loop;
SPARK_Files.Read (Names => File_Names);
end;
SPAT.Log.Debug
(Message => "Parsing completed in " & Timer.Elapsed & ".");
end if;
end Collect_And_Parse;
Process_And_Output :
declare
Info : SPAT.Spark_Info.T;
begin
-- Step 3: Process the JSON data.
if not SPARK_Files.Is_Empty then
Timer.Start;
for C in SPARK_Files.Iterate loop
Parse_JSON_File :
declare
Read_Result : constant GNATCOLL.JSON.Read_Result :=
SPARK_Files (C);
File : constant SPAT.SPARK_File_Name :=
SPAT.Spark_Files.Key (C);
begin
if Read_Result.Success then
Info.Map_Spark_File (Root => Read_Result.Value,
File => File);
else
SPAT.Log.Warning
(Message =>
SPAT.To_String (Source => File) & ": " &
GNATCOLL.JSON.Format_Parsing_Error
(Error => Read_Result.Error));
end if;
end Parse_JSON_File;
end loop;
SPAT.Log.Debug
(Message => "Reading completed in " & Timer.Elapsed & ".");
end if;
SPAT.Log.Debug
(Message =>
"Collecting files completed in " & Timer.Elapsed_Total & ".");
SPAT.Log.Debug
(Message => "Cut off point set to " & SPAT.Image (Cut_Off) & ".");
-- Step 4: Output the JSON data.
if SPAT.Command_Line.Summary.Get then
Print_Summary (Info => Info,
Sort_By => Sort_By,
Cut_Off => Cut_Off);
end if;
if Report_Mode /= SPAT.Command_Line.None then
Print_Entities (Info => Info,
Sort_By => Sort_By,
Cut_Off => Cut_Off,
Entity_Filter => Entity_Filter);
end if;
if SPAT.Command_Line.Suggest.Get then
Print_Suggestion (Info => Info,
File_Map => File_List);
end if;
exception
when E : others =>
SPAT.Log.Dump_Exception
(E => E,
Message => "Internal error encountered when processing data!");
end Process_And_Output;
end Do_Run_SPAT;
SPAT.Spark_Files.Shutdown;
Ada.Command_Line.Set_Exit_Status (Code => Ada.Command_Line.Success);
exception
when E : others =>
SPAT.Spark_Files.Shutdown;
-- This shouldn't happen, other exception handlers should have caught
-- such earlier.
SPAT.Log.Dump_Exception
(E => E,
Message => "Fatal error encountered in SPAT!");
Ada.Command_Line.Set_Exit_Status (Code => Ada.Command_Line.Failure);
end Run_SPAT;
|