From f7937111e8c8cfaf5ea79d97c65d6b6dc29b261f Mon Sep 17 00:00:00 2001 From: Gary Dismukes Date: Mon, 2 Nov 2020 01:21:09 -0500 Subject: [PATCH] [Ada] Implement inheritance for Default_Initial_Condition and address other gaps gcc/ada/ * einfo.ads (Is_Partial_DIC_Procedure): New function. (Partial_DIC_Procedure): New procedure. * einfo.adb (Is_Partial_DIC_Procedure): New function to return whether a subprogram is a partial Default_Initial_Condition procedure by checking the name (to avoid adding a new field). (DIC_Procedure): Add a test that excludes partial DIC procedures from being returned. (Partial_DIC_Procedure): New procedure to return the partial DIC procedure of a type, if it has one (otherwise returns Empty). (Set_DIC_Procedure): Remove check for duplicate DIC procedures. * exp_aggr.adb (Gen_Assign): Generate a call to the type's DIC procedure in the case where an array component is default initialized (due to an association with a box). (Build_Record_Aggr_Code): For an extension aggregate, generate a call to the ancestor type's DIC procedure (if any) when the ancestor part is a subtype mark. For a record component association that was specified with a box (tested for by checking the new flag Was_Default_Init_Box_Association), generate a call to the component type's DIC procedure (if it has one). * exp_ch4.adb (Expand_N_Allocator): When the allocated object is default initialized and the designated type has a DIC aspect, generate a call to the DIC procedure. * exp_util.ads (Build_DIC_Call): Change the formal Obj_Id to name Obj_Name, and change its type from Entity_Id to Node_Id (and update comment). (Build_DIC_Procedure_Body): Add formal Partial_DIC, remove formal For_Freeze, and update comment accordingly. (Build_DIC_Procedure_Declaration): Add formal Partial_DIC and update comment. * exp_util.adb (Build_DIC_Call): Revised to use its Obj_Name (formerly Obj_Id) formal directly rather than calling New_Occurrence_Of on it, to allow arbitrary names to be passed rather than being limited to Entity_Ids. (Build_DIC_Procedure_Body): Call Add_Parent_DICs to generate checks for DICs associated with any parent types, implementing the required "additive" semantics for DICs. When building a DIC procedure body for a partial view (when Partial_DIC is True), call Add_Own_DIC when the type has its own DIC. In the case of "full" DIC procedures, a call is generated to any partial DIC procedure of the type (unless the procedure has a null body), along with checks for any DICs inherited by the full view. (Build_DIC_Procedure_Declaration): Add handling for partial DIC procedures. For the suffix of a regular DIC procedure's name, use "DIC" (instead of "Default_Initial_Condition"), and for the suffix of a partial DIC procedure's name, use "Partial_DIC". (Add_DIC_Check): Add the DIC pragma to the list of seen pragmas (Pragmas_Seen). (Add_Inherited_Tagged_DIC): Remove the formals Par_Typ, Deriv_Typ, and Obj_Id, and add formal Expr, which denotes DIC's expression. Remove the call to Replace_References (which is now done in Add_Inherited_DICs). (Add_Inherited_DICs): New procedure to locate a DIC pragma associated with a parent type, replace its references appropriately (such as any current instance references), and add a check for the DIC. (Add_Own_DIC): Add an Obj_Id formal to allow caller to pass the _init formal of the generated DIC procedure. (Add_Parent_DICs): New procedure to traverse a type's parents, looking for DICs associated with those and calling Add_Inherited_DICs to apply the appropriate DIC checks. (Is_Verifiable_DIC_Pragma): Treat pragmas that have an Empty first argument the same as a pragma without any arguments (returning False for that case). * exp_ch3.adb (Init_One_Dimension): Generate calls to the component's DIC procedure when needed. (Possible_DIC_Call): New function nested in Init_One_Dimension to build a call to the array component type's DIC-checking function when appropriate. (Build_Array_Init_Proc): The presence of a DIC on the component type is an additional condition for generating an init proc for an array type. (Build_Init_Statements): When the record component's type has a DIC, and the component declaration does not have an initialization expression, generate a call to the component type's DIC procedure. (Expand_N_Object_Declaration): Modify the call to Build_DIC_Call to pass a new occurrence of the object's defining id rather than the id itself. (Freeze_Type): Only build a type's DIC procedure (if it has one) for types that are not interfaces. * exp_spark.adb (Expand_SPARK_N_Freeze_Type): Remove From_Freeze actual and add a ??? comment. (Expand_SPARK_N_Object_Declaration): Modify call to Build_DIC_Call to pass a new occurrence of the object id rather than the object id itself. * sem_aggr.adb (Resolve_Record_Aggregate): Declare local flag Is_Box_Init_By_Default and set it in cases where the component association has a box and the component is being initialized by default (as opposed to initialized by an initialization expression associated with the component's declaration). (Add_Association): If the association has a box for a component initialized by default, the flag Was_Default_Init_Box_Association is set on the new component association (for later testing during expansion). (Get_Value): Reset Is_Box_Init_By_Default to False. * sem_ch3.adb (Build_Assertion_Bodies_For_Type): Rearrange code to build DIC procedure bodies for a (noninterface) type that Has_Own_DIC (for partial type views) or Has_DIC (for full type views) as appropriate. * sem_ch13.adb (Analyze_Aspect_Specifications, Aspect_Default_Initial_Condition): Add an extra argument to the DIC pragma to denote the type associated with the pragma (for use in Build_DIC_Procedure_Body). * sem_prag.adb (Analyze_Pragma): Allow two arguments for pragma Default_Initial_Condition. If not already present, add an extra argument denoting the type that the pragma is associated with. * sem_util.adb (Propagate_DIC_Attributes): Retrieve any partial DIC procedure associated with the type and add it to the type's list of subprograms (Subprograms_For_Type). * sinfo.ads (Was_Default_Init_Box_Association): New flag on N_Component_Association nodes. Add subprograms to get and set flag, as well as updating the documentation. * sinfo.adb (Was_Default_Init_Box_Association): New function to retrieve the corresponding flag (Flag14). (Set_Was_Default_Init_Box_Association): New procedure to set the corresponding flag (Flag14). --- gcc/ada/einfo.adb | 83 +++++- gcc/ada/einfo.ads | 19 ++ gcc/ada/exp_aggr.adb | 43 +++ gcc/ada/exp_ch3.adb | 142 ++++++++-- gcc/ada/exp_ch4.adb | 18 ++ gcc/ada/exp_spark.adb | 7 +- gcc/ada/exp_util.adb | 640 ++++++++++++++++++++++++++++++------------ gcc/ada/exp_util.ads | 30 +- gcc/ada/sem_aggr.adb | 29 +- gcc/ada/sem_ch13.adb | 8 +- gcc/ada/sem_ch3.adb | 82 +++--- gcc/ada/sem_prag.adb | 23 +- gcc/ada/sem_util.adb | 10 +- gcc/ada/sinfo.adb | 16 ++ gcc/ada/sinfo.ads | 18 +- 15 files changed, 900 insertions(+), 268 deletions(-) diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 9e5b0eedfec..8949703f8d7 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -2543,6 +2543,29 @@ package body Einfo is return Flag215 (Base_Type (Id)); end Is_Param_Block_Component_Type; + function Is_Partial_DIC_Procedure (Id : E) return B is + Partial_DIC_Suffix : constant String := "Partial_DIC"; + DIC_Nam : constant String := Get_Name_String (Chars (Id)); + + begin + pragma Assert (Ekind (Id) in E_Function | E_Procedure); + + -- Instead of adding a new Entity_Id flag (which are in short supply), + -- we test the form of the subprogram name. When the node field and flag + -- situation is eased, this should be replaced with a flag. ??? + + if DIC_Nam'Length > Partial_DIC_Suffix'Length + and then + DIC_Nam + (DIC_Nam'Last - Partial_DIC_Suffix'Length + 1 .. DIC_Nam'Last) = + Partial_DIC_Suffix + then + return True; + else + return False; + end if; + end Is_Partial_DIC_Procedure; + function Is_Partial_Invariant_Procedure (Id : E) return B is begin pragma Assert (Ekind (Id) in E_Function | E_Procedure); @@ -7401,7 +7424,13 @@ package body Einfo is while Present (Subp_Elmt) loop Subp_Id := Node (Subp_Elmt); - if Is_DIC_Procedure (Subp_Id) then + -- Currently the flag Is_DIC_Procedure is set for both normal DIC + -- check procedures as well as for partial DIC check procedures, + -- and we don't have a flag for the partial procedures. + + if Is_DIC_Procedure (Subp_Id) + and then not Is_Partial_DIC_Procedure (Subp_Id) + then return Subp_Id; end if; @@ -8792,6 +8821,36 @@ package body Einfo is return Ekind (Id); end Parameter_Mode; + --------------------------- + -- Partial_DIC_Procedure -- + --------------------------- + + function Partial_DIC_Procedure (Id : E) return E is + Subp_Elmt : Elmt_Id; + Subp_Id : Entity_Id; + Subps : Elist_Id; + + begin + pragma Assert (Is_Type (Id)); + + Subps := Subprograms_For_Type (Base_Type (Id)); + + if Present (Subps) then + Subp_Elmt := First_Elmt (Subps); + while Present (Subp_Elmt) loop + Subp_Id := Node (Subp_Elmt); + + if Is_Partial_DIC_Procedure (Subp_Id) then + return Subp_Id; + end if; + + Next_Elmt (Subp_Elmt); + end loop; + end if; + + return Empty; + end Partial_DIC_Procedure; + --------------------------------- -- Partial_Invariant_Procedure -- --------------------------------- @@ -9271,8 +9330,6 @@ package body Einfo is procedure Set_DIC_Procedure (Id : E; V : E) is Base_Typ : Entity_Id; - Subp_Elmt : Elmt_Id; - Subp_Id : Entity_Id; Subps : Elist_Id; begin @@ -9286,21 +9343,17 @@ package body Einfo is Set_Subprograms_For_Type (Base_Typ, Subps); end if; - Subp_Elmt := First_Elmt (Subps); Prepend_Elmt (V, Subps); + end Set_DIC_Procedure; - -- Check for a duplicate default initial condition procedure - - while Present (Subp_Elmt) loop - Subp_Id := Node (Subp_Elmt); - - if Is_DIC_Procedure (Subp_Id) then - raise Program_Error; - end if; + ------------------------------------- + -- Set_Partial_Invariant_Procedure -- + ------------------------------------- - Next_Elmt (Subp_Elmt); - end loop; - end Set_DIC_Procedure; + procedure Set_Partial_DIC_Procedure (Id : E; V : E) is + begin + Set_DIC_Procedure (Id, V); + end Set_Partial_DIC_Procedure; ----------------------------- -- Set_Invariant_Procedure -- diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index a4b4f0fcf76..360ce7ce855 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -3932,6 +3932,20 @@ package Einfo is -- of a single protected/task type, the references are examined as they -- must appear only within the type defintion and the corresponding body. +-- Partial_DIC_Procedure (synthesized) +-- Defined in type entities. Set for a private type and its full view +-- when the type is subject to pragma Default_Initial_Condition (DIC), or +-- when the type inherits a DIC pragma from a parent type. Points to the +-- entity of a procedure that takes a single argument of the given type +-- and verifies the assertion expression of the DIC pragma at run time. +-- When present, the Partial_DIC_Procedure of a type only checks DICs +-- associated with the partial (private) view of the type, and is invoked +-- by the full DIC_Procedure (which may check additional DICs associated +-- with the full view). + +-- Note: the reason this is marked as a synthesized attribute is that the +-- way this is stored is as an element of the Subprograms_For_Type field. + -- Partial_Invariant_Procedure (synthesized) -- Defined in types and subtypes. Set for private types when one or more -- [class-wide] type invariants apply to them. Points to the entity for a @@ -5821,6 +5835,7 @@ package Einfo is -- Is_Full_Access (synth) -- Is_Controlled (synth) -- Object_Size_Clause (synth) + -- Partial_DIC_Procedure (synth) -- Partial_Invariant_Procedure (synth) -- Predicate_Function (synth) -- Predicate_Function_M (synth) @@ -6586,6 +6601,7 @@ package Einfo is -- Is_Invariant_Procedure (Flag257) (non-generic case only) -- Is_Machine_Code_Subprogram (Flag137) (non-generic case only) -- Is_Null_Init_Proc (Flag178) + -- Is_Partial_DIC_Procedure (synth) (non-generic case only) -- Is_Partial_Invariant_Procedure (Flag292) (non-generic case only) -- Is_Predicate_Function (Flag255) (non-generic case only) -- Is_Predicate_Function_M (Flag256) (non-generic case only) @@ -7405,6 +7421,7 @@ package Einfo is function Is_Packed_Array_Impl_Type (Id : E) return B; function Is_Potentially_Use_Visible (Id : E) return B; function Is_Param_Block_Component_Type (Id : E) return B; + function Is_Partial_DIC_Procedure (Id : E) return B; function Is_Partial_Invariant_Procedure (Id : E) return B; function Is_Predicate_Function (Id : E) return B; function Is_Predicate_Function_M (Id : E) return B; @@ -8309,12 +8326,14 @@ package Einfo is --------------------------------------------------- function DIC_Procedure (Id : E) return E; + function Partial_DIC_Procedure (Id : E) return E; function Invariant_Procedure (Id : E) return E; function Partial_Invariant_Procedure (Id : E) return E; function Predicate_Function (Id : E) return E; function Predicate_Function_M (Id : E) return E; procedure Set_DIC_Procedure (Id : E; V : E); + procedure Set_Partial_DIC_Procedure (Id : E; V : E); procedure Set_Invariant_Procedure (Id : E; V : E); procedure Set_Partial_Invariant_Procedure (Id : E; V : E); procedure Set_Predicate_Function (Id : E; V : E); diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb index 986ccc992a9..30f6dd95e7c 100644 --- a/gcc/ada/exp_aggr.adb +++ b/gcc/ada/exp_aggr.adb @@ -1865,6 +1865,21 @@ package body Exp_Aggr is Typ => Ctype, With_Default_Init => True)); + -- If Default_Initial_Condition applies to the component type, + -- add a DIC check after the component is default-initialized. + -- It will be analyzed and resolved before the code for + -- initialization of other components. + + -- Theoretically this might also be needed for cases where + -- the component type doesn't have an init proc (such as for + -- Default_Value cases), but those should be uncommon, and for + -- now we only support the init proc case. ??? + + if Has_DIC (Ctype) and then Present (DIC_Procedure (Ctype)) then + Append_To (Stmts, + Build_DIC_Call (Loc, New_Copy_Tree (Indexed_Comp), Ctype)); + end if; + -- If the component type has invariants, add an invariant -- check after the component is default-initialized. It will -- be analyzed and resolved before the code for initialization @@ -3504,6 +3519,18 @@ package body Exp_Aggr is then Check_Ancestor_Discriminants (Entity (Ancestor)); end if; + + -- If ancestor type has Default_Initialization_Condition, + -- add a DIC check after the ancestor object is initialized + -- by default. + + if Has_DIC (Entity (Ancestor)) + and then Present (DIC_Procedure (Entity (Ancestor))) + then + Append_To (L, + Build_DIC_Call + (Loc, New_Copy_Tree (Ref), Entity (Ancestor))); + end if; end if; -- Handle calls to C++ constructors @@ -4109,6 +4136,22 @@ package body Exp_Aggr is end; end if; + -- If the component association was specified with a box and the + -- component type has a Default_Initial_Condition, then generate + -- a call to the DIC procedure. + + if Has_DIC (Etype (Selector)) + and then Was_Default_Init_Box_Association (Comp) + and then Present (DIC_Procedure (Etype (Selector))) + then + Append_To (L, + Build_DIC_Call (Loc, + Make_Selected_Component (Loc, + Prefix => New_Copy_Tree (Target), + Selector_Name => New_Occurrence_Of (Selector, Loc)), + Etype (Selector))); + end if; + Next (Comp); end loop; diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb index bd2de67fa8a..3fa0641d365 100644 --- a/gcc/ada/exp_ch3.adb +++ b/gcc/ada/exp_ch3.adb @@ -671,24 +671,85 @@ package body Exp_Ch3 is ------------------------ function Init_One_Dimension (N : Int) return List_Id is - Index : Entity_Id; + Index : Entity_Id; + DIC_Call : Node_Id; + Result_List : List_Id; + + function Possible_DIC_Call return Node_Id; + -- If the component type has Default_Initial_Conditions and a DIC + -- procedure that is not an empty body, then builds a call to the + -- DIC procedure and returns it. + + ----------------------- + -- Possible_DIC_Call -- + ----------------------- + + function Possible_DIC_Call return Node_Id is + begin + -- When the component's type has a Default_Initial_Condition, then + -- create a call for the DIC check. + + if Has_DIC (Comp_Type) + -- In GNATprove mode, the component DICs are checked by other + -- means. They should not be added to the record type DIC + -- procedure, so that the procedure can be used to check the + -- record type invariants or DICs if any. + + and then not GNATprove_Mode + + and then Present (DIC_Procedure (Comp_Type)) + + and then not Has_Null_Body (DIC_Procedure (Comp_Type)) + then + return + Build_DIC_Call (Loc, + Make_Indexed_Component (Loc, + Prefix => Make_Identifier (Loc, Name_uInit), + Expressions => Index_List), + Comp_Type); + else + return Empty; + end if; + end Possible_DIC_Call; + + -- Start of processing for Init_One_Dimension begin -- If the component does not need initializing, then there is nothing -- to do here, so we return a null body. This occurs when generating -- the dummy Init_Proc needed for Initialize_Scalars processing. + -- An exception is if component type has a Default_Initial_Condition, + -- in which case we generate a call to the type's DIC procedure. if not Has_Non_Null_Base_Init_Proc (Comp_Type) and then not Comp_Simple_Init and then not Has_Task (Comp_Type) and then not Has_Default_Aspect (A_Type) + and then (not Has_DIC (Comp_Type) + or else N > Number_Dimensions (A_Type)) then - return New_List (Make_Null_Statement (Loc)); + DIC_Call := Possible_DIC_Call; + + if Present (DIC_Call) then + return New_List (DIC_Call); + else + return New_List (Make_Null_Statement (Loc)); + end if; -- If all dimensions dealt with, we simply initialize the component + -- and append a call to component type's DIC procedure when needed. elsif N > Number_Dimensions (A_Type) then - return Init_Component; + DIC_Call := Possible_DIC_Call; + + if Present (DIC_Call) then + Result_List := Init_Component; + Append (DIC_Call, Result_List); + return Result_List; + + else + return Init_Component; + end if; -- Here we generate the required loop @@ -753,6 +814,7 @@ package body Exp_Ch3 is -- 3. Tasks are present -- 4. The type is marked as a public entity -- 5. The array type has a Default_Component_Value aspect + -- 6. The array component type has a Default_Initialization_Condition -- The reason for the public entity test is to deal properly with the -- Initialize_Scalars pragma. This pragma can be set in the client and @@ -771,7 +833,8 @@ package body Exp_Ch3 is Has_Default_Init := Has_Non_Null_Base_Init_Proc (Comp_Type) or else Comp_Simple_Init or else Has_Task (Comp_Type) - or else Has_Default_Aspect (A_Type); + or else Has_Default_Aspect (A_Type) + or else Has_DIC (Comp_Type); if Has_Default_Init or else (not Restriction_Active (No_Initialize_Scalars) @@ -3438,6 +3501,38 @@ package body Exp_Ch3 is Actions := No_List; end if; + -- When the component's type has a Default_Initial_Condition, + -- and the component is default initialized, then check the + -- DIC here. + + if Has_DIC (Typ) + and then not Present (Expression (Decl)) + and then Present (DIC_Procedure (Typ)) + and then not Has_Null_Body (DIC_Procedure (Typ)) + + -- The DICs of ancestors are checked as part of the type's + -- DIC procedure. + + and then Chars (Id) /= Name_uParent + + -- In GNATprove mode, the component DICs are checked by other + -- means. They should not be added to the record type DIC + -- procedure, so that the procedure can be used to check the + -- record type invariants or DICs if any. + + and then not GNATprove_Mode + then + Append_New_To (Actions, + Build_DIC_Call + (Comp_Loc, + Make_Selected_Component (Comp_Loc, + Prefix => + Make_Identifier (Comp_Loc, Name_uInit), + Selector_Name => + New_Occurrence_Of (Id, Comp_Loc)), + Typ)); + end if; + if Present (Checks) then if Chars (Id) = Name_uParent then Append_List_To (Parent_Stmts, Checks); @@ -7552,12 +7647,14 @@ package body Exp_Ch3 is if Comes_From_Source (Def_Id) and then Has_DIC (Typ) and then Present (DIC_Procedure (Typ)) + and then not Has_Null_Body (DIC_Procedure (Typ)) and then not Has_Init_Expression (N) and then not Is_Imported (Def_Id) then declare - DIC_Call : constant Node_Id := Build_DIC_Call (Loc, Def_Id, Typ); - + DIC_Call : constant Node_Id := + Build_DIC_Call + (Loc, New_Occurrence_Of (Def_Id, Loc), Typ); begin if Present (Next_N) then Insert_Before_And_Analyze (Next_N, DIC_Call); @@ -8331,13 +8428,6 @@ package body Exp_Ch3 is Process_Pending_Access_Types (Def_Id); Freeze_Stream_Operations (N, Def_Id); - -- Generate the [spec and] body of the procedure tasked with the runtime - -- verification of pragma Default_Initial_Condition's expression. - - if Has_DIC (Def_Id) then - Build_DIC_Procedure_Body (Def_Id, For_Freeze => True); - end if; - -- Generate the [spec and] body of the invariant procedure tasked with -- the runtime verification of all invariants that pertain to the type. -- This includes invariants on the partial and full view, inherited @@ -8363,14 +8453,24 @@ package body Exp_Ch3 is -- subprograms, which may involve local declarations of local -- subtypes to which these checks do not apply. - elsif Has_Invariants (Def_Id) then - if not Predicate_Check_In_Scope (Def_Id) - or else (Ekind (Current_Scope) = E_Function - and then Is_Predicate_Function (Current_Scope)) - then - null; - else - Build_Invariant_Procedure_Body (Def_Id); + else + if Has_Invariants (Def_Id) then + if not Predicate_Check_In_Scope (Def_Id) + or else (Ekind (Current_Scope) = E_Function + and then Is_Predicate_Function (Current_Scope)) + then + null; + else + Build_Invariant_Procedure_Body (Def_Id); + end if; + end if; + + -- Generate the [spec and] body of the procedure tasked with the + -- run-time verification of pragma Default_Initial_Condition's + -- expression. + + if Has_DIC (Def_Id) then + Build_DIC_Procedure_Body (Def_Id); end if; end if; diff --git a/gcc/ada/exp_ch4.adb b/gcc/ada/exp_ch4.adb index d65dac9e543..ecaeeb27ff6 100644 --- a/gcc/ada/exp_ch4.adb +++ b/gcc/ada/exp_ch4.adb @@ -5388,6 +5388,24 @@ package body Exp_Ch4 is Rewrite (N, New_Occurrence_Of (Temp, Loc)); Analyze_And_Resolve (N, PtrT); + + -- When designated type has Default_Initial_Condition aspects, + -- make a call to the type's DIC procedure to perform the + -- checks. Theoretically this might also be needed for cases + -- where the type doesn't have an init proc, but those should + -- be very uncommon, and for now we only support the init proc + -- case. ??? + + if Has_DIC (Dtyp) + and then Present (DIC_Procedure (Dtyp)) + and then not Has_Null_Body (DIC_Procedure (Dtyp)) + then + Insert_Action (N, + Build_DIC_Call (Loc, + Make_Explicit_Dereference (Loc, + Prefix => New_Occurrence_Of (Temp, Loc)), + Dtyp)); + end if; end if; end if; end; diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index 7909944f61b..d65136be09d 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -357,7 +357,10 @@ package body Exp_SPARK is -- procedure for it as done during regular expansion for compilation. if Has_DIC (E) and then Is_Tagged_Type (E) then - Build_DIC_Procedure_Body (E, For_Freeze => True); + -- Why is this needed for DIC, but not for other aspects (such as + -- Type_Invariant)??? + + Build_DIC_Procedure_Body (E); end if; end Expand_SPARK_N_Freeze_Type; @@ -530,7 +533,7 @@ package body Exp_SPARK is and then Present (DIC_Procedure (Typ)) and then not Has_Init_Expression (N) then - Call := Build_DIC_Call (Loc, Obj_Id, Typ); + Call := Build_DIC_Call (Loc, New_Occurrence_Of (Obj_Id, Loc), Typ); -- Partially insert the call into the tree by setting its parent -- pointer. diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index 11efd46651e..9e08e9c0f28 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -1446,21 +1446,27 @@ package body Exp_Util is -------------------- function Build_DIC_Call - (Loc : Source_Ptr; - Obj_Id : Entity_Id; - Typ : Entity_Id) return Node_Id + (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 ( Make_Unchecked_Type_Conversion (Loc, Subtype_Mark => New_Occurrence_Of (Formal_Typ, Loc), - Expression => New_Occurrence_Of (Obj_Id, Loc)))); + Expression => Obj_Name))); end Build_DIC_Call; ------------------------------ @@ -1472,9 +1478,13 @@ package body Exp_Util is -- Ghost mode. procedure Build_DIC_Procedure_Body - (Typ : Entity_Id; - For_Freeze : Boolean := False) + (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; @@ -1494,24 +1504,46 @@ package body Exp_Util is -- pragma. All generated code is added to list Stmts. procedure Add_Inherited_Tagged_DIC - (DIC_Prag : Node_Id; - Par_Typ : Entity_Id; - Deriv_Typ : Entity_Id; - Stmts : in out List_Id); + (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. Par_Typ is the - -- parent type whose DIC pragma is being inherited. Deriv_Typ is the - -- derived type inheriting the DIC pragma. All generated code is added - -- to list Stmts. + -- 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. All generated code - -- is added to list Stmts. + -- 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 -- @@ -1549,6 +1581,10 @@ package body Exp_Util is 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; ----------------------- @@ -1590,65 +1626,172 @@ package body Exp_Util is ------------------------------ procedure Add_Inherited_Tagged_DIC - (DIC_Prag : Node_Id; - Par_Typ : Entity_Id; - Deriv_Typ : Entity_Id; - Stmts : in out List_Id) + (DIC_Prag : Node_Id; + Expr : Node_Id; + Stmts : in out List_Id) is - Deriv_Proc : constant Entity_Id := DIC_Procedure (Deriv_Typ); - DIC_Args : constant List_Id := - Pragma_Argument_Associations (DIC_Prag); - DIC_Arg : constant Node_Id := First (DIC_Args); - DIC_Expr : constant Node_Id := Expression_Copy (DIC_Arg); - Par_Proc : constant Entity_Id := DIC_Procedure (Par_Typ); + begin + -- Once the DIC assertion expression is fully processed, add a check + -- to the statements of the DIC procedure. - Expr : Node_Id; + 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 - -- The processing of an inherited DIC assertion expression starts off - -- with a copy of the original parent expression where all references - -- to the parent type have already been replaced with references to - -- the _object formal parameter of the parent type's DIC procedure. + if not Present (Priv_Typ) and then not Present (Full_Typ) then + return; + end if; - pragma Assert (Present (DIC_Expr)); - Expr := New_Copy_Tree (DIC_Expr); + -- 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. - -- Perform the following substitutions: + if Is_Concurrent_Type (T) then + Deriv_Typ := Corresponding_Record_Type (T); + else + Deriv_Typ := T; + end if; - -- * Replace a reference to the _object parameter of the parent - -- type's DIC procedure with a reference to the _object parameter - -- of the derived types' DIC procedure. + pragma Assert (Present (Deriv_Typ)); - -- * Replace a reference to a discriminant of the parent type with - -- a suitable value from the point of view of the derived type. + -- 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. - -- * Replace a call to an overridden parent primitive with a call - -- to the overriding derived type primitive. + if Present (Priv_Typ) then + Prag := First_Rep_Item (Priv_Typ); + else + Prag := First_Rep_Item (Full_Typ); + end if; - -- * Replace a call to an inherited parent primitive with a call to - -- the internally-generated inherited derived type primitive. + 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 - -- Note that primitives defined in the private part are automatically - -- handled by the overriding/inheritance mechanism and do not require - -- an extra replacement pass. + if Contains (Pragmas_Seen, Prag) then + return; + end if; - pragma Assert (Present (Deriv_Proc) and then Present (Par_Proc)); + -- Extract arguments of the Default_Initial_Condition pragma - Replace_References - (Expr => Expr, - Par_Typ => Par_Typ, - Deriv_Typ => Deriv_Typ, - Par_Obj => First_Formal (Par_Proc), - Deriv_Obj => First_Formal (Deriv_Proc)); + Prag_Expr_Arg := First (Pragma_Argument_Associations (Prag)); + Prag_Expr := Expression_Copy (Prag_Expr_Arg); - -- Once the DIC assertion expression is fully processed, add a check - -- to the statements of the DIC procedure. + -- Pick up the implicit second argument of the pragma, which + -- indicates the type that the pragma applies to. - Add_DIC_Check - (DIC_Prag => DIC_Prag, - DIC_Expr => Expr, - Stmts => Stmts); - end Add_Inherited_Tagged_DIC; + 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 -- @@ -1657,6 +1800,7 @@ package body Exp_Util is 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 := @@ -1664,8 +1808,6 @@ package body Exp_Util is 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); - DIC_Proc : constant Entity_Id := DIC_Procedure (DIC_Typ); - Obj_Id : constant Entity_Id := First_Formal (DIC_Proc); -- Local variables @@ -1722,6 +1864,66 @@ package body Exp_Util is Stmts => Stmts); 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 + + begin + -- 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); @@ -1740,8 +1942,20 @@ package body Exp_Util is Proc_Id : Entity_Id; Stmts : List_Id := No_List; - Build_Body : Boolean := False; - -- Flag set when the type requires a DIC procedure body to be built + 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 @@ -1805,25 +2019,41 @@ package body Exp_Util is goto Leave; end if; - -- The working type may lack a DIC procedure declaration. This may be - -- due to several reasons: + -- Obtain both views of the type + + Get_Views (Work_Typ, Priv_Typ, Full_Typ, Dummy_1, CRec_Typ); - -- * The working type's own DIC pragma does not contain a verifiable - -- assertion expression. In this case there is no need to build a - -- DIC procedure because there is nothing to check. + -- The caller requests a body for the partial DIC procedure - -- * The working type derives from a parent type. In this case a DIC - -- procedure should be built only when the inherited DIC pragma has - -- a verifiable assertion expression. + if Partial_DIC then + Proc_Id := Partial_DIC_Procedure (Work_Typ); - Proc_Id := DIC_Procedure (Work_Typ); + -- The "full" DIC procedure body was already created - -- Build a DIC procedure declaration when the working type derives from - -- a parent type. + -- 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); - if No (Proc_Id) then - Build_DIC_Procedure_Declaration (Work_Typ); - Proc_Id := DIC_Procedure (Work_Typ); + 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 @@ -1843,123 +2073,146 @@ package body Exp_Util is Push_Scope (Proc_Id); Install_Formals (Proc_Id); - -- The working type defines its own DIC pragma. Replace the current - -- instance of the working type with the formal of the DIC procedure. - -- Note that there is no need to consider inherited DIC pragmas from - -- parent types because the working type's DIC pragma "hides" all - -- inherited DIC pragmas. + Obj_Id := First_Formal (Proc_Id); + pragma Assert (Present (Obj_Id)); - if Has_Own_DIC (Work_Typ) then - pragma Assert (DIC_Typ = Work_Typ); + -- The "partial" DIC procedure verifies the DICs of the partial view + -- only. - Add_Own_DIC - (DIC_Prag => DIC_Prag, - DIC_Typ => DIC_Typ, - Stmts => Stmts); + 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; - Build_Body := True; + -- Otherwise the "full" DIC procedure verifies the DICs of the full + -- view, well as DICs inherited from parent types. In addition, it + -- indirectly verifies the DICs of the partial view by calling the + -- "partial" DIC procedure. - -- Otherwise the working type inherits a DIC pragma from a parent type. - -- This processing is carried out when the type is frozen because the - -- state of all parent discriminants is known at that point. Note that - -- it is semantically sound to delay the creation of the DIC procedure - -- body till the freeze point. If the type has a DIC pragma of its own, - -- then the DIC procedure body would have already been constructed at - -- the end of the visible declarations and all parent DIC pragmas are - -- effectively "hidden" and irrelevant. + else + pragma Assert (Present (Full_Typ)); - elsif For_Freeze then - pragma Assert (Has_Inherited_DIC (Work_Typ)); - pragma Assert (DIC_Typ /= Work_Typ); + -- Check the DIC of the partial view by calling the "partial" DIC + -- procedure, unless the partial DIC body is empty. Generate: - -- The working type is tagged. The verification of the assertion - -- expression is subject to the same semantics as class-wide pre- - -- and postconditions. + -- 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; - if Is_Tagged_Type (Work_Typ) then - Add_Inherited_Tagged_DIC - (DIC_Prag => DIC_Prag, - Par_Typ => DIC_Typ, - Deriv_Typ => Work_Typ, - Stmts => Stmts); + -- Derived subtypes do not have a partial view - -- Otherwise the working type is not tagged. Verify the assertion - -- expression of the inherited DIC pragma by directly calling the - -- DIC procedure of the parent type. + if Present (Priv_Typ) then - else - Add_Inherited_DIC - (DIC_Prag => DIC_Prag, - Par_Typ => DIC_Typ, - Deriv_Typ => Work_Typ, - Stmts => Stmts); + -- The processing of the "full" DIC 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 DICs 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_DIC => ...; + -- + -- end Pack_2; + + -- As a result, the processing of the full view must also consider + -- all DICs of the partial view. + + if Is_Untagged_Private_Derivation (Priv_Typ, Full_Typ) then + null; + + -- Otherwise the DICs of the partial view are ignored + + else + -- Ignore the DICs of the partial view by eliminating the view + + Priv_Typ := Empty; + end if; end if; - Build_Body := True; + -- Process inherited Default_Initial_Conditions for all parent types + + Add_Parent_DICs (Work_Typ, Obj_Id, Stmts); end if; End_Scope; - if Build_Body then + -- Produce an empty completing body in the following cases: + -- * Assertions are disabled + -- * The DIC Assertion_Policy is Ignore - -- 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; - if No (Stmts) then - Stmts := New_List (Make_Null_Statement (Loc)); - end if; + -- Generate: + -- procedure DIC (_object : ) is + -- begin + -- + -- end DIC; - -- Generate: - -- procedure DIC (_object : ) is - -- begin - -- - -- end 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 - - Set_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; + 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); - -- Semi-insert the body into the tree for GNATprove by setting its - -- Parent field. This allows for proper upstream tree traversals. + -- Perform minor decoration in case the body is not analyzed - elsif GNATprove_Mode then - Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ))); + Set_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)); - -- Otherwise the body is part of the freezing actions of the working - -- type. + -- Link both spec and body to avoid generating duplicates - else - Append_Freeze_Action (Work_Typ, Proc_Body); - end if; + 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; <> @@ -1974,7 +2227,10 @@ package body Exp_Util is -- replaced by gotos which jump to the end of the routine and restore the -- Ghost mode. - procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id) is + 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; @@ -1985,6 +2241,7 @@ package body Exp_Util is DIC_Typ : Entity_Id; Proc_Decl : Node_Id; Proc_Id : Entity_Id; + Proc_Nam : Name_Id; Typ_Decl : Node_Id; CRec_Typ : Entity_Id; @@ -2060,17 +2317,35 @@ package body Exp_Util is 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 DIC procedure + -- 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 => - New_External_Name (Chars (Work_Typ), "Default_Initial_Condition")); + Make_Defining_Identifier (Loc, Chars => Proc_Nam); -- Perform minor decoration in case the declaration is not analyzed @@ -8908,6 +9183,13 @@ package body Exp_Util is return Present (Args) + + -- If there are args, but the first arg is Empty, then treat the + -- pragma the same as having no args (there may be a second arg that + -- is an implicitly added type arg, and Empty is a placeholder). + + and then Present (Get_Pragma_Arg (First (Args))) + and then Nkind (Get_Pragma_Arg (First (Args))) /= N_Null; end Is_Verifiable_DIC_Pragma; diff --git a/gcc/ada/exp_util.ads b/gcc/ada/exp_util.ads index 37eb86fba00..202ac3c954c 100644 --- a/gcc/ada/exp_util.ads +++ b/gcc/ada/exp_util.ads @@ -293,23 +293,29 @@ package Exp_Util is -- type is frozen. function Build_DIC_Call - (Loc : Source_Ptr; - Obj_Id : Entity_Id; - Typ : Entity_Id) return Node_Id; - -- Build a call to the DIC procedure of type Typ with Obj_Id as the actual + (Loc : Source_Ptr; + Obj_Name : Node_Id; + Typ : Entity_Id) return Node_Id; + -- Build a call to the DIC procedure for Typ with Obj_Name as the actual -- parameter. procedure Build_DIC_Procedure_Body - (Typ : Entity_Id; - For_Freeze : Boolean := False); + (Typ : Entity_Id; + Partial_DIC : Boolean := False); -- Create the body of the procedure which verifies the assertion expression - -- of pragma Default_Initial_Condition at run time. Flag For_Freeze should - -- be set when the body is constructed as part of the freezing actions for - -- Typ. - - procedure Build_DIC_Procedure_Declaration (Typ : Entity_Id); + -- of pragma Default_Initial_Condition at run time. Partial_DIC indicates + -- that a partial DIC-checking procedure body should be built, for checking + -- a DIC associated with the type's partial view, and which will be called + -- by the main DIC procedure. + + procedure Build_DIC_Procedure_Declaration + (Typ : Entity_Id; + Partial_DIC : Boolean := False); -- Create the declaration of the procedure which verifies the assertion - -- expression of pragma Default_Initial_Condition at run time. + -- expression of pragma Default_Initial_Condition at run time. Partial_DIC + -- indicates that a partial DIC-checking procedure should be declared, + -- for checking a DIC associated with the type's partial view, and which + -- will be called by the main DIC procedure. procedure Build_Invariant_Procedure_Body (Typ : Entity_Id; diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb index 5a1f8c49b8f..3caa84f0cb0 100644 --- a/gcc/ada/sem_aggr.adb +++ b/gcc/ada/sem_aggr.adb @@ -3715,9 +3715,10 @@ package body Sem_Aggr is -- -- This variable is updated as a side effect of function Get_Value. - Box_Node : Node_Id := Empty; - Is_Box_Present : Boolean := False; - Others_Box : Natural := 0; + Box_Node : Node_Id := Empty; + Is_Box_Present : Boolean := False; + Is_Box_Init_By_Default : Boolean := False; + Others_Box : Natural := 0; -- Ada 2005 (AI-287): Variables used in case of default initialization -- to provide a functionality similar to Others_Etype. Box_Present -- indicates that the component takes its default initialization; @@ -3842,6 +3843,17 @@ package body Sem_Aggr is Choices => Choice_List, Expression => Expr, Box_Present => Is_Box_Present)); + + -- If this association has a box for a component that is initialized + -- by default, then set flag on the new association to indicate that + -- the original association was for such a box-initialized component. + + if Resolve_Record_Aggregate.Is_Box_Present + and then not Is_Box_Present + and then Is_Box_Init_By_Default -- ??? + then + Set_Was_Default_Init_Box_Association (Last (Assoc_List)); + end if; end Add_Association; ----------------------------- @@ -4059,6 +4071,7 @@ package body Sem_Aggr is begin Is_Box_Present := False; + Is_Box_Init_By_Default := False; if No (From) then return Empty; @@ -5054,6 +5067,11 @@ package body Sem_Aggr is Ctyp : constant Entity_Id := Etype (Component); begin + -- Initially assume that the box is for a default-initialized + -- component and reset to False in cases where that's not true. + + Is_Box_Init_By_Default := True; + -- If there is a default expression for the aggregate, copy -- it into a new association. This copy must modify the scopes -- of internal types that may be attached to the expression @@ -5077,6 +5095,11 @@ package body Sem_Aggr is and then Nkind (Parent (Component)) = N_Component_Declaration and then Present (Expression (Parent (Component))) then + -- If component declaration has an initialization expression + -- then this is not a case of default initialization. + + Is_Box_Init_By_Default := False; + Expr := New_Copy_Tree_And_Copy_Dimensions (Expression (Parent (Component)), diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index ba7f5b8e0e8..b48aeb47739 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -3606,11 +3606,17 @@ package body Sem_Ch13 is -- wrapped inside of a procedure at the freeze point of the -- private type's full view. + -- A type entity argument is appended to facilitate inheriting + -- the aspect from parent types (see Build_DIC_Procedure_Body), + -- though that extra argument isn't documented for the pragma. + when Aspect_Default_Initial_Condition => Aitem := Make_Aitem_Pragma (Pragma_Argument_Associations => New_List ( Make_Pragma_Argument_Association (Loc, - Expression => Relocate_Node (Expr))), + Expression => Relocate_Node (Expr)), + Make_Pragma_Argument_Association (Sloc (Ent), + Expression => Ent)), Pragma_Name => Name_Default_Initial_Condition); diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index f487f734587..00834cea113 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2312,13 +2312,6 @@ package body Sem_Ch3 is procedure Build_Assertion_Bodies_For_Type (Typ : Entity_Id) is begin - -- Preanalyze and resolve the Default_Initial_Condition assertion - -- expression at the end of the declarations to catch any errors. - - if Has_DIC (Typ) then - Build_DIC_Procedure_Body (Typ); - end if; - if Nkind (Context) = N_Package_Specification then -- Preanalyze and resolve the class-wide invariants of an @@ -2341,32 +2334,57 @@ package body Sem_Ch3 is Partial_Invariant => True); end if; - -- Preanalyze and resolve the invariants of a private type - -- at the end of the visible declarations to catch potential - -- errors. Inherited class-wide invariants are not included - -- because they have already been resolved. + elsif Decls = Visible_Declarations (Context) then + -- Preanalyze and resolve the invariants of a private type + -- at the end of the visible declarations to catch potential + -- errors. Inherited class-wide invariants are not included + -- because they have already been resolved. - elsif Decls = Visible_Declarations (Context) - and then Ekind (Typ) in E_Limited_Private_Type - | E_Private_Type - | E_Record_Type_With_Private - and then Has_Own_Invariants (Typ) - then - Build_Invariant_Procedure_Body - (Typ => Typ, - Partial_Invariant => True); - - -- Preanalyze and resolve the invariants of a private type's - -- full view at the end of the private declarations to catch - -- potential errors. - - elsif Decls = Private_Declarations (Context) - and then (not Is_Private_Type (Typ) - or else Present (Underlying_Full_View (Typ))) - and then Has_Private_Declaration (Typ) - and then Has_Invariants (Typ) - then - Build_Invariant_Procedure_Body (Typ); + if Ekind (Typ) in E_Limited_Private_Type + | E_Private_Type + | E_Record_Type_With_Private + and then Has_Own_Invariants (Typ) + then + Build_Invariant_Procedure_Body + (Typ => Typ, + Partial_Invariant => True); + end if; + + -- Preanalyze and resolve the Default_Initial_Condition + -- assertion expression at the end of the declarations to + -- catch any errors. + + if Ekind (Typ) in E_Limited_Private_Type + | E_Private_Type + | E_Record_Type_With_Private + and then Has_Own_DIC (Typ) + then + Build_DIC_Procedure_Body + (Typ => Typ, + Partial_DIC => True); + end if; + + elsif Decls = Private_Declarations (Context) then + + -- Preanalyze and resolve the invariants of a private type's + -- full view at the end of the private declarations to catch + -- potential errors. + + if (not Is_Private_Type (Typ) + or else Present (Underlying_Full_View (Typ))) + and then Has_Private_Declaration (Typ) + and then Has_Invariants (Typ) + then + Build_Invariant_Procedure_Body (Typ); + end if; + + if (not Is_Private_Type (Typ) + or else Present (Underlying_Full_View (Typ))) + and then Has_Private_Declaration (Typ) + and then Has_DIC (Typ) + then + Build_DIC_Procedure_Body (Typ); + end if; end if; end if; end Build_Assertion_Bodies_For_Type; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 02369bc3660..1bcbb25d5f9 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -15111,7 +15111,7 @@ package body Sem_Prag is begin GNAT_Pragma; Check_No_Identifiers; - Check_At_Most_N_Arguments (1); + Check_At_Most_N_Arguments (2); -- Accounts for implicit type arg Typ := Empty; Stmt := Prev (N); @@ -15174,6 +15174,27 @@ package body Sem_Prag is Set_Has_Own_DIC (Typ); + -- A type entity argument is appended to facilitate inheriting the + -- aspect/pragma from parent types (see Build_DIC_Procedure_Body), + -- though that extra argument isn't documented for the pragma. + + if not Present (Arg2) then + -- When the pragma has no arguments, create an argument with + -- the value Empty, so the type name argument can be appended + -- following it (since it's expected as the second argument). + + if not Present (Arg1) then + Set_Pragma_Argument_Associations (N, New_List ( + Make_Pragma_Argument_Association (Sloc (Typ), + Expression => Empty))); + end if; + + Append_To + (Pragma_Argument_Associations (N), + Make_Pragma_Argument_Association (Sloc (Typ), + Expression => New_Occurrence_Of (Typ, Sloc (Typ)))); + end if; + -- Chain the pragma on the rep item chain for further processing Discard := Rep_Item_Too_Late (Typ, N, FOnly => True); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index e1535e2f540..72dbc6868af 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -26184,7 +26184,8 @@ package body Sem_Util is (Typ : Entity_Id; From_Typ : Entity_Id) is - DIC_Proc : Entity_Id; + DIC_Proc : Entity_Id; + Partial_DIC_Proc : Entity_Id; begin if Present (Typ) and then Present (From_Typ) then @@ -26205,6 +26206,7 @@ package body Sem_Util is end if; DIC_Proc := DIC_Procedure (From_Typ); + Partial_DIC_Proc := Partial_DIC_Procedure (From_Typ); -- The setting of the attributes is intentionally conservative. This -- prevents accidental clobbering of enabled attributes. @@ -26220,6 +26222,12 @@ package body Sem_Util is if Present (DIC_Proc) and then No (DIC_Procedure (Typ)) then Set_DIC_Procedure (Typ, DIC_Proc); end if; + + if Present (Partial_DIC_Proc) + and then No (Partial_DIC_Procedure (Typ)) + then + Set_Partial_DIC_Procedure (Typ, Partial_DIC_Proc); + end if; end if; end Propagate_DIC_Attributes; diff --git a/gcc/ada/sinfo.adb b/gcc/ada/sinfo.adb index c88d9a99533..2d0a9572f2c 100644 --- a/gcc/ada/sinfo.adb +++ b/gcc/ada/sinfo.adb @@ -3535,6 +3535,14 @@ package body Sinfo is return Flag2 (N); end Was_Attribute_Reference; + function Was_Default_Init_Box_Association + (N : Node_Id) return Boolean is + begin + pragma Assert (False + or else NT (N).Nkind = N_Component_Association); + return Flag14 (N); + end Was_Default_Init_Box_Association; + function Was_Expression_Function (N : Node_Id) return Boolean is begin @@ -7036,6 +7044,14 @@ package body Sinfo is Set_Flag2 (N, Val); end Set_Was_Attribute_Reference; + procedure Set_Was_Default_Init_Box_Association + (N : Node_Id; Val : Boolean := True) is + begin + pragma Assert (False + or else NT (N).Nkind = N_Component_Association); + Set_Flag14 (N, Val); + end Set_Was_Default_Init_Box_Association; + procedure Set_Was_Expression_Function (N : Node_Id; Val : Boolean := True) is begin diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads index 439eef4683e..f9b0667f8af 100644 --- a/gcc/ada/sinfo.ads +++ b/gcc/ada/sinfo.ads @@ -2412,6 +2412,11 @@ package Sinfo is -- instantiation prologue renames these attributes, and expansion later -- converts them into subprogram bodies. + -- Was_Default_Init_Box_Association (Flag14-Sem) + -- Present in N_Component_Association. Set to True if the original source + -- is an aggregate component association with a box (<>) for a component + -- that is initialized by default. + -- Was_Expression_Function (Flag18-Sem) -- Present in N_Subprogram_Body. True if the original source had an -- N_Expression_Function, which was converted to the N_Subprogram_Body @@ -4120,6 +4125,7 @@ package Sinfo is -- Expression (Node3) (empty if Box_Present) -- Loop_Actions (List5-Sem) -- Box_Present (Flag15) + -- Was_Default_Init_Box_Association (Flag14) -- Inherited_Discriminant (Flag13) -- Note: this structure is used for both record component associations @@ -4128,7 +4134,9 @@ package Sinfo is -- list of selector names in the record aggregate case, or a list of -- discrete choices in the array aggregate case or an N_Others_Choice -- node (which appears as a singleton list). Box_Present gives support - -- to Ada 2005 (AI-287). + -- to Ada 2005 (AI-287). Was_Default_Init_Box_Association is used for + -- determining the need for Default_Initial_Condition check on component + -- associations with a box. ---------------------------------- -- 4.3.1 Component Choice List -- @@ -10254,6 +10262,9 @@ package Sinfo is function Was_Attribute_Reference (N : Node_Id) return Boolean; -- Flag2 + function Was_Default_Init_Box_Association + (N : Node_Id) return Boolean; -- Flag14 + function Was_Expression_Function (N : Node_Id) return Boolean; -- Flag18 @@ -11366,6 +11377,9 @@ package Sinfo is procedure Set_Was_Attribute_Reference (N : Node_Id; Val : Boolean := True); -- Flag2 + procedure Set_Was_Default_Init_Box_Association + (N : Node_Id; Val : Boolean := True); -- Flag14 + procedure Set_Was_Expression_Function (N : Node_Id; Val : Boolean := True); -- Flag18 @@ -13477,6 +13491,7 @@ package Sinfo is pragma Inline (Visible_Declarations); pragma Inline (Used_Operations); pragma Inline (Was_Attribute_Reference); + pragma Inline (Was_Default_Init_Box_Association); pragma Inline (Was_Expression_Function); pragma Inline (Was_Originally_Stub); @@ -13842,6 +13857,7 @@ package Sinfo is pragma Inline (Set_Variants); pragma Inline (Set_Visible_Declarations); pragma Inline (Set_Was_Attribute_Reference); + pragma Inline (Set_Was_Default_Init_Box_Association); pragma Inline (Set_Was_Expression_Function); pragma Inline (Set_Was_Originally_Stub); -- 2.30.2