File : spark_xrefs.ads
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT COMPILER COMPONENTS --
4 -- --
5 -- S P A R K _ X R E F S --
6 -- --
7 -- S p e c --
8 -- --
9 -- Copyright (C) 2011-2016, Free Software Foundation, Inc. --
10 -- --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License --
17 -- for more details. You should have received a copy of the GNU General --
18 -- Public License distributed with GNAT; see file COPYING3. If not, go to --
19 -- http://www.gnu.org/licenses for a complete copy of the license. --
20 -- --
21 -- GNAT was originally developed by the GNAT team at New York University. --
22 -- Extensive contributions were provided by Ada Core Technologies Inc. --
23 -- --
24 ------------------------------------------------------------------------------
25
26 -- This package defines tables used to store information needed for the SPARK
27 -- mode. It is used by procedures in Lib.Xref.SPARK_Specific to build the
28 -- SPARK specific cross-references information before writing it out to the
29 -- ALI file, and by Get_SPARK_Xrefs/Put_SPARK_Xrefs to read and write the text
30 -- form that is used in the ALI file.
31
32 with Types; use Types;
33 with GNAT.Table;
34
35 package SPARK_Xrefs is
36
37 -- SPARK cross-reference information can exist in one of two forms. In
38 -- the ALI file, it is represented using a text format that is described
39 -- in this specification. Internally it is stored using three tables:
40 -- SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which are
41 -- also defined in this unit.
42
43 -- Lib.Xref.SPARK_Specific is part of the compiler. It extracts SPARK
44 -- cross-reference information from the complete set of cross-references
45 -- generated during compilation.
46
47 -- Get_SPARK_Xrefs reads the text lines in ALI format and populates the
48 -- internal tables with corresponding information.
49
50 -- Put_SPARK_Xrefs reads the internal tables and generates text lines in
51 -- the ALI format.
52
53 ----------------------------
54 -- SPARK Xrefs ALI Format --
55 ----------------------------
56
57 -- SPARK cross-reference information is generated on a unit-by-unit basis
58 -- in the ALI file, using lines that start with the identifying character F
59 -- ("Formal"). These lines are generated if GNATprove_Mode is True.
60
61 -- The SPARK cross-reference information comes after the shared
62 -- cross-reference information, so it can be ignored by tools like
63 -- gnatbind, gnatmake, etc.
64
65 -- -------------------
66 -- -- Scope Section --
67 -- -------------------
68
69 -- A first section defines the scopes in which entities are defined and
70 -- referenced. A scope is a package/subprogram/protected_type/task_type
71 -- declaration/body. Note that a package declaration and body define two
72 -- different scopes. Similarly, a subprogram, protected type and task type
73 -- declaration and body, when both present, define two different scopes.
74
75 -- FD dependency-number filename (-> unit-filename)?
76
77 -- This header precedes scope information for the unit identified by
78 -- dependency number and file name. The dependency number is the index
79 -- into the generated D lines and is ones-origin (e.g. 2 = reference to
80 -- second generated D line).
81
82 -- The list of FD lines should match the list of D lines defined in the
83 -- ALI file, in the same order.
84
85 -- Note that the filename here will reflect the original name if a
86 -- Source_Reference pragma was encountered (since all line number
87 -- references will be with respect to the original file).
88
89 -- Note: the filename is redundant in that it could be deduced from the
90 -- corresponding D line, but it is convenient at least for human
91 -- reading of the SPARK cross-reference information, and means that
92 -- the SPARK cross-reference information can stand on its own without
93 -- needing other parts of the ALI file.
94
95 -- The optional unit filename is given only for subunits.
96
97 -- FS . scope line type col entity (-> spec-file . spec-scope)?
98
99 -- (The ? mark stands for an optional entry in the syntax)
100
101 -- scope is the ones-origin scope number for the current file (e.g. 2 =
102 -- reference to the second FS line in this FD block).
103
104 -- line is the line number of the scope entity. The name of the entity
105 -- starts in column col. Columns are numbered from one, and if
106 -- horizontal tab characters are present, the column number is computed
107 -- assuming standard 1,9,17,.. tab stops. For example, if the entity is
108 -- the first token on the line, and is preceded by space-HT-space, then
109 -- the column would be column 10.
110
111 -- type is a single letter identifying the type of the entity, using
112 -- the same code as in cross-references:
113
114 -- K = package (k = generic package)
115 -- V = function (v = generic function)
116 -- U = procedure (u = generic procedure)
117 -- Y = entry
118
119 -- col is the column number of the scope entity
120
121 -- entity is the name of the scope entity, with casing in the canonical
122 -- casing for the source file where it is defined.
123
124 -- spec-file and spec-scope are respectively the file and scope for the
125 -- spec corresponding to the current body scope, when they differ.
126
127 -- ------------------
128 -- -- Xref Section --
129 -- ------------------
130
131 -- A second section defines cross-references useful for computing the set
132 -- of global variables read/written in each subprogram/package.
133
134 -- FX dependency-number filename . entity-number entity
135
136 -- dependency-number and filename identify a file in FD lines
137
138 -- entity-number and entity identify a scope in FS lines
139 -- for the file previously identified file.
140
141 -- (filename and entity are just a textual representations of
142 -- dependency-number and entity-number)
143
144 -- F line typ col entity ref*
145
146 -- line is the line number of the referenced entity
147
148 -- typ is the type of the referenced entity, using a code similar to
149 -- the one used for cross-references:
150
151 -- > = IN parameter
152 -- < = OUT parameter
153 -- = = IN OUT parameter
154 -- * = all other cases
155
156 -- col is the column number of the referenced entity
157
158 -- entity is the name of the referenced entity as written in the source
159 -- file where it is defined.
160
161 -- There may be zero or more ref entries on each line
162
163 -- (file |)? ((. scope :)? line type col)*
164
165 -- file is the dependency number of the file with the reference. It and
166 -- the following vertical bar are omitted if the file is the same as
167 -- the previous ref, and the refs for the current file are first (and
168 -- do not need a bar).
169
170 -- scope is the scope number of the scope with the reference. It and
171 -- the following colon are omitted if the scope is the same as the
172 -- previous ref, and the refs for the current scope are first (and do
173 -- not need a colon).
174
175 -- line is the line number of the reference
176
177 -- col is the column number of the reference
178
179 -- type is one of the following, using the same code as in
180 -- cross-references:
181
182 -- m = modification
183 -- r = reference
184 -- c = reference to constant object
185 -- s = subprogram reference in a static call
186
187 -- Special entries for reads and writes to memory reference a special
188 -- variable called "__HEAP". These special entries are present in every
189 -- scope where reads and writes to memory are present. Line and column for
190 -- this special variable are always 0.
191
192 -- Examples: ??? add examples here
193
194 -- -------------------------------
195 -- -- Generated Globals Section --
196 -- -------------------------------
197
198 -- The Generated Globals section is located at the end of the ALI file
199
200 -- All lines introducing information related to the Generated Globals
201 -- have the string "GG" appearing in the beginning. This string ("GG")
202 -- should therefore not be used in the beginning of any line that does
203 -- not relate to Generated Globals.
204
205 -- The processing (reading and writing) of this section happens in
206 -- package Flow_Generated_Globals (from the SPARK 2014 sources), for
207 -- further information please refer there.
208
209 ----------------
210 -- Xref Table --
211 ----------------
212
213 -- The following table records SPARK cross-references
214
215 type Xref_Index is new Nat;
216 -- Used to index values in this table. Values start at 1 and are assigned
217 -- sequentially as entries are constructed; value 0 is used temporarily
218 -- until a proper value is determined.
219
220 type SPARK_Xref_Record is record
221 Entity_Name : String_Ptr;
222 -- Pointer to entity name in ALI file
223
224 Entity_Line : Nat;
225 -- Line number for the entity referenced
226
227 Etype : Character;
228 -- Indicates type of entity, using code used in ALI file:
229 -- > = IN parameter
230 -- < = OUT parameter
231 -- = = IN OUT parameter
232 -- * = all other cases
233
234 Entity_Col : Nat;
235 -- Column number for the entity referenced
236
237 File_Num : Nat;
238 -- Set to the file dependency number for the cross-reference. Note
239 -- that if no file entry is present explicitly, this is just a copy
240 -- of the reference for the current cross-reference section.
241
242 Scope_Num : Nat;
243 -- Set to the scope number for the cross-reference. Note that if no
244 -- scope entry is present explicitly, this is just a copy of the
245 -- reference for the current cross-reference section.
246
247 Line : Nat;
248 -- Line number for the reference
249
250 Rtype : Character;
251 -- Indicates type of reference, using code used in ALI file:
252 -- r = reference
253 -- c = reference to constant object
254 -- m = modification
255 -- s = call
256
257 Col : Nat;
258 -- Column number for the reference
259 end record;
260
261 package SPARK_Xref_Table is new GNAT.Table (
262 Table_Component_Type => SPARK_Xref_Record,
263 Table_Index_Type => Xref_Index,
264 Table_Low_Bound => 1,
265 Table_Initial => 2000,
266 Table_Increment => 300);
267
268 -----------------
269 -- Scope Table --
270 -----------------
271
272 -- This table keeps track of the scopes and the corresponding starting and
273 -- ending indexes (From, To) in the Xref table.
274
275 type Scope_Index is new Nat;
276 -- Used to index values in this table. Values start at 1 and are assigned
277 -- sequentially as entries are constructed; value 0 indicates that no
278 -- entries have been constructed and is also used until a proper value is
279 -- determined.
280
281 type SPARK_Scope_Record is record
282 Scope_Name : String_Ptr;
283 -- Pointer to scope name in ALI file
284
285 File_Num : Nat;
286 -- Set to the file dependency number for the scope
287
288 Scope_Num : Pos;
289 -- Set to the scope number for the scope
290
291 Spec_File_Num : Nat;
292 -- Set to the file dependency number for the scope corresponding to the
293 -- spec of the current scope entity, if different, or else 0.
294
295 Spec_Scope_Num : Nat;
296 -- Set to the scope number for the scope corresponding to the spec of
297 -- the current scope entity, if different, or else 0.
298
299 Line : Nat;
300 -- Line number for the scope
301
302 Stype : Character;
303 -- Indicates type of scope, using code used in ALI file:
304 -- K = package
305 -- T = task
306 -- U = procedure
307 -- V = function
308 -- Y = entry
309
310 Col : Nat;
311 -- Column number for the scope
312
313 From_Xref : Xref_Index;
314 -- Starting index in Xref table for this scope
315
316 To_Xref : Xref_Index;
317 -- Ending index in Xref table for this scope
318
319 -- The following component is only used in-memory, not printed out in
320 -- ALI file.
321
322 Scope_Entity : Entity_Id := Empty;
323 -- Entity (subprogram or package) for the scope
324 end record;
325
326 package SPARK_Scope_Table is new GNAT.Table (
327 Table_Component_Type => SPARK_Scope_Record,
328 Table_Index_Type => Scope_Index,
329 Table_Low_Bound => 1,
330 Table_Initial => 200,
331 Table_Increment => 300);
332
333 ----------------
334 -- File Table --
335 ----------------
336
337 -- This table keeps track of the units and the corresponding starting and
338 -- ending indexes (From, To) in the Scope table.
339
340 type File_Index is new Nat;
341 -- Used to index values in this table. Values start at 1 and are assigned
342 -- sequentially as entries are constructed; value 0 indicates that no
343 -- entries have been constructed.
344
345 type SPARK_File_Record is record
346 File_Name : String_Ptr;
347 -- Pointer to file name in ALI file
348
349 Unit_File_Name : String_Ptr;
350 -- Pointer to file name for unit in ALI file, when File_Name refers to a
351 -- subunit. Otherwise null.
352
353 File_Num : Nat;
354 -- Dependency number in ALI file
355
356 From_Scope : Scope_Index;
357 -- Starting index in Scope table for this unit
358
359 To_Scope : Scope_Index;
360 -- Ending index in Scope table for this unit
361 end record;
362
363 package SPARK_File_Table is new GNAT.Table (
364 Table_Component_Type => SPARK_File_Record,
365 Table_Index_Type => File_Index,
366 Table_Low_Bound => 1,
367 Table_Initial => 20,
368 Table_Increment => 200);
369
370 ---------------
371 -- Constants --
372 ---------------
373
374 Name_Of_Heap_Variable : constant String := "__HEAP";
375 -- Name of special variable used in effects to denote reads and writes
376 -- through explicit dereference.
377
378 -----------------
379 -- Subprograms --
380 -----------------
381
382 procedure Initialize_SPARK_Tables;
383 -- Reset tables for a new compilation
384
385 procedure dspark;
386 -- Debug routine to dump internal SPARK cross-reference tables. This is a
387 -- raw format dump showing exactly what the tables contain.
388
389 procedure pspark;
390 -- Debugging procedure to output contents of SPARK cross-reference binary
391 -- tables in the format in which they appear in an ALI file.
392
393 end SPARK_Xrefs;