gcc/ada/lib-xref-spark_specific.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT COMPILER COMPONENTS                         --
   4 --                                                                          --
   5 --              L I B . X R E F . S P A R K _ S P E C I F I C               --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2011-2017, 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 Einfo;       use Einfo;
  27 with Nmake;       use Nmake;
  28 with SPARK_Xrefs; use SPARK_Xrefs;
  29
  30 separate (Lib.Xref)
  31 package body SPARK_Specific is
  32
  33    ---------------------
  34    -- Local Constants --
  35    ---------------------
  36
  37    --  Table of SPARK_Entities, True for each entity kind used in SPARK
  38
  39    SPARK_Entities : constant array (Entity_Kind) of Boolean :=
  40      (E_Constant         => True,
  41       E_Entry            => True,
  42       E_Function         => True,
  43       E_In_Out_Parameter => True,
  44       E_In_Parameter     => True,
  45       E_Loop_Parameter   => True,
  46       E_Operator         => True,
  47       E_Out_Parameter    => True,
  48       E_Procedure        => True,
  49       E_Variable         => True,
  50       others             => False);
  51
  52    --  True for each reference type used in SPARK
  53
  54    SPARK_References : constant array (Character) of Boolean :=
  55      ('m'    => True,
  56       'r'    => True,
  57       's'    => True,
  58       others => False);
  59
  60    ---------------------
  61    -- Local Variables --
  62    ---------------------
  63
  64    package Drefs is new Table.Table (
  65      Table_Component_Type => Xref_Entry,
  66      Table_Index_Type     => Xref_Entry_Number,
  67      Table_Low_Bound      => 1,
  68      Table_Initial        => Alloc.Drefs_Initial,
  69      Table_Increment      => Alloc.Drefs_Increment,
  70      Table_Name           => "Drefs");
  71    --  Table of cross-references for reads and writes through explicit
  72    --  dereferences, that are output as reads/writes to the special variable
  73    --  "Heap". These references are added to the regular references when
  74    --  computing SPARK cross-references.
  75
  76    -------------------------
  77    -- Iterate_SPARK_Xrefs --
  78    -------------------------
  79
  80    procedure Iterate_SPARK_Xrefs is
  81
  82       procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry);
  83
  84       function Is_SPARK_Reference
  85         (E   : Entity_Id;
  86          Typ : Character) return Boolean;
  87       --  Return whether entity reference E meets SPARK requirements. Typ is
  88       --  the reference type.
  89
  90       function Is_SPARK_Scope (E : Entity_Id) return Boolean;
  91       --  Return whether the entity or reference scope meets requirements for
  92       --  being a SPARK scope.
  93
  94       --------------------
  95       -- Add_SPARK_Xref --
  96       --------------------
  97
  98       procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry) is
  99          Ref : Xref_Key renames Xref.Key;
 100       begin
 101          --  Eliminate entries not appropriate for SPARK
 102
 103          if SPARK_Entities (Ekind (Ref.Ent))
 104            and then SPARK_References (Ref.Typ)
 105            and then Is_SPARK_Scope (Ref.Ent_Scope)
 106            and then Is_SPARK_Scope (Ref.Ref_Scope)
 107            and then Is_SPARK_Reference (Ref.Ent, Ref.Typ)
 108          then
 109             Process
 110               (Index,
 111                (Entity    => Ref.Ent,
 112                 Ref_Scope => Ref.Ref_Scope,
 113                 Rtype     => Ref.Typ));
 114          end if;
 115
 116       end Add_SPARK_Xref;
 117
 118       ------------------------
 119       -- Is_SPARK_Reference --
 120       ------------------------
 121
 122       function Is_SPARK_Reference
 123         (E   : Entity_Id;
 124          Typ : Character) return Boolean
 125       is
 126       begin
 127          --  The only references of interest on callable entities are calls. On
 128          --  uncallable entities, the only references of interest are reads and
 129          --  writes.
 130
 131          if Ekind (E) in Overloadable_Kind then
 132             return Typ = 's';
 133
 134          --  In all other cases, result is true for reference/modify cases,
 135          --  and false for all other cases.
 136
 137          else
 138             return Typ = 'r' or else Typ = 'm';
 139          end if;
 140       end Is_SPARK_Reference;
 141
 142       --------------------
 143       -- Is_SPARK_Scope --
 144       --------------------
 145
 146       function Is_SPARK_Scope (E : Entity_Id) return Boolean is
 147          Can_Be_Renamed : constant Boolean :=
 148                             Present (E)
 149                               and then (Is_Subprogram_Or_Entry (E)
 150                                          or else Ekind (E) = E_Package);
 151       begin
 152          return Present (E)
 153            and then not Is_Generic_Unit (E)
 154            and then (not Can_Be_Renamed or else No (Renamed_Entity (E)));
 155       end Is_SPARK_Scope;
 156
 157    --  Start of processing for Add_SPARK_Xrefs
 158
 159    begin
 160       --  Expose cross-references from private frontend tables to the backend
 161
 162       for Index in Drefs.First .. Drefs.Last loop
 163          Add_SPARK_Xref (Index, Drefs.Table (Index));
 164       end loop;
 165
 166       for Index in Xrefs.First .. Xrefs.Last loop
 167          Add_SPARK_Xref (-Index, Xrefs.Table (Index));
 168       end loop;
 169    end Iterate_SPARK_Xrefs;
 170
 171    -------------------------------------
 172    -- Enclosing_Subprogram_Or_Package --
 173    -------------------------------------
 174
 175    function Enclosing_Subprogram_Or_Library_Package
 176      (N : Node_Id) return Entity_Id
 177    is
 178       Context : Entity_Id;
 179
 180    begin
 181       --  If N is the defining identifier for a subprogram, then return the
 182       --  enclosing subprogram or package, not this subprogram.
 183
 184       if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol)
 185         and then (Ekind (N) in Entry_Kind
 186                    or else Ekind (N) = E_Subprogram_Body
 187                    or else Ekind (N) in Generic_Subprogram_Kind
 188                    or else Ekind (N) in Subprogram_Kind)
 189       then
 190          Context := Parent (Unit_Declaration_Node (N));
 191
 192          --  If this was a library-level subprogram then replace Context with
 193          --  its Unit, which points to N_Subprogram_* node.
 194
 195          if Nkind (Context) = N_Compilation_Unit then
 196             Context := Unit (Context);
 197          end if;
 198       else
 199          Context := N;
 200       end if;
 201
 202       while Present (Context) loop
 203          case Nkind (Context) is
 204             when N_Package_Body
 205                | N_Package_Specification
 206             =>
 207                --  Only return a library-level package
 208
 209                if Is_Library_Level_Entity (Defining_Entity (Context)) then
 210                   Context := Defining_Entity (Context);
 211                   exit;
 212                else
 213                   Context := Parent (Context);
 214                end if;
 215
 216             when N_Pragma =>
 217
 218                --  The enclosing subprogram for a precondition, postcondition,
 219                --  or contract case should be the declaration preceding the
 220                --  pragma (skipping any other pragmas between this pragma and
 221                --  this declaration.
 222
 223                while Nkind (Context) = N_Pragma
 224                  and then Is_List_Member (Context)
 225                  and then Present (Prev (Context))
 226                loop
 227                   Context := Prev (Context);
 228                end loop;
 229
 230                if Nkind (Context) = N_Pragma then
 231                   Context := Parent (Context);
 232                end if;
 233
 234             when N_Entry_Body
 235                | N_Entry_Declaration
 236                | N_Protected_Type_Declaration
 237                | N_Subprogram_Body
 238                | N_Subprogram_Declaration
 239                | N_Subprogram_Specification
 240                | N_Task_Body
 241                | N_Task_Type_Declaration
 242             =>
 243                Context := Defining_Entity (Context);
 244                exit;
 245
 246             when others =>
 247                Context := Parent (Context);
 248          end case;
 249       end loop;
 250
 251       if Nkind (Context) = N_Defining_Program_Unit_Name then
 252          Context := Defining_Identifier (Context);
 253       end if;
 254
 255       --  Do not return a scope without a proper location
 256
 257       if Present (Context)
 258         and then Sloc (Context) = No_Location
 259       then
 260          return Empty;
 261       end if;
 262
 263       return Context;
 264    end Enclosing_Subprogram_Or_Library_Package;
 265
 266    --------------------------
 267    -- Generate_Dereference --
 268    --------------------------
 269
 270    procedure Generate_Dereference
 271      (N   : Node_Id;
 272       Typ : Character := 'r')
 273    is
 274       procedure Create_Heap;
 275       --  Create and decorate the special entity which denotes the heap
 276
 277       -----------------
 278       -- Create_Heap --
 279       -----------------
 280
 281       procedure Create_Heap is
 282       begin
 283          Name_Len := Name_Of_Heap_Variable'Length;
 284          Name_Buffer (1 .. Name_Len) := Name_Of_Heap_Variable;
 285
 286          Heap := Make_Defining_Identifier (Standard_Location, Name_Enter);
 287
 288          Set_Ekind       (Heap, E_Variable);
 289          Set_Is_Internal (Heap, True);
 290          Set_Has_Fully_Qualified_Name (Heap);
 291       end Create_Heap;
 292
 293       --  Local variables
 294
 295       Loc : constant Source_Ptr := Sloc (N);
 296
 297    --  Start of processing for Generate_Dereference
 298
 299    begin
 300       if Loc > No_Location then
 301          Drefs.Increment_Last;
 302
 303          declare
 304             Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last);
 305             Deref       : Xref_Key   renames Deref_Entry.Key;
 306
 307          begin
 308             if No (Heap) then
 309                Create_Heap;
 310             end if;
 311
 312             Deref.Ent := Heap;
 313             Deref.Loc := Loc;
 314             Deref.Typ := Typ;
 315
 316             --  It is as if the special "Heap" was defined in the main unit,
 317             --  in the scope of the entity for the main unit. This single
 318             --  definition point is required to ensure that sorting cross
 319             --  references works for "Heap" references as well.
 320
 321             Deref.Eun := Main_Unit;
 322             Deref.Lun := Get_Top_Level_Code_Unit (Loc);
 323
 324             Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
 325             Deref.Ent_Scope := Cunit_Entity (Main_Unit);
 326
 327             Deref_Entry.Def := No_Location;
 328
 329             Deref_Entry.Ent_Scope_File := Main_Unit;
 330          end;
 331       end if;
 332    end Generate_Dereference;
 333
 334 end SPARK_Specific;