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: 30312 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:adf:f944:0:0:0:0:0 with SMTP id q4csp2841136wrr; Tue, 6 Dec 2022 06:08:42 -0800 (PST) X-Google-Smtp-Source: AA0mqf4QEeCj2TQjHnE0YECH8LGdWciztl1rXSNMEUAEA4RYw2asjyQzNYf4G+wndA7dN4oBgLjF X-Received: by 2002:a17:906:824e:b0:7c0:ec3f:e55d with SMTP id f14-20020a170906824e00b007c0ec3fe55dmr9187068ejx.508.1670335722493; Tue, 06 Dec 2022 06:08:42 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1670335722; cv=none; d=google.com; s=arc-20160816; b=K9Y+LEc7wGzACZMuh1FwMVRK6bThKId1Vga59wx85xx0nw0Zq/Np/IHRVp8sD5Jrkn knaa1084Vlr1P4WZx/8aM2guUKgr4LGYcm+3uqYtUaoBfBEPK4ivHdOOVD1USVcNiTIa +L3c0/LbuaJMwXmy6BR/FkX32KdHpwW2XriOt3iA44XE7UYNpOEtLeL7DdB3YMnHOe/m py+0OBKgEgNglDSiNxDoxP458RqazFyPLdVbNoa6ZJ2n29+V9eSRujnvk5WsRx/C9MUm SuKUABjpuyRPq+gid4OjxAtCZetjVLF8olYjmioBd0Lac3WWcEXF4esNsP55chFrchkb grxg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:reply-to:from:list-subscribe:list-help:list-post :list-archive:list-unsubscribe:list-id:precedence :content-transfer-encoding:mime-version:message-id:date:subject:cc :to:dmarc-filter:delivered-to:dkim-signature:dkim-filter; bh=pCDIquFIbR/o2M0i7Lq9p+yzSsNgr0n4r3gvLZBOyjI=; b=lCPUsNr+qSALotvogPBDzCAdK/91P+NOvMZjZiw22FzIkUFTGLbljdYe8vtbS6VsYe WqvywcKkt+0Bjthm75BDXGkXqTvPiTW12KgNxAQYkry5roElgb4VkxQ/o1J4CsJEEbjL TKpIc7FQFzoAIkeEEPJz7SKG+dPvD5osOnsc4SKdKO5HoaEWcpbdKP9aHsTEEzjzXkNq ETe1W7HCflLC/mYoVANtSFNzgnXxld1cWy2pM4D4Q6HmCyO677Ah2wAiI1LrrqbWuhWq c/JQmldGnrAeaW18tRUmnSS+fpysWxTau9CLcclNNKV4J6gkWDL1f4JK30SuDEPlTmCC j6fQ== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=jrC5fWht; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from sourceware.org (server2.sourceware.org. [2620:52:3:1:0:246e:9693:128c]) by mx.google.com with ESMTPS id rn5-20020a170906d92500b007c0d40cd759si5747233ejb.827.2022.12.06.06.08.42 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 06 Dec 2022 06:08:42 -0800 (PST) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) client-ip=2620:52:3:1:0:246e:9693:128c; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=jrC5fWht; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 415E13846985 for ; Tue, 6 Dec 2022 14:08:11 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 415E13846985 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1670335691; 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=jrC5fWhtT9EVxqD/HQz1x3nn7zXWcJ/kyYvT8zUDgD4Vgf9suOGsqa+Kk1wolw5xx SKiGzHpKi9S32wFUVGotiLAdhOznInLZb9MSP9tuA0pc6N495S98opkn96xVZDMg1N jQ6pbci541BWr8PtpE/IKUhrxD5knQH+z/kYUsuQ= 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-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+ouuuleilei=gmail.com@gcc.gnu.org Sender: "Gcc-patches" X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1751473950022186997?= X-GMAIL-MSGID: =?utf-8?q?1751473950022186997?= 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