From 51148ddab1495aa357e57f1c209940f7cde571c1 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 25 Apr 2017 11:06:09 +0200 Subject: [PATCH] [multiple changes] 2017-04-25 Hristian Kirtchev * sem_util.adb (Check_Part_Of_Reference): Continue to examine the context if the reference appears within an expression function. 2017-04-25 Justin Squirek * exp_ch7.adb, exp_ch7.ads Remove Build_Invariant_Procedure_Body and Build_Invariant_Procedure_Declaration. * exp_util.ads, exp_util.adb Add Build_Invariant_Procedure_Body and Build_Invariant_Procedure_Declaration from exp_ch7 and break-out Is_Untagged_Private_Derivation from Build_Invariant_Procedure_Body. (Replace_Type_References): Append an extra parameter to allow for dispatching replacements and add the corrasponding logic. (Type_Invariant): Remove Replace_Typ_Refs and replace its references with calls to Replace_Type_References. * sem_ch3.adb, sem_prag.adb: Remove with and use of exp_ch7. From-SVN: r247152 --- gcc/ada/ChangeLog | 22 + gcc/ada/exp_ch7.adb | 1468 ------------------------------------------ gcc/ada/exp_ch7.ads | 15 - gcc/ada/exp_util.adb | 1425 +++++++++++++++++++++++++++++++++++++++- gcc/ada/exp_util.ads | 28 +- gcc/ada/sem_ch3.adb | 1 - gcc/ada/sem_prag.adb | 1 - gcc/ada/sem_util.adb | 16 +- 8 files changed, 1481 insertions(+), 1495 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 3f938e8364c..917785a5bfa 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,25 @@ +2017-04-25 Hristian Kirtchev + + * sem_util.adb (Check_Part_Of_Reference): + Continue to examine the context if the reference appears within + an expression function. + +2017-04-25 Justin Squirek + + * exp_ch7.adb, exp_ch7.ads Remove Build_Invariant_Procedure_Body + and Build_Invariant_Procedure_Declaration. + * exp_util.ads, exp_util.adb Add Build_Invariant_Procedure_Body + and Build_Invariant_Procedure_Declaration from exp_ch7 + and break-out Is_Untagged_Private_Derivation from + Build_Invariant_Procedure_Body. + (Replace_Type_References): + Append an extra parameter to allow for dispatching replacements + and add the corrasponding logic. + (Type_Invariant): Remove + Replace_Typ_Refs and replace its references with calls to + Replace_Type_References. + * sem_ch3.adb, sem_prag.adb: Remove with and use of exp_ch7. + 2017-04-25 Bob Duff * sem_util.ads, sem_util.adb (Should_Ignore_Pragma): New function diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb index 93573a29ea3..5d981608e63 100644 --- a/gcc/ada/exp_ch7.adb +++ b/gcc/ada/exp_ch7.adb @@ -42,7 +42,6 @@ with Exp_Prag; use Exp_Prag; with Exp_Tss; use Exp_Tss; with Exp_Util; use Exp_Util; with Freeze; use Freeze; -with Ghost; use Ghost; with Lib; use Lib; with Nlists; use Nlists; with Nmake; use Nmake; @@ -55,15 +54,12 @@ with Sinfo; use Sinfo; with Sem; use Sem; with Sem_Aux; use Sem_Aux; with Sem_Ch3; use Sem_Ch3; -with Sem_Ch6; use Sem_Ch6; with Sem_Ch7; use Sem_Ch7; with Sem_Ch8; use Sem_Ch8; -with Sem_Ch13; use Sem_Ch13; with Sem_Res; use Sem_Res; with Sem_Util; use Sem_Util; with Snames; use Snames; with Stand; use Stand; -with Stringt; use Stringt; with Tbuild; use Tbuild; with Ttypes; use Ttypes; with Uintp; use Uintp; @@ -3451,1470 +3447,6 @@ package body Exp_Ch7 is Expand_At_End_Handler (HSS, Empty); end Build_Finalizer_Call; - ------------------------------------ - -- 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 from 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_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_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. - - procedure Add_Type_Invariants - (Priv_Typ : Entity_Id; - Full_Typ : Entity_Id; - CRec_Typ : Entity_Id; - Obj_Id : Entity_Id; - Checks : in out List_Id; - Inherit : Boolean := False; - Priv_Item : Node_Id := Empty); - -- Generate an invariant check for each invariant found in one of the - -- following types (if available): - -- - -- Priv_Typ - the partial view of a type - -- Full_Typ - the full view of a type - -- CRec_Typ - the corresponding record of a protected or a task type - -- - -- Obj_Id denotes the entity of the _object formal parameter of the - -- invariant procedure. All created checks are added to list Checks. - -- Flag Inherit should be set when generating invariant checks for - -- inherited class-wide invariants. Priv_Item denotes the first rep - -- item of the private type. - - function Is_Untagged_Private_Derivation - (Priv_Typ : Entity_Id; - Full_Typ : Entity_Id) return Boolean; - -- Determine whether private type Priv_Typ and its full view Full_Typ - -- represent an untagged derivation from a private parent. - - ------------------------------------ - -- 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: - -- Invariant (_object ()); - - -- 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_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 in _object'Range () loop - -- - -- 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_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 - 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 - Add_Type_Invariants - (Priv_Typ => Empty, - Full_Typ => Node (Iface_Elmt), - CRec_Typ => Empty, - Obj_Id => Obj_Id, - Checks => Checks, - Inherit => True); - - Next_Elmt (Iface_Elmt); - end loop; - end if; - end Add_Interface_Invariants; - - --------------------------- - -- 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); - - Add_Type_Invariants - (Priv_Typ => Priv_Typ, - Full_Typ => Full_Typ, - CRec_Typ => Empty, - Obj_Id => Obj_Id, - Checks => Checks, - Inherit => True); - - Curr_Typ := Par_Typ; - end loop; - end Add_Parent_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: - -- Invariant (T (_object).); - - -- 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; - - ------------------------- - -- Add_Type_Invariants -- - ------------------------- - - procedure Add_Type_Invariants - (Priv_Typ : Entity_Id; - Full_Typ : Entity_Id; - CRec_Typ : Entity_Id; - Obj_Id : Entity_Id; - Checks : in out List_Id; - Inherit : Boolean := False; - Priv_Item : Node_Id := Empty) - is - procedure Add_Invariant (Prag : Node_Id); - -- Create a runtime check to verify the invariant exression of pragma - -- Prag. All generated code is added to list Checks. - - procedure Process_Type (T : Entity_Id; Stop_Item : Node_Id := Empty); - -- Generate invariant checks for type T by inspecting the rep item - -- chain of the type. Stop_Item denotes a rep item which once seen - -- will stop the inspection. - - ------------------- - -- Add_Invariant -- - ------------------- - - procedure Add_Invariant (Prag : Node_Id) is - Rep_Typ : Entity_Id; - -- The replacement type used in the substitution of the current - -- instance of a type with the _object formal parameter. - - procedure Replace_Type_Ref (N : Node_Id); - -- Substitute the occurrence of a type name denoted by N with a - -- reference to the _object formal parameter. - - ---------------------- - -- Replace_Type_Ref -- - ---------------------- - - procedure Replace_Type_Ref (N : Node_Id) is - Nloc : constant Source_Ptr := Sloc (N); - Ref : Node_Id; - - begin - -- Decorate the reference to Ref_Typ even though it may be - -- rewritten further down. This is done for two reasons: - - -- 1) ASIS has all necessary semantic information in the - -- original tree. - - -- 2) Routines which examine properties of the Original_Node - -- have some semantic information. - - if Nkind (N) = N_Identifier then - Set_Entity (N, Rep_Typ); - Set_Etype (N, Rep_Typ); - - elsif Nkind (N) = N_Selected_Component then - Analyze (Prefix (N)); - Set_Entity (Selector_Name (N), Rep_Typ); - Set_Etype (Selector_Name (N), Rep_Typ); - end if; - - -- Perform the following substitution: - - -- Ref_Typ --> _object - - Ref := Make_Identifier (Nloc, Chars (Obj_Id)); - Set_Entity (Ref, Obj_Id); - Set_Etype (Ref, Rep_Typ); - - -- When the pragma denotes a class-wide invariant, perform the - -- following substitution: - - -- Rep_Typ --> Rep_Typ'Class (_object) - - if Class_Present (Prag) then - Ref := - Make_Type_Conversion (Nloc, - Subtype_Mark => - Make_Attribute_Reference (Nloc, - Prefix => - New_Occurrence_Of (Rep_Typ, Nloc), - Attribute_Name => Name_Class), - Expression => Ref); - end if; - - Rewrite (N, Ref); - Set_Comes_From_Source (N, True); - end Replace_Type_Ref; - - procedure Replace_Type_Refs is - new Replace_Type_References_Generic (Replace_Type_Ref); - - -- Local variables - - Asp : constant Node_Id := Corresponding_Aspect (Prag); - Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag); - Ploc : constant Source_Ptr := Sloc (Prag); - - Arg1 : Node_Id; - Arg2 : Node_Id; - Arg3 : Node_Id; - ASIS_Expr : Node_Id; - Assoc : List_Id; - Expr : Node_Id; - Str : String_Id; - - -- Start of processing for Add_Invariant - - begin - -- 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 - - Arg1 := First (Pragma_Argument_Associations (Prag)); - Arg2 := Next (Arg1); - Arg3 := Next (Arg2); - - Arg1 := Get_Pragma_Arg (Arg1); - Arg2 := Get_Pragma_Arg (Arg2); - - -- The pragma applies to the partial view - - if Present (Priv_Typ) and then Entity (Arg1) = Priv_Typ then - Rep_Typ := Priv_Typ; - - -- The pragma applies to the full view - - elsif Present (Full_Typ) and then Entity (Arg1) = Full_Typ then - Rep_Typ := Full_Typ; - - -- Otherwise the pragma applies to a parent type in which case it - -- will be processed at a later stage by Add_Parent_Invariants or - -- Add_Interface_Invariants. - - else - return; - end if; - - -- Nothing to do when the caller requests the processing of all - -- inherited class-wide invariants, but the pragma does not fall - -- in this category. - - if Inherit and then not Class_Present (Prag) then - return; - end if; - - Expr := New_Copy_Tree (Arg2); - - -- Substitute all references to type Rep_Typ with references to - -- the _object formal parameter. - - Replace_Type_Refs (Expr, Rep_Typ); - - -- Additional processing for non-class-wide invariants - - if not Inherit then - - -- Preanalyze the invariant expression to detect errors and at - -- the same time capture the visibility of the proper package - -- part. - - -- Historical note: the old implementation of invariants used - -- node N as the parent, but a package specification as parent - -- of an expression is bizarre. - - Set_Parent (Expr, Parent (Arg2)); - Preanalyze_Assert_Expression (Expr, Any_Boolean); - - -- 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 (Asp) then - Set_Entity (Identifier (Asp), New_Copy_Tree (Expr)); - end if; - - -- Analyze the original invariant expression for ASIS - - if ASIS_Mode then - ASIS_Expr := Empty; - - if Comes_From_Source (Prag) then - ASIS_Expr := Arg2; - elsif Present (Asp) then - ASIS_Expr := Expression (Asp); - end if; - - if Present (ASIS_Expr) then - Replace_Type_Refs (ASIS_Expr, Rep_Typ); - Preanalyze_Assert_Expression (ASIS_Expr, Any_Boolean); - end if; - end if; - - -- A class-wide invariant may be inherited in a separate unit, - -- where the corresponding expression cannot be resolved by - -- visibility, because it refers to a local function. Propagate - -- semantic information to the original representation item, to - -- be used when an invariant procedure for a derived type is - -- constructed. - - -- ??? Unclear how to handle class-wide invariants that are not - -- function calls. - - if Class_Present (Prag) - and then Nkind (Expr) = N_Function_Call - and then Nkind (Arg2) = N_Indexed_Component - then - Rewrite (Arg2, - Make_Function_Call (Ploc, - Name => - New_Occurrence_Of (Entity (Name (Expr)), Ploc), - Parameter_Associations => Expressions (Arg2))); - end if; - end if; - - -- The invariant is ignored, nothing left to do - - if Is_Ignored (Prag) then - null; - - -- Otherwise the invariant is checked. Build a Check pragma to - -- verify the expression at runtime. - - 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 (Arg3) then - Str := Strval (Get_Pragma_Arg (Arg3)); - - -- When inheriting an invariant, modify the message from - -- "failed invariant" to "failed inherited invariant". - - if Inherit 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 (, , ); - - 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 Inherit 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; - - ------------------ - -- Process_Type -- - ------------------ - - procedure Process_Type - (T : Entity_Id; - Stop_Item : Node_Id := Empty) - is - Rep_Item : Node_Id; - - begin - Rep_Item := First_Rep_Item (T); - while Present (Rep_Item) loop - if Nkind (Rep_Item) = N_Pragma - and then Pragma_Name (Rep_Item) = Name_Invariant - then - -- Stop the traversal of the rep item chain once a specific - -- item is encountered. - - if Present (Stop_Item) and then Rep_Item = Stop_Item then - exit; - - -- Otherwise generate an invariant check - - else - Add_Invariant (Rep_Item); - end if; - end if; - - Next_Rep_Item (Rep_Item); - end loop; - end Process_Type; - - -- Start of processing for Add_Type_Invariants - - begin - -- Process the invariants of the partial view - - if Present (Priv_Typ) then - Process_Type (Priv_Typ); - end if; - - -- Process the invariants of the full view - - if Present (Full_Typ) then - Process_Type (Full_Typ, Stop_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, 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; - end if; - - -- Process the components of a corresponding record type - - if Present (CRec_Typ) then - Add_Record_Component_Invariants (CRec_Typ, Obj_Id, Checks); - end if; - end Add_Type_Invariants; - - ------------------------------------ - -- Is_Untagged_Private_Derivation -- - ------------------------------------ - - function Is_Untagged_Private_Derivation - (Priv_Typ : Entity_Id; - Full_Typ : Entity_Id) return Boolean - is - begin - return - Present (Priv_Typ) - and then Is_Untagged_Derivation (Priv_Typ) - and then Is_Private_Type (Etype (Priv_Typ)) - and then Present (Full_Typ) - and then Is_Itype (Full_Typ); - end Is_Untagged_Private_Derivation; - - -- Local variables - - Dummy : Entity_Id; - Mode : Ghost_Mode_Type; - 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; - -- The corresponding record type of Full_Typ - - Full_Proc : Entity_Id; - -- The entity of the "full" invariant procedure - - Full_Typ : Entity_Id; - -- The full view of the working type - - Obj_Id : Entity_Id; - -- The _object formal parameter of the invariant procedure - - Part_Proc : Entity_Id; - -- The entity of the "partial" invariant procedure - - Priv_Typ : Entity_Id; - -- The partial view of the working type - - Work_Typ : Entity_Id; - -- The working type - - -- Start of processing for Build_Invariant_Procedure_Body - - 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 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, Mode); - - -- 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)); - - -- Nothing to do for interface types as their class-wide invariants are - -- inherited by implementing types. - - if Is_Interface (Work_Typ) then - goto Leave; - end if; - - -- Obtain both views of the type - - Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy, CRec_Typ); - - -- 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 of the invariant procedure 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_Type_Invariants - (Priv_Typ => Priv_Typ, - Full_Typ => Empty, - CRec_Typ => Empty, - 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: - - -- 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 - -- - -- end Pack_1; - - -- with Pack_1; - -- package Pack_2 is - -- type Child is new Pack_1.Root with Type_Invariant => ...; - -- - -- 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_Type_Invariants - (Priv_Typ => Priv_Typ, - Full_Typ => Full_Typ, - CRec_Typ => CRec_Typ, - Obj_Id => Obj_Id, - Checks => Stmts, - Priv_Item => Priv_Item); - - -- 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 [Partial_]Invariant (_object : ) is - -- begin - -- - -- end [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 - - Set_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 - -- ASIS or 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 ASIS_Mode or 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; - - <> - Restore_Ghost_Mode (Mode); - 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); - - Mode : Ghost_Mode_Type; - 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_Base : Entity_Id; - -- The base 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 - - Priv_Typ : Entity_Id; - -- The partial view of working type - - 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, Mode); - - -- 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 for interface types as their class-wide invariants are - -- inherited by implementing types. - - if Is_Interface (Work_Typ) then - goto Leave; - - -- Nothing to do if the type already has a "partial" invariant procedure - - elsif 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 - - Set_Ekind (Proc_Id, E_Procedure); - Set_Etype (Proc_Id, Standard_Void_Type); - Set_Scope (Proc_Id, Current_Scope); - - if Partial_Invariant then - Set_Is_Partial_Invariant_Procedure (Proc_Id); - Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id); - else - Set_Is_Invariant_Procedure (Proc_Id); - Set_Invariant_Procedure (Work_Typ, Proc_Id); - end if; - - -- The invariant procedure requires debug info when the invariants are - -- subject to Source Coverage Obligations. - - if Opt.Generate_SCO then - Set_Needs_Debug_Info (Proc_Id); - end if; - - -- Obtain all views of the input type - - Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ); - - -- Associate the invariant procedure with all views - - Propagate_Invariant_Attributes (Priv_Typ, From_Typ => Work_Typ); - Propagate_Invariant_Attributes (Full_Typ, From_Typ => Work_Typ); - Propagate_Invariant_Attributes (Full_Base, From_Typ => Work_Typ); - Propagate_Invariant_Attributes (CRec_Typ, From_Typ => Work_Typ); - - -- The declaration of the invariant procedure is 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 invariant 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 current type instance. - - Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject); - - -- Perform minor decoration in case the declaration is not analyzed - - Set_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); - - -- Generate: - -- procedure [Partial_]Invariant (_object : ); - - 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 ASIS or a generic unit because it is not part of the template. - - if ASIS_Mode or 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 - pragma Assert (Present (Typ_Decl)); - Insert_After_And_Analyze (Typ_Decl, Proc_Decl); - end if; - - <> - Restore_Ghost_Mode (Mode); - end Build_Invariant_Procedure_Declaration; - --------------------- -- Build_Late_Proc -- --------------------- diff --git a/gcc/ada/exp_ch7.ads b/gcc/ada/exp_ch7.ads index 0db3df5f076..b0a8b0b8b8b 100644 --- a/gcc/ada/exp_ch7.ads +++ b/gcc/ada/exp_ch7.ads @@ -118,21 +118,6 @@ package Exp_Ch7 is -- finalization master must be analyzed. Insertion_Node is the insertion -- point before which the master is to be inserted. - procedure Build_Invariant_Procedure_Body - (Typ : Entity_Id; - Partial_Invariant : Boolean := False); - -- Create the body of the procedure which verifies the invariants of type - -- Typ at runtime. Flag Partial_Invariant should be set when Typ denotes a - -- private type, otherwise it is assumed that Typ denotes the full view of - -- a private type. - - procedure Build_Invariant_Procedure_Declaration - (Typ : Entity_Id; - Partial_Invariant : Boolean := False); - -- Create the declaration of the procedure which verifies the invariants of - -- type Typ at runtime. Flag Partial_Invariant should be set when building - -- the invariant procedure for a private type. - procedure Build_Late_Proc (Typ : Entity_Id; Nam : Name_Id); -- Build one controlling procedure when a late body overrides one of the -- controlling operations. diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 638f57417e0..bb36ce99643 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1949,6 +1949,1383 @@ package body Exp_Util is Restore_Ghost_Mode (Mode); 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 from 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_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_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. + + procedure Add_Type_Invariants + (Priv_Typ : Entity_Id; + Full_Typ : Entity_Id; + CRec_Typ : Entity_Id; + Obj_Id : Entity_Id; + Checks : in out List_Id; + Inherit : Boolean := False; + Priv_Item : Node_Id := Empty); + -- Generate an invariant check for each invariant found in one of the + -- following types (if available): + -- + -- Priv_Typ - the partial view of a type + -- Full_Typ - the full view of a type + -- CRec_Typ - the corresponding record of a protected or a task type + -- + -- Obj_Id denotes the entity of the _object formal parameter of the + -- invariant procedure. All created checks are added to list Checks. + -- Flag Inherit should be set when generating invariant checks for + -- inherited class-wide invariants. Priv_Item denotes the first rep + -- item of the private type. + + ------------------------------------ + -- 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: + -- Invariant (_object ()); + + -- 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_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 in _object'Range () loop + -- + -- 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_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 + 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 + Add_Type_Invariants + (Priv_Typ => Empty, + Full_Typ => Node (Iface_Elmt), + CRec_Typ => Empty, + Obj_Id => Obj_Id, + Checks => Checks, + Inherit => True); + + Next_Elmt (Iface_Elmt); + end loop; + end if; + end Add_Interface_Invariants; + + --------------------------- + -- 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); + + Add_Type_Invariants + (Priv_Typ => Priv_Typ, + Full_Typ => Full_Typ, + CRec_Typ => Empty, + Obj_Id => Obj_Id, + Checks => Checks, + Inherit => True); + + Curr_Typ := Par_Typ; + end loop; + end Add_Parent_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: + -- Invariant (T (_object).); + + -- 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; + + ------------------------- + -- Add_Type_Invariants -- + ------------------------- + + procedure Add_Type_Invariants + (Priv_Typ : Entity_Id; + Full_Typ : Entity_Id; + CRec_Typ : Entity_Id; + Obj_Id : Entity_Id; + Checks : in out List_Id; + Inherit : Boolean := False; + Priv_Item : Node_Id := Empty) + is + procedure Add_Invariant (Prag : Node_Id); + -- Create a runtime check to verify the invariant exression of pragma + -- Prag. All generated code is added to list Checks. + + procedure Process_Type (T : Entity_Id; Stop_Item : Node_Id := Empty); + -- Generate invariant checks for type T by inspecting the rep item + -- chain of the type. Stop_Item denotes a rep item which once seen + -- will stop the inspection. + + ------------------- + -- Add_Invariant -- + ------------------- + + procedure Add_Invariant (Prag : Node_Id) is + Asp : constant Node_Id := Corresponding_Aspect (Prag); + Nam : constant Name_Id := Original_Aspect_Pragma_Name (Prag); + Ploc : constant Source_Ptr := Sloc (Prag); + + Arg1 : Node_Id; + Arg2 : Node_Id; + Arg3 : Node_Id; + ASIS_Expr : Node_Id; + Assoc : List_Id; + Expr : Node_Id; + Str : String_Id; + + Rep_Typ : Entity_Id; + -- The replacement type used in the substitution of the current + -- instance of a type with the _object formal parameter. + + begin + -- 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 + + Arg1 := First (Pragma_Argument_Associations (Prag)); + Arg2 := Next (Arg1); + Arg3 := Next (Arg2); + + Arg1 := Get_Pragma_Arg (Arg1); + Arg2 := Get_Pragma_Arg (Arg2); + + -- The pragma applies to the partial view + + if Present (Priv_Typ) and then Entity (Arg1) = Priv_Typ then + Rep_Typ := Priv_Typ; + + -- The pragma applies to the full view + + elsif Present (Full_Typ) and then Entity (Arg1) = Full_Typ then + Rep_Typ := Full_Typ; + + -- Otherwise the pragma applies to a parent type in which case it + -- will be processed at a later stage by Add_Parent_Invariants or + -- Add_Interface_Invariants. + + else + return; + end if; + + -- Nothing to do when the caller requests the processing of all + -- inherited class-wide invariants, but the pragma does not fall + -- in this category. + + if Inherit and then not Class_Present (Prag) then + return; + end if; + + Expr := New_Copy_Tree (Arg2); + + -- Substitute all references to type Rep_Typ with references to + -- the _object formal parameter. Dispatching here must be removed + -- due to AI12-0150-1 !!! + + Replace_Type_References + (Expr, Rep_Typ, Obj_Id, Dispatch => Class_Present (Prag)); + + -- Additional processing for non-class-wide invariants + + if not Inherit then + + -- Preanalyze the invariant expression to detect errors and at + -- the same time capture the visibility of the proper package + -- part. + + -- Historical note: the old implementation of invariants used + -- node N as the parent, but a package specification as parent + -- of an expression is bizarre. + + Set_Parent (Expr, Parent (Arg2)); + Preanalyze_Assert_Expression (Expr, Any_Boolean); + + -- 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 (Asp) then + Set_Entity (Identifier (Asp), New_Copy_Tree (Expr)); + end if; + + -- Analyze the original invariant expression for ASIS + + if ASIS_Mode then + ASIS_Expr := Empty; + + if Comes_From_Source (Prag) then + ASIS_Expr := Arg2; + elsif Present (Asp) then + ASIS_Expr := Expression (Asp); + end if; + + if Present (ASIS_Expr) then + Replace_Type_References + (ASIS_Expr, Rep_Typ, Obj_Id, Class_Present (Prag)); + Preanalyze_Assert_Expression (ASIS_Expr, Any_Boolean); + end if; + end if; + + -- A class-wide invariant may be inherited in a separate unit, + -- where the corresponding expression cannot be resolved by + -- visibility, because it refers to a local function. Propagate + -- semantic information to the original representation item, to + -- be used when an invariant procedure for a derived type is + -- constructed. + + -- ??? Unclear how to handle class-wide invariants that are not + -- function calls. + + if Class_Present (Prag) + and then Nkind (Expr) = N_Function_Call + and then Nkind (Arg2) = N_Indexed_Component + then + Rewrite (Arg2, + Make_Function_Call (Ploc, + Name => + New_Occurrence_Of (Entity (Name (Expr)), Ploc), + Parameter_Associations => Expressions (Arg2))); + end if; + end if; + + -- The invariant is ignored, nothing left to do + + if Is_Ignored (Prag) then + null; + + -- Otherwise the invariant is checked. Build a Check pragma to + -- verify the expression at runtime. + + 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 (Arg3) then + Str := Strval (Get_Pragma_Arg (Arg3)); + + -- When inheriting an invariant, modify the message from + -- "failed invariant" to "failed inherited invariant". + + if Inherit 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 (, , ); + + 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 Inherit 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; + + ------------------ + -- Process_Type -- + ------------------ + + procedure Process_Type + (T : Entity_Id; + Stop_Item : Node_Id := Empty) + is + Rep_Item : Node_Id; + + begin + Rep_Item := First_Rep_Item (T); + while Present (Rep_Item) loop + if Nkind (Rep_Item) = N_Pragma + and then Pragma_Name (Rep_Item) = Name_Invariant + then + -- Stop the traversal of the rep item chain once a specific + -- item is encountered. + + if Present (Stop_Item) and then Rep_Item = Stop_Item then + exit; + + -- Otherwise generate an invariant check + + else + Add_Invariant (Rep_Item); + end if; + end if; + + Next_Rep_Item (Rep_Item); + end loop; + end Process_Type; + + -- Start of processing for Add_Type_Invariants + + begin + -- Process the invariants of the partial view + + if Present (Priv_Typ) then + Process_Type (Priv_Typ); + end if; + + -- Process the invariants of the full view + + if Present (Full_Typ) then + Process_Type (Full_Typ, Stop_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, 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; + end if; + + -- Process the components of a corresponding record type + + if Present (CRec_Typ) then + Add_Record_Component_Invariants (CRec_Typ, Obj_Id, Checks); + end if; + end Add_Type_Invariants; + + -- Local variables + + Dummy : Entity_Id; + Mode : Ghost_Mode_Type; + 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; + -- The corresponding record type of Full_Typ + + Full_Proc : Entity_Id; + -- The entity of the "full" invariant procedure + + Full_Typ : Entity_Id; + -- The full view of the working type + + Obj_Id : Entity_Id; + -- The _object formal parameter of the invariant procedure + + Part_Proc : Entity_Id; + -- The entity of the "partial" invariant procedure + + Priv_Typ : Entity_Id; + -- The partial view of the working type + + Work_Typ : Entity_Id; + -- The working type + + -- Start of processing for Build_Invariant_Procedure_Body + + 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 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, Mode); + + -- 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)); + + -- Nothing to do for interface types as their class-wide invariants are + -- inherited by implementing types. + + if Is_Interface (Work_Typ) then + goto Leave; + end if; + + -- Obtain both views of the type + + Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy, CRec_Typ); + + -- 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 of the invariant procedure 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_Type_Invariants + (Priv_Typ => Priv_Typ, + Full_Typ => Empty, + CRec_Typ => Empty, + 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: + + -- 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 + -- + -- end Pack_1; + + -- with Pack_1; + -- package Pack_2 is + -- type Child is new Pack_1.Root with Type_Invariant => ...; + -- + -- 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_Type_Invariants + (Priv_Typ => Priv_Typ, + Full_Typ => Full_Typ, + CRec_Typ => CRec_Typ, + Obj_Id => Obj_Id, + Checks => Stmts, + Priv_Item => Priv_Item); + + -- 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 [Partial_]Invariant (_object : ) is + -- begin + -- + -- end [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 + + Set_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 + -- ASIS or 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 ASIS_Mode or 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; + + <> + Restore_Ghost_Mode (Mode); + 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); + + Mode : Ghost_Mode_Type; + 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_Base : Entity_Id; + -- The base 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 + + Priv_Typ : Entity_Id; + -- The partial view of working type + + 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, Mode); + + -- 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 for interface types as their class-wide invariants are + -- inherited by implementing types. + + if Is_Interface (Work_Typ) then + goto Leave; + + -- Nothing to do if the type already has a "partial" invariant procedure + + elsif 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 + + Set_Ekind (Proc_Id, E_Procedure); + Set_Etype (Proc_Id, Standard_Void_Type); + Set_Scope (Proc_Id, Current_Scope); + + if Partial_Invariant then + Set_Is_Partial_Invariant_Procedure (Proc_Id); + Set_Partial_Invariant_Procedure (Work_Typ, Proc_Id); + else + Set_Is_Invariant_Procedure (Proc_Id); + Set_Invariant_Procedure (Work_Typ, Proc_Id); + end if; + + -- The invariant procedure requires debug info when the invariants are + -- subject to Source Coverage Obligations. + + if Opt.Generate_SCO then + Set_Needs_Debug_Info (Proc_Id); + end if; + + -- Obtain all views of the input type + + Get_Views (Work_Typ, Priv_Typ, Full_Typ, Full_Base, CRec_Typ); + + -- Associate the invariant procedure with all views + + Propagate_Invariant_Attributes (Priv_Typ, From_Typ => Work_Typ); + Propagate_Invariant_Attributes (Full_Typ, From_Typ => Work_Typ); + Propagate_Invariant_Attributes (Full_Base, From_Typ => Work_Typ); + Propagate_Invariant_Attributes (CRec_Typ, From_Typ => Work_Typ); + + -- The declaration of the invariant procedure is 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 invariant 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 current type instance. + + Obj_Id := Make_Defining_Identifier (Loc, Chars => Name_uObject); + + -- Perform minor decoration in case the declaration is not analyzed + + Set_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); + + -- Generate: + -- procedure [Partial_]Invariant (_object : ); + + 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 ASIS or a generic unit because it is not part of the template. + + if ASIS_Mode or 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 + pragma Assert (Present (Typ_Decl)); + Insert_After_And_Analyze (Typ_Decl, Proc_Decl); + end if; + + <> + Restore_Ghost_Mode (Mode); + end Build_Invariant_Procedure_Declaration; + -------------------------- -- Build_Procedure_Form -- -------------------------- @@ -7124,6 +8501,23 @@ package body Exp_Util is and then Etype (Full_View (T)) /= T); end Is_Untagged_Derivation; + ------------------------------------ + -- Is_Untagged_Private_Derivation -- + ------------------------------------ + + function Is_Untagged_Private_Derivation + (Priv_Typ : Entity_Id; + Full_Typ : Entity_Id) return Boolean + is + begin + return + Present (Priv_Typ) + and then Is_Untagged_Derivation (Priv_Typ) + and then Is_Private_Type (Etype (Priv_Typ)) + and then Present (Full_Typ) + and then Is_Itype (Full_Typ); + end Is_Untagged_Private_Derivation; + --------------------------- -- Is_Volatile_Reference -- --------------------------- @@ -10181,9 +11575,10 @@ package body Exp_Util is ----------------------------- procedure Replace_Type_References - (Expr : Node_Id; - Typ : Entity_Id; - Obj_Id : Entity_Id) + (Expr : Node_Id; + Typ : Entity_Id; + Obj_Id : Entity_Id; + Dispatch : Boolean := False) is procedure Replace_Type_Ref (N : Node_Id); -- Substitute a single reference of the current instance of type Typ @@ -10194,7 +11589,8 @@ package body Exp_Util is ---------------------- procedure Replace_Type_Ref (N : Node_Id) is - Ref : Node_Id; + Nloc : constant Source_Ptr := Sloc (N); + Ref : Node_Id; begin -- Decorate the reference to Typ even though it may be rewritten @@ -10224,8 +11620,27 @@ package body Exp_Util is Set_Entity (Ref, Obj_Id); Set_Etype (Ref, Typ); - Rewrite (N, Ref); + -- When the pragma denotes a class-wide and the Dispatch flag is set + -- perform the following substitution. Note: dispatching in this + -- fashion is illegal Ada according to AI12-0150-1 because class-wide + -- aspects like type invariants and default initial conditions be + -- evaluated statically. Currently it is used only for class-wide + -- type invariants, but this will be fixed. + + -- Rep_Typ --> Rep_Typ'Class (_object) + if Dispatch then + Ref := + Make_Type_Conversion (Nloc, + Subtype_Mark => + Make_Attribute_Reference (Nloc, + Prefix => + New_Occurrence_Of (Typ, Nloc), + Attribute_Name => Name_Class), + Expression => Ref); + end if; + + Rewrite (N, Ref); Set_Comes_From_Source (N, True); end Replace_Type_Ref; diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads index 8e0021748d3..0a409f3d22c 100644 --- a/gcc/ada/exp_util.ads +++ b/gcc/ada/exp_util.ads @@ -290,6 +290,21 @@ package Exp_Util is -- Create the declaration of the procedure which verifies the assertion -- expression of pragma Default_Initial_Condition at run time. + procedure Build_Invariant_Procedure_Body + (Typ : Entity_Id; + Partial_Invariant : Boolean := False); + -- Create the body of the procedure which verifies the invariants of type + -- Typ at runtime. Flag Partial_Invariant should be set when Typ denotes a + -- private type, otherwise it is assumed that Typ denotes the full view of + -- a private type. + + procedure Build_Invariant_Procedure_Declaration + (Typ : Entity_Id; + Partial_Invariant : Boolean := False); + -- Create the declaration of the procedure which verifies the invariants of + -- type Typ at runtime. Flag Partial_Invariant should be set when building + -- the invariant procedure for a private type. + procedure Build_Procedure_Form (N : Node_Id); -- Create a procedure declaration which emulates the behavior of a function -- that returns an array type, for C-compatible generation. @@ -805,6 +820,12 @@ package Exp_Util is -- Returns true if type T is not tagged and is a derived type, -- or is a private type whose completion is such a type. + function Is_Untagged_Private_Derivation + (Priv_Typ : Entity_Id; + Full_Typ : Entity_Id) return Boolean; + -- Determine whether private type Priv_Typ and its full view Full_Typ + -- represent an untagged derivation from a private parent. + function Is_Volatile_Reference (N : Node_Id) return Boolean; -- Checks if the node N represents a volatile reference, which can be -- either a direct reference to a variable treated as volatile, or an @@ -1037,9 +1058,10 @@ package Exp_Util is -- the internally-generated inherited primitive of Deriv_Typ. procedure Replace_Type_References - (Expr : Node_Id; - Typ : Entity_Id; - Obj_Id : Entity_Id); + (Expr : Node_Id; + Typ : Entity_Id; + Obj_Id : Entity_Id; + Dispatch : Boolean := False); -- Substitute all references of the current instance of type Typ with -- references to formal parameter Obj_Id within expression Expr. diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 0c4d2301a3c..cbae00f158f 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -33,7 +33,6 @@ with Einfo; use Einfo; with Errout; use Errout; with Eval_Fat; use Eval_Fat; with Exp_Ch3; use Exp_Ch3; -with Exp_Ch7; use Exp_Ch7; with Exp_Ch9; use Exp_Ch9; with Exp_Disp; use Exp_Disp; with Exp_Dist; use Exp_Dist; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index c16973763dd..2638b37d5cc 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -39,7 +39,6 @@ with Debug; use Debug; with Einfo; use Einfo; with Elists; use Elists; with Errout; use Errout; -with Exp_Ch7; use Exp_Ch7; with Exp_Dist; use Exp_Dist; with Exp_Util; use Exp_Util; with Freeze; use Freeze; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 700203598ab..ed883731b30 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -1823,8 +1823,20 @@ package body Sem_Util is N_Subprogram_Declaration) and then not Comes_From_Source (Par) then - OK_Use := True; - exit; + -- Continue to examine the context if the reference appears in a + -- subprogram body which was previously an expression function. + + if Nkind (Par) = N_Subprogram_Body + and then Was_Expression_Function (Par) + then + null; + + -- Otherwise the reference is legal + + else + OK_Use := True; + exit; + end if; -- The reference has been relocated to an inlined body for GNATprove. -- Assume that the reference is legal as the real check was already -- 2.30.2