From 4127ebece723b172aeecacbba9b523af98cc646b Mon Sep 17 00:00:00 2001 From: Steve Baird Date: Fri, 31 Jan 2020 11:36:51 -0800 Subject: [PATCH] [Ada] Allow specifying volatility refinement aspects for types 2020-06-11 Steve Baird gcc/ada/ * contracts.adb (Add_Contract_Item): Support specifying volatility refinement aspects for types. (Analyze_Contracts): Add call to Analyze_Type_Contract in the case of a contract for a type. (Freeze_Contracts): Add call to Analyze_Type_Contract in the case of a contract for a type. (Check_Type_Or_Object_External_Properties): A new procedure which performs the work that needs to be done for both object declarations and types. (Analyze_Object_Contract): Add a call to Check_Type_Or_Object_External_Properties and remove the code in this procedure which did much of the work that is now performed by that call. (Analyze_Type_Contract): Implement this new routine as nothing more than a call to Check_Type_Or_Object_External_Properties. * contracts.ads: Update comment for Add_Contract_To_Item because types can have contracts. Follow (questionable) precedent and declare new routine Analyze_Type_Contract as visible (following example of Analyze_Object_Contract), despite the fact that it is never called from outside of the package where it is declared. * einfo.adb (Contract, Set_Contract): Id argument can be a type; support this case. (Write_Field34_Name): Field name is "contract" for a type. * einfo.ads: Update comment describing Contract attribute. * sem_ch3.adb (Build_Derived_Numeric_Type): Is_Volatile should return same answer for all subtypes of a given type. Thus, when building the base type for something like type Volatile_1_To_10 is range 1 .. 10 with Volatile; that basetype should be marked as being volatile. (Access_Type_Declaration): Add SPARK-specific legality check that the designated type of an access type shall be compatible with respect to volatility with the access type. * sem_ch12.adb (Check_Shared_Variable_Control_Aspects): Add SPARK-specific legality check that an actual type parameter in an instantiation shall be compatible with respect to volatility with the corresponding formal type. * sem_ch13.adb (Analyze_Aspect_Specifications): Perform checks for aspect specs for the 4 volatility refinement aspects that were already being performed for all language-defined aspects. * sem_prag.adb (Analyze_External_Property_In_Decl_Part, Analyze_Pragma): External properties (other than No_Caching) may be specified for a type, including a generic formal type. * sem_util.ads: Declare new subprograms - Async_Readers_Enabled, Async_Writers_Enabled, Effective_Reads, Effective_Writes, and Check_Volatility_Compatibility. * sem_util.adb (Async_Readers_Enabled, Async_Writers_Enabled, Effective_Reads, Effective_Writes): Initial implementation of new functions for querying aspect values. (Check_Volatility_Compatibility): New procedure intended for use in checking all SPARK legality rules of the form "<> shall be compatible with respect to volatility with <>". (Has_Enabled_Property): Update comment because Item_Id can be a type. Change name of nested Variable_Has_Enabled_Property function to Type_Or_Variable_Has_Enabled_Property; add a parameter to that function because recursion may be needed, e.g., in the case of a derived typ). Cope with the case where the argument to Has_Enabled_Property is a type. --- gcc/ada/contracts.adb | 391 +++++++++++++++++++++++++++++++++++++------------- gcc/ada/contracts.ads | 17 ++- gcc/ada/einfo.adb | 9 +- gcc/ada/einfo.ads | 6 +- gcc/ada/sem_ch12.adb | 47 ++++++ gcc/ada/sem_ch13.adb | 11 +- gcc/ada/sem_ch3.adb | 21 +++ gcc/ada/sem_prag.adb | 67 ++++++--- gcc/ada/sem_util.adb | 229 +++++++++++++++++++++++------ gcc/ada/sem_util.ads | 33 +++-- 10 files changed, 647 insertions(+), 184 deletions(-) diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 79078df..42f36d5 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -61,6 +61,11 @@ package body Contracts is -- -- Part_Of + procedure Check_Type_Or_Object_External_Properties + (Type_Or_Obj_Id : Entity_Id); + -- Perform checking of external properties pragmas that is common to both + -- type declarations and object declarations. + procedure Expand_Subprogram_Contract (Body_Id : Entity_Id); -- Expand the contracts of a subprogram body and its correspoding spec (if -- any). This routine processes all [refined] pre- and postconditions as @@ -244,18 +249,33 @@ package body Contracts is raise Program_Error; end if; - -- Protected units, the applicable pragmas are: - -- Part_Of - - elsif Ekind (Id) = E_Protected_Type then - if Prag_Nam = Name_Part_Of then - Add_Classification; + -- The four volatility refinement pragmas are ok for all types. + -- Part_Of is ok for task types and protected types. + -- Depends and Global are ok for task types. + + elsif Is_Type (Id) then + declare + Is_OK : constant Boolean := + Nam_In (Prag_Nam, Name_Async_Readers, + Name_Async_Writers, + Name_Effective_Reads, + Name_Effective_Writes) + or else (Ekind (Id) = E_Task_Type + and Nam_In (Prag_Nam, Name_Part_Of, + Name_Depends, + Name_Global)) + or else (Ekind (Id) = E_Protected_Type + and Prag_Nam = Name_Part_Of); + begin + if Is_OK then + Add_Classification; + else - -- The pragma is not a proper contract item + -- The pragma is not a proper contract item - else - raise Program_Error; - end if; + raise Program_Error; + end if; + end; -- Subprogram bodies, the applicable pragmas are: -- Postcondition @@ -299,16 +319,6 @@ package body Contracts is -- Global -- Part_Of - elsif Ekind (Id) = E_Task_Type then - if Nam_In (Prag_Nam, Name_Depends, Name_Global, Name_Part_Of) then - Add_Classification; - - -- The pragma is not a proper contract item - - else - raise Program_Error; - end if; - -- Variables, the applicable pragmas are: -- Async_Readers -- Async_Writers @@ -338,6 +348,9 @@ package body Contracts is else raise Program_Error; end if; + + else + raise Program_Error; end if; end Add_Contract_Item; @@ -430,6 +443,15 @@ package body Contracts is end; end if; + if Nkind_In (Decl, N_Full_Type_Declaration, + N_Private_Type_Declaration, + N_Task_Type_Declaration, + N_Protected_Type_Declaration, + N_Formal_Type_Declaration) + then + Analyze_Type_Contract (Defining_Identifier (Decl)); + end if; + Next (Decl); end loop; end Analyze_Contracts; @@ -720,6 +742,233 @@ package body Contracts is end if; end Analyze_Entry_Or_Subprogram_Contract; + ---------------------------------------------- + -- Check_Type_Or_Object_External_Properties -- + ---------------------------------------------- + + procedure Check_Type_Or_Object_External_Properties + (Type_Or_Obj_Id : Entity_Id) + is + function Decl_Kind (Is_Type : Boolean; + Object_Kind : String) return String; + -- Returns "type" or Object_Kind, depending on Is_Type + + --------------- + -- Decl_Kind -- + --------------- + + function Decl_Kind (Is_Type : Boolean; + Object_Kind : String) return String is + begin + if Is_Type then + return "type"; + else + return Object_Kind; + end if; + end Decl_Kind; + + Is_Type_Id : constant Boolean := Is_Type (Type_Or_Obj_Id); + + -- Local variables + + AR_Val : Boolean := False; + AW_Val : Boolean := False; + ER_Val : Boolean := False; + EW_Val : Boolean := False; + Seen : Boolean := False; + Prag : Node_Id; + Obj_Typ : Entity_Id; + + -- Start of processing for Check_Type_Or_Object_External_Properties + + begin + -- Analyze all external properties + + if Is_Type_Id then + Obj_Typ := Type_Or_Obj_Id; + + -- If the parent type of a derived type is volatile + -- then the derived type inherits volatility-related flags. + + if Is_Derived_Type (Type_Or_Obj_Id) then + declare + Parent_Type : constant Entity_Id := + Etype (Base_Type (Type_Or_Obj_Id)); + begin + if Is_Effectively_Volatile (Parent_Type) then + AR_Val := Async_Readers_Enabled (Parent_Type); + AW_Val := Async_Writers_Enabled (Parent_Type); + ER_Val := Effective_Reads_Enabled (Parent_Type); + EW_Val := Effective_Writes_Enabled (Parent_Type); + end if; + end; + end if; + else + Obj_Typ := Etype (Type_Or_Obj_Id); + end if; + + Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Readers); + + if Present (Prag) then + declare + Saved_AR_Val : constant Boolean := AR_Val; + begin + Analyze_External_Property_In_Decl_Part (Prag, AR_Val); + Seen := True; + if Saved_AR_Val and not AR_Val then + Error_Msg_N + ("illegal non-confirming Async_Readers specification", + Prag); + end if; + end; + end if; + + Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Writers); + + if Present (Prag) then + declare + Saved_AW_Val : constant Boolean := AW_Val; + begin + Analyze_External_Property_In_Decl_Part (Prag, AW_Val); + Seen := True; + if Saved_AW_Val and not AW_Val then + Error_Msg_N + ("illegal non-confirming Async_Writers specification", + Prag); + end if; + end; + end if; + + Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Reads); + + if Present (Prag) then + declare + Saved_ER_Val : constant Boolean := ER_Val; + begin + Analyze_External_Property_In_Decl_Part (Prag, ER_Val); + Seen := True; + if Saved_ER_Val and not ER_Val then + Error_Msg_N + ("illegal non-confirming Effective_Reads specification", + Prag); + end if; + end; + end if; + + Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Effective_Writes); + + if Present (Prag) then + declare + Saved_EW_Val : constant Boolean := EW_Val; + begin + Analyze_External_Property_In_Decl_Part (Prag, EW_Val); + Seen := True; + if Saved_EW_Val and not EW_Val then + Error_Msg_N + ("illegal non-confirming Effective_Writes specification", + Prag); + end if; + end; + end if; + + -- Verify the mutual interaction of the various external properties + + if Seen then + Check_External_Properties + (Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); + end if; + + -- The following checks are relevant only when SPARK_Mode is on, as + -- they are not standard Ada legality rules. Internally generated + -- temporaries are ignored. + + if SPARK_Mode = On and then Comes_From_Source (Type_Or_Obj_Id) then + if Is_Effectively_Volatile (Type_Or_Obj_Id) then + + -- The declaration of an effectively volatile object or type must + -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)). + + if not Is_Library_Level_Entity (Type_Or_Obj_Id) then + Error_Msg_N + ("effectively volatile " + & Decl_Kind (Is_Type => Is_Type_Id, + Object_Kind => "variable") + & " & must be declared at library level " + & "(SPARK RM 7.1.3(3))", Type_Or_Obj_Id); + + -- An object of a discriminated type cannot be effectively + -- volatile except for protected objects (SPARK RM 7.1.3(5)). + + elsif Has_Discriminants (Obj_Typ) + and then not Is_Protected_Type (Obj_Typ) + then + Error_Msg_N + ("discriminated " + & Decl_Kind (Is_Type => Is_Type_Id, + Object_Kind => "object") + & " & cannot be volatile", + Type_Or_Obj_Id); + end if; + + -- An object decl shall be compatible with respect to volatility + -- with its type (SPARK RM 7.1.3(2)). + + if not Is_Type_Id then + if Is_Effectively_Volatile (Obj_Typ) then + Check_Volatility_Compatibility + (Type_Or_Obj_Id, Obj_Typ, + "volatile object", "its type", + Srcpos_Bearer => Type_Or_Obj_Id); + end if; + + -- A component of a composite type (in this case, the composite + -- type is an array type) shall be compatible with respect to + -- volatility with the composite type (SPARK RM 7.1.3(6)). + + elsif Is_Array_Type (Obj_Typ) then + Check_Volatility_Compatibility + (Component_Type (Obj_Typ), Obj_Typ, + "component type", "its enclosing array type", + Srcpos_Bearer => Obj_Typ); + + -- A component of a composite type (in this case, the composite + -- type is a record type) shall be compatible with respect to + -- volatility with the composite type (SPARK RM 7.1.3(6)). + + elsif Is_Record_Type (Obj_Typ) then + declare + Comp : Entity_Id := First_Component (Obj_Typ); + begin + while Present (Comp) loop + Check_Volatility_Compatibility + (Etype (Comp), Obj_Typ, + "record component " & Get_Name_String (Chars (Comp)), + "its enclosing record type", + Srcpos_Bearer => Comp); + Next_Component (Comp); + end loop; + end; + end if; + + -- The type or object is not effectively volatile + + else + -- A non-effectively volatile type cannot have effectively + -- volatile components (SPARK RM 7.1.3(6)). + + if Is_Type_Id + and then not Is_Effectively_Volatile (Type_Or_Obj_Id) + and then Has_Volatile_Component (Type_Or_Obj_Id) + then + Error_Msg_N + ("non-volatile type & cannot have volatile" + & " components", + Type_Or_Obj_Id); + end if; + end if; + end if; + end Check_Type_Or_Object_External_Properties; + ----------------------------- -- Analyze_Object_Contract -- ----------------------------- @@ -738,15 +987,10 @@ package body Contracts is Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; -- Save the SPARK_Mode-related data to restore on exit - AR_Val : Boolean := False; - AW_Val : Boolean := False; - ER_Val : Boolean := False; - EW_Val : Boolean := False; NC_Val : Boolean := False; Items : Node_Id; Prag : Node_Id; Ref_Elmt : Elmt_Id; - Seen : Boolean := False; begin -- The loop parameter in an element iterator over a formal container @@ -813,41 +1057,8 @@ package body Contracts is else pragma Assert (Ekind (Obj_Id) = E_Variable); - -- Analyze all external properties - - Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers); - - if Present (Prag) then - Analyze_External_Property_In_Decl_Part (Prag, AR_Val); - Seen := True; - end if; - - Prag := Get_Pragma (Obj_Id, Pragma_Async_Writers); - - if Present (Prag) then - Analyze_External_Property_In_Decl_Part (Prag, AW_Val); - Seen := True; - end if; - - Prag := Get_Pragma (Obj_Id, Pragma_Effective_Reads); - - if Present (Prag) then - Analyze_External_Property_In_Decl_Part (Prag, ER_Val); - Seen := True; - end if; - - Prag := Get_Pragma (Obj_Id, Pragma_Effective_Writes); - - if Present (Prag) then - Analyze_External_Property_In_Decl_Part (Prag, EW_Val); - Seen := True; - end if; - - -- Verify the mutual interaction of the various external properties - - if Seen then - Check_External_Properties (Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); - end if; + Check_Type_Or_Object_External_Properties + (Type_Or_Obj_Id => Obj_Id); -- Analyze the non-external volatility property No_Caching @@ -911,47 +1122,6 @@ package body Contracts is else Check_Missing_Part_Of (Obj_Id); end if; - - -- The following checks are relevant only when SPARK_Mode is on, as - -- they are not standard Ada legality rules. Internally generated - -- temporaries are ignored. - - if SPARK_Mode = On and then Comes_From_Source (Obj_Id) then - 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(3), C.6(6)). - - if not Is_Library_Level_Entity (Obj_Id) then - Error_Msg_N - ("volatile variable & must be declared at library level " - & "(SPARK RM 7.1.3(3))", Obj_Id); - - -- An object of a discriminated type cannot be effectively - -- volatile except for protected objects (SPARK RM 7.1.3(5)). - - elsif Has_Discriminants (Obj_Typ) - and then not Is_Protected_Type (Obj_Typ) - then - Error_Msg_N - ("discriminated object & cannot be volatile", Obj_Id); - end if; - - -- The object is not effectively volatile - - else - -- A non-effectively volatile object cannot have effectively - -- volatile components (SPARK RM 7.1.3(6)). - - if not Is_Effectively_Volatile (Obj_Id) - and then Has_Volatile_Component (Obj_Typ) - then - Error_Msg_N - ("non-volatile object & cannot have volatile components", - Obj_Id); - end if; - end if; - end if; end if; -- Common checks @@ -1304,6 +1474,16 @@ package body Contracts is Restore_SPARK_Mode (Saved_SM, Saved_SMP); end Analyze_Task_Contract; + --------------------------- + -- Analyze_Type_Contract -- + --------------------------- + + procedure Analyze_Type_Contract (Type_Id : Entity_Id) is + begin + Check_Type_Or_Object_External_Properties + (Type_Or_Obj_Id => Type_Id); + end Analyze_Type_Contract; + ----------------------------- -- Create_Generic_Contract -- ----------------------------- @@ -2757,6 +2937,15 @@ package body Contracts is Analyze_Task_Contract (Defining_Entity (Decl)); end if; + if Nkind_In (Decl, N_Full_Type_Declaration, + N_Private_Type_Declaration, + N_Task_Type_Declaration, + N_Protected_Type_Declaration, + N_Formal_Type_Declaration) + then + Analyze_Type_Contract (Defining_Identifier (Decl)); + end if; + Prev (Decl); end loop; end Freeze_Contracts; diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads index a41285f..9e7b955 100644 --- a/gcc/ada/contracts.ads +++ b/gcc/ada/contracts.ads @@ -33,8 +33,8 @@ package Contracts is procedure Add_Contract_Item (Prag : Node_Id; Id : Entity_Id); -- Add pragma Prag to the contract of a constant, entry, entry family, -- [generic] package, package body, protected unit, [generic] subprogram, - -- subprogram body, variable or task unit denoted by Id. The following are - -- valid pragmas: + -- subprogram body, variable, task unit, or type denoted by Id. + -- The following are valid pragmas: -- -- Abstract_State -- Async_Readers @@ -114,6 +114,19 @@ package Contracts is -- Freeze_Id is the entity of a [generic] package body or a [generic] -- subprogram body which "freezes" the contract of Obj_Id. + procedure Analyze_Type_Contract (Type_Id : Entity_Id); + -- Analyze all delayed pragmas chained on the contract of object Obj_Id as + -- if they appeared at the end of the declarative region. The pragmas to be + -- considered are: + -- + -- Async_Readers + -- Async_Writers + -- Effective_Reads + -- Effective_Writes + -- + -- In the case of a protected or task type, there will also be + -- a call to Analyze_Protected_Contract or Analyze_Task_Contract. + procedure Analyze_Package_Body_Contract (Body_Id : Entity_Id; Freeze_Id : Entity_Id := Empty); diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index ee1aecb..83beff6 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -1291,6 +1291,8 @@ package body Einfo is E_Package, E_Package_Body) or else + Is_Type (Id) -- types + or else Ekind (Id) = E_Void); -- special purpose return Node34 (Id); end Contract; @@ -4146,6 +4148,10 @@ package body Einfo is Ekind_In (Id, E_Generic_Package, -- packages E_Package, E_Package_Body) + + or else + Is_Type (Id) -- types + or else Ekind (Id) = E_Void); -- special purpose Set_Node34 (Id, V); @@ -11271,11 +11277,10 @@ package body Einfo is | E_Package | E_Package_Body | E_Procedure - | E_Protected_Type | E_Subprogram_Body | E_Task_Body - | E_Task_Type | E_Variable + | Type_Kind | E_Void => Write_Str ("Contract"); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index e28fcd0..75474cd 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -744,9 +744,9 @@ package Einfo is -- Contract (Node34) -- Defined in constant, entry, entry family, operator, [generic] package, --- package body, protected type, [generic] subprogram, subprogram body, --- variable and task type entities. Points to the contract of the entity, --- holding various assertion items and data classifiers. +-- package body, protected unit, [generic] subprogram, subprogram body, +-- variable, task unit, and type entities. Points to the contract of the +-- entity, holding various assertion items and data classifiers. -- Contract_Wrapper (Node25) -- Defined in entry and entry family entities. Set only when the entry diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 93a3ca5..e366531 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -11315,6 +11315,44 @@ package body Sem_Ch12 is Actual); end if; + -- Check actual/formal compatibility with respect to the four + -- volatility refinement aspects. + + declare + Actual_Obj : Entity_Id; + N : Node_Id := Actual; + begin + -- Similar to Sem_Util.Get_Enclosing_Object, but treat + -- pointer dereference like component selection. + loop + if Is_Entity_Name (N) then + Actual_Obj := Entity (N); + exit; + end if; + + case Nkind (N) is + when N_Indexed_Component + | N_Selected_Component + | N_Slice + | N_Explicit_Dereference + => + N := Prefix (N); + + when N_Type_Conversion => + N := Expression (N); + + when others => + Actual_Obj := Etype (N); + exit; + end case; + end loop; + + Check_Volatility_Compatibility + (Actual_Obj, A_Gen_Obj, "actual object", + "its corresponding formal object of mode in out", + Srcpos_Bearer => Actual); + end; + -- Formal in-parameter else @@ -11510,6 +11548,7 @@ package body Sem_Ch12 is and then Present (Actual) and then Is_Object_Reference (Actual) and then Is_Effectively_Volatile_Object (Actual) + and then not Is_Effectively_Volatile (A_Gen_Obj) then Error_Msg_N ("volatile object cannot act as actual in generic instantiation", @@ -12480,6 +12519,14 @@ package body Sem_Ch12 is ("actual for& must have Independent_Components specified", Actual, A_Gen_T); end if; + + -- Check actual/formal compatibility with respect to the four + -- volatility refinement aspects. + + Check_Volatility_Compatibility + (Act_T, A_Gen_T, + "actual type", "its corresponding formal type", + Srcpos_Bearer => Act_T); end if; end Check_Shared_Variable_Control_Aspects; diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index f73b55a..4b042d8 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -2180,7 +2180,12 @@ package body Sem_Ch13 is -- Check some general restrictions on language defined aspects - if not Implementation_Defined_Aspect (A_Id) then + if not Implementation_Defined_Aspect (A_Id) + or else 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_Reads + then Error_Msg_Name_1 := Nam; -- Not allowed for renaming declarations. Examine the original @@ -2209,6 +2214,10 @@ package body Sem_Ch13 is and then A_Id /= Aspect_Atomic_Components and then A_Id /= Aspect_Independent_Components and then A_Id /= Aspect_Volatile_Components + and then A_Id /= Aspect_Async_Readers + and then A_Id /= Aspect_Async_Writers + and then A_Id /= Aspect_Effective_Reads + and then A_Id /= Aspect_Effective_Reads then Error_Msg_N ("aspect % not allowed for formal type declaration", diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index ccb0ea9..f38d6e7 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -1398,6 +1398,26 @@ package body Sem_Ch3 is Set_Is_Tagged_Type (T, False); end if; + -- For SPARK, check that the designated type is compatible with + -- respect to volatility with the access type. + + if SPARK_Mode /= Off + and then Comes_From_Source (T) + then + -- ??? UNIMPLEMENTED + -- In the case where the designated type is incomplete at this point, + -- performing this check here is harmless but the check will need to + -- be repeated when the designated type is complete. + + -- The preceding call to Comes_From_Source is needed because the + -- FE sometimes introduces implicitly declared access types. See, + -- for example, the expansion of nested_po.ads in OA28-015. + + Check_Volatility_Compatibility + (Full_Desig, T, "designated type", "access type", + Srcpos_Bearer => T); + end if; + Set_Etype (T, T); -- If the type has appeared already in a with_type clause, it is frozen @@ -7265,6 +7285,7 @@ package body Sem_Ch3 is Set_First_Rep_Item (Implicit_Base, First_Rep_Item (Parent_Base)); Set_Parent (Implicit_Base, Parent (Derived_Type)); Set_Is_Known_Valid (Implicit_Base, Is_Known_Valid (Parent_Base)); + Set_Is_Volatile (Implicit_Base, Is_Volatile (Parent_Base)); -- Set RM Size for discrete type or decimal fixed-point type -- Ordinary fixed-point is excluded, why??? diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index d05b8fe..05171d4 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2123,7 +2123,8 @@ package body Sem_Prag is & """No_Caching"" (SPARK RM 7.1.2(6))", N); else SPARK_Msg_N - ("external property % must apply to a volatile object", N); + ("external property % must apply to a volatile type or object", + N); end if; -- Pragma No_Caching should only apply to volatile variables of @@ -7847,6 +7848,7 @@ package body Sem_Prag is and then Prag_Id = Pragma_Volatile and then not Nkind_In (Original_Node (Decl), N_Full_Type_Declaration, + N_Formal_Type_Declaration, N_Object_Declaration, N_Single_Protected_Declaration, N_Single_Task_Declaration) @@ -13476,41 +13478,65 @@ package body Sem_Prag is | Pragma_No_Caching => Async_Effective : declare - Obj_Decl : Node_Id; - Obj_Id : Entity_Id; - + Obj_Or_Type_Decl : Node_Id; + Obj_Or_Type_Id : Entity_Id; begin GNAT_Pragma; Check_No_Identifiers; Check_At_Most_N_Arguments (1); - Obj_Decl := Find_Related_Context (N, Do_Checks => True); - - -- Object declaration - - if Nkind (Obj_Decl) /= N_Object_Declaration then - Pragma_Misplaced; - return; + Obj_Or_Type_Decl := Find_Related_Context (N, Do_Checks => True); + + -- Pragma must apply to a object declaration or to a type + -- declaration (only the former in the No_Caching case). + -- Original_Node is necessary to account for untagged derived + -- types that are rewritten as subtypes of their + -- respective root types. + + if Nkind (Obj_Or_Type_Decl) /= N_Object_Declaration then + if (Prag_Id = Pragma_No_Caching) + or not Nkind_In (Original_Node (Obj_Or_Type_Decl), + N_Full_Type_Declaration, + N_Private_Type_Declaration, + N_Formal_Type_Declaration, + N_Task_Type_Declaration, + N_Protected_Type_Declaration) + then + Pragma_Misplaced; + return; + end if; end if; - Obj_Id := Defining_Entity (Obj_Decl); + Obj_Or_Type_Id := Defining_Entity (Obj_Or_Type_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. + -- least a variable or a type. Subsequent finer grained checks + -- will be done at the end of the declarative region that + -- contains the pragma. - if Ekind (Obj_Id) = E_Variable then + if Ekind (Obj_Or_Type_Id) = E_Variable or Is_Type (Obj_Or_Type_Id) + then + + -- In the case of a type, pragma is a type-related + -- representation item and so requires checks common to + -- all type-related representation items. + + if Is_Type (Obj_Or_Type_Id) + and then Rep_Item_Too_Late (Obj_Or_Type_Id, N) + then + return; + end if; -- A pragma that applies to a Ghost entity becomes Ghost for -- the purposes of legality checks and removal of ignored Ghost -- code. - Mark_Ghost_Pragma (N, Obj_Id); + Mark_Ghost_Pragma (N, Obj_Or_Type_Id); -- Chain the pragma on the contract for further processing by -- Analyze_External_Property_In_Decl_Part. - Add_Contract_Item (N, Obj_Id); + Add_Contract_Item (N, Obj_Or_Type_Id); -- Analyze the Boolean expression (if any) @@ -13521,7 +13547,8 @@ package body Sem_Prag is -- Otherwise the external property applies to a constant else - Error_Pragma ("pragma % must apply to a volatile object"); + Error_Pragma + ("pragma % must apply to a volatile type or object"); end if; end Async_Effective; @@ -30170,7 +30197,9 @@ package body Sem_Prag is -- Skip internally generated code - elsif not Comes_From_Source (Stmt) then + elsif not Comes_From_Source (Stmt) + and then not Comes_From_Source (Original_Node (Stmt)) + then -- The anonymous object created for a single concurrent type is a -- suitable context. diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index d1c63ab..76eb665 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -116,8 +116,8 @@ package body Sem_Util is (Item_Id : Entity_Id; Property : Name_Id) return Boolean; -- Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled. - -- Determine whether an abstract state or a variable denoted by entity - -- Item_Id has enabled property Property. + -- Determine whether the state abstraction, variable, or type denoted by + -- entity Item_Id has enabled property Property. function Has_Null_Extension (T : Entity_Id) return Boolean; -- T is a derived tagged type. Check whether the type extension is null. @@ -4911,6 +4911,96 @@ package body Sem_Util is end if; end Check_Unused_Body_States; + ------------------------------------ + -- Check_Volatility_Compatibility -- + ------------------------------------ + + procedure Check_Volatility_Compatibility + (Id1, Id2 : Entity_Id; + Description_1, Description_2 : String; + Srcpos_Bearer : Node_Id) is + + begin + if SPARK_Mode /= On then + return; + end if; + + declare + AR1 : constant Boolean := Async_Readers_Enabled (Id1); + AW1 : constant Boolean := Async_Writers_Enabled (Id1); + ER1 : constant Boolean := Effective_Reads_Enabled (Id1); + EW1 : constant Boolean := Effective_Writes_Enabled (Id1); + AR2 : constant Boolean := Async_Readers_Enabled (Id2); + AW2 : constant Boolean := Async_Writers_Enabled (Id2); + ER2 : constant Boolean := Effective_Reads_Enabled (Id2); + EW2 : constant Boolean := Effective_Writes_Enabled (Id2); + + AR_Check_Failed : constant Boolean := AR1 and not AR2; + AW_Check_Failed : constant Boolean := AW1 and not AW2; + ER_Check_Failed : constant Boolean := ER1 and not ER2; + EW_Check_Failed : constant Boolean := EW1 and not EW2; + + package Failure_Description is + procedure Note_If_Failure + (Failed : Boolean; Aspect_Name : String); + -- If Failed is False, do nothing. + -- If Failed is True, add Aspect_Name to the failure description. + + function Failure_Text return String; + -- returns accumulated list of failing aspects + end Failure_Description; + + package body Failure_Description is + Description_Buffer : Bounded_String; + + --------------------- + -- Note_If_Failure -- + --------------------- + + procedure Note_If_Failure + (Failed : Boolean; Aspect_Name : String) is + begin + if Failed then + if Description_Buffer.Length /= 0 then + Append (Description_Buffer, ", "); + end if; + Append (Description_Buffer, Aspect_Name); + end if; + end Note_If_Failure; + + ------------------ + -- Failure_Text -- + ------------------ + + function Failure_Text return String is + begin + return +Description_Buffer; + end Failure_Text; + end Failure_Description; + + use Failure_Description; + begin + if AR_Check_Failed + or AW_Check_Failed + or ER_Check_Failed + or EW_Check_Failed + then + Note_If_Failure (AR_Check_Failed, "Async_Readers"); + Note_If_Failure (AW_Check_Failed, "Async_Writers"); + Note_If_Failure (ER_Check_Failed, "Effective_Reads"); + Note_If_Failure (EW_Check_Failed, "Effective_Writes"); + + Error_Msg_N + (Description_1 + & " and " + & Description_2 + & " are not compatible with respect to volatility due to " + & Failure_Text, + Srcpos_Bearer); + end if; + end; + end Check_Volatility_Compatibility; + ----------------- -- Choice_List -- ----------------- @@ -11036,28 +11126,26 @@ package body Sem_Util is (Item_Id : Entity_Id; Property : Name_Id) return Boolean is - function Protected_Object_Has_Enabled_Property return Boolean; - -- Determine whether a protected object denoted by Item_Id has the - -- property enabled. + function Protected_Type_Or_Variable_Has_Enabled_Property return Boolean; + -- Determine whether a protected type or variable denoted by Item_Id + -- has the property enabled. function State_Has_Enabled_Property return Boolean; -- Determine whether a state denoted by Item_Id has the property enabled - function Variable_Has_Enabled_Property return Boolean; - -- Determine whether a variable denoted by Item_Id has the property - -- enabled. - - ------------------------------------------- - -- Protected_Object_Has_Enabled_Property -- - ------------------------------------------- + function Type_Or_Variable_Has_Enabled_Property + (Item_Id : Entity_Id) return Boolean; + -- Determine whether type or variable denoted by Item_Id has the + -- property enabled. - function Protected_Object_Has_Enabled_Property return Boolean is - Constits : constant Elist_Id := Part_Of_Constituents (Item_Id); - Constit_Elmt : Elmt_Id; - Constit_Id : Entity_Id; + ----------------------------------------------------- + -- Protected_Type_Or_Variable_Has_Enabled_Property -- + ----------------------------------------------------- + function Protected_Type_Or_Variable_Has_Enabled_Property return Boolean + is begin - -- Protected objects always have the properties Async_Readers and + -- Protected entities always have the properties Async_Readers and -- Async_Writers (SPARK RM 7.1.2(16)). if Property = Name_Async_Readers @@ -11069,21 +11157,30 @@ package body Sem_Util is -- properties Effective_Reads and Effective_Writes -- (SPARK RM 7.1.2(16)). - elsif Present (Constits) then - Constit_Elmt := First_Elmt (Constits); - while Present (Constit_Elmt) loop - Constit_Id := Node (Constit_Elmt); + elsif Is_Single_Protected_Object (Item_Id) then + declare + Constit_Elmt : Elmt_Id; + Constit_Id : Entity_Id; + Constits : constant Elist_Id + := Part_Of_Constituents (Item_Id); + begin + if Present (Constits) then + Constit_Elmt := First_Elmt (Constits); + while Present (Constit_Elmt) loop + Constit_Id := Node (Constit_Elmt); + + if Has_Enabled_Property (Constit_Id, Property) then + return True; + end if; - if Has_Enabled_Property (Constit_Id, Property) then - return True; + Next_Elmt (Constit_Elmt); + end loop; end if; - - Next_Elmt (Constit_Elmt); - end loop; + end; end if; return False; - end Protected_Object_Has_Enabled_Property; + end Protected_Type_Or_Variable_Has_Enabled_Property; -------------------------------- -- State_Has_Enabled_Property -- @@ -11245,11 +11342,13 @@ package body Sem_Util is return False; end State_Has_Enabled_Property; - ----------------------------------- - -- Variable_Has_Enabled_Property -- - ----------------------------------- + ------------------------------------------- + -- Type_Or_Variable_Has_Enabled_Property -- + ------------------------------------------- - function Variable_Has_Enabled_Property return Boolean is + function Type_Or_Variable_Has_Enabled_Property + (Item_Id : Entity_Id) return Boolean + is function Is_Enabled (Prag : Node_Id) return Boolean; -- Determine whether property pragma Prag (if present) denotes an -- enabled property. @@ -11297,7 +11396,11 @@ package body Sem_Util is EW : constant Node_Id := Get_Pragma (Item_Id, Pragma_Effective_Writes); - -- Start of processing for Variable_Has_Enabled_Property + Is_Derived_Type_With_Volatile_Parent_Type : constant Boolean := + Is_Derived_Type (Item_Id) + and then Is_Effectively_Volatile (Etype (Base_Type (Item_Id))); + + -- Start of processing for Type_Or_Variable_Has_Enabled_Property begin -- A non-effectively volatile object can never possess external @@ -11312,23 +11415,57 @@ package body Sem_Util is -- property is enabled when the flag evaluates to True or the flag is -- missing altogether. - elsif Property = Name_Async_Readers and then Is_Enabled (AR) then - return True; + elsif Property = Name_Async_Readers and then Present (AR) then + return Is_Enabled (AR); - elsif Property = Name_Async_Writers and then Is_Enabled (AW) then - return True; + elsif Property = Name_Async_Writers and then Present (AW) then + return Is_Enabled (AW); - elsif Property = Name_Effective_Reads and then Is_Enabled (ER) then - return True; + elsif Property = Name_Effective_Reads and then Present (ER) then + return Is_Enabled (ER); - elsif Property = Name_Effective_Writes and then Is_Enabled (EW) then - return True; + elsif Property = Name_Effective_Writes and then Present (EW) then + return Is_Enabled (EW); + + -- If other properties are set explicitly, then this one is set + -- implicitly to False, except in the case of a derived type + -- whose parent type is volatile (in that case, we will inherit + -- from the parent type, below). + + elsif (Present (AR) + or else Present (AW) + or else Present (ER) + or else Present (EW)) + and then not Is_Derived_Type_With_Volatile_Parent_Type + then + return False; + + -- For a private type, may need to look at the full view + + elsif Is_Private_Type (Item_Id) and then Present (Full_View (Item_Id)) + then + return Type_Or_Variable_Has_Enabled_Property (Full_View (Item_Id)); + + -- For a derived type whose parent type is volatile, the + -- property may be inherited (but ignore a non-volatile parent). + + elsif Is_Derived_Type_With_Volatile_Parent_Type then + return Type_Or_Variable_Has_Enabled_Property + (First_Subtype (Etype (Base_Type (Item_Id)))); + + -- If not specified explicitly for an object and the type + -- is effectively volatile, then take result from the type. + + elsif not Is_Type (Item_Id) + and then Is_Effectively_Volatile (Etype (Item_Id)) + then + return Has_Enabled_Property (Etype (Item_Id), Property); -- The implicit case lacks all property pragmas elsif No (AR) and then No (AW) and then No (ER) and then No (EW) then if Is_Protected_Type (Etype (Item_Id)) then - return Protected_Object_Has_Enabled_Property; + return Protected_Type_Or_Variable_Has_Enabled_Property; else return True; end if; @@ -11336,7 +11473,7 @@ package body Sem_Util is else return False; end if; - end Variable_Has_Enabled_Property; + end Type_Or_Variable_Has_Enabled_Property; -- Start of processing for Has_Enabled_Property @@ -11348,7 +11485,11 @@ package body Sem_Util is return State_Has_Enabled_Property; elsif Ekind (Item_Id) = E_Variable then - return Variable_Has_Enabled_Property; + return Type_Or_Variable_Has_Enabled_Property (Item_Id); + + elsif Is_Type (Item_Id) then + return Type_Or_Variable_Has_Enabled_Property + (Item_Id => First_Subtype (Item_Id)); -- By default, protected objects only have the properties Async_Readers -- and Async_Writers. If they have Part_Of components, they also inherit @@ -11356,7 +11497,7 @@ package body Sem_Util is -- (SPARK RM 7.1.2(16)). elsif Ekind (Item_Id) = E_Protected_Object then - return Protected_Object_Has_Enabled_Property; + return Protected_Type_Or_Variable_Has_Enabled_Property; -- Otherwise a property is enabled when the related item is effectively -- volatile. diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 07619fc..74fa2a6 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -157,14 +157,12 @@ package Sem_Util is -- force an error). function Async_Readers_Enabled (Id : Entity_Id) return Boolean; - -- Given the entity of an abstract state or a variable, determine whether - -- Id is subject to external property Async_Readers and if it is, the - -- related expression evaluates to True. + -- Id should be the entity of a state abstraction, a variable, or a type. + -- Returns True iff Id is subject to external property Async_Readers. function Async_Writers_Enabled (Id : Entity_Id) return Boolean; - -- Given the entity of an abstract state or a variable, determine whether - -- Id is subject to external property Async_Writers and if it is, the - -- related expression evaluates to True. + -- Id should be the entity of a state abstraction, a variable, or a type. + -- Returns True iff Id is subject to external property Async_Writers. function Available_Full_View_Of_Component (T : Entity_Id) return Boolean; -- If at the point of declaration an array type has a private or limited @@ -456,6 +454,19 @@ package Sem_Util is -- and the context is external to the protected operation, to warn against -- a possible unlocked access to data. + procedure Check_Volatility_Compatibility + (Id1, Id2 : Entity_Id; + Description_1, Description_2 : String; + Srcpos_Bearer : Node_Id); + -- Id1 and Id2 should each be the entity of a state abstraction, a + -- variable, or a type (i.e., something suitable for passing to + -- Async_Readers_Enabled and similar functions). + -- Does nothing if SPARK_Mode /= On. Otherwise, flags a legality violation + -- if one or more of the four volatility-related aspects is False for Id1 + -- and True for Id2. The two descriptions are included in the error message + -- text; the source position for the generated message is determined by + -- Srcpos_Bearer. + function Choice_List (N : Node_Id) return List_Id; -- Utility to retrieve the choices of a Component_Association or the -- Discrete_Choices of an Iterated_Component_Association. For various @@ -664,14 +675,12 @@ package Sem_Util is -- are looked through. function Effective_Reads_Enabled (Id : Entity_Id) return Boolean; - -- Given the entity of an abstract state or a variable, determine whether - -- Id is subject to external property Effective_Reads and if it is, the - -- related expression evaluates to True. + -- Id should be the entity of a state abstraction, a variable, or a type. + -- Returns True iff Id is subject to external property Effective_Reads. function Effective_Writes_Enabled (Id : Entity_Id) return Boolean; - -- Given the entity of an abstract state or a variable, determine whether - -- Id is subject to external property Effective_Writes and if it is, the - -- related expression evaluates to True. + -- Id should be the entity of a state abstraction, a variable, or a type. + -- Returns True iff Id is subject to external property Effective_Writes. function Enclosing_Comp_Unit_Node (N : Node_Id) return Node_Id; -- Returns the enclosing N_Compilation_Unit node that is the root of a -- 2.7.4