From patchwork Tue Jan 9 13:15:44 2024 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: 186374 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a05:7300:2411:b0:101:2151:f287 with SMTP id m17csp100962dyi; Tue, 9 Jan 2024 05:20:32 -0800 (PST) X-Google-Smtp-Source: AGHT+IGhYbWdj5LT7DdxBzGl5Q+UhFfV4DSdjQ1rbVcjqzc7+ByRmCxYGMzVNOafkwU9EjPbWmou X-Received: by 2002:a4a:ab07:0:b0:598:2d9f:d4a0 with SMTP id i7-20020a4aab07000000b005982d9fd4a0mr2915764oon.0.1704806432057; Tue, 09 Jan 2024 05:20:32 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1704806432; cv=pass; d=google.com; s=arc-20160816; b=Yjae7dnvXKQu+BNvFD5vHXtuoTTkjsap/XAH0TVpmCFtsZ0urPOQbLwwHA1bGljESs rDUul2QzYh5J7tZPsxCONUgLprZbSehBYoVeSyB1wpDaEkTQ57HQjdZIHSFxZHgeLZUp dUgMv655c/RR4evdqlYoljBcQ4iBnDSUDX4Esiz2Y3MX6zpPMPIm/aavA7LgbOYwEtcw TOLSzaQhyXfOn+s+VYolfcjOEsDFJqFMCYc0XJ18foxSZTUbYqPXloBsa+OnTAgVJ/oy 5B/+EOZJjdeg6gGaKTIvYxRWapxZioqcrRjItGDkLlG8m38JSbzoFCnyLaibOmr8Tm0Z u+xQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=errors-to:list-subscribe:list-help:list-post:list-archive :list-unsubscribe:list-id:precedence:content-transfer-encoding :mime-version:message-id:date:subject:cc:to:from:dkim-signature :arc-filter:dmarc-filter:delivered-to; bh=2NaywD19BKq4ohQgyIw/7jbUOkEmsBbsO8DVfOXHTKw=; fh=QRb7QY4BZ0mIIAPiH2G4K0PcYKRtRn2i5A6VLUA8cN4=; b=0exT4xUJpH/NEDFR81ZcHb9/0/OQBTqtSYkJa6XsuyeoG6kP4lHKObYLWLSQF5+LLH pamgCLIfCLNFo6P+6D8Aq761R3fS53IWJHCfWvhgFZDyhuZyjVWCvqXegwABKzCuSgUy YyjHXmVKjMhlPoiDi2N1o2IUlt2DYqvQBRt2gbgV4H3FICBeIpe3dxqYFlkCCwVHE9HB S8eadIgM2haEWtJyP2pM1xbs/miruYhGbP4iPSFuRKjeuqXhoWFuM/7X0f8lDVRA97/s PH8/UBK43WTnvo2hkNQlFoG+Dcd67rabQmYqxMpHVNHldHgZCcMMpLr7+6TJCkHGasQq I9PA== ARC-Authentication-Results: i=2; mx.google.com; dkim=pass header.i=@adacore.com header.s=google header.b=U8aO+GJm; arc=pass (i=1); 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=QUARANTINE sp=QUARANTINE dis=NONE) header.from=adacore.com Received: from server2.sourceware.org (server2.sourceware.org. [2620:52:3:1:0:246e:9693:128c]) by mx.google.com with ESMTPS id z8-20020a05622a060800b004298787b034si2067511qta.518.2024.01.09.05.20.31 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 09 Jan 2024 05:20:32 -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=@adacore.com header.s=google header.b=U8aO+GJm; arc=pass (i=1); 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=QUARANTINE sp=QUARANTINE dis=NONE) header.from=adacore.com Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id B9E1D3861831 for ; Tue, 9 Jan 2024 13:20:31 +0000 (GMT) X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x335.google.com (mail-wm1-x335.google.com [IPv6:2a00:1450:4864:20::335]) by sourceware.org (Postfix) with ESMTPS id A3D1B3861844 for ; Tue, 9 Jan 2024 13:15:46 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org A3D1B3861844 Authentication-Results: sourceware.org; dmarc=pass (p=quarantine dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com ARC-Filter: OpenARC Filter v1.0.0 sourceware.org A3D1B3861844 Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::335 ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1704806149; cv=none; b=jCmuj7MYSpvJBvN/zOqpKUwBOPPEPsTNerSxaj8Kbpx3uw5Ur4DkZeJPYAmGhS8nqxbtlOXKTTU/DouSkihrewwpZ7LtCJ49OUf/fAr+dcB3+9ltzC5pJCaRqETSLAE0t6V/q8fBORx0eeuM5Zl/xSRM3y63qLBzmn1zSjNsiiw= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1704806149; c=relaxed/simple; bh=ZyBG5NloM0vHj5SIYYP48sdYWDJ7hYKRirHe5+Xzj1Y=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=m2Wi2WGG+F6zmTTgPDu5CcTO10PWc6AjXi3N3MbSGlPhzYy7XmLdQHG8XvLT4MDeN8T2/RL52fAc9PywB90O83uHubwLWOOH+FolpNyr/UzEHY6LbvMybtKBWDFnqVLc1MaFqttvJVaIe2A1qcIIKkxY/AeSElx5ctTJtx/JLng= ARC-Authentication-Results: i=1; server2.sourceware.org Received: by mail-wm1-x335.google.com with SMTP id 5b1f17b1804b1-40e461c1f44so23169115e9.3 for ; Tue, 09 Jan 2024 05:15:46 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1704806145; x=1705410945; darn=gcc.gnu.org; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=2NaywD19BKq4ohQgyIw/7jbUOkEmsBbsO8DVfOXHTKw=; b=U8aO+GJmeBfLT7lUUmMpi9iVPyJeYVD2uh+VUie2szYAY1nmKsR2XYGW01aOO8pH7a UPe9w9PP+0D3Sna5Aute0ZVRhIlftzrzFf/0OskAVja4L3eSJ2VJPRQM0WOiMKxd9gEe wnokDee32zlD7NpdVOflfL+9cfFYWCif+LSzqMcBoOPS6BWAvJT8y+U7h9yPl2XuDKWA kDOlnS0YnVXfFHt1Kbaz6owg+89pIMMgTzhenV6VNTDr1nVxaaD3AktL1nFRwMB49/c/ R4Lp+rwaA7++QGKZmDVHdD9U8pOLpQX8TuqWVNxpC/gPxd07tVpUgPS/nLS1lmwwT3R+ +lLg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1704806145; x=1705410945; 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=2NaywD19BKq4ohQgyIw/7jbUOkEmsBbsO8DVfOXHTKw=; b=DjmgvCAQICSxzXDEYXEto7EhOEh+LurA1ZMVUGwGh5VECAakKe4hE4eMRmxcfD5thH T7YiUnCjgwtQ9znMDb0cEXoIvnLbWhGMX4FlruVs2qZO3pROMScPbN/eJYoBYsBs5xv3 OWKbvG0FJvsqLAy8YA6wCD1H6KTsfRxIMVcalIho+LIJRCkMrP5fv/Kg/Gvb4Y8SbSfP a/8F7xXplCgmjei9yGlwPCSyq3ExEMRgs46nmMQtDXa4Qi/rAOMxY7cdphjDs5il9iDY 6rgJovqgy3n8/lX7l8vrsKpGmgRrmdY8gme1aoi/gUrhvxHfm5yeyDreAomfYD3TV3ND 9+EA== X-Gm-Message-State: AOJu0Yz+1bVC5W14tTNKJItaOPGK8BZDoozBwr1OOxktpVBPJv1IVVcX GQMkvhToSdyARiaowd96Af1UbcZY35A89ZIhTaZiN9VlDQ== X-Received: by 2002:a05:600c:348d:b0:40e:4872:c12f with SMTP id a13-20020a05600c348d00b0040e4872c12fmr1303121wmq.64.1704806145442; Tue, 09 Jan 2024 05:15:45 -0800 (PST) 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 r14-20020a05600c35ce00b0040e48abec33sm6005783wmq.45.2024.01.09.05.15.44 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 09 Jan 2024 05:15:45 -0800 (PST) From: =?utf-8?q?Marc_Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [COMMITTED] ada: Remove side effects depending on the context of subtype declaration Date: Tue, 9 Jan 2024 14:15:44 +0100 Message-ID: <20240109131544.744378-1-poulhies@adacore.com> X-Mailer: git-send-email 2.43.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.7 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.30 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org X-getmail-retrieved-from-mailbox: INBOX X-GMAIL-THRID: 1787619109496773026 X-GMAIL-MSGID: 1787619109496773026 From: Piotr Trojanek In GNATprove mode the removal of side effects is only needed in certain syntactic contexts, which include subtype declarations. Now this removal is limited to genuine subtype declarations and not to itypes coming from expressions where side effects are not expected. gcc/ada/ * exp_util.adb (Possible_Side_Effect_In_SPARK): Refine handling of itype declarations. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/exp_util.adb | 74 +++++++++++++++++++++++++++++++++++++------- 1 file changed, 63 insertions(+), 11 deletions(-) diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb index b9346a9f405..1df63ed38c8 100644 --- a/gcc/ada/exp_util.adb +++ b/gcc/ada/exp_util.adb @@ -12012,19 +12012,71 @@ package body Exp_Util is function Possible_Side_Effect_In_SPARK (Exp : Node_Id) return Boolean is begin - -- Side-effect removal in SPARK should only occur when not inside a - -- generic and not doing a preanalysis, inside an object renaming or - -- a type declaration or a for-loop iteration scheme. + -- Side-effect removal in SPARK should only occur when not inside a + -- generic and not doing a preanalysis, inside an object renaming or + -- a type declaration or a for-loop iteration scheme. - return not Inside_A_Generic + if not Inside_A_Generic and then Full_Analysis - and then Nkind (Enclosing_Declaration (Exp)) in - N_Component_Declaration - | N_Full_Type_Declaration - | N_Iterator_Specification - | N_Loop_Parameter_Specification - | N_Object_Renaming_Declaration - | N_Subtype_Declaration; + then + + case Nkind (Enclosing_Declaration (Exp)) is + when N_Component_Declaration + | N_Full_Type_Declaration + | N_Iterator_Specification + | N_Loop_Parameter_Specification + | N_Object_Renaming_Declaration + => + return True; + + -- If the expression belongs to an itype declaration, then + -- check if side effects are allowed in the original + -- associated node. + + when N_Subtype_Declaration => + declare + Subt : constant Entity_Id := + Defining_Identifier (Enclosing_Declaration (Exp)); + begin + if Is_Itype (Subt) then + + -- When this routine is called while the itype + -- is being created, the entity might not yet be + -- decorated with the associated node, but should + -- have the related expression. + + if Present (Associated_Node_For_Itype (Subt)) then + return + Possible_Side_Effect_In_SPARK + (Associated_Node_For_Itype (Subt)); + + elsif Present (Related_Expression (Subt)) then + return + Possible_Side_Effect_In_SPARK + (Related_Expression (Subt)); + + -- When the itype doesn't have any indication of its + -- origin (which currently only happens for packed + -- array types created by freezing that shouldn't + -- be picked by GNATprove anyway), then we can + -- conservatively assume that the expression can + -- be kept as it appears in the source code. + + else + pragma Assert (Is_Packed_Array_Impl_Type (Subt)); + return False; + end if; + else + return True; + end if; + end; + + when others => + return False; + end case; + else + return False; + end if; end Possible_Side_Effect_In_SPARK; -- Local variables