]>
Commit | Line | Data |
---|---|---|
56e94186 AC |
1 | ------------------------------------------------------------------------------ |
2 | -- -- | |
3 | -- GNAT COMPILER COMPONENTS -- | |
4 | -- -- | |
06b599fd | 5 | -- L I B . X R E F . S P A R K _ S P E C I F I C -- |
56e94186 AC |
6 | -- -- |
7 | -- B o d y -- | |
8 | -- -- | |
8d0d46f4 | 9 | -- Copyright (C) 2011-2021, Free Software Foundation, Inc. -- |
56e94186 AC |
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 | ||
76f9c7f4 | 26 | with Einfo.Entities; use Einfo.Entities; |
63b5225b | 27 | with Nmake; use Nmake; |
9db78a42 | 28 | with SPARK_Xrefs; use SPARK_Xrefs; |
996c8821 | 29 | |
56e94186 | 30 | separate (Lib.Xref) |
06b599fd | 31 | package body SPARK_Specific is |
56e94186 AC |
32 | |
33 | --------------------- | |
34 | -- Local Constants -- | |
35 | --------------------- | |
36 | ||
06b599fd | 37 | -- Table of SPARK_Entities, True for each entity kind used in SPARK |
e917aec2 | 38 | |
06b599fd | 39 | SPARK_Entities : constant array (Entity_Kind) of Boolean := |
cdc96e3e | 40 | (E_Constant => True, |
7b52257c | 41 | E_Entry => True, |
cdc96e3e AC |
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); | |
56e94186 | 51 | |
06b599fd | 52 | -- True for each reference type used in SPARK |
5b0113d6 | 53 | |
06b599fd | 54 | SPARK_References : constant array (Character) of Boolean := |
80007176 AC |
55 | ('m' => True, |
56 | 'r' => True, | |
57 | 's' => True, | |
56e94186 AC |
58 | others => False); |
59 | ||
226a7fa4 AC |
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, | |
ce5c2061 YM |
68 | Table_Initial => Alloc.Drefs_Initial, |
69 | Table_Increment => Alloc.Drefs_Increment, | |
226a7fa4 AC |
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 | |
c01817d2 | 73 | -- "Heap". These references are added to the regular references when |
06b599fd | 74 | -- computing SPARK cross-references. |
226a7fa4 | 75 | |
c23f55b4 PMR |
76 | ------------------------- |
77 | -- Iterate_SPARK_Xrefs -- | |
78 | ------------------------- | |
cdc96e3e | 79 | |
c23f55b4 | 80 | procedure Iterate_SPARK_Xrefs is |
80007176 | 81 | |
c23f55b4 | 82 | procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry); |
24fd21c3 | 83 | |
06b599fd | 84 | function Is_SPARK_Reference |
cdc96e3e AC |
85 | (E : Entity_Id; |
86 | Typ : Character) return Boolean; | |
06b599fd YM |
87 | -- Return whether entity reference E meets SPARK requirements. Typ is |
88 | -- the reference type. | |
cdc96e3e | 89 | |
06b599fd | 90 | function Is_SPARK_Scope (E : Entity_Id) return Boolean; |
cdc96e3e | 91 | -- Return whether the entity or reference scope meets requirements for |
8e2d104b | 92 | -- being a SPARK scope. |
cdc96e3e | 93 | |
c23f55b4 PMR |
94 | -------------------- |
95 | -- Add_SPARK_Xref -- | |
96 | -------------------- | |
cdc96e3e | 97 | |
c23f55b4 PMR |
98 | procedure Add_SPARK_Xref (Index : Int; Xref : Xref_Entry) is |
99 | Ref : Xref_Key renames Xref.Key; | |
cdc96e3e | 100 | begin |
c23f55b4 | 101 | -- Eliminate entries not appropriate for SPARK |
cdc96e3e | 102 | |
c23f55b4 PMR |
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; | |
cdc96e3e | 115 | |
c23f55b4 | 116 | end Add_SPARK_Xref; |
cdc96e3e | 117 | |
24fd21c3 AC |
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 | |
363f2c58 AC |
128 | -- uncallable entities, the only references of interest are reads and |
129 | -- writes. | |
24fd21c3 AC |
130 | |
131 | if Ekind (E) in Overloadable_Kind then | |
132 | return Typ = 's'; | |
133 | ||
24fd21c3 AC |
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 | |
333e4f86 | 147 | Can_Be_Renamed : constant Boolean := |
13126368 YM |
148 | Present (E) |
149 | and then (Is_Subprogram_Or_Entry (E) | |
150 | or else Ekind (E) = E_Package); | |
24fd21c3 AC |
151 | begin |
152 | return Present (E) | |
153 | and then not Is_Generic_Unit (E) | |
c23f55b4 | 154 | and then (not Can_Be_Renamed or else No (Renamed_Entity (E))); |
24fd21c3 AC |
155 | end Is_SPARK_Scope; |
156 | ||
06b599fd | 157 | -- Start of processing for Add_SPARK_Xrefs |
56e94186 | 158 | |
996c8821 | 159 | begin |
c23f55b4 | 160 | -- Expose cross-references from private frontend tables to the backend |
56e94186 | 161 | |
c23f55b4 PMR |
162 | for Index in Drefs.First .. Drefs.Last loop |
163 | Add_SPARK_Xref (Index, Drefs.Table (Index)); | |
56e94186 AC |
164 | end loop; |
165 | ||
c23f55b4 PMR |
166 | for Index in Xrefs.First .. Xrefs.Last loop |
167 | Add_SPARK_Xref (-Index, Xrefs.Table (Index)); | |
56e94186 | 168 | end loop; |
c23f55b4 | 169 | end Iterate_SPARK_Xrefs; |
56e94186 | 170 | |
8016e567 PT |
171 | --------------------------------------------- |
172 | -- Enclosing_Subprogram_Or_Library_Package -- | |
173 | --------------------------------------------- | |
226a7fa4 | 174 | |
63b5225b YM |
175 | function Enclosing_Subprogram_Or_Library_Package |
176 | (N : Node_Id) return Entity_Id | |
177 | is | |
4871a41d | 178 | Context : Entity_Id; |
226a7fa4 AC |
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 | ||
4a08c95c AC |
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 | |
226a7fa4 | 189 | then |
4871a41d | 190 | Context := Parent (Unit_Declaration_Node (N)); |
f6f40114 | 191 | |
4871a41d | 192 | -- If this was a library-level subprogram then replace Context with |
f6f40114 | 193 | -- its Unit, which points to N_Subprogram_* node. |
cdabbb52 | 194 | |
4871a41d AC |
195 | if Nkind (Context) = N_Compilation_Unit then |
196 | Context := Unit (Context); | |
f6f40114 | 197 | end if; |
226a7fa4 | 198 | else |
4871a41d | 199 | Context := N; |
226a7fa4 AC |
200 | end if; |
201 | ||
4871a41d AC |
202 | while Present (Context) loop |
203 | case Nkind (Context) is | |
d8f43ee6 HK |
204 | when N_Package_Body |
205 | | N_Package_Specification | |
206 | => | |
63b5225b YM |
207 | -- Only return a library-level package |
208 | ||
4871a41d AC |
209 | if Is_Library_Level_Entity (Defining_Entity (Context)) then |
210 | Context := Defining_Entity (Context); | |
63b5225b YM |
211 | exit; |
212 | else | |
4871a41d | 213 | Context := Parent (Context); |
63b5225b | 214 | end if; |
226a7fa4 | 215 | |
226a7fa4 | 216 | when N_Pragma => |
9e92ad49 | 217 | |
15918371 | 218 | -- The enclosing subprogram for a precondition, postcondition, |
ab986406 AC |
219 | -- or contract case should be the declaration preceding the |
220 | -- pragma (skipping any other pragmas between this pragma and | |
221 | -- this declaration. | |
222 | ||
4871a41d AC |
223 | while Nkind (Context) = N_Pragma |
224 | and then Is_List_Member (Context) | |
225 | and then Present (Prev (Context)) | |
ab986406 | 226 | loop |
4871a41d | 227 | Context := Prev (Context); |
ab986406 AC |
228 | end loop; |
229 | ||
4871a41d | 230 | if Nkind (Context) = N_Pragma then |
92a68a04 | 231 | |
b7e875ce PT |
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; | |
226a7fa4 AC |
243 | end if; |
244 | ||
d8f43ee6 HK |
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 | => | |
4871a41d | 254 | Context := Defining_Entity (Context); |
eff69022 AC |
255 | exit; |
256 | ||
226a7fa4 | 257 | when others => |
4871a41d | 258 | Context := Parent (Context); |
226a7fa4 AC |
259 | end case; |
260 | end loop; | |
261 | ||
4871a41d AC |
262 | if Nkind (Context) = N_Defining_Program_Unit_Name then |
263 | Context := Defining_Identifier (Context); | |
226a7fa4 AC |
264 | end if; |
265 | ||
5b0113d6 | 266 | -- Do not return a scope without a proper location |
226a7fa4 | 267 | |
4871a41d AC |
268 | if Present (Context) |
269 | and then Sloc (Context) = No_Location | |
226a7fa4 AC |
270 | then |
271 | return Empty; | |
272 | end if; | |
273 | ||
4871a41d | 274 | return Context; |
63b5225b | 275 | end Enclosing_Subprogram_Or_Library_Package; |
226a7fa4 | 276 | |
226a7fa4 AC |
277 | -------------------------- |
278 | -- Generate_Dereference -- | |
279 | -------------------------- | |
280 | ||
281 | procedure Generate_Dereference | |
282 | (N : Node_Id; | |
283 | Typ : Character := 'r') | |
284 | is | |
cdc96e3e AC |
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 | |
e386872e PT |
294 | Heap := |
295 | Make_Defining_Identifier | |
296 | (Standard_Location, | |
297 | Name_Enter (Name_Of_Heap_Variable)); | |
cdc96e3e AC |
298 | |
299 | Set_Ekind (Heap, E_Variable); | |
300 | Set_Is_Internal (Heap, True); | |
56730418 | 301 | Set_Etype (Heap, Standard_Void_Type); |
7abe7526 | 302 | Set_Scope (Heap, Standard_Standard); |
cdc96e3e AC |
303 | Set_Has_Fully_Qualified_Name (Heap); |
304 | end Create_Heap; | |
305 | ||
306 | -- Local variables | |
307 | ||
b48a45e3 | 308 | Loc : constant Source_Ptr := Sloc (N); |
226a7fa4 | 309 | |
cdc96e3e AC |
310 | -- Start of processing for Generate_Dereference |
311 | ||
226a7fa4 | 312 | begin |
23e7bf6a | 313 | if Loc > No_Location then |
226a7fa4 | 314 | Drefs.Increment_Last; |
cdc96e3e AC |
315 | |
316 | declare | |
b48a45e3 | 317 | Deref_Entry : Xref_Entry renames Drefs.Table (Drefs.Last); |
cdc96e3e AC |
318 | Deref : Xref_Key renames Deref_Entry.Key; |
319 | ||
320 | begin | |
321 | if No (Heap) then | |
322 | Create_Heap; | |
323 | end if; | |
226a7fa4 | 324 | |
cdc96e3e | 325 | Deref.Ent := Heap; |
23e7bf6a | 326 | Deref.Loc := Loc; |
cdc96e3e | 327 | Deref.Typ := Typ; |
226a7fa4 | 328 | |
a5150cb1 AC |
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. | |
226a7fa4 | 333 | |
a5150cb1 AC |
334 | Deref.Eun := Main_Unit; |
335 | Deref.Lun := Get_Top_Level_Code_Unit (Loc); | |
226a7fa4 | 336 | |
b48a45e3 | 337 | Deref.Ref_Scope := Enclosing_Subprogram_Or_Library_Package (N); |
a5150cb1 | 338 | Deref.Ent_Scope := Cunit_Entity (Main_Unit); |
226a7fa4 | 339 | |
cdc96e3e | 340 | Deref_Entry.Def := No_Location; |
226a7fa4 | 341 | |
a5150cb1 | 342 | Deref_Entry.Ent_Scope_File := Main_Unit; |
cdc96e3e | 343 | end; |
226a7fa4 AC |
344 | end if; |
345 | end Generate_Dereference; | |
346 | ||
06b599fd | 347 | end SPARK_Specific; |