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-2013, 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 -- Xref Table -- 192 ---------------- 193 194 -- The following table records SPARK cross-references 195 196 type Xref_Index is new Int; 197 -- Used to index values in this table. Values start at 1 and are assigned 198 -- sequentially as entries are constructed. 199 200 type SPARK_Xref_Record is record 201 Entity_Name : String_Ptr; 202 -- Pointer to entity name in ALI file 203 204 Entity_Line : Nat; 205 -- Line number for the entity referenced 206 207 Etype : Character; 208 -- Indicates type of entity, using code used in ALI file: 209 -- > = IN parameter 210 -- < = OUT parameter 211 -- = = IN OUT parameter 212 -- * = all other cases 213 214 Entity_Col : Nat; 215 -- Column number for the entity referenced 216 217 File_Num : Nat; 218 -- Set to the file dependency number for the cross-reference. Note 219 -- that if no file entry is present explicitly, this is just a copy 220 -- of the reference for the current cross-reference section. 221 222 Scope_Num : Nat; 223 -- Set to the scope number for the cross-reference. Note that if no 224 -- scope entry is present explicitly, this is just a copy of the 225 -- reference for the current cross-reference section. 226 227 Line : Nat; 228 -- Line number for the reference 229 230 Rtype : Character; 231 -- Indicates type of reference, using code used in ALI file: 232 -- r = reference 233 -- c = reference to constant object 234 -- m = modification 235 -- s = call 236 237 Col : Nat; 238 -- Column number for the reference 239 end record; 240 241 package SPARK_Xref_Table is new GNAT.Table ( 242 Table_Component_Type => SPARK_Xref_Record, 243 Table_Index_Type => Xref_Index, 244 Table_Low_Bound => 1, 245 Table_Initial => 2000, 246 Table_Increment => 300); 247 248 ----------------- 249 -- Scope Table -- 250 ----------------- 251 252 -- This table keeps track of the scopes and the corresponding starting and 253 -- ending indexes (From, To) in the Xref table. 254 255 type Scope_Index is new Int; 256 -- Used to index values in this table. Values start at 1 and are assigned 257 -- sequentially as entries are constructed. 258 259 type SPARK_Scope_Record is record 260 Scope_Name : String_Ptr; 261 -- Pointer to scope name in ALI file 262 263 File_Num : Nat; 264 -- Set to the file dependency number for the scope 265 266 Scope_Num : Nat; 267 -- Set to the scope number for the scope 268 269 Spec_File_Num : Nat; 270 -- Set to the file dependency number for the scope corresponding to the 271 -- spec of the current scope entity, if different, or else 0. 272 273 Spec_Scope_Num : Nat; 274 -- Set to the scope number for the scope corresponding to the spec of 275 -- the current scope entity, if different, or else 0. 276 277 Line : Nat; 278 -- Line number for the scope 279 280 Stype : Character; 281 -- Indicates type of scope, using code used in ALI file: 282 -- K = package 283 -- V = function 284 -- U = procedure 285 286 Col : Nat; 287 -- Column number for the scope 288 289 From_Xref : Xref_Index; 290 -- Starting index in Xref table for this scope 291 292 To_Xref : Xref_Index; 293 -- Ending index in Xref table for this scope 294 295 -- The following component is only used in-memory, not printed out in 296 -- ALI file. 297 298 Scope_Entity : Entity_Id := Empty; 299 -- Entity (subprogram or package) for the scope 300 end record; 301 302 package SPARK_Scope_Table is new GNAT.Table ( 303 Table_Component_Type => SPARK_Scope_Record, 304 Table_Index_Type => Scope_Index, 305 Table_Low_Bound => 1, 306 Table_Initial => 200, 307 Table_Increment => 300); 308 309 ---------------- 310 -- File Table -- 311 ---------------- 312 313 -- This table keeps track of the units and the corresponding starting and 314 -- ending indexes (From, To) in the Scope table. 315 316 type File_Index is new Int; 317 -- Used to index values in this table. Values start at 1 and are assigned 318 -- sequentially as entries are constructed. 319 320 type SPARK_File_Record is record 321 File_Name : String_Ptr; 322 -- Pointer to file name in ALI file 323 324 Unit_File_Name : String_Ptr; 325 -- Pointer to file name for unit in ALI file, when File_Name refers to a 326 -- subunit. Otherwise null. 327 328 File_Num : Nat; 329 -- Dependency number in ALI file 330 331 From_Scope : Scope_Index; 332 -- Starting index in Scope table for this unit 333 334 To_Scope : Scope_Index; 335 -- Ending index in Scope table for this unit 336 end record; 337 338 package SPARK_File_Table is new GNAT.Table ( 339 Table_Component_Type => SPARK_File_Record, 340 Table_Index_Type => File_Index, 341 Table_Low_Bound => 1, 342 Table_Initial => 20, 343 Table_Increment => 200); 344 345 --------------- 346 -- Constants -- 347 --------------- 348 349 Name_Of_Heap_Variable : constant String := "__HEAP"; 350 -- Name of special variable used in effects to denote reads and writes 351 -- through explicit dereference. 352 353 ----------------- 354 -- Subprograms -- 355 ----------------- 356 357 procedure Initialize_SPARK_Tables; 358 -- Reset tables for a new compilation 359 360 procedure dspark; 361 -- Debug routine to dump internal SPARK cross-reference tables. This is a 362 -- raw format dump showing exactly what the tables contain. 363 364 procedure pspark; 365 -- Debugging procedure to output contents of SPARK cross-reference binary 366 -- tables in the format in which they appear in an ALI file. 367 368end SPARK_Xrefs; 369