[thirdparty/gcc.git] / gcc / ada / ghost.ads

------------------------------------------------------------------------------
--                                                                          --
--                         GNAT COMPILER COMPONENTS                         --
--                                                                          --
--                                G H O S T                                 --
--                                                                          --
--                                 S p e c                                  --
--                                                                          --
--          Copyright (C) 2014-2022, Free Software Foundation, Inc.         --
--                                                                          --
-- GNAT is free software;  you can  redistribute it  and/or modify it under --
-- terms of the  GNU General Public License as published  by the Free Soft- --
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License --
-- for  more details.  You should have  received  a copy of the GNU General --
-- Public License  distributed with GNAT; see file COPYING3.  If not, go to --
-- http://www.gnu.org/licenses for a complete copy of the license.          --
--                                                                          --
-- GNAT was originally developed  by the GNAT team at  New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc.      --
--                                                                          --
------------------------------------------------------------------------------

--  This package contains routines that deal with the static and runtime
--  semantics of Ghost entities.

with Opt;   use Opt;
with Types; use Types;

package Ghost is

   procedure Check_Ghost_Completion
     (Prev_Id  : Entity_Id;
      Compl_Id : Entity_Id);
   --  Verify that the Ghost policy of initial entity Prev_Id is compatible
   --  with the Ghost policy of completing entity Compl_Id. Emit an error if
   --  this is not the case.

   procedure Check_Ghost_Context
     (Ghost_Id  : Entity_Id;
      Ghost_Ref : Node_Id);
   --  Determine whether node Ghost_Ref appears within a Ghost-friendly context
   --  where Ghost entity Ghost_Id can safely reside.

   procedure Check_Ghost_Context_In_Generic_Association
     (Actual : Node_Id;
      Formal : Entity_Id);
   --  Check that if Actual contains references to ghost entities, generic
   --  formal parameter Formal is ghost (SPARK RM 6.9(10)).

   procedure Check_Ghost_Formal_Procedure_Or_Package
     (N          : Node_Id;
      Actual     : Entity_Id;
      Formal     : Entity_Id;
      Is_Default : Boolean := False);
   --  Verify that if generic formal procedure (resp. package) Formal is ghost,
   --  then Actual is not Empty and also a ghost procedure (resp. package)
   --  (SPARK RM 6.9(13-14)). The error if any is located on N. If
   --  Is_Default is False, N and Actual represent the actual parameter in an
   --  instantiation. Otherwise, they represent the default subprogram of a
   --  formal subprogram declaration.

   procedure Check_Ghost_Formal_Variable
     (Actual     : Node_Id;
      Formal     : Entity_Id;
      Is_Default : Boolean := False);
   --  Verify that if Formal (either an IN OUT generic formal parameter, or an
   --  IN generic formal parameter of access-to-variable type) is ghost, then
   --  Actual is a ghost object (SPARK RM 6.9(13-14)). Is_Default is True when
   --  Actual is the default expression of the formal object declaration.

   procedure Check_Ghost_Overriding
     (Subp            : Entity_Id;
      Overridden_Subp : Entity_Id);
   --  Verify that the Ghost policy of parent subprogram Overridden_Subp is
   --  compatible with the Ghost policy of overriding subprogram Subp. Emit
   --  an error if this is not the case.

   procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id);
   --  Verify that the Ghost policy of primitive operation Prim is the same as
   --  the Ghost policy of tagged type Typ. Emit an error if this is not the
   --  case.

   procedure Check_Ghost_Refinement
     (State      : Node_Id;
      State_Id   : Entity_Id;
      Constit    : Node_Id;
      Constit_Id : Entity_Id);
   --  Verify that the Ghost policy of constituent Constit_Id is compatible
   --  with the Ghost policy of abstract state State_I.

   procedure Check_Ghost_Type (Typ : Entity_Id);
   --  Verify that Ghost type Typ is neither concurrent, nor effectively
   --  volatile.

   function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
   --  Determine whether type Typ implements at least one Ghost interface

   procedure Initialize;
   --  Initialize internal tables

   procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
   pragma Inline (Install_Ghost_Region);
   --  Install a Ghost region described by mode Mode and ignored region start
   --  node N.

   function Is_Ghost_Assignment (N : Node_Id) return Boolean;
   --  Determine whether arbitrary node N denotes an assignment statement whose
   --  target is a Ghost entity.

   function Is_Ghost_Declaration (N : Node_Id) return Boolean;
   --  Determine whether arbitrary node N denotes a declaration which defines
   --  a Ghost entity.

   function Is_Ghost_Pragma (N : Node_Id) return Boolean;
   --  Determine whether arbitrary node N denotes a pragma which encloses a
   --  Ghost entity or is associated with a Ghost entity.

   function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean;
   --  Determine whether arbitrary node N denotes a procedure call invoking a
   --  Ghost procedure.

   function Is_Ignored_Ghost_Unit (N : Node_Id) return Boolean;
   --  Determine whether compilation unit N is subject to pragma Ghost with
   --  policy Ignore.

   procedure Lock;
   --  Lock internal tables before calling backend

   procedure Mark_And_Set_Ghost_Assignment (N : Node_Id);
   --  Mark assignment statement N as Ghost when:
   --
   --    * The left hand side denotes a Ghost entity
   --
   --  Install the Ghost mode of the assignment statement. This routine starts
   --  a Ghost region and must be used with routine Restore_Ghost_Region.

   procedure Mark_And_Set_Ghost_Body
     (N       : Node_Id;
      Spec_Id : Entity_Id);
   --  Mark package or subprogram body N as Ghost when:
   --
   --    * The body is subject to pragma Ghost
   --
   --    * The body completes a previous declaration whose spec denoted by
   --      Spec_Id is a Ghost entity.
   --
   --    * The body appears within a Ghost region
   --
   --  Install the Ghost mode of the body. This routine starts a Ghost region
   --  and must be used with routine Restore_Ghost_Region.

   procedure Mark_And_Set_Ghost_Completion
     (N       : Node_Id;
      Prev_Id : Entity_Id);
   --  Mark completion N of a deferred constant or private type [extension]
   --  Ghost when:
   --
   --    * The entity of the previous declaration denoted by Prev_Id is Ghost
   --
   --    * The completion appears within a Ghost region
   --
   --  Install the Ghost mode of the completion. This routine starts a Ghost
   --  region and must be used with routine Restore_Ghost_Region.

   procedure Mark_And_Set_Ghost_Declaration (N : Node_Id);
   --  Mark declaration N as Ghost when:
   --
   --    * The declaration is subject to pragma Ghost
   --
   --    * The declaration denotes a child package or subprogram and the parent
   --      is a Ghost unit.
   --
   --    * The declaration appears within a Ghost region
   --
   --  Install the Ghost mode of the declaration. This routine starts a Ghost
   --  region and must be used with routine Restore_Ghost_Region.

   procedure Mark_And_Set_Ghost_Instantiation
     (N      : Node_Id;
      Gen_Id : Entity_Id);
   --  Mark instantiation N as Ghost when:
   --
   --    * The instantiation is subject to pragma Ghost
   --
   --    * The generic template denoted by Gen_Id is Ghost
   --
   --    * The instantiation appears within a Ghost region
   --
   --  Install the Ghost mode of the instantiation. This routine starts a Ghost
   --  region and must be used with routine Restore_Ghost_Region.

   procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id);
   --  Mark procedure call N as Ghost when:
   --
   --    * The procedure being invoked is a Ghost entity
   --
   --  Install the Ghost mode of the procedure call. This routine starts a
   --  Ghost region and must be used with routine Restore_Ghost_Region.

   procedure Mark_Ghost_Clause (N : Node_Id);
   --  Mark use package, use type, or with clause N as Ghost when:
   --
   --    * The clause mentions a Ghost entity

   procedure Mark_Ghost_Pragma
     (N  : Node_Id;
      Id : Entity_Id);
   --  Mark pragma N as Ghost when:
   --
   --    * The pragma encloses Ghost entity Id
   --
   --    * The pragma is associated with Ghost entity Id

   procedure Mark_Ghost_Renaming
     (N  : Node_Id;
      Id : Entity_Id);
   --  Mark renaming declaration N as Ghost when:
   --
   --    * Renamed entity Id denotes a Ghost entity

   procedure Remove_Ignored_Ghost_Code;
   --  Remove all code marked as ignored Ghost from the trees of all qualifying
   --  units (SPARK RM 6.9(4)).
   --
   --  WARNING: this is a separate front end pass, care should be taken to keep
   --  it optimized.

   procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
   pragma Inline (Restore_Ghost_Region);
   --  Restore a Ghost region to a previous state described by mode Mode and
   --  ignored region start node N. This routine must be used in conjunction
   --  with the following routines:
   --
   --    Install_Ghost_Region
   --    Mark_And_Set_xxx
   --    Set_Ghost_Mode

   procedure Set_Ghost_Mode (N : Node_Or_Entity_Id);
   --  Install the Ghost mode of arbitrary node N. This routine starts a Ghost
   --  region and must be used with routine Restore_Ghost_Region.

   procedure Set_Is_Ghost_Entity (Id : Entity_Id);
   --  Set the relevant Ghost attributes of entity Id depending on the current
   --  Ghost assertion policy in effect.

