[gcc r14-7051] ada: Remove side effects depending on the context of subtype declaration

[Marc Poulhi?s]

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

commit r14-7051-gda75ce88bde06bfcef2d454054f43ed430d96b00
Author: Piotr Trojanek <trojanek@adacore.com>
Date:   Mon Dec 4 17:41:27 2023 +0100

    ada: Remove side effects depending on the context of subtype declaration
    
    In GNATprove mode the removal of side effects is only needed in certain
    syntactic contexts, which include subtype declarations. Now this removal
    is limited to genuine subtype declarations and not to itypes coming from
    expressions where side effects are not expected.
    
    gcc/ada/
    
            * exp_util.adb (Possible_Side_Effect_In_SPARK): Refine handling of
            itype declarations.

Diff:
---
 gcc/ada/exp_util.adb | 74 ++++++++++++++++++++++++++++++++++++++++++++--------
 1 file changed, 63 insertions(+), 11 deletions(-)

diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index b9346a9f405..1df63ed38c8 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -12012,19 +12012,71 @@ package body Exp_Util is
 
       function Possible_Side_Effect_In_SPARK (Exp : Node_Id) return Boolean is
       begin
-        --  Side-effect removal in SPARK should only occur when not inside a
-        --  generic and not doing a preanalysis, inside an object renaming or
-        --  a type declaration or a for-loop iteration scheme.
+         --  Side-effect removal in SPARK should only occur when not inside a
+         --  generic and not doing a preanalysis, inside an object renaming or
+         --  a type declaration or a for-loop iteration scheme.
 
-         return not Inside_A_Generic
+         if not Inside_A_Generic
            and then Full_Analysis
-           and then Nkind (Enclosing_Declaration (Exp)) in
-                      N_Component_Declaration
-                    | N_Full_Type_Declaration
-                    | N_Iterator_Specification
-                    | N_Loop_Parameter_Specification
-                    | N_Object_Renaming_Declaration
-                    | N_Subtype_Declaration;
+         then
+
+            case Nkind (Enclosing_Declaration (Exp)) is
+               when N_Component_Declaration
+                  | N_Full_Type_Declaration
+                  | N_Iterator_Specification
+                  | N_Loop_Parameter_Specification
+                  | N_Object_Renaming_Declaration
+               =>
+                  return True;
+
+               --  If the expression belongs to an itype declaration, then
+               --  check if side effects are allowed in the original
+               --  associated node.
+
+               when N_Subtype_Declaration =>
+                  declare
+                     Subt : constant Entity_Id :=
+                       Defining_Identifier (Enclosing_Declaration (Exp));
+                  begin
+                     if Is_Itype (Subt) then
+
+                        --  When this routine is called while the itype
+                        --  is being created, the entity might not yet be
+                        --  decorated with the associated node, but should
+                        --  have the related expression.
+
+                        if Present (Associated_Node_For_Itype (Subt)) then
+                           return
+                             Possible_Side_Effect_In_SPARK
+                               (Associated_Node_For_Itype (Subt));
+
+                        elsif Present (Related_Expression (Subt)) then
+                           return
+                             Possible_Side_Effect_In_SPARK
+                               (Related_Expression (Subt));
+
+                        --  When the itype doesn't have any indication of its
+                        --  origin (which currently only happens for packed
+                        --  array types created by freezing that shouldn't
+                        --  be picked by GNATprove anyway), then we can
+                        --  conservatively assume that the expression can
+                        --  be kept as it appears in the source code.
+
+                        else
+                           pragma Assert (Is_Packed_Array_Impl_Type (Subt));
+                           return False;
+                        end if;
+                     else
+                        return True;
+                     end if;
+                  end;
+
+               when others =>
+                  return False;
+            end case;
+         else
+            return False;
+         end if;
       end Possible_Side_Effect_In_SPARK;
 
       --  Local variables