This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Implement Ghost entities


This patch implements aspect/pragma Ghost which is subject to the following
semantic and legality rules:

SPARK 2014 defines the Boolean-valued representation aspect Ghost. Ghost is an
aspect of all entities. An entity whose Ghost aspect is True is said to be a
ghost entity; terms such as "ghost function" or "ghost variable" are defined
analogously. In addition, a subcomponent of a ghost object is a ghost object.

The Ghost aspect of an entity declared inside of a ghost entity is defined to
be True. The Ghost aspect of an entity implicitly declared as part of the
explicit declaration of a ghost entity is defined to be True. The Ghost aspect
of a child of a ghost library unit is defined to be True.

A statement or pragma is said to be a "ghost statement" if
   * it occurs within a ghost subprogram or package; or
   * it is a call to a ghost procedure; or
   * it is an assignment statement whose target is a ghost variable; or
   * it is a pragma which encloses a name denoting a ghost entity or which
     specifies an aspect of a ghost entity.
A ghost subprogram profile and a non-ghost subprogram profile are not subtype
conformant.

The Ghost aspect may only be specified for the declaration of a subprogram, a
generic subprogram, a type, an object, a package, or a generic package. The
Ghost aspect may be specified via either an aspect_specification or via a
pragma. The representation pragma Ghost takes a single argument, a name
denoting one or more entities whose Ghost aspect is then specified to be True.

A Ghost aspect value of False shall not be explicitly specified except in a
confirming aspect specification.

A ghost type or object shall not be effectively volatile. A ghost object shall
not be imported or exported.

A type extension shall be a ghost type if and only if its parent type and all
of its progenitor types are ghost types.

A Ghost pragma which applies to a declaration occuring in the visible part of a
package shall not occur in the private part of that package.

A non-ghost library unit package or generic package specification shall not
require a completion solely because of ghost declarations.

A ghost entity shall only be referenced:
   * from within an assertion expression; or
   * within the declaration or completion of a ghost entity
   * within a ghost statement; or
   * within a with_clause.

If the Ghost assertion policy in effect at the point of the declaration of a
ghost entity is Ignore, then the Ghost assertion policy in effect at the point
of any reference to that entity shall be Ignore. If the Ghost assertion policy
in effect at the point of the declaration of a ghost variable is Check, then
the Ghost assertion policy in effect at the point of any assignment to a part
of that variable shall be Check.

An Assertion_Policy pragma specifying a Ghost assertion policy shall not occur
within a ghost subprogram or package. If a ghost entity has a completion then
the Ghost assertion policies in effect at the declaration and at the completion
of the entity shall be the same.

The Ghost assertion policies in effect at the declaration of a state
abstraction and at the declaration of each constituent of that abstraction
shall be the same.

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

--  ghost_entities.ads

package Ghost_Entities with SPARK_Mode is
   package LR7 with Ghost is
      procedure Error_1 with Ghost => False;
   end LR7;

   package LR8 is
      type Error_2 is null record with Ghost, Volatile;
   end LR8;

   package LR9 is
      type Iface is interface;
      type Ghost_Parent is tagged null record with Ghost;

      type Error_3 is new Ghost_Parent and Iface with Ghost with null record;
   end LR9;

   package LR10 is
      Error_4 : constant Integer;
   private
      Error_4 : constant Integer := 4 with Ghost;
   end LR10;

   package LR12 is
      Ghost_Obj : Integer := 12 with Ghost;
      Error_5   : constant Integer := Ghost_Obj + 12;
   end LR12;

   package LR13 is
      pragma Assertion_Policy (Ghost => Check);
      Error_6 : constant Integer with Ghost;
   private
      pragma Assertion_Policy (Ghost => Ignore);
      Error_6 : constant Integer := 6;
   end LR13;

   package LR14 with Ghost is
      pragma Assertion_Policy (Ghost => Check);
   end LR14;

   package LR15 with Abstract_State => (State with Ghost) is
      procedure Force_Body;
   private
      Error_7   : Integer := 1 with Part_Of => State;
      Ghost_Obj : Integer := 1 with Part_Of => State, Ghost;
   end LR15;
end Ghost_Entities;

--  ghost_entities.adb

package body Ghost_Entities with SPARK_Mode is
   package body LR7 is
      procedure Error_1 is begin null; end Error_1;
   end LR7;

   package body LR15
     with Refined_State => (State => (Error_7, Ghost_Obj))
   is
      procedure Force_Body is begin null; end Force_Body;
   end LR15;
end Ghost_Entities;

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

$ gcc -c ghost_entities.adb
ghost_entities.adb:7:39: constituent of ghost state "State" must be ghost
ghost_entities.ads:3:30: aspect "Ghost" with value False cannot appear in
  enabled ghost region
