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: 61154 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 D59FD38532C6 for ; Mon, 28 Nov 2022 12:05:18 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org D59FD38532C6 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1669637118; 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=EIbJUIO4L7PpP/K0D0KC4Cf3RI2RR4++eogaM8Nxu1OTyiAzgxw17Q/MqpjrRvfY/ QAM88fGDUznNsvaBj/o7AyCBHD0Qt7zC5C2uE2d83cRAjPELcF8aXTCMgu7O0ejPt/ VPDo5Tj7RW5UqNHSwj+xRwbNd5PajpHQxVW//Z2U= 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-Google-Smtp-Source: AA0mqf4aqaa1aX4RUDO/6vV3LfvtEUXlfW+IkbuGXd+Xg1Zg3P+YT7SgX7vSKBRMzS0HxtQvGlB5Kg== 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+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" 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 "