From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 7871) id 654F3384C93A; Tue, 6 Dec 2022 14:01:35 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 654F3384C93A DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1670335295; bh=4gEYPI1h5tASlXCH1pv8rmZYh2PYEIlFP0hXLmNCWK4=; h=From:To:Subject:Date:From; b=DuixJvaDoAjQQuBopN+kkktXG7gQ9yZtAM7debyFvIn5DxRvC3G92AdtpeykNBbEe IWfRP8nj7UB4bcUqJNeP3ocTfYGs2V1qidvMBFUc+3YKeuK7rpzKrO+BEZSa8xFl76 GKSjyMFtkIgg1qJDyoJ6NyeeDIZgq4frbgGyD02M= MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Marc Poulhi?s To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-4515] ada: Allow No_Caching on volatile types X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: 7dc44f280e7d1126b4d05e79c53b40df1afe334a X-Git-Newrev: 400d9fc1f04336118c3200e2af14a620e7ea1d95 Message-Id: <20221206140135.654F3384C93A@sourceware.org> Date: Tue, 6 Dec 2022 14:01:35 +0000 (GMT) List-Id: https://gcc.gnu.org/g:400d9fc1f04336118c3200e2af14a620e7ea1d95 commit r13-4515-g400d9fc1f04336118c3200e2af14a620e7ea1d95 Author: Yannick Moy Date: Fri Nov 25 17:16:06 2022 +0100 ada: Allow No_Caching on volatile types SPARK RM now allow the property No_Caching on volatile types, to indicate that they should be considered volatile for compilation, but not by GNATprove's analysis. gcc/ada/ * contracts.adb (Add_Contract_Item): Allow No_Caching on types. (Check_Type_Or_Object_External_Properties): Check No_Caching. Check that non-effectively volatile types does not contain an effectively volatile component (instead of just a volatile component). (Analyze_Object_Contract): Remove shared checking of No_Caching. * sem_prag.adb (Analyze_External_Property_In_Decl_Part): Adapt checking of No_Caching for types. (Analyze_Pragma): Allow No_Caching on types. * sem_util.adb (Has_Effectively_Volatile_Component): New query function. (Is_Effectively_Volatile): Type with Volatile and No_Caching is not effectively volatile. (No_Caching_Enabled): Remove assertion to apply to all entities. * sem_util.ads: Same. Diff: --- gcc/ada/contracts.adb | 32 ++++++++++++++++---------------- gcc/ada/sem_prag.adb | 49 ++++++++++++++++++++++++++----------------------- gcc/ada/sem_util.adb | 37 ++++++++++++++++++++++++++++++++++--- gcc/ada/sem_util.ads | 11 ++++++++--- 4 files changed, 84 insertions(+), 45 deletions(-) diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index 6f474eb2944..59121ca9ea2 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -316,6 +316,7 @@ package body Contracts is | Name_Async_Writers | Name_Effective_Reads | Name_Effective_Writes + | Name_No_Caching or else (Ekind (Id) = E_Task_Type and Prag_Nam in Name_Part_Of | Name_Depends @@ -859,6 +860,7 @@ package body Contracts is AW_Val : Boolean := False; ER_Val : Boolean := False; EW_Val : Boolean := False; + NC_Val : Boolean; Seen : Boolean := False; Prag : Node_Id; Obj_Typ : Entity_Id; @@ -956,18 +958,25 @@ package body Contracts is end if; -- Verify the mutual interaction of the various external properties. - -- For variables for which No_Caching is enabled, it has been checked - -- already that only False values for other external properties are - -- allowed. + -- For types and variables for which No_Caching is enabled, it has been + -- checked already that only False values for other external properties + -- are allowed. if Seen - and then (Ekind (Type_Or_Obj_Id) /= E_Variable - or else not No_Caching_Enabled (Type_Or_Obj_Id)) + and then not No_Caching_Enabled (Type_Or_Obj_Id) then Check_External_Properties (Type_Or_Obj_Id, AR_Val, AW_Val, ER_Val, EW_Val); end if; + -- Analyze the non-external volatility property No_Caching + + Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_No_Caching); + + if Present (Prag) then + Analyze_External_Property_In_Decl_Part (Prag, NC_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, as well as return objects. @@ -1047,10 +1056,10 @@ package body Contracts is if Is_Type_Id and then not Is_Effectively_Volatile (Type_Or_Obj_Id) - and then Has_Volatile_Component (Type_Or_Obj_Id) + and then Has_Effectively_Volatile_Component (Type_Or_Obj_Id) then Error_Msg_N - ("non-volatile type & cannot have volatile" + ("non-volatile type & cannot have effectively volatile" & " components", Type_Or_Obj_Id); end if; @@ -1076,7 +1085,6 @@ package body Contracts is Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; -- Save the SPARK_Mode-related data to restore on exit - NC_Val : Boolean; Items : Node_Id; Prag : Node_Id; Ref_Elmt : Elmt_Id; @@ -1118,14 +1126,6 @@ package body Contracts is Check_Type_Or_Object_External_Properties (Type_Or_Obj_Id => Obj_Id); - -- Analyze the non-external volatility property No_Caching - - Prag := Get_Pragma (Obj_Id, Pragma_No_Caching); - - if Present (Prag) then - Analyze_External_Property_In_Decl_Part (Prag, NC_Val); - end if; - -- Constant-related checks if Ekind (Obj_Id) = E_Constant then diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 27bd879903e..f3c23caeae4 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2116,9 +2116,16 @@ package body Sem_Prag is First (Pragma_Argument_Associations (N)); Obj_Decl : constant Node_Id := Find_Related_Context (N); Obj_Id : constant Entity_Id := Defining_Entity (Obj_Decl); + Obj_Typ : Entity_Id; Expr : Node_Id; begin + if Is_Type (Obj_Id) then + Obj_Typ := Obj_Id; + else + Obj_Typ := Etype (Obj_Id); + end if; + -- Ensure that the Boolean expression (if present) is static. A missing -- argument defaults the value to True (SPARK RM 7.1.2(5)). @@ -2153,9 +2160,7 @@ package body Sem_Prag is if Prag_Id /= Pragma_No_Caching and then not Is_Effectively_Volatile (Obj_Id) then - if Ekind (Obj_Id) = E_Variable - and then No_Caching_Enabled (Obj_Id) - then + if No_Caching_Enabled (Obj_Id) then if Expr_Val then -- Confirming value of False is allowed SPARK_Msg_N ("illegal combination of external property % and property " @@ -2167,15 +2172,16 @@ package body Sem_Prag is N); end if; - -- Pragma No_Caching should only apply to volatile variables of + -- Pragma No_Caching should only apply to volatile types or variables of -- a non-effectively volatile type (SPARK RM 7.1.2). elsif Prag_Id = Pragma_No_Caching then - if Is_Effectively_Volatile (Etype (Obj_Id)) then - SPARK_Msg_N ("property % must not apply to an object of " + if Is_Effectively_Volatile (Obj_Typ) then + SPARK_Msg_N ("property % must not apply to a type or object of " & "an effectively volatile type", N); elsif not Is_Volatile (Obj_Id) then - SPARK_Msg_N ("property % must apply to a volatile object", N); + SPARK_Msg_N + ("property % must apply to a volatile type or object", N); end if; end if; @@ -13484,22 +13490,19 @@ package body Sem_Prag is 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 else Nkind (Original_Node (Obj_Or_Type_Decl)) not in - N_Full_Type_Declaration | - N_Private_Type_Declaration | - N_Formal_Type_Declaration | - N_Task_Type_Declaration | - N_Protected_Type_Declaration - then - Pragma_Misplaced; - end if; + -- declaration. 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 + and then Nkind (Original_Node (Obj_Or_Type_Decl)) not in + N_Full_Type_Declaration | + N_Private_Type_Declaration | + N_Formal_Type_Declaration | + N_Task_Type_Declaration | + N_Protected_Type_Declaration + then + Pragma_Misplaced; end if; Obj_Or_Type_Id := Defining_Entity (Obj_Or_Type_Decl); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 1fef8475c05..a1cebb08291 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -13530,6 +13530,36 @@ package body Sem_Util is return Has_Undef_Ref; end Has_Undefined_Reference; + ---------------------------------------- + -- Has_Effectively_Volatile_Component -- + ---------------------------------------- + + function Has_Effectively_Volatile_Component + (Typ : Entity_Id) return Boolean + is + Comp : Entity_Id; + + begin + if Has_Volatile_Components (Typ) then + return True; + + elsif Is_Array_Type (Typ) then + return Is_Effectively_Volatile (Component_Type (Typ)); + + elsif Is_Record_Type (Typ) then + Comp := First_Component (Typ); + while Present (Comp) loop + if Is_Effectively_Volatile (Etype (Comp)) then + return True; + end if; + + Next_Component (Comp); + end loop; + end if; + + return False; + end Has_Effectively_Volatile_Component; + ---------------------------- -- Has_Volatile_Component -- ---------------------------- @@ -16663,9 +16693,11 @@ package body Sem_Util is if Is_Type (Id) then -- An arbitrary type is effectively volatile when it is subject to - -- pragma Atomic or Volatile. + -- pragma Atomic or Volatile, unless No_Caching is enabled. - if Is_Volatile (Id) then + if Is_Volatile (Id) + and then not No_Caching_Enabled (Id) + then return True; -- An array type is effectively volatile when it is subject to pragma @@ -24579,7 +24611,6 @@ package body Sem_Util is ------------------------ function No_Caching_Enabled (Id : Entity_Id) return Boolean is - pragma Assert (Ekind (Id) = E_Variable); Prag : constant Node_Id := Get_Pragma (Id, Pragma_No_Caching); Arg1 : Node_Id; diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 34aaa9a932f..b647e68ff7f 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1564,6 +1564,11 @@ package Sem_Util is -- Given arbitrary expression Expr, determine whether it contains at -- least one name whose entity is Any_Id. + function Has_Effectively_Volatile_Component + (Typ : Entity_Id) return Boolean; + -- Given arbitrary type Typ, determine whether it contains at least one + -- effectively volatile component. + function Has_Volatile_Component (Typ : Entity_Id) return Boolean; -- Given arbitrary type Typ, determine whether it contains at least one -- volatile component. @@ -2758,9 +2763,9 @@ package Sem_Util is -- inline this procedural form, but not the functional form above. function No_Caching_Enabled (Id : Entity_Id) return Boolean; - -- Given the entity of a variable, determine whether Id is subject to - -- volatility property No_Caching and if it is, the related expression - -- evaluates to True. + -- Given any entity Id, determine whether Id is subject to volatility + -- property No_Caching and if it is, the related expression evaluates + -- to True. function No_Heap_Finalization (Typ : Entity_Id) return Boolean; -- Determine whether type Typ is subject to pragma No_Heap_Finalization