[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 --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 00e0fcc58f8352c60e5e75c7dbea0ba54d897198..c89d604aa8098224b9a713581e1c6125b9789d63 100644 (file)
--- 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 0cc7171588a7fbbdc06d1ab553ecb5b9aafb4cc1..cc10c2933e4dec98af4f402d632a38a206ffdada 100644 (file)
--- 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 a5422aa971f62ea86832986b927bb80e5496a6db..05aaac751e6120987a6a22007d3e618132cfb546 100644 (file)
--- 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 d0bafc6e06f0cfb3e8b37297fc275ab9b0ab2baa..bc083359813a6fd7fc63bfb5f11340e0d6695e54 100644 (file)
--- 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 38ed14f27b387715b932ef5d9702ca49e973d407..2939394d88d7f743ab114273ce6b8a283df3a668 100644 (file)
--- 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