[Ada] Implement Ghost entities

This patch implements the following rules related to aspect/pragma Ghost:

A statement or pragma is said to be a "ghost statement" if
   * it is a pragma which encloses a name denoting a ghost entity or which
     specifies an aspect of a ghost entity.

A ghost entity shall only be referenced:
   * from within an aspect specification (either an aspect_specification or an
     aspect-specifying pragma)
   * within a renaming_declaration which either renames a ghost entity or
     occurs within a ghost subprogram or package.

A ghost entity shall not be referenced within an aspect specification
(including an aspect-specifying pragma) which specifies an aspect of a
non-ghost entity except in the following cases:
   * the reference occurs within an assertion expression
   * the specified aspect is either Global, Depends, Refined_Global,
     Refined_Depends, Initializes, or Refined_State.

The Ghost assertion policies in effect at the declaration of an overriding
ghost primitive subprogram of a tagged type and at the declaration of the
(ancestor's or progenitor's) primitive subprogram corresponding to the
overridden inherited subprogram shall be the same.

If the Ghost assertion policy in effect at the point of an a reference to a
Ghost entity which occurs within an assertion expression is Ignore, then the
assertion policy which governs the assertion expression shall also be Ignore.

------------
-- Source --
------------

--  lr11.ads

--  6.9(11) - A ghost entity shall only be referenced within a with_clause

with Ghost_Pack;                                                     --  OK

package LR11

  --  6.9(11) - A ghost entity shall only be referenced within an aspect
  --  specification.

  with Initializes => Ghost_Obj                                      --  OK
is
   procedure Force_Body;

   --  6.9(11) - A ghost entity shall only be referenced within an aspect
   --  specifying pragma.

   pragma Global ((Input => Ghost_Obj));                             --  OK

   type Many_Comps is array (Integer range <>) of Integer;

   Ghost_Obj : Integer := 1 with Ghost;
   type Ghost_Typ is null record with Ghost;

   --  6.9(11) - A ghost entity shall only be referenced from within an
   --  assertion expression.

   pragma Assert (Ghost_Obj = 1);                                    --  OK

   --  6.9(11) - A ghost entity shall only be referenced within the declaration
   --  or completion of a ghost entity.

   Ghost_Obj_2 : Integer := Ghost_Obj + 1 with Ghost;                --  OK
   Ghost_Obj_3 : constant Integer with Ghost;

   type Ghost_Typ_1 (Discr : Integer := Ghost_Obj)                   --  OK
   is tagged limited record
      Comp : Integer;
   end record with Ghost;

   type Ghost_Typ_2 (Discr : Integer := Ghost_Obj)                   --  OK
   is tagged limited private with Ghost;

   type Ghost_Typ_3 is record
      Comp : Integer := Ghost_Obj;                                   --  OK
   end record with Ghost;

   type Ghost_Typ_4 is record
      Comp : Many_Comps (1 .. Ghost_Obj) := (others => 1);           --  OK
   end record with Ghost;

   procedure Ghost_Proc (Formal : Integer := Ghost_Obj) with Ghost;  --  OK

   --  6.9(11) - A ghost entity shall only be referenced from within a
   --  renaming declaration which either renames a Ghost entity...

   Ghost_Ren_Obj : Integer renames Ghost_Obj;                        --  OK
   procedure Ghost_Ren_Proc (Formal : Integer := Ghost_Obj)          --  OK
     renames Ghost_Proc;                                             --  OK

private
   Ghost_Obj_3 : constant Integer := Ghost_Obj + 1;                  --  OK
   type Ghost_Typ_2 (Discr : Integer := Ghost_Obj)                   --  OK
   is tagged limited null record;
end LR11;

--  lr11.adb

package body LR11 is
   procedure Force_Body is begin null; end Force_Body;

   procedure Ghost_Proc (Formal : Integer := Ghost_Obj) is
      Living_Var : Integer := 2;

      --  6.9(11) - A ghost entity shall only be referenced within a renaming
      --  declaration which occurs within a Ghost subprogram or package.

      Living_Ren : Integer renames Living_Var;                       --  OK

      procedure Nested_Ghost_Proc (Formal : Integer) with Ghost is
      begin
         null;
      end Nested_Ghost_Proc;

   begin
      --  6.9(11) - A ghost entity shall only be referenced within a ghost
      --  statement.

      --  assignment

      Ghost_Obj := Ghost_Obj + 1;                                    --  OK

      --  procedure call

      Nested_Ghost_Proc (Ghost_Obj);                                 --  OK
   end Ghost_Proc;