end Ghost;
Commit	Line	Data
8636f52f HK	1	------------------------------------------------------------------------------
	2	-- --
	3	-- GNAT COMPILER COMPONENTS --
	4	-- --
	5	-- G H O S T --
	6	-- --
	7	-- S p e c --
	8	-- --
bc0b26b9	9	-- Copyright (C) 2014-2022, Free Software Foundation, Inc. --
8636f52f HK	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	-- This package contains routines that deal with the static and runtime
	27	-- semantics of Ghost entities.
	28
d65a80fd	29	with Opt; use Opt;
8636f52f HK	30	with Types; use Types;
	31
	32	package Ghost is
	33
8636f52f	34	procedure Check_Ghost_Completion
d65a80fd HK	35	(Prev_Id : Entity_Id;
	36	Compl_Id : Entity_Id);
	37	-- Verify that the Ghost policy of initial entity Prev_Id is compatible
	38	-- with the Ghost policy of completing entity Compl_Id. Emit an error if
	39	-- this is not the case.
	40
	41	procedure Check_Ghost_Context
	42	(Ghost_Id : Entity_Id;
	43	Ghost_Ref : Node_Id);
8636f52f HK	44	-- Determine whether node Ghost_Ref appears within a Ghost-friendly context
	45	-- where Ghost entity Ghost_Id can safely reside.
	46
