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