From 3c802e974955085696b6ba3ca20bcde2e2c53921 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 11 Mar 2022 11:19:37 +0100 Subject: [PATCH] [Ada] Allow inlining for proof inside generics For local subprograms without contracts inside generics, allow their inlining for proof in GNATprove mode. This requires forbidding the inlining of subprograms which contain references to object renamings, which would be replaced in the SPARK expansion and violate assumptions of the inlining code. gcc/ada/ * exp_spark.adb (Expand_SPARK_Potential_Renaming): Deal with no entity case. * inline.ads (Check_Object_Renaming_In_GNATprove_Mode): New procedure. * inline.adb (Check_Object_Renaming_In_GNATprove_Mode): New procedure. (Can_Be_Inlined_In_GNATprove_Mode): Remove case forbidding inlining for subprograms inside generics. * sem_ch12.adb (Copy_Generic_Node): Preserve global entities when inlining in GNATprove mode. * sem_ch6.adb (Analyse_Subprogram_Body_Helper): Remove body to inline if renaming is detected in GNATprove mode. --- gcc/ada/exp_spark.adb | 7 +++-- gcc/ada/inline.adb | 76 ++++++++++++++++++++++++++++++++++++++++++++++----- gcc/ada/inline.ads | 9 ++++++ gcc/ada/sem_ch12.adb | 5 +++- gcc/ada/sem_ch6.adb | 16 +++++++++++ 5 files changed, 103 insertions(+), 10 deletions(-) diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index 00e0fcc..c89d604 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -850,9 +850,12 @@ package body Exp_SPARK is -- Start of processing for Expand_SPARK_Potential_Renaming begin - -- Replace a reference to a renaming with the actual renamed object + -- Replace a reference to a renaming with the actual renamed object. + -- Protect against previous errors leaving no entity in N. - if Is_Object (Obj_Id) then + if Present (Obj_Id) + and then Is_Object (Obj_Id) + then Ren := Renamed_Object (Obj_Id); if Present (Ren) then diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb index 0cc7171..cc10c29 100644 --- a/gcc/ada/inline.adb +++ b/gcc/ada/inline.adb @@ -1893,13 +1893,6 @@ package body Inline is then return False; - -- Subprograms in generic instances are currently not inlined, as this - -- interacts badly with the expansion of object renamings in GNATprove - -- mode. - - elsif Instantiation_Location (Sloc (Id)) /= No_Location then - return False; - -- Do not inline subprograms and entries defined inside protected types, -- which typically are not helper subprograms, which also avoids getting -- spurious messages on calls that cannot be inlined. @@ -2643,6 +2636,75 @@ package body Inline is end if; end Check_And_Split_Unconstrained_Function; + --------------------------------------------- + -- Check_Object_Renaming_In_GNATprove_Mode -- + --------------------------------------------- + + procedure Check_Object_Renaming_In_GNATprove_Mode (Spec_Id : Entity_Id) is + Decl : constant Node_Id := Unit_Declaration_Node (Spec_Id); + Body_Decl : constant Node_Id := + Unit_Declaration_Node (Corresponding_Body (Decl)); + + function Check_Object_Renaming (N : Node_Id) return Traverse_Result; + -- Returns Abandon on node N if this is a reference to an object + -- renaming, which will be expanded into the renamed object in + -- GNATprove mode. + + --------------------------- + -- Check_Object_Renaming -- + --------------------------- + + function Check_Object_Renaming (N : Node_Id) return Traverse_Result is + begin + case Nkind (Original_Node (N)) is + when N_Expanded_Name + | N_Identifier + => + declare + Obj_Id : constant Entity_Id := Entity (Original_Node (N)); + begin + -- Recognize the case when SPARK expansion rewrites a + -- reference to an object renaming. + + if Present (Obj_Id) + and then Is_Object (Obj_Id) + and then Present (Renamed_Object (Obj_Id)) + and then Nkind (Renamed_Object (Obj_Id)) not in N_Entity + + -- Copy_Generic_Node called for inlining expects the + -- references to global entities to have the same kind + -- in the "generic" code and its "instantiation". + + and then Nkind (Original_Node (N)) /= + Nkind (Renamed_Object (Obj_Id)) + then + return Abandon; + else + return OK; + end if; + end; + + when others => + return OK; + end case; + end Check_Object_Renaming; + + function Check_All_Object_Renamings is new + Traverse_Func (Check_Object_Renaming); + + -- Start of processing for Check_Object_Renaming_In_GNATprove_Mode + + begin + -- Subprograms with object renamings replaced by the special SPARK + -- expansion cannot be inlined. + + if Check_All_Object_Renamings (Body_Decl) /= OK then + Cannot_Inline ("cannot inline & (object renaming)?", + Body_Decl, Spec_Id); + Set_Body_To_Inline (Decl, Empty); + end if; + end Check_Object_Renaming_In_GNATprove_Mode; + ------------------------------------- -- Check_Package_Body_For_Inlining -- ------------------------------------- diff --git a/gcc/ada/inline.ads b/gcc/ada/inline.ads index a5422aa..05aaac7 100644 --- a/gcc/ada/inline.ads +++ b/gcc/ada/inline.ads @@ -198,6 +198,15 @@ package Inline is -- cases documented in Check_Body_To_Inline) then build the body-to-inline -- associated with N and attach it to the declaration node of Spec_Id. + procedure Check_Object_Renaming_In_GNATprove_Mode (Spec_Id : Entity_Id) + with + Pre => GNATprove_Mode; + -- This procedure is called only in GNATprove mode, on subprograms for + -- which a Body_To_Inline was created, to check if the subprogram has + -- references to object renamings which will be replaced by the special + -- SPARK expansion into nodes of a different kind, which is not expected + -- by the inlining mechanism. In that case, the Body_To_Inline is deleted. + procedure Check_Package_Body_For_Inlining (N : Node_Id; P : Entity_Id); -- If front-end inlining is enabled and a package declaration contains -- inlined subprograms, load and compile the package body to collect the diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index d0bafc6..bc08335 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -8122,7 +8122,10 @@ package body Sem_Ch12 is Set_Entity (New_N, Entity (Name (Assoc))); elsif Nkind (Assoc) in N_Entity - and then Expander_Active + and then (Expander_Active or + (GNATprove_Mode + and then not In_Spec_Expression + and then not Inside_A_Generic)) then -- Inlining case: we are copying a tree that contains -- global entities, which are preserved in the copy to be diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 38ed14f..2939394 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -5459,6 +5459,22 @@ package body Sem_Ch6 is end; end; + -- Check if a Body_To_Inline was created, but the subprogram has + -- references to object renamings which will be replaced by the special + -- SPARK expansion into nodes of a different kind, which is not expected + -- by the inlining mechanism. In that case, the Body_To_Inline is + -- deleted prior to being analyzed. This check needs to take place + -- after analysis of the subprogram body. + + if GNATprove_Mode + and then Present (Spec_Id) + and then + Nkind (Unit_Declaration_Node (Spec_Id)) = N_Subprogram_Declaration + and then Present (Body_To_Inline (Unit_Declaration_Node (Spec_Id))) + then + Check_Object_Renaming_In_GNATprove_Mode (Spec_Id); + end if; + -- Check for variables that are never modified declare -- 2.7.4