From patchwork Mon May 9 09:30:32 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 53641 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 830B6384B0CC for ; Mon, 9 May 2022 09:51:40 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 830B6384B0CC DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1652089900; bh=+M2j87/vcgZy6HZWcHpBuBqCVDsfR0F2OE20xxxfyT8=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=DqxnfmKsFI+1hWUmG5Jncy4+X0kTxQnmFyA2PvcdsqSREbOBcgKB35mHOR/R5h4ct Tv4DmOmoXdjwsyYUWpjGn+A91/fvG3xpFUdxFiWrqSQZSSzn7Ooux3KQkTEq2WX0tz 3dgnflGzDIN1x0Ct8Idd551R68sr7WCVpkIzWmkc= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x332.google.com (mail-wm1-x332.google.com [IPv6:2a00:1450:4864:20::332]) by sourceware.org (Postfix) with ESMTPS id C323F3856254 for ; Mon, 9 May 2022 09:30:33 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org C323F3856254 Received: by mail-wm1-x332.google.com with SMTP id n126-20020a1c2784000000b0038e8af3e788so7902718wmn.1 for ; Mon, 09 May 2022 02:30:33 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=+M2j87/vcgZy6HZWcHpBuBqCVDsfR0F2OE20xxxfyT8=; b=c13WWSJgmhLPiMkRbAvi19eXQrXh+Q35sxv5U/lRZV0pdOUeixboYwmS/whUCjTn/7 WpGWGmHLdMDap1S5HhPdQaNvVlz+5CZcnqL5IxttUsACSg1GcsqYxFAdiW5oEmZ7Fiee AQYlMuRqSuTyhyFM7IRJoiRQtnBxLVFx+q/KfTJNLxfFoQZLDwIjFno0J4xtPN9FTjFf 20qvT+bDmuYLq58yGTvHDyy81B3IjLXvZGxBHN/w+tO30Xw0o08vRQ4tZZtI3guxWVrJ xJ++9Eyqo/c/5lK0N0nKrxJotHKPxXLKupPnvHTZ3i1pXlA/IhgCOti0eJDs7WLrem+V r0SQ== X-Gm-Message-State: AOAM530WLYQq5xh1HCygOKBNjpwSNRrOMxW1xLwc5udBmZypNqV5Ku7g RsIWnTw8ODcGyVlqMbCRinqeD3nAdXkimg== X-Google-Smtp-Source: ABdhPJztCj1dPnelBcthjCLavMRs5usWAvWOQIRVIUneUg26clWRI82BVgeYDNLji2M24eBqLY2jiw== X-Received: by 2002:a1c:a301:0:b0:392:9bc5:203c with SMTP id m1-20020a1ca301000000b003929bc5203cmr15212525wme.67.1652088633289; Mon, 09 May 2022 02:30:33 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id b17-20020adff911000000b0020c5253d8casm10555552wrr.22.2022.05.09.02.30.32 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 09 May 2022 02:30:32 -0700 (PDT) Date: Mon, 9 May 2022 09:30:32 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Prevent inlining-for-proof for calls inside ELSIF condition Message-ID: <20220509093032.GA3184496@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-12.7 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.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) 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: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Piotr Trojanek Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org Sender: "Gcc-patches" In GNATprove we don't want inlining-for-proof to expand subprogram bodies into actions attached to nodes. These actions are attached either to expressions or to statements. For expressions, we prevented inlining by Is_Potentially_Unevaluated. For statements, we prevented inlining by In_While_Loop_Condition, but forgot about actions attached to ELSIF condition. There are no other expression or statements nodes where actions could be attached, so this fix is exhaustive. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * sem_util.ads (In_Statement_Condition_With_Actions): Renamed from In_While_Loop_Condition; move to fit the alphabetic order. * sem_util.adb (In_Statement_Condition_With_Actions): Detect Elsif condition; stop search on other statements; prevent search from going too far; move to fit the alphabetic order. * sem_res.adb (Resolve_Call): Adapt caller. diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -7346,7 +7346,7 @@ package body Sem_Res is -- loops, as this would create complex actions inside -- the condition, that are not handled by GNATprove. - elsif In_While_Loop_Condition (N) then + elsif In_Statement_Condition_With_Actions (N) then Cannot_Inline ("cannot inline & (in while loop condition)?", N, Nam_UA); diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -14986,41 +14986,58 @@ package body Sem_Util is return False; end In_Return_Value; - --------------------- - -- In_Visible_Part -- - --------------------- - - function In_Visible_Part (Scope_Id : Entity_Id) return Boolean is - begin - return Is_Package_Or_Generic_Package (Scope_Id) - and then In_Open_Scopes (Scope_Id) - and then not In_Package_Body (Scope_Id) - and then not In_Private_Part (Scope_Id); - end In_Visible_Part; - - ----------------------------- - -- In_While_Loop_Condition -- - ----------------------------- + ----------------------------------------- + -- In_Statement_Condition_With_Actions -- + ----------------------------------------- - function In_While_Loop_Condition (N : Node_Id) return Boolean is + function In_Statement_Condition_With_Actions (N : Node_Id) return Boolean is Prev : Node_Id := N; P : Node_Id := Parent (N); -- P and Prev will be used for traversing the AST, while maintaining an -- invariant that P = Parent (Prev). begin - loop - if No (P) then - return False; - elsif Nkind (P) = N_Iteration_Scheme + while Present (P) loop + if Nkind (P) = N_Iteration_Scheme and then Prev = Condition (P) then return True; - else - Prev := P; - P := Parent (P); + + elsif Nkind (P) = N_Elsif_Part + and then Prev = Condition (P) + then + return True; + + -- No point in going beyond statements + + elsif Nkind (N) in N_Statement_Other_Than_Procedure_Call + | N_Procedure_Call_Statement + then + exit; + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (P) then + exit; end if; + + Prev := P; + P := Parent (P); end loop; - end In_While_Loop_Condition; + + return False; + end In_Statement_Condition_With_Actions; + + --------------------- + -- In_Visible_Part -- + --------------------- + + function In_Visible_Part (Scope_Id : Entity_Id) return Boolean is + begin + return Is_Package_Or_Generic_Package (Scope_Id) + and then In_Open_Scopes (Scope_Id) + and then not In_Package_Body (Scope_Id) + and then not In_Private_Part (Scope_Id); + end In_Visible_Part; -------------------------------- -- Incomplete_Or_Partial_View -- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -1723,14 +1723,18 @@ package Sem_Util is -- This version is more efficient than calling the single root version of -- Is_Subtree twice. + function In_Statement_Condition_With_Actions (N : Node_Id) return Boolean; + -- Returns true if the expression N occurs within the condition of a + -- statement node with actions. Subsidiary to inlining for GNATprove, where + -- inlining of function calls in such expressions would expand the called + -- body into actions list of the condition node. GNATprove cannot yet cope + -- with such a complex AST. + function In_Visible_Part (Scope_Id : Entity_Id) return Boolean; -- Determine whether a declaration occurs within the visible part of a -- package specification. The package must be on the scope stack, and the -- corresponding private part must not. - function In_While_Loop_Condition (N : Node_Id) return Boolean; - -- Returns true if the expression N occurs within the condition of a while - function Incomplete_Or_Partial_View (Id : Entity_Id) return Entity_Id; -- Given the entity of a constant or a type, retrieve the incomplete or -- partial view of the same entity. Note that Id may not have a partial