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