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: 1884456 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@legolas.ozlabs.org Authentication-Results: legolas.ozlabs.org; dkim=pass (2048-bit key; secure) header.d=adacore.com header.i=@adacore.com header.a=rsa-sha256 header.s=google header.b=U8aO+GJm; dkim-atps=neutral Authentication-Results: legolas.ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=2620:52:3:1:0:246e:9693:128c; helo=server2.sourceware.org; envelope-from=gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=patchwork.ozlabs.org) Received: from server2.sourceware.org (server2.sourceware.org [IPv6:2620:52:3:1:0:246e:9693:128c]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature ECDSA (secp384r1) server-digest SHA384) (No client certificate requested) by legolas.ozlabs.org (Postfix) with ESMTPS id 4T8WkV6Skjz1yP3 for ; Wed, 10 Jan 2024 00:20:02 +1100 (AEDT) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id C2B313861896 for ; Tue, 9 Jan 2024 13:20:00 +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-Google-Smtp-Source: AGHT+IGcevUj8cF+iNSOFHe35qAcplvKtU7WCuvBOo4IMNhIRvKX5+pr2Rz7/RtWRmzWCdS8PnEfww== 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+incoming=patchwork.ozlabs.org@gcc.gnu.org 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