From patchwork Tue Jan 9 13:15:42 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: 186380 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a05:7300:2411:b0:101:2151:f287 with SMTP id m17csp102774dyi; Tue, 9 Jan 2024 05:23:19 -0800 (PST) X-Google-Smtp-Source: AGHT+IFE46mt8KFPWc/AaJD1H2/zA8a/Fs0VoBYAfiCDFDCMncsyOL8ccpVaTGcSdoH6pYs3dfrM X-Received: by 2002:a4a:b087:0:b0:598:1fa3:80b9 with SMTP id k7-20020a4ab087000000b005981fa380b9mr3205004oon.14.1704806599466; Tue, 09 Jan 2024 05:23:19 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1704806599; cv=pass; d=google.com; s=arc-20160816; b=s1pxf+iJ6dIkHxQan43QBmGRNy8+OD8xThaDg3WNE8ro5fi3BNkKWM6WicVI82+t2F /p1qAkMCySGihIt8ojUdDSeHJk0De8mgFiD3Jjz/z54Xr8vBFtAjDrElodQH7lNnSt3i +dLuzJzxk5BxeZxPMWsjgPhgXQHAQm7dElzOSOAsLkmRTFG2YMjuzC3fzS5t5REIu4jz uaC6MGBsGIGY4UeYutpXtWYpLMxsfSUXzomNW+4nzGHG4/DBsBsO52k4KF9QoaD+EZ6z pE5/ho8csOqkVJAhfn4BMm1Q8/oGCUH1svsjKNby/ECPEP8Eo9F7dX+Wz8+PMPrc805E iC7w== 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=DQRJ/Zc3Lf1RM0VnBGaFrDbvW5G+2fkGHCTXiWvuRQg=; fh=QRb7QY4BZ0mIIAPiH2G4K0PcYKRtRn2i5A6VLUA8cN4=; b=KMJ5EIKM3QB1+mlcm/Kmxh/PJ3UGPYthflTJzmq2RBK0a0qzF5s8pxgYz4tMpWvyAc MrtYzZXZBGWoM5a2R0rX8exzfow6LSJuhY04YIwSIzYeFSvinAy0CI0xYXYErFO+9Jaq j0pAGKzJ+gKaNH80i9mxCx4ZAfkZCpqooGzbZSXZLMs3IvA240rwYRz4fY614ciVq3XO 1OJ/+z5piqUsgB33tN/Lw26S1EL0ciDuimNMsVe00T4+qCdN2nPspq1uGTJS4jfLlCWS aZhDql2Vmigrdo2ZphU5wS0I1F0g5tec75P3ZmnjYe//9U/WjoibMMTIZWm8/pKJP7ZY TNVw== ARC-Authentication-Results: i=2; mx.google.com; dkim=pass header.i=@adacore.com header.s=google header.b=dd0Hwytf; arc=pass (i=1); spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 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. [8.43.85.97]) by mx.google.com with ESMTPS id o1-20020a05622a008100b00427e8bb628csi2061879qtw.447.2024.01.09.05.23.19 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 09 Jan 2024 05:23:19 -0800 (PST) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 as permitted sender) client-ip=8.43.85.97; Authentication-Results: mx.google.com; dkim=pass header.i=@adacore.com header.s=google header.b=dd0Hwytf; arc=pass (i=1); spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 8.43.85.97 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 AF6243861845 for ; Tue, 9 Jan 2024 13:23:18 +0000 (GMT) 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 2500B3857C79 for ; Tue, 9 Jan 2024 13:15:45 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 2500B3857C79 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 2500B3857C79 Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::334 ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1704806148; cv=none; b=CmNHtno5gNUyDAPzWxE5pJCERBt/Fs4vIYPBjuL1oXbUOM6Ei12VAmhiqesKt5sOJKTtUlu9zjMttEIzQshn9i8vcfUzShzlescsrNoXS2ehndRhLIwoGxr4eOPfcMTrz2UGg2yjDZqsKdFPcqBOSYi4vQQAxWQB6LS6H8ri6PM= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1704806148; c=relaxed/simple; bh=eQ5mpdGEsccVogB84Q9nYsTZzr7DmER9J7+mM+JBVSA=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=Si/Q+kkWjYQMCSEuiJ1Z2LnTHgEBmCf172/D8IWWqYBzmvXPLLq7qKFknpgprHQXW4hjYqnnt+7AHMO2s0uXwUE+yROPKsc6pCQNzF4OINg8EgkOyTUhpx0889ogvTjNm8SfZ8p0/15X0cGvArymMPiTYaFO+6pgCC4ZQ6xiVxE= ARC-Authentication-Results: i=1; server2.sourceware.org Received: by mail-wm1-x334.google.com with SMTP id 5b1f17b1804b1-40e4f71288bso6267205e9.1 for ; Tue, 09 Jan 2024 05:15:45 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1704806144; x=1705410944; 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=DQRJ/Zc3Lf1RM0VnBGaFrDbvW5G+2fkGHCTXiWvuRQg=; b=dd0HwytfIp27UaPNLSY0zT+f1dg3Di7tnN6kvIhOtvO/iZcXViHDWOnVXQidRVTUAJ reh0+c5rHJw/iyP4+YEeQxJ393UpIImlmXJYdoTLAXryvbaVdXR3l6+e807W3vG2MTqm wmCcrM3XhDSnCiSjBl/by4FQFbLlRT/lgbs6Pjq3yUOh0M14A/SAB+WyjwIK6Ctauuj4 QLjERblr5M0gke4Xqd6mWS/hzhV++1tThgJYpSGhA8v+kTMB/Sr4x9+HRV5z2AUKHG1g VY7FEoI4aNaBo694/1e4Vt1Am5Evm0kCrcvFeUbFzcNmaNA6zBUzB86jlU+DVLOO9DVy 1+Wg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1704806144; x=1705410944; 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=DQRJ/Zc3Lf1RM0VnBGaFrDbvW5G+2fkGHCTXiWvuRQg=; b=o+WrM48LNjGKGveiBw/h8vs+Fm6MWZxxX/Y1xVXCA5IXNxQm0Yi4v+c83mfWu7PDnG 5JDzopWntWXa0TOZGljGCfeG1E94FYdtiiUGAAS4w1ZRPnZKE4UXuUXOQ5WsOnqcHlSS bAw34nOrtQkIX+xglS6dDCUcSB2axrS1+a+TCW8UlimAj0/5U+epFStLnCacBuzmMKP/ wkJCx0O5HqvKH8HG3vI5mlCM3NjAvXNfKxfHaKDupNVKzqDmL/CatsklL8wDgbXtfZRt seWCvkgNxB5WVBDAD7B1DRdwc6wyfo+UEMDto+iswy789k9pfFiBYqcvBL7S8gf+ld0v IVVg== X-Gm-Message-State: AOJu0YzOHGEBV6f72KRpEEgMN0s/hHozjMwcN7zti9FLiyRF6ywzmJ5S FjX5sTHKui5L8QA3CSvs7Ay39G9yfArHoy8//eUR/nQjFg== X-Received: by 2002:a05:600c:4e90:b0:40d:7822:bf54 with SMTP id f16-20020a05600c4e9000b0040d7822bf54mr1913186wmq.132.1704806143936; Tue, 09 Jan 2024 05:15:43 -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 f13-20020a05600c154d00b0040e3635ca65sm14890980wmg.2.2024.01.09.05.15.43 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 09 Jan 2024 05:15:43 -0800 (PST) From: =?utf-8?q?Marc_Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [COMMITTED] ada: More aggressive inlining of subprogram calls in GNATprove mode Date: Tue, 9 Jan 2024 14:15:42 +0100 Message-ID: <20240109131542.744317-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: 1787619284854732792 X-GMAIL-MSGID: 1787619284854732792 From: Piotr Trojanek Previously if a subprogram call could not be inlined in GNATprove mode, then all subsequent calls to the same subprogram were not inlined either (because a failed attempt to inline clears flag Is_Inlined_Always and we tested this flag when attempting to inline subsequent calls). Now a failure in inlining of a particular call does not prevent inlining of subsequent calls to the same subprogram, except when inlining failed because the subprogram was detected to be recursive (which clears the Is_Inlined flag that we now examine). This change allows more checks to be proved and reduces interactions between inlining and SPARK legality checks. gcc/ada/ * sem_ch6.adb (Analyze_Subprogram_Specification): Set Is_Inlined flag by default in GNATprove mode. * sem_res.adb (Resolve_Call): Only look at flag which is cleared when inlined subprogram is detected to be recursive. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/sem_ch6.adb | 5 ++++- gcc/ada/sem_res.adb | 11 +++++++---- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index da6f6c40c92..bdfe446d014 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -5325,10 +5325,13 @@ package body Sem_Ch6 is -- Flag Is_Inlined_Always is True by default, and reversed to False for -- those subprograms which could be inlined in GNATprove mode (because - -- Body_To_Inline is non-Empty) but should not be inlined. + -- Body_To_Inline is non-Empty) but should not be inlined. Flag + -- Is_Inlined is True by default and reversed to False when inlining + -- fails because the subprogram is detected to be recursive. if GNATprove_Mode then Set_Is_Inlined_Always (Designator); + Set_Is_Inlined (Designator); end if; -- Introduce new scope for analysis of the formals and the return type diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index d81a5af9032..cfcbb94af89 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7193,7 +7193,7 @@ package body Sem_Res is -- In GNATprove mode, expansion is disabled, but we want to inline some -- subprograms to facilitate formal verification. Indirect calls through -- a subprogram type or within a generic cannot be inlined. Inlining is - -- performed only for calls subject to SPARK_Mode on. + -- performed only for calls subject to SPARK_Mode => On. elsif GNATprove_Mode and then SPARK_Mode = On @@ -7206,10 +7206,13 @@ package body Sem_Res is if Nkind (Nam_Decl) = N_Subprogram_Declaration then Body_Id := Corresponding_Body (Nam_Decl); - -- Nothing to do if the subprogram is not eligible for inlining in - -- GNATprove mode, or inlining is disabled with switch -gnatdm + -- Nothing to do if the subprogram is not inlined (because it is + -- recursive, directly or indirectly), or is not eligible for + -- inlining GNATprove mode (because of properties of the + -- subprogram itself), or inlining has been disabled with switch + -- -gnatdm. - if not Is_Inlined_Always (Nam_UA) + if not Is_Inlined (Nam_UA) or else not Can_Be_Inlined_In_GNATprove_Mode (Nam_UA, Body_Id) or else Debug_Flag_M then