From patchwork Mon Nov 28 12:04:37 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: 26711 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:adf:f944:0:0:0:0:0 with SMTP id q4csp5611340wrr; Mon, 28 Nov 2022 04:05:53 -0800 (PST) X-Google-Smtp-Source: AA0mqf5zEpyY76CcAA/1cL/sAOTY2cF7IS/wEg0u94Br6EP3Rrbi1rR+YgAwBnxGkDGEvlYf5XYR X-Received: by 2002:a05:6402:ea0:b0:463:a83c:e019 with SMTP id h32-20020a0564020ea000b00463a83ce019mr30375386eda.253.1669637153606; Mon, 28 Nov 2022 04:05:53 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1669637153; cv=none; d=google.com; s=arc-20160816; b=nx7AG9yzmo0TigevCfpFQsDlEcSNixmJDXmcjxDcOsw+spHGS0sutZ6dxhKxkvh374 rj5ISMvp6K3HBIcg7svmW4zF354RGGr7TU7tVlFrwdrKBLCd4pk1R5FYeBPqR2I1eoiv HQi8Yzg56lkpsbiCTKdIR7XPgaiGZEaca9N7epHPVJzZNCu/rj8iUiSKEiSJWiuYL/OO bQNRCUN/VGSwLzaRt4tj84Gu5df0HNkruqCpwc00U/8qIW/11a+K9a/cgwLDRazoY/Il W8Fp+iRUXziJvezKJxqzqC5X2MfAGOK88bhSdc5xbekpGTwMAQOh4w206l+72sNHWiHB l7Aw== 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=HbsF9COfcL+cB4+nMQfuxWKWP8kttZiHf+2SkyqCutw=; b=EcfRHgK5Ildicd9V3XNj5RSBc0tgIDjke3iWARqTySgz0ICLA6ULItAcM59m1CFyF/ XDOm2DQXt20xsLA3B5nSuu2EPPoZrVn4wmmlgpNAA993Fth5JGHkiI+cHFehj5djsIA9 aFbQNKcEYpxeEoQT4ZM8cePd2QPPSRCyM1PySfcPP8fjQk66JQQsJwJ45FTliBASIO61 IQyKx9SLwohQ/gC+Cj86ydK86LMGaOh/7HQKfW8RwJFffvATw8RrL1l5b8sAof7TNuPt /Sy2U0snLFxXzLKb/7TSDG5n1h0O9xa45zBBLGy/3CGhrc1XzBFxBGMwSxb1antNG4HI NEOQ== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=HFMllP6K; 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 j21-20020a508a95000000b0045cc02ce2aasi8631449edj.319.2022.11.28.04.05.53 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 28 Nov 2022 04:05:53 -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=HFMllP6K; 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 344F93852232 for ; Mon, 28 Nov 2022 12:05:34 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 344F93852232 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1669637134; bh=HbsF9COfcL+cB4+nMQfuxWKWP8kttZiHf+2SkyqCutw=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=HFMllP6K7vuDFW4LByz3yLf3z9AjWC/rcgnyzjdCn13wc1djNM0RpO5oGO631v2ii WsWlnQkbF9/IAjtyxzVSDCs2O65D8yk5fq2SnKPcnTZDqr04EA/RepnF/9lwWD034J nTtq13r47w+CDcl+Kx/WABYsCQNPsK2kBzdgjWsc= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x331.google.com (mail-wm1-x331.google.com [IPv6:2a00:1450:4864:20::331]) by sourceware.org (Postfix) with ESMTPS id B47263858C62 for ; Mon, 28 Nov 2022 12:04:48 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org B47263858C62 Received: by mail-wm1-x331.google.com with SMTP id 83-20020a1c0256000000b003d03017c6efso10758782wmc.4 for ; Mon, 28 Nov 2022 04:04:48 -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=HbsF9COfcL+cB4+nMQfuxWKWP8kttZiHf+2SkyqCutw=; b=ScvPdTR8Z6GbimQrU9+T9yltvI04qWfoAWQb40ka6wLh6XEFavGtyKVJs2ncEs59kT vRilEs6r1z3irPu69Nj7oUlV5/FoathhwiqC4qfF414fTCYj1chKbgW2y53Y3iwl4zB9 QAUjq2pdrm9jxOLLEGT+9mkhSg0X41x/S4SGk9twMFfby2I4swKZ0Oz8gfx1rik62E5I iMwpsjaSp3qOLDjHerKECyqyaxYWeE/Isa94pcMGKfdeLPEV1nOkF8vM7HzsVXLlCV0v K2EvAAECmuuWGkGB0WoGBOabi0Mv7fs3ZRTq2feKqJ9eFUYb0xujO7a2TbpDdhd4jZc0 aocA== X-Gm-Message-State: ANoB5pnenRcGPYqyHoL1esIFAsBLdIx5k/P2TGsieXbRDOf9bO68CTDN yjL80tUX7q7umFr8RwiEm/MH5ZMwjbyZ+g== X-Received: by 2002:a7b:cb97:0:b0:3cf:ac0d:3f80 with SMTP id m23-20020a7bcb97000000b003cfac0d3f80mr23152973wmi.185.1669637087327; Mon, 28 Nov 2022 04:04:47 -0800 (PST) Received: from localhost.localdomain (static-176-191-105-132.ftth.abo.bbox.fr. [176.191.105.132]) by smtp.gmail.com with ESMTPSA id a12-20020adfe5cc000000b0022cc3e67fc5sm10427530wrn.65.2022.11.28.04.04.46 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 28 Nov 2022 04:04:46 -0800 (PST) To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Implement change to SPARK RM rule on state refinement Date: Mon, 28 Nov 2022 13:04:37 +0100 Message-Id: <20221128120437.171358-1-poulhies@adacore.com> X-Mailer: git-send-email 2.34.1 MIME-Version: 1.0 X-Spam-Status: No, score=-13.5 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, 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?1750741448165247833?= X-GMAIL-MSGID: =?utf-8?q?1750741448165247833?= From: Yannick Moy SPARK RM 7.1.4(4) does not mandate anymore that a package with abstract states has a completing body, unless the package state is mentioned in Part_Of specifications. Implement that change. gcc/ada/ * sem_prag.adb (Check_Part_Of_Abstract_State): Add verification related to use of Part_Of, so that constituents in private childs that refer to state in a sibling or parent unit force that unit to have a body. * sem_util.adb (Check_State_Refinements): Drop the requirement to have always a package body for state refinement, when the package state is mentioned in no Part_Of specification. * sem_ch3.adb (Analyze_Declarations): Refresh SPARK refs in comment. * sem_ch7.adb (Analyze_Package_Declaration): Likewise. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/sem_ch3.adb | 3 ++- gcc/ada/sem_ch7.adb | 10 +++++----- gcc/ada/sem_prag.adb | 16 ++++++++++++++++ gcc/ada/sem_util.adb | 14 ++++++++++---- 4 files changed, 33 insertions(+), 10 deletions(-) diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index ce5a00b7fc8..61386e27feb 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2942,7 +2942,8 @@ package body Sem_Ch3 is -- Verify that all abstract states found in any package declared in -- the input declarative list have proper refinements. The check is -- performed only when the context denotes a block, entry, package, - -- protected, subprogram, or task body (SPARK RM 7.2.2(3)). + -- protected, subprogram, or task body (SPARK RM 7.1.4(4) and SPARK + -- RM 7.2.2(3)). Check_State_Refinements (Context); diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index 0fb9fe10ff6..284706981d6 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -1243,11 +1243,11 @@ package body Sem_Ch7 is Check_Completion; -- If the package spec does not require an explicit body, then all - -- abstract states declared in nested packages cannot possibly get - -- a proper refinement (SPARK RM 7.2.2(3)). This check is performed - -- only when the compilation unit is the main unit to allow for - -- modular SPARK analysis where packages do not necessarily have - -- bodies. + -- abstract states declared in nested packages cannot possibly get a + -- proper refinement (SPARK RM 7.1.4(4) and SPARK RM 7.2.2(3)). This + -- check is performed only when the compilation unit is the main + -- unit to allow for modular SPARK analysis where packages do not + -- necessarily have bodies. if Is_Comp_Unit then Check_State_Refinements diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 0a91518cff9..27bd879903e 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -63,6 +63,7 @@ with Sem; use Sem; with Sem_Aux; use Sem_Aux; with Sem_Ch3; use Sem_Ch3; with Sem_Ch6; use Sem_Ch6; +with Sem_Ch7; use Sem_Ch7; with Sem_Ch8; use Sem_Ch8; with Sem_Ch12; use Sem_Ch12; with Sem_Ch13; use Sem_Ch13; @@ -3567,6 +3568,21 @@ package body Sem_Prag is return; end if; + -- In the case of state in a (descendant of a private) child which + -- is Part_Of the state of another package, the package defining the + -- encapsulating abstract state should have a body, to ensure that it + -- has a state refinement (SPARK RM 7.1.4(4)). + + if Enclosing_Comp_Unit_Node (Encap_Id) /= + Enclosing_Comp_Unit_Node (Item_Id) + and then not Unit_Requires_Body (Scope (Encap_Id)) + then + SPARK_Msg_N + ("indicator Part_Of must denote abstract state of package " + & "with a body (SPARK RM 7.1.4(4))", Indic); + return; + end if; + -- At this point it is known that the Part_Of indicator is legal Legal := True; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index f331b4b78ba..a13d9ebef5b 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -5450,12 +5450,18 @@ package body Sem_Util is while Present (State_Elmt) loop State_Id := Node (State_Elmt); - -- Emit an error when a non-null state lacks any form of - -- refinement. + -- Emit an error when a non-null state lacks refinement, + -- but has Part_Of constituents or there is a package + -- body (SPARK RM 7.1.4(4)). Constituents in private + -- child packages, which are not known at this stage, + -- independently require the existence of a package body. if not Is_Null_State (State_Id) - and then not Has_Null_Refinement (State_Id) - and then not Has_Non_Null_Refinement (State_Id) + and then No (Refinement_Constituents (State_Id)) + and then + (Present (Part_Of_Constituents (State_Id)) + or else + Present (Body_Id)) then Error_Msg_N ("state & requires refinement", State_Id); Error_Msg_N ("\package body should have Refined_State "