public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-545] [Ada] Allow inlining for proof inside generics
@ 2022-05-17 8:29 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-05-17 8:29 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:3c802e974955085696b6ba3ca20bcde2e2c53921
commit r13-545-g3c802e974955085696b6ba3ca20bcde2e2c53921
Author: Yannick Moy <moy@adacore.com>
Date: Fri Mar 11 11:19:37 2022 +0100
[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.
Diff:
---
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 00e0fcc58f8..c89d604aa80 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 0cc7171588a..cc10c2933e4 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 a5422aa971f..05aaac751e6 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 d0bafc6e06f..bc083359813 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 38ed14f27b3..2939394d88d 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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-05-17 8:29 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-17 8:29 [gcc r13-545] [Ada] Allow inlining for proof inside generics Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).