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