ghost_entities.ads:7:12: ghost type "Error_2" cannot be volatile
ghost_entities.ads:14:12: type extension "Error_3" cannot be ghost
ghost_entities.ads:14:12: interface type "Iface" is not ghost
ghost_entities.ads:14:27: type derived from tagged type must have extension
ghost_entities.ads:14:60: missing ";"
ghost_entities.ads:20:44: aspect "Ghost" must apply to declaration of deferred
  constant "Error_4"
ghost_entities.ads:25:39: ghost entity cannot appear in this context (SPARK RM
  6.9(12))
ghost_entities.ads:30:07: incompatible ghost policies in effect
ghost_entities.ads:30:07: "Error_6" declared with ghost policy Check
ghost_entities.ads:30:07: "Error_6" completed at line 33 with ghost policy
  Ignore
ghost_entities.ads:37:32: pragma "Check_Policy" cannot appear within ghost
  subprogram or package

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

2014-10-31  Hristian Kirtchev  <kirtchev@adacore.com>

	* aspects.adb Add an entry for aspect Ghost in table
	Canonical_Aspect.
	* aspects.ads Add an entry for aspect Ghost in tables
	Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names and
	Implementation_Defined_Aspect.
	* einfo.adb: Flags 277 and 278 are now in use.
	(Is_Checked_Ghost_Entity): New routine.
	(Is_Ghost_Entity): Removed.
	(Is_Ghost_Subprogram): Removed.
	(Is_Ignored_Ghost_Entity): New routine.
	(Set_Is_Checked_Ghost_Entity): New routine.
	(Set_Is_Ignored_Ghost_Entity): New routine.
	(Write_Entity_Flags): Output flags Is_Checked_Ghost_Entity and
	Is_Ignored_Ghost_Entity.
	* einfo.ads: Add new flags Is_Checked_Ghost_Entity
	and Is_Ignored_Ghost_Entity along with usage in nodes.
	(Is_Checked_Ghost_Entity): New routine and pragma Inline.
	(Is_Ghost_Entity): Removed along with synthesized flag
	description and usage in nodes.
	(Is_Ghost_Subprogram): Removed along with synthesized flag description
	and usage in nodes.
	(Is_Ignored_Ghost_Entity): New routine and pragma Inline.
	(Set_Is_Checked_Ghost_Entity): New routine and pragma Inline.
	(Set_Is_Ignored_Ghost_Entity): New routine and pragma Inline.
	* freeze.adb (Freeze_Entity): A Ghost type cannot be effectively
	volatile.
	* par-prag.adb Pragma Ghost does not need special handling by
	the parser.
	* repinfo.adb (List_Mechanisms): Remove the entry for convention Ghost.
	* sem_attr.adb (Analyze_Access_Attribute): Remove obsolete check.
	* sem_ch3.adb (Analyze_Full_Type_Declaration): Mark
	the type as Ghost when its enclosing context is Ghost.
	(Analyze_Incomplete_Type_Decl): Mark the type as Ghost when
	its enclosing context is Ghost.
	(Analyze_Number_Declaration): Mark the number as Ghost when its
	enclosing context is Ghost.
	(Analyze_Object_Declaration): Mark the object as Ghost when its
	enclosing context is Ghost. Verify the Ghost policy between
	initial declaration and completion of a deferred constant.
	(Analyze_Object_Contract): A Ghost variable cannot be effectively
	volatile, imported or exported.
	(Build_Derived_Record_Type): Mark a type extension as Ghost when it
	implements a Ghost interface.
	(Build_Record_Type): Inherit volatility and "ghostness" from
	the parent type.
	(Check_Completion): A Ghost entity declared
	in a non-Ghost package does not require completion in a body.
	(Implements_Ghost_Interface): New routine.
	(Process_Full_View): Inherit "ghostness" from the partial view. Verify
	the Ghost policy between the partial and full views. Verify the
	completion of a Ghost type extension.
	* sem_ch4.adb (Check_Ghost_Subprogram_Call): Removed.
	* sem_ch5.adb (Analyze_Assignment): Analyze the left hand side first.
	* sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Mark
	the subprogram as Ghost when its enclosing context is Ghost.
	(Analyze_Generic_Subprogram_Body): Mark the generic body as Ghost
	when its enclosing context is Ghost. Verify the Ghost policy
	between the spec and body.
	(Analyze_Subprogram_Body_Helper): Mark the body as Ghost when its
	enclosing context is Ghost. Verify the Ghost policy between the spec
	and body.
	(Check_Conformance): A Ghost subprogram profile and a non-Ghost
	subprogram profile are not subtype conformant.
	(Convention_Of): Removed.
	* sem_ch7.adb (Analyze_Package_Body_Helper): Inherit the
	"ghostness" from the spec. Verify the Ghost policy between
	the spec and body.
	(Analyze_Private_Type_Declaration): Mark the type as Ghost when its
	enclosing context is Ghost.
	(Requires_Completion_In_Body): New routine.
	(Unit_Requires_Body): Use Requires_Completion_In_Body.
	(Unit_Requires_Body_Info): Rename formal parameter P to Pack_Id, update
	comment on usage and all uses of P in the body. Use
	Requires_Completion_In_Body.
	* sem_ch7.ads (Unit_Requires_Body): Rename formal parameter P
	to Pack_Id, update comment on usage and all uses of P in the body.
	* sem_ch8.adb (Analyze_Exception_Renaming): Inherit the "ghostness"
	from the renamed excention.
	(Analyze_Generic_Renaming): Inherit the "ghostness" from the
	renamed generic subprogram.
	(Analyze_Object_Renaming): Inherit the "ghostness" from the renamed
	object.
	(Analyze_Package_Renaming): Inherit the "ghostness" from the
	renamed package.
	(Analyze_Subprogram_Renaming): Inherit the "ghostness" from the
	renamed subprogram.
	* sem_ch11.adb (Analyze_Exception_Declaration): Mark an exception
	as Ghost when its enclosing context is Ghost.
	* sem_ch12.adb (Analyze_Generic_Package_Declaration,
	Analyze_Generic_Subprogram_Declaration): Mark an exception as
	Ghost when its enclosing context is Ghost.
	(Preanalyze_Actuals): Remove obsolete check.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Ghost.
	(Check_Aspect_At_Freeze_Point): Aspects
	Depends and Global do no need special checking at freeze point.
	(Insert_After_SPARK_Mode): Update comment on usage.
	* sem_mech.adb (Set_Mechanisms): Remove the entry for convention Ghost.
	* sem_prag.adb Add an entry for pragma Ghost in table Sig_Flags.
	(Analyze_Abstract_State): Update the grammar of the pragma. Add
	formal parameter Pack_Id along with comment on usage. Mark an
	abstract state as Ghost when its enclosing context is Ghost. Add
	processing for option Ghost.
	(Analyze_Constituent): Verify
	that a Ghost abstract state is refined by Ghost constituents.
	(Analyze_Pragma): "Ghost" is now a valid policy. Add checks
	related to the use and placement of Check_Policy Ghost. Add
	processing for pragma Ghost.
	(Check_Ghost_Constituent): New routine.
	(Is_Valid_Assertion_Kind): "Ghost" is now a valid assertion.
	(Process_Convention): Remove obsolete check.
	(Set_Convention_From_Pragma): Remove the processing for convention
	Ghost.
	* sem_res.adb (Check_Ghost_Context): New routine.
	(Resolve_Call): Verify that a reference to a Ghost entity appears in a
	suitable context. Verify the Ghost polity between point of declaration
	and point of use.
	(Resolve_Entity_Name): Verify that a reference to
	a Ghost entity appears in a suitable context. Verify the Ghost
	polity between point of declaration and point of use.
	* sem_util.adb (Check_Ghost_Completion): New routine.
	(Check_Ghost_Derivation): New routine.
	(Incomplete_Or_Partial_View): New routine.
	(Incomplete_Or_Private_View): Removed.
	(Is_Ghost_Entity): New routine.
	(Is_Ghost_Statement_Or_Pragma): New routine.
	(Is_Subject_To_Ghost): New routine.
	(Policy_In_Effect): New routine.
	(Set_Is_Ghost_Entity): New routine.
	(Within_Ghost_Scope): New routine.
	* sem_util.ads (Check_Ghost_Completion): New routine.
	(Check_Ghost_Derivation): New routine.
	(Incomplete_Or_Partial_View): New routine.
	(Incomplete_Or_Private_View): Removed.
	(Is_Ghost_Entity): New routine.
	(Is_Ghost_Statement_Or_Pragma): New routine.
	(Is_Subject_To_Ghost): New routine.
	(Policy_In_Effect): New routine.
	(Set_Is_Ghost_Entity): New routine.
	(Within_Ghost_Scope): New routine.
	* snames.adb-tmpl (Get_Convention_Id): Remove the entry for
	convention Ghost.
	(Get_Convention_Name): Remove the entry for convention Ghost.
	* snames.ads-tmpl Remove the convention id for Ghost. Add a
	pragma id for Ghost.

Attachment: difs
Description: Text document


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]