gcc/ada/get_spark_xrefs.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --                       G E T _ S P A R K _ X R E F S                      --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   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 with SPARK_Xrefs; use SPARK_Xrefs;
  27 with Types;       use Types;
  28
  29 with Ada.IO_Exceptions; use Ada.IO_Exceptions;
  30
  31 procedure Get_SPARK_Xrefs is
  32    C : Character;
  33
  34    use ASCII;
  35    --  For CR/LF
  36
  37    Cur_File : Nat;
  38    --  Dependency number for the current file
  39
  40    Cur_Scope : Nat;
  41    --  Scope number for the current scope entity
  42
  43    Cur_File_Idx : File_Index;
  44    --  Index in SPARK_File_Table of the current file
  45
  46    Cur_Scope_Idx : Scope_Index;
  47    --  Index in SPARK_Scope_Table of the current scope
  48
  49    Name_Str : String (1 .. 32768);
  50    Name_Len : Natural := 0;
  51    --  Local string used to store name of File/entity scanned as
  52    --  Name_Str (1 .. Name_Len).
  53
  54    File_Name : String_Ptr;
  55    Unit_File_Name : String_Ptr;
  56
  57    -----------------------
  58    -- Local Subprograms --
  59    -----------------------
  60
  61    function At_EOL return Boolean;
  62    --  Skips any spaces, then checks if at the end of a line. If so, returns
  63    --  True (but does not skip the EOL sequence). If not, then returns False.
  64
  65    procedure Check (C : Character);
  66    --  Checks that file is positioned at given character, and if so skips past
  67    --  it, If not, raises Data_Error.
  68
  69    function Get_Nat return Nat;
  70    --  On entry the file is positioned to a digit. On return, the file is
  71    --  positioned past the last digit, and the returned result is the decimal
  72    --  value read. Data_Error is raised for overflow (value greater than
  73    --  Int'Last), or if the initial character is not a digit.
  74
  75    procedure Get_Name;
  76    --  On entry the file is positioned to a name. On return, the file is
  77    --  positioned past the last character, and the name scanned is returned
  78    --  in Name_Str (1 .. Name_Len).
  79
  80    procedure Skip_EOL;
  81    --  Called with the current character about to be read being LF or CR. Skips
  82    --  past CR/LF characters until either a non-CR/LF character is found, or
  83    --  the end of file is encountered.
  84
  85    procedure Skip_Spaces;
  86    --  Skips zero or more spaces at the current position, leaving the file
  87    --  positioned at the first non-blank character (or Types.EOF).
  88
  89    ------------
  90    -- At_EOL --
  91    ------------
  92
  93    function At_EOL return Boolean is
  94    begin
  95       Skip_Spaces;
  96       return Nextc = CR or else Nextc = LF;
  97    end At_EOL;
  98
  99    -----------
 100    -- Check --
 101    -----------
 102
 103    procedure Check (C : Character) is
 104    begin
 105       if Nextc = C then
 106          Skipc;
 107       else
 108          raise Data_Error;
 109       end if;
 110    end Check;
 111
 112    -------------
 113    -- Get_Nat --
 114    -------------
 115
 116    function Get_Nat return Nat is
 117       C   : Character := Nextc;
 118       Val : Nat := 0;
 119
 120    begin
 121       if C not in '0' .. '9' then
 122          raise Data_Error;
 123       end if;
 124
 125       --  Loop to read digits of integer value
 126
 127       loop
 128          declare
 129             pragma Unsuppress (Overflow_Check);
 130          begin
 131             Val := Val * 10 + (Character'Pos (C) - Character'Pos ('0'));
 132          end;
 133
 134          Skipc;
 135          C := Nextc;
 136
 137          exit when C not in '0' .. '9';
 138       end loop;
 139
 140       return Val;
 141
 142    exception
 143       when Constraint_Error =>
 144          raise Data_Error;
 145    end Get_Nat;
 146
 147    --------------
 148    -- Get_Name --
 149    --------------
 150
 151    procedure Get_Name is
 152       N : Natural := 0;
 153
 154    begin
 155       while Nextc > ' ' loop
 156          N := N + 1;
 157          Name_Str (N) := Getc;
 158       end loop;
 159
 160       Name_Len := N;
 161    end Get_Name;
 162
 163    --------------
 164    -- Skip_EOL --
 165    --------------
 166
 167    procedure Skip_EOL is
 168       C : Character;
 169
 170    begin
 171       loop
 172          Skipc;
 173          C := Nextc;
 174          exit when C /= LF and then C /= CR;
 175
 176          if C = ' ' then
 177             Skip_Spaces;
 178             C := Nextc;
 179             exit when C /= LF and then C /= CR;
 180          end if;
 181       end loop;
 182    end Skip_EOL;
 183
 184    -----------------
 185    -- Skip_Spaces --
 186    -----------------
 187
 188    procedure Skip_Spaces is
 189    begin
 190       while Nextc = ' ' loop
 191          Skipc;
 192       end loop;
 193    end Skip_Spaces;
 194
 195 --  Start of processing for Get_SPARK_Xrefs
 196
 197 begin
 198    Initialize_SPARK_Tables;
 199
 200    Cur_File      := 0;
 201    Cur_Scope     := 0;
 202    Cur_File_Idx  := 1;
 203    Cur_Scope_Idx := 0;
 204
 205    --  Loop through lines of SPARK cross-reference information
 206
 207    while Nextc = 'F' loop
 208       Skipc;
 209
 210       C := Getc;
 211
 212       --  Make sure first line is a File line
 213
 214       if SPARK_File_Table.Last = 0 and then C /= 'D' then
 215          raise Data_Error;
 216       end if;
 217
 218       --  Otherwise dispatch on type of line
 219
 220       case C is
 221
 222          --  Header entry for scope section
 223
 224          when 'D' =>
 225
 226             --  Complete previous entry if any
 227
 228             if SPARK_File_Table.Last /= 0 then
 229                SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
 230                  SPARK_Scope_Table.Last;
 231             end if;
 232
 233             --  Scan out dependency number and file name
 234
 235             Skip_Spaces;
 236             Cur_File := Get_Nat;
 237             Skip_Spaces;
 238
 239             Get_Name;
 240             File_Name := new String'(Name_Str (1 .. Name_Len));
 241             Skip_Spaces;
 242
 243             --  Scan out unit file name when present (for subunits)
 244
 245             if Nextc = '-' then
 246                Skipc;
 247                Check ('>');
 248                Skip_Spaces;
 249                Get_Name;
 250                Unit_File_Name := new String'(Name_Str (1 .. Name_Len));
 251
 252             else
 253                Unit_File_Name := null;
 254             end if;
 255
 256             --  Make new File table entry (will fill in To_Scope later)
 257
 258             SPARK_File_Table.Append (
 259               (File_Name      => File_Name,
 260                Unit_File_Name => Unit_File_Name,
 261                File_Num       => Cur_File,
 262                From_Scope     => SPARK_Scope_Table.Last + 1,
 263                To_Scope       => 0));
 264
 265             --  Initialize counter for scopes
 266
 267             Cur_Scope := 1;
 268
 269          --  Scope entry
 270
 271          when 'S' =>
 272             declare
 273                Spec_File  : Nat;
 274                Spec_Scope : Nat;
 275                Scope      : Nat;
 276                Line       : Nat;
 277                Col        : Nat;
 278                Typ        : Character;
 279
 280             begin
 281                --  Scan out location
 282
 283                Skip_Spaces;
 284                Check ('.');
 285                Scope := Get_Nat;
 286                Check (' ');
 287                Line  := Get_Nat;
 288                Typ   := Getc;
 289                Col   := Get_Nat;
 290
 291                pragma Assert (Scope = Cur_Scope);
 292
 293                --  Scan out scope entity name
 294
 295                Skip_Spaces;
 296                Get_Name;
 297                Skip_Spaces;
 298
 299                if Nextc = '-' then
 300                   Skipc;
 301                   Check ('>');
 302                   Skip_Spaces;
 303                   Spec_File := Get_Nat;
 304                   Check ('.');
 305                   Spec_Scope := Get_Nat;
 306
 307                else
 308                   Spec_File  := 0;
 309                   Spec_Scope := 0;
 310                end if;
 311
 312                --  Make new scope table entry (will fill in From_Xref and
 313                --  To_Xref later). Initial range (From_Xref .. To_Xref) is
 314                --  empty for scopes without entities.
 315
 316                SPARK_Scope_Table.Append (
 317                  (Scope_Entity   => Empty,
 318                   Scope_Name     => new String'(Name_Str (1 .. Name_Len)),
 319                   File_Num       => Cur_File,
 320                   Scope_Num      => Cur_Scope,
 321                   Spec_File_Num  => Spec_File,
 322                   Spec_Scope_Num => Spec_Scope,
 323                   Line           => Line,
 324                   Stype          => Typ,
 325                   Col            => Col,
 326                   From_Xref      => 1,
 327                   To_Xref        => 0));
 328             end;
 329
 330             --  Update counter for scopes
 331
 332             Cur_Scope := Cur_Scope + 1;
 333
 334          --  Header entry for cross-ref section
 335
 336          when 'X' =>
 337
 338             --  Scan out dependency number and file name (ignored)
 339
 340             Skip_Spaces;
 341             Cur_File := Get_Nat;
 342             Skip_Spaces;
 343             Get_Name;
 344
 345             --  Update component From_Xref of current file if first reference
 346             --  in this file.
 347
 348             while SPARK_File_Table.Table (Cur_File_Idx).File_Num /= Cur_File
 349             loop
 350                Cur_File_Idx := Cur_File_Idx + 1;
 351             end loop;
 352
 353             --  Scan out scope entity number and entity name (ignored)
 354
 355             Skip_Spaces;
 356             Check ('.');
 357             Cur_Scope := Get_Nat;
 358             Skip_Spaces;
 359             Get_Name;
 360
 361             --  Update component To_Xref of previous scope
 362
 363             if Cur_Scope_Idx /= 0 then
 364                SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref :=
 365                  SPARK_Xref_Table.Last;
 366             end if;
 367
 368             --  Update component From_Xref of current scope
 369
 370             Cur_Scope_Idx := SPARK_File_Table.Table (Cur_File_Idx).From_Scope;
 371
 372             while SPARK_Scope_Table.Table (Cur_Scope_Idx).Scope_Num /=
 373               Cur_Scope
 374             loop
 375                Cur_Scope_Idx := Cur_Scope_Idx + 1;
 376             end loop;
 377
 378             SPARK_Scope_Table.Table (Cur_Scope_Idx).From_Xref :=
 379               SPARK_Xref_Table.Last + 1;
 380
 381          --  Cross reference entry
 382
 383          when ' ' =>
 384             declare
 385                XR_Entity      : String_Ptr;
 386                XR_Entity_Line : Nat;
 387                XR_Entity_Col  : Nat;
 388                XR_Entity_Typ  : Character;
 389
 390                XR_File : Nat;
 391                --  Keeps track of the current file (changed by nn|)
 392
 393                XR_Scope : Nat;
 394                --  Keeps track of the current scope (changed by nn:)
 395
 396             begin
 397                XR_File  := Cur_File;
 398                XR_Scope := Cur_Scope;
 399
 400                XR_Entity_Line := Get_Nat;
 401                XR_Entity_Typ  := Getc;
 402                XR_Entity_Col  := Get_Nat;
 403
 404                Skip_Spaces;
 405                Get_Name;
 406                XR_Entity := new String'(Name_Str (1 .. Name_Len));
 407
 408                --  Initialize to scan items on one line
 409
 410                Skip_Spaces;
 411
 412                --  Loop through cross-references for this entity
 413
 414                loop
 415                   declare
 416                      Line  : Nat;
 417                      Col   : Nat;
 418                      N     : Nat;
 419                      Rtype : Character;
 420
 421                   begin
 422                      Skip_Spaces;
 423
 424                      if At_EOL then
 425                         Skip_EOL;
 426                         exit when Nextc /= '.';
 427                         Skipc;
 428                         Skip_Spaces;
 429                      end if;
 430
 431                      if Nextc = '.' then
 432                         Skipc;
 433                         XR_Scope := Get_Nat;
 434                         Check (':');
 435
 436                      else
 437                         N := Get_Nat;
 438
 439                         if Nextc = '|' then
 440                            XR_File := N;
 441                            Skipc;
 442
 443                         else
 444                            Line  := N;
 445                            Rtype := Getc;
 446                            Col   := Get_Nat;
 447
 448                            pragma Assert
 449                              (Rtype = 'r' or else
 450                               Rtype = 'c' or else
 451                               Rtype = 'm' or else
 452                               Rtype = 's');
 453
 454                            SPARK_Xref_Table.Append (
 455                              (Entity_Name => XR_Entity,
 456                               Entity_Line => XR_Entity_Line,
 457                               Etype       => XR_Entity_Typ,
 458                               Entity_Col  => XR_Entity_Col,
 459                               File_Num    => XR_File,
 460                               Scope_Num   => XR_Scope,
 461                               Line        => Line,
 462                               Rtype       => Rtype,
 463                               Col         => Col));
 464                         end if;
 465                      end if;
 466                   end;
 467                end loop;
 468             end;
 469
 470          --  No other SPARK lines are possible
 471
 472          when others =>
 473             raise Data_Error;
 474       end case;
 475
 476       --  For cross reference lines, the EOL character has been skipped already
 477
 478       if C /= ' ' then
 479          Skip_EOL;
 480       end if;
 481    end loop;
 482
 483    --  Here with all Xrefs stored, complete last entries in File/Scope tables
 484
 485    if SPARK_File_Table.Last /= 0 then
 486       SPARK_File_Table.Table (SPARK_File_Table.Last).To_Scope :=
 487         SPARK_Scope_Table.Last;
 488    end if;
 489
 490    if Cur_Scope_Idx /= 0 then
 491       SPARK_Scope_Table.Table (Cur_Scope_Idx).To_Xref := SPARK_Xref_Table.Last;
 492    end if;
 493 end Get_SPARK_Xrefs;