1------------------------------------------------------------------------------ 2-- -- 3-- GNAT COMPILER COMPONENTS -- 4-- -- 5-- G H O S T -- 6-- -- 7-- B o d y -- 8-- -- 9-- Copyright (C) 2014-2020, Free Software Foundation, Inc. -- 10-- -- 11-- GNAT is free software; you can redistribute it and/or modify it under -- 12-- terms of the GNU General Public License as published by the Free Soft- -- 13-- ware Foundation; either version 3, or (at your option) any later ver- -- 14-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- 15-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- 16-- or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- 17-- for more details. You should have received a copy of the GNU General -- 18-- Public License distributed with GNAT; see file COPYING3. If not, go to -- 19-- http://www.gnu.org/licenses for a complete copy of the license. -- 20-- -- 21-- GNAT was originally developed by the GNAT team at New York University. -- 22-- Extensive contributions were provided by Ada Core Technologies Inc. -- 23-- -- 24------------------------------------------------------------------------------ 25 26with Alloc; 27with Aspects; use Aspects; 28with Atree; use Atree; 29with Einfo; use Einfo; 30with Elists; use Elists; 31with Errout; use Errout; 32with Namet; use Namet; 33with Nlists; use Nlists; 34with Nmake; use Nmake; 35with Sem; use Sem; 36with Sem_Aux; use Sem_Aux; 37with Sem_Disp; use Sem_Disp; 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 Table; 45 46package body Ghost is 47 48 --------------------- 49 -- Data strictures -- 50 --------------------- 51 52 -- The following table contains all ignored Ghost nodes that must be 53 -- eliminated from the tree by routine Remove_Ignored_Ghost_Code. 54 55 package Ignored_Ghost_Nodes 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_Nodes_Initial, 60 Table_Increment => Alloc.Ignored_Ghost_Nodes_Increment, 61 Table_Name => "Ignored_Ghost_Nodes"); 62 63 ----------------------- 64 -- Local subprograms -- 65 ----------------------- 66 67 function Whole_Object_Ref (Ref : Node_Id) return Node_Id; 68 -- For a name that denotes an object, returns a name that denotes the whole 69 -- object, declared by an object declaration, formal parameter declaration, 70 -- etc. For example, for P.X.Comp (J), if P is a package X is a record 71 -- object, this returns P.X. 72 73 function Ghost_Entity (Ref : Node_Id) return Entity_Id; 74 pragma Inline (Ghost_Entity); 75 -- Obtain the entity of a Ghost entity from reference Ref. Return Empty if 76 -- no such entity exists. 77 78 procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type); 79 pragma Inline (Install_Ghost_Mode); 80 -- Install Ghost mode Mode as the Ghost mode in effect 81 82 procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id); 83 pragma Inline (Install_Ghost_Region); 84 -- Install a Ghost region comprised of mode Mode and ignored region start 85 -- node N. 86 87 function Is_Subject_To_Ghost (N : Node_Id) return Boolean; 88 -- Determine whether declaration or body N is subject to aspect or pragma 89 -- Ghost. This routine must be used in cases where pragma Ghost has not 90 -- been analyzed yet, but the context needs to establish the "ghostness" 91 -- of N. 92 93 procedure Mark_Ghost_Declaration_Or_Body 94 (N : Node_Id; 95 Mode : Name_Id); 96 -- Mark the defining entity of declaration or body N as Ghost depending on 97 -- mode Mode. Mark all formals parameters when N denotes a subprogram or a 98 -- body. 99 100 function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type; 101 pragma Inline (Name_To_Ghost_Mode); 102 -- Convert a Ghost mode denoted by name Mode into its respective enumerated 103 -- value. 104 105 procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id); 106 -- Save ignored Ghost node or entity N in table Ignored_Ghost_Nodes for 107 -- later elimination. 108 109 ---------------------------- 110 -- Check_Ghost_Completion -- 111 ---------------------------- 112 113 procedure Check_Ghost_Completion 114 (Prev_Id : Entity_Id; 115 Compl_Id : Entity_Id) 116 is 117 Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); 118 119 begin 120 -- Nothing to do if one of the views is missing 121 122 if No (Prev_Id) or else No (Compl_Id) then 123 null; 124 125 -- The Ghost policy in effect at the point of declaration and at the 126 -- point of completion must match (SPARK RM 6.9(14)). 127 128 elsif Is_Checked_Ghost_Entity (Prev_Id) 129 and then Policy = Name_Ignore 130 then 131 Error_Msg_Sloc := Sloc (Compl_Id); 132 133 Error_Msg_N ("incompatible ghost policies in effect", Prev_Id); 134 Error_Msg_N ("\& declared with ghost policy `Check`", Prev_Id); 135 Error_Msg_N ("\& completed # with ghost policy `Ignore`", Prev_Id); 136 137 elsif Is_Ignored_Ghost_Entity (Prev_Id) 138 and then Policy = Name_Check 139 then 140 Error_Msg_Sloc := Sloc (Compl_Id); 141 142 Error_Msg_N ("incompatible ghost policies in effect", Prev_Id); 143 Error_Msg_N ("\& declared with ghost policy `Ignore`", Prev_Id); 144 Error_Msg_N ("\& completed # with ghost policy `Check`", Prev_Id); 145 end if; 146 end Check_Ghost_Completion; 147 148 ------------------------- 149 -- Check_Ghost_Context -- 150 ------------------------- 151 152 procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is 153 procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id); 154 -- Verify that the Ghost policy at the point of declaration of entity Id 155 -- matches the policy at the point of reference Ref. If this is not the 156 -- case emit an error at Ref. 157 158 function Is_OK_Ghost_Context (Context : Node_Id) return Boolean; 159 -- Determine whether node Context denotes a Ghost-friendly context where 160 -- a Ghost entity can safely reside (SPARK RM 6.9(10)). 161 162 ------------------------- 163 -- Is_OK_Ghost_Context -- 164 ------------------------- 165 166 function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is 167 function Is_OK_Declaration (Decl : Node_Id) return Boolean; 168 -- Determine whether node Decl is a suitable context for a reference 169 -- to a Ghost entity. To qualify as such, Decl must either 170 -- 171 -- * Define a Ghost entity 172 -- 173 -- * Be subject to pragma Ghost 174 175 function Is_OK_Pragma (Prag : Node_Id) return Boolean; 176 -- Determine whether node Prag is a suitable context for a reference 177 -- to a Ghost entity. To qualify as such, Prag must either 178 -- 179 -- * Be an assertion expression pragma 180 -- 181 -- * Denote pragma Global, Depends, Initializes, Refined_Global, 182 -- Refined_Depends or Refined_State. 183 -- 184 -- * Specify an aspect of a Ghost entity 185 -- 186 -- * Contain a reference to a Ghost entity 187 188 function Is_OK_Statement (Stmt : Node_Id) return Boolean; 189 -- Determine whether node Stmt is a suitable context for a reference 190 -- to a Ghost entity. To qualify as such, Stmt must either 191 -- 192 -- * Denote a procedure call to a Ghost procedure 193 -- 194 -- * Denote an assignment statement whose target is Ghost 195 196 ----------------------- 197 -- Is_OK_Declaration -- 198 ----------------------- 199 200 function Is_OK_Declaration (Decl : Node_Id) return Boolean is 201 function In_Subprogram_Body_Profile (N : Node_Id) return Boolean; 202 -- Determine whether node N appears in the profile of a subprogram 203 -- body. 204 205 -------------------------------- 206 -- In_Subprogram_Body_Profile -- 207 -------------------------------- 208 209 function In_Subprogram_Body_Profile (N : Node_Id) return Boolean is 210 Spec : constant Node_Id := Parent (N); 211 212 begin 213 -- The node appears in a parameter specification in which case 214 -- it is either the parameter type or the default expression or 215 -- the node appears as the result definition of a function. 216 217 return 218 (Nkind (N) = N_Parameter_Specification 219 or else 220 (Nkind (Spec) = N_Function_Specification 221 and then N = Result_Definition (Spec))) 222 and then Nkind (Parent (Spec)) = N_Subprogram_Body; 223 end In_Subprogram_Body_Profile; 224 225 -- Local variables 226 227 Subp_Decl : Node_Id; 228 Subp_Id : Entity_Id; 229 230 -- Start of processing for Is_OK_Declaration 231 232 begin 233 if Is_Ghost_Declaration (Decl) then 234 return True; 235 236 -- Special cases 237 238 -- A reference to a Ghost entity may appear within the profile of 239 -- a subprogram body. This context is treated as suitable because 240 -- it duplicates the context of the corresponding spec. The real 241 -- check was already performed during the analysis of the spec. 242 243 elsif In_Subprogram_Body_Profile (Decl) then 244 return True; 245 246 -- A reference to a Ghost entity may appear within an expression 247 -- function which is still being analyzed. This context is treated 248 -- as suitable because it is not yet known whether the expression 249 -- function is an initial declaration or a completion. The real 250 -- check is performed when the expression function is expanded. 251 252 elsif Nkind (Decl) = N_Expression_Function 253 and then not Analyzed (Decl) 254 then 255 return True; 256 257 -- References to Ghost entities may be relocated in internally 258 -- generated bodies. 259 260 elsif Nkind (Decl) = N_Subprogram_Body 261 and then not Comes_From_Source (Decl) 262 then 263 Subp_Id := Corresponding_Spec (Decl); 264 265 if Present (Subp_Id) then 266 267 -- The context is the internally built _Postconditions 268 -- procedure, which is OK because the real check was done 269 -- before expansion activities. 270 271 if Chars (Subp_Id) = Name_uPostconditions then 272 return True; 273 274 -- The context is the internally built predicate function, 275 -- which is OK because the real check was done before the 276 -- predicate function was generated. 277 278 elsif Is_Predicate_Function (Subp_Id) then 279 return True; 280 281 else 282 Subp_Decl := 283 Original_Node (Unit_Declaration_Node (Subp_Id)); 284 285 -- The original context is an expression function that 286 -- has been split into a spec and a body. The context is 287 -- OK as long as the initial declaration is Ghost. 288 289 if Nkind (Subp_Decl) = N_Expression_Function then 290 return Is_Ghost_Declaration (Subp_Decl); 291 end if; 292 end if; 293 294 -- Otherwise this is either an internal body or an internal 295 -- completion. Both are OK because the real check was done 296 -- before expansion activities. 297 298 else 299 return True; 300 end if; 301 end if; 302 303 return False; 304 end Is_OK_Declaration; 305 306 ------------------ 307 -- Is_OK_Pragma -- 308 ------------------ 309 310 function Is_OK_Pragma (Prag : Node_Id) return Boolean is 311 procedure Check_Policies (Prag_Nam : Name_Id); 312 -- Verify that the Ghost policy in effect is the same as the 313 -- assertion policy for pragma name Prag_Nam. Emit an error if 314 -- this is not the case. 315 316 -------------------- 317 -- Check_Policies -- 318 -------------------- 319 320 procedure Check_Policies (Prag_Nam : Name_Id) is 321 AP : constant Name_Id := Check_Kind (Prag_Nam); 322 GP : constant Name_Id := Policy_In_Effect (Name_Ghost); 323 324 begin 325 -- If the Ghost policy in effect at the point of a Ghost entity 326 -- reference is Ignore, then the assertion policy of the pragma 327 -- must be Ignore (SPARK RM 6.9(18)). 328 329 if GP = Name_Ignore and then AP /= Name_Ignore then 330 Error_Msg_N 331 ("incompatible ghost policies in effect", 332 Ghost_Ref); 333 Error_Msg_NE 334 ("\ghost entity & has policy `Ignore`", 335 Ghost_Ref, Ghost_Id); 336 337 Error_Msg_Name_1 := AP; 338 Error_Msg_N 339 ("\assertion expression has policy %", Ghost_Ref); 340 end if; 341 end Check_Policies; 342 343 -- Local variables 344 345 Prag_Id : Pragma_Id; 346 Prag_Nam : Name_Id; 347 348 -- Start of processing for Is_OK_Pragma 349 350 begin 351 if Nkind (Prag) = N_Pragma then 352 Prag_Id := Get_Pragma_Id (Prag); 353 Prag_Nam := Original_Aspect_Pragma_Name (Prag); 354 355 -- A pragma that applies to a Ghost construct or specifies an 356 -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3)) 357 358 if Is_Ghost_Pragma (Prag) then 359 return True; 360 361 -- An assertion expression pragma is Ghost when it contains a 362 -- reference to a Ghost entity (SPARK RM 6.9(10)), except for 363 -- predicate pragmas (SPARK RM 6.9(11)). 364 365 elsif Assertion_Expression_Pragma (Prag_Id) 366 and then Prag_Id /= Pragma_Predicate 367 then 368 -- Ensure that the assertion policy and the Ghost policy are 369 -- compatible (SPARK RM 6.9(18)). 370 371 Check_Policies (Prag_Nam); 372 return True; 373 374 -- Several pragmas that may apply to a non-Ghost entity are 375 -- treated as Ghost when they contain a reference to a Ghost 376 -- entity (SPARK RM 6.9(11)). 377 378 elsif Prag_Nam in Name_Global 379 | Name_Depends 380 | Name_Initializes 381 | Name_Refined_Global 382 | Name_Refined_Depends 383 | Name_Refined_State 384 then 385 return True; 386 end if; 387 end if; 388 389 return False; 390 end Is_OK_Pragma; 391 392 --------------------- 393 -- Is_OK_Statement -- 394 --------------------- 395 396 function Is_OK_Statement (Stmt : Node_Id) return Boolean is 397 begin 398 -- An assignment statement is Ghost when the target is a Ghost 399 -- entity. 400 401 if Nkind (Stmt) = N_Assignment_Statement then 402 return Is_Ghost_Assignment (Stmt); 403 404 -- A procedure call is Ghost when it calls a Ghost procedure 405 406 elsif Nkind (Stmt) = N_Procedure_Call_Statement then 407 return Is_Ghost_Procedure_Call (Stmt); 408 409 -- Special cases 410 411 -- An if statement is a suitable context for a Ghost entity if it 412 -- is the byproduct of assertion expression expansion. Note that 413 -- the assertion expression may not be related to a Ghost entity, 414 -- but it may still contain references to Ghost entities. 415 416 elsif Nkind (Stmt) = N_If_Statement 417 and then Nkind (Original_Node (Stmt)) = N_Pragma 418 and then Assertion_Expression_Pragma 419 (Get_Pragma_Id (Original_Node (Stmt))) 420 then 421 return True; 422 end if; 423 424 return False; 425 end Is_OK_Statement; 426 427 -- Local variables 428 429 Par : Node_Id; 430 431 -- Start of processing for Is_OK_Ghost_Context 432 433 begin 434 -- The context is Ghost when it appears within a Ghost package or 435 -- subprogram. 436 437 if Ghost_Mode > None then 438 return True; 439 440 -- A Ghost type may be referenced in a use_type clause 441 -- (SPARK RM 6.9.10). 442 443 elsif Present (Parent (Context)) 444 and then Nkind (Parent (Context)) = N_Use_Type_Clause 445 then 446 return True; 447 448 -- Routine Expand_Record_Extension creates a parent subtype without 449 -- inserting it into the tree. There is no good way of recognizing 450 -- this special case as there is no parent. Try to approximate the 451 -- context. 452 453 elsif No (Parent (Context)) and then Is_Tagged_Type (Ghost_Id) then 454 return True; 455 456 -- Otherwise climb the parent chain looking for a suitable Ghost 457 -- context. 458 459 else 460 Par := Context; 461 while Present (Par) loop 462 if Is_Ignored_Ghost_Node (Par) then 463 return True; 464 465 -- A reference to a Ghost entity can appear within an aspect 466 -- specification (SPARK RM 6.9(10)). The precise checking will 467 -- occur when analyzing the corresponding pragma. We make an 468 -- exception for predicate aspects that only allow referencing 469 -- a Ghost entity when the corresponding type declaration is 470 -- Ghost (SPARK RM 6.9(11)). 471 472 elsif Nkind (Par) = N_Aspect_Specification 473 and then not Same_Aspect 474 (Get_Aspect_Id (Par), Aspect_Predicate) 475 then 476 return True; 477 478 elsif Is_OK_Declaration (Par) then 479 return True; 480 481 elsif Is_OK_Pragma (Par) then 482 return True; 483 484 elsif Is_OK_Statement (Par) then 485 return True; 486 487 -- Prevent the search from going too far 488 489 elsif Is_Body_Or_Package_Declaration (Par) then 490 exit; 491 end if; 492 493 Par := Parent (Par); 494 end loop; 495 496 -- The expansion of assertion expression pragmas and attribute Old 497 -- may cause a legal Ghost entity reference to become illegal due 498 -- to node relocation. Check the In_Assertion_Expr counter as last 499 -- resort to try and infer the original legal context. 500 501 if In_Assertion_Expr > 0 then 502 return True; 503 504 -- Otherwise the context is not suitable for a reference to a 505 -- Ghost entity. 506 507 else 508 return False; 509 end if; 510 end if; 511 end Is_OK_Ghost_Context; 512 513 ------------------------ 514 -- Check_Ghost_Policy -- 515 ------------------------ 516 517 procedure Check_Ghost_Policy (Id : Entity_Id; Ref : Node_Id) is 518 Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); 519 520 begin 521 -- The Ghost policy in effect a the point of declaration and at the 522 -- point of use must match (SPARK RM 6.9(13)). 523 524 if Is_Checked_Ghost_Entity (Id) 525 and then Policy = Name_Ignore 526 and then May_Be_Lvalue (Ref) 527 then 528 Error_Msg_Sloc := Sloc (Ref); 529 530 Error_Msg_N ("incompatible ghost policies in effect", Ref); 531 Error_Msg_NE ("\& declared with ghost policy `Check`", Ref, Id); 532 Error_Msg_NE ("\& used # with ghost policy `Ignore`", Ref, Id); 533 534 elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then 535 Error_Msg_Sloc := Sloc (Ref); 536 537 Error_Msg_N ("incompatible ghost policies in effect", Ref); 538 Error_Msg_NE ("\& declared with ghost policy `Ignore`", Ref, Id); 539 Error_Msg_NE ("\& used # with ghost policy `Check`", Ref, Id); 540 end if; 541 end Check_Ghost_Policy; 542 543 -- Start of processing for Check_Ghost_Context 544 545 begin 546 -- Once it has been established that the reference to the Ghost entity 547 -- is within a suitable context, ensure that the policy at the point of 548 -- declaration and at the point of use match. 549 550 if Is_OK_Ghost_Context (Ghost_Ref) then 551 Check_Ghost_Policy (Ghost_Id, Ghost_Ref); 552 553 -- Otherwise the Ghost entity appears in a non-Ghost context and affects 554 -- its behavior or value (SPARK RM 6.9(10,11)). 555 556 else 557 Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref); 558 end if; 559 end Check_Ghost_Context; 560 561 ---------------------------- 562 -- Check_Ghost_Overriding -- 563 ---------------------------- 564 565 procedure Check_Ghost_Overriding 566 (Subp : Entity_Id; 567 Overridden_Subp : Entity_Id) 568 is 569 Deriv_Typ : Entity_Id; 570 Over_Subp : Entity_Id; 571 572 begin 573 if Present (Subp) and then Present (Overridden_Subp) then 574 Over_Subp := Ultimate_Alias (Overridden_Subp); 575 Deriv_Typ := Find_Dispatching_Type (Subp); 576 577 -- A Ghost primitive of a non-Ghost type extension cannot override an 578 -- inherited non-Ghost primitive (SPARK RM 6.9(8)). 579 580 if Is_Ghost_Entity (Subp) 581 and then Present (Deriv_Typ) 582 and then not Is_Ghost_Entity (Deriv_Typ) 583 and then not Is_Ghost_Entity (Over_Subp) 584 and then not Is_Abstract_Subprogram (Over_Subp) 585 then 586 Error_Msg_N ("incompatible overriding in effect", Subp); 587 588 Error_Msg_Sloc := Sloc (Over_Subp); 589 Error_Msg_N ("\& declared # as non-ghost subprogram", Subp); 590 591 Error_Msg_Sloc := Sloc (Subp); 592 Error_Msg_N ("\overridden # with ghost subprogram", Subp); 593 end if; 594 595 -- A non-Ghost primitive of a type extension cannot override an 596 -- inherited Ghost primitive (SPARK RM 6.9(8)). 597 598 if Is_Ghost_Entity (Over_Subp) 599 and then not Is_Ghost_Entity (Subp) 600 and then not Is_Abstract_Subprogram (Subp) 601 then 602 Error_Msg_N ("incompatible overriding in effect", Subp); 603 604 Error_Msg_Sloc := Sloc (Over_Subp); 605 Error_Msg_N ("\& declared # as ghost subprogram", Subp); 606 607 Error_Msg_Sloc := Sloc (Subp); 608 Error_Msg_N ("\overridden # with non-ghost subprogram", Subp); 609 end if; 610 611 if Present (Deriv_Typ) 612 and then not Is_Ignored_Ghost_Entity (Deriv_Typ) 613 then 614 -- When a tagged type is either non-Ghost or checked Ghost and 615 -- one of its primitives overrides an inherited operation, the 616 -- overridden operation of the ancestor type must be ignored Ghost 617 -- if the primitive is ignored Ghost (SPARK RM 6.9(17)). 618 619 if Is_Ignored_Ghost_Entity (Subp) then 620 621 -- Both the parent subprogram and overriding subprogram are 622 -- ignored Ghost. 623 624 if Is_Ignored_Ghost_Entity (Over_Subp) then 625 null; 626 627 -- The parent subprogram carries policy Check 628 629 elsif Is_Checked_Ghost_Entity (Over_Subp) then 630 Error_Msg_N 631 ("incompatible ghost policies in effect", Subp); 632 633 Error_Msg_Sloc := Sloc (Over_Subp); 634 Error_Msg_N 635 ("\& declared # with ghost policy `Check`", Subp); 636 637 Error_Msg_Sloc := Sloc (Subp); 638 Error_Msg_N 639 ("\overridden # with ghost policy `Ignore`", Subp); 640 641 -- The parent subprogram is non-Ghost 642 643 else 644 Error_Msg_N 645 ("incompatible ghost policies in effect", Subp); 646 647 Error_Msg_Sloc := Sloc (Over_Subp); 648 Error_Msg_N ("\& declared # as non-ghost subprogram", Subp); 649 650 Error_Msg_Sloc := Sloc (Subp); 651 Error_Msg_N 652 ("\overridden # with ghost policy `Ignore`", Subp); 653 end if; 654 655 -- When a tagged type is either non-Ghost or checked Ghost and 656 -- one of its primitives overrides an inherited operation, the 657 -- the primitive of the tagged type must be ignored Ghost if the 658 -- overridden operation is ignored Ghost (SPARK RM 6.9(17)). 659 660 elsif Is_Ignored_Ghost_Entity (Over_Subp) then 661 662 -- Both the parent subprogram and the overriding subprogram are 663 -- ignored Ghost. 664 665 if Is_Ignored_Ghost_Entity (Subp) then 666 null; 667 668 -- The overriding subprogram carries policy Check 669 670 elsif Is_Checked_Ghost_Entity (Subp) then 671 Error_Msg_N 672 ("incompatible ghost policies in effect", Subp); 673 674 Error_Msg_Sloc := Sloc (Over_Subp); 675 Error_Msg_N 676 ("\& declared # with ghost policy `Ignore`", Subp); 677 678 Error_Msg_Sloc := Sloc (Subp); 679 Error_Msg_N 680 ("\overridden # with Ghost policy `Check`", Subp); 681 682 -- The overriding subprogram is non-Ghost 683 684 else 685 Error_Msg_N 686 ("incompatible ghost policies in effect", Subp); 687 688 Error_Msg_Sloc := Sloc (Over_Subp); 689 Error_Msg_N 690 ("\& declared # with ghost policy `Ignore`", Subp); 691 692 Error_Msg_Sloc := Sloc (Subp); 693 Error_Msg_N 694 ("\overridden # with non-ghost subprogram", Subp); 695 end if; 696 end if; 697 end if; 698 end if; 699 end Check_Ghost_Overriding; 700 701 --------------------------- 702 -- Check_Ghost_Primitive -- 703 --------------------------- 704 705 procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is 706 begin 707 -- The Ghost policy in effect at the point of declaration of a primitive 708 -- operation and a tagged type must match (SPARK RM 6.9(16)). 709 710 if Is_Tagged_Type (Typ) then 711 if Is_Checked_Ghost_Entity (Prim) 712 and then Is_Ignored_Ghost_Entity (Typ) 713 then 714 Error_Msg_N ("incompatible ghost policies in effect", Prim); 715 716 Error_Msg_Sloc := Sloc (Typ); 717 Error_Msg_NE 718 ("\tagged type & declared # with ghost policy `Ignore`", 719 Prim, Typ); 720 721 Error_Msg_Sloc := Sloc (Prim); 722 Error_Msg_N 723 ("\primitive subprogram & declared # with ghost policy `Check`", 724 Prim); 725 726 elsif Is_Ignored_Ghost_Entity (Prim) 727 and then Is_Checked_Ghost_Entity (Typ) 728 then 729 Error_Msg_N ("incompatible ghost policies in effect", Prim); 730 731 Error_Msg_Sloc := Sloc (Typ); 732 Error_Msg_NE 733 ("\tagged type & declared # with ghost policy `Check`", 734 Prim, Typ); 735 736 Error_Msg_Sloc := Sloc (Prim); 737 Error_Msg_N 738 ("\primitive subprogram & declared # with ghost policy `Ignore`", 739 Prim); 740 end if; 741 end if; 742 end Check_Ghost_Primitive; 743 744 ---------------------------- 745 -- Check_Ghost_Refinement -- 746 ---------------------------- 747 748 procedure Check_Ghost_Refinement 749 (State : Node_Id; 750 State_Id : Entity_Id; 751 Constit : Node_Id; 752 Constit_Id : Entity_Id) 753 is 754 begin 755 if Is_Ghost_Entity (State_Id) then 756 if Is_Ghost_Entity (Constit_Id) then 757 758 -- The Ghost policy in effect at the point of abstract state 759 -- declaration and constituent must match (SPARK RM 6.9(15)). 760 761 if Is_Checked_Ghost_Entity (State_Id) 762 and then Is_Ignored_Ghost_Entity (Constit_Id) 763 then 764 Error_Msg_Sloc := Sloc (Constit); 765 SPARK_Msg_N ("incompatible ghost policies in effect", State); 766 767 SPARK_Msg_NE 768 ("\abstract state & declared with ghost policy `Check`", 769 State, State_Id); 770 SPARK_Msg_NE 771 ("\constituent & declared # with ghost policy `Ignore`", 772 State, Constit_Id); 773 774 elsif Is_Ignored_Ghost_Entity (State_Id) 775 and then Is_Checked_Ghost_Entity (Constit_Id) 776 then 777 Error_Msg_Sloc := Sloc (Constit); 778 SPARK_Msg_N ("incompatible ghost policies in effect", State); 779 780 SPARK_Msg_NE 781 ("\abstract state & declared with ghost policy `Ignore`", 782 State, State_Id); 783 SPARK_Msg_NE 784 ("\constituent & declared # with ghost policy `Check`", 785 State, Constit_Id); 786 end if; 787 788 -- A constituent of a Ghost abstract state must be a Ghost entity 789 -- (SPARK RM 7.2.2(12)). 790 791 else 792 SPARK_Msg_NE 793 ("constituent of ghost state & must be ghost", 794 Constit, State_Id); 795 end if; 796 end if; 797 end Check_Ghost_Refinement; 798 799 ---------------------- 800 -- Check_Ghost_Type -- 801 ---------------------- 802 803 procedure Check_Ghost_Type (Typ : Entity_Id) is 804 Conc_Typ : Entity_Id; 805 Full_Typ : Entity_Id; 806 807 begin 808 if Is_Ghost_Entity (Typ) then 809 Conc_Typ := Empty; 810 Full_Typ := Typ; 811 812 if Is_Single_Concurrent_Type (Typ) then 813 Conc_Typ := Anonymous_Object (Typ); 814 Full_Typ := Conc_Typ; 815 816 elsif Is_Concurrent_Type (Typ) then 817 Conc_Typ := Typ; 818 end if; 819 820 -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this 821 -- legality rule first to give a finer-grained diagnostic. 822 823 if Present (Conc_Typ) then 824 Error_Msg_N ("ghost type & cannot be concurrent", Conc_Typ); 825 end if; 826 827 -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7)) 828 829 if Is_Effectively_Volatile (Full_Typ) then 830 Error_Msg_N ("ghost type & cannot be volatile", Full_Typ); 831 end if; 832 end if; 833 end Check_Ghost_Type; 834 835 ------------------ 836 -- Ghost_Entity -- 837 ------------------ 838 839 function Ghost_Entity (Ref : Node_Id) return Entity_Id is 840 Obj_Ref : constant Node_Id := Ultimate_Prefix (Ref); 841 842 begin 843 -- When the reference denotes a subcomponent, recover the related whole 844 -- object (SPARK RM 6.9(1)). 845 846 if Is_Entity_Name (Obj_Ref) then 847 return Entity (Obj_Ref); 848 849 -- Otherwise the reference cannot possibly denote a Ghost entity 850 851 else 852 return Empty; 853 end if; 854 end Ghost_Entity; 855 856 -------------------------------- 857 -- Implements_Ghost_Interface -- 858 -------------------------------- 859 860 function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is 861 Iface_Elmt : Elmt_Id; 862 863 begin 864 -- Traverse the list of interfaces looking for a Ghost interface 865 866 if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then 867 Iface_Elmt := First_Elmt (Interfaces (Typ)); 868 while Present (Iface_Elmt) loop 869 if Is_Ghost_Entity (Node (Iface_Elmt)) then 870 return True; 871 end if; 872 873 Next_Elmt (Iface_Elmt); 874 end loop; 875 end if; 876 877 return False; 878 end Implements_Ghost_Interface; 879 880 ---------------- 881 -- Initialize -- 882 ---------------- 883 884 procedure Initialize is 885 begin 886 Ignored_Ghost_Nodes.Init; 887 888 -- Set the soft link which enables Atree.Mark_New_Ghost_Node to record 889 -- an ignored Ghost node or entity. 890 891 Set_Ignored_Ghost_Recording_Proc (Record_Ignored_Ghost_Node'Access); 892 end Initialize; 893 894 ------------------------ 895 -- Install_Ghost_Mode -- 896 ------------------------ 897 898 procedure Install_Ghost_Mode (Mode : Ghost_Mode_Type) is 899 begin 900 Install_Ghost_Region (Mode, Empty); 901 end Install_Ghost_Mode; 902 903 -------------------------- 904 -- Install_Ghost_Region -- 905 -------------------------- 906 907 procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is 908 begin 909 -- The context is already within an ignored Ghost region. Maintain the 910 -- start of the outermost ignored Ghost region. 911 912 if Present (Ignored_Ghost_Region) then 913 null; 914 915 -- The current region is the outermost ignored Ghost region. Save its 916 -- starting node. 917 918 elsif Present (N) and then Mode = Ignore then 919 Ignored_Ghost_Region := N; 920 921 -- Otherwise the current region is not ignored, nothing to save 922 923 else 924 Ignored_Ghost_Region := Empty; 925 end if; 926 927 Ghost_Mode := Mode; 928 end Install_Ghost_Region; 929 930 procedure Install_Ghost_Region (Mode : Name_Id; N : Node_Id) is 931 begin 932 Install_Ghost_Region (Name_To_Ghost_Mode (Mode), N); 933 end Install_Ghost_Region; 934 935 ------------------------- 936 -- Is_Ghost_Assignment -- 937 ------------------------- 938 939 function Is_Ghost_Assignment (N : Node_Id) return Boolean is 940 Id : Entity_Id; 941 942 begin 943 -- An assignment statement is Ghost when its target denotes a Ghost 944 -- entity. 945 946 if Nkind (N) = N_Assignment_Statement then 947 Id := Ghost_Entity (Name (N)); 948 949 return Present (Id) and then Is_Ghost_Entity (Id); 950 end if; 951 952 return False; 953 end Is_Ghost_Assignment; 954 955 -------------------------- 956 -- Is_Ghost_Declaration -- 957 -------------------------- 958 959 function Is_Ghost_Declaration (N : Node_Id) return Boolean is 960 Id : Entity_Id; 961 962 begin 963 -- A declaration is Ghost when it elaborates a Ghost entity or is 964 -- subject to pragma Ghost. 965 966 if Is_Declaration (N) then 967 Id := Defining_Entity (N); 968 969 return Is_Ghost_Entity (Id) or else Is_Subject_To_Ghost (N); 970 end if; 971 972 return False; 973 end Is_Ghost_Declaration; 974 975 --------------------- 976 -- Is_Ghost_Pragma -- 977 --------------------- 978 979 function Is_Ghost_Pragma (N : Node_Id) return Boolean is 980 begin 981 return Is_Checked_Ghost_Pragma (N) or else Is_Ignored_Ghost_Pragma (N); 982 end Is_Ghost_Pragma; 983 984 ----------------------------- 985 -- Is_Ghost_Procedure_Call -- 986 ----------------------------- 987 988 function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean is 989 Id : Entity_Id; 990 991 begin 992 -- A procedure call is Ghost when it invokes a Ghost procedure 993 994 if Nkind (N) = N_Procedure_Call_Statement then 995 Id := Ghost_Entity (Name (N)); 996 997 return Present (Id) and then Is_Ghost_Entity (Id); 998 end if; 999 1000 return False; 1001 end Is_Ghost_Procedure_Call; 1002 1003 --------------------------- 1004 -- Is_Ignored_Ghost_Unit -- 1005 --------------------------- 1006 1007 function Is_Ignored_Ghost_Unit (N : Node_Id) return Boolean is 1008 function Ultimate_Original_Node (Nod : Node_Id) return Node_Id; 1009 -- Obtain the original node of arbitrary node Nod following a potential 1010 -- chain of rewritings. 1011 1012 ---------------------------- 1013 -- Ultimate_Original_Node -- 1014 ---------------------------- 1015 1016 function Ultimate_Original_Node (Nod : Node_Id) return Node_Id is 1017 Res : Node_Id := Nod; 1018 begin 1019 while Original_Node (Res) /= Res loop 1020 Res := Original_Node (Res); 1021 end loop; 1022 1023 return Res; 1024 end Ultimate_Original_Node; 1025 1026 -- Start of processing for Is_Ignored_Ghost_Unit 1027 1028 begin 1029 -- Inspect the original node of the unit in case removal of ignored 1030 -- Ghost code has already taken place. 1031 1032 return 1033 Nkind (N) = N_Compilation_Unit 1034 and then Is_Ignored_Ghost_Entity 1035 (Defining_Entity (Ultimate_Original_Node (Unit (N)))); 1036 end Is_Ignored_Ghost_Unit; 1037 1038 ------------------------- 1039 -- Is_Subject_To_Ghost -- 1040 ------------------------- 1041 1042 function Is_Subject_To_Ghost (N : Node_Id) return Boolean is 1043 function Enables_Ghostness (Arg : Node_Id) return Boolean; 1044 -- Determine whether aspect or pragma argument Arg enables "ghostness" 1045 1046 ----------------------- 1047 -- Enables_Ghostness -- 1048 ----------------------- 1049 1050 function Enables_Ghostness (Arg : Node_Id) return Boolean is 1051 Expr : Node_Id; 1052 1053 begin 1054 Expr := Arg; 1055 1056 if Nkind (Expr) = N_Pragma_Argument_Association then 1057 Expr := Get_Pragma_Arg (Expr); 1058 end if; 1059 1060 -- Determine whether the expression of the aspect or pragma is static 1061 -- and denotes True. 1062 1063 if Present (Expr) then 1064 Preanalyze_And_Resolve (Expr); 1065 1066 return 1067 Is_OK_Static_Expression (Expr) 1068 and then Is_True (Expr_Value (Expr)); 1069 1070 -- Otherwise Ghost defaults to True 1071 1072 else 1073 return True; 1074 end if; 1075 end Enables_Ghostness; 1076 1077 -- Local variables 1078 1079 Id : constant Entity_Id := Defining_Entity (N); 1080 Asp : Node_Id; 1081 Decl : Node_Id; 1082 Prev_Id : Entity_Id; 1083 1084 -- Start of processing for Is_Subject_To_Ghost 1085 1086 begin 1087 -- The related entity of the declaration has not been analyzed yet, do 1088 -- not inspect its attributes. 1089 1090 if Ekind (Id) = E_Void then 1091 null; 1092 1093 elsif Is_Ghost_Entity (Id) then 1094 return True; 1095 1096 -- The completion of a type or a constant is not fully analyzed when the 1097 -- reference to the Ghost entity is resolved. Because the completion is 1098 -- not marked as Ghost yet, inspect the partial view. 1099 1100 elsif Is_Record_Type (Id) 1101 or else Ekind (Id) = E_Constant 1102 or else (Nkind (N) = N_Object_Declaration 1103 and then Constant_Present (N)) 1104 then 1105 Prev_Id := Incomplete_Or_Partial_View (Id); 1106 1107 if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then 1108 return True; 1109 end if; 1110 end if; 1111 1112 -- Examine the aspect specifications (if any) looking for aspect Ghost 1113 1114 if Permits_Aspect_Specifications (N) then 1115 Asp := First (Aspect_Specifications (N)); 1116 while Present (Asp) loop 1117 if Chars (Identifier (Asp)) = Name_Ghost then 1118 return Enables_Ghostness (Expression (Asp)); 1119 end if; 1120 1121 Next (Asp); 1122 end loop; 1123 end if; 1124 1125 Decl := Empty; 1126 1127 -- When the context is a [generic] package declaration, pragma Ghost 1128 -- resides in the visible declarations. 1129 1130 if Nkind (N) in N_Generic_Package_Declaration | N_Package_Declaration 1131 then 1132 Decl := First (Visible_Declarations (Specification (N))); 1133 1134 -- When the context is a package or a subprogram body, pragma Ghost 1135 -- resides in the declarative part. 1136 1137 elsif Nkind (N) in N_Package_Body | N_Subprogram_Body then 1138 Decl := First (Declarations (N)); 1139 1140 -- Otherwise pragma Ghost appears in the declarations following N 1141 1142 elsif Is_List_Member (N) then 1143 Decl := Next (N); 1144 end if; 1145 1146 while Present (Decl) loop 1147 if Nkind (Decl) = N_Pragma 1148 and then Pragma_Name (Decl) = Name_Ghost 1149 then 1150 return 1151 Enables_Ghostness (First (Pragma_Argument_Associations (Decl))); 1152 1153 -- A source construct ends the region where pragma Ghost may appear, 1154 -- stop the traversal. Check the original node as source constructs 1155 -- may be rewritten into something else by expansion. 1156 1157 elsif Comes_From_Source (Original_Node (Decl)) then 1158 exit; 1159 end if; 1160 1161 Next (Decl); 1162 end loop; 1163 1164 return False; 1165 end Is_Subject_To_Ghost; 1166 1167 ---------- 1168 -- Lock -- 1169 ---------- 1170 1171 procedure Lock is 1172 begin 1173 Ignored_Ghost_Nodes.Release; 1174 Ignored_Ghost_Nodes.Locked := True; 1175 end Lock; 1176 1177 ----------------------------------- 1178 -- Mark_And_Set_Ghost_Assignment -- 1179 ----------------------------------- 1180 1181 procedure Mark_And_Set_Ghost_Assignment (N : Node_Id) is 1182 -- A ghost assignment is an assignment whose left-hand side denotes a 1183 -- ghost object. Subcomponents are not marked "ghost", so we need to 1184 -- find the containing "whole" object. So, for "P.X.Comp (J) := ...", 1185 -- where P is a package, X is a record, and Comp is an array, we need 1186 -- to check the ghost flags of X. 1187 1188 Orig_Lhs : constant Node_Id := Name (N); 1189 begin 1190 -- Ghost assignments are irrelevant when the expander is inactive, and 1191 -- processing them in that mode can lead to spurious errors. 1192 1193 if Expander_Active then 1194 if not Analyzed (Orig_Lhs) 1195 and then Nkind (Orig_Lhs) = N_Indexed_Component 1196 and then Nkind (Prefix (Orig_Lhs)) = N_Selected_Component 1197 and then Nkind (Prefix (Prefix (Orig_Lhs))) = 1198 N_Indexed_Component 1199 then 1200 Analyze (Orig_Lhs); 1201 end if; 1202 1203 -- Make sure Lhs is at least preanalyzed, so we can tell whether 1204 -- it denotes a ghost variable. In some cases we need to do a full 1205 -- analysis, or else the back end gets confused. Note that in the 1206 -- preanalysis case, we are preanalyzing a copy of the left-hand 1207 -- side name, temporarily attached to the tree. 1208 1209 declare 1210 Lhs : constant Node_Id := 1211 (if Analyzed (Orig_Lhs) then Orig_Lhs 1212 else New_Copy_Tree (Orig_Lhs)); 1213 begin 1214 if not Analyzed (Lhs) then 1215 Set_Name (N, Lhs); 1216 Set_Parent (Lhs, N); 1217 Preanalyze_Without_Errors (Lhs); 1218 Set_Name (N, Orig_Lhs); 1219 end if; 1220 1221 declare 1222 Whole : constant Node_Id := Whole_Object_Ref (Lhs); 1223 Id : Entity_Id; 1224 begin 1225 if Is_Entity_Name (Whole) then 1226 Id := Entity (Whole); 1227 1228 if Present (Id) then 1229 -- Left-hand side denotes a Checked ghost entity, so 1230 -- install the region. 1231 1232 if Is_Checked_Ghost_Entity (Id) then 1233 Install_Ghost_Region (Check, N); 1234 1235 -- Left-hand side denotes an Ignored ghost entity, so 1236 -- install the region, and mark the assignment statement 1237 -- as an ignored ghost assignment, so it will be removed 1238 -- later. 1239 1240 elsif Is_Ignored_Ghost_Entity (Id) then 1241 Install_Ghost_Region (Ignore, N); 1242 Set_Is_Ignored_Ghost_Node (N); 1243 Record_Ignored_Ghost_Node (N); 1244 end if; 1245 end if; 1246 end if; 1247 end; 1248 end; 1249 end if; 1250 end Mark_And_Set_Ghost_Assignment; 1251 1252 ----------------------------- 1253 -- Mark_And_Set_Ghost_Body -- 1254 ----------------------------- 1255 1256 procedure Mark_And_Set_Ghost_Body 1257 (N : Node_Id; 1258 Spec_Id : Entity_Id) 1259 is 1260 Body_Id : constant Entity_Id := Defining_Entity (N); 1261 Policy : Name_Id := No_Name; 1262 1263 begin 1264 -- A body becomes Ghost when it is subject to aspect or pragma Ghost 1265 1266 if Is_Subject_To_Ghost (N) then 1267 Policy := Policy_In_Effect (Name_Ghost); 1268 1269 -- A body declared within a Ghost region is automatically Ghost 1270 -- (SPARK RM 6.9(2)). 1271 1272 elsif Ghost_Mode = Check then 1273 Policy := Name_Check; 1274 1275 elsif Ghost_Mode = Ignore then 1276 Policy := Name_Ignore; 1277 1278 -- Inherit the "ghostness" of the previous declaration when the body 1279 -- acts as a completion. 1280 1281 elsif Present (Spec_Id) then 1282 if Is_Checked_Ghost_Entity (Spec_Id) then 1283 Policy := Name_Check; 1284 1285 elsif Is_Ignored_Ghost_Entity (Spec_Id) then 1286 Policy := Name_Ignore; 1287 end if; 1288 end if; 1289 1290 -- The Ghost policy in effect at the point of declaration and at the 1291 -- point of completion must match (SPARK RM 6.9(14)). 1292 1293 Check_Ghost_Completion 1294 (Prev_Id => Spec_Id, 1295 Compl_Id => Body_Id); 1296 1297 -- Mark the body as its formals as Ghost 1298 1299 Mark_Ghost_Declaration_Or_Body (N, Policy); 1300 1301 -- Install the appropriate Ghost region 1302 1303 Install_Ghost_Region (Policy, N); 1304 end Mark_And_Set_Ghost_Body; 1305 1306 ----------------------------------- 1307 -- Mark_And_Set_Ghost_Completion -- 1308 ----------------------------------- 1309 1310 procedure Mark_And_Set_Ghost_Completion 1311 (N : Node_Id; 1312 Prev_Id : Entity_Id) 1313 is 1314 Compl_Id : constant Entity_Id := Defining_Entity (N); 1315 Policy : Name_Id := No_Name; 1316 1317 begin 1318 -- A completion elaborated in a Ghost region is automatically Ghost 1319 -- (SPARK RM 6.9(2)). 1320 1321 if Ghost_Mode = Check then 1322 Policy := Name_Check; 1323 1324 elsif Ghost_Mode = Ignore then 1325 Policy := Name_Ignore; 1326 1327 -- The completion becomes Ghost when its initial declaration is also 1328 -- Ghost. 1329 1330 elsif Is_Checked_Ghost_Entity (Prev_Id) then 1331 Policy := Name_Check; 1332 1333 elsif Is_Ignored_Ghost_Entity (Prev_Id) then 1334 Policy := Name_Ignore; 1335 end if; 1336 1337 -- The Ghost policy in effect at the point of declaration and at the 1338 -- point of completion must match (SPARK RM 6.9(14)). 1339 1340 Check_Ghost_Completion 1341 (Prev_Id => Prev_Id, 1342 Compl_Id => Compl_Id); 1343 1344 -- Mark the completion as Ghost 1345 1346 Mark_Ghost_Declaration_Or_Body (N, Policy); 1347 1348 -- Install the appropriate Ghost region 1349 1350 Install_Ghost_Region (Policy, N); 1351 end Mark_And_Set_Ghost_Completion; 1352 1353 ------------------------------------ 1354 -- Mark_And_Set_Ghost_Declaration -- 1355 ------------------------------------ 1356 1357 procedure Mark_And_Set_Ghost_Declaration (N : Node_Id) is 1358 Par_Id : Entity_Id; 1359 Policy : Name_Id := No_Name; 1360 1361 begin 1362 -- A declaration becomes Ghost when it is subject to aspect or pragma 1363 -- Ghost. 1364 1365 if Is_Subject_To_Ghost (N) then 1366 Policy := Policy_In_Effect (Name_Ghost); 1367 1368 -- A declaration elaborated in a Ghost region is automatically Ghost 1369 -- (SPARK RM 6.9(2)). 1370 1371 elsif Ghost_Mode = Check then 1372 Policy := Name_Check; 1373 1374 elsif Ghost_Mode = Ignore then 1375 Policy := Name_Ignore; 1376 1377 -- A child package or subprogram declaration becomes Ghost when its 1378 -- parent is Ghost (SPARK RM 6.9(2)). 1379 1380 elsif Nkind (N) in N_Generic_Function_Renaming_Declaration 1381 | N_Generic_Package_Declaration 1382 | N_Generic_Package_Renaming_Declaration 1383 | N_Generic_Procedure_Renaming_Declaration 1384 | N_Generic_Subprogram_Declaration 1385 | N_Package_Declaration 1386 | N_Package_Renaming_Declaration 1387 | N_Subprogram_Declaration 1388 | N_Subprogram_Renaming_Declaration 1389 and then Present (Parent_Spec (N)) 1390 then 1391 Par_Id := Defining_Entity (Unit (Parent_Spec (N))); 1392 1393 if Is_Checked_Ghost_Entity (Par_Id) then 1394 Policy := Name_Check; 1395 1396 elsif Is_Ignored_Ghost_Entity (Par_Id) then 1397 Policy := Name_Ignore; 1398 end if; 1399 end if; 1400 1401 -- Mark the declaration and its formals as Ghost 1402 1403 Mark_Ghost_Declaration_Or_Body (N, Policy); 1404 1405 -- Install the appropriate Ghost region 1406 1407 Install_Ghost_Region (Policy, N); 1408 end Mark_And_Set_Ghost_Declaration; 1409 1410 -------------------------------------- 1411 -- Mark_And_Set_Ghost_Instantiation -- 1412 -------------------------------------- 1413 1414 procedure Mark_And_Set_Ghost_Instantiation 1415 (N : Node_Id; 1416 Gen_Id : Entity_Id) 1417 is 1418 procedure Check_Ghost_Actuals; 1419 -- Check the context of ghost actuals 1420 1421 ------------------------- 1422 -- Check_Ghost_Actuals -- 1423 ------------------------- 1424 1425 procedure Check_Ghost_Actuals is 1426 Assoc : Node_Id := First (Generic_Associations (N)); 1427 Act : Node_Id; 1428 1429 begin 1430 while Present (Assoc) loop 1431 if Nkind (Assoc) /= N_Others_Choice then 1432 Act := Explicit_Generic_Actual_Parameter (Assoc); 1433 1434 -- Within a nested instantiation, a defaulted actual is an 1435 -- empty association, so nothing to check. 1436 1437 if No (Act) then 1438 null; 1439 1440 elsif Comes_From_Source (Act) 1441 and then Nkind (Act) in N_Has_Etype 1442 and then Present (Etype (Act)) 1443 and then Is_Ghost_Entity (Etype (Act)) 1444 then 1445 Check_Ghost_Context (Etype (Act), Act); 1446 end if; 1447 end if; 1448 1449 Next (Assoc); 1450 end loop; 1451 end Check_Ghost_Actuals; 1452 1453 -- Local variables 1454 1455 Policy : Name_Id := No_Name; 1456 1457 begin 1458 -- An instantiation becomes Ghost when it is subject to pragma Ghost 1459 1460 if Is_Subject_To_Ghost (N) then 1461 Policy := Policy_In_Effect (Name_Ghost); 1462 1463 -- An instantiation declaration within a Ghost region is automatically 1464 -- Ghost (SPARK RM 6.9(2)). 1465 1466 elsif Ghost_Mode = Check then 1467 Policy := Name_Check; 1468 1469 elsif Ghost_Mode = Ignore then 1470 Policy := Name_Ignore; 1471 1472 -- Inherit the "ghostness" of the generic unit 1473 1474 elsif Is_Checked_Ghost_Entity (Gen_Id) then 1475 Policy := Name_Check; 1476 1477 elsif Is_Ignored_Ghost_Entity (Gen_Id) then 1478 Policy := Name_Ignore; 1479 end if; 1480 1481 -- Mark the instantiation as Ghost 1482 1483 Mark_Ghost_Declaration_Or_Body (N, Policy); 1484 1485 -- Install the appropriate Ghost region 1486 1487 Install_Ghost_Region (Policy, N); 1488 1489 -- Check Ghost actuals. Given that this routine is unconditionally 1490 -- invoked with subprogram and package instantiations, this check 1491 -- verifies the context of all the ghost entities passed in generic 1492 -- instantiations. 1493 1494 Check_Ghost_Actuals; 1495 end Mark_And_Set_Ghost_Instantiation; 1496 1497 --------------------------------------- 1498 -- Mark_And_Set_Ghost_Procedure_Call -- 1499 --------------------------------------- 1500 1501 procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id) is 1502 Id : Entity_Id; 1503 1504 begin 1505 -- A procedure call becomes Ghost when the procedure being invoked is 1506 -- Ghost. Install the Ghost mode of the procedure. 1507 1508 Id := Ghost_Entity (Name (N)); 1509 1510 if Present (Id) then 1511 if Is_Checked_Ghost_Entity (Id) then 1512 Install_Ghost_Region (Check, N); 1513 1514 elsif Is_Ignored_Ghost_Entity (Id) then 1515 Install_Ghost_Region (Ignore, N); 1516 1517 Set_Is_Ignored_Ghost_Node (N); 1518 Record_Ignored_Ghost_Node (N); 1519 end if; 1520 end if; 1521 end Mark_And_Set_Ghost_Procedure_Call; 1522 1523 ----------------------- 1524 -- Mark_Ghost_Clause -- 1525 ----------------------- 1526 1527 procedure Mark_Ghost_Clause (N : Node_Id) is 1528 Nam : Node_Id := Empty; 1529 1530 begin 1531 if Nkind (N) = N_Use_Package_Clause then 1532 Nam := Name (N); 1533 1534 elsif Nkind (N) = N_Use_Type_Clause then 1535 Nam := Subtype_Mark (N); 1536 1537 elsif Nkind (N) = N_With_Clause then 1538 Nam := Name (N); 1539 end if; 1540 1541 if Present (Nam) 1542 and then Is_Entity_Name (Nam) 1543 and then Present (Entity (Nam)) 1544 and then Is_Ignored_Ghost_Entity (Entity (Nam)) 1545 then 1546 Set_Is_Ignored_Ghost_Node (N); 1547 Record_Ignored_Ghost_Node (N); 1548 end if; 1549 end Mark_Ghost_Clause; 1550 1551 ------------------------------------ 1552 -- Mark_Ghost_Declaration_Or_Body -- 1553 ------------------------------------ 1554 1555 procedure Mark_Ghost_Declaration_Or_Body 1556 (N : Node_Id; 1557 Mode : Name_Id) 1558 is 1559 Id : constant Entity_Id := Defining_Entity (N); 1560 1561 Mark_Formals : Boolean := False; 1562 Param : Node_Id; 1563 Param_Id : Entity_Id; 1564 1565 begin 1566 -- Mark the related node and its entity 1567 1568 if Mode = Name_Check then 1569 Mark_Formals := True; 1570 Set_Is_Checked_Ghost_Entity (Id); 1571 1572 elsif Mode = Name_Ignore then 1573 Mark_Formals := True; 1574 Set_Is_Ignored_Ghost_Entity (Id); 1575 Set_Is_Ignored_Ghost_Node (N); 1576 Record_Ignored_Ghost_Node (N); 1577 end if; 1578 1579 -- Mark all formal parameters when the related node denotes a subprogram 1580 -- or a body. The traversal is performed via the specification because 1581 -- the related subprogram or body may be unanalyzed. 1582 1583 -- ??? could extra formal parameters cause a Ghost leak? 1584 1585 if Mark_Formals 1586 and then Nkind (N) in N_Abstract_Subprogram_Declaration 1587 | N_Formal_Abstract_Subprogram_Declaration 1588 | N_Formal_Concrete_Subprogram_Declaration 1589 | N_Generic_Subprogram_Declaration 1590 | N_Subprogram_Body 1591 | N_Subprogram_Body_Stub 1592 | N_Subprogram_Declaration 1593 | N_Subprogram_Renaming_Declaration 1594 then 1595 Param := First (Parameter_Specifications (Specification (N))); 1596 while Present (Param) loop 1597 Param_Id := Defining_Entity (Param); 1598 1599 if Mode = Name_Check then 1600 Set_Is_Checked_Ghost_Entity (Param_Id); 1601 1602 elsif Mode = Name_Ignore then 1603 Set_Is_Ignored_Ghost_Entity (Param_Id); 1604 end if; 1605 1606 Next (Param); 1607 end loop; 1608 end if; 1609 end Mark_Ghost_Declaration_Or_Body; 1610 1611 ----------------------- 1612 -- Mark_Ghost_Pragma -- 1613 ----------------------- 1614 1615 procedure Mark_Ghost_Pragma 1616 (N : Node_Id; 1617 Id : Entity_Id) 1618 is 1619 begin 1620 -- A pragma becomes Ghost when it encloses a Ghost entity or relates to 1621 -- a Ghost entity. 1622 1623 if Is_Checked_Ghost_Entity (Id) then 1624 Set_Is_Checked_Ghost_Pragma (N); 1625 1626 elsif Is_Ignored_Ghost_Entity (Id) then 1627 Set_Is_Ignored_Ghost_Pragma (N); 1628 Set_Is_Ignored_Ghost_Node (N); 1629 Record_Ignored_Ghost_Node (N); 1630 end if; 1631 end Mark_Ghost_Pragma; 1632 1633 ------------------------- 1634 -- Mark_Ghost_Renaming -- 1635 ------------------------- 1636 1637 procedure Mark_Ghost_Renaming 1638 (N : Node_Id; 1639 Id : Entity_Id) 1640 is 1641 Policy : Name_Id := No_Name; 1642 1643 begin 1644 -- A renaming becomes Ghost when it renames a Ghost entity 1645 1646 if Is_Checked_Ghost_Entity (Id) then 1647 Policy := Name_Check; 1648 1649 elsif Is_Ignored_Ghost_Entity (Id) then 1650 Policy := Name_Ignore; 1651 end if; 1652 1653 Mark_Ghost_Declaration_Or_Body (N, Policy); 1654 end Mark_Ghost_Renaming; 1655 1656 ------------------------ 1657 -- Name_To_Ghost_Mode -- 1658 ------------------------ 1659 1660 function Name_To_Ghost_Mode (Mode : Name_Id) return Ghost_Mode_Type is 1661 begin 1662 if Mode = Name_Check then 1663 return Check; 1664 1665 elsif Mode = Name_Ignore then 1666 return Ignore; 1667 1668 -- Otherwise the mode must denote one of the following: 1669 -- 1670 -- * Disable indicates that the Ghost policy in effect is Disable 1671 -- 1672 -- * None or No_Name indicates that the associated construct is not 1673 -- subject to any Ghost annotation. 1674 1675 else 1676 pragma Assert (Mode in Name_Disable | Name_None | No_Name); 1677 return None; 1678 end if; 1679 end Name_To_Ghost_Mode; 1680 1681 ------------------------------- 1682 -- Record_Ignored_Ghost_Node -- 1683 ------------------------------- 1684 1685 procedure Record_Ignored_Ghost_Node (N : Node_Or_Entity_Id) is 1686 begin 1687 -- Save all "top level" ignored Ghost nodes which can be safely replaced 1688 -- with a null statement. Note that there is need to save other kinds of 1689 -- nodes because those will always be enclosed by some top level ignored 1690 -- Ghost node. 1691 1692 if Is_Body (N) 1693 or else Is_Declaration (N) 1694 or else Nkind (N) in N_Generic_Instantiation 1695 | N_Push_Pop_xxx_Label 1696 | N_Raise_xxx_Error 1697 | N_Representation_Clause 1698 | N_Statement_Other_Than_Procedure_Call 1699 | N_Call_Marker 1700 | N_Freeze_Entity 1701 | N_Freeze_Generic_Entity 1702 | N_Itype_Reference 1703 | N_Pragma 1704 | N_Procedure_Call_Statement 1705 | N_Use_Package_Clause 1706 | N_Use_Type_Clause 1707 | N_Variable_Reference_Marker 1708 | N_With_Clause 1709 then 1710 -- Only ignored Ghost nodes must be recorded in the table 1711 1712 pragma Assert (Is_Ignored_Ghost_Node (N)); 1713 Ignored_Ghost_Nodes.Append (N); 1714 end if; 1715 end Record_Ignored_Ghost_Node; 1716 1717 ------------------------------- 1718 -- Remove_Ignored_Ghost_Code -- 1719 ------------------------------- 1720 1721 procedure Remove_Ignored_Ghost_Code is 1722 procedure Remove_Ignored_Ghost_Node (N : Node_Id); 1723 -- Eliminate ignored Ghost node N from the tree 1724 1725 ------------------------------- 1726 -- Remove_Ignored_Ghost_Node -- 1727 ------------------------------- 1728 1729 procedure Remove_Ignored_Ghost_Node (N : Node_Id) is 1730 begin 1731 -- The generation and processing of ignored Ghost nodes may cause the 1732 -- same node to be saved multiple times. Reducing the number of saves 1733 -- to one involves costly solutions such as a hash table or the use 1734 -- of a flag shared by all nodes. To solve this problem, the removal 1735 -- machinery allows for multiple saves, but does not eliminate a node 1736 -- which has already been eliminated. 1737 1738 if Nkind (N) = N_Null_Statement then 1739 null; 1740 1741 -- Otherwise the ignored Ghost node must be eliminated 1742 1743 else 1744 -- Only ignored Ghost nodes must be eliminated from the tree 1745 1746 pragma Assert (Is_Ignored_Ghost_Node (N)); 1747 1748 -- Eliminate the node by rewriting it into null. Another option 1749 -- is to remove it from the tree, however multiple corner cases 1750 -- emerge which have be dealt individually. 1751 1752 Rewrite (N, Make_Null_Statement (Sloc (N))); 1753 1754 -- Eliminate any aspects hanging off the ignored Ghost node 1755 1756 Remove_Aspects (N); 1757 end if; 1758 end Remove_Ignored_Ghost_Node; 1759 1760 -- Start of processing for Remove_Ignored_Ghost_Code 1761 1762 begin 1763 for Index in Ignored_Ghost_Nodes.First .. Ignored_Ghost_Nodes.Last loop 1764 Remove_Ignored_Ghost_Node (Ignored_Ghost_Nodes.Table (Index)); 1765 end loop; 1766 end Remove_Ignored_Ghost_Code; 1767 1768 -------------------------- 1769 -- Restore_Ghost_Region -- 1770 -------------------------- 1771 1772 procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id) is 1773 begin 1774 Ghost_Mode := Mode; 1775 Ignored_Ghost_Region := N; 1776 end Restore_Ghost_Region; 1777 1778 -------------------- 1779 -- Set_Ghost_Mode -- 1780 -------------------- 1781 1782 procedure Set_Ghost_Mode (N : Node_Or_Entity_Id) is 1783 procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id); 1784 -- Install the Ghost mode of entity Id 1785 1786 -------------------------------- 1787 -- Set_Ghost_Mode_From_Entity -- 1788 -------------------------------- 1789 1790 procedure Set_Ghost_Mode_From_Entity (Id : Entity_Id) is 1791 begin 1792 if Is_Checked_Ghost_Entity (Id) then 1793 Install_Ghost_Mode (Check); 1794 elsif Is_Ignored_Ghost_Entity (Id) then 1795 Install_Ghost_Mode (Ignore); 1796 else 1797 Install_Ghost_Mode (None); 1798 end if; 1799 end Set_Ghost_Mode_From_Entity; 1800 1801 -- Local variables 1802 1803 Id : Entity_Id; 1804 1805 -- Start of processing for Set_Ghost_Mode 1806 1807 begin 1808 -- The Ghost mode of an assignment statement depends on the Ghost mode 1809 -- of the target. 1810 1811 if Nkind (N) = N_Assignment_Statement then 1812 Id := Ghost_Entity (Name (N)); 1813 1814 if Present (Id) then 1815 Set_Ghost_Mode_From_Entity (Id); 1816 end if; 1817 1818 -- The Ghost mode of a body or a declaration depends on the Ghost mode 1819 -- of its defining entity. 1820 1821 elsif Is_Body (N) or else Is_Declaration (N) then 1822 Set_Ghost_Mode_From_Entity (Defining_Entity (N)); 1823 1824 -- The Ghost mode of an entity depends on the entity itself 1825 1826 elsif Nkind (N) in N_Entity then 1827 Set_Ghost_Mode_From_Entity (N); 1828 1829 -- The Ghost mode of a [generic] freeze node depends on the Ghost mode 1830 -- of the entity being frozen. 1831 1832 elsif Nkind (N) in N_Freeze_Entity | N_Freeze_Generic_Entity then 1833 Set_Ghost_Mode_From_Entity (Entity (N)); 1834 1835 -- The Ghost mode of a pragma depends on the associated entity. The 1836 -- property is encoded in the pragma itself. 1837 1838 elsif Nkind (N) = N_Pragma then 1839 if Is_Checked_Ghost_Pragma (N) then 1840 Install_Ghost_Mode (Check); 1841 elsif Is_Ignored_Ghost_Pragma (N) then 1842 Install_Ghost_Mode (Ignore); 1843 else 1844 Install_Ghost_Mode (None); 1845 end if; 1846 1847 -- The Ghost mode of a procedure call depends on the Ghost mode of the 1848 -- procedure being invoked. 1849 1850 elsif Nkind (N) = N_Procedure_Call_Statement then 1851 Id := Ghost_Entity (Name (N)); 1852 1853 if Present (Id) then 1854 Set_Ghost_Mode_From_Entity (Id); 1855 end if; 1856 end if; 1857 end Set_Ghost_Mode; 1858 1859 ------------------------- 1860 -- Set_Is_Ghost_Entity -- 1861 ------------------------- 1862 1863 procedure Set_Is_Ghost_Entity (Id : Entity_Id) is 1864 Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); 1865 begin 1866 if Policy = Name_Check then 1867 Set_Is_Checked_Ghost_Entity (Id); 1868 elsif Policy = Name_Ignore then 1869 Set_Is_Ignored_Ghost_Entity (Id); 1870 end if; 1871 end Set_Is_Ghost_Entity; 1872 1873 ---------------------- 1874 -- Whole_Object_Ref -- 1875 ---------------------- 1876 1877 function Whole_Object_Ref (Ref : Node_Id) return Node_Id is 1878 begin 1879 if Nkind (Ref) in N_Indexed_Component | N_Slice 1880 or else (Nkind (Ref) = N_Selected_Component 1881 and then Is_Object_Reference (Prefix (Ref))) 1882 then 1883 if Is_Access_Type (Etype (Prefix (Ref))) then 1884 return Ref; 1885 else 1886 return Whole_Object_Ref (Prefix (Ref)); 1887 end if; 1888 else 1889 return Ref; 1890 end if; 1891 end Whole_Object_Ref; 1892 1893end Ghost; 1894