be3bdaa1 YM	47	procedure Check_Ghost_Context_In_Generic_Association
	48	(Actual : Node_Id;
	49	Formal : Entity_Id);
	50	-- Check that if Actual contains references to ghost entities, generic
	51	-- formal parameter Formal is ghost (SPARK RM 6.9(10)).
	52
	53	procedure Check_Ghost_Formal_Procedure_Or_Package
	54	(N : Node_Id;
	55	Actual : Entity_Id;
	56	Formal : Entity_Id;
	57	Is_Default : Boolean := False);
	58	-- Verify that if generic formal procedure (resp. package) Formal is ghost,
	59	-- then Actual is not Empty and also a ghost procedure (resp. package)
	60	-- (SPARK RM 6.9(13-14)). The error if any is located on N. If
	61	-- Is_Default is False, N and Actual represent the actual parameter in an
	62	-- instantiation. Otherwise, they represent the default subprogram of a
	63	-- formal subprogram declaration.
	64
	65	procedure Check_Ghost_Formal_Variable
	66	(Actual : Node_Id;
	67	Formal : Entity_Id;
	68	Is_Default : Boolean := False);
	69	-- Verify that if Formal (either an IN OUT generic formal parameter, or an
	70	-- IN generic formal parameter of access-to-variable type) is ghost, then
	71	-- Actual is a ghost object (SPARK RM 6.9(13-14)). Is_Default is True when
	72	-- Actual is the default expression of the formal object declaration.
	73
241ebe89 HK	74	procedure Check_Ghost_Overriding
	75	(Subp : Entity_Id;
	76	Overridden_Subp : Entity_Id);
