From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-lj1-x229.google.com (mail-lj1-x229.google.com [IPv6:2a00:1450:4864:20::229]) by sourceware.org (Postfix) with ESMTPS id B74C038582B7 for ; Tue, 1 Aug 2023 08:08:25 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org B74C038582B7 Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com Received: by mail-lj1-x229.google.com with SMTP id 38308e7fff4ca-2b9e6cc93c6so30863591fa.2 for ; Tue, 01 Aug 2023 01:08:25 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1690877304; x=1691482104; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=NNu+dPpBNoX4bm4XAsb+9uChXAiS/qv6mulnulUl2c0=; b=A7JDzmNjDxdJNEK4REJULk7lircWh9yBoetOt0Y13b7TzBfO/tPE/yBxDtRQKjlv48 9ZkqzpgRW8X8worTPcesfCUNwyh7qxPMoUL4KodCBEYXJcHicsA3A2bp5ezmuMaMv4yW beZ7Y79Rxv1S16Rm+7QzdXUB/K0WJ/XXxf7jhsfDqBc5OZQN0U8AW/E5s5W07sz/pF8o hQJT8qfsk2h5lzgqDpLtaV+WFFuFnCfDp3Pj0ytHshtCh49tXsNwdpuCAqk2gLjJCeQZ ZcjCEGDHv79n5AAj1TYNsq4/AdkqE6NOeZZ+rPpGVnSNTT6LgWcvnJAWAm/s3dihpyFF 8uCQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1690877304; x=1691482104; 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=NNu+dPpBNoX4bm4XAsb+9uChXAiS/qv6mulnulUl2c0=; b=aBqJ/OcYMrnx+J+/xRi1qHEFT+nGM2k8RkyyTMKsGx4xez1no2PaPgE5CEiXWsDezv ixutN/XMbYiZf8saTXmDI2LlnsyZYJQYTe6IipCYE9zKhDMOjyWBKyjqRLkwZHR4iT/e 3TESksheOmh0Q2IiIq2f8bK0nc2XZwjhoPqDHr6m/SFff2y8AbPvPXXi6KFQRJ1HuNV4 OuuiTqAozgFYLF6CHpJ5xxexy+TEeaM7khNGLUkQxOarwhh/w5lIXgl24Y/QV4EEx84v H3bxnhe0NdDNAZ6cxfD84/VLb8CUF5kGEBpXP/4R4TBW3/IdpTThfX24TqkObeWncPP9 rzaQ== X-Gm-Message-State: ABy/qLaIp7NlGsn9Ly9hFyl2Q7/C/AJ1hGjcks/G2eu8cC9Mq1frc4hS twAUv+AxAIEb5weXdfYZGRj0OldaKMCQLZPRlkCmcA== X-Google-Smtp-Source: APBJJlHNt7uiHaP3hMitrFdTGW8F6oNHBJPbEXjZ9MdfjqDDt79md3Jp7mKPoItnvXpLi0Ilsy6NEw== X-Received: by 2002:a2e:9c82:0:b0:2b6:e2aa:8fc2 with SMTP id x2-20020a2e9c82000000b002b6e2aa8fc2mr1672950lji.46.1690877304092; Tue, 01 Aug 2023 01:08:24 -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 d14-20020adff2ce000000b003176053506fsm11629314wrp.99.2023.08.01.01.08.23 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 01 Aug 2023 01:08:23 -0700 (PDT) From: =?UTF-8?q?Marc=20Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Disable inlining of subprograms with Skip(_Flow_And)_Proof in GNATprove Date: Tue, 1 Aug 2023 10:08:21 +0200 Message-Id: <20230801080821.2271747-1-poulhies@adacore.com> X-Mailer: git-send-email 2.40.0 MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Status: No, score=-13.3 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 List-Id: From: Yannick Moy Subprograms with these Skip(_Flow_And)_Proof annotations should not be inlined in GNATprove, as we want to skip part of the analysis for their body. gcc/ada/ * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Check for Skip_Proof and Skip_Flow_And_Proof annotations for deciding whether a subprogram can be inlined. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/inline.adb | 49 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 49 insertions(+) diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index edb90a9fe20..db8b4164e87 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1503,6 +1503,10 @@ package body Inline is -- an unconstrained record type with per-object constraints on component -- types. + function Has_Skip_Proof_Annotation (Id : Entity_Id) return Boolean; + -- Returns True if subprogram Id has an annotation Skip_Proof or + -- Skip_Flow_And_Proof. + function Has_Some_Contract (Id : Entity_Id) return Boolean; -- Return True if subprogram Id has any contract. The presence of -- Extensions_Visible or Volatile_Function is also considered as a @@ -1701,6 +1705,45 @@ package body Inline is return False; end Has_Formal_With_Discriminant_Dependent_Fields; + ------------------------------- + -- Has_Skip_Proof_Annotation -- + ------------------------------- + + function Has_Skip_Proof_Annotation (Id : Entity_Id) return Boolean is + Decl : Node_Id := Unit_Declaration_Node (Id); + + begin + Next (Decl); + + while Present (Decl) + and then Nkind (Decl) = N_Pragma + loop + if Get_Pragma_Id (Decl) = Pragma_Annotate + and then List_Length (Pragma_Argument_Associations (Decl)) = 3 + then + declare + Arg1 : constant Node_Id := + First (Pragma_Argument_Associations (Decl)); + Arg2 : constant Node_Id := Next (Arg1); + Arg1_Name : constant String := + Get_Name_String (Chars (Get_Pragma_Arg (Arg1))); + Arg2_Name : constant String := + Get_Name_String (Chars (Get_Pragma_Arg (Arg2))); + begin + if Arg1_Name = "gnatprove" + and then Arg2_Name in "skip_proof" | "skip_flow_and_proof" + then + return True; + end if; + end; + end if; + + Next (Decl); + end loop; + + return False; + end Has_Skip_Proof_Annotation; + ----------------------- -- Has_Some_Contract -- ----------------------- @@ -1903,6 +1946,12 @@ package body Inline is elsif Maybe_Traversal_Function (Id) then return False; + -- Do not inline subprograms with the Skip_Proof or Skip_Flow_And_Proof + -- annotation, which should be handled separately. + + elsif Has_Skip_Proof_Annotation (Id) then + return False; + -- Otherwise, this is a subprogram declared inside the private part of a -- package, or inside a package body, or locally in a subprogram, and it -- does not have any contract. Inline it. -- 2.40.0