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-2015, 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 32with Types; use Types; 33with GNAT.Table; 34 35package 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 Frame_Condition_Mode is True. 60 61 -- The SPARK cross-reference information comes after the shared 62 -- cross-reference information, so it needs not be read 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 declaration/body. Note that 71 -- a package declaration and body define two different scopes. Similarly, a 72 -- subprogram declaration and body, when both present, define two different 73 -- 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 identity a file in FD lines 137 138 -- entity-number and identity identify a scope entity in FS lines for 139 -- the file previously identified. 140 141 -- F line typ col entity ref* 142 143 -- line is the line number of the referenced entity 144 145 -- typ is the type of the referenced entity, using a code similar to 146 -- the one used for cross-references: 147 148 -- > = IN parameter 149 -- < = OUT parameter 150 -- = = IN OUT parameter 151 -- * = all other cases 152 153 -- col is the column number of the referenced entity 154 155 -- entity is the name of the referenced entity as written in the source 156 -- file where it is defined. 157 158 -- There may be zero or more ref entries on each line 159 160 -- (file |)? ((. scope :)? line type col)* 161 162 -- file is the dependency number of the file with the reference. It and 163 -- the following vertical bar are omitted if the file is the same as 164 -- the previous ref, and the refs for the current file are first (and 165 -- do not need a bar). 166 167 -- scope is the scope number of the scope with the reference. It and 168 -- the following colon are omitted if the scope is the same as the 169 -- previous ref, and the refs for the current scope are first (and do 170 -- not need a colon). 171 172 -- line is the line number of the reference 173 174 -- col is the column number of the reference 175 176 -- type is one of the following, using the same code as in 177 -- cross-references: 178 179 -- m = modification 180 -- r = reference 181 -- c = reference to constant object 182 -- s = subprogram reference in a static call 183 184 -- Special entries for reads and writes to memory reference a special 185 -- variable called "__HEAP". These special entries are present in every 186 -- scope where reads and writes to memory are present. Line and column for 187 -- this special variable are always 0. 188 189 -- Examples: ??? add examples here 190 191 -- ------------------------------- 192 -- -- Generated Globals Section -- 193 -- ------------------------------- 194 195 -- The Generated Globals section is located at the end of the ALI file. 196 197 -- All lines introducing information related to the Generated Globals 198 -- have the string "GG" appearing in the beginning. This string ("GG") 199 -- should therefore not be used in the beginning of any line that does 200 -- not relate to Generated Globals. 201 202 -- The processing (reading and writing) of this section happens in 203 -- package Flow_Computed_Globals (from the SPARK 2014 sources), for 204 -- further information please refer there. 205 206 ---------------- 207 -- Xref Table -- 208 ---------------- 209 210 -- The following table records SPARK cross-references 211 212 type Xref_Index is new Int; 213 -- Used to index values in this table. Values start at 1 and are assigned 214 -- sequentially as entries are constructed. 215 216 type SPARK_Xref_Record is record 217 Entity_Name : String_Ptr; 218 -- Pointer to entity name in ALI file 219 220 Entity_Line : Nat; 221 -- Line number for the entity referenced 222 223 Etype : Character; 224 -- Indicates type of entity, using code used in ALI file: 225 -- > = IN parameter 226 -- < = OUT parameter 227 -- = = IN OUT parameter 228 -- * = all other cases 229 230 Entity_Col : Nat; 231 -- Column number for the entity referenced 232 233 File_Num : Nat; 234 -- Set to the file dependency number for the cross-reference. Note 235 -- that if no file entry is present explicitly, this is just a copy 236 -- of the reference for the current cross-reference section. 237 238 Scope_Num : Nat; 239 -- Set to the scope number for the cross-reference. Note that if no 240 -- scope entry is present explicitly, this is just a copy of the 241 -- reference for the current cross-reference section. 242 243 Line : Nat; 244 -- Line number for the reference 245 246 Rtype : Character; 247 -- Indicates type of reference, using code used in ALI file: 248 -- r = reference 249 -- c = reference to constant object 250 -- m = modification 251 -- s = call 252 253 Col : Nat; 254 -- Column number for the reference 255 end record; 256 257 package SPARK_Xref_Table is new GNAT.Table ( 258 Table_Component_Type => SPARK_Xref_Record, 259 Table_Index_Type => Xref_Index, 260 Table_Low_Bound => 1, 261 Table_Initial => 2000, 262 Table_Increment => 300); 263 264 ----------------- 265 -- Scope Table -- 266 ----------------- 267 268 -- This table keeps track of the scopes and the corresponding starting and 269 -- ending indexes (From, To) in the Xref table. 270 271 type Scope_Index is new Int; 272 -- Used to index values in this table. Values start at 1 and are assigned 273 -- sequentially as entries are constructed. 274 275 type SPARK_Scope_Record is record 276 Scope_Name : String_Ptr; 277 -- Pointer to scope name in ALI file 278 279 File_Num : Nat; 280 -- Set to the file dependency number for the scope 281 282 Scope_Num : Nat; 283 -- Set to the scope number for the scope 284 285 Spec_File_Num : Nat; 286 -- Set to the file dependency number for the scope corresponding to the 287 -- spec of the current scope entity, if different, or else 0. 288 289 Spec_Scope_Num : Nat; 290 -- Set to the scope number for the scope corresponding to the spec of 291 -- the current scope entity, if different, or else 0. 292 293 Line : Nat; 294 -- Line number for the scope 295 296 Stype : Character; 297 -- Indicates type of scope, using code used in ALI file: 298 -- K = package 299 -- V = function 300 -- U = procedure 301 302 Col : Nat; 303 -- Column number for the scope 304 305 From_Xref : Xref_Index; 306 -- Starting index in Xref table for this scope 307 308 To_Xref : Xref_Index; 309 -- Ending index in Xref table for this scope 310 311 -- The following component is only used in-memory, not printed out in 312 -- ALI file. 313 314 Scope_Entity : Entity_Id := Empty; 315 -- Entity (subprogram or package) for the scope 316 end record; 317 318 package SPARK_Scope_Table is new GNAT.Table ( 319 Table_Component_Type => SPARK_Scope_Record, 320 Table_Index_Type => Scope_Index, 321 Table_Low_Bound => 1, 322 Table_Initial => 200, 323 Table_Increment => 300); 324 325 ---------------- 326 -- File Table -- 327 ---------------- 328 329 -- This table keeps track of the units and the corresponding starting and 330 -- ending indexes (From, To) in the Scope table. 331 332 type File_Index is new Int; 333 -- Used to index values in this table. Values start at 1 and are assigned 334 -- sequentially as entries are constructed. 335 336 type SPARK_File_Record is record 337 File_Name : String_Ptr; 338 -- Pointer to file name in ALI file 339 340 Unit_File_Name : String_Ptr; 341 -- Pointer to file name for unit in ALI file, when File_Name refers to a 342 -- subunit. Otherwise null. 343 344 File_Num : Nat; 345 -- Dependency number in ALI file 346 347 From_Scope : Scope_Index; 348 -- Starting index in Scope table for this unit 349 350 To_Scope : Scope_Index; 351 -- Ending index in Scope table for this unit 352 end record; 353 354 package SPARK_File_Table is new GNAT.Table ( 355 Table_Component_Type => SPARK_File_Record, 356 Table_Index_Type => File_Index, 357 Table_Low_Bound => 1, 358 Table_Initial => 20, 359 Table_Increment => 200); 360 361 --------------- 362 -- Constants -- 363 --------------- 364 365 Name_Of_Heap_Variable : constant String := "__HEAP"; 366 -- Name of special variable used in effects to denote reads and writes 367 -- through explicit dereference. 368 369 ----------------- 370 -- Subprograms -- 371 ----------------- 372 373 procedure Initialize_SPARK_Tables; 374 -- Reset tables for a new compilation 375 376 procedure dspark; 377 -- Debug routine to dump internal SPARK cross-reference tables. This is a 378 -- raw format dump showing exactly what the tables contain. 379 380 procedure pspark; 381 -- Debugging procedure to output contents of SPARK cross-reference binary 382 -- tables in the format in which they appear in an ALI file. 383 384end SPARK_Xrefs; 385