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-2025, 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.Entities; use Einfo.Entities;
  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          if No (Unit_Declaration_Node (N)) then
 191             return Empty;
 192          end if;
 193
 194          Context := Parent (Unit_Declaration_Node (N));
 195
 196          --  If this was a library-level subprogram then replace Context with
 197          --  its Unit, which points to N_Subprogram_* node.
 198
 199          if Nkind (Context) = N_Compilation_Unit then
 200             Context := Unit (Context);
 201          end if;
 202       else
 203          Context := N;
 204       end if;
 205
 206       while Present (Context) loop
 207          case Nkind (Context) is
 208             when N_Package_Body
 209                | N_Package_Specification
 210             =>
 211                --  Only return a library-level package
 212
 213                if Is_Library_Level_Entity (Defining_Entity (Context)) then
 214                   Context := Defining_Entity (Context);
 215                   exit;
 216                else
 217                   Context := Parent (Context);
 218                end if;
 219
 220             when N_Pragma =>
 221
 222                --  The enclosing subprogram for a precondition, postcondition,
 223                --  or contract case should be the declaration preceding the
 224                --  pragma (skipping any other pragmas between this pragma and
 225                --  this declaration.
 226
 227                while Nkind (Context) = N_Pragma
 228                  and then Is_List_Member (Context)
 229                  and then Present (Prev (Context))
 230                loop
 231                   Context := Prev (Context);
 232                end loop;
 233
 234                if Nkind (Context) = N_Pragma then
 235
 236                   --  When used for cross-references then aspects might not be
 237                   --  yet linked to pragmas; when used for AST navigation in
 238                   --  GNATprove this routine is expected to follow those links.
 239
 240                   if From_Aspect_Specification (Context) then
 241                      Context := Corresponding_Aspect (Context);
 242                      pragma Assert (Nkind (Context) = N_Aspect_Specification);
 243                      Context := Entity (Context);
 244                   else
 245                      Context := Parent (Context);
 246                   end if;
 247                end if;
 248
 249             when N_Entry_Body
 250                | N_Entry_Declaration
 251                | N_Protected_Type_Declaration
 252                | N_Subprogram_Body
 253                | N_Subprogram_Declaration
 254                | N_Subprogram_Specification
 255                | N_Task_Body
 256                | N_Task_Type_Declaration
 257             =>
 258                Context := Defining_Entity (Context);
 259                exit;
 260
 261             when N_Subunit =>
 262                Context := Corresponding_Stub (Context);
 263
 264             when N_Body_Stub =>
 265                Context := Corresponding_Spec_Of_Stub (Context);
 266                exit;
 267
 268             when others =>
 269                Context := Parent (Context);
 270          end case;
 271       end loop;
 272
 273       if Nkind (Context) = N_Defining_Program_Unit_Name then
 274          Context := Defining_Identifier (Context);
 275       end if;
 276
 277       --  Do not return a scope without a proper location
 278
 279       if Present (Context)
 280         and then Sloc (Context) = No_Location
 281       then
 282          return Empty;
 283       end if;
 284
 285       return Context;
 286    end Enclosing_Subprogram_Or_Library_Package;
 287
 288    --------------------------
 289    -- Generate_Dereference --
 290    --------------------------
 291
 292    procedure Generate_Dereference
 293      (N   : Node_Id;
 294       Typ : Character := 'r')
 295    is
 296       procedure Create_Heap;
 297       --  Create and decorate the special entity which denotes the heap
 298
 299       -----------------
 300       -- Create_Heap --
 301       -----------------
 302
 303       procedure Create_Heap is
 304       begin
 305          Heap :=
 306            Make_Defining_Identifier
 307              (Standard_Location,
 308               Name_Enter (Name_Of_Heap_Variable));
 309
 310          Mutate_Ekind    (Heap, E_Variable);
 311          Set_Is_Internal (Heap, True);
 312          Set_Etype       (Heap, Standard_Void_Type);
 313          Set_Scope       (Heap, Standard_Standard);
 314          Set_Has_Fully_Qualified_Name (Heap);
 315       end Create_Heap;
 316
 317       --  Local variables
 318
 319       Loc : constant Source_Ptr := Sloc (N);
 320
 321    --  Start of processing for Generate_Dereference
 322
 323    begin
 324       if Loc > No_Location then
 325          Drefs.Increment_Last;
 326
 327          declare
 328             Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last);
 329             Deref       : Xref_Key   renames Deref_Entry.Key;
 330
 331          begin
 332             if No (Heap) then
 333                Create_Heap;
 334             end if;
 335
 336             Deref.Ent := Heap;
 337             Deref.Loc := Loc;
 338             Deref.Typ := Typ;
 339
 340             --  It is as if the special "Heap" was defined in the main unit,
 341             --  in the scope of the entity for the main unit. This single
 342             --  definition point is required to ensure that sorting cross
 343             --  references works for "Heap" references as well.
 344
 345             Deref.Eun := Main_Unit;
 346             Deref.Lun := Get_Top_Level_Code_Unit (Loc);
 347
 348             Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
 349             Deref.Ent_Scope := Cunit_Entity (Main_Unit);
 350
 351             Deref_Entry.Def := No_Location;
 352
 353             Deref_Entry.Ent_Scope_File := Main_Unit;
 354          end;
 355       end if;
 356    end Generate_Dereference;
 357
 358 end SPARK_Specific;