diff mbox series

[Ada] Set range checks for for 'Update on arrays in GNATprove expansion

Message ID 20200707092735.GA41431@adacore.com
State New
Headers show
Series [Ada] Set range checks for for 'Update on arrays in GNATprove expansion | expand

Commit Message

Pierre-Marie de Rodat July 7, 2020, 9:27 a.m. UTC 
This is a follow-up of a recent change, where setting of range checks
for 'Update on records was moved from Resolve_Attribute (where it was
shared between GNAT and GNATprove) to custom expansion for GNATprove
(and GNAT sets them as well in its own expansion).  This patch does the
same for 'Update on arrays.

Just like the previous patch, this one also eliminates unnecessary
checks, for example, on a code like this:

   type T is array (Positive range <>) of Boolean;
   function P return Positive;
   X : T := ...'Update (P => ...);  --  no need for range check

we no longer emit a range check for the result of P being in T'Range,
while still generating them where required, e.g.:

   function N return Natural;
   X : T := ...'Update (N => ...);  -- range check needed

Also, range checks for single-dimensional arrays were added in both
analysis and resolution, while for multi-dimensional arrays only in
resulution, which was inconsistent.

Note: attribute Update is soon to be replaced by delta_aggregate. This
cleanup is for reusing its implementation (if possible) or at least to
mirror it and not introduce more confusion.

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

gcc/ada/

	* exp_spark.adb (Expand_SPARK_N_Attribute_Reference): Add scalar
	range checks for 'Update on arrays just like for 'Update on
	records.
	* sem_attr.adb (Analyze_Array_Component_Update): Do not set
	range checks for single-dimensional arrays.
	(Resolve_Attribute): Do not set range checks for both single-
	and multi- dimensional arrays.
diff mbox series

Patch

diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -258,25 +258,91 @@  package body Exp_SPARK is
 
             Assoc     : Node_Id;
             Comp      : Node_Id;
-            Comp_Type : Node_Id;
+            Comp_Type : Entity_Id;
             Expr      : Node_Id;
+            Index     : Node_Id;
+            Index_Typ : Entity_Id;
 
          begin
             --  Apply scalar range checks on the updated components, if needed
 
             if Is_Array_Type (Typ) then
-               Assoc := First (Component_Associations (Aggr));
 
-               while Present (Assoc) loop
-                  Expr      := Expression (Assoc);
-                  Comp_Type := Component_Type (Typ);
+               --  Multi-dimensional array
 
-                  if Is_Scalar_Type (Comp_Type) then
-                     Apply_Scalar_Range_Check (Expr, Comp_Type);
-                  end if;
+               if Present (Next_Index (First_Index (Typ))) then
+                  Assoc := First (Component_Associations (Aggr));
 
-                  Next (Assoc);
-               end loop;
+                  while Present (Assoc) loop
+                     Expr      := Expression (Assoc);
+                     Comp_Type := Component_Type (Typ);
+
+                     if Is_Scalar_Type (Comp_Type) then
+                        Apply_Scalar_Range_Check (Expr, Comp_Type);
+                     end if;
+
+                     --  The current association contains a sequence of indexes
+                     --  denoting an element of a multidimensional array:
+                     --
+                     --    (Index_1, ..., Index_N)
+
+                     Expr := First (Choices (Assoc));
+
+                     pragma Assert (Nkind (Aggr) = N_Aggregate);
+
+                     while Present (Expr) loop
+                        Index     := First (Expressions (Expr));
+                        Index_Typ := First_Index (Typ);
+
+                        while Present (Index_Typ) loop
+                           Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
+                           Next (Index);
+                           Next_Index (Index_Typ);
+                        end loop;
+
+                        Next (Expr);
+                     end loop;
+
+                     Next (Assoc);
+                  end loop;
+
+               --  One-dimensional array
+
+               else
+                  Assoc := First (Component_Associations (Aggr));
+
+                  while Present (Assoc) loop
+                     Expr      := Expression (Assoc);
+                     Comp_Type := Component_Type (Typ);
+
+                     if Is_Scalar_Type (Comp_Type) then
+                        Apply_Scalar_Range_Check (Expr, Comp_Type);
+                     end if;
+
+                     Index     := First (Choices (Assoc));
+                     Index_Typ := First_Index (Typ);
+
+                     while Present (Index) loop
+                        --  The index denotes a range of elements
+
+                        if Nkind (Index) = N_Range then
+                           Apply_Scalar_Range_Check
+                             (Low_Bound  (Index), Etype (Index_Typ));
+                           Apply_Scalar_Range_Check
+                             (High_Bound (Index), Etype (Index_Typ));
+
+                        --  Otherwise the index denotes a single element
+
+                        else
+                           Apply_Scalar_Range_Check (Index, Etype (Index_Typ));
+                        end if;
+
+                        Next (Index);
+                     end loop;
+
+                     Next (Assoc);
+                  end loop;
+               end if;
 
             else pragma Assert (Is_Record_Type (Typ));
 


diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -6764,30 +6764,10 @@  package body Sem_Attr is
                      Analyze_And_Resolve (Low,  Etype (Index_Typ));
                      Analyze_And_Resolve (High, Etype (Index_Typ));
 
-                     --  Add a range check to ensure that the bounds of the
-                     --  range are within the index type when this cannot be
-                     --  determined statically.
-
-                     if not Is_OK_Static_Expression (Low) then
-                        Set_Do_Range_Check (Low);
-                     end if;
-
-                     if not Is_OK_Static_Expression (High) then
-                        Set_Do_Range_Check (High);
-                     end if;
-
                   --  Otherwise the index denotes a single element
 
                   else
                      Analyze_And_Resolve (Index, Etype (Index_Typ));
-
-                     --  Add a range check to ensure that the index is within
-                     --  the index type when it is not possible to determine
-                     --  this statically.
-
-                     if not Is_OK_Static_Expression (Index) then
-                        Set_Do_Range_Check (Index);
-                     end if;
                   end if;
 
                   Next (Index);
@@ -12019,14 +11999,12 @@  package body Sem_Attr is
 
                         if Nkind (C) /= N_Aggregate then
                            Analyze_And_Resolve (C, Etype (Indx));
-                           Apply_Constraint_Check (C, Etype (Indx));
                            Check_Non_Static_Context (C);
 
                         else
                            C_E := First (Expressions (C));
                            while Present (C_E) loop
                               Analyze_And_Resolve (C_E, Etype (Indx));
-                              Apply_Constraint_Check (C_E, Etype (Indx));
                               Check_Non_Static_Context (C_E);
 
                               Next (C_E);