[Ada] Move check for null array aggregates to expansion

[Ada] Move check for null array aggregates to expansion

[Marc Poulhiès]

[-- Attachment #1: Type: text/plain, Size: 655 bytes --]

Despite recent changes to runtime checks for null array aggregates,
GNATprove still struggles with N_Raise_Constraint_Error nodes inserted
into AST by aggregate resolution. The ultimate fix is to move these
checks to expansion (which is disabled in GNATprove mode) and explicitly
emit a proof check in the GNATprove backend.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* exp_aggr.adb (Check_Bounds): Move code and comment related to
	check for null array aggregate from Resolve_Null_Array_Aggregate.
	* sem_aggr.ads (Is_Null_Aggregate): Move spec from unit body.
	* sem_aggr.adb (Resolve_Null_Array_Aggregate): Move check to
	expansion.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 4278 bytes --]

diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -5734,7 +5734,8 @@ package body Exp_Aggr is
 
       procedure Check_Bounds (Aggr_Bounds_Node, Index_Bounds_Node : Node_Id);
       --  Checks that the bounds of Aggr_Bounds are within the bounds defined
-      --  by Index_Bounds.
+      --  by Index_Bounds. For null array aggregate (Ada 2022) check that the
+      --  aggregate bounds define a null range.
 
       procedure Check_Same_Aggr_Bounds (Sub_Aggr : Node_Id; Dim : Pos);
       --  Checks that in a multidimensional array aggregate all subaggregates
@@ -5850,6 +5851,22 @@ package body Exp_Aggr is
          Cond : Node_Id := Empty;
 
       begin
+         --  For a null array aggregate check that high bound (i.e., low
+         --  bound predecessor) exists. Fail if low bound is low bound of
+         --  base subtype (in all cases, including modular).
+
+         if Is_Null_Aggregate (N) then
+            Insert_Action (N,
+              Make_Raise_Constraint_Error (Loc,
+                Condition =>
+                  Make_Op_Eq (Loc,
+                    New_Copy_Tree (Aggr_Bounds.First),
+                    New_Copy_Tree
+                      (Type_Low_Bound (Base_Type (Etype (Ind_Bounds.First))))),
+                Reason    => CE_Range_Check_Failed));
+            return;
+         end if;
+
          --  Generate the following test:
 
          --    [constraint_error when


diff --git a/gcc/ada/sem_aggr.adb b/gcc/ada/sem_aggr.adb
--- a/gcc/ada/sem_aggr.adb
+++ b/gcc/ada/sem_aggr.adb
@@ -404,10 +404,6 @@ package body Sem_Aggr is
    --  The bounds of the aggregate itype are cooked up to look reasonable
    --  (in this particular case the bounds will be 1 .. 2).
 
-   function Is_Null_Aggregate (N : Node_Id) return Boolean;
-   --  Returns True for a "[]" aggregate (an Ada 2022 feature), even after
-   --  it has been transformed by expansion. Returns False otherwise.
-
    procedure Make_String_Into_Aggregate (N : Node_Id);
    --  A string literal can appear in a context in which a one dimensional
    --  array of characters is expected. This procedure simply rewrites the
@@ -419,9 +415,6 @@ package body Sem_Aggr is
    --  is constrained). If the subtype is unconstrained, then the bounds
    --  are determined in much the same way as the bounds for a null string
    --  literal with no applicable index constraint.
-   --  Emit a check that the bounds for each dimension define a null
-   --  range; no check is emitted if it is statically known that the
-   --  check would succeed.
 
    ---------------------------------
    --  Delta aggregate processing --
@@ -4102,7 +4095,6 @@ package body Sem_Aggr is
       Loc    : constant Source_Ptr := Sloc (N);
       Typ    : constant Entity_Id := Etype (N);
 
-      Check  : Node_Id;
       Index  : Node_Id;
       Lo, Hi : Node_Id;
       Constr : constant List_Id := New_List;
@@ -4127,18 +4119,6 @@ package body Sem_Aggr is
              Attribute_Name => Name_Pred,
              Expressions    => New_List (New_Copy_Tree (Lo)));
 
-         --  Check that high bound (i.e., low bound predecessor) exists.
-         --  Fail if low bound is low bound of base subtype (in all cases,
-         --  including modular).
-
-         Check :=
-           Make_Raise_Constraint_Error (Loc,
-             Condition =>
-               Make_Op_Le (Loc, New_Copy_Tree (Lo), New_Copy_Tree (Hi)),
-             Reason => CE_Range_Check_Failed);
-
-         Insert_Action (N, Check);
-
          Append (Make_Range (Loc, New_Copy_Tree (Lo), Hi), Constr);
          Analyze_And_Resolve (Last (Constr), Etype (Index));
 


diff --git a/gcc/ada/sem_aggr.ads b/gcc/ada/sem_aggr.ads
--- a/gcc/ada/sem_aggr.ads
+++ b/gcc/ada/sem_aggr.ads
@@ -43,6 +43,10 @@ package Sem_Aggr is
 
    --  WARNING: There is a matching C declaration of this subprogram in fe.h
 
+   function Is_Null_Aggregate (N : Node_Id) return Boolean;
+   --  Returns True for a "[]" aggregate (an Ada 2022 feature), even after
+   --  it has been transformed by expansion. Returns False otherwise.
+
    function Is_Null_Array_Aggregate_High_Bound (N : Node_Id) return Boolean;
    --  Returns True for the high bound of a null array aggregate.