From patchwork Thu May 25 08:05:07 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: 98837 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:994d:0:b0:3d9:f83d:47d9 with SMTP id k13csp192524vqr; Thu, 25 May 2023 01:07:13 -0700 (PDT) X-Google-Smtp-Source: ACHHUZ47J06i1CPWsnpIKx4TgVYxk26kBVGrL5y6sqPLQLFD2u94BAik16JRzGCs/fcEsarAYf3X X-Received: by 2002:a05:6402:3451:b0:510:ee0f:1eab with SMTP id l17-20020a056402345100b00510ee0f1eabmr3221560edc.41.1685002033234; Thu, 25 May 2023 01:07:13 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1685002033; cv=none; d=google.com; s=arc-20160816; b=rUiB5dPfP0Uay1roG5q1/umnUy98cqzRwuT7z/ImVmwMDVnpISvi3GLXBp8zlGZrX2 XmAxbrV3oR+qhga4FsVluvT8SyCU1aPhapmLsYWh14SenIyr9+VnUvTeTi3CytCG662d pgytU7WKRosyjDhHSUqe2P0ZFtrkSHSC3WBzD1ITppi02EChdbSTAe0nBzPhqRcaTKwk n8Hu0VRzcvybd6MThEbmH9G8OFPLABncySXp9zjLjN3xl8YJpklgIgTEJMFyRaFnWeHy BZlZ/MmNhmopQSO4tQf7tn1gnllAi2kHJwRcozma9dVrNldMVk3xK8r8IrkZMH8ODeET dy9g== 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=tkfRNDTjwumz1/O7oOwwJbzJ9hpqo/XYA1690OS7waY=; b=CWfo3ESgcjE/sC33h3HKAuRP7w7gZmc3Ys0V0KDf52CIkxQkah1D3kvVj0QY+vt9P3 INoNPwXtwIcmA+ze8kau7CY1nuRn+XmEiiWyPyyJ18SJir7LmLN5WFOu60SBSLupwYJD PQkzvqDxyWafCt+90Dr83CWZL6jrb65Y1akMH2JDxcB3gTzBcifJKTVUxcsGROExe4/0 JjgIuoEpmLNYFaPoxjJIhg67xZsfOWVN6Q4vAsWPXWdhZAFQlIjQMPwtHKJ7iNJQbNV2 PKSZOzaPdCD782fwj4CItzJ9dqJH25KMr5A/mV5R5smjSwqPZttPK0SjPoFLDdqVm6fG VyVA== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=Pf7hhuId; 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 i3-20020aa7c703000000b0050bc50e50f8si611335edq.559.2023.05.25.01.07.12 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 25 May 2023 01:07:13 -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=Pf7hhuId; 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 36ADE3846446 for ; Thu, 25 May 2023 08:06:24 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 36ADE3846446 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1685001984; bh=tkfRNDTjwumz1/O7oOwwJbzJ9hpqo/XYA1690OS7waY=; h=To:Cc:Subject:Date:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:List-Subscribe:From:Reply-To:From; b=Pf7hhuIdcIaVJ78HFt9I6XW2XLxrildJnP0KGgihw5ZwPcMmZNMGVT+tDDggO+57/ ncd4NcvmPFOsXsXgv9pkllGE/AOVWA1vITfOKrFUbTIg5tsWjTzT3f9MAcB4fM64QC ydlJUegLVEmllE7H4pBXunsj9CZUPoDH3gWTyxZM= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x432.google.com (mail-wr1-x432.google.com [IPv6:2a00:1450:4864:20::432]) by sourceware.org (Postfix) with ESMTPS id 569233858430 for ; Thu, 25 May 2023 08:05:20 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 569233858430 Received: by mail-wr1-x432.google.com with SMTP id ffacd0b85a97d-309550263e0so1721186f8f.2 for ; Thu, 25 May 2023 01:05:20 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1685001919; x=1687593919; 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=tkfRNDTjwumz1/O7oOwwJbzJ9hpqo/XYA1690OS7waY=; b=hjKadSzixGSckripqW0rIczfk536AoNGdZsfWiuIOlCG+GoczElI0UOYRyfE44tfm7 3HiX6q2Ixv4EzBvMUiYJqBsadycj6OpfE2n03mugpVRW2IoWjyGrBhsfxD/cH4kadqgl gG2pgqZ1ZL47zPhdWs1L913r4VgXwFr/8WEDTGu4FkK6ETvd32Zcd3sW02Mcpqz9LqmO 71zmWhCzpPxfY+iAt/PeHDh3AW2ZGjGW4/1pxpv6l9vBSDp2MianfE0up28sMN4vCO6n xtrbIm4mNga+DebLc0YQTDhyHDpAzruNAFEvrSnWA8VFY/mx7XtLdHYGLkxAyGNrAmC5 dUxA== X-Gm-Message-State: AC+VfDwFmdN8RxypP5Et9ooJeAd8AKkiW6Oo5oD1l3Iu6ukxp+aA7tmu suAQxhAddjpStt3ChodHkVexSLnAbtgQq7locCnbIw== X-Received: by 2002:a5d:4e83:0:b0:309:509f:a7ef with SMTP id e3-20020a5d4e83000000b00309509fa7efmr1658841wru.67.1685001919051; Thu, 25 May 2023 01:05:19 -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 i13-20020a5d522d000000b00307c8d6b4a0sm898966wra.26.2023.05.25.01.05.18 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 25 May 2023 01:05:18 -0700 (PDT) To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [COMMITTED] ada: Restrict use of formal parameters within exceptional cases Date: Thu, 25 May 2023 10:05:07 +0200 Message-Id: <20230525080507.1955270-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 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, 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?1766852692130713747?= X-GMAIL-MSGID: =?utf-8?q?1766852692130713747?= From: Piotr Trojanek Restrict references to formal parameters within the new SPARK aspect Exceptional_Cases and allow occurrences of 'Old in this aspect. gcc/ada/ * sem_attr.adb (Analyze_Attribute_Old_Result): Allow uses of 'Old and 'Result within the new aspect. * sem_res.adb (Within_Exceptional_Cases_Consequence): New utility routine. (Resolve_Entity_Name): Restrict use of formal parameters within the new aspect. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/sem_attr.adb | 8 ++++++ gcc/ada/sem_res.adb | 61 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 69 insertions(+) diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index bc4e3cf019e..0cfc2da29dd 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -1423,6 +1423,14 @@ package body Sem_Attr is elsif Prag_Nam = Name_Contract_Cases then Check_Placement_In_Contract_Cases (Prag); + -- Attributes 'Old and 'Result are allowed to appear in + -- consequence of aspect or pragma Exceptional_Cases. We already + -- examined the exception_choice part of contract syntax, so we + -- can accept all remaining occurrences within the pragma. + + elsif Prag_Nam = Name_Exceptional_Cases then + null; + -- Attribute 'Result is allowed to appear in aspect or pragma -- [Refined_]Depends (SPARK RM 6.1.5(11)). diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 3b7d821158c..4e49a0a1473 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7832,6 +7832,11 @@ package body Sem_Res is -- Determine whether Expr is part of an N_Attribute_Reference -- expression. + function Within_Exceptional_Cases_Consequence + (Expr : Node_Id) + return Boolean; + -- Determine whether Expr is part of an Exceptional_Cases consequence + ---------------------------------------- -- Is_Assignment_Or_Object_Expression -- ---------------------------------------- @@ -7896,6 +7901,39 @@ package body Sem_Res is return False; end Is_Attribute_Expression; + ------------------------------------------ + -- Within_Exceptional_Cases_Consequence -- + ------------------------------------------ + + function Within_Exceptional_Cases_Consequence + (Expr : Node_Id) + return Boolean + is + Context : Node_Id := Parent (Expr); + begin + while Present (Context) loop + if Nkind (Context) = N_Pragma then + + -- In Exceptional_Cases references to formal parameters are + -- only allowed within consequences, so it is enough to + -- recognize the pragma itself. + + if Get_Pragma_Id (Context) = Pragma_Exceptional_Cases then + return True; + end if; + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Context) then + return False; + end if; + + Context := Parent (Context); + end loop; + + return False; + end Within_Exceptional_Cases_Consequence; + -- Local variables E : constant Entity_Id := Entity (N); @@ -8040,6 +8078,29 @@ package body Sem_Res is & "(SPARK RM 7.1.3(10))", N); end if; + -- Parameters of modes OUT or IN OUT of the subprogram shall not + -- occur in the consequences of an exceptional contract unless + -- they either are of a by-reference type or occur in the prefix + -- of a reference to the 'Old attribute. + + if Ekind (E) in E_Out_Parameter | E_In_Out_Parameter + and then Within_Exceptional_Cases_Consequence (N) + and then not Is_Attribute_Old (Parent (N)) + and then not Is_By_Reference_Type (Etype (E)) + then + if Ekind (E) = E_Out_Parameter then + Error_Msg_N + ("formal parameter of mode `OUT` cannot appear " & + "in consequence of Exceptional_Cases", N); + else + Error_Msg_N + ("formal parameter of mode `IN OUT` cannot appear " & + "in consequence of Exceptional_Cases", N); + end if; + Error_Msg_N + ("\only parameters of by-reference types are allowed", N); + end if; + -- Check for possible elaboration issues with respect to reads of -- variables. The act of renaming the variable is not considered a -- read as it simply establishes an alias.