From 847d950d3a26b03229a289bfaa5163a5352ed7f4 Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Tue, 20 Oct 2015 10:43:21 +0000 Subject: [PATCH] 2015-10-20 Hristian Kirtchev * aspects.adb Add aspect Volatile_Function to table Canonical_Aspect. * aspect.ads Add aspect Volatile_Function to tables Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names and Implementation_Defined_Aspect. Aspects Async_Readers, Async_Writers, Effective_Reads and Effective_Writes are no longer Boolean. * einfo.adb (Get_Pragma): Add an entry for pragma Volatile_Function. * par-prag.adb (Prag): Pragma Volatile_Function does not need special processing by the parser. * rtsfind.ads Add an entry for Ada.Synchronous_Task_Control in table RTU_Id. Add an entry for Suspension_Object in table RE_Id. * sem_ch3.adb Fix SPARK RM references. (Analyze_Object_Contract): Update the error guard. * sem_ch5.adb Fix SPARK RM references. * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Ensure that a non-volatile function does not contain an effectively volatile parameter. (Analyze_Subprogram_Contract): Ensure that a non-volatile function does not contain an effectively volatile parameter. * sem_ch12.adb (Instantiate_Object): Remove the reference to the SPARK RM from the error message. * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing for aspects Async_Readers, Async_Writers, Effective_Reads, Effective_Writes and Volatile_Function. (Check_Aspect_At_Freeze_Point): Aspects Async_Readers, Async_Writers, Effective_Reads, Effective_Writes and Volatile_Function do not need special processing at the freeze point. * sem_prag.adb Add an entry for pragma Volatile_Function in table Sig_Flags. (Analyze_External_Property_In_Decl_Part): Reimplemented as Async_Readers, Async_Writers, Effective_Reads and Effective_Writes are no longer Boolean pragmas. (Analyze_Global_Item): An external state or effectively volatile object cannot appear as an item in pragma [Refined_]Global. (Analyze_Pragma): Change the implementation of Async_Readers, Async_Writers, Effective_Reads and Effective_Writes as these are no longer Boolean pragmas. Use routine Check_Static_Boolean_Expression to verify the optional Boolean expression of Async_Readers, Async_Writers, Constant_After_Elaboration, Effective_Reads, Effective_Writes, Extensions_Visible and Volatile_Function. Add processing for pragma Volatile_Function. (Check_Static_Boolean_Expression): New routine. (Find_Related_Context): Update the comment on usage. (Is_Enabled_Pragma): New routine. * sem_prag.ads (Is_Enabled_Pragma): New routine. * sem_res.adb Fix SPARK RM references. (Is_OK_Volatile_Context): Add detection for return statements. (Resolve_Actuals): Remove the check concerning an effectively volatile OUT actual parameter as this is now done by the SPARK flow analyzer. (Resolve_Entity_Name): Remove the check concerning an effectively volatile OUT formal parameter as this is now done by the SPARK flow analyzer. (Within_Volatile_Function): New routine. * sem_util.adb (Add_Contract_Item): Add processing for pragma Volatile_Function. (Check_Nonvolatile_Function_Profile): New routine. (Is_Descendant_Of_Suspension_Object): New routine. (Is_Effectively_Volatile): Protected types and descendants of Suspension_Object are now treated as effectively volatile. (Is_Enabled): The optional Boolean expression of pragmas Async_Readers, Async_Writers, Effective_Reads and Effective_Writes now appears as the first argument. (Is_Volatile_Function): New routine. * sem_util.ads Add SPARK RM references. (Add_Contract_Item): Update the comment on usage. (Check_Nonvolatile_Function_Profile): New routine. (Is_Effectively_Volatile): Update the comment on usage. (Is_Volatile_Function): New routine. * snames.ads-tmpl Add a predefined name and pragma id for Volatile_Function. From-SVN: r229047 --- gcc/ada/ChangeLog | 78 +++++++++++ gcc/ada/aspects.adb | 1 + gcc/ada/aspects.ads | 19 ++- gcc/ada/einfo.adb | 3 +- gcc/ada/par-prag.adb | 1 + gcc/ada/rtsfind.ads | 13 +- gcc/ada/sem_ch12.adb | 38 +++--- gcc/ada/sem_ch13.adb | 121 +++++++++++------ gcc/ada/sem_ch3.adb | 27 ++-- gcc/ada/sem_ch5.adb | 12 +- gcc/ada/sem_ch6.adb | 75 +++++++---- gcc/ada/sem_prag.adb | 291 ++++++++++++++++++++++++++++------------ gcc/ada/sem_prag.ads | 17 +++ gcc/ada/sem_res.adb | 90 +++++++++---- gcc/ada/sem_util.adb | 144 +++++++++++++++++++- gcc/ada/sem_util.ads | 28 +++- gcc/ada/snames.ads-tmpl | 2 + 17 files changed, 717 insertions(+), 243 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index db9d2158c42..1278c0a9cc8 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,81 @@ +2015-10-20 Hristian Kirtchev + + * aspects.adb Add aspect Volatile_Function to table + Canonical_Aspect. + * aspect.ads Add aspect Volatile_Function to tables + Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names + and Implementation_Defined_Aspect. Aspects Async_Readers, + Async_Writers, Effective_Reads and Effective_Writes are no + longer Boolean. + * einfo.adb (Get_Pragma): Add an entry for pragma + Volatile_Function. + * par-prag.adb (Prag): Pragma Volatile_Function does not need + special processing by the parser. + * rtsfind.ads Add an entry for Ada.Synchronous_Task_Control in + table RTU_Id. Add an entry for Suspension_Object in table RE_Id. + * sem_ch3.adb Fix SPARK RM references. + (Analyze_Object_Contract): Update the error guard. + * sem_ch5.adb Fix SPARK RM references. + * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Ensure + that a non-volatile function does not contain an effectively + volatile parameter. + (Analyze_Subprogram_Contract): Ensure + that a non-volatile function does not contain an effectively + volatile parameter. + * sem_ch12.adb (Instantiate_Object): Remove the reference to + the SPARK RM from the error message. + * sem_ch13.adb (Analyze_Aspect_Specifications): Add + processing for aspects Async_Readers, Async_Writers, + Effective_Reads, Effective_Writes and Volatile_Function. + (Check_Aspect_At_Freeze_Point): Aspects Async_Readers, + Async_Writers, Effective_Reads, Effective_Writes and + Volatile_Function do not need special processing at the freeze + point. + * sem_prag.adb Add an entry for pragma Volatile_Function in + table Sig_Flags. + (Analyze_External_Property_In_Decl_Part): + Reimplemented as Async_Readers, Async_Writers, Effective_Reads + and Effective_Writes are no longer Boolean pragmas. + (Analyze_Global_Item): An external state or effectively + volatile object cannot appear as an item in pragma + [Refined_]Global. + (Analyze_Pragma): Change the implementation + of Async_Readers, Async_Writers, Effective_Reads and + Effective_Writes as these are no longer Boolean pragmas. + Use routine Check_Static_Boolean_Expression to verify the + optional Boolean expression of Async_Readers, Async_Writers, + Constant_After_Elaboration, Effective_Reads, Effective_Writes, + Extensions_Visible and Volatile_Function. Add processing for + pragma Volatile_Function. + (Check_Static_Boolean_Expression): New routine. + (Find_Related_Context): Update the comment on usage. + (Is_Enabled_Pragma): New routine. + * sem_prag.ads (Is_Enabled_Pragma): New routine. + * sem_res.adb Fix SPARK RM references. + (Is_OK_Volatile_Context): Add detection for return statements. + (Resolve_Actuals): Remove the check concerning an effectively volatile + OUT actual parameter as this is now done by the SPARK flow analyzer. + (Resolve_Entity_Name): Remove the check concerning an effectively + volatile OUT formal parameter as this is now done by the SPARK + flow analyzer. (Within_Volatile_Function): New routine. + * sem_util.adb (Add_Contract_Item): Add processing for pragma + Volatile_Function. + (Check_Nonvolatile_Function_Profile): New routine. + (Is_Descendant_Of_Suspension_Object): New routine. + (Is_Effectively_Volatile): Protected types and descendants of + Suspension_Object are now treated as effectively volatile. + (Is_Enabled): The optional Boolean expression of pragmas + Async_Readers, Async_Writers, Effective_Reads and Effective_Writes + now appears as the first argument. + (Is_Volatile_Function): New routine. + * sem_util.ads Add SPARK RM references. + (Add_Contract_Item): Update the comment on usage. + (Check_Nonvolatile_Function_Profile): New routine. + (Is_Effectively_Volatile): Update the comment on usage. + (Is_Volatile_Function): New routine. + * snames.ads-tmpl Add a predefined name and pragma id for + Volatile_Function. + 2015-10-20 Arnaud Charlet * gnat_ugn.texi, gnat_rm.texi: Regenerate. diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index b945a8befb4..3fc20498fc1 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -610,6 +610,7 @@ package body Aspects is Aspect_Volatile => Aspect_Volatile, Aspect_Volatile_Components => Aspect_Volatile_Components, Aspect_Volatile_Full_Access => Aspect_Volatile_Full_Access, + Aspect_Volatile_Function => Aspect_Volatile_Function, Aspect_Warnings => Aspect_Warnings, Aspect_Write => Aspect_Write); diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 2d71394e149..8b7fca89b6e 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -78,6 +78,8 @@ package Aspects is Aspect_Address, Aspect_Alignment, Aspect_Annotate, -- GNAT + Aspect_Async_Readers, -- GNAT + Aspect_Async_Writers, -- GNAT Aspect_Attach_Handler, Aspect_Bit_Order, Aspect_Component_Size, @@ -96,6 +98,8 @@ package Aspects is Aspect_Dimension_System, -- GNAT Aspect_Dispatching_Domain, Aspect_Dynamic_Predicate, + Aspect_Effective_Reads, -- GNAT + Aspect_Effective_Writes, -- GNAT Aspect_Extensions_Visible, -- GNAT Aspect_External_Name, Aspect_External_Tag, @@ -145,6 +149,7 @@ package Aspects is Aspect_Unsuppress, Aspect_Value_Size, -- GNAT Aspect_Variable_Indexing, + Aspect_Volatile_Function, -- GNAT Aspect_Warnings, -- GNAT Aspect_Write, @@ -167,15 +172,11 @@ package Aspects is -- the aspect value is inherited from the parent, in which case, we do -- not allow False if we inherit a True value from the parent. - Aspect_Async_Readers, -- GNAT - Aspect_Async_Writers, -- GNAT Aspect_Asynchronous, Aspect_Atomic, Aspect_Atomic_Components, Aspect_Disable_Controlled, -- GNAT Aspect_Discard_Names, - Aspect_Effective_Reads, -- GNAT - Aspect_Effective_Writes, -- GNAT Aspect_Export, Aspect_Favor_Top_Level, -- GNAT Aspect_Independent, @@ -264,6 +265,7 @@ package Aspects is Aspect_Unreferenced => True, Aspect_Unreferenced_Objects => True, Aspect_Value_Size => True, + Aspect_Volatile_Function => True, Aspect_Warnings => True, others => False); @@ -291,7 +293,7 @@ package Aspects is -- aspect is enabled. If it is False, the aspect is disabled. subtype Boolean_Aspects is - Aspect_Id range Aspect_Async_Readers .. Aspect_Id'Last; + Aspect_Id range Aspect_Asynchronous .. Aspect_Id'Last; subtype Pre_Post_Aspects is Aspect_Id range Aspect_Post .. Aspect_Precondition; @@ -312,6 +314,8 @@ package Aspects is Aspect_Address => Expression, Aspect_Alignment => Expression, Aspect_Annotate => Expression, + Aspect_Async_Readers => Optional_Expression, + Aspect_Async_Writers => Optional_Expression, Aspect_Attach_Handler => Expression, Aspect_Bit_Order => Expression, Aspect_Component_Size => Expression, @@ -330,6 +334,8 @@ package Aspects is Aspect_Dimension_System => Expression, Aspect_Dispatching_Domain => Expression, Aspect_Dynamic_Predicate => Expression, + Aspect_Effective_Reads => Optional_Expression, + Aspect_Effective_Writes => Optional_Expression, Aspect_Extensions_Visible => Optional_Expression, Aspect_External_Name => Expression, Aspect_External_Tag => Expression, @@ -379,6 +385,7 @@ package Aspects is Aspect_Unsuppress => Name, Aspect_Value_Size => Expression, Aspect_Variable_Indexing => Name, + Aspect_Volatile_Function => Optional_Expression, Aspect_Warnings => Name, Aspect_Write => Name, @@ -511,6 +518,7 @@ package Aspects is Aspect_Volatile => Name_Volatile, Aspect_Volatile_Components => Name_Volatile_Components, Aspect_Volatile_Full_Access => Name_Volatile_Full_Access, + Aspect_Volatile_Function => Name_Volatile_Function, Aspect_Warnings => Name_Warnings, Aspect_Write => Name_Write); @@ -731,6 +739,7 @@ package Aspects is Aspect_Synchronization => Never_Delay, Aspect_Test_Case => Never_Delay, Aspect_Unimplemented => Never_Delay, + Aspect_Volatile_Function => Never_Delay, Aspect_Warnings => Never_Delay, Aspect_Alignment => Rep_Aspect, diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index 4e5d0836236..5adc28f3652 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -7000,7 +7000,8 @@ package body Einfo is Id = Pragma_Part_Of or else Id = Pragma_Refined_Depends or else Id = Pragma_Refined_Global or else - Id = Pragma_Refined_State; + Id = Pragma_Refined_State or else + Id = Pragma_Volatile_Function; -- Contract / test case pragmas diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index bcb8adde678..a3ed732995b 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1486,6 +1486,7 @@ begin Pragma_Volatile | Pragma_Volatile_Components | Pragma_Volatile_Full_Access | + Pragma_Volatile_Function | Pragma_Warning_As_Error | Pragma_Weak_External | Pragma_Validity_Checks => diff --git a/gcc/ada/rtsfind.ads b/gcc/ada/rtsfind.ads index af2b6757875..22f93901e0c 100644 --- a/gcc/ada/rtsfind.ads +++ b/gcc/ada/rtsfind.ads @@ -23,15 +23,15 @@ -- -- ------------------------------------------------------------------------------ -with Types; use Types; - -package Rtsfind is - -- This package contains the routine that is used to obtain runtime library -- entities, loading in the required runtime library packages on demand. It -- is also used for such purposes as finding System.Address when System has -- not been explicitly With'ed. +with Types; use Types; + +package Rtsfind is + ------------------------ -- Runtime Unit Table -- ------------------------ @@ -131,6 +131,7 @@ package Rtsfind is Ada_Real_Time, Ada_Streams, Ada_Strings, + Ada_Synchronous_Task_Control, Ada_Tags, Ada_Task_Identification, Ada_Task_Termination, @@ -606,6 +607,8 @@ package Rtsfind is RE_Unbounded_String, -- Ada.Strings.Unbounded + RE_Suspension_Object, -- Ada.Synchronous_Task_Control + RE_Access_Level, -- Ada.Tags RE_Alignment, -- Ada.Tags RE_Address_Array, -- Ada.Tags @@ -1837,6 +1840,8 @@ package Rtsfind is RE_Unbounded_String => Ada_Strings_Unbounded, + RE_Suspension_Object => Ada_Synchronous_Task_Control, + RE_Access_Level => Ada_Tags, RE_Alignment => Ada_Tags, RE_Address_Array => Ada_Tags, diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index ba0daa9f3ac..beb67574629 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -5318,28 +5318,24 @@ package body Sem_Ch12 is if Need_Subprogram_Instance_Body (N, Act_Decl_Id) then Check_Forward_Instantiation (Gen_Decl); - -- The wrapper package is always delayed, because it does not - -- constitute a freeze point, but to insure that the freeze - -- node is placed properly, it is created directly when - -- instantiating the body (otherwise the freeze node might - -- appear to early for nested instantiations). + -- The wrapper package is always delayed, because it does not + -- constitute a freeze point, but to insure that the freeze node + -- is placed properly, it is created directly when instantiating + -- the body (otherwise the freeze node might appear to early for + -- nested instantiations). For ASIS purposes, indicate that the + -- wrapper package has replaced the instantiation node. elsif Nkind (Parent (N)) = N_Compilation_Unit then - - -- For ASIS purposes, indicate that the wrapper package has - -- replaced the instantiation node. - Rewrite (N, Unit (Parent (N))); Set_Unit (Parent (N), N); end if; - elsif Nkind (Parent (N)) = N_Compilation_Unit then + -- Replace instance node for library-level instantiations of + -- intrinsic subprograms, for ASIS use. - -- Replace instance node for library-level instantiations of - -- intrinsic subprograms, for ASIS use. - - Rewrite (N, Unit (Parent (N))); - Set_Unit (Parent (N), N); + elsif Nkind (Parent (N)) = N_Compilation_Unit then + Rewrite (N, Unit (Parent (N))); + Set_Unit (Parent (N), N); end if; if Parent_Installed then @@ -5359,7 +5355,6 @@ package body Sem_Ch12 is if SPARK_Mode = On then Dynamic_Elaboration_Checks := False; end if; - end if; <> @@ -10663,17 +10658,18 @@ package body Sem_Ch12 is ("actual must exclude null to match generic formal#", Actual); end if; - -- An effectively volatile object cannot be used as an actual in - -- a generic instance. The following check is only relevant when - -- SPARK_Mode is on as it is not a standard Ada legality rule. + -- An effectively volatile object cannot be used as an actual in a + -- generic instantiation (SPARK RM 7.1.3(7)). The following check is + -- relevant only when SPARK_Mode is on as it is not a standard Ada + -- legality rule. if SPARK_Mode = On and then Present (Actual) and then Is_Effectively_Volatile_Object (Actual) then Error_Msg_N - ("volatile object cannot act as actual in generic instantiation " - & "(SPARK RM 7.1.3(8))", Actual); + ("volatile object cannot act as actual in generic instantiation", + Actual); end if; return List; diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 95624e69401..820a2d1cb4c 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -2284,6 +2284,36 @@ package body Sem_Ch13 is goto Continue; end Abstract_State; + -- Aspect Async_Readers is never delayed because it is + -- equivalent to a source pragma which appears after the + -- related object declaration. + + when Aspect_Async_Readers => + Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Async_Readers); + + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); + goto Continue; + + -- Aspect Async_Writers is never delayed because it is + -- equivalent to a source pragma which appears after the + -- related object declaration. + + when Aspect_Async_Writers => + Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Async_Writers); + + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); + goto Continue; + -- Aspect Constant_After_Elaboration is never delayed because -- it is equivalent to a source pragma which appears after the -- related object declaration. @@ -2354,6 +2384,36 @@ package body Sem_Ch13 is Insert_Pragma (Aitem); goto Continue; + -- Aspect Effecitve_Reads is never delayed because it is + -- equivalent to a source pragma which appears after the + -- related object declaration. + + when Aspect_Effective_Reads => + Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Effective_Reads); + + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); + goto Continue; + + -- Aspect Effective_Writes is never delayed because it is + -- equivalent to a source pragma which appears after the + -- related object declaration. + + when Aspect_Effective_Writes => + Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Effective_Writes); + + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); + goto Continue; + -- Aspect Extensions_Visible is never delayed because it is -- equivalent to a source pragma which appears after the -- related subprogram. @@ -2779,6 +2839,21 @@ package body Sem_Ch13 is end; end if; + -- Aspect Volatile_Function is never delayed because it is + -- equivalent to a source pragma which appears after the + -- related subprogram. + + when Aspect_Volatile_Function => + Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Volatile_Function); + + Decorate (Aspect, Aitem); + Insert_Pragma (Aitem); + goto Continue; + -- Case 2e: Annotate aspect when Aspect_Annotate => @@ -3234,47 +3309,10 @@ package body Sem_Ch13 is goto Continue; end if; - -- External property aspects are Boolean by nature, but - -- their pragmas must contain two arguments, the second - -- being the optional Boolean expression. - - if A_Id = Aspect_Async_Readers or else - A_Id = Aspect_Async_Writers or else - A_Id = Aspect_Effective_Reads or else - A_Id = Aspect_Effective_Writes - then - declare - Args : List_Id; - - begin - -- The first argument of the external property pragma - -- is the related object. - - Args := - New_List ( - Make_Pragma_Argument_Association (Sloc (Ent), - Expression => Ent)); - - -- The second argument is the optional Boolean - -- expression which must be propagated even if it - -- evaluates to False as this has special semantic - -- meaning. - - if Present (Expr) then - Append_To (Args, - Make_Pragma_Argument_Association (Loc, - Expression => Relocate_Node (Expr))); - end if; - - Make_Aitem_Pragma - (Pragma_Argument_Associations => Args, - Pragma_Name => Nam); - end; - -- Cases where we do not delay, includes all cases where the -- expression is missing other than the above cases. - elsif not Delay_Required or else No (Expr) then + if not Delay_Required or else No (Expr) then Make_Aitem_Pragma (Pragma_Argument_Associations => New_List ( Make_Pragma_Argument_Association (Sloc (Ent), @@ -9285,12 +9323,16 @@ package body Sem_Ch13 is when Aspect_Abstract_State | Aspect_Annotate | + Aspect_Async_Readers | + Aspect_Async_Writers | Aspect_Constant_After_Elaboration | Aspect_Contract_Cases | Aspect_Default_Initial_Condition | Aspect_Depends | Aspect_Dimension | Aspect_Dimension_System | + Aspect_Effective_Reads | + Aspect_Effective_Writes | Aspect_Extensions_Visible | Aspect_Ghost | Aspect_Global | @@ -9309,7 +9351,8 @@ package body Sem_Ch13 is Aspect_Refined_State | Aspect_SPARK_Mode | Aspect_Test_Case | - Aspect_Unimplemented => + Aspect_Unimplemented | + Aspect_Volatile_Function => raise Program_Error; end case; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index b8f901da512..555c361b1d3 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -3313,19 +3313,16 @@ package body Sem_Ch3 is if Ekind (Obj_Id) = E_Constant then - -- A constant cannot be effectively volatile. This check is only - -- relevant with SPARK_Mode on as it is not a standard Ada legality - -- rule. Do not flag internally-generated constants that map generic - -- formals to actuals in instantiations (SPARK RM 7.1.3(6)). + -- A constant cannot be effectively volatile (SPARK RM 7.1.3(4)). + -- This check is relevant only when SPARK_Mode is on as it is not a + -- standard Ada legality rule. Internally-generated constants that + -- map generic formals to actuals in instantiations are allowed to + -- be volatile. if SPARK_Mode = On + and then Comes_From_Source (Obj_Id) and then Is_Effectively_Volatile (Obj_Id) and then No (Corresponding_Generic_Association (Parent (Obj_Id))) - - -- Don't give this for internally generated entities (such as the - -- FIRST and LAST temporaries generated for bounds). - - and then Comes_From_Source (Obj_Id) then Error_Msg_N ("constant cannot be volatile", Obj_Id); end if; @@ -3334,7 +3331,7 @@ package body Sem_Ch3 is else pragma Assert (Ekind (Obj_Id) = E_Variable); - -- The following checks are only relevant when SPARK_Mode is on as + -- The following checks are relevant only when SPARK_Mode is on as -- they are not standard Ada legality rules. Internally generated -- temporaries are ignored. @@ -3342,7 +3339,7 @@ package body Sem_Ch3 is if Is_Effectively_Volatile (Obj_Id) then -- The declaration of an effectively volatile object must - -- appear at the library level (SPARK RM 7.1.3(7), C.6(6)). + -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)). if not Is_Library_Level_Entity (Obj_Id) then Error_Msg_N @@ -3367,7 +3364,7 @@ package body Sem_Ch3 is else -- A non-effectively volatile object cannot have effectively - -- volatile components (SPARK RM 7.1.3(7)). + -- volatile components (SPARK RM 7.1.3(6)). if not Is_Effectively_Volatile (Obj_Id) and then Has_Volatile_Component (Obj_Typ) @@ -19282,9 +19279,9 @@ package body Sem_Ch3 is end if; end if; - -- A discriminant cannot be effectively volatile. This check is only - -- relevant when SPARK_Mode is on as it is not standard Ada legality - -- rule (SPARK RM 7.1.3(6)). + -- A discriminant cannot be effectively volatile (SPARK RM 7.1.3(6)). + -- This check is relevant only when SPARK_Mode is on as it is not a + -- standard Ada legality rule. if SPARK_Mode = On and then Is_Effectively_Volatile (Defining_Identifier (Discr)) diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 234317c0f1d..3e2e26b620b 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -2279,9 +2279,9 @@ package body Sem_Ch5 is end if; end if; - -- A loop parameter cannot be effectively volatile. This check is - -- peformed only when SPARK_Mode is on as it is not a standard Ada - -- legality check (SPARK RM 7.1.3(6)). + -- A loop parameter cannot be effectively volatile (SPARK RM 7.1.3(4)). + -- This check is relevant only when SPARK_Mode is on as it is not a + -- standard Ada legality check. -- Not clear whether this applies to element iterators, where the -- cursor is not an explicit entity ??? @@ -3037,9 +3037,9 @@ package body Sem_Ch5 is end; end if; - -- A loop parameter cannot be effectively volatile. This check is - -- peformed only when SPARK_Mode is on as it is not a standard Ada - -- legality check (SPARK RM 7.1.3(6)). + -- A loop parameter cannot be effectively volatile (SPARK RM 7.1.3(4)). + -- This check is relevant only when SPARK_Mode is on as it is not a + -- standard Ada legality check. if SPARK_Mode = On and then Is_Effectively_Volatile (Id) then Error_Msg_N ("loop parameter cannot be volatile", Id); diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 0d61181840d..5e1ddf5d167 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -2228,6 +2228,19 @@ package body Sem_Ch6 is Check_Result_And_Post_State (Body_Id); + -- A stand alone non-volatile function body cannot have an effectively + -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This + -- check is relevant only when SPARK_Mode is on as it is not a standard + -- legality rule. The check is performed here because Volatile_Function + -- is processed after the analysis of the related subprogram body. + + if SPARK_Mode = On + and then Ekind_In (Body_Id, E_Function, E_Generic_Function) + and then not Is_Volatile_Function (Body_Id) + then + Check_Nonvolatile_Function_Profile (Body_Id); + end if; + -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. @@ -4086,6 +4099,19 @@ package body Sem_Ch6 is Check_Result_And_Post_State (Subp_Id); end if; + -- A non-volatile function cannot have an effectively volatile formal + -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant + -- only when SPARK_Mode is on as it is not a standard legality rule. The + -- check is performed here because pragma Volatile_Function is processed + -- after the analysis of the related subprogram declaration. + + if SPARK_Mode = On + and then Ekind_In (Subp_Id, E_Function, E_Generic_Function) + and then not Is_Volatile_Function (Subp_Id) + then + Check_Nonvolatile_Function_Profile (Subp_Id); + end if; + -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. @@ -4451,9 +4477,9 @@ package body Sem_Ch6 is -- the check is applied later (see Analyze_Subprogram_Declaration). if not Nkind_In (Original_Node (Parent (N)), - N_Subprogram_Renaming_Declaration, N_Abstract_Subprogram_Declaration, - N_Formal_Abstract_Subprogram_Declaration) + N_Formal_Abstract_Subprogram_Declaration, + N_Subprogram_Renaming_Declaration) then if Is_Abstract_Type (Etype (Designator)) and then not Is_Interface (Etype (Designator)) @@ -4464,14 +4490,15 @@ package body Sem_Ch6 is -- Ada 2012 (AI-0073): Extend this test to subprograms with an -- access result whose designated type is abstract. - elsif Nkind (Result_Definition (N)) = N_Access_Definition + elsif Ada_Version >= Ada_2012 + and then Nkind (Result_Definition (N)) = N_Access_Definition and then not Is_Class_Wide_Type (Designated_Type (Etype (Designator))) and then Is_Abstract_Type (Designated_Type (Etype (Designator))) - and then Ada_Version >= Ada_2012 then - Error_Msg_N ("function whose access result designates " - & "abstract type must be abstract", N); + Error_Msg_N + ("function whose access result designates abstract type " + & "must be abstract", N); end if; end if; end if; @@ -9933,17 +9960,6 @@ package body Sem_Ch6 is (T : List_Id; Related_Nod : Node_Id) is - Context : constant Node_Id := Parent (Parent (T)); - Param_Spec : Node_Id; - Formal : Entity_Id; - Formal_Type : Entity_Id; - Default : Node_Id; - Ptype : Entity_Id; - - Num_Out_Params : Nat := 0; - First_Out_Param : Entity_Id := Empty; - -- Used for setting Is_Only_Out_Parameter - function Designates_From_Limited_With (Typ : Entity_Id) return Boolean; -- Determine whether an access type designates a type coming from a -- limited view. @@ -9986,6 +10002,19 @@ package body Sem_Ch6 is and then Is_Class_Wide_Type (Etype (Prefix (D)))); end Is_Class_Wide_Default; + -- Local variables + + Context : constant Node_Id := Parent (Parent (T)); + Default : Node_Id; + Formal : Entity_Id; + Formal_Type : Entity_Id; + Param_Spec : Node_Id; + Ptype : Entity_Id; + + Num_Out_Params : Nat := 0; + First_Out_Param : Entity_Id := Empty; + -- Used for setting Is_Only_Out_Parameter + -- Start of processing for Process_Formals begin @@ -10269,8 +10298,8 @@ package body Sem_Ch6 is Null_Exclusion_Static_Checks (Param_Spec); end if; - -- The following checks are relevant when SPARK_Mode is on as these - -- are not standard Ada legality rules. + -- The following checks are relevant only when SPARK_Mode is on as + -- these are not standard Ada legality rules. if SPARK_Mode = On then if Ekind_In (Scope (Formal), E_Function, E_Generic_Function) then @@ -10282,14 +10311,6 @@ package body Sem_Ch6 is Error_Msg_N ("function cannot have parameter of mode `OUT` or " & "`IN OUT`", Formal); - - -- A function cannot have an effectively volatile formal - -- parameter (SPARK RM 7.1.3(10)). - - elsif Is_Effectively_Volatile (Formal) then - Error_Msg_N - ("function cannot have a volatile formal parameter", - Formal); end if; -- A procedure cannot have an effectively volatile formal diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index dabacf576df..2733dc39bd2 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -206,7 +206,8 @@ package body Sem_Prag is function Find_Related_Context (Prag : Node_Id; Do_Checks : Boolean := False) return Node_Id; - -- Subsidiaty to the analysis of pragmas Constant_After_Elaboration and + -- Subsidiaty to the analysis of pragmas Async_Readers, Async_Writers, + -- Constant_After_Elaboration, Effective_Reads, Effective_Writers and -- Part_Of. Find the first source declaration or statement found while -- traversing the previous node chain starting from pragma Prag. If flag -- Do_Checks is set, the routine reports duplicate pragmas. The routine @@ -1720,19 +1721,12 @@ package body Sem_Prag is (N : Node_Id; Expr_Val : out Boolean) is - Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); - Expr : constant Node_Id := Get_Pragma_Arg (Next (Arg1)); - Obj_Id : constant Entity_Id := Entity (Get_Pragma_Arg (Arg1)); - - Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode; + Arg1 : constant Node_Id := First (Pragma_Argument_Associations (N)); + Obj_Decl : constant Node_Id := Find_Related_Context (N); + Obj_Id : constant Entity_Id := Defining_Entity (Obj_Decl); + Expr : Node_Id; begin - -- Set the Ghost mode in effect from the pragma. Due to the delayed - -- analysis of the pragma, the Ghost mode at point of declaration and - -- point of analysis may not necessarely be the same. Use the mode in - -- effect at the point of declaration. - - Set_Ghost_Mode (N); Error_Msg_Name_1 := Pragma_Name (N); -- An external property pragma must apply to an effectively volatile @@ -1754,17 +1748,13 @@ package body Sem_Prag is Expr_Val := True; - if Present (Expr) then - Analyze_And_Resolve (Expr, Standard_Boolean); + if Present (Arg1) then + Expr := Get_Pragma_Arg (Arg1); if Is_OK_Static_Expression (Expr) then Expr_Val := Is_True (Expr_Value (Expr)); - else - SPARK_Msg_N ("expression of % must be static", Expr); end if; end if; - - Ghost_Mode := Save_Ghost_Mode; end Analyze_External_Property_In_Decl_Part; --------------------------------- @@ -1924,6 +1914,18 @@ package body Sem_Prag is SPARK_Msg_N ("\use its constituents instead", Item); return; + -- An external state cannot appear as a global item of a + -- nonvolatile function (SPARK RM 7.1.3(8)). + + elsif Is_External_State (Item_Id) + and then Ekind_In (Spec_Id, E_Function, E_Generic_Function) + and then not Is_Volatile_Function (Spec_Id) + then + SPARK_Msg_NE + ("external state & cannot act as global item of " + & "nonvolatile function", Item, Item_Id); + return; + -- If the reference to the abstract state appears in an -- enclosing package body that will eventually refine the -- state, record the reference for future checks. @@ -1956,9 +1958,11 @@ package body Sem_Prag is and then Is_Effectively_Volatile (Item_Id) then -- An effectively volatile object cannot appear as a global - -- item of a function (SPARK RM 7.1.3(9)). + -- item of a nonvolatile function (SPARK RM 7.1.3(8)). - if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then + if Ekind_In (Spec_Id, E_Function, E_Generic_Function) + and then not Is_Volatile_Function (Spec_Id) + then Error_Msg_NE ("volatile object & cannot act as global item of a " & "function", Item, Item_Id); @@ -2936,6 +2940,13 @@ package body Sem_Prag is -- In this version of the procedure, the identifier name is given as -- a string with lower case letters. + procedure Check_Static_Boolean_Expression (Expr : Node_Id); + -- Subsidiary to the analysis of pragmas Async_Readers, Async_Writers, + -- Constant_After_Elaboration, Effective_Reads, Effective_Writes, + -- Extensions_Visible and Volatile_Function. Ensure that expression Expr + -- is an OK static boolean expression. Emit an error if this is not the + -- case. + procedure Check_Static_Constraint (Constr : Node_Id); -- Constr is a constraint from an N_Subtype_Indication node from a -- component constraint in an Unchecked_Union type. This routine checks @@ -5070,6 +5081,22 @@ package body Sem_Prag is Check_Optional_Identifier (Arg, Name_Find); end Check_Optional_Identifier; + ------------------------------------- + -- Check_Static_Boolean_Expression -- + ------------------------------------- + + procedure Check_Static_Boolean_Expression (Expr : Node_Id) is + begin + if Present (Expr) then + Analyze_And_Resolve (Expr, Standard_Boolean); + + if not Is_OK_Static_Expression (Expr) then + Error_Pragma_Arg + ("expression of pragma % must be static", Expr); + end if; + end if; + end Check_Static_Boolean_Expression; + ----------------------------- -- Check_Static_Constraint -- ----------------------------- @@ -11079,43 +11106,45 @@ package body Sem_Prag is -- Async_Readers/Async_Writers/Effective_Reads/Effective_Writes -- ------------------------------------------------------------------ - -- pragma Asynch_Readers ( object_LOCAL_NAME [, FLAG] ); - -- pragma Asynch_Writers ( object_LOCAL_NAME [, FLAG] ); - -- pragma Effective_Reads ( object_LOCAL_NAME [, FLAG] ); - -- pragma Effective_Writes ( object_LOCAL_NAME [, FLAG] ); - - -- FLAG ::= boolean_EXPRESSION + -- pragma Asynch_Readers [ (boolean_EXPRESSION) ]; + -- pragma Asynch_Writers [ (boolean_EXPRESSION) ]; + -- pragma Effective_Reads [ (boolean_EXPRESSION) ]; + -- pragma Effective_Writes [ (boolean_EXPRESSION) ]; when Pragma_Async_Readers | Pragma_Async_Writers | Pragma_Effective_Reads | Pragma_Effective_Writes => Async_Effective : declare - Duplic : Node_Id; - Expr : Node_Id; - Obj : Node_Id; - Obj_Id : Entity_Id; + Obj_Decl : Node_Id; + Obj_Id : Entity_Id; begin GNAT_Pragma; Check_No_Identifiers; - Check_At_Least_N_Arguments (1); - Check_At_Most_N_Arguments (2); - Check_Arg_Is_Local_Name (Arg1); - Error_Msg_Name_1 := Pname; + Check_At_Most_N_Arguments (1); - Obj := Get_Pragma_Arg (Arg1); - Expr := Get_Pragma_Arg (Arg2); + Obj_Decl := Find_Related_Context (N, Do_Checks => True); + + -- Object declaration + + if Nkind (Obj_Decl) = N_Object_Declaration then + null; + + -- Otherwise the pragma is associated with an illegal construact + + else + Pragma_Misplaced; + return; + end if; + + Obj_Id := Defining_Entity (Obj_Decl); -- Perform minimal verification to ensure that the argument is at -- least a variable. Subsequent finer grained checks will be done -- at the end of the declarative region the contains the pragma. - if Is_Entity_Name (Obj) - and then Present (Entity (Obj)) - and then Ekind (Entity (Obj)) = E_Variable - then - Obj_Id := Entity (Obj); + if Ekind (Obj_Id) = E_Variable then -- A pragma that applies to a Ghost entity becomes Ghost for -- the purposes of legality checks and removal of ignored Ghost @@ -11123,30 +11152,19 @@ package body Sem_Prag is Mark_Pragma_As_Ghost (N, Obj_Id); - -- Detect a duplicate pragma. Note that it is not efficient to - -- examine preceding statements as Boolean aspects may appear - -- anywhere between the related object declaration and its - -- freeze point. As an alternative, inspect the contents of the - -- variable contract. - - Duplic := Get_Pragma (Obj_Id, Prag_Id); + -- Analyze the Boolean expression (if any) - if Present (Duplic) then - Error_Msg_Sloc := Sloc (Duplic); - Error_Msg_N ("pragma % duplicates pragma declared #", N); + if Present (Arg1) then + Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1)); + end if; - -- No duplicate detected + -- Chain the pragma on the contract for further processing by + -- Analyze_External_Property_In_Decl_Part. - else - if Present (Expr) then - Preanalyze_And_Resolve (Expr, Standard_Boolean); - end if; + Add_Contract_Item (N, Obj_Id); - -- Chain the pragma on the contract for further processing - -- by Analyze_External_Property_In_Decl_Part. + -- Otherwise the external property applies to a constant - Add_Contract_Item (N, Obj_Id); - end if; else Error_Pragma ("pragma % must apply to a volatile object"); end if; @@ -12150,7 +12168,6 @@ package body Sem_Prag is when Pragma_Constant_After_Elaboration => Constant_After_Elaboration : declare - Expr : Node_Id; Obj_Decl : Node_Id; Obj_Id : Entity_Id; @@ -12208,15 +12225,7 @@ package body Sem_Prag is -- Analyze the Boolean expression (if any) if Present (Arg1) then - Expr := Get_Pragma_Arg (Arg1); - - Analyze_And_Resolve (Expr, Standard_Boolean); - - if not Is_OK_Static_Expression (Expr) then - Error_Pragma_Arg - ("expression of pragma % must be static", Expr); - return; - end if; + Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1)); end if; -- Chain the pragma on the contract for completeness @@ -13950,7 +13959,6 @@ package body Sem_Prag is -- the annotation must instantiate itself. when Pragma_Extensions_Visible => Extensions_Visible : declare - Expr : Node_Id; Formal : Entity_Id; Has_OK_Formal : Boolean := False; Spec_Id : Entity_Id; @@ -14043,15 +14051,8 @@ package body Sem_Prag is -- Analyze the Boolean expression (if any) if Present (Arg1) then - Expr := Expression (Get_Argument (N, Spec_Id)); - - Analyze_And_Resolve (Expr, Standard_Boolean); - - if not Is_OK_Static_Expression (Expr) then - Error_Pragma_Arg - ("expression of pragma % must be static", Expr); - return; - end if; + Check_Static_Boolean_Expression + (Expression (Get_Argument (N, Spec_Id))); end if; -- Chain the pragma on the contract for completeness @@ -21486,6 +21487,14 @@ package body Sem_Prag is when Pragma_Volatile => Process_Atomic_Independent_Shared_Volatile; + ------------------------- + -- Volatile_Components -- + ------------------------- + + -- pragma Volatile_Components (array_LOCAL_NAME); + + -- Volatile is handled by the same circuit as Atomic_Components + -------------------------- -- Volatile_Full_Access -- -------------------------- @@ -21496,13 +21505,97 @@ package body Sem_Prag is GNAT_Pragma; Process_Atomic_Independent_Shared_Volatile; - ------------------------- - -- Volatile_Components -- - ------------------------- + ----------------------- + -- Volatile_Function -- + ----------------------- - -- pragma Volatile_Components (array_LOCAL_NAME); + -- pragma Volatile_Function [ (boolean_EXPRESSION) ]; - -- Volatile is handled by the same circuit as Atomic_Components + when Pragma_Volatile_Function => Volatile_Function : declare + Over_Id : Entity_Id; + Spec_Id : Entity_Id; + Subp_Decl : Node_Id; + + begin + GNAT_Pragma; + Check_No_Identifiers; + Check_At_Most_N_Arguments (1); + + Subp_Decl := + Find_Related_Subprogram_Or_Body (N, Do_Checks => True); + + -- Function instantiation + + if Nkind (Subp_Decl) = N_Function_Instantiation then + null; + + -- Generic subprogram + + elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then + null; + + -- Body acts as spec + + elsif Nkind (Subp_Decl) = N_Subprogram_Body + and then No (Corresponding_Spec (Subp_Decl)) + then + null; + + -- Body stub acts as spec + + elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub + and then No (Corresponding_Spec_Of_Stub (Subp_Decl)) + then + null; + + -- Subprogram + + elsif Nkind (Subp_Decl) = N_Subprogram_Declaration then + null; + + else + Pragma_Misplaced; + return; + end if; + + Spec_Id := Corresponding_Spec_Of (Subp_Decl); + Over_Id := Overridden_Operation (Spec_Id); + + -- A pragma that applies to a Ghost entity becomes Ghost for the + -- purposes of legality checks and removal of ignored Ghost code. + + Mark_Pragma_As_Ghost (N, Spec_Id); + + -- A volatile function cannot override a non-volatile function + -- (SPARK RM 7.1.2(15)). Overriding checks are usually performed + -- in New_Overloaded_Entity, however at that point the pragma has + -- not been processed yet. + + if Present (Over_Id) + and then not Is_Volatile_Function (Over_Id) + then + Error_Msg_N + ("incompatible volatile function values in effect", Spec_Id); + + Error_Msg_Sloc := Sloc (Over_Id); + Error_Msg_N + ("\& declared # with Volatile_Function value `False`", + Spec_Id); + + Error_Msg_Sloc := Sloc (Spec_Id); + Error_Msg_N + ("\overridden # with Volatile_Function value `True`", + Spec_Id); + end if; + + -- Analyze the Boolean expression (if any) + + if Present (Arg1) then + Check_Static_Boolean_Expression (Get_Pragma_Arg (Arg1)); + end if; + + Add_Contract_Item (N, Spec_Id); + end Volatile_Function; ---------------------- -- Warning_As_Error -- @@ -26278,6 +26371,33 @@ package body Sem_Prag is and then Nkind (Parent (Parent (N))) = N_Package_Body; end Is_Elaboration_SPARK_Mode; + ----------------------- + -- Is_Enabled_Pragma -- + ----------------------- + + function Is_Enabled_Pragma (Prag : Node_Id) return Boolean is + Arg : Node_Id; + + begin + if Present (Prag) then + Arg := First (Pragma_Argument_Associations (Prag)); + + if Present (Arg) then + return Is_True (Expr_Value (Get_Pragma_Arg (Arg))); + + -- The lack of a Boolean argument automatically enables the pragma + + else + return True; + end if; + + -- The pragma is missing, therefore it is not enabled + + else + return False; + end if; + end Is_Enabled_Pragma; + ----------------------------------------- -- Is_Non_Significant_Pragma_Reference -- ----------------------------------------- @@ -26519,6 +26639,7 @@ package body Sem_Prag is Pragma_Volatile => 0, Pragma_Volatile_Components => 0, Pragma_Volatile_Full_Access => 0, + Pragma_Volatile_Function => 0, Pragma_Warning_As_Error => 0, Pragma_Warnings => 0, Pragma_Weak_External => 0, diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads index 72881a0e01c..cdd3657dfdf 100644 --- a/gcc/ada/sem_prag.ads +++ b/gcc/ada/sem_prag.ads @@ -364,6 +364,23 @@ package Sem_Prag is -- Determine whether pragma SPARK_Mode appears in the statement part of a -- package body. + function Is_Enabled_Pragma (Prag : Node_Id) return Boolean; + -- Determine whether a Boolean-like SPARK pragma Prag is enabled. To be + -- considered enabled, the pragma must either: + -- * Appear without its Boolean expression + -- * The Boolean expression evaluates to "True" + -- + -- Boolean-like SPARK pragmas differ from pure Boolean Ada pragmas in that + -- their optional Boolean expression must be static and cannot benefit from + -- forward references. The following are Boolean-like SPARK pragmas: + -- Async_Readers + -- Async_Writers + -- Constant_After_Elaboration + -- Effective_Reads + -- Effective_Writes + -- Extensions_Visible + -- Volatile_Function + function Is_Non_Significant_Pragma_Reference (N : Node_Id) return Boolean; -- The node N is a node for an entity and the issue is whether the -- occurrence is a reference for the purposes of giving warnings about diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 01b912f459d..5b62aed1ad9 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -4105,22 +4105,11 @@ package body Sem_Res is -- actual to a nested call, since this constitutes a reading of -- the parameter, which is not allowed. - if Is_Entity_Name (A) + if Ada_Version = Ada_83 + and then Is_Entity_Name (A) and then Ekind (Entity (A)) = E_Out_Parameter then - if Ada_Version = Ada_83 then - Error_Msg_N - ("(Ada 83) illegal reading of out parameter", A); - - -- An effectively volatile OUT parameter cannot act as IN or - -- IN OUT actual in a call (SPARK RM 7.1.3(11)). - - elsif SPARK_Mode = On - and then Is_Effectively_Volatile (Entity (A)) - then - Error_Msg_N - ("illegal reading of volatile OUT parameter", A); - end if; + Error_Msg_N ("(Ada 83) illegal reading of out parameter", A); end if; end if; @@ -4472,8 +4461,8 @@ package body Sem_Res is -- temporaries are ignored. if SPARK_Mode = On - and then Is_Effectively_Volatile_Object (A) and then Comes_From_Source (A) + and then Is_Effectively_Volatile_Object (A) then -- An effectively volatile object may act as an actual -- parameter when the corresponding formal is of a non-scalar @@ -6792,7 +6781,7 @@ package body Sem_Res is (Context : Node_Id; Obj_Ref : Node_Id) return Boolean; -- Determine whether node Context denotes a "non-interfering context" - -- (as defined in SPARK RM 7.1.3(13)) where volatile reference Obj_Ref + -- (as defined in SPARK RM 7.1.3(12)) where volatile reference Obj_Ref -- can safely reside. ---------------------------------------- @@ -6851,6 +6840,10 @@ package body Sem_Res is function Within_Procedure_Call (Nod : Node_Id) return Boolean; -- Determine whether an arbitrary node appears in a procedure call + function Within_Volatile_Function (Id : Entity_Id) return Boolean; + -- Determine whether an arbitrary entity appears in a volatile + -- function. + ------------------ -- Within_Check -- ------------------ @@ -6905,6 +6898,32 @@ package body Sem_Res is return False; end Within_Procedure_Call; + ------------------------------ + -- Within_Volatile_Function -- + ------------------------------ + + function Within_Volatile_Function (Id : Entity_Id) return Boolean is + Func_Id : Entity_Id; + + begin + -- Traverse the scope stack looking for a [generic] function + + Func_Id := Id; + while Present (Func_Id) and then Func_Id /= Standard_Standard loop + if Ekind_In (Func_Id, E_Function, E_Generic_Function) then + return Is_Volatile_Function (Func_Id); + end if; + + Func_Id := Scope (Func_Id); + end loop; + + return False; + end Within_Volatile_Function; + + -- Local variables + + Obj_Id : Entity_Id; + -- Start of processing for Is_OK_Volatile_Context begin @@ -6914,14 +6933,26 @@ package body Sem_Res is return True; -- The volatile object is part of the initialization expression of - -- another object. Ensure that the climb of the parent chain came - -- from the expression side and not from the name side. + -- another object. elsif Nkind (Context) = N_Object_Declaration and then Present (Expression (Context)) and then Expression (Context) = Obj_Ref then - return True; + Obj_Id := Defining_Entity (Context); + + -- The volatile object acts as the initialization expression of an + -- extended return statement. This is valid context as long as the + -- function is volatile. + + if Is_Return_Object (Obj_Id) then + return Within_Volatile_Function (Obj_Id); + + -- Otherwise this is a normal object initialization + + else + return True; + end if; -- The volatile object appears as an actual parameter in a call to an -- instance of Unchecked_Conversion whose result is renamed. @@ -6932,6 +6963,15 @@ package body Sem_Res is then return True; + -- The volatile object appears as the expression of a simple return + -- statement that applies to a volatile function. + + elsif Nkind (Context) = N_Simple_Return_Statement + and then Expression (Context) = Obj_Ref + then + return + Within_Volatile_Function (Return_Statement_Entity (Context)); + -- The volatile object appears as the prefix of a name occurring -- in a non-interfering context. @@ -7057,14 +7097,6 @@ package body Sem_Res is then if Ada_Version = Ada_83 then Error_Msg_N ("(Ada 83) illegal reading of out parameter", N); - - -- An effectively volatile OUT parameter cannot be read - -- (SPARK RM 7.1.3(11)). - - elsif SPARK_Mode = On - and then Is_Effectively_Volatile (E) - then - Error_Msg_N ("illegal reading of volatile OUT parameter", N); end if; -- In all other cases, just do the possible static evaluation @@ -7117,7 +7149,7 @@ package body Sem_Res is and then Comes_From_Source (N) then -- The effectively volatile objects appears in a "non-interfering - -- context" as defined in SPARK RM 7.1.3(13). + -- context" as defined in SPARK RM 7.1.3(12). if Is_OK_Volatile_Context (Par, N) then null; @@ -7128,7 +7160,7 @@ package body Sem_Res is else SPARK_Msg_N ("volatile object cannot appear in this context " - & "(SPARK RM 7.1.3(13))", N); + & "(SPARK RM 7.1.3(12))", N); end if; end if; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index d7177b85dc9..27b8f9e5e74 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -375,6 +375,7 @@ package body Sem_Util is -- Postcondition -- Precondition -- Test_Case + -- Volatile_Function elsif Ekind_In (Id, E_Entry, E_Entry_Family) or else Is_Generic_Subprogram (Id) @@ -392,6 +393,11 @@ package body Sem_Util is then Add_Classification; + elsif Prag_Nam = Name_Volatile_Function + and then Ekind_In (Id, E_Function, E_Generic_Function) + then + Add_Classification; + -- The pragma is not a proper contract item else @@ -3146,6 +3152,36 @@ package body Sem_Util is end if; end Check_No_Hidden_State; + ---------------------------------------- + -- Check_Nonvolatile_Function_Profile -- + ---------------------------------------- + + procedure Check_Nonvolatile_Function_Profile (Func_Id : Entity_Id) is + Formal : Entity_Id; + + begin + -- Inspect all formal parameters + + Formal := First_Formal (Func_Id); + while Present (Formal) loop + if Is_Effectively_Volatile (Etype (Formal)) then + Error_Msg_NE + ("nonvolatile function & cannot have a volatile parameter", + Formal, Func_Id); + end if; + + Next_Formal (Formal); + end loop; + + -- Inspect the return type + + if Is_Effectively_Volatile (Etype (Func_Id)) then + Error_Msg_N + ("nonvolatile function & cannot have a volatile return type", + Func_Id); + end if; + end Check_Nonvolatile_Function_Profile; + ------------------------------------------ -- Check_Potentially_Blocking_Operation -- ------------------------------------------ @@ -8577,18 +8613,18 @@ package body Sem_Util is ---------------- function Is_Enabled (Prag : Node_Id) return Boolean is - Arg2 : Node_Id; + Arg1 : Node_Id; begin if Present (Prag) then - Arg2 := Next (First (Pragma_Argument_Associations (Prag))); + Arg1 := First (Pragma_Argument_Associations (Prag)); -- The pragma has an optional Boolean expression, the related -- property is enabled only when the expression evaluates to -- True. - if Present (Arg2) then - return Is_True (Expr_Value (Get_Pragma_Arg (Arg2))); + if Present (Arg1) then + return Is_True (Expr_Value (Get_Pragma_Arg (Arg1))); -- Otherwise the lack of expression enables the property by -- default. @@ -11358,6 +11394,66 @@ package body Sem_Util is ----------------------------- function Is_Effectively_Volatile (Id : Entity_Id) return Boolean is + function Is_Descendant_Of_Suspension_Object + (Typ : Entity_Id) return Boolean; + -- Determine whether type Typ is a descendant of type Suspension_Object + -- defined in Ada.Synchronous_Task_Control. This routine is similar to + -- Sem_Util.Is_Descendent_Of, however this version does not load unit + -- Ada.Synchronous_Task_Control. + + ---------------------------------------- + -- Is_Descendant_Of_Suspension_Object -- + ---------------------------------------- + + function Is_Descendant_Of_Suspension_Object + (Typ : Entity_Id) return Boolean + is + Cur_Typ : Entity_Id; + Par_Typ : Entity_Id; + + begin + -- Do not attempt to load Ada.Synchronous_Task_Control in No_Run_Time + -- mode. The unit contains tagged types and those are not allowed in + -- this mode. + + if No_Run_Time_Mode then + return False; + + -- Unit Ada.Synchronous_Task_Control is not available, the type + -- cannot possibly be a descendant of Suspension_Object. + + elsif not RTE_Available (RE_Suspension_Object) then + return False; + end if; + + -- Climb the type derivation chain checking each parent type against + -- Suspension_Object. + + Cur_Typ := Base_Type (Typ); + while Present (Cur_Typ) loop + Par_Typ := Etype (Cur_Typ); + + -- The current type is a match + + if Is_RTE (Cur_Typ, RE_Suspension_Object) then + return True; + + -- Stop the traversal once the root of the derivation chain has + -- been reached. In that case the current type is its own base + -- type. + + elsif Cur_Typ = Par_Typ then + exit; + end if; + + Cur_Typ := Base_Type (Par_Typ); + end loop; + + return False; + end Is_Descendant_Of_Suspension_Object; + + -- Start of processing for Is_Effectively_Volatile + begin if Is_Type (Id) then @@ -11377,6 +11473,19 @@ package body Sem_Util is or else Is_Effectively_Volatile (Component_Type (Base_Type (Id))); + -- A protected type is always volatile + + elsif Is_Protected_Type (Id) then + return True; + + -- A descendant of Ada.Synchronous_Task_Control.Suspension_Object is + -- automatically volatile. + + elsif Is_Descendant_Of_Suspension_Object (Id) then + return True; + + -- Otherwise the type is not effectively volatile + else return False; end if; @@ -13510,6 +13619,33 @@ package body Sem_Util is and then Scope (Scope (Scope (Root))) = Standard_Standard; end Is_Visibly_Controlled; + -------------------------- + -- Is_Volatile_Function -- + -------------------------- + + function Is_Volatile_Function (Func_Id : Entity_Id) return Boolean is + begin + -- The caller must ensure that Func_Id denotes a function + + pragma Assert (Ekind_In (Func_Id, E_Function, E_Generic_Function)); + + -- A protected function is automatically volatile + + if Is_Primitive (Func_Id) + and then Present (First_Formal (Func_Id)) + and then Is_Protected_Type (Etype (First_Formal (Func_Id))) + then + return True; + + -- Otherwise the function is treated as volatile if it is subject to + -- enabled pragma Volatile_Function. + + else + return + Is_Enabled_Pragma (Get_Pragma (Func_Id, Pragma_Volatile_Function)); + end if; + end Is_Volatile_Function; + ------------------------ -- Is_Volatile_Object -- ------------------------ diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 543d31f0fb5..5583aa001da 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -73,6 +73,7 @@ package Sem_Util is -- Refined_Post -- Refined_States -- Test_Case + -- Volatile_Function procedure Add_Global_Declaration (N : Node_Id); -- These procedures adds a declaration N at the library level, to be @@ -313,6 +314,10 @@ package Sem_Util is -- Determine whether object or state Id introduces a hidden state. If this -- is the case, emit an error. + procedure Check_Nonvolatile_Function_Profile (Func_Id : Entity_Id); + -- Verify that the profile of nonvolatile function Func_Id does not contain + -- effectively volatile parameters or return type. + procedure Check_Potentially_Blocking_Operation (N : Node_Id); -- N is one of the statement forms that is a potentially blocking -- operation. If it appears within a protected action, emit warning. @@ -533,7 +538,7 @@ package Sem_Util is function Enclosing_Declaration (N : Node_Id) return Node_Id; -- Returns the declaration node enclosing N (including possibly N itself), - -- if any, or Empty otherwise + -- if any, or Empty otherwise. function Enclosing_Generic_Body (N : Node_Id) return Node_Id; @@ -1285,13 +1290,17 @@ package Sem_Util is -- . machine_emin = 3 - machine_emax function Is_Effectively_Volatile (Id : Entity_Id) return Boolean; - -- The SPARK property "effectively volatile" applies to both types and - -- objects. To qualify as such, an entity must be either volatile or be - -- (of) an array type subject to aspect Volatile_Components. + -- Determine whether a type or object denoted by entity Id is effectively + -- volatile (SPARK RM 7.1.2). To qualify as such, the entity must be either + -- * Volatile + -- * An array type subject to aspect Volatile_Components + -- * An array type whose component type is effectively volatile + -- * A protected type + -- * Descendant of type Ada.Synchronous_Task_Control.Suspension_Object function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean; -- Determine whether an arbitrary node denotes an effectively volatile - -- object. + -- object (SPARK RM 7.1.2). function Is_Expression_Function (Subp : Entity_Id) return Boolean; -- Predicate to determine whether a scope entity comes from a rewritten @@ -1301,8 +1310,8 @@ package Sem_Util is function Is_EVF_Expression (N : Node_Id) return Boolean; -- Determine whether node N denotes a reference to a formal parameter of -- a specific tagged type whose related subprogram is subject to pragma - -- Extensions_Visible with value "False". Several other constructs fall - -- under this category: + -- Extensions_Visible with value "False" (SPARK RM 6.1.7). Several other + -- constructs fall under this category: -- 1) A qualified expression whose operand is EVF -- 2) A type conversion whose operand is EVF -- 3) An if expression with at least one EVF dependent_expression @@ -1550,6 +1559,11 @@ package Sem_Util is -- Initialize/Adjust/Finalize subprogram does not override the inherited -- one. + function Is_Volatile_Function (Func_Id : Entity_Id) return Boolean; + -- Determine whether [generic] function Func_Id is subject to enabled + -- pragma Volatile_Function. Protected functions are treated as volatile + -- (SPARK RM 7.1.2). + function Is_Volatile_Object (N : Node_Id) return Boolean; -- Determines if the given node denotes an volatile object in the sense of -- the legality checks described in RM C.6(12). Note that the test here is diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 94843115c47..d5b06a8677b 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -632,6 +632,7 @@ package Snames is Name_Volatile : constant Name_Id := N + $; Name_Volatile_Components : constant Name_Id := N + $; Name_Volatile_Full_Access : constant Name_Id := N + $; -- GNAT + Name_Volatile_Function : constant Name_Id := N + $; -- GNAT Name_Weak_External : constant Name_Id := N + $; -- GNAT Last_Pragma_Name : constant Name_Id := N + $; @@ -1937,6 +1938,7 @@ package Snames is Pragma_Volatile, Pragma_Volatile_Components, Pragma_Volatile_Full_Access, + Pragma_Volatile_Function, Pragma_Weak_External, -- The following pragmas are on their own, out of order, because of the -- 2.30.2