gcc/ada/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-reference information before writing it to the ALI
  29 --  file, and by Get_SPARK_Xrefs/Put_SPARK_Xrefs to read/write the textual
  30 --  representation that is stored 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 global
 132    --  variables read/written in each subprogram/package/protected_type/
 133    --  task_type.
 134
 135    --    FX dependency-number filename . entity-number entity
 136
 137    --      dependency-number and filename identify a file in FD lines
 138
 139    --      entity-number and entity identify a scope in FS lines
 140    --      for the previously identified file.
 141
 142    --      (filename and entity are just a textual representations of
 143    --       dependency-number and entity-number)
 144
 145    --    F line typ col entity ref*
 146
 147    --      line is the line number of the referenced entity
 148
 149    --      typ is the type of the referenced entity, using a code similar to
 150    --      the one used for cross-references:
 151
 152    --        > = IN parameter
 153    --        < = OUT parameter
 154    --        = = IN OUT parameter
 155    --        * = all other cases
 156
 157    --      col is the column number of the referenced entity
 158
 159    --      entity is the name of the referenced entity as written in the source
 160    --      file where it is defined.
 161
 162    --  There may be zero or more ref entries on each line
 163
 164    --    (file |)? ((. scope :)? line type col)*
 165
 166    --      file is the dependency number of the file with the reference. It and
 167    --      the following vertical bar are omitted if the file is the same as
 168    --      the previous ref, and the refs for the current file are first (and
 169    --      do not need a bar).
 170
 171    --      scope is the scope number of the scope with the reference. It and
 172    --      the following colon are omitted if the scope is the same as the
 173    --      previous ref, and the refs for the current scope are first (and do
 174    --      not need a colon).
 175
 176    --      line is the line number of the reference
 177
 178    --      col is the column number of the reference
 179
 180    --      type is one of the following, using the same code as in
 181    --      cross-references:
 182
 183    --        m = modification
 184    --        r = reference
 185    --        c = reference to constant object
 186    --        s = subprogram reference in a static call
 187
 188    --  Special entries for reads and writes to memory reference a special
 189    --  variable called "__HEAP". These special entries are present in every
 190    --  scope where reads and writes to memory are present. Line and column for
 191    --  this special variable are always 0.
 192
 193    --    Examples: ??? add examples here
 194
 195    --  -------------------------------
 196    --  -- Generated Globals Section --
 197    --  -------------------------------
 198
 199    --  The Generated Globals section is located at the end of the ALI file
 200
 201    --  All lines with information related to the Generated Globals begin with
 202    --  string "GG". This string should therefore not be used in the beginning
 203    --  of any line not related to Generated Globals.
 204
 205    --  The processing (reading and writing) of this section happens in package
 206    --  Flow_Generated_Globals (from the SPARK 2014 sources), for further
 207    --  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       --  File dependency number for the cross-reference. Note that if no file
 239       --  entry is present explicitly, this is just a copy of the reference for
 240       --  the current cross-reference section.
 241
 242       Scope_Num : Nat;
 243       --  Scope number for the cross-reference. Note that if no scope entry is
 244       --  present explicitly, this is just a copy of the reference for the
 245       --  current cross-reference section.
 246
 247       Line : Nat;
 248       --  Line number for the reference
 249
 250       Rtype : Character;
 251       --  Indicates type of the 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;