From: Yannick Moy Date: Tue, 2 Jun 2020 16:24:16 +0000 (+0200) Subject: [Ada] SPARK: update for effectively volatile types and objects X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=476a8ec4d8ecf3437dc3e78e7de2bd77d34fdbd5;p=gcc.git [Ada] SPARK: update for effectively volatile types and objects gcc/ada/ * sem_prag.adb (Analyze_Global_In_Decl_Part): Update check to reject volatile object for reading. * sem_res.adb (Resolve_Actuals, Resolve_Entity_Name): Update check to reject volatile object for reading. * sem_util.adb, sem_util.ads (Check_Nonvolatile_Function_Profile, Has_Effectively_Volatile_Profile): Detect use of volatile object for reading. (Has_Enabled_Property): Accept constants as well. (Is_Effectively_Volatile_For_Reading): New function based on existing Is_Effectively_Volatile. (Is_Effectively_Volatile_Object_For_Reading): Adapted from the existing Is_Effectively_Volatile_Object, using a shared implementation in Is_Effectively_Volatile_Object_Shared. --- diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 38761983508..7442da1c3f2 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2467,10 +2467,11 @@ package body Sem_Prag is elsif SPARK_Mode = On and then Ekind (Item_Id) = E_Variable - and then Is_Effectively_Volatile (Item_Id) + and then Is_Effectively_Volatile_For_Reading (Item_Id) then - -- An effectively volatile object cannot appear as a global - -- item of a nonvolatile function (SPARK RM 7.1.3(8)). + -- An effectively volatile object for reading cannot appear + -- as a global item of a nonvolatile function (SPARK RM + -- 7.1.3(8)). if Ekind (Spec_Id) in E_Function | E_Generic_Function and then not Is_Volatile_Function (Spec_Id) diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index d1d5e3d80b2..de1bee99540 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -3428,7 +3428,7 @@ package body Sem_Res is procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id); -- Emit an error concerning the illegal usage of an effectively volatile - -- object in interfering context (SPARK RM 7.1.3(10)). + -- object for reading in interfering context (SPARK RM 7.1.3(10)). procedure Insert_Default; -- If the actual is missing in a call, insert in the actuals list @@ -3687,7 +3687,7 @@ package body Sem_Res is procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id) is function Flag_Object (N : Node_Id) return Traverse_Result; -- Determine whether arbitrary node N denotes an effectively volatile - -- object and if it does, emit an error. + -- object for reading and if it does, emit an error. ----------------- -- Flag_Object -- @@ -3707,9 +3707,7 @@ package body Sem_Res is Id := Entity (N); if Is_Object (Id) - and then Is_Effectively_Volatile (Id) - and then (Async_Writers_Enabled (Id) - or else Effective_Reads_Enabled (Id)) + and then Is_Effectively_Volatile_For_Reading (Id) then Error_Msg_N ("volatile object cannot appear in this context (SPARK " @@ -4876,17 +4874,17 @@ package body Sem_Res is if SPARK_Mode = On and then Comes_From_Source (A) then - -- An effectively volatile object may act as an actual when the - -- corresponding formal is of a non-scalar effectively volatile - -- type (SPARK RM 7.1.3(10)). + -- An effectively volatile object for reading may act as an + -- actual when the corresponding formal is of a non-scalar + -- effectively volatile type for reading (SPARK RM 7.1.3(10)). if not Is_Scalar_Type (Etype (F)) - and then Is_Effectively_Volatile (Etype (F)) + and then Is_Effectively_Volatile_For_Reading (Etype (F)) then null; - -- An effectively volatile object may act as an actual in a - -- call to an instance of Unchecked_Conversion. + -- An effectively volatile object for reading may act as an + -- actual in a call to an instance of Unchecked_Conversion. -- (SPARK RM 7.1.3(10)). elsif Is_Unchecked_Conversion_Instance (Nam) then @@ -4894,18 +4892,18 @@ package body Sem_Res is -- The actual denotes an object - elsif Is_Effectively_Volatile_Object (A) then + elsif Is_Effectively_Volatile_Object_For_Reading (A) then Error_Msg_N ("volatile object cannot act as actual in a call (SPARK " & "RM 7.1.3(10))", A); -- Otherwise the actual denotes an expression. Inspect the - -- expression and flag each effectively volatile object with - -- enabled property Async_Writers or Effective_Reads as illegal - -- because it apprears within an interfering context. Note that - -- this is usually done in Resolve_Entity_Name, but when the - -- effectively volatile object appears as an actual in a call, - -- the call must be resolved first. + -- expression and flag each effectively volatile object + -- for reading as illegal because it apprears within an + -- interfering context. Note that this is usually done in + -- Resolve_Entity_Name, but when the effectively volatile + -- object for reading appears as an actual in a call, the + -- call must be resolved first. else Flag_Effectively_Volatile_Objects (A); @@ -4923,7 +4921,7 @@ package body Sem_Res is A_Id := Entity (A); if Ekind (A_Id) = E_Variable - and then Is_Effectively_Volatile (Etype (A_Id)) + and then Is_Effectively_Volatile_For_Reading (Etype (A_Id)) and then Effective_Reads_Enabled (A_Id) then Error_Msg_NE @@ -7770,14 +7768,11 @@ package body Sem_Res is if SPARK_Mode = On then - -- An effectively volatile object subject to enabled properties - -- Async_Writers or Effective_Reads must appear in non-interfering - -- context (SPARK RM 7.1.3(10)). + -- An effectively volatile object for reading must appear in + -- non-interfering context (SPARK RM 7.1.3(10)). if Is_Object (E) - and then Is_Effectively_Volatile (E) - and then (Async_Writers_Enabled (E) - or else Effective_Reads_Enabled (E)) + and then Is_Effectively_Volatile_For_Reading (E) and then not Is_OK_Volatile_Context (Par, N) then SPARK_Msg_N diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 2b92caddafa..9b67a45b6e9 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -127,6 +127,15 @@ package body Sem_Util is -- Determine whether arbitrary entity Id denotes an atomic object as per -- RM C.6(7). + generic + with function Is_Effectively_Volatile_Entity + (Id : Entity_Id) return Boolean; + -- Function to use on object and type entities + function Is_Effectively_Volatile_Object_Shared + (N : Node_Id) return Boolean; + -- Shared function used to detect effectively volatile objects and + -- effectively volatile objects for reading. + function Is_Fully_Initialized_Variant (Typ : Entity_Id) return Boolean; -- Subsidiary to Is_Fully_Initialized_Type. For an unconstrained type -- with discriminants whose default values are static, examine only the @@ -3626,7 +3635,7 @@ package body Sem_Util is Formal := First_Formal (Func_Id); while Present (Formal) loop - if Is_Effectively_Volatile (Etype (Formal)) then + if Is_Effectively_Volatile_For_Reading (Etype (Formal)) then Error_Msg_NE ("nonvolatile function & cannot have a volatile parameter", Formal, Func_Id); @@ -3637,7 +3646,7 @@ package body Sem_Util is -- Inspect the return type - if Is_Effectively_Volatile (Etype (Func_Id)) then + if Is_Effectively_Volatile_For_Reading (Etype (Func_Id)) then Error_Msg_NE ("nonvolatile function & cannot have a volatile return type", Result_Definition (Parent (Func_Id)), Func_Id); @@ -11222,11 +11231,11 @@ package body Sem_Util is begin -- Inspect the formal parameters looking for an effectively volatile - -- type. + -- type for reading. Formal := First_Formal (Subp_Id); while Present (Formal) loop - if Is_Effectively_Volatile (Etype (Formal)) then + if Is_Effectively_Volatile_For_Reading (Etype (Formal)) then return True; end if; @@ -11236,7 +11245,7 @@ package body Sem_Util is -- Inspect the return type of functions if Ekind (Subp_Id) in E_Function | E_Generic_Function - and then Is_Effectively_Volatile (Etype (Subp_Id)) + and then Is_Effectively_Volatile_For_Reading (Etype (Subp_Id)) then return True; end if; @@ -11610,7 +11619,7 @@ package body Sem_Util is if Ekind (Item_Id) = E_Abstract_State then return State_Has_Enabled_Property; - elsif Ekind (Item_Id) = E_Variable then + elsif Ekind (Item_Id) in E_Variable | E_Constant then return Type_Or_Variable_Has_Enabled_Property (Item_Id); -- Other objects can only inherit properties through their type. We @@ -15747,35 +15756,115 @@ package body Sem_Util is end if; end Is_Effectively_Volatile; + ----------------------------------------- + -- Is_Effectively_Volatile_For_Reading -- + ----------------------------------------- + + function Is_Effectively_Volatile_For_Reading + (Id : Entity_Id) return Boolean + is + begin + -- A concurrent type is effectively volatile for reading + + if Is_Concurrent_Type (Id) then + return True; + + elsif Is_Effectively_Volatile (Id) then + + -- Other volatile types and objects are effectively volatile for + -- reading when they have property Async_Writers or Effective_Reads + -- set to True. This includes the case of an array type whose + -- Volatile_Components aspect is True (hence it is effectively + -- volatile) which does not have the properties Async_Writers + -- and Effective_Reads set to False. + + if Async_Writers_Enabled (Id) + or else Effective_Reads_Enabled (Id) + then + return True; + + -- In addition, an array type is effectively volatile for reading + -- when its component type is effectively volatile for reading. + + elsif Is_Array_Type (Id) then + declare + Anc : Entity_Id := Base_Type (Id); + begin + if Is_Private_Type (Anc) then + Anc := Full_View (Anc); + end if; + + -- Test for presence of ancestor, as the full view of a + -- private type may be missing in case of error. + + return + Present (Anc) + and then Is_Effectively_Volatile_For_Reading + (Component_Type (Anc)); + end; + end if; + end if; + + return False; + + end Is_Effectively_Volatile_For_Reading; + ------------------------------------ -- Is_Effectively_Volatile_Object -- ------------------------------------ function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean is + function Is_Effectively_Volatile_Object_Inst + is new Is_Effectively_Volatile_Object_Shared (Is_Effectively_Volatile); + begin + return Is_Effectively_Volatile_Object_Inst (N); + end Is_Effectively_Volatile_Object; + + ------------------------------------------------ + -- Is_Effectively_Volatile_Object_For_Reading -- + ------------------------------------------------ + + function Is_Effectively_Volatile_Object_For_Reading + (N : Node_Id) return Boolean + is + function Is_Effectively_Volatile_Object_For_Reading_Inst + is new Is_Effectively_Volatile_Object_Shared + (Is_Effectively_Volatile_For_Reading); + begin + return Is_Effectively_Volatile_Object_For_Reading_Inst (N); + end Is_Effectively_Volatile_Object_For_Reading; + + ------------------------------------------- + -- Is_Effectively_Volatile_Object_Shared -- + ------------------------------------------- + + function Is_Effectively_Volatile_Object_Shared + (N : Node_Id) return Boolean + is begin if Is_Entity_Name (N) then return Is_Object (Entity (N)) - and then Is_Effectively_Volatile (Entity (N)); + and then Is_Effectively_Volatile_Entity (Entity (N)); elsif Nkind (N) in N_Indexed_Component | N_Slice then - return Is_Effectively_Volatile_Object (Prefix (N)); + return Is_Effectively_Volatile_Object_Shared (Prefix (N)); elsif Nkind (N) = N_Selected_Component then return - Is_Effectively_Volatile_Object (Prefix (N)) + Is_Effectively_Volatile_Object_Shared (Prefix (N)) or else - Is_Effectively_Volatile_Object (Selector_Name (N)); + Is_Effectively_Volatile_Object_Shared (Selector_Name (N)); elsif Nkind (N) in N_Qualified_Expression | N_Unchecked_Type_Conversion | N_Type_Conversion then - return Is_Effectively_Volatile_Object (Expression (N)); + return Is_Effectively_Volatile_Object_Shared (Expression (N)); else return False; end if; - end Is_Effectively_Volatile_Object; + end Is_Effectively_Volatile_Object_Shared; ------------------- -- Is_Entry_Body -- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index e2147e04bee..2b18ac28003 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -408,7 +408,7 @@ package Sem_Util is 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. + -- effectively volatile parameters or return type for reading. procedure Check_Part_Of_Reference (Var_Id : Entity_Id; Ref : Node_Id); -- Verify the legality of reference Ref to variable Var_Id when the @@ -1289,7 +1289,8 @@ package Sem_Util is function Has_Effectively_Volatile_Profile (Subp_Id : Entity_Id) return Boolean; -- Determine whether subprogram Subp_Id has an effectively volatile formal - -- parameter or returns an effectively volatile value. + -- parameter for reading or returns an effectively volatile value for + -- reading. function Has_Full_Default_Initialization (Typ : Entity_Id) return Boolean; -- Determine whether type Typ defines "full default initialization" as @@ -1797,10 +1798,30 @@ package Sem_Util is -- * A protected type -- * Descendant of type Ada.Synchronous_Task_Control.Suspension_Object - function Is_Effectively_Volatile_Object (N : Node_Id) return Boolean; + function Is_Effectively_Volatile_For_Reading + (Id : Entity_Id) return Boolean; + -- Determine whether a type or object denoted by entity Id is effectively + -- volatile for reading (SPARK RM 7.1.2). To qualify as such, the entity + -- must be either + -- * Volatile without No_Caching and have Async_Writers or + -- Effective_Reads set to True + -- * An array type subject to aspect Volatile_Components, unless it has + -- Async_Writers and Effective_Reads set to False + -- * An array type whose component type is effectively volatile for + -- reading + -- * 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 (SPARK RM 7.1.2). + function Is_Effectively_Volatile_Object_For_Reading + (N : Node_Id) return Boolean; + -- Determine whether an arbitrary node denotes an effectively volatile + -- object for reading (SPARK RM 7.1.2). + function Is_Entry_Body (Id : Entity_Id) return Boolean; -- Determine whether entity Id is the body entity of an entry [family]