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
26with Einfo;       use Einfo;
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         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
347end SPARK_Specific;
348