From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 7871) id A42803858D1E; Mon, 6 May 2024 09:15:40 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org A42803858D1E DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1714986940; bh=BlHpeOG0BV973mfiVqAb41shkr73jfKUEqcELAaP8u8=; h=From:To:Subject:Date:From; b=O+zih3WkbK6PBlxm3fR9eAyizxST/NqWMs28OuZitdyqJpx7RBouZUg8W5uKoZK8g fhxFtvjjDnMrut2hMWkDklIHQRlVbTj01WdzEZ4sZ0+Y3f6wLin1ucsjN36gJtj/70 vAs+8fP5hbH06q9f9xeOaS8mdDkYrmsTypo6z2FE= MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Marc Poulhi?s To: gcc-cvs@gcc.gnu.org Subject: [gcc r15-173] ada: Do not inline in GNATprove the subprograms with (Un)Hide_Info X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: 8daf4eb02a2e739d5c62b94528adfddaed506a0a X-Git-Newrev: 53c32e9d7f01ee350803c9371b8630bf3e4844b7 Message-Id: <20240506091540.A42803858D1E@sourceware.org> Date: Mon, 6 May 2024 09:15:40 +0000 (GMT) List-Id: https://gcc.gnu.org/g:53c32e9d7f01ee350803c9371b8630bf3e4844b7 commit r15-173-g53c32e9d7f01ee350803c9371b8630bf3e4844b7 Author: Yannick Moy Date: Wed Dec 13 15:38:59 2023 +0100 ada: Do not inline in GNATprove the subprograms with (Un)Hide_Info The annotations Hide_Info and Unhide_Info in GNATprove are meant to give special visibility in the corresponding scope to the precise definition of some entities. Hence, such scopes should not be inlined in GNATprove. gcc/ada/ * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Adapt checking. Diff: --- gcc/ada/inline.adb | 89 ++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 86 insertions(+), 3 deletions(-) diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index f23100dbb13..2ec92ca9dff 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1503,6 +1503,12 @@ package body Inline is -- an unconstrained record type with per-object constraints on component -- types. + function Has_Hide_Unhide_Annotation + (Spec_Id, Body_Id : Entity_Id) + return Boolean; + -- Returns whether the subprogram has an annotation Hide_Info or + -- Unhide_Info on its spec or body. + 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. @@ -1705,6 +1711,76 @@ package body Inline is return False; end Has_Formal_With_Discriminant_Dependent_Fields; + -------------------------------- + -- Has_Hide_Unhide_Annotation -- + -------------------------------- + + function Has_Hide_Unhide_Annotation + (Spec_Id, Body_Id : Entity_Id) + return Boolean + is + function Has_Hide_Unhide_Pragma (Prag : Node_Id) return Boolean; + -- Return whether a pragma Hide/Unhide is present in the list of + -- pragmas starting with Prag. + + ---------------------------- + -- Has_Hide_Unhide_Pragma -- + ---------------------------- + + function Has_Hide_Unhide_Pragma (Prag : Node_Id) return Boolean is + Decl : Node_Id := Prag; + begin + 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)) = 4 + then + declare + Arg1 : constant Node_Id := + First (Pragma_Argument_Associations (Decl)); + Arg2 : constant Node_Id := Next (Arg1); + Arg1_Name : constant Name_Id := + Chars (Get_Pragma_Arg (Arg1)); + Arg2_Name : constant String := + Get_Name_String (Chars (Get_Pragma_Arg (Arg2))); + begin + if Arg1_Name = Name_Gnatprove + and then Arg2_Name in "hide_info" | "unhide_info" + then + return True; + end if; + end; + end if; + + Next (Decl); + end loop; + + return False; + end Has_Hide_Unhide_Pragma; + + begin + if Present (Spec_Id) + and then Has_Hide_Unhide_Pragma + (Next (Unit_Declaration_Node (Spec_Id))) + then + return True; + + elsif Present (Body_Id) then + declare + Subp_Body : constant N_Subprogram_Body_Id := + Unit_Declaration_Node (Body_Id); + begin + return Has_Hide_Unhide_Pragma (Next (Subp_Body)) + or else + Has_Hide_Unhide_Pragma (First (Declarations (Subp_Body))); + end; + + else + return False; + end if; + end Has_Hide_Unhide_Annotation; + ------------------------------- -- Has_Skip_Proof_Annotation -- ------------------------------- @@ -1725,12 +1801,12 @@ package body Inline is 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))); + Arg1_Name : constant Name_Id := + Chars (Get_Pragma_Arg (Arg1)); Arg2_Name : constant String := Get_Name_String (Chars (Get_Pragma_Arg (Arg2))); begin - if Arg1_Name = "gnatprove" + if Arg1_Name = Name_Gnatprove and then Arg2_Name in "skip_proof" | "skip_flow_and_proof" then return True; @@ -1952,6 +2028,13 @@ package body Inline is elsif Has_Skip_Proof_Annotation (Id) then return False; + -- Do not inline subprograms with the Hide_Info or Unhide_Info + -- annotation, since their scope has special visibility on the + -- precise definition of some entities. + + elsif Has_Hide_Unhide_Annotation (Spec_Id, Body_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.