blob: cb180967d67fe70a74cfecc73b52876560bd536b [file] [log] [blame]
------------------------------------------------------------------------------
-- --
-- GNAT COMPILER COMPONENTS --
-- --
-- E X P _ U T I L --
-- --
-- B o d y --
-- --
-- Copyright (C) 1992-2021, 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. --
-- --
------------------------------------------------------------------------------
with Aspects; use Aspects;
with Atree; use Atree;
with Casing; use Casing;
with Checks; use Checks;
with Debug; use Debug;
with Einfo; use Einfo;
with Einfo.Entities; use Einfo.Entities;
with Einfo.Utils; use Einfo.Utils;
with Elists; use Elists;
with Errout; use Errout;
with Exp_Aggr; use Exp_Aggr;
with Exp_Ch6; use Exp_Ch6;
with Exp_Ch7; use Exp_Ch7;
with Exp_Ch11; use Exp_Ch11;
with Freeze; use Freeze;
with Ghost; use Ghost;
with Inline; use Inline;
with Itypes; use Itypes;
with Lib; use Lib;
with Nlists; use Nlists;
with Nmake; use Nmake;
with Opt; use Opt;
with Restrict; use Restrict;
with Rident; use Rident;
with Sem; use Sem;
with Sem_Aux; use Sem_Aux;
with Sem_Ch3; use Sem_Ch3;
with Sem_Ch6; use Sem_Ch6;
with Sem_Ch8; use Sem_Ch8;
with Sem_Ch12; use Sem_Ch12;
with Sem_Ch13; use Sem_Ch13;
with Sem_Disp; use Sem_Disp;
with Sem_Elab; use Sem_Elab;
with Sem_Eval; use Sem_Eval;
with Sem_Res; use Sem_Res;
with Sem_Type; use Sem_Type;
with Sem_Util; use Sem_Util;
with Sinfo.Utils; use Sinfo.Utils;
with Snames; use Snames;
with Stand; use Stand;
with Stringt; use Stringt;
with Tbuild; use Tbuild;
with Ttypes; use Ttypes;
with Validsw; use Validsw;
with GNAT.HTable;
package body Exp_Util is
---------------------------------------------------------
-- Handling of inherited class-wide pre/postconditions --
---------------------------------------------------------
-- Following AI12-0113, the expression for a class-wide condition is
-- transformed for a subprogram that inherits it, by replacing calls
-- to primitive operations of the original controlling type into the
-- corresponding overriding operations of the derived type. The following
-- hash table manages this mapping, and is expanded on demand whenever
-- such inherited expression needs to be constructed.
-- The mapping is also used to check whether an inherited operation has
-- a condition that depends on overridden operations. For such an
-- operation we must create a wrapper that is then treated as a normal
-- overriding. In SPARK mode such operations are illegal.
-- For a given root type there may be several type extensions with their
-- own overriding operations, so at various times a given operation of
-- the root will be mapped into different overridings. The root type is
-- also mapped into the current type extension to indicate that its
-- operations are mapped into the overriding operations of that current
-- type extension.
-- The contents of the map are as follows:
-- Key Value
-- Discriminant (Entity_Id) Discriminant (Entity_Id)
-- Discriminant (Entity_Id) Non-discriminant name (Entity_Id)
-- Discriminant (Entity_Id) Expression (Node_Id)
-- Primitive subprogram (Entity_Id) Primitive subprogram (Entity_Id)
-- Type (Entity_Id) Type (Entity_Id)
Type_Map_Size : constant := 511;
subtype Type_Map_Header is Integer range 0 .. Type_Map_Size - 1;
function Type_Map_Hash (Id : Entity_Id) return Type_Map_Header;
package Type_Map is new GNAT.HTable.Simple_HTable
(Header_Num => Type_Map_Header,
Key => Entity_Id,
Element => Node_Or_Entity_Id,
No_element => Empty,
Hash => Type_Map_Hash,
Equal => "=");
-----------------------
-- Local Subprograms --
-----------------------
function Build_Task_Array_Image
(Loc : Source_Ptr;
Id_Ref : Node_Id;
A_Type : Entity_Id;
Dyn : Boolean := False) return Node_Id;
-- Build function to generate the image string for a task that is an array
-- component, concatenating the images of each index. To avoid storage
-- leaks, the string is built with successive slice assignments. The flag
-- Dyn indicates whether this is called for the initialization procedure of
-- an array of tasks, or for the name of a dynamically created task that is
-- assigned to an indexed component.
function Build_Task_Image_Function
(Loc : Source_Ptr;
Decls : List_Id;
Stats : List_Id;
Res : Entity_Id) return Node_Id;
-- Common processing for Task_Array_Image and Task_Record_Image. Build
-- function body that computes image.
procedure Build_Task_Image_Prefix
(Loc : Source_Ptr;
Len : out Entity_Id;
Res : out Entity_Id;
Pos : out Entity_Id;
Prefix : Entity_Id;
Sum : Node_Id;
Decls : List_Id;
Stats : List_Id);
-- Common processing for Task_Array_Image and Task_Record_Image. Create
-- local variables and assign prefix of name to result string.
function Build_Task_Record_Image
(Loc : Source_Ptr;
Id_Ref : Node_Id;
Dyn : Boolean := False) return Node_Id;
-- Build function to generate the image string for a task that is a record
-- component. Concatenate name of variable with that of selector. The flag
-- Dyn indicates whether this is called for the initialization procedure of
-- record with task components, or for a dynamically created task that is
-- assigned to a selected component.
procedure Evaluate_Slice_Bounds (Slice : Node_Id);
-- Force evaluation of bounds of a slice, which may be given by a range
-- or by a subtype indication with or without a constraint.
function Is_Verifiable_DIC_Pragma (Prag : Node_Id) return Boolean;
-- Determine whether pragma Default_Initial_Condition denoted by Prag has
-- an assertion expression that should be verified at run time.
function Is_Uninitialized_Aggregate
(Exp : Node_Id;
T : Entity_Id) return Boolean;
-- Determine whether an array aggregate used in an object declaration
-- is uninitialized, when the aggregate is declared with a box and
-- the component type has no default value. Such an aggregate can be
-- optimized away to prevent the copying of uninitialized data, and
-- the bounds of the aggregate can be propagated directly to the
-- object declaration.
function Make_CW_Equivalent_Type
(T : Entity_Id;
E : Node_Id) return Entity_Id;
-- T is a class-wide type entity, E is the initial expression node that
-- constrains T in case such as: " X: T := E" or "new T'(E)". This function
-- returns the entity of the Equivalent type and inserts on the fly the
-- necessary declaration such as:
--
-- type anon is record
-- _parent : Root_Type (T); constrained with E discriminants (if any)
-- Extension : String (1 .. expr to match size of E);
-- end record;
--
-- This record is compatible with any object of the class of T thanks to
-- the first field and has the same size as E thanks to the second.
function Make_Literal_Range
(Loc : Source_Ptr;
Literal_Typ : Entity_Id) return Node_Id;
-- Produce a Range node whose bounds are:
-- Low_Bound (Literal_Type) ..
-- Low_Bound (Literal_Type) + (Length (Literal_Typ) - 1)
-- this is used for expanding declarations like X : String := "sdfgdfg";
--
-- If the index type of the target array is not integer, we generate:
-- Low_Bound (Literal_Type) ..
-- Literal_Type'Val
-- (Literal_Type'Pos (Low_Bound (Literal_Type))
-- + (Length (Literal_Typ) -1))
function Make_Non_Empty_Check
(Loc : Source_Ptr;
N : Node_Id) return Node_Id;
-- Produce a boolean expression checking that the unidimensional array
-- node N is not empty.
function New_Class_Wide_Subtype
(CW_Typ : Entity_Id;
N : Node_Id) return Entity_Id;
-- Create an implicit subtype of CW_Typ attached to node N
function Requires_Cleanup_Actions
(L : List_Id;
Lib_Level : Boolean;
Nested_Constructs : Boolean) return Boolean;
-- Given a list L, determine whether it contains one of the following:
--
-- 1) controlled objects
-- 2) library-level tagged types
--
-- Lib_Level is True when the list comes from a construct at the library
-- level, and False otherwise. Nested_Constructs is True when any nested
-- packages declared in L must be processed, and False otherwise.
function Side_Effect_Free_Attribute (Name : Name_Id) return Boolean;
-- Return True if the evaluation of the given attribute is considered
-- side-effect free, independently of its prefix and expressions.
-------------------------------------
-- Activate_Atomic_Synchronization --
-------------------------------------
procedure Activate_Atomic_Synchronization (N : Node_Id) is
Msg_Node : Node_Id;
begin
case Nkind (Parent (N)) is
-- Check for cases of appearing in the prefix of a construct where we
-- don't need atomic synchronization for this kind of usage.
when
-- Nothing to do if we are the prefix of an attribute, since we
-- do not want an atomic sync operation for things like 'Size.
N_Attribute_Reference
-- The N_Reference node is like an attribute
| N_Reference
-- Nothing to do for a reference to a component (or components)
-- of a composite object. Only reads and updates of the object
-- as a whole require atomic synchronization (RM C.6 (15)).
| N_Indexed_Component
| N_Selected_Component
| N_Slice
=>
-- For all the above cases, nothing to do if we are the prefix
if Prefix (Parent (N)) = N then
return;
end if;
when others =>
null;
end case;
-- Nothing to do for the identifier in an object renaming declaration,
-- the renaming itself does not need atomic synchronization.
if Nkind (Parent (N)) = N_Object_Renaming_Declaration then
return;
end if;
-- Go ahead and set the flag
Set_Atomic_Sync_Required (N);
-- Generate info message if requested
if Warn_On_Atomic_Synchronization then
case Nkind (N) is
when N_Identifier =>
Msg_Node := N;
when N_Expanded_Name
| N_Selected_Component
=>
Msg_Node := Selector_Name (N);
when N_Explicit_Dereference
| N_Indexed_Component
=>
Msg_Node := Empty;
when others =>
pragma Assert (False);
return;
end case;
if Present (Msg_Node) then
Error_Msg_N
("info: atomic synchronization set for &?N?", Msg_Node);
else
Error_Msg_N
("info: atomic synchronization set?N?", N);
end if;
end if;
end Activate_Atomic_Synchronization;
----------------------
-- Adjust_Condition --
----------------------
procedure Adjust_Condition (N : Node_Id) is
begin
if No (N) then
return;
end if;
declare
Loc : constant Source_Ptr := Sloc (N);
T : constant Entity_Id := Etype (N);
begin
-- Defend against a call where the argument has no type, or has a
-- type that is not Boolean. This can occur because of prior errors.
if No (T) or else not Is_Boolean_Type (T) then
return;
end if;
-- Apply validity checking if needed
if Validity_Checks_On and Validity_Check_Tests then
Ensure_Valid (N);
end if;
-- Immediate return if standard boolean, the most common case,
-- where nothing needs to be done.
if Base_Type (T) = Standard_Boolean then
return;
end if;
-- Case of zero/nonzero semantics or nonstandard enumeration
-- representation. In each case, we rewrite the node as:
-- ityp!(N) /= False'Enum_Rep
-- where ityp is an integer type with large enough size to hold any
-- value of type T.
if Nonzero_Is_True (T) or else Has_Non_Standard_Rep (T) then
Rewrite (N,
Make_Op_Ne (Loc,
Left_Opnd =>
Unchecked_Convert_To
(Integer_Type_For (Esize (T), Uns => False), N),
Right_Opnd =>
Make_Attribute_Reference (Loc,
Attribute_Name => Name_Enum_Rep,
Prefix =>
New_Occurrence_Of (First_Literal (T), Loc))));
Analyze_And_Resolve (N, Standard_Boolean);
else
Rewrite (N, Convert_To (Standard_Boolean, N));
Analyze_And_Resolve (N, Standard_Boolean);
end if;
end;
end Adjust_Condition;
------------------------
-- Adjust_Result_Type --
------------------------
procedure Adjust_Result_Type (N : Node_Id; T : Entity_Id) is
begin
-- Ignore call if current type is not Standard.Boolean
if Etype (N) /= Standard_Boolean then
return;
end if;
-- If result is already of correct type, nothing to do. Note that
-- this will get the most common case where everything has a type
-- of Standard.Boolean.
if Base_Type (T) = Standard_Boolean then
return;
else
declare
KP : constant Node_Kind := Nkind (Parent (N));
begin
-- If result is to be used as a Condition in the syntax, no need
-- to convert it back, since if it was changed to Standard.Boolean
-- using Adjust_Condition, that is just fine for this usage.
if KP in N_Raise_xxx_Error or else KP in N_Has_Condition then
return;
-- If result is an operand of another logical operation, no need
-- to reset its type, since Standard.Boolean is just fine, and
-- such operations always do Adjust_Condition on their operands.
elsif KP in N_Op_Boolean
or else KP in N_Short_Circuit
or else KP = N_Op_Not
then
return;
-- Otherwise we perform a conversion from the current type, which
-- must be Standard.Boolean, to the desired type. Use the base
-- type to prevent spurious constraint checks that are extraneous
-- to the transformation. The type and its base have the same
-- representation, standard or otherwise.
else
Set_Analyzed (N);
Rewrite (N, Convert_To (Base_Type (T), N));
Analyze_And_Resolve (N, Base_Type (T));
end if;
end;
end if;
end Adjust_Result_Type;
--------------------------
-- Append_Freeze_Action --
--------------------------
procedure Append_Freeze_Action (T : Entity_Id; N : Node_Id) is
Fnode : Node_Id;
begin
Ensure_Freeze_Node (T);
Fnode := Freeze_Node (T);
if No (Actions (Fnode)) then
Set_Actions (Fnode, New_List (N));
else
Append (N, Actions (Fnode));
end if;
end Append_Freeze_Action;
---------------------------
-- Append_Freeze_Actions --
---------------------------
procedure Append_Freeze_Actions (T : Entity_Id; L : List_Id) is
Fnode : Node_Id;
begin
if No (L) then
return;
end if;
Ensure_Freeze_Node (T);
Fnode := Freeze_Node (T);
if No (Actions (Fnode)) then
Set_Actions (Fnode, L);
else
Append_List (L, Actions (Fnode));
end if;
end Append_Freeze_Actions;
----------------------------------------
-- Attribute_Constrained_Static_Value --
----------------------------------------
function Attribute_Constrained_Static_Value (Pref : Node_Id) return Boolean
is
Ptyp : constant Entity_Id := Etype (Pref);
Formal_Ent : constant Entity_Id := Param_Entity (Pref);
function Is_Constrained_Aliased_View (Obj : Node_Id) return Boolean;
-- Ada 2005 (AI-363): Returns True if the object name Obj denotes a
-- view of an aliased object whose subtype is constrained.
---------------------------------
-- Is_Constrained_Aliased_View --
---------------------------------
function Is_Constrained_Aliased_View (Obj : Node_Id) return Boolean is
E : Entity_Id;
begin
if Is_Entity_Name (Obj) then
E := Entity (Obj);
if Present (Renamed_Object (E)) then
return Is_Constrained_Aliased_View (Renamed_Object (E));
else
return Is_Aliased (E) and then Is_Constrained (Etype (E));
end if;
else
return Is_Aliased_View (Obj)
and then
(Is_Constrained (Etype (Obj))
or else
(Nkind (Obj) = N_Explicit_Dereference
and then
not Object_Type_Has_Constrained_Partial_View
(Typ => Base_Type (Etype (Obj)),
Scop => Current_Scope)));
end if;
end Is_Constrained_Aliased_View;
-- Start of processing for Attribute_Constrained_Static_Value
begin
-- We are in a case where the attribute is known statically, and
-- implicit dereferences have been rewritten.
pragma Assert
(not (Present (Formal_Ent)
and then Ekind (Formal_Ent) /= E_Constant
and then Present (Extra_Constrained (Formal_Ent)))
and then
not (Is_Access_Type (Etype (Pref))
and then (not Is_Entity_Name (Pref)
or else Is_Object (Entity (Pref))))
and then
not (Nkind (Pref) = N_Identifier
and then Ekind (Entity (Pref)) = E_Variable
and then Present (Extra_Constrained (Entity (Pref)))));
if Is_Entity_Name (Pref) then
declare
Ent : constant Entity_Id := Entity (Pref);
Res : Boolean;
begin
-- (RM J.4) obsolescent cases
if Is_Type (Ent) then
-- Private type
if Is_Private_Type (Ent) then
Res := not Has_Discriminants (Ent)
or else Is_Constrained (Ent);
-- It not a private type, must be a generic actual type
-- that corresponded to a private type. We know that this
-- correspondence holds, since otherwise the reference
-- within the generic template would have been illegal.
else
if Is_Composite_Type (Underlying_Type (Ent)) then
Res := Is_Constrained (Ent);
else
Res := True;
end if;
end if;
else
-- If the prefix is not a variable or is aliased, then
-- definitely true; if it's a formal parameter without an
-- associated extra formal, then treat it as constrained.
-- Ada 2005 (AI-363): An aliased prefix must be known to be
-- constrained in order to set the attribute to True.
if not Is_Variable (Pref)
or else Present (Formal_Ent)
or else (Ada_Version < Ada_2005
and then Is_Aliased_View (Pref))
or else (Ada_Version >= Ada_2005
and then Is_Constrained_Aliased_View (Pref))
then
Res := True;
-- Variable case, look at type to see if it is constrained.
-- Note that the one case where this is not accurate (the
-- procedure formal case), has been handled above.
-- We use the Underlying_Type here (and below) in case the
-- type is private without discriminants, but the full type
-- has discriminants. This case is illegal, but we generate
-- it internally for passing to the Extra_Constrained
-- parameter.
else
-- In Ada 2012, test for case of a limited tagged type,
-- in which case the attribute is always required to
-- return True. The underlying type is tested, to make
-- sure we also return True for cases where there is an
-- unconstrained object with an untagged limited partial
-- view which has defaulted discriminants (such objects
-- always produce a False in earlier versions of
-- Ada). (Ada 2012: AI05-0214)
Res :=
Is_Constrained (Underlying_Type (Etype (Ent)))
or else
(Ada_Version >= Ada_2012
and then Is_Tagged_Type (Underlying_Type (Ptyp))
and then Is_Limited_Type (Ptyp));
end if;
end if;
return Res;
end;
-- Prefix is not an entity name. These are also cases where we can
-- always tell at compile time by looking at the form and type of the
-- prefix. If an explicit dereference of an object with constrained
-- partial view, this is unconstrained (Ada 2005: AI95-0363). If the
-- underlying type is a limited tagged type, then Constrained is
-- required to always return True (Ada 2012: AI05-0214).
else
return not Is_Variable (Pref)
or else
(Nkind (Pref) = N_Explicit_Dereference
and then
not Object_Type_Has_Constrained_Partial_View
(Typ => Base_Type (Ptyp),
Scop => Current_Scope))
or else Is_Constrained (Underlying_Type (Ptyp))
or else (Ada_Version >= Ada_2012
and then Is_Tagged_Type (Underlying_Type (Ptyp))
and then Is_Limited_Type (Ptyp));
end if;
end Attribute_Constrained_Static_Value;
------------------------------------
-- Build_Allocate_Deallocate_Proc --
------------------------------------
procedure Build_Allocate_Deallocate_Proc
(N : Node_Id;
Is_Allocate : Boolean)
is
function Find_Object (E : Node_Id) return Node_Id;
-- Given an arbitrary expression of an allocator, try to find an object
-- reference in it, otherwise return the original expression.
function Is_Allocate_Deallocate_Proc (Subp : Entity_Id) return Boolean;
-- Determine whether subprogram Subp denotes a custom allocate or
-- deallocate.
-----------------
-- Find_Object --
-----------------
function Find_Object (E : Node_Id) return Node_Id is
Expr : Node_Id;
begin
pragma Assert (Is_Allocate);
Expr := E;
loop
if Nkind (Expr) = N_Explicit_Dereference then
Expr := Prefix (Expr);
elsif Nkind (Expr) = N_Qualified_Expression then
Expr := Expression (Expr);
elsif Nkind (Expr) = N_Unchecked_Type_Conversion then
-- When interface class-wide types are involved in allocation,
-- the expander introduces several levels of address arithmetic
-- to perform dispatch table displacement. In this scenario the
-- object appears as:
-- Tag_Ptr (Base_Address (<object>'Address))
-- Detect this case and utilize the whole expression as the
-- "object" since it now points to the proper dispatch table.
if Is_RTE (Etype (Expr), RE_Tag_Ptr) then
exit;
-- Continue to strip the object
else
Expr := Expression (Expr);
end if;
else
exit;
end if;
end loop;
return Expr;
end Find_Object;
---------------------------------
-- Is_Allocate_Deallocate_Proc --
---------------------------------
function Is_Allocate_Deallocate_Proc (Subp : Entity_Id) return Boolean is
begin
-- Look for a subprogram body with only one statement which is a
-- call to Allocate_Any_Controlled / Deallocate_Any_Controlled.
if Ekind (Subp) = E_Procedure
and then Nkind (Parent (Parent (Subp))) = N_Subprogram_Body
then
declare
HSS : constant Node_Id :=
Handled_Statement_Sequence (Parent (Parent (Subp)));
Proc : Entity_Id;
begin
if Present (Statements (HSS))
and then Nkind (First (Statements (HSS))) =
N_Procedure_Call_Statement
then
Proc := Entity (Name (First (Statements (HSS))));
return
Is_RTE (Proc, RE_Allocate_Any_Controlled)
or else Is_RTE (Proc, RE_Deallocate_Any_Controlled);
end if;
end;
end if;
return False;
end Is_Allocate_Deallocate_Proc;
-- Local variables
Desig_Typ : Entity_Id;
Expr : Node_Id;
Needs_Fin : Boolean;
Pool_Id : Entity_Id;
Proc_To_Call : Node_Id := Empty;
Ptr_Typ : Entity_Id;
Use_Secondary_Stack_Pool : Boolean;
-- Start of processing for Build_Allocate_Deallocate_Proc
begin
-- Obtain the attributes of the allocation / deallocation
if Nkind (N) = N_Free_Statement then
Expr := Expression (N);
Ptr_Typ := Base_Type (Etype (Expr));
Proc_To_Call := Procedure_To_Call (N);
else
if Nkind (N) = N_Object_Declaration then
Expr := Expression (N);
else
Expr := N;
end if;
-- In certain cases an allocator with a qualified expression may
-- be relocated and used as the initialization expression of a
-- temporary:
-- before:
-- Obj : Ptr_Typ := new Desig_Typ'(...);
-- after:
-- Tmp : Ptr_Typ := new Desig_Typ'(...);
-- Obj : Ptr_Typ := Tmp;
-- Since the allocator is always marked as analyzed to avoid infinite
-- expansion, it will never be processed by this routine given that
-- the designated type needs finalization actions. Detect this case
-- and complete the expansion of the allocator.
if Nkind (Expr) = N_Identifier
and then Nkind (Parent (Entity (Expr))) = N_Object_Declaration
and then Nkind (Expression (Parent (Entity (Expr)))) = N_Allocator
then
Build_Allocate_Deallocate_Proc (Parent (Entity (Expr)), True);
return;
end if;
-- The allocator may have been rewritten into something else in which
-- case the expansion performed by this routine does not apply.
if Nkind (Expr) /= N_Allocator then
return;
end if;
Ptr_Typ := Base_Type (Etype (Expr));
Proc_To_Call := Procedure_To_Call (Expr);
end if;
Pool_Id := Associated_Storage_Pool (Ptr_Typ);
Desig_Typ := Available_View (Designated_Type (Ptr_Typ));
-- Handle concurrent types
if Is_Concurrent_Type (Desig_Typ)
and then Present (Corresponding_Record_Type (Desig_Typ))
then
Desig_Typ := Corresponding_Record_Type (Desig_Typ);
end if;
Use_Secondary_Stack_Pool :=
Is_RTE (Pool_Id, RE_SS_Pool)
or else (Nkind (Expr) = N_Allocator
and then Is_RTE (Storage_Pool (Expr), RE_SS_Pool));
-- Do not process allocations / deallocations without a pool
if No (Pool_Id) then
return;
-- Do not process allocations on / deallocations from the secondary
-- stack, except for access types used to implement indirect temps.
elsif Use_Secondary_Stack_Pool
and then not Old_Attr_Util.Indirect_Temps
.Is_Access_Type_For_Indirect_Temp (Ptr_Typ)
then
return;
-- Optimize the case where we are using the default Global_Pool_Object,
-- and we don't need the heavy finalization machinery.
elsif Is_RTE (Pool_Id, RE_Global_Pool_Object)
and then not Needs_Finalization (Desig_Typ)
then
return;
-- Do not replicate the machinery if the allocator / free has already
-- been expanded and has a custom Allocate / Deallocate.
elsif Present (Proc_To_Call)
and then Is_Allocate_Deallocate_Proc (Proc_To_Call)
then
return;
end if;
-- Finalization actions are required when the object to be allocated or
-- deallocated needs these actions and the associated access type is not
-- subject to pragma No_Heap_Finalization.
Needs_Fin :=
Needs_Finalization (Desig_Typ)
and then not No_Heap_Finalization (Ptr_Typ);
if Needs_Fin then
-- Do nothing if the access type may never allocate / deallocate
-- objects.
if No_Pool_Assigned (Ptr_Typ) then
return;
end if;
-- The allocation / deallocation of a controlled object must be
-- chained on / detached from a finalization master.
pragma Assert (Present (Finalization_Master (Ptr_Typ)));
-- The only other kind of allocation / deallocation supported by this
-- routine is on / from a subpool.
elsif Nkind (Expr) = N_Allocator
and then No (Subpool_Handle_Name (Expr))
then
return;
end if;
declare
Loc : constant Source_Ptr := Sloc (N);
Addr_Id : constant Entity_Id := Make_Temporary (Loc, 'A');
Alig_Id : constant Entity_Id := Make_Temporary (Loc, 'L');
Proc_Id : constant Entity_Id := Make_Temporary (Loc, 'P');
Size_Id : constant Entity_Id := Make_Temporary (Loc, 'S');
Actuals : List_Id;
Fin_Addr_Id : Entity_Id;
Fin_Mas_Act : Node_Id;
Fin_Mas_Id : Entity_Id;
Proc_To_Call : Entity_Id;
Subpool : Node_Id := Empty;
begin
-- Step 1: Construct all the actuals for the call to library routine
-- Allocate_Any_Controlled / Deallocate_Any_Controlled.
-- a) Storage pool
Actuals := New_List (New_Occurrence_Of (Pool_Id, Loc));
if Is_Allocate then
-- b) Subpool
if Nkind (Expr) = N_Allocator then
Subpool := Subpool_Handle_Name (Expr);
end if;
-- If a subpool is present it can be an arbitrary name, so make
-- the actual by copying the tree.
if Present (Subpool) then
Append_To (Actuals, New_Copy_Tree (Subpool, New_Sloc => Loc));
else
Append_To (Actuals, Make_Null (Loc));
end if;
-- c) Finalization master
if Needs_Fin then
Fin_Mas_Id := Finalization_Master (Ptr_Typ);
Fin_Mas_Act := New_Occurrence_Of (Fin_Mas_Id, Loc);
-- Handle the case where the master is actually a pointer to a
-- master. This case arises in build-in-place functions.
if Is_Access_Type (Etype (Fin_Mas_Id)) then
Append_To (Actuals, Fin_Mas_Act);
else
Append_To (Actuals,
Make_Attribute_Reference (Loc,
Prefix => Fin_Mas_Act,
Attribute_Name => Name_Unrestricted_Access));
end if;
else
Append_To (Actuals, Make_Null (Loc));
end if;
-- d) Finalize_Address
-- Primitive Finalize_Address is never generated in CodePeer mode
-- since it contains an Unchecked_Conversion.
if Needs_Fin and then not CodePeer_Mode then
Fin_Addr_Id := Finalize_Address (Desig_Typ);
pragma Assert (Present (Fin_Addr_Id));
Append_To (Actuals,
Make_Attribute_Reference (Loc,
Prefix => New_Occurrence_Of (Fin_Addr_Id, Loc),
Attribute_Name => Name_Unrestricted_Access));
else
Append_To (Actuals, Make_Null (Loc));
end if;
end if;
-- e) Address
-- f) Storage_Size
-- g) Alignment
Append_To (Actuals, New_Occurrence_Of (Addr_Id, Loc));
Append_To (Actuals, New_Occurrence_Of (Size_Id, Loc));
if (Is_Allocate or else not Is_Class_Wide_Type (Desig_Typ))
and then not Use_Secondary_Stack_Pool
then
Append_To (Actuals, New_Occurrence_Of (Alig_Id, Loc));
-- For deallocation of class-wide types we obtain the value of
-- alignment from the Type Specific Record of the deallocated object.
-- This is needed because the frontend expansion of class-wide types
-- into equivalent types confuses the back end.
else
-- Generate:
-- Obj.all'Alignment
-- ... because 'Alignment applied to class-wide types is expanded
-- into the code that reads the value of alignment from the TSD
-- (see Expand_N_Attribute_Reference)
-- In the Use_Secondary_Stack_Pool case, Alig_Id is not
-- passed in and therefore must not be referenced.
Append_To (Actuals,
Unchecked_Convert_To (RTE (RE_Storage_Offset),
Make_Attribute_Reference (Loc,
Prefix =>
Make_Explicit_Dereference (Loc, Relocate_Node (Expr)),
Attribute_Name => Name_Alignment)));
end if;
-- h) Is_Controlled
if Needs_Fin then
Is_Controlled : declare
Flag_Id : constant Entity_Id := Make_Temporary (Loc, 'F');
Flag_Expr : Node_Id;
Param : Node_Id;
Pref : Node_Id;
Temp : Node_Id;
begin
if Is_Allocate then
Temp := Find_Object (Expression (Expr));
else
Temp := Expr;
end if;
-- Processing for allocations where the expression is a subtype
-- indication.
if Is_Allocate
and then Is_Entity_Name (Temp)
and then Is_Type (Entity (Temp))
then
Flag_Expr :=
New_Occurrence_Of
(Boolean_Literals
(Needs_Finalization (Entity (Temp))), Loc);
-- The allocation / deallocation of a class-wide object relies
-- on a runtime check to determine whether the object is truly
-- controlled or not. Depending on this check, the finalization
-- machinery will request or reclaim extra storage reserved for
-- a list header.
elsif Is_Class_Wide_Type (Desig_Typ) then
-- Detect a special case where interface class-wide types
-- are involved as the object appears as:
-- Tag_Ptr (Base_Address (<object>'Address))
-- The expression already yields the proper tag, generate:
-- Temp.all
if Is_RTE (Etype (Temp), RE_Tag_Ptr) then
Param :=
Make_Explicit_Dereference (Loc,
Prefix => Relocate_Node (Temp));
-- In the default case, obtain the tag of the object about
-- to be allocated / deallocated. Generate:
-- Temp'Tag
-- If the object is an unchecked conversion (typically to
-- an access to class-wide type), we must preserve the
-- conversion to ensure that the object is seen as tagged
-- in the code that follows.
else
Pref := Temp;
if Nkind (Parent (Pref)) = N_Unchecked_Type_Conversion
then
Pref := Parent (Pref);
end if;
Param :=
Make_Attribute_Reference (Loc,
Prefix => Relocate_Node (Pref),
Attribute_Name => Name_Tag);
end if;
-- Generate:
-- Needs_Finalization (<Param>)
Flag_Expr :=
Make_Function_Call (Loc,
Name =>
New_Occurrence_Of (RTE (RE_Needs_Finalization), Loc),
Parameter_Associations => New_List (Param));
-- Processing for generic actuals
elsif Is_Generic_Actual_Type (Desig_Typ) then
Flag_Expr :=
New_Occurrence_Of (Boolean_Literals
(Needs_Finalization (Base_Type (Desig_Typ))), Loc);
-- The object does not require any specialized checks, it is
-- known to be controlled.
else
Flag_Expr := New_Occurrence_Of (Standard_True, Loc);
end if;
-- Create the temporary which represents the finalization state
-- of the expression. Generate:
--
-- F : constant Boolean := <Flag_Expr>;
Insert_Action (N,
Make_Object_Declaration (Loc,
Defining_Identifier => Flag_Id,
Constant_Present => True,
Object_Definition =>
New_Occurrence_Of (Standard_Boolean, Loc),
Expression => Flag_Expr));
Append_To (Actuals, New_Occurrence_Of (Flag_Id, Loc));
end Is_Controlled;
-- The object is not controlled
else
Append_To (Actuals, New_Occurrence_Of (Standard_False, Loc));
end if;
-- i) On_Subpool
if Is_Allocate then
Append_To (Actuals,
New_Occurrence_Of (Boolean_Literals (Present (Subpool)), Loc));
end if;
-- Step 2: Build a wrapper Allocate / Deallocate which internally
-- calls Allocate_Any_Controlled / Deallocate_Any_Controlled.
-- Select the proper routine to call
if Is_Allocate then
Proc_To_Call := RTE (RE_Allocate_Any_Controlled);
else
Proc_To_Call := RTE (RE_Deallocate_Any_Controlled);
end if;
-- Create a custom Allocate / Deallocate routine which has identical
-- profile to that of System.Storage_Pools.
declare
-- P : Root_Storage_Pool
function Pool_Param return Node_Id is (
Make_Parameter_Specification (Loc,
Defining_Identifier => Make_Temporary (Loc, 'P'),
Parameter_Type =>
New_Occurrence_Of (RTE (RE_Root_Storage_Pool), Loc)));
-- A : [out] Address
function Address_Param return Node_Id is (
Make_Parameter_Specification (Loc,
Defining_Identifier => Addr_Id,
Out_Present => Is_Allocate,
Parameter_Type =>
New_Occurrence_Of (RTE (RE_Address), Loc)));
-- S : Storage_Count
function Size_Param return Node_Id is (
Make_Parameter_Specification (Loc,
Defining_Identifier => Size_Id,
Parameter_Type =>
New_Occurrence_Of (RTE (RE_Storage_Count), Loc)));
-- L : Storage_Count
function Alignment_Param return Node_Id is (
Make_Parameter_Specification (Loc,
Defining_Identifier => Alig_Id,
Parameter_Type =>
New_Occurrence_Of (RTE (RE_Storage_Count), Loc)));
Formal_Params : List_Id;
begin
if Use_Secondary_Stack_Pool then
-- Gigi expects a different profile in the Secondary_Stack_Pool
-- case. There must be no uses of the two missing formals
-- (i.e., Pool_Param and Alignment_Param) in this case.
Formal_Params := New_List (Address_Param, Size_Param);
else
Formal_Params := New_List (
Pool_Param, Address_Param, Size_Param, Alignment_Param);
end if;
Insert_Action (N,
Make_Subprogram_Body (Loc,
Specification =>
-- procedure Pnn
Make_Procedure_Specification (Loc,
Defining_Unit_Name => Proc_Id,
Parameter_Specifications => Formal_Params),
Declarations => No_List,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
Statements => New_List (
Make_Procedure_Call_Statement (Loc,
Name =>
New_Occurrence_Of (Proc_To_Call, Loc),
Parameter_Associations => Actuals)))),
Suppress => All_Checks);
end;
-- The newly generated Allocate / Deallocate becomes the default
-- procedure to call when the back end processes the allocation /
-- deallocation.
if Is_Allocate then
Set_Procedure_To_Call (Expr, Proc_Id);
else
Set_Procedure_To_Call (N, Proc_Id);
end if;
end;
end Build_Allocate_Deallocate_Proc;
-------------------------------
-- Build_Abort_Undefer_Block --
-------------------------------
function Build_Abort_Undefer_Block
(Loc : Source_Ptr;
Stmts : List_Id;
Context : Node_Id) return Node_Id
is
Exceptions_OK : constant Boolean :=
not Restriction_Active (No_Exception_Propagation);
AUD : Entity_Id;
Blk : Node_Id;
Blk_Id : Entity_Id;
HSS : Node_Id;
begin
-- The block should be generated only when undeferring abort in the
-- context of a potential exception.
pragma Assert (Abort_Allowed and Exceptions_OK);
-- Generate:
-- begin
-- <Stmts>
-- at end
-- Abort_Undefer_Direct;
-- end;
AUD := RTE (RE_Abort_Undefer_Direct);
HSS :=
Make_Handled_Sequence_Of_Statements (Loc,
Statements => Stmts,
At_End_Proc => New_Occurrence_Of (AUD, Loc));
Blk :=
Make_Block_Statement (Loc,
Handled_Statement_Sequence => HSS);
Set_Is_Abort_Block (Blk);
Add_Block_Identifier (Blk, Blk_Id);
Expand_At_End_Handler (HSS, Blk_Id);
-- Present the Abort_Undefer_Direct function to the back end to inline
-- the call to the routine.
Add_Inlined_Body (AUD, Context);
return Blk;
end Build_Abort_Undefer_Block;
---------------------------------
-- Build_Class_Wide_Expression --
---------------------------------
procedure Build_Class_Wide_Expression
(Pragma_Or_Expr : Node_Id;
Subp : Entity_Id;
Par_Subp : Entity_Id;
Adjust_Sloc : Boolean)
is
function Replace_Entity (N : Node_Id) return Traverse_Result;
-- Replace reference to formal of inherited operation or to primitive
-- operation of root type, with corresponding entity for derived type,
-- when constructing the class-wide condition of an overriding
-- subprogram.
--------------------
-- Replace_Entity --
--------------------
function Replace_Entity (N : Node_Id) return Traverse_Result is
New_E : Entity_Id;
begin
if Adjust_Sloc then
Adjust_Inherited_Pragma_Sloc (N);
end if;
if Nkind (N) in N_Identifier | N_Operator_Symbol
and then Present (Entity (N))
and then
(Is_Formal (Entity (N)) or else Is_Subprogram (Entity (N)))
and then
(Nkind (Parent (N)) /= N_Attribute_Reference
or else Attribute_Name (Parent (N)) /= Name_Class)
then
-- The replacement does not apply to dispatching calls within the
-- condition, but only to calls whose static tag is that of the
-- parent type.
if Is_Subprogram (Entity (N))
and then Nkind (Parent (N)) = N_Function_Call
and then Present (Controlling_Argument (Parent (N)))
then
return OK;
end if;
-- Determine whether entity has a renaming
New_E := Type_Map.Get (Entity (N));
if Present (New_E) then
Rewrite (N, New_Occurrence_Of (New_E, Sloc (N)));
end if;
-- Update type of function call node, which should be the same as
-- the function's return type.
if Is_Subprogram (Entity (N))
and then Nkind (Parent (N)) = N_Function_Call
then
Set_Etype (Parent (N), Etype (Entity (N)));
end if;
-- The whole expression will be reanalyzed
elsif Nkind (N) in N_Has_Etype then
Set_Analyzed (N, False);
end if;
return OK;
end Replace_Entity;
procedure Replace_Condition_Entities is
new Traverse_Proc (Replace_Entity);
-- Local variables
Par_Typ : constant Entity_Id := Find_Dispatching_Type (Par_Subp);
Subp_Typ : constant Entity_Id := Find_Dispatching_Type (Subp);
-- Start of processing for Build_Class_Wide_Expression
begin
pragma Assert (Par_Typ /= Subp_Typ);
Update_Primitives_Mapping (Par_Subp, Subp);
Map_Formals (Par_Subp, Subp);
Replace_Condition_Entities (Pragma_Or_Expr);
end Build_Class_Wide_Expression;
--------------------
-- Build_DIC_Call --
--------------------
function Build_DIC_Call
(Loc : Source_Ptr;
Obj_Name : Node_Id;
Typ : Entity_Id) return Node_Id
is
Proc_Id : constant Entity_Id := DIC_Procedure (Typ);
Formal_Typ : constant Entity_Id := Etype (First_Formal (Proc_Id));
begin
-- The DIC procedure has a null body if assertions are disabled or
-- Assertion_Policy Ignore is in effect. In that case, it would be
-- nice to generate a null statement instead of a call to the DIC
-- procedure, but doing that seems to interfere with the determination
-- of ECRs (early call regions) in SPARK. ???
return
Make_Procedure_Call_Statement (Loc,
Name => New_Occurrence_Of (Proc_Id, Loc),
Parameter_Associations => New_List (
Unchecked_Convert_To (Formal_Typ, Obj_Name)));
end Build_DIC_Call;
------------------------------
-- Build_DIC_Procedure_Body --
------------------------------
-- WARNING: This routine manages Ghost regions. Return statements must be
-- replaced by gotos which jump to the end of the routine and restore the
-- Ghost mode.
procedure Build_DIC_Procedure_Body
(Typ : Entity_Id;
Partial_DIC : Boolean := False)
is
Pragmas_Seen : Elist_Id := No_Elist;
-- This list contains all DIC pragmas processed so far. The list is used
-- to avoid redundant Default_Initial_Condition checks.
procedure Add_DIC_Check
(DIC_Prag : Node_Id;
DIC_Expr : Node_Id;
Stmts : in out List_Id);
-- Subsidiary to all Add_xxx_DIC routines. Add a runtime check to verify
-- assertion expression DIC_Expr of pragma DIC_Prag. All generated code
-- is added to list Stmts.
procedure Add_Inherited_DIC
(DIC_Prag : Node_Id;
Par_Typ : Entity_Id;
Deriv_Typ : Entity_Id;
Stmts : in out List_Id);
-- Add a runtime check to verify the assertion expression of inherited
-- pragma DIC_Prag. Par_Typ is parent type, which is also the owner of
-- the DIC pragma. Deriv_Typ is the derived type inheriting the DIC
-- pragma. All generated code is added to list Stmts.
procedure Add_Inherited_Tagged_DIC
(DIC_Prag : Node_Id;
Expr : Node_Id;
Stmts : in out List_Id);
-- Add a runtime check to verify assertion expression DIC_Expr of
-- inherited pragma DIC_Prag. This routine applies class-wide pre-
-- and postcondition-like runtime semantics to the check. Expr is
-- the assertion expression after substitition has been performed
-- (via Replace_References). All generated code is added to list Stmts.
procedure Add_Inherited_DICs
(T : Entity_Id;
Priv_Typ : Entity_Id;
Full_Typ : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id);
-- Generate a DIC check for each inherited Default_Initial_Condition
-- coming from all parent types of type T. Priv_Typ and Full_Typ denote
-- the partial and full view of the parent type. Obj_Id denotes the
-- entity of the _object formal parameter of the DIC procedure. All
-- created checks are added to list Checks.
procedure Add_Own_DIC
(DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
Obj_Id : Entity_Id;
Stmts : in out List_Id);
-- Add a runtime check to verify the assertion expression of pragma
-- DIC_Prag. DIC_Typ is the owner of the DIC pragma. Obj_Id is the
-- object to substitute in the assertion expression for any references
-- to the current instance of the type All generated code is added to
-- list Stmts.
procedure Add_Parent_DICs
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id);
-- Generate a Default_Initial_Condition check for each inherited DIC
-- aspect coming from all parent types of type T. Obj_Id denotes the
-- entity of the _object formal parameter of the DIC procedure. All
-- created checks are added to list Checks.
-------------------
-- Add_DIC_Check --
-------------------
procedure Add_DIC_Check
(DIC_Prag : Node_Id;
DIC_Expr : Node_Id;
Stmts : in out List_Id)
is
Loc : constant Source_Ptr := Sloc (DIC_Prag);
Nam : constant Name_Id := Original_Aspect_Pragma_Name (DIC_Prag);
begin
-- The DIC pragma is ignored, nothing left to do
if Is_Ignored (DIC_Prag) then
null;
-- Otherwise the DIC expression must be checked at run time.
-- Generate:
-- pragma Check (<Nam>, <DIC_Expr>);
else
Append_New_To (Stmts,
Make_Pragma (Loc,
Pragma_Identifier =>
Make_Identifier (Loc, Name_Check),
Pragma_Argument_Associations => New_List (
Make_Pragma_Argument_Association (Loc,
Expression => Make_Identifier (Loc, Nam)),
Make_Pragma_Argument_Association (Loc,
Expression => DIC_Expr))));
end if;
-- Add the pragma to the list of processed pragmas
Append_New_Elmt (DIC_Prag, Pragmas_Seen);
end Add_DIC_Check;
-----------------------
-- Add_Inherited_DIC --
-----------------------
procedure Add_Inherited_DIC
(DIC_Prag : Node_Id;
Par_Typ : Entity_Id;
Deriv_Typ : Entity_Id;
Stmts : in out List_Id)
is
Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ);
Deriv_Obj : constant Entity_Id := First_Entity (Deriv_Proc);
Par_Proc : constant Entity_Id := DIC_Procedure (Par_Typ);
Par_Obj : constant Entity_Id := First_Entity (Par_Proc);
Loc : constant Source_Ptr := Sloc (DIC_Prag);
begin
pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc));
-- Verify the inherited DIC assertion expression by calling the DIC
-- procedure of the parent type.
-- Generate:
-- <Par_Typ>DIC (Par_Typ (_object));
Append_New_To (Stmts,
Make_Procedure_Call_Statement (Loc,
Name => New_Occurrence_Of (Par_Proc, Loc),
Parameter_Associations => New_List (
Convert_To
(Typ => Etype (Par_Obj),
Expr => New_Occurrence_Of (Deriv_Obj, Loc)))));
end Add_Inherited_DIC;
------------------------------
-- Add_Inherited_Tagged_DIC --
------------------------------
procedure Add_Inherited_Tagged_DIC
(DIC_Prag : Node_Id;
Expr : Node_Id;
Stmts : in out List_Id)
is
begin
-- Once the DIC assertion expression is fully processed, add a check
-- to the statements of the DIC procedure.
Add_DIC_Check
(DIC_Prag => DIC_Prag,
DIC_Expr => Expr,
Stmts => Stmts);
end Add_Inherited_Tagged_DIC;
------------------------
-- Add_Inherited_DICs --
------------------------
procedure Add_Inherited_DICs
(T : Entity_Id;
Priv_Typ : Entity_Id;
Full_Typ : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id)
is
Deriv_Typ : Entity_Id;
Expr : Node_Id;
Prag : Node_Id;
Prag_Expr : Node_Id;
Prag_Expr_Arg : Node_Id;
Prag_Typ : Node_Id;
Prag_Typ_Arg : Node_Id;
Par_Proc : Entity_Id;
-- The "partial" invariant procedure of Par_Typ
Par_Typ : Entity_Id;
-- The suitable view of the parent type used in the substitution of
-- type attributes.
begin
if not Present (Priv_Typ) and then not Present (Full_Typ) then
return;
end if;
-- When the type inheriting the class-wide invariant is a concurrent
-- type, use the corresponding record type because it contains all
-- primitive operations of the concurrent type and allows for proper
-- substitution.
if Is_Concurrent_Type (T) then
Deriv_Typ := Corresponding_Record_Type (T);
else
Deriv_Typ := T;
end if;
pragma Assert (Present (Deriv_Typ));
-- Determine which rep item chain to use. Precedence is given to that
-- of the parent type's partial view since it usually carries all the
-- class-wide invariants.
if Present (Priv_Typ) then
Prag := First_Rep_Item (Priv_Typ);
else
Prag := First_Rep_Item (Full_Typ);
end if;
while Present (Prag) loop
if Nkind (Prag) = N_Pragma
and then Pragma_Name (Prag) = Name_Default_Initial_Condition
then
-- Nothing to do if the pragma was already processed
if Contains (Pragmas_Seen, Prag) then
return;
end if;
-- Extract arguments of the Default_Initial_Condition pragma
Prag_Expr_Arg := First (Pragma_Argument_Associations (Prag));
Prag_Expr := Expression_Copy (Prag_Expr_Arg);
-- Pick up the implicit second argument of the pragma, which
-- indicates the type that the pragma applies to.
Prag_Typ_Arg := Next (Prag_Expr_Arg);
if Present (Prag_Typ_Arg) then
Prag_Typ := Get_Pragma_Arg (Prag_Typ_Arg);
else
Prag_Typ := Empty;
end if;
-- The pragma applies to the partial view of the parent type
if Present (Priv_Typ)
and then Present (Prag_Typ)
and then Entity (Prag_Typ) = Priv_Typ
then
Par_Typ := Priv_Typ;
-- The pragma applies to the full view of the parent type
elsif Present (Full_Typ)
and then Present (Prag_Typ)
and then Entity (Prag_Typ) = Full_Typ
then
Par_Typ := Full_Typ;
-- Otherwise the pragma does not belong to the parent type and
-- should not be considered.
else
return;
end if;
-- Substitute references in the DIC expression that are related
-- to the partial type with corresponding references related to
-- the derived type (call to Replace_References below).
Expr := New_Copy_Tree (Prag_Expr);
Par_Proc := Partial_DIC_Procedure (Par_Typ);
-- If there's not a partial DIC procedure (such as when a
-- full type doesn't have its own DIC, but is inherited from
-- a type with DIC), get the full DIC procedure.
if not Present (Par_Proc) then
Par_Proc := DIC_Procedure (Par_Typ);
end if;
Replace_References
(Expr => Expr,
Par_Typ => Par_Typ,
Deriv_Typ => Deriv_Typ,
Par_Obj => First_Formal (Par_Proc),
Deriv_Obj => Obj_Id);
-- Why are there different actions depending on whether T is
-- tagged? Can these be unified? ???
if Is_Tagged_Type (T) then
Add_Inherited_Tagged_DIC
(DIC_Prag => Prag,
Expr => Expr,
Stmts => Checks);
else
Add_Inherited_DIC
(DIC_Prag => Prag,
Par_Typ => Par_Typ,
Deriv_Typ => Deriv_Typ,
Stmts => Checks);
end if;
-- Leave as soon as we get a DIC pragma, since we'll visit
-- the pragmas of the parents, so will get to any "inherited"
-- pragmas that way.
return;
end if;
Next_Rep_Item (Prag);
end loop;
end Add_Inherited_DICs;
-----------------
-- Add_Own_DIC --
-----------------
procedure Add_Own_DIC
(DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
Obj_Id : Entity_Id;
Stmts : in out List_Id)
is
DIC_Args : constant List_Id :=
Pragma_Argument_Associations (DIC_Prag);
DIC_Arg : constant Node_Id := First (DIC_Args);
DIC_Asp : constant Node_Id := Corresponding_Aspect (DIC_Prag);
DIC_Expr : constant Node_Id := Get_Pragma_Arg (DIC_Arg);
-- Local variables
Typ_Decl : constant Node_Id := Declaration_Node (DIC_Typ);
Expr : Node_Id;
-- Start of processing for Add_Own_DIC
begin
pragma Assert (Present (DIC_Expr));
Expr := New_Copy_Tree (DIC_Expr);
-- Perform the following substitution:
-- * Replace the current instance of DIC_Typ with a reference to
-- the _object formal parameter of the DIC procedure.
Replace_Type_References
(Expr => Expr,
Typ => DIC_Typ,
Obj_Id => Obj_Id);
-- Preanalyze the DIC expression to detect errors and at the same
-- time capture the visibility of the proper package part.
Set_Parent (Expr, Typ_Decl);
Preanalyze_Assert_Expression (Expr, Any_Boolean);
-- Save a copy of the expression with all replacements and analysis
-- already taken place in case a derived type inherits the pragma.
-- The copy will be used as the foundation of the derived type's own
-- version of the DIC assertion expression.
if Is_Tagged_Type (DIC_Typ) then
Set_Expression_Copy (DIC_Arg, New_Copy_Tree (Expr));
end if;
-- If the pragma comes from an aspect specification, replace the
-- saved expression because all type references must be substituted
-- for the call to Preanalyze_Spec_Expression in Check_Aspect_At_xxx
-- routines.
if Present (DIC_Asp) then
Set_Entity (Identifier (DIC_Asp), New_Copy_Tree (Expr));
end if;
-- Once the DIC assertion expression is fully processed, add a check
-- to the statements of the DIC procedure (unless the type is an
-- abstract type, in which case we don't want the possibility of
-- generating a call to an abstract function of the type; such DIC
-- procedures can never be called in any case, so not generating the
-- check at all is OK).
if not Is_Abstract_Type (DIC_Typ) or else GNATprove_Mode then
Add_DIC_Check
(DIC_Prag => DIC_Prag,
DIC_Expr => Expr,
Stmts => Stmts);
end if;
end Add_Own_DIC;
---------------------
-- Add_Parent_DICs --
---------------------
procedure Add_Parent_DICs
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id)
is
Dummy_1 : Entity_Id;
Dummy_2 : Entity_Id;
Curr_Typ : Entity_Id;
-- The entity of the current type being examined
Full_Typ : Entity_Id;
-- The full view of Par_Typ
Par_Typ : Entity_Id;
-- The entity of the parent type
Priv_Typ : Entity_Id;
-- The partial view of Par_Typ
Op_Node : Elmt_Id;
Par_Prim : Entity_Id;
Prim : Entity_Id;
begin
-- Map the overridden primitive to the overriding one; required by
-- Replace_References (called by Add_Inherited_DICs) to handle calls
-- to parent primitives.
Op_Node := First_Elmt (Primitive_Operations (T));
while Present (Op_Node) loop
Prim := Node (Op_Node);
if Present (Overridden_Operation (Prim))
and then Comes_From_Source (Prim)
then
Par_Prim := Overridden_Operation (Prim);
-- Create a mapping of the form:
-- parent type primitive -> derived type primitive
Type_Map.Set (Par_Prim, Prim);
end if;
Next_Elmt (Op_Node);
end loop;
-- Climb the parent type chain
Curr_Typ := T;
loop
-- Do not consider subtypes, as they inherit the DICs from their
-- base types.
Par_Typ := Base_Type (Etype (Base_Type (Curr_Typ)));
-- Stop the climb once the root of the parent chain is
-- reached.
exit when Curr_Typ = Par_Typ;
-- Process the DICs of the parent type
Get_Views (Par_Typ, Priv_Typ, Full_Typ, Dummy_1, Dummy_2);
-- Only try to inherit a DIC pragma from the parent type Par_Typ
-- if it Has_Own_DIC pragma. The loop will proceed up the parent
-- chain to find all types that have their own DIC.
if Has_Own_DIC (Par_Typ) then
Add_Inherited_DICs
(T => T,
Priv_Typ => Priv_Typ,
Full_Typ => Full_Typ,
Obj_Id => Obj_Id,
Checks => Checks);
end if;
Curr_Typ := Par_Typ;
end loop;
end Add_Parent_DICs;
-- Local variables
Loc : constant Source_Ptr := Sloc (Typ);
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
-- Save the Ghost-related attributes to restore on exit
DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
Dummy_1 : Entity_Id;
Dummy_2 : Entity_Id;
Proc_Body : Node_Id;
Proc_Body_Id : Entity_Id;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
Stmts : List_Id := No_List;
CRec_Typ : Entity_Id := Empty;
-- The corresponding record type of Full_Typ
Full_Typ : Entity_Id := Empty;
-- The full view of the working type
Obj_Id : Entity_Id := Empty;
-- The _object formal parameter of the invariant procedure
Part_Proc : Entity_Id := Empty;
-- The entity of the "partial" invariant procedure
Priv_Typ : Entity_Id := Empty;
-- The partial view of the working type
Work_Typ : Entity_Id;
-- The working type
-- Start of processing for Build_DIC_Procedure_Body
begin
Work_Typ := Base_Type (Typ);
-- Do not process class-wide types as these are Itypes, but lack a first
-- subtype (see below).
if Is_Class_Wide_Type (Work_Typ) then
return;
-- Do not process the underlying full view of a private type. There is
-- no way to get back to the partial view, plus the body will be built
-- by the full view or the base type.
elsif Is_Underlying_Full_View (Work_Typ) then
return;
-- Use the first subtype when dealing with various base types
elsif Is_Itype (Work_Typ) then
Work_Typ := First_Subtype (Work_Typ);
-- The input denotes the corresponding record type of a protected or a
-- task type. Work with the concurrent type because the corresponding
-- record type may not be visible to clients of the type.
elsif Ekind (Work_Typ) = E_Record_Type
and then Is_Concurrent_Record_Type (Work_Typ)
then
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
-- The working type may be subject to pragma Ghost. Set the mode now to
-- ensure that the DIC procedure is properly marked as Ghost.
Set_Ghost_Mode (Work_Typ);
-- The working type must be either define a DIC pragma of its own or
-- inherit one from a parent type.
pragma Assert (Has_DIC (Work_Typ));
-- Recover the type which defines the DIC pragma. This is either the
-- working type itself or a parent type when the pragma is inherited.
DIC_Typ := Find_DIC_Type (Work_Typ);
pragma Assert (Present (DIC_Typ));
DIC_Prag := Get_Pragma (DIC_Typ, Pragma_Default_Initial_Condition);
pragma Assert (Present (DIC_Prag));
-- Nothing to do if pragma DIC appears without an argument or its sole
-- argument is "null".
if not Is_Verifiable_DIC_Pragma (DIC_Prag) then
goto Leave;
end if;
-- Obtain both views of the type
Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy_1, CRec_Typ);
-- The caller requests a body for the partial DIC procedure
if Partial_DIC then
Proc_Id := Partial_DIC_Procedure (Work_Typ);
-- The "full" DIC procedure body was already created
-- Create a declaration for the "partial" DIC procedure if it
-- is not available.
if No (Proc_Id) then
Build_DIC_Procedure_Declaration
(Typ => Work_Typ,
Partial_DIC => True);
Proc_Id := Partial_DIC_Procedure (Work_Typ);
end if;
-- The caller requests a body for the "full" DIC procedure
else
Proc_Id := DIC_Procedure (Work_Typ);
Part_Proc := Partial_DIC_Procedure (Work_Typ);
-- Create a declaration for the "full" DIC procedure if it is
-- not available.
if No (Proc_Id) then
Build_DIC_Procedure_Declaration (Work_Typ);
Proc_Id := DIC_Procedure (Work_Typ);
end if;
end if;
-- At this point there should be a DIC procedure declaration
pragma Assert (Present (Proc_Id));
Proc_Decl := Unit_Declaration_Node (Proc_Id);
-- Nothing to do if the DIC procedure already has a body
if Present (Corresponding_Body (Proc_Decl)) then
goto Leave;
end if;
-- Emulate the environment of the DIC procedure by installing its scope
-- and formal parameters.
Push_Scope (Proc_Id);
Install_Formals (Proc_Id);
Obj_Id := First_Formal (Proc_Id);
pragma Assert (Present (Obj_Id));
-- The "partial" DIC procedure verifies the DICs of the partial view
-- only.
if Partial_DIC then
pragma Assert (Present (Priv_Typ));
if Has_Own_DIC (Work_Typ) then -- If we're testing this then maybe
Add_Own_DIC -- we shouldn't be calling Find_DIC_Typ above???
(DIC_Prag => DIC_Prag,
DIC_Typ => DIC_Typ, -- Should this just be Work_Typ???
Obj_Id => Obj_Id,
Stmts => Stmts);
end if;
-- Otherwise, the "full" DIC procedure verifies the DICs inherited from
-- parent types, as well as indirectly verifying the DICs of the partial
-- view by calling the "partial" DIC procedure.
else
-- Check the DIC of the partial view by calling the "partial" DIC
-- procedure, unless the partial DIC body is empty. Generate:
-- <Work_Typ>Partial_DIC (_object);
if Present (Part_Proc) and then not Has_Null_Body (Part_Proc) then
Append_New_To (Stmts,
Make_Procedure_Call_Statement (Loc,
Name => New_Occurrence_Of (Part_Proc, Loc),
Parameter_Associations => New_List (
New_Occurrence_Of (Obj_Id, Loc))));
end if;
-- Process inherited Default_Initial_Conditions for all parent types
Add_Parent_DICs (Work_Typ, Obj_Id, Stmts);
end if;
End_Scope;
-- Produce an empty completing body in the following cases:
-- * Assertions are disabled
-- * The DIC Assertion_Policy is Ignore
if No (Stmts) then
Stmts := New_List (Make_Null_Statement (Loc));
end if;
-- Generate:
-- procedure <Work_Typ>DIC (_object : <Work_Typ>) is
-- begin
-- <Stmts>
-- end <Work_Typ>DIC;
Proc_Body :=
Make_Subprogram_Body (Loc,
Specification =>
Copy_Subprogram_Spec (Parent (Proc_Id)),
Declarations => Empty_List,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
Statements => Stmts));
Proc_Body_Id := Defining_Entity (Proc_Body);
-- Perform minor decoration in case the body is not analyzed
Mutate_Ekind (Proc_Body_Id, E_Subprogram_Body);
Set_Etype (Proc_Body_Id, Standard_Void_Type);
Set_Scope (Proc_Body_Id, Current_Scope);
Set_SPARK_Pragma (Proc_Body_Id, SPARK_Pragma (Proc_Id));
Set_SPARK_Pragma_Inherited
(Proc_Body_Id, SPARK_Pragma_Inherited (Proc_Id));
-- Link both spec and body to avoid generating duplicates
Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
Set_Corresponding_Spec (Proc_Body, Proc_Id);
-- The body should not be inserted into the tree when the context
-- is a generic unit because it is not part of the template.
-- Note that the body must still be generated in order to resolve the
-- DIC assertion expression.
if Inside_A_Generic then
null;
-- Semi-insert the body into the tree for GNATprove by setting its
-- Parent field. This allows for proper upstream tree traversals.
elsif GNATprove_Mode then
Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ)));
-- Otherwise the body is part of the freezing actions of the working
-- type.
else
Append_Freeze_Action (Work_Typ, Proc_Body);
end if;
<<Leave>>
Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Build_DIC_Procedure_Body;
-------------------------------------
-- Build_DIC_Procedure_Declaration --
-------------------------------------
-- WARNING: This routine manages Ghost regions. Return statements must be
-- replaced by gotos which jump to the end of the routine and restore the
-- Ghost mode.
procedure Build_DIC_Procedure_Declaration
(Typ : Entity_Id;
Partial_DIC : Boolean := False)
is
Loc : constant Source_Ptr := Sloc (Typ);
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
-- Save the Ghost-related attributes to restore on exit
DIC_Prag : Node_Id;
DIC_Typ : Entity_Id;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
Proc_Nam : Name_Id;
Typ_Decl : Node_Id;
CRec_Typ : Entity_Id;
-- The corresponding record type of Full_Typ
Full_Typ : Entity_Id;
-- The full view of working type
Obj_Id : Entity_Id;
-- The _object formal parameter of the DIC procedure
Priv_Typ : Entity_Id;
-- The partial view of working type
UFull_Typ : Entity_Id;
-- The underlying full view of Full_Typ
Work_Typ : Entity_Id;
-- The working type
begin
Work_Typ := Base_Type (Typ);
-- Do not process class-wide types as these are Itypes, but lack a first
-- subtype (see below).
if Is_Class_Wide_Type (Work_Typ) then
return;
-- Do not process the underlying full view of a private type. There is
-- no way to get back to the partial view, plus the body will be built
-- by the full view or the base type.
elsif Is_Underlying_Full_View (Work_Typ) then
return;
-- Use the first subtype when dealing with various base types
elsif Is_Itype (Work_Typ) then
Work_Typ := First_Subtype (Work_Typ);
-- The input denotes the corresponding record type of a protected or a
-- task type. Work with the concurrent type because the corresponding
-- record type may not be visible to clients of the type.
elsif Ekind (Work_Typ) = E_Record_Type
and then Is_Concurrent_Record_Type (Work_Typ)
then
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
-- The working type may be subject to pragma Ghost. Set the mode now to
-- ensure that the DIC procedure is properly marked as Ghost.
Set_Ghost_Mode (Work_Typ);
-- The type must be either subject to a DIC pragma or inherit one from a
-- parent type.
pragma Assert (Has_DIC (Work_Typ));
-- Recover the type which defines the DIC pragma. This is either the
-- working type itself or a parent type when the pragma is inherited.
DIC_Typ := Find_DIC_Type (Work_Typ);
pragma Assert (Present (DIC_Typ));
DIC_Prag := Get_Pragma (DIC_Typ, Pragma_Default_Initial_Condition);
pragma Assert (Present (DIC_Prag));
-- Nothing to do if pragma DIC appears without an argument or its sole
-- argument is "null".
if not Is_Verifiable_DIC_Pragma (DIC_Prag) then
goto Leave;
end if;
-- Nothing to do if the type already has a "partial" DIC procedure
if Partial_DIC then
if Present (Partial_DIC_Procedure (Work_Typ)) then
goto Leave;
end if;
-- Nothing to do if the type already has a "full" DIC procedure
elsif Present (DIC_Procedure (Work_Typ)) then
goto Leave;
end if;
-- The caller requests the declaration of the "partial" DIC procedure
if Partial_DIC then
Proc_Nam := New_External_Name (Chars (Work_Typ), "Partial_DIC");
-- Otherwise the caller requests the declaration of the "full" DIC
-- procedure.
else
Proc_Nam := New_External_Name (Chars (Work_Typ), "DIC");
end if;
Proc_Id :=
Make_Defining_Identifier (Loc, Chars => Proc_Nam);
-- Perform minor decoration in case the declaration is not analyzed
Mutate_Ekind (Proc_Id, E_Procedure);
Set_Etype (Proc_Id, Standard_Void_Type);
Set_Is_DIC_Procedure (Proc_Id);
Set_Scope (Proc_Id, Current_Scope);
Set_SPARK_Pragma (Proc_Id, SPARK_Mode_Pragma);
Set_SPARK_Pragma_Inherited (Proc_Id);
Set_DIC_Procedure (Work_Typ, Proc_Id);
-- The DIC procedure requires debug info when the assertion expression
-- is subject to Source Coverage Obligations.
if Generate_SCO then
Set_Debug_Info_Needed (Proc_Id);
end if;
-- Obtain all views of the input type
Get_Views (Work_Typ, Priv_Typ, Full_Typ, UFull_Typ, CRec_Typ);
-- Associate the DIC procedure and various flags with all views
Propagate_DIC_Attributes (Priv_Typ, From_Typ => Work_Typ);
Propagate_DIC_Attributes (Full_Typ, From_Typ => Work_Typ);
Propagate_DIC_Attributes (UFull_Typ, From_Typ => Work_Typ);
Propagate_DIC_Attributes (CRec_Typ, From_Typ => Work_Typ);
-- The declaration of the DIC procedure must be inserted after the
-- declaration of the partial view as this allows for proper external
-- visibility.
if Present (Priv_Typ) then
Typ_Decl := Declaration_Node (Priv_Typ);
-- Derived types with the full view as parent do not have a partial
-- view. Insert the DIC procedure after the derived type.
else
Typ_Decl := Declaration_Node (Full_Typ);
end if;
-- The type should have a declarative node
pragma Assert (Present (Typ_Decl));
-- Create the formal parameter which emulates the variable-like behavior
-- of the type's current instance.
Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject);
-- Perform minor decoration in case the declaration is not analyzed
Mutate_Ekind (Obj_Id, E_In_Parameter);
Set_Etype (Obj_Id, Work_Typ);
Set_Scope (Obj_Id, Proc_Id);
Set_First_Entity (Proc_Id, Obj_Id);
Set_Last_Entity (Proc_Id, Obj_Id);
-- Generate:
-- procedure <Work_Typ>DIC (_object : <Work_Typ>);
Proc_Decl :=
Make_Subprogram_Declaration (Loc,
Specification =>
Make_Procedure_Specification (Loc,
Defining_Unit_Name => Proc_Id,
Parameter_Specifications => New_List (
Make_Parameter_Specification (Loc,
Defining_Identifier => Obj_Id,
Parameter_Type =>
New_Occurrence_Of (Work_Typ, Loc)))));
-- The declaration should not be inserted into the tree when the context
-- is a generic unit because it is not part of the template.
if Inside_A_Generic then
null;
-- Semi-insert the declaration into the tree for GNATprove by setting
-- its Parent field. This allows for proper upstream tree traversals.
elsif GNATprove_Mode then
Set_Parent (Proc_Decl, Parent (Typ_Decl));
-- Otherwise insert the declaration
else
Insert_After_And_Analyze (Typ_Decl, Proc_Decl);
end if;
<<Leave>>
Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Build_DIC_Procedure_Declaration;
------------------------------------
-- Build_Invariant_Procedure_Body --
------------------------------------
-- WARNING: This routine manages Ghost regions. Return statements must be
-- replaced by gotos which jump to the end of the routine and restore the
-- Ghost mode.
procedure Build_Invariant_Procedure_Body
(Typ : Entity_Id;
Partial_Invariant : Boolean := False)
is
Loc : constant Source_Ptr := Sloc (Typ);
Pragmas_Seen : Elist_Id := No_Elist;
-- This list contains all invariant pragmas processed so far. The list
-- is used to avoid generating redundant invariant checks.
Produced_Check : Boolean := False;
-- This flag tracks whether the type has produced at least one invariant
-- check. The flag is used as a sanity check at the end of the routine.
-- NOTE: most of the routines in Build_Invariant_Procedure_Body are
-- intentionally unnested to avoid deep indentation of code.
-- NOTE: all Add_xxx_Invariants routines are reactive. In other words
-- they emit checks, loops (for arrays) and case statements (for record
-- variant parts) only when there are invariants to verify. This keeps
-- the body of the invariant procedure free of useless code.
procedure Add_Array_Component_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id);
-- Generate an invariant check for each component of array type T.
-- Obj_Id denotes the entity of the _object formal parameter of the
-- invariant procedure. All created checks are added to list Checks.
procedure Add_Inherited_Invariants
(T : Entity_Id;
Priv_Typ : Entity_Id;
Full_Typ : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id);
-- Generate an invariant check for each inherited class-wide invariant
-- coming from all parent types of type T. Priv_Typ and Full_Typ denote
-- the partial and full view of the parent type. Obj_Id denotes the
-- entity of the _object formal parameter of the invariant procedure.
-- All created checks are added to list Checks.
procedure Add_Interface_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id);
-- Generate an invariant check for each inherited class-wide invariant
-- coming from all interfaces implemented by type T. Obj_Id denotes the
-- entity of the _object formal parameter of the invariant procedure.
-- All created checks are added to list Checks.
procedure Add_Invariant_Check
(Prag : Node_Id;
Expr : Node_Id;
Checks : in out List_Id;
Inherited : Boolean := False);
-- Subsidiary to all Add_xxx_Invariant routines. Add a runtime check to
-- verify assertion expression Expr of pragma Prag. All generated code
-- is added to list Checks. Flag Inherited should be set when the pragma
-- is inherited from a parent or interface type.
procedure Add_Own_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id;
Priv_Item : Node_Id := Empty);
-- Generate an invariant check for each invariant found for type T.
-- Obj_Id denotes the entity of the _object formal parameter of the
-- invariant procedure. All created checks are added to list Checks.
-- Priv_Item denotes the first rep item of the private type.
procedure Add_Parent_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id);
-- Generate an invariant check for each inherited class-wide invariant
-- coming from all parent types of type T. Obj_Id denotes the entity of
-- the _object formal parameter of the invariant procedure. All created
-- checks are added to list Checks.
procedure Add_Record_Component_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id);
-- Generate an invariant check for each component of record type T.
-- Obj_Id denotes the entity of the _object formal parameter of the
-- invariant procedure. All created checks are added to list Checks.
------------------------------------
-- Add_Array_Component_Invariants --
------------------------------------
procedure Add_Array_Component_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id)
is
Comp_Typ : constant Entity_Id := Component_Type (T);
Dims : constant Pos := Number_Dimensions (T);
procedure Process_Array_Component
(Indices : List_Id;
Comp_Checks : in out List_Id);
-- Generate an invariant check for an array component identified by
-- the indices in list Indices. All created checks are added to list
-- Comp_Checks.
procedure Process_One_Dimension
(Dim : Pos;
Indices : List_Id;
Dim_Checks : in out List_Id);
-- Generate a loop over the Nth dimension Dim of an array type. List
-- Indices contains all array indices for the dimension. All created
-- checks are added to list Dim_Checks.
-----------------------------
-- Process_Array_Component --
-----------------------------
procedure Process_Array_Component
(Indices : List_Id;
Comp_Checks : in out List_Id)
is
Proc_Id : Entity_Id;
begin
if Has_Invariants (Comp_Typ) then
-- In GNATprove mode, the component invariants are checked by
-- other means. They should not be added to the array type
-- invariant procedure, so that the procedure can be used to
-- check the array type invariants if any.
if GNATprove_Mode then
null;
else
Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
-- The component type should have an invariant procedure
-- if it has invariants of its own or inherits class-wide
-- invariants from parent or interface types.
pragma Assert (Present (Proc_Id));
-- Generate:
-- <Comp_Typ>Invariant (_object (<Indices>));
-- The invariant procedure has a null body if assertions are
-- disabled or Assertion_Policy Ignore is in effect.
if not Has_Null_Body (Proc_Id) then
Append_New_To (Comp_Checks,
Make_Procedure_Call_Statement (Loc,
Name =>
New_Occurrence_Of (Proc_Id, Loc),
Parameter_Associations => New_List (
Make_Indexed_Component (Loc,
Prefix => New_Occurrence_Of (Obj_Id, Loc),
Expressions => New_Copy_List (Indices)))));
end if;
end if;
Produced_Check := True;
end if;
end Process_Array_Component;
---------------------------
-- Process_One_Dimension --
---------------------------
procedure Process_One_Dimension
(Dim : Pos;
Indices : List_Id;
Dim_Checks : in out List_Id)
is
Comp_Checks : List_Id := No_List;
Index : Entity_Id;
begin
-- Generate the invariant checks for the array component after all
-- dimensions have produced their respective loops.
if Dim > Dims then
Process_Array_Component
(Indices => Indices,
Comp_Checks => Dim_Checks);
-- Otherwise create a loop for the current dimension
else
-- Create a new loop variable for each dimension
Index :=
Make_Defining_Identifier (Loc,
Chars => New_External_Name ('I', Dim));
Append_To (Indices, New_Occurrence_Of (Index, Loc));
Process_One_Dimension
(Dim => Dim + 1,
Indices => Indices,
Dim_Checks => Comp_Checks);
-- Generate:
-- for I<Dim> in _object'Range (<Dim>) loop
-- <Comp_Checks>
-- end loop;
-- Note that the invariant procedure may have a null body if
-- assertions are disabled or Assertion_Policy Ignore is in
-- effect.
if Present (Comp_Checks) then
Append_New_To (Dim_Checks,
Make_Implicit_Loop_Statement (T,
Identifier => Empty,
Iteration_Scheme =>
Make_Iteration_Scheme (Loc,
Loop_Parameter_Specification =>
Make_Loop_Parameter_Specification (Loc,
Defining_Identifier => Index,
Discrete_Subtype_Definition =>
Make_Attribute_Reference (Loc,
Prefix =>
New_Occurrence_Of (Obj_Id, Loc),
Attribute_Name => Name_Range,
Expressions => New_List (
Make_Integer_Literal (Loc, Dim))))),
Statements => Comp_Checks));
end if;
end if;
end Process_One_Dimension;
-- Start of processing for Add_Array_Component_Invariants
begin
Process_One_Dimension
(Dim => 1,
Indices => New_List,
Dim_Checks => Checks);
end Add_Array_Component_Invariants;
------------------------------
-- Add_Inherited_Invariants --
------------------------------
procedure Add_Inherited_Invariants
(T : Entity_Id;
Priv_Typ : Entity_Id;
Full_Typ : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id)
is
Deriv_Typ : Entity_Id;
Expr : Node_Id;
Prag : Node_Id;
Prag_Expr : Node_Id;
Prag_Expr_Arg : Node_Id;
Prag_Typ : Node_Id;
Prag_Typ_Arg : Node_Id;
Par_Proc : Entity_Id;
-- The "partial" invariant procedure of Par_Typ
Par_Typ : Entity_Id;
-- The suitable view of the parent type used in the substitution of
-- type attributes.
begin
if not Present (Priv_Typ) and then not Present (Full_Typ) then
return;
end if;
-- When the type inheriting the class-wide invariant is a concurrent
-- type, use the corresponding record type because it contains all
-- primitive operations of the concurrent type and allows for proper
-- substitution.
if Is_Concurrent_Type (T) then
Deriv_Typ := Corresponding_Record_Type (T);
else
Deriv_Typ := T;
end if;
pragma Assert (Present (Deriv_Typ));
-- Determine which rep item chain to use. Precedence is given to that
-- of the parent type's partial view since it usually carries all the
-- class-wide invariants.
if Present (Priv_Typ) then
Prag := First_Rep_Item (Priv_Typ);
else
Prag := First_Rep_Item (Full_Typ);
end if;
while Present (Prag) loop
if Nkind (Prag) = N_Pragma
and then Pragma_Name (Prag) = Name_Invariant
then
-- Nothing to do if the pragma was already processed
if Contains (Pragmas_Seen, Prag) then
return;
-- Nothing to do when the caller requests the processing of all
-- inherited class-wide invariants, but the pragma does not
-- fall in this category.
elsif not Class_Present (Prag) then
return;
end if;
-- Extract the arguments of the invariant pragma
Prag_Typ_Arg := First (Pragma_Argument_Associations (Prag));
Prag_Expr_Arg := Next (Prag_Typ_Arg);
Prag_Expr := Expression_Copy (Prag_Expr_Arg);
Prag_Typ := Get_Pragma_Arg (Prag_Typ_Arg);
-- The pragma applies to the partial view of the parent type
if Present (Priv_Typ)
and then Entity (Prag_Typ) = Priv_Typ
then
Par_Typ := Priv_Typ;
-- The pragma applies to the full view of the parent type
elsif Present (Full_Typ)
and then Entity (Prag_Typ) = Full_Typ
then
Par_Typ := Full_Typ;
-- Otherwise the pragma does not belong to the parent type and
-- should not be considered.
else
return;
end if;
-- Perform the following substitutions:
-- * Replace a reference to the _object parameter of the
-- parent type's partial invariant procedure with a
-- reference to the _object parameter of the derived
-- type's full invariant procedure.
-- * Replace a reference to a discriminant of the parent type
-- with a suitable value from the point of view of the
-- derived type.
-- * Replace a call to an overridden parent primitive with a
-- call to the overriding derived type primitive.
-- * Replace a call to an inherited parent primitive with a
-- call to the internally-generated inherited derived type
-- primitive.
Expr := New_Copy_Tree (Prag_Expr);
-- The parent type must have a "partial" invariant procedure
-- because class-wide invariants are captured exclusively by
-- it.
Par_Proc := Partial_Invariant_Procedure (Par_Typ);
pragma Assert (Present (Par_Proc));
Replace_References
(Expr => Expr,
Par_Typ => Par_Typ,
Deriv_Typ => Deriv_Typ,
Par_Obj => First_Formal (Par_Proc),
Deriv_Obj => Obj_Id);
Add_Invariant_Check (Prag, Expr, Checks, Inherited => True);
end if;
Next_Rep_Item (Prag);
end loop;
end Add_Inherited_Invariants;
------------------------------
-- Add_Interface_Invariants --
------------------------------
procedure Add_Interface_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id)
is
Iface_Elmt : Elmt_Id;
Ifaces : Elist_Id;
begin
-- Generate an invariant check for each class-wide invariant coming
-- from all interfaces implemented by type T.
if Is_Tagged_Type (T) then
Collect_Interfaces (T, Ifaces);
-- Process the class-wide invariants of all implemented interfaces
Iface_Elmt := First_Elmt (Ifaces);
while Present (Iface_Elmt) loop
-- The Full_Typ parameter is intentionally left Empty because
-- interfaces are treated as the partial view of a private type
-- in order to achieve uniformity with the general case.
Add_Inherited_Invariants
(T => T,
Priv_Typ => Node (Iface_Elmt),
Full_Typ => Empty,
Obj_Id => Obj_Id,
Checks => Checks);
Next_Elmt (Iface_Elmt);
end loop;
end if;
end Add_Interface_Invariants;
-------------------------
-- Add_Invariant_Check --
-------------------------
procedure Add_Invariant_Check
(Prag : Node_Id;
Expr : Node_Id;
Checks : in out List_Id;
Inherited : Boolean := False)
is
Args : constant List_Id := Pragma_Argument_Associations (Prag);
Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag);
Ploc : constant Source_Ptr := Sloc (Prag);
Str_Arg : constant Node_Id := Next (Next (First (Args)));
Assoc : List_Id;
Str : String_Id;
begin
-- The invariant is ignored, nothing left to do
if Is_Ignored (Prag) then
null;
-- Otherwise the invariant is checked. Build a pragma Check to verify
-- the expression at run time.
else
Assoc := New_List (
Make_Pragma_Argument_Association (Ploc,
Expression => Make_Identifier (Ploc, Nam)),
Make_Pragma_Argument_Association (Ploc,
Expression => Expr));
-- Handle the String argument (if any)
if Present (Str_Arg) then
Str := Strval (Get_Pragma_Arg (Str_Arg));
-- When inheriting an invariant, modify the message from
-- "failed invariant" to "failed inherited invariant".
if Inherited then
String_To_Name_Buffer (Str);
if Name_Buffer (1 .. 16) = "failed invariant" then
Insert_Str_In_Name_Buffer ("inherited ", 8);
Str := String_From_Name_Buffer;
end if;
end if;
Append_To (Assoc,
Make_Pragma_Argument_Association (Ploc,
Expression => Make_String_Literal (Ploc, Str)));
end if;
-- Generate:
-- pragma Check (<Nam>, <Expr>, <Str>);
Append_New_To (Checks,
Make_Pragma (Ploc,
Chars => Name_Check,
Pragma_Argument_Associations => Assoc));
end if;
-- Output an info message when inheriting an invariant and the
-- listing option is enabled.
if Inherited and Opt.List_Inherited_Aspects then
Error_Msg_Sloc := Sloc (Prag);
Error_Msg_N
("info: & inherits `Invariant''Class` aspect from #?L?", Typ);
end if;
-- Add the pragma to the list of processed pragmas
Append_New_Elmt (Prag, Pragmas_Seen);
Produced_Check := True;
end Add_Invariant_Check;
---------------------------
-- Add_Parent_Invariants --
---------------------------
procedure Add_Parent_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id)
is
Dummy_1 : Entity_Id;
Dummy_2 : Entity_Id;
Curr_Typ : Entity_Id;
-- The entity of the current type being examined
Full_Typ : Entity_Id;
-- The full view of Par_Typ
Par_Typ : Entity_Id;
-- The entity of the parent type
Priv_Typ : Entity_Id;
-- The partial view of Par_Typ
begin
-- Do not process array types because they cannot have true parent
-- types. This also prevents the generation of a duplicate invariant
-- check when the input type is an array base type because its Etype
-- denotes the first subtype, both of which share the same component
-- type.
if Is_Array_Type (T) then
return;
end if;
-- Climb the parent type chain
Curr_Typ := T;
loop
-- Do not consider subtypes as they inherit the invariants
-- from their base types.
Par_Typ := Base_Type (Etype (Curr_Typ));
-- Stop the climb once the root of the parent chain is
-- reached.
exit when Curr_Typ = Par_Typ;
-- Process the class-wide invariants of the parent type
Get_Views (Par_Typ, Priv_Typ, Full_Typ, Dummy_1, Dummy_2);
-- Process the elements of an array type
if Is_Array_Type (Full_Typ) then
Add_Array_Component_Invariants (Full_Typ, Obj_Id, Checks);
-- Process the components of a record type
elsif Ekind (Full_Typ) = E_Record_Type then
Add_Record_Component_Invariants (Full_Typ, Obj_Id, Checks);
end if;
Add_Inherited_Invariants
(T => T,
Priv_Typ => Priv_Typ,
Full_Typ => Full_Typ,
Obj_Id => Obj_Id,
Checks => Checks);
Curr_Typ := Par_Typ;
end loop;
end Add_Parent_Invariants;
------------------------
-- Add_Own_Invariants --
------------------------
procedure Add_Own_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id;
Priv_Item : Node_Id := Empty)
is
Expr : Node_Id;
Prag : Node_Id;
Prag_Asp : Node_Id;
Prag_Expr : Node_Id;
Prag_Expr_Arg : Node_Id;
Prag_Typ : Node_Id;
Prag_Typ_Arg : Node_Id;
begin
if not Present (T) then
return;
end if;
Prag := First_Rep_Item (T);
while Present (Prag) loop
if Nkind (Prag) = N_Pragma
and then Pragma_Name (Prag) = Name_Invariant
then
-- Stop the traversal of the rep item chain once a specific
-- item is encountered.
if Present (Priv_Item) and then Prag = Priv_Item then
exit;
end if;
-- Nothing to do if the pragma was already processed
if Contains (Pragmas_Seen, Prag) then
return;
end if;
-- Extract the arguments of the invariant pragma
Prag_Typ_Arg := First (Pragma_Argument_Associations (Prag));
Prag_Expr_Arg := Next (Prag_Typ_Arg);
Prag_Expr := Get_Pragma_Arg (Prag_Expr_Arg);
Prag_Typ := Get_Pragma_Arg (Prag_Typ_Arg);
Prag_Asp := Corresponding_Aspect (Prag);
-- Verify the pragma belongs to T, otherwise the pragma applies
-- to a parent type in which case it will be processed later by
-- Add_Parent_Invariants or Add_Interface_Invariants.
if Entity (Prag_Typ) /= T then
return;
end if;
Expr := New_Copy_Tree (Prag_Expr);
-- Substitute all references to type T with references to the
-- _object formal parameter.
Replace_Type_References (Expr, T, Obj_Id);
-- Preanalyze the invariant expression to detect errors and at
-- the same time capture the visibility of the proper package
-- part.
Set_Parent (Expr, Parent (Prag_Expr));
Preanalyze_Assert_Expression (Expr, Any_Boolean);
-- Save a copy of the expression when T is tagged to detect
-- errors and capture the visibility of the proper package part
-- for the generation of inherited type invariants.
if Is_Tagged_Type (T) then
Set_Expression_Copy (Prag_Expr_Arg, New_Copy_Tree (Expr));
end if;
-- If the pragma comes from an aspect specification, replace
-- the saved expression because all type references must be
-- substituted for the call to Preanalyze_Spec_Expression in
-- Check_Aspect_At_xxx routines.
if Present (Prag_Asp) then
Set_Entity (Identifier (Prag_Asp), New_Copy_Tree (Expr));
end if;
Add_Invariant_Check (Prag, Expr, Checks);
end if;
Next_Rep_Item (Prag);
end loop;
end Add_Own_Invariants;
-------------------------------------
-- Add_Record_Component_Invariants --
-------------------------------------
procedure Add_Record_Component_Invariants
(T : Entity_Id;
Obj_Id : Entity_Id;
Checks : in out List_Id)
is
procedure Process_Component_List
(Comp_List : Node_Id;
CL_Checks : in out List_Id);
-- Generate invariant checks for all record components found in
-- component list Comp_List, including variant parts. All created
-- checks are added to list CL_Checks.
procedure Process_Record_Component
(Comp_Id : Entity_Id;
Comp_Checks : in out List_Id);
-- Generate an invariant check for a record component identified by
-- Comp_Id. All created checks are added to list Comp_Checks.
----------------------------
-- Process_Component_List --
----------------------------
procedure Process_Component_List
(Comp_List : Node_Id;
CL_Checks : in out List_Id)
is
Comp : Node_Id;
Var : Node_Id;
Var_Alts : List_Id := No_List;
Var_Checks : List_Id := No_List;
Var_Stmts : List_Id;
Produced_Variant_Check : Boolean := False;
-- This flag tracks whether the component has produced at least
-- one invariant check.
begin
-- Traverse the component items
Comp := First (Component_Items (Comp_List));
while Present (Comp) loop
if Nkind (Comp) = N_Component_Declaration then
-- Generate the component invariant check
Process_Record_Component
(Comp_Id => Defining_Entity (Comp),
Comp_Checks => CL_Checks);
end if;
Next (Comp);
end loop;
-- Traverse the variant part
if Present (Variant_Part (Comp_List)) then
Var := First (Variants (Variant_Part (Comp_List)));
while Present (Var) loop
Var_Checks := No_List;
-- Generate invariant checks for all components and variant
-- parts that qualify.
Process_Component_List
(Comp_List => Component_List (Var),
CL_Checks => Var_Checks);
-- The components of the current variant produced at least
-- one invariant check.
if Present (Var_Checks) then
Var_Stmts := Var_Checks;
Produced_Variant_Check := True;
-- Otherwise there are either no components with invariants,
-- assertions are disabled, or Assertion_Policy Ignore is in
-- effect.
else
Var_Stmts := New_List (Make_Null_Statement (Loc));
end if;
Append_New_To (Var_Alts,
Make_Case_Statement_Alternative (Loc,
Discrete_Choices =>
New_Copy_List (Discrete_Choices (Var)),
Statements => Var_Stmts));
Next (Var);
end loop;
-- Create a case statement which verifies the invariant checks
-- of a particular component list depending on the discriminant
-- values only when there is at least one real invariant check.
if Produced_Variant_Check then
Append_New_To (CL_Checks,
Make_Case_Statement (Loc,
Expression =>
Make_Selected_Component (Loc,
Prefix => New_Occurrence_Of (Obj_Id, Loc),
Selector_Name =>
New_Occurrence_Of
(Entity (Name (Variant_Part (Comp_List))), Loc)),
Alternatives => Var_Alts));
end if;
end if;
end Process_Component_List;
------------------------------
-- Process_Record_Component --
------------------------------
procedure Process_Record_Component
(Comp_Id : Entity_Id;
Comp_Checks : in out List_Id)
is
Comp_Typ : constant Entity_Id := Etype (Comp_Id);
Proc_Id : Entity_Id;
Produced_Component_Check : Boolean := False;
-- This flag tracks whether the component has produced at least
-- one invariant check.
begin
-- Nothing to do for internal component _parent. Note that it is
-- not desirable to check whether the component comes from source
-- because protected type components are relocated to an internal
-- corresponding record, but still need processing.
if Chars (Comp_Id) = Name_uParent then
return;
end if;
-- Verify the invariant of the component. Note that an access
-- type may have an invariant when it acts as the full view of a
-- private type and the invariant appears on the partial view. In
-- this case verify the access value itself.
if Has_Invariants (Comp_Typ) then
-- In GNATprove mode, the component invariants are checked by
-- other means. They should not be added to the record type
-- invariant procedure, so that the procedure can be used to
-- check the record type invariants if any.
if GNATprove_Mode then
null;
else
Proc_Id := Invariant_Procedure (Base_Type (Comp_Typ));
-- The component type should have an invariant procedure
-- if it has invariants of its own or inherits class-wide
-- invariants from parent or interface types.
pragma Assert (Present (Proc_Id));
-- Generate:
-- <Comp_Typ>Invariant (T (_object).<Comp_Id>);
-- Note that the invariant procedure may have a null body if
-- assertions are disabled or Assertion_Policy Ignore is in
-- effect.
if not Has_Null_Body (Proc_Id) then
Append_New_To (Comp_Checks,
Make_Procedure_Call_Statement (Loc,
Name =>
New_Occurrence_Of (Proc_Id, Loc),
Parameter_Associations => New_List (
Make_Selected_Component (Loc,
Prefix =>
Unchecked_Convert_To
(T, New_Occurrence_Of (Obj_Id, Loc)),
Selector_Name =>
New_Occurrence_Of (Comp_Id, Loc)))));
end if;
end if;
Produced_Check := True;
Produced_Component_Check := True;
end if;
if Produced_Component_Check and then Has_Unchecked_Union (T) then
Error_Msg_NE
("invariants cannot be checked on components of "
& "unchecked_union type &??", Comp_Id, T);
end if;
end Process_Record_Component;
-- Local variables
Comps : Node_Id;
Def : Node_Id;
-- Start of processing for Add_Record_Component_Invariants
begin
-- An untagged derived type inherits the components of its parent
-- type. In order to avoid creating redundant invariant checks, do
-- not process the components now. Instead wait until the ultimate
-- parent of the untagged derivation chain is reached.
if not Is_Untagged_Derivation (T) then
Def := Type_Definition (Parent (T));
if Nkind (Def) = N_Derived_Type_Definition then
Def := Record_Extension_Part (Def);
end if;
pragma Assert (Nkind (Def) = N_Record_Definition);
Comps := Component_List (Def);
if Present (Comps) then
Process_Component_List
(Comp_List => Comps,
CL_Checks => Checks);
end if;
end if;
end Add_Record_Component_Invariants;
-- Local variables
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
-- Save the Ghost-related attributes to restore on exit
Dummy : Entity_Id;
Priv_Item : Node_Id;
Proc_Body : Node_Id;
Proc_Body_Id : Entity_Id;
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
Stmts : List_Id := No_List;
CRec_Typ : Entity_Id := Empty;
-- The corresponding record type of Full_Typ
Full_Proc : Entity_Id := Empty;
-- The entity of the "full" invariant procedure
Full_Typ : Entity_Id := Empty;
-- The full view of the working type
Obj_Id : Entity_Id := Empty;
-- The _object formal parameter of the invariant procedure
Part_Proc : Entity_Id := Empty;
-- The entity of the "partial" invariant procedure
Priv_Typ : Entity_Id := Empty;
-- The partial view of the working type
Work_Typ : Entity_Id := Empty;
-- The working type
-- Start of processing for Build_Invariant_Procedure_Body
begin
Work_Typ := Typ;
-- Do not process the underlying full view of a private type. There is
-- no way to get back to the partial view, plus the body will be built
-- by the full view or the base type.
if Is_Underlying_Full_View (Work_Typ) then
return;
-- The input type denotes the implementation base type of a constrained
-- array type. Work with the first subtype as all invariant pragmas are
-- on its rep item chain.
elsif Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then
Work_Typ := First_Subtype (Work_Typ);
-- The input type denotes the corresponding record type of a protected
-- or task type. Work with the concurrent type because the corresponding
-- record type may not be visible to clients of the type.
elsif Ekind (Work_Typ) = E_Record_Type
and then Is_Concurrent_Record_Type (Work_Typ)
then
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
-- The working type may be subject to pragma Ghost. Set the mode now to
-- ensure that the invariant procedure is properly marked as Ghost.
Set_Ghost_Mode (Work_Typ);
-- The type must either have invariants of its own, inherit class-wide
-- invariants from parent types or interfaces, or be an array or record
-- type whose components have invariants.
pragma Assert (Has_Invariants (Work_Typ));
-- Interfaces are treated as the partial view of a private type in order
-- to achieve uniformity with the general case.
if Is_Interface (Work_Typ) then
Priv_Typ := Work_Typ;
-- Otherwise obtain both views of the type
else
Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy, CRec_Typ);
end if;
-- The caller requests a body for the partial invariant procedure
if Partial_Invariant then
Full_Proc := Invariant_Procedure (Work_Typ);
Proc_Id := Partial_Invariant_Procedure (Work_Typ);
-- The "full" invariant procedure body was already created
if Present (Full_Proc)
and then Present
(Corresponding_Body (Unit_Declaration_Node (Full_Proc)))
then
-- This scenario happens only when the type is an untagged
-- derivation from a private parent and the underlying full
-- view was processed before the partial view.
pragma Assert
(Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ));
-- Nothing to do because the processing of the underlying full
-- view already checked the invariants of the partial view.
goto Leave;
end if;
-- Create a declaration for the "partial" invariant procedure if it
-- is not available.
if No (Proc_Id) then
Build_Invariant_Procedure_Declaration
(Typ => Work_Typ,
Partial_Invariant => True);
Proc_Id := Partial_Invariant_Procedure (Work_Typ);
end if;
-- The caller requests a body for the "full" invariant procedure
else
Proc_Id := Invariant_Procedure (Work_Typ);
Part_Proc := Partial_Invariant_Procedure (Work_Typ);
-- Create a declaration for the "full" invariant procedure if it is
-- not available.
if No (Proc_Id) then
Build_Invariant_Procedure_Declaration (Work_Typ);
Proc_Id := Invariant_Procedure (Work_Typ);
end if;
end if;
-- At this point there should be an invariant procedure declaration
pragma Assert (Present (Proc_Id));
Proc_Decl := Unit_Declaration_Node (Proc_Id);
-- Nothing to do if the invariant procedure already has a body
if Present (Corresponding_Body (Proc_Decl)) then
goto Leave;
end if;
-- Emulate the environment of the invariant procedure by installing its
-- scope and formal parameters. Note that this is not needed, but having
-- the scope installed helps with the detection of invariant-related
-- errors.
Push_Scope (Proc_Id);
Install_Formals (Proc_Id);
Obj_Id := First_Formal (Proc_Id);
pragma Assert (Present (Obj_Id));
-- The "partial" invariant procedure verifies the invariants of the
-- partial view only.
if Partial_Invariant then
pragma Assert (Present (Priv_Typ));
Add_Own_Invariants
(T => Priv_Typ,
Obj_Id => Obj_Id,
Checks => Stmts);
-- Otherwise the "full" invariant procedure verifies the invariants of
-- the full view, all array or record components, as well as class-wide
-- invariants inherited from parent types or interfaces. In addition, it
-- indirectly verifies the invariants of the partial view by calling the
-- "partial" invariant procedure.
else
pragma Assert (Present (Full_Typ));
-- Check the invariants of the partial view by calling the "partial"
-- invariant procedure. Generate:
-- <Work_Typ>Partial_Invariant (_object);
if Present (Part_Proc) then
Append_New_To (Stmts,
Make_Procedure_Call_Statement (Loc,
Name => New_Occurrence_Of (Part_Proc, Loc),
Parameter_Associations => New_List (
New_Occurrence_Of (Obj_Id, Loc))));
Produced_Check := True;
end if;
Priv_Item := Empty;
-- Derived subtypes do not have a partial view
if Present (Priv_Typ) then
-- The processing of the "full" invariant procedure intentionally
-- skips the partial view because a) this may result in changes of
-- visibility and b) lead to duplicate checks. However, when the
-- full view is the underlying full view of an untagged derived
-- type whose parent type is private, partial invariants appear on
-- the rep item chain of the partial view only.
-- package Pack_1 is
-- type Root ... is private;
-- private
-- <full view of Root>
-- end Pack_1;
-- with Pack_1;
-- package Pack_2 is
-- type Child is new Pack_1.Root with Type_Invariant => ...;
-- <underlying full view of Child>
-- end Pack_2;
-- As a result, the processing of the full view must also consider
-- all invariants of the partial view.
if Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ) then
null;
-- Otherwise the invariants of the partial view are ignored
else
-- Note that the rep item chain is shared between the partial
-- and full views of a type. To avoid processing the invariants
-- of the partial view, signal the logic to stop when the first
-- rep item of the partial view has been reached.
Priv_Item := First_Rep_Item (Priv_Typ);
-- Ignore the invariants of the partial view by eliminating the
-- view.
Priv_Typ := Empty;
end if;
end if;
-- Process the invariants of the full view and in certain cases those
-- of the partial view. This also handles any invariants on array or
-- record components.
Add_Own_Invariants
(T => Priv_Typ,
Obj_Id => Obj_Id,
Checks => Stmts,
Priv_Item => Priv_Item);
Add_Own_Invariants
(T => Full_Typ,
Obj_Id => Obj_Id,
Checks => Stmts,
Priv_Item => Priv_Item);
-- Process the elements of an array type
if Is_Array_Type (Full_Typ) then
Add_Array_Component_Invariants (Full_Typ, Obj_Id, Stmts);
-- Process the components of a record type
elsif Ekind (Full_Typ) = E_Record_Type then
Add_Record_Component_Invariants (Full_Typ, Obj_Id, Stmts);
-- Process the components of a corresponding record
elsif Present (CRec_Typ) then
Add_Record_Component_Invariants (CRec_Typ, Obj_Id, Stmts);
end if;
-- Process the inherited class-wide invariants of all parent types.
-- This also handles any invariants on record components.
Add_Parent_Invariants (Full_Typ, Obj_Id, Stmts);
-- Process the inherited class-wide invariants of all implemented
-- interface types.
Add_Interface_Invariants (Full_Typ, Obj_Id, Stmts);
end if;
End_Scope;
-- At this point there should be at least one invariant check. If this
-- is not the case, then the invariant-related flags were not properly
-- set, or there is a missing invariant procedure on one of the array
-- or record components.
pragma Assert (Produced_Check);
-- Account for the case where assertions are disabled or all invariant
-- checks are subject to Assertion_Policy Ignore. Produce a completing
-- empty body.
if No (Stmts) then
Stmts := New_List (Make_Null_Statement (Loc));
end if;
-- Generate:
-- procedure <Work_Typ>[Partial_]Invariant (_object : <Obj_Typ>) is
-- begin
-- <Stmts>
-- end <Work_Typ>[Partial_]Invariant;
Proc_Body :=
Make_Subprogram_Body (Loc,
Specification =>
Copy_Subprogram_Spec (Parent (Proc_Id)),
Declarations => Empty_List,
Handled_Statement_Sequence =>
Make_Handled_Sequence_Of_Statements (Loc,
Statements => Stmts));
Proc_Body_Id := Defining_Entity (Proc_Body);
-- Perform minor decoration in case the body is not analyzed
Mutate_Ekind (Proc_Body_Id, E_Subprogram_Body);
Set_Etype (Proc_Body_Id, Standard_Void_Type);
Set_Scope (Proc_Body_Id, Current_Scope);
-- Link both spec and body to avoid generating duplicates
Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
Set_Corresponding_Spec (Proc_Body, Proc_Id);
-- The body should not be inserted into the tree when the context is
-- a generic unit because it is not part of the template. Note
-- that the body must still be generated in order to resolve the
-- invariants.
if Inside_A_Generic then
null;
-- Semi-insert the body into the tree for GNATprove by setting its
-- Parent field. This allows for proper upstream tree traversals.
elsif GNATprove_Mode then
Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ)));
-- Otherwise the body is part of the freezing actions of the type
else
Append_Freeze_Action (Work_Typ, Proc_Body);
end if;
<<Leave>>
Restore_Ghost_Region (Saved_GM, Saved_IGR);
end Build_Invariant_Procedure_Body;
-------------------------------------------
-- Build_Invariant_Procedure_Declaration --
-------------------------------------------
-- WARNING: This routine manages Ghost regions. Return statements must be
-- replaced by gotos which jump to the end of the routine and restore the
-- Ghost mode.
procedure Build_Invariant_Procedure_Declaration
(Typ : Entity_Id;
Partial_Invariant : Boolean := False)
is
Loc : constant Source_Ptr := Sloc (Typ);
Saved_GM : constant Ghost_Mode_Type := Ghost_Mode;
Saved_IGR : constant Node_Id := Ignored_Ghost_Region;
-- Save the Ghost-related attributes to restore on exit
Proc_Decl : Node_Id;
Proc_Id : Entity_Id;
Proc_Nam : Name_Id;
Typ_Decl : Node_Id;
CRec_Typ : Entity_Id;
-- The corresponding record type of Full_Typ
Full_Typ : Entity_Id;
-- The full view of working type
Obj_Id : Entity_Id;
-- The _object formal parameter of the invariant procedure
Obj_Typ : Entity_Id;
-- The type of the _object formal parameter
Priv_Typ : Entity_Id;
-- The partial view of working type
UFull_Typ : Entity_Id;
-- The underlying full view of Full_Typ
Work_Typ : Entity_Id;
-- The working type
begin
Work_Typ := Typ;
-- The input type denotes the implementation base type of a constrained
-- array type. Work with the first subtype as all invariant pragmas are
-- on its rep item chain.
if Ekind (Work_Typ) = E_Array_Type and then Is_Itype (Work_Typ) then
Work_Typ := First_Subtype (Work_Typ);
-- The input denotes the corresponding record type of a protected or a
-- task type. Work with the concurrent type because the corresponding
-- record type may not be visible to clients of the type.
elsif Ekind (Work_Typ) = E_Record_Type
and then Is_Concurrent_Record_Type (Work_Typ)
then
Work_Typ := Corresponding_Concurrent_Type (Work_Typ);
end if;
-- The working type may be subject to pragma Ghost. Set the mode now to
-- ensure that the invariant procedure is properly marked as Ghost.
Set_Ghost_Mode (Work_Typ);
-- The type must either have invariants of its own, inherit class-wide
-- invariants from parent or interface types, or be an array or record
-- type whose components have invariants.
pragma Assert (Has_Invariants (Work_Typ));
-- Nothing to do if the type already has a "partial" invariant procedure
if Partial_Invariant then
if Present (Partial_Invariant_Procedure (Work_Typ)) then
goto Leave;
end if;
-- Nothing to do if the type already has a "full" invariant procedure
elsif Present (Invariant_Procedure (Work_Typ)) then
goto Leave;
end if;
-- The caller requests the declaration of the "partial" invariant
-- procedure.
if Partial_Invariant then
Proc_Nam := New_External_Name (Chars (Work_Typ), "Partial_Invariant");
-- Otherwise the caller requests the declaration of the "full" invariant
-- procedure.
else
Proc_Nam := New_External_Name (Chars (Work_Typ), "Invariant");
end if;
Proc_Id := Make_Defining_Identifier (Loc, Chars => Proc_Nam);
-- Perform minor decoration in case the declaration is not analyzed
Mutate_Ekind (Proc_Id, E_Procedure);
Set_Etype (Proc_Id, Standard_Void_Type);
Set_Scope (Proc_Id, Current_Scope);