4179af27 HK	77	-- Verify that the Ghost policy of parent subprogram Overridden_Subp is
	78	-- compatible with the Ghost policy of overriding subprogram Subp. Emit
	79	-- an error if this is not the case.
	80
	81	procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id);
	82	-- Verify that the Ghost policy of primitive operation Prim is the same as
	83	-- the Ghost policy of tagged type Typ. Emit an error if this is not the
	84	-- case.
	85
	86	procedure Check_Ghost_Refinement
	87	(State : Node_Id;
	88	State_Id : Entity_Id;
	89	Constit : Node_Id;
	90	Constit_Id : Entity_Id);
	91	-- Verify that the Ghost policy of constituent Constit_Id is compatible
	92	-- with the Ghost policy of abstract state State_I.
241ebe89	93
a85dbeec HK	94	procedure Check_Ghost_Type (Typ : Entity_Id);
	95	-- Verify that Ghost type Typ is neither concurrent, nor effectively
	96	-- volatile.
	97
8636f52f HK	98	function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
	99	-- Determine whether type Typ implements at least one Ghost interface
	100
	101	procedure Initialize;
	102	-- Initialize internal tables
	103
9057bd6a HK	104	procedure Install_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
	105	pragma Inline (Install_Ghost_Region);
	106	-- Install a Ghost region described by mode Mode and ignored region start
	107	-- node N.
8636f52f	108
d65a80fd HK	109	function Is_Ghost_Assignment (N : Node_Id) return Boolean;
	110	-- Determine whether arbitrary node N denotes an assignment statement whose
	111	-- target is a Ghost entity.
241ebe89	112
d65a80fd HK	113	function Is_Ghost_Declaration (N : Node_Id) return Boolean;
	114	-- Determine whether arbitrary node N denotes a declaration which defines
	115	-- a Ghost entity.
241ebe89	116
d65a80fd HK	117	function Is_Ghost_Pragma (N : Node_Id) return Boolean;
	118	-- Determine whether arbitrary node N denotes a pragma which encloses a
	119	-- Ghost entity or is associated with a Ghost entity.
241ebe89	120
d65a80fd HK	121	function Is_Ghost_Procedure_Call (N : Node_Id) return Boolean;
	122	-- Determine whether arbitrary node N denotes a procedure call invoking a
	123	-- Ghost procedure.
8636f52f	124
dafe11cd HK	125	function Is_Ignored_Ghost_Unit (N : Node_Id) return Boolean;
	126	-- Determine whether compilation unit N is subject to pragma Ghost with
	127	-- policy Ignore.
	128
d65a80fd HK	129	procedure Lock;
	130	-- Lock internal tables before calling backend
	131
f9a8f910	132	procedure Mark_And_Set_Ghost_Assignment (N : Node_Id);
d65a80fd HK	133	-- Mark assignment statement N as Ghost when:
	134	--
	135	-- * The left hand side denotes a Ghost entity
	136	--
f9a8f910	137	-- Install the Ghost mode of the assignment statement. This routine starts
9057bd6a	138	-- a Ghost region and must be used with routine Restore_Ghost_Region.
d65a80fd HK	139
	140	procedure Mark_And_Set_Ghost_Body
	141	(N : Node_Id;
f9a8f910	142	Spec_Id : Entity_Id);
d65a80fd HK	143	-- Mark package or subprogram body N as Ghost when:
	144	--
	145	-- * The body is subject to pragma Ghost
	146	--
	147	-- * The body completes a previous declaration whose spec denoted by
	148	-- Spec_Id is a Ghost entity.
	149	--
	150	-- * The body appears within a Ghost region
