[Ada] Fix expansion of 'Update with multiple choices in GNATprove
[gcc.git] / gcc / ada / exp_spark.adb
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT COMPILER COMPONENTS --
4 -- --
5 -- E X P _ S P A R K --
6 -- --
7 -- B o d y --
8 -- --
9 -- Copyright (C) 1992-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 Atree; use Atree;
27 with Checks; use Checks;
28 with Einfo; use Einfo;
29 with Exp_Attr;
30 with Exp_Ch4;
31 with Exp_Ch5; use Exp_Ch5;
32 with Exp_Dbug; use Exp_Dbug;
33 with Exp_Util; use Exp_Util;
34 with Namet; use Namet;
35 with Nlists; use Nlists;
36 with Nmake; use Nmake;
37 with Rtsfind; use Rtsfind;
38 with Sem; use Sem;
39 with Sem_Prag; use Sem_Prag;
40 with Sem_Res; use Sem_Res;
41 with Sem_Util; use Sem_Util;
42 with Sinfo; use Sinfo;
43 with Snames; use Snames;
44 with Stand; use Stand;
45 with Tbuild; use Tbuild;
46 with Uintp; use Uintp;
47
48 package body Exp_SPARK is
49
50 -----------------------
51 -- Local Subprograms --
52 -----------------------
53
54 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
55 -- Perform attribute-reference-specific expansion
56
57 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id);
58 -- Build the DIC procedure of a type when needed, if not already done
59
60 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id);
61 -- Perform loop-statement-specific expansion
62
63 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
64 -- Perform object-declaration-specific expansion
65
66 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id);
67 -- Perform name evaluation for a renamed object
68
69 procedure Expand_SPARK_N_Op_Ne (N : Node_Id);
70 -- Rewrite operator /= based on operator = when defined explicitly
71
72 ------------------
73 -- Expand_SPARK --
74 ------------------
75
76 procedure Expand_SPARK (N : Node_Id) is
77 begin
78 case Nkind (N) is
79
80 -- Qualification of entity names in formal verification mode
81 -- is limited to the addition of a suffix for homonyms (see
82 -- Exp_Dbug.Qualify_Entity_Name). We used to qualify entity names
83 -- as full expansion does, but this was removed as this prevents the
84 -- verification back-end from using a short name for debugging and
85 -- user interaction. The verification back-end already takes care
86 -- of qualifying names when needed.
87
88 when N_Block_Statement
89 | N_Entry_Declaration
90 | N_Package_Body
91 | N_Package_Declaration
92 | N_Protected_Type_Declaration
93 | N_Subprogram_Body
94 | N_Task_Type_Declaration
95 =>
96 Qualify_Entity_Names (N);
97
98 -- Replace occurrences of System'To_Address by calls to
99 -- System.Storage_Elements.To_Address.
100
101 when N_Attribute_Reference =>
102 Expand_SPARK_N_Attribute_Reference (N);
103
104 when N_Expanded_Name
105 | N_Identifier
106 =>
107 Expand_SPARK_Potential_Renaming (N);
108
109 -- Loop iterations over arrays need to be expanded, to avoid getting
110 -- two names referring to the same object in memory (the array and
111 -- the iterator) in GNATprove, especially since both can be written
112 -- (thus possibly leading to interferences due to aliasing). No such
113 -- problem arises with quantified expressions over arrays, which are
114 -- dealt with specially in GNATprove.
115
116 when N_Loop_Statement =>
117 Expand_SPARK_N_Loop_Statement (N);
118
119 when N_Object_Declaration =>
120 Expand_SPARK_N_Object_Declaration (N);
121
122 when N_Object_Renaming_Declaration =>
123 Expand_SPARK_N_Object_Renaming_Declaration (N);
124
125 when N_Op_Ne =>
126 Expand_SPARK_N_Op_Ne (N);
127
128 when N_Freeze_Entity =>
129 if Is_Type (Entity (N)) then
130 Expand_SPARK_N_Freeze_Type (Entity (N));
131 end if;
132
133 -- In SPARK mode, no other constructs require expansion
134
135 when others =>
136 null;
137 end case;
138 end Expand_SPARK;
139
140 --------------------------------
141 -- Expand_SPARK_N_Freeze_Type --
142 --------------------------------
143
144 procedure Expand_SPARK_N_Freeze_Type (E : Entity_Id) is
145 begin
146 -- When a DIC is inherited by a tagged type, it may need to be
147 -- specialized to the descendant type, hence build a separate DIC
148 -- procedure for it as done during regular expansion for compilation.
149
150 if Has_DIC (E) and then Is_Tagged_Type (E) then
151 Build_DIC_Procedure_Body (E, For_Freeze => True);
152 end if;
153 end Expand_SPARK_N_Freeze_Type;
154
155 ----------------------------------------
156 -- Expand_SPARK_N_Attribute_Reference --
157 ----------------------------------------
158
159 procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id) is
160 Aname : constant Name_Id := Attribute_Name (N);
161 Attr_Id : constant Attribute_Id := Get_Attribute_Id (Aname);
162 Loc : constant Source_Ptr := Sloc (N);
163 Pref : constant Node_Id := Prefix (N);
164 Typ : constant Entity_Id := Etype (N);
165 Expr : Node_Id;
166
167 begin
168 if Attr_Id = Attribute_To_Address then
169
170 -- Extract and convert argument to expected type for call
171
172 Expr :=
173 Make_Type_Conversion (Loc,
174 Subtype_Mark =>
175 New_Occurrence_Of (RTE (RE_Integer_Address), Loc),
176 Expression => Relocate_Node (First (Expressions (N))));
177
178 -- Replace attribute reference with call
179
180 Rewrite (N,
181 Make_Function_Call (Loc,
182 Name =>
183 New_Occurrence_Of (RTE (RE_To_Address), Loc),
184 Parameter_Associations => New_List (Expr)));
185 Analyze_And_Resolve (N, Typ);
186
187 elsif Attr_Id = Attribute_Object_Size
188 or else Attr_Id = Attribute_Size
189 or else Attr_Id = Attribute_Value_Size
190 or else Attr_Id = Attribute_VADS_Size
191 then
192 Exp_Attr.Expand_Size_Attribute (N);
193
194 -- For attributes which return Universal_Integer, introduce a conversion
195 -- to the expected type with the appropriate check flags set.
196
197 elsif Attr_Id = Attribute_Alignment
198 or else Attr_Id = Attribute_Bit
199 or else Attr_Id = Attribute_Bit_Position
200 or else Attr_Id = Attribute_Descriptor_Size
201 or else Attr_Id = Attribute_First_Bit
202 or else Attr_Id = Attribute_Last_Bit
203 or else Attr_Id = Attribute_Length
204 or else Attr_Id = Attribute_Max_Size_In_Storage_Elements
205 or else Attr_Id = Attribute_Pos
206 or else Attr_Id = Attribute_Position
207 or else Attr_Id = Attribute_Range_Length
208 or else Attr_Id = Attribute_Aft
209 or else Attr_Id = Attribute_Max_Alignment_For_Allocation
210 then
211 -- If the expected type is Long_Long_Integer, there will be no check
212 -- flag as the compiler assumes attributes always fit in this type.
213 -- Since in SPARK_Mode we do not take Storage_Error into account, we
214 -- cannot make this assumption and need to produce a check.
215 -- ??? It should be enough to add this check for attributes 'Length
216 -- and 'Range_Length when the type is as big as Long_Long_Integer.
217
218 declare
219 Typ : Entity_Id;
220 begin
221 if Attr_Id = Attribute_Range_Length then
222 Typ := Etype (Prefix (N));
223
224 elsif Attr_Id = Attribute_Length then
225 Typ := Get_Index_Subtype (N);
226
227 else
228 Typ := Empty;
229 end if;
230
231 Apply_Universal_Integer_Attribute_Checks (N);
232
233 if Present (Typ)
234 and then RM_Size (Typ) = RM_Size (Standard_Long_Long_Integer)
235 then
236 Set_Do_Overflow_Check (N);
237 end if;
238 end;
239
240 elsif Attr_Id = Attribute_Constrained then
241
242 -- If the prefix is an access to object, the attribute applies to
243 -- the designated object, so rewrite with an explicit dereference.
244
245 if Is_Access_Type (Etype (Pref))
246 and then
247 (not Is_Entity_Name (Pref) or else Is_Object (Entity (Pref)))
248 then
249 Rewrite (Pref,
250 Make_Explicit_Dereference (Loc, Relocate_Node (Pref)));
251 Analyze_And_Resolve (N, Standard_Boolean);
252 end if;
253
254 elsif Attr_Id = Attribute_Update then
255 declare
256 Aggr : constant Node_Id := First (Expressions (N));
257 -- The aggregate expression
258
259 Assoc : Node_Id;
260 Comp : Node_Id;
261 Comp_Id : Entity_Id;
262 Comp_Type : Entity_Id;
263 Expr : Node_Id;
264 Index : Node_Id;
265 Index_Typ : Entity_Id;
266 New_Assoc : Node_Id;
267
268 begin
269 -- Apply scalar range checks on the updated components, if needed
270
271 if Is_Array_Type (Typ) then
272
273 -- Multi-dimensional array
274
275 if Present (Next_Index (First_Index (Typ))) then
276 Assoc := First (Component_Associations (Aggr));
277
278 while Present (Assoc) loop
279 Expr := Expression (Assoc);
280 Comp_Type := Component_Type (Typ);
281
282 if Is_Scalar_Type (Comp_Type) then
283 Apply_Scalar_Range_Check (Expr, Comp_Type);
284 end if;
285
286 -- The current association contains a sequence of indexes
287 -- denoting an element of a multidimensional array:
288 --
289 -- (Index_1, ..., Index_N)
290
291 Expr := First (Choices (Assoc));
292
293 pragma Assert (Nkind (Aggr) = N_Aggregate);
294
295 while Present (Expr) loop
296 Index := First (Expressions (Expr));
297 Index_Typ := First_Index (Typ);
298
299 while Present (Index_Typ) loop
300 Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
301 Next (Index);
302 Next_Index (Index_Typ);
303 end loop;
304
305 Next (Expr);
306 end loop;
307
308 Next (Assoc);
309 end loop;
310
311 -- One-dimensional array
312
313 else
314 Assoc := First (Component_Associations (Aggr));
315
316 while Present (Assoc) loop
317 Expr := Expression (Assoc);
318 Comp_Type := Component_Type (Typ);
319
320 if Is_Scalar_Type (Comp_Type) then
321 Apply_Scalar_Range_Check (Expr, Comp_Type);
322 end if;
323
324 Index := First (Choices (Assoc));
325 Index_Typ := First_Index (Typ);
326
327 while Present (Index) loop
328 -- The index denotes a range of elements
329
330 if Nkind (Index) = N_Range then
331 Apply_Scalar_Range_Check
332 (Low_Bound (Index), Etype (Index_Typ));
333 Apply_Scalar_Range_Check
334 (High_Bound (Index), Etype (Index_Typ));
335
336 -- Otherwise the index denotes a single element
337
338 else
339 Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
340 end if;
341
342 Next (Index);
343 end loop;
344
345 Next (Assoc);
346 end loop;
347 end if;
348
349 else pragma Assert (Is_Record_Type (Typ));
350
351 -- If the aggregate has multiple component choices, e.g.
352 --
353 -- X'Update (A | B | C => 123)
354 --
355 -- then each component might be of a different type and might
356 -- or might not require a range check. We first rewrite
357 -- associations into single-component choices, e.g.:
358 --
359 -- X'Update (A => 123, B => 123, C => 123)
360 --
361 -- and then apply range checks to individual copies of the
362 -- expressions.
363
364 -- Iterate over associations of the original aggregate
365
366 Assoc := First (Component_Associations (Aggr));
367
368 -- Rewrite into a new aggregate and decorate
369
370 Rewrite
371 (Aggr,
372 Make_Aggregate
373 (Sloc => Sloc (Aggr),
374 Component_Associations => New_List));
375
376 Set_Etype (Aggr, Typ);
377
378 -- Populate the new aggregate with component associations
379
380 while Present (Assoc) loop
381 Expr := Expression (Assoc);
382 Comp := First (Choices (Assoc));
383
384 while Present (Comp) loop
385 Comp_Id := Entity (Comp);
386 Comp_Type := Etype (Comp_Id);
387
388 New_Assoc :=
389 Make_Component_Association
390 (Sloc => Sloc (Assoc),
391 Choices =>
392 New_List
393 (New_Occurrence_Of (Comp_Id, Sloc (Comp))),
394 Expression => New_Copy_Tree (Expr));
395
396 -- New association must be attached as a child of the
397 -- aggregate before we analyze it.
398
399 Append (New_Assoc, Component_Associations (Aggr));
400
401 Analyze_And_Resolve (Expression (New_Assoc), Comp_Type);
402
403 if Is_Scalar_Type (Comp_Type) then
404 Apply_Scalar_Range_Check
405 (Expression (New_Assoc), Comp_Type);
406 end if;
407
408 Next (Comp);
409 end loop;
410
411 Next (Assoc);
412 end loop;
413 end if;
414 end;
415 end if;
416 end Expand_SPARK_N_Attribute_Reference;
417
418 -----------------------------------
419 -- Expand_SPARK_N_Loop_Statement --
420 -----------------------------------
421
422 procedure Expand_SPARK_N_Loop_Statement (N : Node_Id) is
423 Scheme : constant Node_Id := Iteration_Scheme (N);
424
425 begin
426 -- Loop iterations over arrays need to be expanded, to avoid getting
427 -- two names referring to the same object in memory (the array and the
428 -- iterator) in GNATprove, especially since both can be written (thus
429 -- possibly leading to interferences due to aliasing). No such problem
430 -- arises with quantified expressions over arrays, which are dealt with
431 -- specially in GNATprove.
432
433 if Present (Scheme)
434 and then Present (Iterator_Specification (Scheme))
435 and then Is_Iterator_Over_Array (Iterator_Specification (Scheme))
436 then
437 Expand_Iterator_Loop_Over_Array (N);
438 end if;
439 end Expand_SPARK_N_Loop_Statement;
440
441 ---------------------------------------
442 -- Expand_SPARK_N_Object_Declaration --
443 ---------------------------------------
444
445 procedure Expand_SPARK_N_Object_Declaration (N : Node_Id) is
446 Loc : constant Source_Ptr := Sloc (N);
447 Obj_Id : constant Entity_Id := Defining_Identifier (N);
448 Typ : constant Entity_Id := Etype (Obj_Id);
449
450 Call : Node_Id;
451
452 begin
453 -- If the object declaration denotes a variable without initialization
454 -- whose type is subject to pragma Default_Initial_Condition, create
455 -- and analyze a dummy call to the DIC procedure of the type in order
456 -- to detect potential elaboration issues.
457
458 if Comes_From_Source (Obj_Id)
459 and then Ekind (Obj_Id) = E_Variable
460 and then Has_DIC (Typ)
461 and then Present (DIC_Procedure (Typ))
462 and then not Has_Init_Expression (N)
463 then
464 Call := Build_DIC_Call (Loc, Obj_Id, Typ);
465
466 -- Partially insert the call into the tree by setting its parent
467 -- pointer.
468
469 Set_Parent (Call, N);
470 Analyze (Call);
471 end if;
472 end Expand_SPARK_N_Object_Declaration;
473
474 ------------------------------------------------
475 -- Expand_SPARK_N_Object_Renaming_Declaration --
476 ------------------------------------------------
477
478 procedure Expand_SPARK_N_Object_Renaming_Declaration (N : Node_Id) is
479 CFS : constant Boolean := Comes_From_Source (N);
480 Loc : constant Source_Ptr := Sloc (N);
481 Obj_Id : constant Entity_Id := Defining_Entity (N);
482 Nam : constant Node_Id := Name (N);
483 Typ : constant Entity_Id := Etype (Obj_Id);
484
485 begin
486 -- Transform a renaming of the form
487
488 -- Obj_Id : <subtype mark> renames <function call>;
489
490 -- into
491
492 -- Obj_Id : constant <subtype mark> := <function call>;
493
494 -- Invoking Evaluate_Name and ultimately Remove_Side_Effects introduces
495 -- a temporary to capture the function result. Once potential renamings
496 -- are rewritten for SPARK, the temporary may be leaked out into source
497 -- constructs and lead to confusing error diagnostics. Using an object
498 -- declaration prevents this unwanted side effect.
499
500 if Nkind (Nam) = N_Function_Call then
501 Rewrite (N,
502 Make_Object_Declaration (Loc,
503 Defining_Identifier => Obj_Id,
504 Constant_Present => True,
505 Object_Definition => New_Occurrence_Of (Typ, Loc),
506 Expression => Nam));
507
508 -- Inherit the original Comes_From_Source status of the renaming
509
510 Set_Comes_From_Source (N, CFS);
511
512 -- Sever the link to the renamed function result because the entity
513 -- will no longer alias anything.
514
515 Set_Renamed_Object (Obj_Id, Empty);
516
517 -- Remove the entity of the renaming declaration from visibility as
518 -- the analysis of the object declaration will reintroduce it again.
519
520 Remove_Entity_And_Homonym (Obj_Id);
521 Analyze (N);
522
523 -- Otherwise unconditionally remove all side effects from the name
524
525 else
526 Evaluate_Name (Nam);
527 end if;
528 end Expand_SPARK_N_Object_Renaming_Declaration;
529
530 --------------------------
531 -- Expand_SPARK_N_Op_Ne --
532 --------------------------
533
534 procedure Expand_SPARK_N_Op_Ne (N : Node_Id) is
535 Typ : constant Entity_Id := Etype (Left_Opnd (N));
536
537 begin
538 -- Case of elementary type with standard operator
539
540 if Is_Elementary_Type (Typ)
541 and then Sloc (Entity (N)) = Standard_Location
542 then
543 null;
544
545 else
546 Exp_Ch4.Expand_N_Op_Ne (N);
547 end if;
548 end Expand_SPARK_N_Op_Ne;
549
550 -------------------------------------
551 -- Expand_SPARK_Potential_Renaming --
552 -------------------------------------
553
554 procedure Expand_SPARK_Potential_Renaming (N : Node_Id) is
555 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean;
556 -- Determine whether arbitrary node Nod appears within a significant
557 -- pragma for SPARK.
558
559 -----------------------------
560 -- In_Insignificant_Pragma --
561 -----------------------------
562
563 function In_Insignificant_Pragma (Nod : Node_Id) return Boolean is
564 Par : Node_Id;
565
566 begin
567 -- Climb the parent chain looking for an enclosing pragma
568
569 Par := Nod;
570 while Present (Par) loop
571 if Nkind (Par) = N_Pragma then
572 return not Pragma_Significant_In_SPARK (Get_Pragma_Id (Par));
573
574 -- Prevent the search from going too far
575
576 elsif Is_Body_Or_Package_Declaration (Par) then
577 exit;
578 end if;
579
580 Par := Parent (Par);
581 end loop;
582
583 return False;
584 end In_Insignificant_Pragma;
585
586 -- Local variables
587
588 Loc : constant Source_Ptr := Sloc (N);
589 Obj_Id : constant Entity_Id := Entity (N);
590 Typ : constant Entity_Id := Etype (N);
591 Ren : Node_Id;
592
593 -- Start of processing for Expand_SPARK_Potential_Renaming
594
595 begin
596 -- Replace a reference to a renaming with the actual renamed object
597
598 if Is_Object (Obj_Id) then
599 Ren := Renamed_Object (Obj_Id);
600
601 if Present (Ren) then
602
603 -- Do not process a reference when it appears within a pragma of
604 -- no significance to SPARK. It is assumed that the replacement
605 -- will violate the semantics of the pragma and cause a spurious
606 -- error.
607
608 if In_Insignificant_Pragma (N) then
609 return;
610
611 -- Instantiations and inlining of subprograms employ "prologues"
612 -- which map actual to formal parameters by means of renamings.
613 -- Replace a reference to a formal by the corresponding actual
614 -- parameter.
615
616 elsif Nkind (Ren) in N_Entity then
617 Rewrite (N, New_Occurrence_Of (Ren, Loc));
618
619 -- Otherwise the renamed object denotes a name
620
621 else
622 Rewrite (N, New_Copy_Tree (Ren, New_Sloc => Loc));
623 Reset_Analyzed_Flags (N);
624 end if;
625
626 Analyze_And_Resolve (N, Typ);
627 end if;
628 end if;
629 end Expand_SPARK_Potential_Renaming;
630
631 end Exp_SPARK;