File : ghost.adb
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT COMPILER COMPONENTS --
4 -- --
5 -- G H O S T --
6 -- --
7 -- B o d y --
8 -- --
9 -- Copyright (C) 2014-2016, 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 Alloc; use Alloc;
27 with Aspects; use Aspects;
28 with Atree; use Atree;
29 with Einfo; use Einfo;
30 with Elists; use Elists;
31 with Errout; use Errout;
32 with Lib; use Lib;
33 with Namet; use Namet;
34 with Nlists; use Nlists;
35 with Nmake; use Nmake;
36 with Opt; use Opt;
37 with Sem; use Sem;
38 with Sem_Aux; use Sem_Aux;
39 with Sem_Disp; use Sem_Disp;
40 with Sem_Eval; use Sem_Eval;
41 with Sem_Prag; use Sem_Prag;
42 with Sem_Res; use Sem_Res;
43 with Sem_Util; use Sem_Util;
44 with Sinfo; use Sinfo;
45 with Snames; use Snames;
46 with Table;
47
48 package body Ghost is
49
50 -- The following table contains the N_Compilation_Unit node for a unit that
51 -- is either subject to pragma Ghost with policy Ignore or contains ignored
52 -- Ghost code. The table is used in the removal of ignored Ghost code from
53 -- units.
54
55 package Ignored_Ghost_Units is new Table.Table (
56 Table_Component_Type => Node_Id,
57 Table_Index_Type => Int,
58 Table_Low_Bound => 0,
59 Table_Initial => Alloc.Ignored_Ghost_Units_Initial,
60 Table_Increment => Alloc.Ignored_Ghost_Units_Increment,
61 Table_Name => "Ignored_Ghost_Units");
62
63 -----------------------
64 -- Local Subprograms --
65 -----------------------
66
67 function Ghost_Entity (N : Node_Id) return Entity_Id;
68 -- Subsidiary to Check_Ghost_Context and Set_Ghost_Mode. Find the entity of
69 -- a reference to a Ghost entity. Return Empty if there is no such entity.
70
71 function Is_Subject_To_Ghost (N : Node_Id) return Boolean;
72 -- Subsidiary to routines Is_OK_xxx and Set_Ghost_Mode. Determine whether
73 -- declaration or body N is subject to aspect or pragma Ghost. Use this
74 -- routine in cases where [source] pragma Ghost has not been analyzed yet,
75 -- but the context needs to establish the "ghostness" of N.
76
77 procedure Propagate_Ignored_Ghost_Code (N : Node_Id);
78 -- Subsidiary to routines Mark_xxx_As_Ghost and Set_Ghost_Mode_From_xxx.
79 -- Signal all enclosing scopes that they now contain ignored Ghost code.
80 -- Add the compilation unit containing N to table Ignored_Ghost_Units for
81 -- post processing.
82
83 ----------------------------
84 -- Add_Ignored_Ghost_Unit --
85 ----------------------------
86
87 procedure Add_Ignored_Ghost_Unit (Unit : Node_Id) is
88 begin
89 pragma Assert (Nkind (Unit) = N_Compilation_Unit);
90
91 -- Avoid duplicates in the table as pruning the same unit more than once
92 -- is wasteful. Since ignored Ghost code tends to be grouped up, check
93 -- the contents of the table in reverse.
94
95 for Index in reverse Ignored_Ghost_Units.First ..
96 Ignored_Ghost_Units.Last
97 loop
98 -- If the unit is already present in the table, do not add it again
99
100 if Unit = Ignored_Ghost_Units.Table (Index) then
101 return;
102 end if;
103 end loop;
104
105 -- If we get here, then this is the first time the unit is being added
106
107 Ignored_Ghost_Units.Append (Unit);
108 end Add_Ignored_Ghost_Unit;
109
110 ----------------------------
111 -- Check_Ghost_Completion --
112 ----------------------------
113
114 procedure Check_Ghost_Completion
115 (Partial_View : Entity_Id;
116 Full_View : Entity_Id)
117 is
118 Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
119
120 begin
121 -- The Ghost policy in effect at the point of declaration and at the
122 -- point of completion must match (SPARK RM 6.9(14)).
123
124 if Is_Checked_Ghost_Entity (Partial_View)
125 and then Policy = Name_Ignore
126 then
127 Error_Msg_Sloc := Sloc (Full_View);
128
129 Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
130 Error_Msg_N ("\& declared with ghost policy `Check`", Partial_View);
131 Error_Msg_N ("\& completed # with ghost policy `Ignore`",
132 Partial_View);
133
134 elsif Is_Ignored_Ghost_Entity (Partial_View)
135 and then Policy = Name_Check
136 then
137 Error_Msg_Sloc := Sloc (Full_View);
138
139 Error_Msg_N ("incompatible ghost policies in effect", Partial_View);
140 Error_Msg_N ("\& declared with ghost policy `Ignore`", Partial_View);
141 Error_Msg_N ("\& completed # with ghost policy `Check`",
142 Partial_View);
143 end if;
144 end Check_Ghost_Completion;
145
146 -------------------------
147 -- Check_Ghost_Context --
148 -------------------------
149
150 procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is
151 procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id);
152 -- Verify that the Ghost policy at the point of declaration of entity Id
153 -- matches the policy at the point of reference. If this is not the case
154 -- emit an error at Err_N.
155
156 function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
157 -- Determine whether node Context denotes a Ghost-friendly context where
158 -- a Ghost entity can safely reside (SPARK RM 6.9(10)).
159
160 -------------------------
161 -- Is_OK_Ghost_Context --
162 -------------------------
163
164 function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is
165 function Is_OK_Declaration (Decl : Node_Id) return Boolean;
166 -- Determine whether node Decl is a suitable context for a reference
167 -- to a Ghost entity. To qualify as such, Decl must either
168 -- 1) Be subject to pragma Ghost
169 -- 2) Rename a Ghost entity
170
171 function Is_OK_Pragma (Prag : Node_Id) return Boolean;
172 -- Determine whether node Prag is a suitable context for a reference
173 -- to a Ghost entity. To qualify as such, Prag must either
174 -- 1) Be an assertion expression pragma
175 -- 2) Denote pragma Global, Depends, Initializes, Refined_Global,
176 -- Refined_Depends or Refined_State
177 -- 3) Specify an aspect of a Ghost entity
178 -- 4) Contain a reference to a Ghost entity
179
180 function Is_OK_Statement (Stmt : Node_Id) return Boolean;
181 -- Determine whether node Stmt is a suitable context for a reference
182 -- to a Ghost entity. To qualify as such, Stmt must either
183 -- 1) Denote a call to a Ghost procedure
184 -- 2) Denote an assignment statement whose target is Ghost
185
186 -----------------------
187 -- Is_OK_Declaration --
188 -----------------------
189
190 function Is_OK_Declaration (Decl : Node_Id) return Boolean is
191 function In_Subprogram_Body_Profile (N : Node_Id) return Boolean;
192 -- Determine whether node N appears in the profile of a subprogram
193 -- body.
194
195 function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean;
196 -- Determine whether node Ren_Decl denotes a renaming declaration
197 -- with a Ghost name.
198
199 --------------------------------
200 -- In_Subprogram_Body_Profile --
201 --------------------------------
202
203 function In_Subprogram_Body_Profile (N : Node_Id) return Boolean is
204 Spec : constant Node_Id := Parent (N);
205
206 begin
207 -- The node appears in a parameter specification in which case
208 -- it is either the parameter type or the default expression or
209 -- the node appears as the result definition of a function.
210
211 return
212 (Nkind (N) = N_Parameter_Specification
213 or else
214 (Nkind (Spec) = N_Function_Specification
215 and then N = Result_Definition (Spec)))
216 and then Nkind (Parent (Spec)) = N_Subprogram_Body;
217 end In_Subprogram_Body_Profile;
218
219 -----------------------
220 -- Is_Ghost_Renaming --
221 -----------------------
222
223 function Is_Ghost_Renaming (Ren_Decl : Node_Id) return Boolean is
224 Nam_Id : Entity_Id;
225
226 begin
227 if Is_Renaming_Declaration (Ren_Decl) then
228 Nam_Id := Ghost_Entity (Name (Ren_Decl));
229
230 return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
231 end if;
232
233 return False;
234 end Is_Ghost_Renaming;
235
236 -- Local variables
237
238 Subp_Decl : Node_Id;
239 Subp_Id : Entity_Id;
240
241 -- Start of processing for Is_OK_Declaration
242
243 begin
244 if Is_Declaration (Decl) then
245
246 -- A renaming declaration is Ghost when it renames a Ghost
247 -- entity.
248
249 if Is_Ghost_Renaming (Decl) then
250 return True;
251
252 -- The declaration may not have been analyzed yet, determine
253 -- whether it is subject to pragma Ghost.
254
255 elsif Is_Subject_To_Ghost (Decl) then
256 return True;
257 end if;
258
259 -- Special cases
260
261 -- A reference to a Ghost entity may appear within the profile of
262 -- a subprogram body. This context is treated as suitable because
263 -- it duplicates the context of the corresponding spec. The real
264 -- check was already performed during the analysis of the spec.
265
266 elsif In_Subprogram_Body_Profile (Decl) then
267 return True;
268
269 -- A reference to a Ghost entity may appear within an expression
270 -- function which is still being analyzed. This context is treated
271 -- as suitable because it is not yet known whether the expression
272 -- function is an initial declaration or a completion. The real
273 -- check is performed when the expression function is expanded.
274
275 elsif Nkind (Decl) = N_Expression_Function
276 and then not Analyzed (Decl)
277 then
278 return True;
279
280 -- References to Ghost entities may be relocated in internally
281 -- generated bodies.
282
283 elsif Nkind (Decl) = N_Subprogram_Body
284 and then not Comes_From_Source (Decl)
285 then
286 Subp_Id := Corresponding_Spec (Decl);
287
288 if Present (Subp_Id) then
289
290 -- The context is the internally built _Postconditions
291 -- procedure, which is OK because the real check was done
292 -- before expansion activities.
293
294 if Chars (Subp_Id) = Name_uPostconditions then
295 return True;
296
297 else
298 Subp_Decl :=
299 Original_Node (Unit_Declaration_Node (Subp_Id));
300
301 -- The original context is an expression function that
302 -- has been split into a spec and a body. The context is
303 -- OK as long as the initial declaration is Ghost.
304
305 if Nkind (Subp_Decl) = N_Expression_Function then
306 return Is_Subject_To_Ghost (Subp_Decl);
307 end if;
308 end if;
309
310 -- Otherwise this is either an internal body or an internal
311 -- completion. Both are OK because the real check was done
312 -- before expansion activities.
313
314 else
315 return True;
316 end if;
317 end if;
318
319 return False;
320 end Is_OK_Declaration;
321
322 ------------------
323 -- Is_OK_Pragma --
324 ------------------
325
326 function Is_OK_Pragma (Prag : Node_Id) return Boolean is
327 procedure Check_Policies (Prag_Nam : Name_Id);
328 -- Verify that the Ghost policy in effect is the same as the
329 -- assertion policy for pragma name Prag_Nam. Emit an error if
330 -- this is not the case.
331
332 --------------------
333 -- Check_Policies --
334 --------------------
335
336 procedure Check_Policies (Prag_Nam : Name_Id) is
337 AP : constant Name_Id := Check_Kind (Prag_Nam);
338 GP : constant Name_Id := Policy_In_Effect (Name_Ghost);
339
340 begin
341 -- If the Ghost policy in effect at the point of a Ghost entity
342 -- reference is Ignore, then the assertion policy of the pragma
343 -- must be Ignore (SPARK RM 6.9(18)).
344
345 if GP = Name_Ignore and then AP /= Name_Ignore then
346 Error_Msg_N
347 ("incompatible ghost policies in effect",
348 Ghost_Ref);
349 Error_Msg_NE
350 ("\ghost entity & has policy `Ignore`",
351 Ghost_Ref, Ghost_Id);
352
353 Error_Msg_Name_1 := AP;
354 Error_Msg_N
355 ("\assertion expression has policy %", Ghost_Ref);
356 end if;
357 end Check_Policies;
358
359 -- Local variables
360
361 Arg : Node_Id;
362 Arg_Id : Entity_Id;
363 Prag_Id : Pragma_Id;
364 Prag_Nam : Name_Id;
365
366 -- Start of processing for Is_OK_Pragma
367
368 begin
369 if Nkind (Prag) = N_Pragma then
370 Prag_Id := Get_Pragma_Id (Prag);
371 Prag_Nam := Original_Aspect_Pragma_Name (Prag);
372
373 -- A pragma that applies to a Ghost construct or specifies an
374 -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
375
376 if Is_Ghost_Pragma (Prag) then
377 return True;
378
379 -- An assertion expression pragma is Ghost when it contains a
380 -- reference to a Ghost entity (SPARK RM 6.9(10)).
381
382 elsif Assertion_Expression_Pragma (Prag_Id) then
383
384 -- Ensure that the assertion policy and the Ghost policy are
385 -- compatible (SPARK RM 6.9(18)).
386
387 Check_Policies (Prag_Nam);
388 return True;
389
390 -- Several pragmas that may apply to a non-Ghost entity are
391 -- treated as Ghost when they contain a reference to a Ghost
392 -- entity (SPARK RM 6.9(11)).
393
394 elsif Nam_In (Prag_Nam, Name_Global,
395 Name_Depends,
396 Name_Initializes,
397 Name_Refined_Global,
398 Name_Refined_Depends,
399 Name_Refined_State)
400 then
401 return True;
402
403 -- Otherwise a normal pragma is Ghost when it encloses a Ghost
404 -- name (SPARK RM 6.9(3)).
405
406 else
407 Arg := First (Pragma_Argument_Associations (Prag));
408 while Present (Arg) loop
409 Arg_Id := Ghost_Entity (Get_Pragma_Arg (Arg));
410
411 if Present (Arg_Id) and then Is_Ghost_Entity (Arg_Id) then
412 return True;
413 end if;
414
415 Next (Arg);
416 end loop;
417 end if;
418 end if;
419
420 return False;
421 end Is_OK_Pragma;
422
423 ---------------------
424 -- Is_OK_Statement --
425 ---------------------
426
427 function Is_OK_Statement (Stmt : Node_Id) return Boolean is
428 Nam_Id : Entity_Id;
429
430 begin
431 -- An assignment statement or a procedure call is Ghost when the
432 -- name denotes a Ghost entity.
433
434 if Nkind_In (Stmt, N_Assignment_Statement,
435 N_Procedure_Call_Statement)
436 then
437 Nam_Id := Ghost_Entity (Name (Stmt));
438
439 return Present (Nam_Id) and then Is_Ghost_Entity (Nam_Id);
440
441 -- Special cases
442
443 -- An if statement is a suitable context for a Ghost entity if it
444 -- is the byproduct of assertion expression expansion. Note that
445 -- the assertion expression may not be related to a Ghost entity,
446 -- but it may still contain references to Ghost entities.
447
448 elsif Nkind (Stmt) = N_If_Statement
449 and then Nkind (Original_Node (Stmt)) = N_Pragma
450 and then Assertion_Expression_Pragma
451 (Get_Pragma_Id (Original_Node (Stmt)))
452 then
453 return True;
454 end if;
455
456 return False;
457 end Is_OK_Statement;
458
459 -- Local variables
460
461 Par : Node_Id;
462
463 -- Start of processing for Is_OK_Ghost_Context
464
465 begin
466 -- The context is Ghost when it appears within a Ghost package or
467 -- subprogram.
468
469 if Ghost_Mode > None then
470 return True;
471
472 -- Routine Expand_Record_Extension creates a parent subtype without
473 -- inserting it into the tree. There is no good way of recognizing
474 -- this special case as there is no parent. Try to approximate the
475 -- context.
476
477 elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then
478 return True;
479
480 -- Otherwise climb the parent chain looking for a suitable Ghost
481 -- context.
482
483 else
484 Par := Context;
485 while Present (Par) loop
486 if Is_Ignored_Ghost_Node (Par) then
487 return True;
488
489 -- A reference to a Ghost entity can appear within an aspect
490 -- specification (SPARK RM 6.9(10)).
491
492 elsif Nkind (Par) = N_Aspect_Specification then
493 return True;
494
495 elsif Is_OK_Declaration (Par) then
496 return True;
497
498 elsif Is_OK_Pragma (Par) then
499 return True;
500
501 elsif Is_OK_Statement (Par) then
502 return True;
503
504 -- Prevent the search from going too far
505
506 elsif Is_Body_Or_Package_Declaration (Par) then
507 exit;
508 end if;
509
510 Par := Parent (Par);
511 end loop;
512
513 -- The expansion of assertion expression pragmas and attribute Old
514 -- may cause a legal Ghost entity reference to become illegal due
515 -- to node relocation. Check the In_Assertion_Expr counter as last
516 -- resort to try and infer the original legal context.
517
518 if In_Assertion_Expr > 0 then
519 return True;
520
521 -- Otherwise the context is not suitable for a reference to a
522 -- Ghost entity.
523
524 else
525 return False;
526 end if;
527 end if;
528 end Is_OK_Ghost_Context;
529
530 ------------------------
531 -- Check_Ghost_Policy --
532 ------------------------
533
534 procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is
535 Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
536
537 begin
538 -- The Ghost policy in effect a the point of declaration and at the
539 -- point of use must match (SPARK RM 6.9(13)).
540
541 if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
542 Error_Msg_Sloc := Sloc (Err_N);
543
544 Error_Msg_N ("incompatible ghost policies in effect", Err_N);
545 Error_Msg_NE ("\& declared with ghost policy `Check`", Err_N, Id);
546 Error_Msg_NE ("\& used # with ghost policy `Ignore`", Err_N, Id);
547
548 elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then
549 Error_Msg_Sloc := Sloc (Err_N);
550
551 Error_Msg_N ("incompatible ghost policies in effect", Err_N);
552 Error_Msg_NE ("\& declared with ghost policy `Ignore`", Err_N, Id);
553 Error_Msg_NE ("\& used # with ghost policy `Check`", Err_N, Id);
554 end if;
555 end Check_Ghost_Policy;
556
557 -- Start of processing for Check_Ghost_Context
558
559 begin
560 -- Once it has been established that the reference to the Ghost entity
561 -- is within a suitable context, ensure that the policy at the point of
562 -- declaration and at the point of use match.
563
564 if Is_OK_Ghost_Context (Ghost_Ref) then
565 Check_Ghost_Policy (Ghost_Id, Ghost_Ref);
566
567 -- Otherwise the Ghost entity appears in a non-Ghost context and affects
568 -- its behavior or value (SPARK RM 6.9(11,12)).
569
570 else
571 Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref);
572 end if;
573 end Check_Ghost_Context;
574
575 ----------------------------
576 -- Check_Ghost_Overriding --
577 ----------------------------
578
579 procedure Check_Ghost_Overriding
580 (Subp : Entity_Id;
581 Overridden_Subp : Entity_Id)
582 is
583 Deriv_Typ : Entity_Id;
584 Over_Subp : Entity_Id;
585
586 begin
587 if Present (Subp) and then Present (Overridden_Subp) then
588 Over_Subp := Ultimate_Alias (Overridden_Subp);
589 Deriv_Typ := Find_Dispatching_Type (Subp);
590
591 -- A Ghost primitive of a non-Ghost type extension cannot override an
592 -- inherited non-Ghost primitive (SPARK RM 6.9(8)).
593
594 if Is_Ghost_Entity (Subp)
595 and then Present (Deriv_Typ)
596 and then not Is_Ghost_Entity (Deriv_Typ)
597 and then not Is_Ghost_Entity (Over_Subp)
598 then
599 Error_Msg_N ("incompatible overriding in effect", Subp);
600
601 Error_Msg_Sloc := Sloc (Over_Subp);
602 Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
603
604 Error_Msg_Sloc := Sloc (Subp);
605 Error_Msg_N ("\overridden # with ghost subprogram", Subp);
606 end if;
607
608 -- A non-Ghost primitive of a type extension cannot override an
609 -- inherited Ghost primitive (SPARK RM 6.9(8)).
610
611 if not Is_Ghost_Entity (Subp)
612 and then Is_Ghost_Entity (Over_Subp)
613 then
614 Error_Msg_N ("incompatible overriding in effect", Subp);
615
616 Error_Msg_Sloc := Sloc (Over_Subp);
617 Error_Msg_N ("\& declared # as ghost subprogram", Subp);
618
619 Error_Msg_Sloc := Sloc (Subp);
620 Error_Msg_N ("\overridden # with non-ghost subprogram", Subp);
621 end if;
622
623 if Present (Deriv_Typ)
624 and then not Is_Ignored_Ghost_Entity (Deriv_Typ)
625 then
626 -- When a tagged type is either non-Ghost or checked Ghost and
627 -- one of its primitives overrides an inherited operation, the
628 -- overridden operation of the ancestor type must be ignored Ghost
629 -- if the primitive is ignored Ghost (SPARK RM 6.9(17)).
630
631 if Is_Ignored_Ghost_Entity (Subp) then
632
633 -- Both the parent subprogram and overriding subprogram are
634 -- ignored Ghost.
635
636 if Is_Ignored_Ghost_Entity (Over_Subp) then
637 null;
638
639 -- The parent subprogram carries policy Check
640
641 elsif Is_Checked_Ghost_Entity (Over_Subp) then
642 Error_Msg_N
643 ("incompatible ghost policies in effect", Subp);
644
645 Error_Msg_Sloc := Sloc (Over_Subp);
646 Error_Msg_N
647 ("\& declared # with ghost policy `Check`", Subp);
648
649 Error_Msg_Sloc := Sloc (Subp);
650 Error_Msg_N
651 ("\overridden # with ghost policy `Ignore`", Subp);
652
653 -- The parent subprogram is non-Ghost
654
655 else
656 Error_Msg_N
657 ("incompatible ghost policies in effect", Subp);
658
659 Error_Msg_Sloc := Sloc (Over_Subp);
660 Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
661
662 Error_Msg_Sloc := Sloc (Subp);
663 Error_Msg_N
664 ("\overridden # with ghost policy `Ignore`", Subp);
665 end if;
666
667 -- When a tagged type is either non-Ghost or checked Ghost and
668 -- one of its primitives overrides an inherited operation, the
669 -- the primitive of the tagged type must be ignored Ghost if the
670 -- overridden operation is ignored Ghost (SPARK RM 6.9(17)).
671
672 elsif Is_Ignored_Ghost_Entity (Over_Subp) then
673
674 -- Both the parent subprogram and the overriding subprogram are
675 -- ignored Ghost.
676
677 if Is_Ignored_Ghost_Entity (Subp) then
678 null;
679
680 -- The overriding subprogram carries policy Check
681
682 elsif Is_Checked_Ghost_Entity (Subp) then
683 Error_Msg_N
684 ("incompatible ghost policies in effect", Subp);
685
686 Error_Msg_Sloc := Sloc (Over_Subp);
687 Error_Msg_N
688 ("\& declared # with ghost policy `Ignore`", Subp);
689
690 Error_Msg_Sloc := Sloc (Subp);
691 Error_Msg_N
692 ("\overridden # with Ghost policy `Check`", Subp);
693
694 -- The overriding subprogram is non-Ghost
695
696 else
697 Error_Msg_N
698 ("incompatible ghost policies in effect", Subp);
699
700 Error_Msg_Sloc := Sloc (Over_Subp);
701 Error_Msg_N
702 ("\& declared # with ghost policy `Ignore`", Subp);
703
704 Error_Msg_Sloc := Sloc (Subp);
705 Error_Msg_N
706 ("\overridden # with non-ghost subprogram", Subp);
707 end if;
708 end if;
709 end if;
710 end if;
711 end Check_Ghost_Overriding;
712
713 ---------------------------
714 -- Check_Ghost_Primitive --
715 ---------------------------
716
717 procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is
718 begin
719 -- The Ghost policy in effect at the point of declaration of a primitive
720 -- operation and a tagged type must match (SPARK RM 6.9(16)).
721
722 if Is_Tagged_Type (Typ) then
723 if Is_Checked_Ghost_Entity (Prim)
724 and then Is_Ignored_Ghost_Entity (Typ)
725 then
726 Error_Msg_N ("incompatible ghost policies in effect", Prim);
727
728 Error_Msg_Sloc := Sloc (Typ);
729 Error_Msg_NE
730 ("\tagged type & declared # with ghost policy `Ignore`",
731 Prim, Typ);
732
733 Error_Msg_Sloc := Sloc (Prim);
734 Error_Msg_N
735 ("\primitive subprogram & declared # with ghost policy `Check`",
736 Prim);
737
738 elsif Is_Ignored_Ghost_Entity (Prim)
739 and then Is_Checked_Ghost_Entity (Typ)
740 then
741 Error_Msg_N ("incompatible ghost policies in effect", Prim);
742
743 Error_Msg_Sloc := Sloc (Typ);
744 Error_Msg_NE
745 ("\tagged type & declared # with ghost policy `Check`",
746 Prim, Typ);
747
748 Error_Msg_Sloc := Sloc (Prim);
749 Error_Msg_N
750 ("\primitive subprogram & declared # with ghost policy `Ignore`",
751 Prim);
752 end if;
753 end if;
754 end Check_Ghost_Primitive;
755
756 ----------------------------
757 -- Check_Ghost_Refinement --
758 ----------------------------
759
760 procedure Check_Ghost_Refinement
761 (State : Node_Id;
762 State_Id : Entity_Id;
763 Constit : Node_Id;
764 Constit_Id : Entity_Id)
765 is
766 begin
767 if Is_Ghost_Entity (State_Id) then
768 if Is_Ghost_Entity (Constit_Id) then
769
770 -- The Ghost policy in effect at the point of abstract state
771 -- declaration and constituent must match (SPARK RM 6.9(15)).
772
773 if Is_Checked_Ghost_Entity (State_Id)
774 and then Is_Ignored_Ghost_Entity (Constit_Id)
775 then
776 Error_Msg_Sloc := Sloc (Constit);
777 SPARK_Msg_N ("incompatible ghost policies in effect", State);
778
779 SPARK_Msg_NE
780 ("\abstract state & declared with ghost policy `Check`",
781 State, State_Id);
782 SPARK_Msg_NE
783 ("\constituent & declared # with ghost policy `Ignore`",
784 State, Constit_Id);
785
786 elsif Is_Ignored_Ghost_Entity (State_Id)
787 and then Is_Checked_Ghost_Entity (Constit_Id)
788 then
789 Error_Msg_Sloc := Sloc (Constit);
790 SPARK_Msg_N ("incompatible ghost policies in effect", State);
791
792 SPARK_Msg_NE
793 ("\abstract state & declared with ghost policy `Ignore`",
794 State, State_Id);
795 SPARK_Msg_NE
796 ("\constituent & declared # with ghost policy `Check`",
797 State, Constit_Id);
798 end if;
799
800 -- A constituent of a Ghost abstract state must be a Ghost entity
801 -- (SPARK RM 7.2.2(12)).
802
803 else
804 SPARK_Msg_NE
805 ("constituent of ghost state & must be ghost",
806 Constit, State_Id);
807 end if;
808 end if;
809 end Check_Ghost_Refinement;
810
811 ------------------
812 -- Ghost_Entity --
813 ------------------
814
815 function Ghost_Entity (N : Node_Id) return Entity_Id is
816 Ref : Node_Id;
817
818 begin
819 -- When the reference extracts a subcomponent, recover the related
820 -- object (SPARK RM 6.9(1)).
821
822 Ref := N;
823 while Nkind_In (Ref, N_Explicit_Dereference,
824 N_Indexed_Component,
825 N_Selected_Component,
826 N_Slice)
827 loop
828 Ref := Prefix (Ref);
829 end loop;
830
831 if Is_Entity_Name (Ref) then
832 return Entity (Ref);
833 else
834 return Empty;
835 end if;
836 end Ghost_Entity;
837
838 --------------------------------
839 -- Implements_Ghost_Interface --
840 --------------------------------
841
842 function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is
843 Iface_Elmt : Elmt_Id;
844
845 begin
846 -- Traverse the list of interfaces looking for a Ghost interface
847
848 if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
849 Iface_Elmt := First_Elmt (Interfaces (Typ));
850 while Present (Iface_Elmt) loop
851 if Is_Ghost_Entity (Node (Iface_Elmt)) then
852 return True;
853 end if;
854
855 Next_Elmt (Iface_Elmt);
856 end loop;
857 end if;
858
859 return False;
860 end Implements_Ghost_Interface;
861
862 ----------------
863 -- Initialize --
864 ----------------
865
866 procedure Initialize is
867 begin
868 Ignored_Ghost_Units.Init;
869 end Initialize;
870
871 -------------------------
872 -- Is_Subject_To_Ghost --
873 -------------------------
874
875 function Is_Subject_To_Ghost (N : Node_Id) return Boolean is
876 function Enables_Ghostness (Arg : Node_Id) return Boolean;
877 -- Determine whether aspect or pragma argument Arg enables "ghostness"
878
879 -----------------------
880 -- Enables_Ghostness --
881 -----------------------
882
883 function Enables_Ghostness (Arg : Node_Id) return Boolean is
884 Expr : Node_Id;
885
886 begin
887 Expr := Arg;
888
889 if Nkind (Expr) = N_Pragma_Argument_Association then
890 Expr := Get_Pragma_Arg (Expr);
891 end if;
892
893 -- Determine whether the expression of the aspect or pragma is static
894 -- and denotes True.
895
896 if Present (Expr) then
897 Preanalyze_And_Resolve (Expr);
898
899 return
900 Is_OK_Static_Expression (Expr)
901 and then Is_True (Expr_Value (Expr));
902
903 -- Otherwise Ghost defaults to True
904
905 else
906 return True;
907 end if;
908 end Enables_Ghostness;
909
910 -- Local variables
911
912 Id : constant Entity_Id := Defining_Entity (N);
913 Asp : Node_Id;
914 Decl : Node_Id;
915 Prev_Id : Entity_Id;
916
917 -- Start of processing for Is_Subject_To_Ghost
918
919 begin
920 -- The related entity of the declaration has not been analyzed yet, do
921 -- not inspect its attributes.
922
923 if Ekind (Id) = E_Void then
924 null;
925
926 elsif Is_Ghost_Entity (Id) then
927 return True;
928
929 -- The completion of a type or a constant is not fully analyzed when the
930 -- reference to the Ghost entity is resolved. Because the completion is
931 -- not marked as Ghost yet, inspect the partial view.
932
933 elsif Is_Record_Type (Id)
934 or else Ekind (Id) = E_Constant
935 or else (Nkind (N) = N_Object_Declaration
936 and then Constant_Present (N))
937 then
938 Prev_Id := Incomplete_Or_Partial_View (Id);
939
940 if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then
941 return True;
942 end if;
943 end if;
944
945 -- Examine the aspect specifications (if any) looking for aspect Ghost
946
947 if Permits_Aspect_Specifications (N) then
948 Asp := First (Aspect_Specifications (N));
949 while Present (Asp) loop
950 if Chars (Identifier (Asp)) = Name_Ghost then
951 return Enables_Ghostness (Expression (Asp));
952 end if;
953
954 Next (Asp);
955 end loop;
956 end if;
957
958 Decl := Empty;
959
960 -- When the context is a [generic] package declaration, pragma Ghost
961 -- resides in the visible declarations.
962
963 if Nkind_In (N, N_Generic_Package_Declaration,
964 N_Package_Declaration)
965 then
966 Decl := First (Visible_Declarations (Specification (N)));
967
968 -- When the context is a package or a subprogram body, pragma Ghost
969 -- resides in the declarative part.
970
971 elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
972 Decl := First (Declarations (N));
973
974 -- Otherwise pragma Ghost appears in the declarations following N
975
976 elsif Is_List_Member (N) then
977 Decl := Next (N);
978 end if;
979
980 while Present (Decl) loop
981 if Nkind (Decl) = N_Pragma
982 and then Pragma_Name (Decl) = Name_Ghost
983 then
984 return
985 Enables_Ghostness (First (Pragma_Argument_Associations (Decl)));
986
987 -- A source construct ends the region where pragma Ghost may appear,
988 -- stop the traversal. Check the original node as source constructs
989 -- may be rewritten into something else by expansion.
990
991 elsif Comes_From_Source (Original_Node (Decl)) then
992 exit;
993 end if;
994
995 Next (Decl);
996 end loop;
997
998 return False;
999 end Is_Subject_To_Ghost;
1000
1001 ----------
1002 -- Lock --
1003 ----------
1004
1005 procedure Lock is
1006 begin
1007 Ignored_Ghost_Units.Locked := True;
1008 Ignored_Ghost_Units.Release;
1009 end Lock;
1010
1011 -----------------------------
1012 -- Mark_Full_View_As_Ghost --
1013 -----------------------------
1014
1015 procedure Mark_Full_View_As_Ghost
1016 (Priv_Typ : Entity_Id;
1017 Full_Typ : Entity_Id)
1018 is
1019 Full_Decl : constant Node_Id := Declaration_Node (Full_Typ);
1020
1021 begin
1022 if Is_Checked_Ghost_Entity (Priv_Typ) then
1023 Set_Is_Checked_Ghost_Entity (Full_Typ);
1024
1025 elsif Is_Ignored_Ghost_Entity (Priv_Typ) then
1026 Set_Is_Ignored_Ghost_Entity (Full_Typ);
1027 Set_Is_Ignored_Ghost_Node (Full_Decl);
1028 Propagate_Ignored_Ghost_Code (Full_Decl);
1029 end if;
1030 end Mark_Full_View_As_Ghost;
1031
1032 --------------------------
1033 -- Mark_Pragma_As_Ghost --
1034 --------------------------
1035
1036 procedure Mark_Pragma_As_Ghost
1037 (Prag : Node_Id;
1038 Context_Id : Entity_Id)
1039 is
1040 begin
1041 if Is_Checked_Ghost_Entity (Context_Id) then
1042 Set_Is_Ghost_Pragma (Prag);
1043
1044 elsif Is_Ignored_Ghost_Entity (Context_Id) then
1045 Set_Is_Ghost_Pragma (Prag);
1046 Set_Is_Ignored_Ghost_Node (Prag);
1047 Propagate_Ignored_Ghost_Code (Prag);
1048 end if;
1049 end Mark_Pragma_As_Ghost;
1050
1051 ----------------------------
1052 -- Mark_Renaming_As_Ghost --
1053 ----------------------------
1054
1055 procedure Mark_Renaming_As_Ghost
1056 (Ren_Decl : Node_Id;
1057 Nam_Id : Entity_Id)
1058 is
1059 Ren_Id : constant Entity_Id := Defining_Entity (Ren_Decl);
1060
1061 begin
1062 if Is_Checked_Ghost_Entity (Nam_Id) then
1063 Set_Is_Checked_Ghost_Entity (Ren_Id);
1064
1065 elsif Is_Ignored_Ghost_Entity (Nam_Id) then
1066 Set_Is_Ignored_Ghost_Entity (Ren_Id);
1067 Set_Is_Ignored_Ghost_Node (Ren_Decl);
1068 Propagate_Ignored_Ghost_Code (Ren_Decl);
1069 end if;
1070 end Mark_Renaming_As_Ghost;
1071
1072 ----------------------------------
1073 -- Propagate_Ignored_Ghost_Code --
1074 ----------------------------------
1075
1076 procedure Propagate_Ignored_Ghost_Code (N : Node_Id) is
1077 Nod : Node_Id;
1078 Scop : Entity_Id;
1079
1080 begin
1081 -- Traverse the parent chain looking for blocks, packages and
1082 -- subprograms or their respective bodies.
1083
1084 Nod := Parent (N);
1085 while Present (Nod) loop
1086 Scop := Empty;
1087
1088 if Nkind (Nod) = N_Block_Statement then
1089 Scop := Entity (Identifier (Nod));
1090
1091 elsif Nkind_In (Nod, N_Package_Body,
1092 N_Package_Declaration,
1093 N_Subprogram_Body,
1094 N_Subprogram_Declaration)
1095 then
1096 Scop := Defining_Entity (Nod);
1097 end if;
1098
1099 -- The current node denotes a scoping construct
1100
1101 if Present (Scop) then
1102
1103 -- Stop the traversal when the scope already contains ignored
1104 -- Ghost code as all enclosing scopes have already been marked.
1105
1106 if Contains_Ignored_Ghost_Code (Scop) then
1107 exit;
1108
1109 -- Otherwise mark this scope and keep climbing
1110
1111 else
1112 Set_Contains_Ignored_Ghost_Code (Scop);
1113 end if;
1114 end if;
1115
1116 Nod := Parent (Nod);
1117 end loop;
1118
1119 -- The unit containing the ignored Ghost code must be post processed
1120 -- before invoking the back end.
1121
1122 Add_Ignored_Ghost_Unit (Cunit (Get_Code_Unit (N)));
1123 end Propagate_Ignored_Ghost_Code;
1124
1125 -------------------------------
1126 -- Remove_Ignored_Ghost_Code --
1127 -------------------------------
1128
1129 procedure Remove_Ignored_Ghost_Code is
1130 procedure Prune_Tree (Root : Node_Id);
1131 -- Remove all code marked as ignored Ghost from the tree of denoted by
1132 -- Root.
1133
1134 ----------------
1135 -- Prune_Tree --
1136 ----------------
1137
1138 procedure Prune_Tree (Root : Node_Id) is
1139 procedure Prune (N : Node_Id);
1140 -- Remove a given node from the tree by rewriting it into null
1141
1142 function Prune_Node (N : Node_Id) return Traverse_Result;
1143 -- Determine whether node N denotes an ignored Ghost construct. If
1144 -- this is the case, rewrite N as a null statement. See the body for
1145 -- special cases.
1146
1147 -----------
1148 -- Prune --
1149 -----------
1150
1151 procedure Prune (N : Node_Id) is
1152 begin
1153 -- Destroy any aspects that may be associated with the node
1154
1155 if Permits_Aspect_Specifications (N) and then Has_Aspects (N) then
1156 Remove_Aspects (N);
1157 end if;
1158
1159 Rewrite (N, Make_Null_Statement (Sloc (N)));
1160 end Prune;
1161
1162 ----------------
1163 -- Prune_Node --
1164 ----------------
1165
1166 function Prune_Node (N : Node_Id) return Traverse_Result is
1167 Id : Entity_Id;
1168
1169 begin
1170 -- The node is either declared as ignored Ghost or is a byproduct
1171 -- of expansion. Destroy it and stop the traversal on this branch.
1172
1173 if Is_Ignored_Ghost_Node (N) then
1174 Prune (N);
1175 return Skip;
1176
1177 -- A freeze node for an ignored ghost entity must be pruned as
1178 -- well, to prevent meaningless references in the back end.
1179
1180 -- ??? the freeze node itself should be ignored ghost
1181
1182 elsif Nkind (N) = N_Freeze_Entity
1183 and then Is_Ignored_Ghost_Entity (Entity (N))
1184 then
1185 Prune (N);
1186 return Skip;
1187
1188 -- Scoping constructs such as blocks, packages, subprograms and
1189 -- bodies offer some flexibility with respect to pruning.
1190
1191 elsif Nkind_In (N, N_Block_Statement,
1192 N_Package_Body,
1193 N_Package_Declaration,
1194 N_Subprogram_Body,
1195 N_Subprogram_Declaration)
1196 then
1197 if Nkind (N) = N_Block_Statement then
1198 Id := Entity (Identifier (N));
1199 else
1200 Id := Defining_Entity (N);
1201 end if;
1202
1203 -- The scoping construct contains both living and ignored Ghost
1204 -- code, let the traversal prune all relevant nodes.
1205
1206 if Contains_Ignored_Ghost_Code (Id) then
1207 return OK;
1208
1209 -- Otherwise the construct contains only living code and should
1210 -- not be pruned.
1211
1212 else
1213 return Skip;
1214 end if;
1215
1216 -- Otherwise keep searching for ignored Ghost nodes
1217
1218 else
1219 return OK;
1220 end if;
1221 end Prune_Node;
1222
1223 procedure Prune_Nodes is new Traverse_Proc (Prune_Node);
1224
1225 -- Start of processing for Prune_Tree
1226
1227 begin
1228 Prune_Nodes (Root);
1229 end Prune_Tree;
1230
1231 -- Start of processing for Remove_Ignored_Ghost_Code
1232
1233 begin
1234 for Index in Ignored_Ghost_Units.First .. Ignored_Ghost_Units.Last loop
1235 Prune_Tree (Unit (Ignored_Ghost_Units.Table (Index)));
1236 end loop;
1237 end Remove_Ignored_Ghost_Code;
1238
1239 --------------------
1240 -- Set_Ghost_Mode --
1241 --------------------
1242
1243 procedure Set_Ghost_Mode (N : Node_Id; Id : Entity_Id := Empty) is
1244 procedure Set_From_Entity (Ent_Id : Entity_Id);
1245 -- Set the value of global variable Ghost_Mode depending on the mode of
1246 -- entity Ent_Id.
1247
1248 procedure Set_From_Policy;
1249 -- Set the value of global variable Ghost_Mode depending on the current
1250 -- Ghost policy in effect.
1251
1252 ---------------------
1253 -- Set_From_Entity --
1254 ---------------------
1255
1256 procedure Set_From_Entity (Ent_Id : Entity_Id) is
1257 begin
1258 Set_Ghost_Mode_From_Entity (Ent_Id);
1259
1260 if Is_Ignored_Ghost_Entity (Ent_Id) then
1261 Set_Is_Ignored_Ghost_Node (N);
1262 Propagate_Ignored_Ghost_Code (N);
1263 end if;
1264 end Set_From_Entity;
1265
1266 ---------------------
1267 -- Set_From_Policy --
1268 ---------------------
1269
1270 procedure Set_From_Policy is
1271 Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
1272
1273 begin
1274 if Policy = Name_Check then
1275 Ghost_Mode := Check;
1276
1277 elsif Policy = Name_Ignore then
1278 Ghost_Mode := Ignore;
1279
1280 Set_Is_Ignored_Ghost_Node (N);
1281 Propagate_Ignored_Ghost_Code (N);
1282 end if;
1283 end Set_From_Policy;
1284
1285 -- Local variables
1286
1287 Nam_Id : Entity_Id;
1288
1289 -- Start of processing for Set_Ghost_Mode
1290
1291 begin
1292 -- The input node denotes one of the many declaration kinds that may be
1293 -- subject to pragma Ghost.
1294
1295 if Is_Declaration (N) then
1296 if Is_Subject_To_Ghost (N) then
1297 Set_From_Policy;
1298
1299 -- The declaration denotes the completion of a deferred constant,
1300 -- pragma Ghost appears on the partial declaration.
1301
1302 elsif Nkind (N) = N_Object_Declaration
1303 and then Constant_Present (N)
1304 and then Present (Id)
1305 then
1306 Set_From_Entity (Id);
1307
1308 -- The declaration denotes the full view of a private type, pragma
1309 -- Ghost appears on the partial declaration.
1310
1311 elsif Nkind (N) = N_Full_Type_Declaration
1312 and then Is_Private_Type (Defining_Entity (N))
1313 and then Present (Id)
1314 then
1315 Set_From_Entity (Id);
1316 end if;
1317
1318 -- The input denotes an assignment or a procedure call. In this case
1319 -- the Ghost mode is dictated by the name of the construct.
1320
1321 elsif Nkind_In (N, N_Assignment_Statement,
1322 N_Procedure_Call_Statement)
1323 then
1324 Nam_Id := Ghost_Entity (Name (N));
1325
1326 if Present (Nam_Id) then
1327 Set_From_Entity (Nam_Id);
1328 end if;
1329
1330 -- The input denotes a package or subprogram body
1331
1332 elsif Nkind_In (N, N_Package_Body, N_Subprogram_Body) then
1333 if (Present (Id) and then Is_Ghost_Entity (Id))
1334 or else Is_Subject_To_Ghost (N)
1335 then
1336 Set_From_Policy;
1337 end if;
1338
1339 -- The input denotes a pragma
1340
1341 elsif Nkind (N) = N_Pragma and then Is_Ghost_Pragma (N) then
1342 if Is_Ignored_Ghost_Node (N) then
1343 Ghost_Mode := Ignore;
1344 else
1345 Ghost_Mode := Check;
1346 end if;
1347
1348 -- The input denotes a freeze node
1349
1350 elsif Nkind (N) = N_Freeze_Entity and then Present (Id) then
1351 Set_From_Entity (Id);
1352 end if;
1353 end Set_Ghost_Mode;
1354
1355 --------------------------------
1356 -- Set_Ghost_Mode_From_Entity --
1357 --------------------------------
1358
1359 procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is
1360 begin
1361 if Is_Checked_Ghost_Entity (Id) then
1362 Ghost_Mode := Check;
1363 elsif Is_Ignored_Ghost_Entity (Id) then
1364 Ghost_Mode := Ignore;
1365 end if;
1366 end Set_Ghost_Mode_From_Entity;
1367
1368 -------------------------
1369 -- Set_Is_Ghost_Entity --
1370 -------------------------
1371
1372 procedure Set_Is_Ghost_Entity (Id : Entity_Id) is
1373 Policy : constant Name_Id := Policy_In_Effect (Name_Ghost);
1374 begin
1375 if Policy = Name_Check then
1376 Set_Is_Checked_Ghost_Entity (Id);
1377 elsif Policy = Name_Ignore then
1378 Set_Is_Ignored_Ghost_Entity (Id);
1379 end if;
1380 end Set_Is_Ghost_Entity;
1381
1382 end Ghost;