From a026b59e7711ffa23137a1255f1acc5c73589412 Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Wed, 23 Sep 2020 16:38:10 +0200 Subject: [PATCH] [Ada] Fix GNATprove support for iterated_component_associations gcc/ada/ * exp_spark.adb (Expand_SPARK_Array_Aggregate): Dedicated routine for array aggregates; mostly reuses existing code, but calls itself recursively for multi-dimensional array aggregates. (Expand_SPARK_N_Aggregate): Call Expand_SPARK_Array_Aggregate to do the actual expansion, starting from the first index of the array type. --- gcc/ada/exp_spark.adb | 172 +++++++++++++++++++++++++++--------------- 1 file changed, 112 insertions(+), 60 deletions(-) diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb index 3041c736a2f..75cdbe63446 100644 --- a/gcc/ada/exp_spark.adb +++ b/gcc/ada/exp_spark.adb @@ -52,6 +52,13 @@ package body Exp_SPARK is -- Local Subprograms -- ----------------------- + procedure Expand_SPARK_Array_Aggregate (N : Node_Id; Index : Node_Id); + -- Perform array-aggregate-specific expansion of an array sub-aggregate N + -- corresponding to the Index of the outer-most aggregate. This routine + -- mimics Resolve_Array_Aggregate which only checks the aggregate for being + -- well-formed, but doesn't analyze nor apply range checks to + -- iterated_component_associations. + procedure Expand_SPARK_N_Aggregate (N : Node_Id); -- Perform aggregate-specific expansion @@ -153,6 +160,107 @@ package body Exp_SPARK is end case; end Expand_SPARK; + ---------------------------------- + -- Expand_SPARK_Array_Aggregate -- + ---------------------------------- + + procedure Expand_SPARK_Array_Aggregate (N : Node_Id; Index : Node_Id) is + + procedure Expand_Aggr_Expr (Expr : Node_Id); + -- If Expr is a subaggregate, then process it recursively; otherwise it + -- is an expression for the array components which might not have been + -- analyzed and where scalar range checks could be missing. + + ---------------------- + -- Expand_Aggr_Expr -- + ---------------------- + + procedure Expand_Aggr_Expr (Expr : Node_Id) is + Nxt_Ind : constant Node_Id := Next_Index (Index); + begin + if Present (Nxt_Ind) then + Expand_SPARK_Array_Aggregate (Expr, Index => Nxt_Ind); + else + declare + Comp_Type : constant Entity_Id := Component_Type (Etype (N)); + begin + Analyze_And_Resolve (Expr, Comp_Type); + + if Is_Scalar_Type (Comp_Type) then + Apply_Scalar_Range_Check (Expr, Comp_Type); + end if; + end; + end if; + end Expand_Aggr_Expr; + + -- Local variables + + Assoc : Node_Id := First (Component_Associations (N)); + + -- Start of processing for Expand_SPARK_Array_Aggregate + + begin + while Present (Assoc) loop + -- For iterated_component_association we must apply range check to + -- discrete choices and re-analyze the expression, because frontend + -- only checks its legality and then analyzes the expanded loop code. + + if Nkind (Assoc) = N_Iterated_Component_Association then + declare + Choice : Node_Id; + begin + -- Analyze discrete choices + + Choice := First (Discrete_Choices (Assoc)); + + while Present (Choice) loop + + -- The index denotes a range of elements where range checks + -- have been already applied. + + if Nkind (Choice) in N_Others_Choice + | N_Range + | N_Subtype_Indication + then + null; + + -- Otherwise the index denotes a single element (or a + -- subtype name which doesn't require range checks). + + else pragma Assert (Nkind (Choice) in N_Subexpr); + Apply_Scalar_Range_Check (Choice, Etype (Index)); + end if; + + Next (Choice); + end loop; + + -- Keep processing the expression with index parameter in scope + + Push_Scope (Scope (Defining_Identifier (Assoc))); + Enter_Name (Defining_Identifier (Assoc)); + Expand_Aggr_Expr (Expression (Assoc)); + End_Scope; + end; + + -- For ordinary component associations we recurse into subaggregates, + -- because there could be nested iterated_component_association (and + -- it is harmless to analyze and apply checks if there is none). + + else pragma Assert (Nkind (Assoc) = N_Component_Association); + declare + Expr : constant Node_Id := Expression (Assoc); + pragma Assert (Present (Expr) xor Box_Present (Assoc)); + begin + if Present (Expr) then + Expand_Aggr_Expr (Expr); + end if; + end; + end if; + + Next (Assoc); + end loop; + end Expand_SPARK_Array_Aggregate; + ---------------------------------- -- Expand_SPARK_Delta_Or_Update -- ---------------------------------- @@ -372,67 +480,11 @@ package body Exp_SPARK is ------------------------------ procedure Expand_SPARK_N_Aggregate (N : Node_Id) is - Assoc : Node_Id := First (Component_Associations (N)); + Aggr_Typ : constant Entity_Id := Etype (N); begin - -- For compilation, frontend analyses a copy of the - -- iterated_component_association's expression for legality checking; - -- (then the expression is copied again when expanding association into - -- assignments for the individual choices). For SPARK we analyze the - -- original expression and apply range checks, if required. - - while Present (Assoc) loop - if Nkind (Assoc) = N_Iterated_Component_Association then - declare - Typ : constant Entity_Id := Etype (N); - - Comp_Type : constant Entity_Id := Component_Type (Typ); - Expr : constant Node_Id := Expression (Assoc); - Index_Typ : constant Entity_Id := First_Index (Typ); - - Index : Node_Id; - - begin - -- Analyze expression with index parameter in scope - - Push_Scope (Scope (Defining_Identifier (Assoc))); - Enter_Name (Defining_Identifier (Assoc)); - Analyze_And_Resolve (Expr, Comp_Type); - - if Is_Scalar_Type (Comp_Type) then - Apply_Scalar_Range_Check (Expr, Comp_Type); - end if; - - End_Scope; - - -- Analyze discrete choices - - Index := First (Discrete_Choices (Assoc)); - - while Present (Index) loop - - -- The index denotes a range of elements where range checks - -- have been already applied. - - if Nkind (Index) in N_Others_Choice - | N_Range - | N_Subtype_Indication - then - null; - - -- Otherwise the index denotes a single element (or a - -- subtype name which doesn't require range checks). - - else pragma Assert (Nkind (Index) in N_Subexpr); - Apply_Scalar_Range_Check (Index, Etype (Index_Typ)); - end if; - - Next (Index); - end loop; - end; - end if; - - Next (Assoc); - end loop; + if Is_Array_Type (Aggr_Typ) then + Expand_SPARK_Array_Aggregate (N, Index => First_Index (Aggr_Typ)); + end if; end Expand_SPARK_N_Aggregate; ---------------------------------------- -- 2.30.2