end LR11;

--  lr12.ads

package LR12
  with Abstract_State => (Ghost_State with Ghost),

       --  6.9(12) - A ghost entity shall not be referenced within an aspect
       --  specification which specifies an aspect of a non-ghost entity except
       --  when the specified aspect is Initializes.

       Initializes => Ghost_Obj                                      --  OK
is
   Ghost_Obj : Integer := 1 with Ghost;

   function Living_Func_1 (Input : Integer) return Integer

          --  6.9(12) - A ghost entity shall not be referenced within an aspect
          --  specification which specifies an aspect of a non-ghost entity
          --  except when the reference occurs within an assertion expression.

     with Pre     => Ghost_Obj + Input > 0,                          --  OK
          Post    => Ghost_Obj + Living_Func_1'Result > 0,           --  OK

          --  6.9(12) - A ghost entity shall not be referenced within an aspect
          --  specification which specifies an aspect of a non-ghost entity
          --  except when the specified aspect is Global, Depends.

          Global  => (Input => Ghost_State),                         --  OK
          Depends => (Living_Func_1'Result => (Input, Ghost_State)); --  OK

   --  Same as above, but with pragmas

   function Living_Func_2 (Input : Integer) return Integer;
   pragma Pre (Ghost_Obj + Input > 0);                               --  OK
   pragma Post (Ghost_Obj + Living_Func_2'Result > 0);               --  OK
   pragma Global ((Input => Ghost_State));                           --  OK
   pragma Depends ((Living_Func_2'Result => (Input, Ghost_State)));  --  OK
end LR12;

--  lr12.adb

package body LR12

       --  6.9(12) - A ghost entity shall not be referenced within an aspect
       --  specification which specifies an aspect of a non-ghost entity except
       --  when the specified aspect is Refined_State.

  with Refined_State => (Ghost_State => Ghost_Constit)               --  OK
is
   Ghost_Constit : Integer := 2 with Ghost;

   function Living_Func_1 (Input : Integer) return Integer

          --  6.9(12) - A ghost entity shall not be referenced within an
          --  aspect specification which specifies an aspect of a non-ghost
          --  entity except when the specified aspect is Refined_Global,
          --  Refined_Depends.

     with Refined_Global  => (Input => Ghost_Constit),               --  OK
          Refined_Depends =>
            (Living_Func_1'Result => (Input, Ghost_Constit))         --  OK
   is
   begin
      return Input + 1;
   end Living_Func_1;

   --  Same as above, but with pragmas

   function Living_Func_2 (Input : Integer) return Integer is
      pragma Refined_Global ((Input => Ghost_Constit));              --  OK
      pragma Refined_Depends
               ((Living_Func_2'Result => (Input, Ghost_Constit)));   --  OK
   begin
      return Input + 1;
   end Living_Func_2;
end LR12;

-- lr17.ads

pragma Assertion_Policy (Ghost => Check);

package LR17 is
   type Root_Typ is tagged null record;
   procedure Prim_Typ_Op (Formal : in out Root_Typ) with Ghost;

   type Root_Iface is interface;
   procedure Prim_Iface_Op (Formal : in out Root_Iface) is abstract with Ghost;
end LR17;

--  lr17.adb

package body LR17 is
   procedure Prim_Typ_Op (Formal : in out Root_Typ) is
   begin
      null;
   end Prim_Typ_Op;
end LR17;

--  lr17b.ads

pragma Assertion_Policy (Ghost => Ignore);

with LR17; use LR17;

package LR17b is

   --  6.9(17) - The Ghost assertion policies in effect at the declaration of
   --  an overriding ghost primitive subprogram of a tagged type and at the
   --  declaration of the (ancestor's or progenitor's) primitive subprogram
   --  corresponding to the overridden inherited subprogram shall be the same.

   type Child_Typ is new Root_Typ and Root_Iface with null record;

   procedure Prim_Typ_Op (Formal : in out Child_Typ) with Ghost;     --  Error
   procedure Prim_Iface_Op (Formal : in out Child_Typ) with Ghost;   --  Error
end LR17b;

--  lr17b.adb

pragma Assertion_Policy (Ghost => Ignore);

package body LR17b is
   procedure Prim_Typ_Op (Formal : in out Child_Typ) is
   begin
      null;
   end Prim_Typ_Op;

   procedure Prim_Iface_Op (Formal : in out Child_Typ) is
   begin
      null;
   end Prim_Iface_Op;
end LR17b;

--  lr18a.ads

pragma Assertion_Policy (Pre => Check, Ghost => Ignore);

package LR18a is
   Ghost_Obj : Integer := 1 with Ghost;

   --  6.9(18) - If the Ghost assertion policy in effect at the point of an a
   --  reference to a Ghost entity which occurs within an assertion expression
   --  is Ignore, then the assertion policy which governs the assertion
   --  expression shall [also] be Ignore.

   procedure Proc
     with Pre => Ghost_Obj > 10;                                     --  Error
end LR18a;

--  lr18a.adb

package body LR18a is
   procedure Proc is begin null; end Proc;
end LR18a;

--  pack_post.ads

pragma Assertion_Policy (Post => Ignore, Ghost => Ignore);

package Pack_Post is
   function Func (Val : Natural) return Natural
     with Post => Is_Zero (Func'Result);

   function Func2 (Val : Natural) return Natural
     with Post => Is_Zero2 (Func2'Result);

   function Func3 (Val : Natural) return Natural
     with Post => Is_Zero2 (Func3'Result),
          Ghost;

   function Is_Zero (Val : Natural) return Boolean;

   function Is_Zero2 (Val : Natural) return Boolean
     with Ghost;
end Pack_Post;

--  pack_post.adb

pragma Assertion_Policy (Ghost => Ignore);

package body Pack_Post is
   function Func (Val : Natural) return Natural is
   begin
      return Val + 10;
   end Func;

   function Func2 (Val : Natural) return Natural is
   begin
      return Val + 10;
   end Func2;

   function Func3 (Val : Natural) return Natural is
   begin
      return Val + 10;
   end Func3;

   function Is_Zero (Val : Natural) return Boolean is
   begin
      return Val = 0;
   end Is_Zero;

   function Is_Zero2 (Val : Natural) return Boolean is
   begin
      return Val = 0;
   end Is_Zero2;
end Pack_Post;

--  test_post.adb

pragma Assertion_Policy (Ghost => Ignore);

with Ada.Text_IO; use Ada.Text_IO;
with Pack_Post;   use Pack_Post;

procedure Test_Post is
begin
   --  Ghost variable + assertion expression

   begin
      declare
         Val : constant Natural := Func (1)
           with Ghost;
      begin
         Put_Line ("OK");
      end;

   exception
      when others => Put_Line ("ERROR 1: policy Post is Ignore");
   end;

   --  Living variable + assertion expression with Ghost function call

   begin
      declare
         Val : constant Natural := Func2 (1);
      begin
         Put_Line ("OK");
      end;

   exception
      when others => Put_Line ("ERROR 2: policy Post is Ignore");
   end;

   --  Ghost variable + Ghost assertion expression

   begin
      declare
         Val : constant Natural := Func3 (1)
           with Ghost;
      begin
         Put_Line ("OK");
      end;

   exception
      when others => Put_Line ("ERROR 3: policy Post is Ignore");
   end;
end Test_Post;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c lr11.adb
$ gcc -c lr12.adb
$ gcc -c lr17b.adb
$ gcc -c lr18a.adb
$ gnatmake -q -gnata test_post.adb
$ ./test_post
lr17b.ads:14:14: incompatible ghost policies in effect
lr17b.ads:14:14: "Prim_Typ_Op" declared at lr17.ads:5 with ghost policy "Check"
lr17b.ads:14:14: overridden at line 14 with ghost policy "Ignore"
lr17b.ads:15:14: incompatible ghost policies in effect
lr17b.ads:15:14: "Prim_Iface_Op" declared at lr17.ads:8 with ghost policy
  "Check"
lr17b.ads:15:14: overridden at line 15 with ghost policy "Ignore"
lr18a.ads:12:18: incompatible ghost policies in effect
lr18a.ads:12:18: ghost entity "Ghost_Obj" has policy "Ignore"
lr18a.ads:12:18: assertion expression has policy "Check"
OK
OK
OK

Tested on x86_64-pc-linux-gnu, committed on trunk

2015-05-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch3.adb (Expand_N_Full_Type_Declaration): Capture, set and
	restore the Ghost mode.
	(Expand_N_Object_Declaration): Capture, set and restore the Ghost mode.
	(Freeze_Type): Update the call to Set_Ghost_Mode.
	(Restore_Globals): New routine.
	* exp_ch5.adb Add with and use clauses for Ghost.
	(Expand_N_Assignment_Statement): Capture, set and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* exp_ch6.adb Add with and use clauses for Ghost.
	(Expand_N_Procedure_Call_Statement): Capture, set and
	restore the Ghost mode.
	(Expand_N_Subprogram_Body):
	Code cleanup. Capture, set and restore the Ghost mode.
	(Expand_N_Subprogram_Declaration): Capture, set and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* exp_ch7.adb Add with and use clauses for Ghost.
	(Expand_N_Package_Body): Capture, set and restore the Ghost mode.
	(Expand_N_Package_Declaration): Capture, set and restore the
	Ghost mode.
	(Wrap_HSS_In_Block): Create a proper identifier for the block.
	* exp_ch8.adb Add with and use clauses for Ghost.
	(Expand_N_Exception_Renaming_Declaration): Code
	cleanup. Capture, set and restore the Ghost mode.
	(Expand_N_Object_Renaming_Declaration): Capture, set and restore
	the Ghost mode.
	(Expand_N_Package_Renaming_Declaration): Capture, set and restore the
	Ghost mode.
	(Expand_N_Subprogram_Renaming_Declaration): Capture, set and
	restore the Ghost mode.
	* exp_ch11.adb (Expand_N_Exception_Declaration): Code
	cleanup. Capture, set and restore the Ghost mode.
	* exp_disp.adb (Make_DT): Update the call to Set_Ghost_Mode. Do
	not initialize the dispatch table slot of a Ghost subprogram.
	* exp_prag.adb Add with and use clauses for Ghost.
	(Expand_Pragma_Check): Capture, set and restore the Ghost mode.
	(Expand_Pragma_Contract_Cases): Capture, set and restore the
	Ghost mode.
	(Expand_Pragma_Initial_Condition): Capture, set and
	restore the Ghost mode.
	(Expand_Pragma_Loop_Variant): Capture,
	set and restore the Ghost mode.
	(Restore_Globals): New routine.
	* exp_util.adb Add with and use clauses for Ghost.
	(Make_Predicate_Call): Code cleanup. Capture, set and restore
	the Ghost mode.
	(Restore_Globals): New routine.
	* freeze.adb (Freeze_Entity): Code cleanup. Update the call
	to Set_Ghost_Mode.
	* ghost.adb Add with and use clause for Sem_Prag.
	(Check_Ghost_Completion): Code cleanup.
	(Check_Ghost_Overriding): New routine.
	(Check_Ghost_Policy): Code cleanup.
	(Ghost_Entity): New routine.
	(Is_Ghost_Declaration): Removed.
	(Is_Ghost_Statement_Or_Pragma): Removed.
	(Is_OK_Context): Reimplemented.
	(Is_OK_Declaration): New routine.
	(Is_OK_Pragma): New routine.
	(Is_OK_Statement): New routine.
	(Mark_Full_View_As_Ghost): New routine.
	(Mark_Pragma_As_Ghost): New routine.
	(Mark_Renaming_As_Ghost): New routine.
	(Propagate_Ignored_Ghost_Code): Update the comment on usage.
	(Set_From_Entity): New routine.
	(Set_From_Policy): New routine.
	(Set_Ghost_Mode): This routine now handles pragmas and freeze nodes.
	(Set_Ghost_Mode_For_Freeze): Removed.
	(Set_Ghost_Mode_From_Entity): New routine.
	(Set_Ghost_Mode_From_Policy): Removed.
	* ghost.ads (Check_Ghost_Overriding): New routine.
	(Mark_Full_View_As_Ghost): New routine.
	(Mark_Pragma_As_Ghost): New routine.
	(Mark_Renaming_As_Ghost): New routine.
	(Set_Ghost_Mode): Update the parameter profile. Update the
	comment on usage.
	(Set_Ghost_Mode_For_Freeze): Removed.
	(Set_Ghost_Mode_From_Entity): New routine.
	* sem_ch3.adb (Analyze_Full_Type_Declaration):
	Capture and restore the Ghost mode. Mark a type
	as Ghost regardless of whether it comes from source.
	(Analyze_Incomplete_Type_Decl): Capture, set and restore the
	Ghost mode.
	(Analyze_Number_Declaration): Capture and restore the Ghost mode.
	(Analyze_Object_Declaration): Capture and restore the Ghost mode.
	(Analyze_Private_Extension_Declaration): Capture and
	restore the Ghost mode.
	(Analyze_Subtype_Declaration): Capture and restore the Ghost mode.
	(Process_Full_View): The full view inherits all Ghost-related
	attributes from the private view.
	(Restore_Globals): New routine.
	* sem_ch5.adb (Analyze_Assignment): Capture and restore the
	Ghost mode.
	(Restore_Globals): New routine.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration):
	Code cleanup. Capture and restore the Ghost mode. Mark a
	subprogram as Ghost regarless of whether it comes from source.
	(Analyze_Procedure_Call): Capture and restore the Ghost mode.
	(Analyze_Subprogram_Body_Helper): Capture and restore the Ghost mode.
	(Analyze_Subprogram_Declaration): Capture and restore the Ghost mode.
	(New_Overloaded_Entity): Ensure that a
	parent subprogram and an overriding subprogram have compatible
	Ghost policies.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Capture and restore
	the Ghost mode.
	(Analyze_Package_Declaration): Capture and
	restore the Ghost mode. Mark a package as Ghost when it is
	declared in a Ghost region.
	(Analyze_Private_Type_Declaration): Capture and restore the Ghost mode.
	(Restore_Globals): New routine.
	* sem_ch8.adb (Analyze_Exception_Renaming): Code
	reformatting. Capture and restore the Ghost mode. A renaming
	becomes Ghost when its name references a Ghost entity.
	(Analyze_Generic_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Object_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Package_Renaming): Capture and restore the Ghost mode. A
	renaming becomes Ghost when its name references a Ghost entity.
	(Analyze_Subprogram_Renaming): Capture and restore the Ghost
	mode. A renaming becomes Ghost when its name references a
	Ghost entity.
	* sem_ch11.adb (Analyze_Exception_Declaration): Capture, set
	and restore the Ghost mode.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration): Capture and
	restore the Ghost mode.
	(Analyze_Generic_Subprogram_Declaration):
	Capture and restore the Ghost mode.
	* sem_ch13.adb Add with and use clauses for Ghost.
	(Add_Invariant): New routine.
	(Add_Invariants): Factor out code.
	(Add_Predicate): New routine.
	(Add_Predicates): Factor out code.
	(Build_Invariant_Procedure_Declaration): Code cleanup. Capture,
	set and restore the Ghost mode.
	(Build_Invariant_Procedure): Code cleanup.
	(Build_Predicate_Functions): Capture, set and
	restore the Ghost mode. Mark the generated functions as Ghost.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
	Capture, set and restore the Ghost mode.
	(Analyze_External_Property_In_Decl_Part): Capture, set and restore
	the Ghost mode.
	(Analyze_Initial_Condition_In_Decl_Part):
	Capture, set and restore the Ghost mode.
	(Analyze_Pragma):
	Code cleanup. Capture, set and restore the Ghost mode. Flag
	pragmas Linker_Section, No_Return, Unmodified, Unreferenced and
	Unreferenced_Objects as illegal when it applies to both Ghost
	and living arguments. Pragma Ghost cannot apply to synchronized
	objects.
	(Check_Kind): Moved to the spec of Sem_Prag.
	(Process_Inline): Flag the pragma as illegal when it applies to
	both Ghost and living arguments.
	(Restore_Globals): New routine.
	* sem_prag.ads Add pragma Default_Initial_Condition
	to table Assertion_Expression_Pragma. Add new table
	Is_Aspect_Specifying_Pragma.
	(Check_Kind): Moved from body of Sem_Prag.
	* sem_util.adb Add with and use clauses for Ghost.
	(Build_Default_Init_Cond_Procedure_Body): Capture, set and restore
	the Ghost mode.
	(Build_Default_Init_Cond_Procedure_Declaration):
	Capture, set and restore the Ghost mode. Mark the default
	initial condition procedure as Ghost when it is declared
	in a Ghost region.
	(Is_Renaming_Declaration): New routine.
	(Policy_In_List): Account for the single argument version of
	Check_Pragma.
	* sem_util.ads (Is_Renaming_Declaration): New routine.
	* sinfo.adb (Is_Ghost_Pragma): New routine.
	(Set_Is_Ghost_Pragma): New routine.
	* sinfo.ads New attribute Is_Ghost_Pragma.
	(Is_Ghost_Pragma): New routine along with pragma Inline.
	(Set_Is_Ghost_Pragma): New routine along with pragma Inline.

[Ada] Implement Ghost entities

Commit Message

Patch