[gcc r15-1268] ada: Do not inline subprogram which could cause SPARK violation

[Marc Poulhi?s]

https://gcc.gnu.org/g:df9d6153e1981676b08109fbe3371ca6e9d5f755

commit r15-1268-gdf9d6153e1981676b08109fbe3371ca6e9d5f755
Author: Yannick Moy <moy@adacore.com>
Date:   Tue Apr 23 13:16:51 2024 +0200

    ada: Do not inline subprogram which could cause SPARK violation
    
    Inlining in GNATprove a subprogram containing a constant declaration with
    an address clause/aspect might lead to a spurious error if the address
    expression is based on a constant view of a mutable object at call site.
    Do not allow such inlining in GNATprove.
    
    gcc/ada/
    
            * inline.adb (Can_Be_Inlined_In_GNATprove_Mode): Do not inline
            when constant with address clause is found.

Diff:
---
 gcc/ada/inline.adb | 83 +++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 82 insertions(+), 1 deletion(-)

diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 04cf1194009d..8e98fb5ad101 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -1094,7 +1094,6 @@ package body Inline is
       --  If the body of the subprogram includes a call that returns an
       --  unconstrained type, the secondary stack is involved, and it is
       --  not worth inlining.
-
       -------------------------
       -- Has_Extended_Return --
       -------------------------
@@ -1462,6 +1461,14 @@ package body Inline is
      (Spec_Id : Entity_Id;
       Body_Id : Entity_Id) return Boolean
    is
+      function Has_Constant_With_Address_Clause
+        (Body_Node : Node_Id)
+         return Boolean;
+      --  Returns true if the subprogram contains a declaration of a constant
+      --  with an address clause, which could become illegal in SPARK after
+      --  inlining, if the address clause mentions a constant view of a mutable
+      --  object at call site.
+
       function Has_Formal_Or_Result_Of_Deep_Type
         (Id : Entity_Id) return Boolean;
       --  Returns true if the subprogram has at least one formal parameter or
@@ -1502,6 +1509,70 @@ package body Inline is
       --  knowledge of the SPARK boundary is needed to determine exactly
       --  traversal functions.
 
+      --------------------------------------
+      -- Has_Constant_With_Address_Clause --
+      --------------------------------------
+
+      function Has_Constant_With_Address_Clause
+        (Body_Node : Node_Id)
+         return Boolean
+      is
+         function Check_Constant_With_Addresss_Clause
+           (N : Node_Id)
+            return Traverse_Result;
+         --  Returns Abandon on node N if this is a declaration of a constant
+         --  object with an address clause.
+
+         -----------------------------------------
+         -- Check_Constant_With_Addresss_Clause --
+         -----------------------------------------
+
+         function Check_Constant_With_Addresss_Clause
+           (N : Node_Id)
+            return Traverse_Result
+         is
+         begin
+            case Nkind (N) is
+               when N_Object_Declaration =>
+                  declare
+                     Obj : constant Entity_Id := Defining_Entity (N);
+                  begin
+                     if Constant_Present (N)
+                       and then
+                         (Present (Address_Clause (Obj))
+                            or else Has_Aspect (Obj, Aspect_Address))
+                     then
+                        return Abandon;
+                     else
+                        return OK;
+                     end if;
+                  end;
+
+               --  Skip locally declared subprogram bodies inside the body to
+               --  inline, as the declarations inside those do not count.
+
+               when N_Subprogram_Body =>
+                  if N = Body_Node then
+                     return OK;
+                  else
+                     return Skip;
+                  end if;
+
+               when others =>
+                  return OK;
+            end case;
+         end Check_Constant_With_Addresss_Clause;
+
+         function Check_All_Constants_With_Address_Clause is new
+           Traverse_Func (Check_Constant_With_Addresss_Clause);
+
+      --  Start of processing for Has_Constant_With_Address_Clause
+
+      begin
+         return Check_All_Constants_With_Address_Clause
+           (Body_Node) = Abandon;
+      end Has_Constant_With_Address_Clause;
+
       ---------------------------------------
       -- Has_Formal_Or_Result_Of_Deep_Type --
       ---------------------------------------
@@ -2009,6 +2080,16 @@ package body Inline is
       elsif Has_Hide_Unhide_Annotation (Spec_Id, Body_Id) then
          return False;
 
+      --  Do not inline subprograms containing constant declarations with an
+      --  address clause, as inlining could lead to a spurious violation of
+      --  SPARK rules.
+
+      elsif Present (Body_Id)
+        and then
+          Has_Constant_With_Address_Clause (Unit_Declaration_Node (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.