From patchwork Tue May 16 08:40:15 2023 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: 94535 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:b0ea:0:b0:3b6:4342:cba0 with SMTP id b10csp274504vqo; Tue, 16 May 2023 01:52:59 -0700 (PDT) X-Google-Smtp-Source: ACHHUZ6kUV5Hvv8wzNKIoYSH7AxVwdTYULnGnIzezFU/UaMN0gOumrxLZW1sPWOxJx+bPxsHY7SR X-Received: by 2002:a17:907:2ce5:b0:969:9fd0:7cf2 with SMTP id hz5-20020a1709072ce500b009699fd07cf2mr26124211ejc.10.1684227179789; Tue, 16 May 2023 01:52:59 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1684227179; cv=none; d=google.com; s=arc-20160816; b=vpG/WSPeszC76ubURzrl8YSm1udS+/T9GGh0HaQ76Rjpo9NVB4LlL12Z2sAZlKM2Mu j5OSp5QBuLKsUlins/M6DIu95K5Mz85A0cpAHUeoiFT3LUVIIzuLxdM1Aa/EDJOkkzYn 14fMY0wLejyzZneCPiuTh3e9/DknISbagaqymkxblKZI1xU1k/QTTat3KLeBeQnrO+j9 xNQ25unHPdmjO5mSmFQwkA5F3yAGZdWEPo49xcmpGBm12qLFcjAxLP2PcbyITB4/Je3P c4KwwKoZMl2nlZJccfZ47+tPM93B21E4cln8sHBhG/Zcay4VKQmiEnlKzJNPCQ0u75fP E7KA== 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=oSlL7u4od+LU2XbQKIeMFelgg7zz9niQdX7k3UNIS6E=; b=TrMmZKuQiuZoRq3uLCqdWXtiX5QjCRDmE70utpJU09thF27HUb5sBsrgzSYVraNm+H F/gNFCv4pvVCyLph9lwSXMrZVtpQv/wlTcAjEYfKmAB3HxDqr4IusgjMZoKKhe88YvEm OvDwh1lgf/zUOroSfSgzB5UA6TmWdbB4yqhanX2+iBvpRNidi72twLuwsjFajNYMQu12 zRmpMlgTHeWXXzSZPOf+iYmurq2rzgWSbVRRMcSpXiJNGY6EhL6+1yWslYMvx24e5uEe rHXw95lZsRSimBklfODcovUeayQHeiSlkoBgiti5rImuRZfZftZEdGIJ8H58ShFNs0EN /uwA== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=cF72Dprr; 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 ka7-20020a170907990700b0094f54c032dbsi15145534ejc.154.2023.05.16.01.52.59 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 16 May 2023 01:52:59 -0700 (PDT) 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=cF72Dprr; 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 64206388187D for ; Tue, 16 May 2023 08:46:31 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 64206388187D DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1684226791; bh=oSlL7u4od+LU2XbQKIeMFelgg7zz9niQdX7k3UNIS6E=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=cF72DprrXQpLOvYlPDhoFKoutJFY3TJDDuPF2ca9+a/DQw8emoxnE0cTjvN1MlUdN kmib4F2r5Pn7/rsejXoPs9hTbx5PQtod2bz5GfTamZ3im3FFjn0n/NWPMM3T2yQeQq DuUeaC699gLlmCJ1OQIvrLqPJI/ZSbBQ9y3Mf2UA= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x334.google.com (mail-wm1-x334.google.com [IPv6:2a00:1450:4864:20::334]) by sourceware.org (Postfix) with ESMTPS id A2D77386D616 for ; Tue, 16 May 2023 08:40:18 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org A2D77386D616 Received: by mail-wm1-x334.google.com with SMTP id 5b1f17b1804b1-3f42c865535so80115285e9.1 for ; Tue, 16 May 2023 01:40:18 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1684226417; x=1686818417; 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=oSlL7u4od+LU2XbQKIeMFelgg7zz9niQdX7k3UNIS6E=; b=NVRnOQjruz0L6TsjBXtdATH5tWQ7t/IpwJN3X7uNveoY0d3t1ljbXcIrZqX1IQWOUX 3p/Suclm6W81XSg/QV8h5B6wamuIYyJ7oOdteS9wpRKQF52aVxJ7x2DM0zSuVs2Qs6Qu tgLRJTd4qToR8T8+9e6nwH3IvZl04b40GAFyCz6dSQPP2+iH2ac1kQOfsamnUf+VuIDh KDf9sAa0lgY4b1b9EfeH6UJf36BHNdYq8bQKY3ujQYyDgQdnAbfAkI08o8JgOH8VgxKN 2IBlDGaUkfJStGlSfn8FdXygEGdGtloIagY6QxubllVkD/fyTyM/lsozTk3kB4ezJ/gU PIeQ== X-Gm-Message-State: AC+VfDzYC8AJfAhM16BpG/bDsc3PqpV5TOu3kbfAWdnBx+ylQz9mRyzc crLV/WxmIFGsEvcrw57Lg1yOcpwxFDEpskhEIupKtQ== X-Received: by 2002:a1c:f702:0:b0:3f5:170:30a6 with SMTP id v2-20020a1cf702000000b003f5017030a6mr6049962wmh.10.1684226417514; Tue, 16 May 2023 01:40:17 -0700 (PDT) Received: from poulhies-Precision-5550.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id g14-20020a5d46ce000000b00304aba2cfcbsm1865434wrs.7.2023.05.16.01.40.16 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 16 May 2023 01:40:16 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [COMMITTED] ada: Build invariant procedure while freezing in GNATprove mode Date: Tue, 16 May 2023 10:40:15 +0200 Message-Id: <20230516084015.1501411-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 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, T_SCC_BODY_TEXT_LINE 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?1766040199344345190?= X-GMAIL-MSGID: =?utf-8?q?1766040199344345190?= From: Piotr Trojanek Invariant procedure bodies are created either by expansion of freezing nodes (but only in ordinary compilation mode) or at the end of package private declarations (but not for with private types in the type derivation chain). In GNATprove mode we didn't create invariant procedure bodies in lightweight expansion, so we didn't create them at all when there were private types in the type derivation chain. This patch copies the relevant freezing part from ordinary to lightweight expansion. This obviously involves code duplication, but it seems better to duplicate whole sections that work properly instead of small pieces that are incomplete. There are other pieces of freezing that are similarly duplicated, so this patch doesn't make the code substantially worse. gcc/ada/ * exp_spark.adb (SPARK_Freeze_Type): Copy whole handling of DIC and Type_Invariant from Freeze_Type. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/exp_spark.adb | 54 ++++++++++++++++++++++++++++++++++++------- 1 file changed, 46 insertions(+), 8 deletions(-) diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index efa5c2cd8da..c344dc1e706 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -101,7 +101,7 @@ package body Exp_SPARK is -- expanded body would compare the _parent component, which is -- intentionally not generated in the GNATprove mode. -- - -- We build the DIC procedure body here as well. + -- We build the DIC and Type_Invariant procedure bodies here as well. ------------------ -- Expand_SPARK -- @@ -920,15 +920,53 @@ package body Exp_SPARK is Set_Ghost_Mode (Typ); - -- When a DIC is inherited by a tagged type, it may need to be - -- specialized to the descendant type, hence build a separate DIC - -- procedure for it as done during regular expansion for compilation. + -- Generate the [spec and] body of the invariant procedure tasked with + -- the runtime verification of all invariants that pertain to the type. + -- This includes invariants on the partial and full view, inherited + -- class-wide invariants from parent types or interfaces, and invariants + -- on array elements or record components. But skip internal types. - if Has_DIC (Typ) and then Is_Tagged_Type (Typ) then - -- Why is this needed for DIC, but not for other aspects (such as - -- Type_Invariant)??? + if Is_Itype (Typ) then + null; + + elsif Is_Interface (Typ) then + + -- Interfaces are treated as the partial view of a private type in + -- order to achieve uniformity with the general case. As a result, an + -- interface receives only a "partial" invariant procedure which is + -- never called. + + if Has_Own_Invariants (Typ) then + Build_Invariant_Procedure_Body + (Typ => Typ, + Partial_Invariant => Is_Interface (Typ)); + end if; + + -- Non-interface types - Build_DIC_Procedure_Body (Typ); + -- Do not generate invariant procedure within other assertion + -- subprograms, which may involve local declarations of local + -- subtypes to which these checks do not apply. + + else + if Has_Invariants (Typ) then + if not Predicate_Check_In_Scope (Typ) + or else (Ekind (Current_Scope) = E_Function + and then Is_Predicate_Function (Current_Scope)) + then + null; + else + Build_Invariant_Procedure_Body (Typ); + end if; + end if; + + -- Generate the [spec and] body of the procedure tasked with the + -- run-time verification of pragma Default_Initial_Condition's + -- expression. + + if Has_DIC (Typ) then + Build_DIC_Procedure_Body (Typ); + end if; end if; if Ekind (Typ) = E_Record_Type