From patchwork Tue Dec 6 14:02:28 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 61570 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id E4B93384C934 for ; Tue, 6 Dec 2022 14:07:55 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org E4B93384C934 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1670335675; bh=pCDIquFIbR/o2M0i7Lq9p+yzSsNgr0n4r3gvLZBOyjI=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=TGt2Ii3GoJhb1w2ewuADVKRXRjK2HF1Kc/kC504kZLzG9BfN4wqNwQa+nc2WK+HOl F4o2I30JyMKl91u/VIdDxS8gONOl/DgE1RDGnaPeh8KSUjz2BV9qYYORzwNXnKyWLE Rl6qE5O4CeNCZ52zSNUN2NkvfKFf04xuCQGRpSfU= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x433.google.com (mail-wr1-x433.google.com [IPv6:2a00:1450:4864:20::433]) by sourceware.org (Postfix) with ESMTPS id 6713F3875B61 for ; Tue, 6 Dec 2022 14:02:31 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 6713F3875B61 Received: by mail-wr1-x433.google.com with SMTP id d1so23562165wrs.12 for ; Tue, 06 Dec 2022 06:02:31 -0800 (PST) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=pCDIquFIbR/o2M0i7Lq9p+yzSsNgr0n4r3gvLZBOyjI=; b=VJO1dxFNRDgIRhmAdNnFufVpyKmAxPU1v6GBc5RRmE58++PLKiHe9RWNVMa+rcxeL/ aS3r8k7cHbkdPGNSPTbPFCmFzfp1EfdMMV5DEE/vk6jUtAsOOO9+tzO6KSgvmlB/a3oy IH1YU80U6Cfu4cuTClQ/y0K8YKCw2lLsUh92VA+6PWTZjd9aFatz2/6Nidu9nyTERjn5 7VOm0qtgxExX8ROexdZhLfGLc8NyD1X8PENA/YkHNQW3V5OjY00ACxjujo7zwyYEi8sJ ceS89EJLgt34TTklqSnNiBLOPGEMSEgQjsVpsfeeDcEb57F2qCMleumH5oUl6nDRLwXh nbBg== X-Gm-Message-State: ANoB5pnMdzmh+y5owsqYTDyZjCL58dTBIdxcLj2qAirl4uKRStcfrUWT pJ7WhmXHIl3MP2BR5BOvib+Oa84lm0thpU5c X-Google-Smtp-Source: AA0mqf7vcgzTQ8It6AL+R+MQWDmNh31bas1mVv5wpvswhGLElbOr6aEsj8wFo4QXFYsk+7TQLw4SlA== X-Received: by 2002:adf:e347:0:b0:236:76de:7280 with SMTP id n7-20020adfe347000000b0023676de7280mr54557105wrj.194.1670335350945; Tue, 06 Dec 2022 06:02:30 -0800 (PST) Received: from poulhies-Precision-5550.lan (static-176-191-105-132.ftth.abo.bbox.fr. [176.191.105.132]) by smtp.gmail.com with ESMTPSA id e15-20020a5d530f000000b002420dba6447sm16498720wrv.59.2022.12.06.06.02.30 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 06 Dec 2022 06:02:30 -0800 (PST) To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Allow No_Caching on volatile types Date: Tue, 6 Dec 2022 15:02:28 +0100 Message-Id: <20221206140228.717520-1-poulhies@adacore.com> X-Mailer: git-send-email 2.34.1 MIME-Version: 1.0 X-Spam-Status: No, score=-13.2 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: =?utf-8?q?Marc_Poulhi=C3=A8s_via_Gcc-patches?= From: =?utf-8?q?Marc_Poulhi=C3=A8s?= Reply-To: =?utf-8?q?Marc_Poulhi=C3=A8s?= Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" From: Yannick Moy 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. Tested on x86_64-pc-linux-gnu, committed on master. --- 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