From db290a9e3745e79710d836c955588845baa2bb6b Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Sat, 9 May 2020 22:30:56 +0200 Subject: [PATCH] [Ada] Set range checks for for 'Update on arrays in GNATprove expansion 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. --- gcc/ada/exp_spark.adb | 86 ++++++++++++++++++++++++++++++++++++++----- gcc/ada/sem_attr.adb | 22 ----------- 2 files changed, 76 insertions(+), 32 deletions(-) diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index 1f95aa49aa8..6ef03c3180e 100644 --- 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 index 5e61810fbf9..d2678110f65 100644 --- 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);