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-2020, 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_Library_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 (N) in N_Defining_Identifier | N_Defining_Operator_Symbol
 185         and then Ekind (N) in Entry_Kind
 186                             | E_Subprogram_Body
 187                             | Generic_Subprogram_Kind
 188                             | 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
 232                   --  When used for cross-references then aspects might not be
 233                   --  yet linked to pragmas; when used for AST navigation in
 234                   --  GNATprove this routine is expected to follow those links.
 235
 236                   if From_Aspect_Specification (Context) then
 237                      Context := Corresponding_Aspect (Context);
 238                      pragma Assert (Nkind (Context) = N_Aspect_Specification);
 239                      Context := Entity (Context);
 240                   else
 241                      Context := Parent (Context);
 242                   end if;
 243                end if;
 244
 245             when N_Entry_Body
 246                | N_Entry_Declaration
 247                | N_Protected_Type_Declaration
 248                | N_Subprogram_Body
 249                | N_Subprogram_Declaration
 250                | N_Subprogram_Specification
 251                | N_Task_Body
 252                | N_Task_Type_Declaration
 253             =>
 254                Context := Defining_Entity (Context);
 255                exit;
 256
 257             when others =>
 258                Context := Parent (Context);
 259          end case;
 260       end loop;
 261
 262       if Nkind (Context) = N_Defining_Program_Unit_Name then
 263          Context := Defining_Identifier (Context);
 264       end if;
 265
 266       --  Do not return a scope without a proper location
 267
 268       if Present (Context)
 269         and then Sloc (Context) = No_Location
 270       then
 271          return Empty;
 272       end if;
 273
 274       return Context;
 275    end Enclosing_Subprogram_Or_Library_Package;
 276
 277    --------------------------
 278    -- Generate_Dereference --
 279    --------------------------
 280
 281    procedure Generate_Dereference
 282      (N   : Node_Id;
 283       Typ : Character := 'r')
 284    is
 285       procedure Create_Heap;
 286       --  Create and decorate the special entity which denotes the heap
 287
 288       -----------------
 289       -- Create_Heap --
 290       -----------------
 291
 292       procedure Create_Heap is
 293       begin
 294          Heap :=
 295            Make_Defining_Identifier
 296              (Standard_Location,
 297               Name_Enter (Name_Of_Heap_Variable));
 298
 299          Set_Ekind       (Heap, E_Variable);
 300          Set_Is_Internal (Heap, True);
 301          Set_Etype       (Heap, Standard_Void_Type);
 302          Set_Scope       (Heap, Standard_Standard);
 303          Set_Has_Fully_Qualified_Name (Heap);
 304       end Create_Heap;
 305
 306       --  Local variables
 307
 308       Loc : constant Source_Ptr := Sloc (N);
 309
 310    --  Start of processing for Generate_Dereference
 311
 312    begin
 313       if Loc > No_Location then
 314          Drefs.Increment_Last;
 315
 316          declare
 317             Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last);
 318             Deref       : Xref_Key   renames Deref_Entry.Key;
 319
 320          begin
 321             if No (Heap) then
 322                Create_Heap;
 323             end if;
 324
 325             Deref.Ent := Heap;
 326             Deref.Loc := Loc;
 327             Deref.Typ := Typ;
 328
 329             --  It is as if the special "Heap" was defined in the main unit,
 330             --  in the scope of the entity for the main unit. This single
 331             --  definition point is required to ensure that sorting cross
 332             --  references works for "Heap" references as well.
 333
 334             Deref.Eun := Main_Unit;
 335             Deref.Lun := Get_Top_Level_Code_Unit (Loc);
 336
 337             Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
 338             Deref.Ent_Scope := Cunit_Entity (Main_Unit);
 339
 340             Deref_Entry.Def := No_Location;
 341
 342             Deref_Entry.Ent_Scope_File := Main_Unit;
 343          end;
 344       end if;
 345    end Generate_Dereference;
 346
 347 end SPARK_Specific;