------------------------------------------------------------------------------ -- -- -- GNAT COMPILER COMPONENTS -- -- -- -- S P A R K _ X R E F S -- -- -- -- S p e c -- -- -- -- Copyright (C) 2011-2014, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- -- ware Foundation; either version 3, or (at your option) any later ver- -- -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- -- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- -- for more details. You should have received a copy of the GNU General -- -- Public License distributed with GNAT; see file COPYING3. If not, go to -- -- http://www.gnu.org/licenses for a complete copy of the license. -- -- -- -- GNAT was originally developed by the GNAT team at New York University. -- -- Extensive contributions were provided by Ada Core Technologies Inc. -- -- -- ------------------------------------------------------------------------------ -- This package defines tables used to store information needed for the SPARK -- mode. It is used by procedures in Lib.Xref.SPARK_Specific to build the -- SPARK specific cross-references information before writing it out to the -- ALI file, and by Get_SPARK_Xrefs/Put_SPARK_Xrefs to read and write the text -- form that is used in the ALI file. with Types; use Types; with GNAT.Table; package SPARK_Xrefs is -- SPARK cross-reference information can exist in one of two forms. In the -- ALI file, it is represented using a text format that is described in -- this specification. Internally it is stored using three tables -- SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which are also -- defined in this unit. -- Lib.Xref.SPARK_Specific is part of the compiler. It extracts SPARK -- cross-reference information from the complete set of cross-references -- generated during compilation. -- Get_SPARK_Xrefs reads the text lines in ALI format and populates the -- internal tables with corresponding information. -- Put_SPARK_Xrefs reads the internal tables and generates text lines in -- the ALI format. ---------------------------- -- SPARK Xrefs ALI Format -- ---------------------------- -- SPARK cross-reference information is generated on a unit-by-unit basis -- in the ALI file, using lines that start with the identifying character F -- ("Formal"). These lines are generated if Frame_Condition_Mode is True. -- The SPARK cross-reference information comes after the shared -- cross-reference information, so it needs not be read by tools like -- gnatbind, gnatmake etc. -- ------------------- -- -- Scope Section -- -- ------------------- -- A first section defines the scopes in which entities are defined and -- referenced. A scope is a package/subprogram declaration/body. Note that -- a package declaration and body define two different scopes. Similarly, a -- subprogram declaration and body, when both present, define two different -- scopes. -- FD dependency-number filename (-> unit-filename)? -- This header precedes scope information for the unit identified by -- dependency number and file name. The dependency number is the index -- into the generated D lines and is ones-origin (e.g. 2 = reference to -- second generated D line). -- The list of FD lines should match the list of D lines defined in the -- ALI file, in the same order. -- Note that the filename here will reflect the original name if a -- Source_Reference pragma was encountered (since all line number -- references will be with respect to the original file). -- Note: the filename is redundant in that it could be deduced from the -- corresponding D line, but it is convenient at least for human -- reading of the SPARK cross-reference information, and means that -- the SPARK cross-reference information can stand on its own without -- needing other parts of the ALI file. -- The optional unit filename is given only for subunits. -- FS . scope line type col entity (-> spec-file . spec-scope)? -- (The ? mark stands for an optional entry in the syntax) -- scope is the ones-origin scope number for the current file (e.g. 2 = -- reference to the second FS line in this FD block). -- line is the line number of the scope entity. The name of the entity -- starts in column col. Columns are numbered from one, and if -- horizontal tab characters are present, the column number is computed -- assuming standard 1,9,17,.. tab stops. For example, if the entity is -- the first token on the line, and is preceded by space-HT-space, then -- the column would be column 10. -- type is a single letter identifying the type of the entity, using -- the same code as in cross-references: -- K = package -- V = function -- U = procedure -- col is the column number of the scope entity -- entity is the name of the scope entity, with casing in the canonical -- casing for the source file where it is defined. -- spec-file and spec-scope are respectively the file and scope for the -- spec corresponding to the current body scope, when they differ. -- ------------------ -- -- Xref Section -- -- ------------------ -- A second section defines cross-references useful for computing the set -- of global variables read/written in each subprogram/package. -- FX dependency-number filename . entity-number entity -- dependency-number and filename identity a file in FD lines -- entity-number and identity identify a scope entity in FS lines for -- the file previously identified. -- line typ col entity ref* -- line is the line number of the referenced entity -- typ is the type of the referenced entity, using a code similar to -- the one used for cross-references: -- > = IN parameter -- < = OUT parameter -- = = IN OUT parameter -- * = all other cases -- col is the column number of the referenced entity -- entity is the name of the referenced entity as written in the source -- file where it is defined. -- There may be zero or more ref entries on each line -- (file |)? ((. scope :)? line type col)* -- file is the dependency number of the file with the reference. It and -- the following vertical bar are omitted if the file is the same as -- the previous ref, and the refs for the current file are first (and -- do not need a bar). -- scope is the scope number of the scope with the reference. It and -- the following colon are omitted if the scope is the same as the -- previous ref, and the refs for the current scope are first (and do -- not need a colon). -- line is the line number of the reference -- col is the column number of the reference -- type is one of the following, using the same code as in -- cross-references: -- m = modification -- r = reference -- c = reference to constant object -- s = subprogram reference in a static call -- Special entries for reads and writes to memory reference a special -- variable called "__HEAP". These special entries are present in every -- scope where reads and writes to memory are present. Line and column for -- this special variable are always 0. -- Examples: ??? add examples here -- ------------------------------- -- -- Generated Globals Section -- -- ------------------------------- -- The Generated Globals section is located at the end of the ALI file. -- All lines introducing information related to the Generated Globals -- have the string "GG" appearing in the beginning. This string ("GG") -- should therefore not be used in the beginning of any line that does -- not relate to Generated Globals. -- The processing (reading and writing) of this section happens in -- package Flow_Computed_Globals (from the SPARK 2014 sources), for -- further information please refer there. ---------------- -- Xref Table -- ---------------- -- The following table records SPARK cross-references type Xref_Index is new Int; -- Used to index values in this table. Values start at 1 and are assigned -- sequentially as entries are constructed. type SPARK_Xref_Record is record Entity_Name : String_Ptr; -- Pointer to entity name in ALI file Entity_Line : Nat; -- Line number for the entity referenced Etype : Character; -- Indicates type of entity, using code used in ALI file: -- > = IN parameter -- < = OUT parameter -- = = IN OUT parameter -- * = all other cases Entity_Col : Nat; -- Column number for the entity referenced File_Num : Nat; -- Set to the file dependency number for the cross-reference. Note -- that if no file entry is present explicitly, this is just a copy -- of the reference for the current cross-reference section. Scope_Num : Nat; -- Set to the scope number for the cross-reference. Note that if no -- scope entry is present explicitly, this is just a copy of the -- reference for the current cross-reference section. Line : Nat; -- Line number for the reference Rtype : Character; -- Indicates type of reference, using code used in ALI file: -- r = reference -- c = reference to constant object -- m = modification -- s = call Col : Nat; -- Column number for the reference end record; package SPARK_Xref_Table is new GNAT.Table ( Table_Component_Type => SPARK_Xref_Record, Table_Index_Type => Xref_Index, Table_Low_Bound => 1, Table_Initial => 2000, Table_Increment => 300); ----------------- -- Scope Table -- ----------------- -- This table keeps track of the scopes and the corresponding starting and -- ending indexes (From, To) in the Xref table. type Scope_Index is new Int; -- Used to index values in this table. Values start at 1 and are assigned -- sequentially as entries are constructed. type SPARK_Scope_Record is record Scope_Name : String_Ptr; -- Pointer to scope name in ALI file File_Num : Nat; -- Set to the file dependency number for the scope Scope_Num : Nat; -- Set to the scope number for the scope Spec_File_Num : Nat; -- Set to the file dependency number for the scope corresponding to the -- spec of the current scope entity, if different, or else 0. Spec_Scope_Num : Nat; -- Set to the scope number for the scope corresponding to the spec of -- the current scope entity, if different, or else 0. Line : Nat; -- Line number for the scope Stype : Character; -- Indicates type of scope, using code used in ALI file: -- K = package -- V = function -- U = procedure Col : Nat; -- Column number for the scope From_Xref : Xref_Index; -- Starting index in Xref table for this scope To_Xref : Xref_Index; -- Ending index in Xref table for this scope -- The following component is only used in-memory, not printed out in -- ALI file. Scope_Entity : Entity_Id := Empty; -- Entity (subprogram or package) for the scope end record; package SPARK_Scope_Table is new GNAT.Table ( Table_Component_Type => SPARK_Scope_Record, Table_Index_Type => Scope_Index, Table_Low_Bound => 1, Table_Initial => 200, Table_Increment => 300); ---------------- -- File Table -- ---------------- -- This table keeps track of the units and the corresponding starting and -- ending indexes (From, To) in the Scope table. type File_Index is new Int; -- Used to index values in this table. Values start at 1 and are assigned -- sequentially as entries are constructed. type SPARK_File_Record is record File_Name : String_Ptr; -- Pointer to file name in ALI file Unit_File_Name : String_Ptr; -- Pointer to file name for unit in ALI file, when File_Name refers to a -- subunit. Otherwise null. File_Num : Nat; -- Dependency number in ALI file From_Scope : Scope_Index; -- Starting index in Scope table for this unit To_Scope : Scope_Index; -- Ending index in Scope table for this unit end record; package SPARK_File_Table is new GNAT.Table ( Table_Component_Type => SPARK_File_Record, Table_Index_Type => File_Index, Table_Low_Bound => 1, Table_Initial => 20, Table_Increment => 200); --------------- -- Constants -- --------------- Name_Of_Heap_Variable : constant String := "__HEAP"; -- Name of special variable used in effects to denote reads and writes -- through explicit dereference. ----------------- -- Subprograms -- ----------------- procedure Initialize_SPARK_Tables; -- Reset tables for a new compilation procedure dspark; -- Debug routine to dump internal SPARK cross-reference tables. This is a -- raw format dump showing exactly what the tables contain. procedure pspark; -- Debugging procedure to output contents of SPARK cross-reference binary -- tables in the format in which they appear in an ALI file. end SPARK_Xrefs;