8636f52f	151	--
f9a8f910	152	-- Install the Ghost mode of the body. This routine starts a Ghost region
9057bd6a	153	-- and must be used with routine Restore_Ghost_Region.
d65a80fd HK	154
	155	procedure Mark_And_Set_Ghost_Completion
	156	(N : Node_Id;
f9a8f910	157	Prev_Id : Entity_Id);
d65a80fd HK	158	-- Mark completion N of a deferred constant or private type [extension]
d65a80fd HK	159	-- Ghost when:
8636f52f	160	--
d65a80fd	161	-- * The entity of the previous declaration denoted by Prev_Id is Ghost
241ebe89	162	--
d65a80fd	163	-- * The completion appears within a Ghost region
241ebe89	164	--
f9a8f910	165	-- Install the Ghost mode of the completion. This routine starts a Ghost
9057bd6a	166	-- region and must be used with routine Restore_Ghost_Region.
d65a80fd	167
f9a8f910	168	procedure Mark_And_Set_Ghost_Declaration (N : Node_Id);
d65a80fd	169	-- Mark declaration N as Ghost when:
8636f52f	170	--
d65a80fd	171	-- * The declaration is subject to pragma Ghost
8636f52f	172	--
d65a80fd HK	173	-- * The declaration denotes a child package or subprogram and the parent
d65a80fd HK	174	-- is a Ghost unit.
8636f52f	175	--
d65a80fd	176	-- * The declaration appears within a Ghost region
8636f52f	177	--
f9a8f910	178	-- Install the Ghost mode of the declaration. This routine starts a Ghost
9057bd6a	179	-- region and must be used with routine Restore_Ghost_Region.
d65a80fd HK	180
	181	procedure Mark_And_Set_Ghost_Instantiation
	182	(N : Node_Id;
f9a8f910	183	Gen_Id : Entity_Id);
d65a80fd HK	184	-- Mark instantiation N as Ghost when:
	185	--
	186	-- * The instantiation is subject to pragma Ghost
	187	--
	188	-- * The generic template denoted by Gen_Id is Ghost
	189	--
	190	-- * The instantiation appears within a Ghost region
	191	--
f9a8f910	192	-- Install the Ghost mode of the instantiation. This routine starts a Ghost
9057bd6a	193	-- region and must be used with routine Restore_Ghost_Region.
d65a80fd	194
f9a8f910	195	procedure Mark_And_Set_Ghost_Procedure_Call (N : Node_Id);
d65a80fd HK	196	-- Mark procedure call N as Ghost when:
	197	--
	198	-- * The procedure being invoked is a Ghost entity
	199	--
f9a8f910	200	-- Install the Ghost mode of the procedure call. This routine starts a
9057bd6a	201	-- Ghost region and must be used with routine Restore_Ghost_Region.
d65a80fd	202
6e9e35e1 AC	203	procedure Mark_Ghost_Clause (N : Node_Id);
	204	-- Mark use package, use type, or with clause N as Ghost when:
	205	--
	206	-- * The clause mentions a Ghost entity
	207
d65a80fd HK	208	procedure Mark_Ghost_Pragma
	209	(N : Node_Id;
	210	Id : Entity_Id);
	211	-- Mark pragma N as Ghost when:
	212	--
	213	-- * The pragma encloses Ghost entity Id
	214	--
	215	-- * The pragma is associated with Ghost entity Id
8636f52f	216
d65a80fd HK	217	procedure Mark_Ghost_Renaming
	218	(N : Node_Id;
	219	Id : Entity_Id);
	220	-- Mark renaming declaration N as Ghost when:
8636f52f	221	--
d65a80fd HK	222	-- * Renamed entity Id denotes a Ghost entity
	223
	224	procedure Remove_Ignored_Ghost_Code;
	225	-- Remove all code marked as ignored Ghost from the trees of all qualifying
	226	-- units (SPARK RM 6.9(4)).
	227	--
	228	-- WARNING: this is a separate front end pass, care should be taken to keep
	229	-- it optimized.
	230
9057bd6a HK	231	procedure Restore_Ghost_Region (Mode : Ghost_Mode_Type; N : Node_Id);
	232	pragma Inline (Restore_Ghost_Region);
	233	-- Restore a Ghost region to a previous state described by mode Mode and
	234	-- ignored region start node N. This routine must be used in conjunction
	235	-- with the following routines:
	236	--
	237	-- Install_Ghost_Region
	238	-- Mark_And_Set_xxx
	239	-- Set_Ghost_Mode
d65a80fd	240
f9a8f910 HK	241	procedure Set_Ghost_Mode (N : Node_Or_Entity_Id);
f9a8f910 HK	242	-- Install the Ghost mode of arbitrary node N. This routine starts a Ghost
9057bd6a	243	-- region and must be used with routine Restore_Ghost_Region.
8636f52f HK	244
8636f52f HK	245	procedure Set_Is_Ghost_Entity (Id : Entity_Id);
241ebe89	246	-- Set the relevant Ghost attributes of entity Id depending on the current
8636f52f HK	247	-- Ghost assertion policy in effect.
	248
	249	end Ghost;