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-2021, 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
26with Einfo.Entities; use Einfo.Entities;
27with Nmake;          use Nmake;
28with SPARK_Xrefs;    use SPARK_Xrefs;
29
30separate (Lib.Xref)
31package 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 others =>
262               Context := Parent (Context);
263         end case;
264      end loop;
265
266      if Nkind (Context) = N_Defining_Program_Unit_Name then
267         Context := Defining_Identifier (Context);
268      end if;
269
270      --  Do not return a scope without a proper location
271
272      if Present (Context)
273        and then Sloc (Context) = No_Location
274      then
275         return Empty;
276      end if;
277
278      return Context;
279   end Enclosing_Subprogram_Or_Library_Package;
280
281   --------------------------
282   -- Generate_Dereference --
283   --------------------------
284
285   procedure Generate_Dereference
286     (N   : Node_Id;
287      Typ : Character := 'r')
288   is
289      procedure Create_Heap;
290      --  Create and decorate the special entity which denotes the heap
291
292      -----------------
293      -- Create_Heap --
294      -----------------
295
296      procedure Create_Heap is
297      begin
298         Heap :=
299           Make_Defining_Identifier
300             (Standard_Location,
301              Name_Enter (Name_Of_Heap_Variable));
302
303         Mutate_Ekind    (Heap, E_Variable);
304         Set_Is_Internal (Heap, True);
305         Set_Etype       (Heap, Standard_Void_Type);
306         Set_Scope       (Heap, Standard_Standard);
307         Set_Has_Fully_Qualified_Name (Heap);
308      end Create_Heap;
309
310      --  Local variables
311
312      Loc : constant Source_Ptr := Sloc (N);
313
314   --  Start of processing for Generate_Dereference
315
316   begin
317      if Loc > No_Location then
318         Drefs.Increment_Last;
319
320         declare
321            Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last);
322            Deref       : Xref_Key   renames Deref_Entry.Key;
323
324         begin
325            if No (Heap) then
326               Create_Heap;
327            end if;
328
329            Deref.Ent := Heap;
330            Deref.Loc := Loc;
331            Deref.Typ := Typ;
332
333            --  It is as if the special "Heap" was defined in the main unit,
334            --  in the scope of the entity for the main unit. This single
335            --  definition point is required to ensure that sorting cross
336            --  references works for "Heap" references as well.
337
338            Deref.Eun := Main_Unit;
339            Deref.Lun := Get_Top_Level_Code_Unit (Loc);
340
341            Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N);
342            Deref.Ent_Scope := Cunit_Entity (Main_Unit);
343
344            Deref_Entry.Def := No_Location;
345
346            Deref_Entry.Ent_Scope_File := Main_Unit;
347         end;
348      end if;
349   end Generate_Dereference;
350
351end SPARK_Specific;
352