From: Yannick Moy <m...@adacore.com>
GNATprove supports container aggregates, except for indexed aggregates.
It needs all expressions to have suitable target types and Do_Range_Check
flags, which are added by the special expansion for GNATprove.
There is no impact on code generation.
gcc/ada/
* exp_spark.adb (Expand_SPARK_N_Aggregate): New procedure for the
special expansion.
(Expand_SPARK): Call the new expansion procedure.
* sem_util.adb (Is_Container_Aggregate): Implement missing test.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/exp_spark.adb | 146 ++++++++++++++++++++++++++++++++++++++++++
gcc/ada/sem_util.adb | 17 ++---
2 files changed, 155 insertions(+), 8 deletions(-)
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index ae0e616c797..f77d5f9f829 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -23,6 +23,7 @@
-- --
------------------------------------------------------------------------------
+with Aspects; use Aspects;
with Atree; use Atree;
with Checks; use Checks;
with Einfo; use Einfo;
@@ -47,6 +48,7 @@ with Sem_Aggr; use Sem_Aggr;
with Sem_Aux; use Sem_Aux;
with Sem_Ch7; use Sem_Ch7;
with Sem_Ch8; use Sem_Ch8;
+with Sem_Ch13; use Sem_Ch13;
with Sem_Prag; use Sem_Prag;
with Sem_Res; use Sem_Res;
with Sem_Util; use Sem_Util;
@@ -64,6 +66,10 @@ package body Exp_SPARK is
-- Local Subprograms --
-----------------------
+ procedure Expand_SPARK_N_Aggregate (N : Node_Id);
+ -- Perform specific expansion of container aggregates, to ensure suitable
+ -- checking of expressions.
+
procedure Expand_SPARK_N_Attribute_Reference (N : Node_Id);
-- Perform attribute-reference-specific expansion
@@ -139,6 +145,9 @@ package body Exp_SPARK is
when N_Delta_Aggregate =>
Expand_SPARK_N_Delta_Aggregate (N);
+ when N_Aggregate =>
+ Expand_SPARK_N_Aggregate (N);
+
when N_Expanded_Name
| N_Identifier
=>
@@ -418,6 +427,143 @@ package body Exp_SPARK is
end if;
end Expand_SPARK_Delta_Or_Update;
+ ------------------------------
+ -- Expand_SPARK_N_Aggregate --
+ ------------------------------
+
+ procedure Expand_SPARK_N_Aggregate (N : Node_Id) is
+
+ -- Local subprograms
+
+ procedure Parse_Named_Subp
+ (Subp : Subprogram_Kind_Id;
+ Key_Type : out Type_Kind_Id;
+ Element_Type : out Type_Kind_Id);
+ -- Retrieve key and element types from subprogram for named addition
+
+ procedure Parse_Unnamed_Subp
+ (Subp : Subprogram_Kind_Id;
+ Element_Type : out Type_Kind_Id);
+ -- Retrieve element types from subprogram for unnamed addition
+
+ procedure Wrap_For_Checks (Expr : N_Subexpr_Id; Typ : Type_Kind_Id);
+ -- If Expr might require a range check for conversion to type Typ, set
+ -- Do_Range_Check on Expr. In all cases, wrap Expr in a type conversion
+ -- if Typ is not the type of Expr already, for GNATprove to correctly
+ -- identity the target type for the range check and insert any other
+ -- checks.
+
+ ----------------------
+ -- Parse_Named_Subp --
+ ----------------------
+
+ procedure Parse_Named_Subp
+ (Subp : Subprogram_Kind_Id;
+ Key_Type : out Type_Kind_Id;
+ Element_Type : out Type_Kind_Id)
+ is
+ Formal : Entity_Id := First_Formal (Subp);
+ begin
+ Next_Formal (Formal);
+ Key_Type := Etype (Formal);
+ Next_Formal (Formal);
+ Element_Type := Etype (Formal);
+ end Parse_Named_Subp;
+
+ ------------------------
+ -- Parse_Unnamed_Subp --
+ ------------------------
+
+ procedure Parse_Unnamed_Subp
+ (Subp : Subprogram_Kind_Id;
+ Element_Type : out Type_Kind_Id)
+ is
+ Formal : Entity_Id := First_Formal (Subp);
+ begin
+ Next_Formal (Formal);
+ Element_Type := Etype (Formal);
+ end Parse_Unnamed_Subp;
+
+ ---------------------
+ -- Wrap_For_Checks --
+ ---------------------
+
+ procedure Wrap_For_Checks (Expr : N_Subexpr_Id; Typ : Type_Kind_Id) is
+ begin
+ if Is_Scalar_Type (Typ) then
+ Apply_Scalar_Range_Check (Expr, Typ);
+ end if;
+
+ Convert_To_And_Rewrite (Typ, Expr);
+ end Wrap_For_Checks;
+
+ -- Local variables
+
+ Typ : constant Entity_Id := Etype (N);
+ Asp : constant Node_Id := Find_Value_Of_Aspect (Typ, Aspect_Aggregate);
+
+ Empty_Subp : Node_Id := Empty;
+ Add_Named_Subp : Node_Id := Empty;
+ Add_Unnamed_Subp : Node_Id := Empty;
+ New_Indexed_Subp : Node_Id := Empty;
+ Assign_Indexed_Subp : Node_Id := Empty;
+ Key_Type : Entity_Id;
+ Element_Type : Entity_Id;
+
+ Assocs : constant List_Id := Component_Associations (N);
+ Exprs : constant List_Id := Expressions (N);
+ Choice : Node_Id;
+ Assoc : Node_Id;
+ Expr : Node_Id;
+
+ -- Start of processing for Expand_SPARK_N_Aggregate
+
+ begin
+ if Is_Container_Aggregate (N) then
+
+ Parse_Aspect_Aggregate (Asp,
+ Empty_Subp, Add_Named_Subp, Add_Unnamed_Subp,
+ New_Indexed_Subp, Assign_Indexed_Subp);
+
+ Assoc := First (Assocs);
+ Expr := First (Exprs);
+
+ -- Both lists could be empty as in [] but they can't be both
+ -- non-empty.
+ pragma Assert (not (Present (Assoc) and then Present (Expr)));
+
+ -- Deal with cases supported in GNATprove:
+ -- - named container aggregate which is not an indexed aggregate
+ -- - positional container aggregate
+
+ if Present (Assoc)
+ and then Present (Add_Named_Subp)
+ then
+ Parse_Named_Subp (Entity (Add_Named_Subp), Key_Type, Element_Type);
+
+ while Present (Assoc) loop
+ Choice := First (Choice_List (Assoc));
+
+ while Present (Choice) loop
+ Wrap_For_Checks (Choice, Key_Type);
+ Next (Choice);
+ end loop;
+
+ Wrap_For_Checks (Expression (Assoc), Element_Type);
+ Next (Assoc);
+ end loop;
+
+ elsif Present (Expr) then
+ Parse_Unnamed_Subp (Entity (Add_Unnamed_Subp), Element_Type);
+
+ while Present (Expr) loop
+ Wrap_For_Checks (Expr, Element_Type);
+ Next (Expr);
+ end loop;
+ end if;
+ end if;
+ end Expand_SPARK_N_Aggregate;
+
----------------------------------
-- Expand_SPARK_N_Freeze_Entity --
----------------------------------
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 2a31a11f9a2..f8922fed322 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -12349,14 +12349,15 @@ package body Sem_Util is
function Is_Container_Aggregate (Exp : Node_Id) return Boolean is
- function Is_Record_Aggregate return Boolean is (False);
- -- ??? Unimplemented. Given an aggregate whose type is a
- -- record type with specified Aggregate aspect, how do we
- -- determine whether it is a record aggregate or a container
- -- aggregate? If the code where the aggregate occurs can see only
- -- a partial view of the aggregate's type then the aggregate
- -- cannot be a record type; an aggregate of a private type has to
- -- be a container aggregate.
+ function Is_Record_Aggregate return Boolean is
+ (Is_Parenthesis_Aggregate (Exp));
+ -- Given an aggregate whose type is a record type with specified
+ -- Aggregate aspect, we determine whether it is a record aggregate or
+ -- a container aggregate by ckecking whether it uses parentheses () or
+ -- square brackets []. If the code where the aggregate occurs can see
+ -- only a partial view of the aggregate's type then the aggregate cannot
+ -- be a record type and must then use []; an aggregate of a private type
+ -- has to be a container aggregate and must then use [].
begin
return Nkind (Exp) = N_Aggregate
--
2.43.0
