From 81b33b5d04971766005af5fb1dda9934279b7191 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Laurent=20Th=C3=A9venoux?= Date: Thu, 23 May 2024 14:21:06 +0200 Subject: [PATCH] Add support for deep delta aggregates As described here: https://github.com/AdaCore/ada-spark-rfcs/blob/sttaft/ada-spark-rfcs/topic/rfc-deep-delta-aggregates.md. --- ada/nodes.lkt | 205 +++- ada/parser.lkt | 23 +- .../aggregates_ada2020/test.out | 4 +- .../deep_delta_aggregates/arr.adb | 26 + .../deep_delta_aggregates/base.adb | 95 ++ .../deep_delta_aggregates/multidim.adb | 17 + .../deep_delta_aggregates/test.adb | 31 + .../deep_delta_aggregates/test.out | 1016 +++++++++++++++++ .../deep_delta_aggregates/test.yaml | 2 + .../deep_delta_aggregates/test_array.adb | 29 + .../name_resolution/delta_aggregate/arr.adb | 18 + .../name_resolution/delta_aggregate/test.out | 70 +- .../name_resolution/delta_aggregate/test.yaml | 2 +- .../name_resolution/target_name/test.out | 2 +- .../parser/deep_delta_array_aggregate/input | 1 + .../deep_delta_array_aggregate/test.out | 50 + .../deep_delta_array_aggregate/test.yaml | 2 + 17 files changed, 1581 insertions(+), 12 deletions(-) create mode 100644 testsuite/tests/name_resolution/deep_delta_aggregates/arr.adb create mode 100644 testsuite/tests/name_resolution/deep_delta_aggregates/base.adb create mode 100644 testsuite/tests/name_resolution/deep_delta_aggregates/multidim.adb create mode 100644 testsuite/tests/name_resolution/deep_delta_aggregates/test.adb create mode 100644 testsuite/tests/name_resolution/deep_delta_aggregates/test.out create mode 100644 testsuite/tests/name_resolution/deep_delta_aggregates/test.yaml create mode 100644 testsuite/tests/name_resolution/deep_delta_aggregates/test_array.adb create mode 100644 testsuite/tests/name_resolution/delta_aggregate/arr.adb create mode 100644 testsuite/tests/parser/deep_delta_array_aggregate/input create mode 100644 testsuite/tests/parser/deep_delta_array_aggregate/test.out create mode 100644 testsuite/tests/parser/deep_delta_array_aggregate/test.yaml diff --git a/ada/nodes.lkt b/ada/nodes.lkt index f6b153ca3..7c7f5d008 100644 --- a/ada/nodes.lkt +++ b/ada/nodes.lkt @@ -2975,6 +2975,7 @@ class AggregateAssoc: BasicAssoc { elif agg.parent.as[AspectAssoc]?.id.name_is(s"Contract_Cases") then self.contract_cases_assoc_equation() elif agg is BracketAggregate and td?.has_aspect(s"Aggregate") then self.container_aggregate_equation(td) elif agg.parent is AspectClause | AspectAssoc | PragmaArgumentAssoc then %true + elif agg is DeltaAggregate then self.delta_aggregate_assoc_equation() elif atd.is_null then self.record_assoc_equation() else self.array_assoc_equation(atd, mra) } @@ -2993,6 +2994,90 @@ class AggregateAssoc: BasicAssoc { ) } + |" Equation for the case where this is an aggregate assoc for a delta + |" aggregate. This is an Ada 2022 feature (:rmlink:`4.3.4`). This equation + |" also supports the so called "deep" delta aggregates, a GNAT + |" experimental feature. + @with_dynvars(env, origin, entry_point) + fun delta_aggregate_assoc_equation(): Equation = { + val agg = self.base_aggregate(); + val agg_type = agg.type_val().as[BaseTypeDecl]; + + # Determine whether this is a delta array aggregate rather than a deep + # delta aggregate by checking whether any alternative designates a + # position in an array. + val positional_assoc = agg_type.is_array() and not self.names().any( + # leftmost_name returns null if n starts with + # ArraySubcomponentChoiceName (which denotes a deep aggregate). + (n) => n.as[Name]?.leftmost_name().is_null + ); + + val agg_components = (not agg_type.is_array()).do( + (_) => node.unpack_formals(agg.all_components()) + ); + + # If this is a record delta aggregate, try to match the components + # corresponding to these names in order to correctly set the + # environments from which they should be resolved. + val matches = self.names().map( + (n) => if n is Name then + # Get the leftmost name to match a component with if any + n.as[Name].leftmost_name().do( + (id) => agg_components.find( + (c) => c.name.matches(id) + ) + ) + # If not a Name, there can be no component match (can be a BinOp + # denoting a range in an array for example.) + else null[Expr].as_entity + ); + + self.names().logic_all( + (n, i) => { + # Resolve the name from the matched component if any + bind env = matches[i].do( + (l) => l.children_env(), + default_val=env + ); + + n.as[Expr].as_entity.sub_equation() + } and ( + # Check that all alternatives resolve to the same type + if i > 0 then + %predicate(BaseTypeDecl.matching_type, + n.as[Expr].type_var(), + self.names()[0].as[Expr].type_var(), + error_location=node) + else %true + ) and ( + # We cannot set the expected type of the alternative in case the + # aggregate is a record aggregate or a deep one (both record and + # array) because the expected type of the alternative can be any + # one of the record components (including those from parents). + # Only simple array aggregate associations's alternatives can + # have an expected type (i.e., the alternative designates a + # position or a range). + if positional_assoc then + %eq(n.as[Expr].expected_type_var(), + agg_type.index_type(0)) + and n.as[Expr].matches_expected_type() + else %true + ) + ) and ( + # Set the expected type of the expression only once since all the + # alternatives should have the same type. + if positional_assoc then + %eq(self.expr().expected_type_var(), agg_type.comp_type()) + else + %eq(self.expr().expected_type_var(), + self.names()[0].as[Expr].type_var()) + ) and ( + # Build the equation for the expression + self.expr().sub_equation() and self.expr().matches_expected_type() + ) + } + + |" Equation for the case where this is an aggregate assoc for a record |" type. @with_dynvars(env, origin, entry_point) @@ -11999,6 +12084,34 @@ class Name: Expr { else node } + |" Returns the leftmost name following the name chain. + |" For example, given:: + |" + |" A (B) (C) (D) -- Case 1: CallExpr + |" (A) (B) -- Case 2: ArraySubcomponentChoiceName + |" A.B.C (D).E -- Case 3: DottedName + |" A -- Case 4: Identifier + |" A'First -- Case 5: AttributeRef + |" + |" ``self.leftmost_name`` will return: + |" + |" - A for Case 1, + |" - null for Case 2, + |" - A for Case 3, + |" - A for Case 4, + |" - A for Case 5. + |" + |" This property has been introduced to resolve deep delta aggregates so it + |" may not be useful in other context as is. Do not make it exported. + fun leftmost_name(): Name = match node { + case ce: CallExpr => ce.name.leftmost_name() + case ascn: ArraySubcomponentChoiceName => + ascn.name?.leftmost_name() + case dn: DottedName => dn.prefix.leftmost_name() + case ar: AttributeRef => ar.prefix.leftmost_name() + case _ => node + } + |" Construct the xref equation for the chain of parent nested names. @with_dynvars(env, origin, entry_point) fun parent_name_equation(typ: Entity[BaseTypeDecl], root: Name): Equation = { @@ -13255,7 +13368,18 @@ class CallExpr: Name { } ), default_val=%false ) - else self.all_args_xref_equation(root) and ( + else { + # If we are resolving this CallExpr from a DeltaAggregate, env is the + # one of the aggregate type, so we need to bind env to self's env to + # resolve the CallExpr params (array indicies). + bind env = if entry_point.as[AggregateAssoc]?.as_entity + .base_aggregate() is DeltaAggregate + then + self.children_env() + else env; + + self.all_args_xref_equation(root) + } and ( # For each potential entity match, we want to express the # following constraints: { @@ -14265,6 +14389,85 @@ class DottedName: Name { self.prefix.is_constant() or self.suffix.is_constant() } + +|" Name for an array subcomponent choice of a deep delta aggregate. +class ArraySubcomponentChoiceName: Name { + # This node can basically be seen as a CallExpr where `name` can be a null + # node. + + # The name field can be null when the ArraySubcomponentChoiceName is of the + # form "(suffix)" (where suffix is a list of expression: "expr{, expr}" + # representing the indexes of a mono- or multi-dimentional array, or a + # range). When the node is of the form of "name (suffix)", name can only be + # another ArraySubcomponentChoiceName or a DottedName. + @parse_field @nullable name: Name + @parse_field suffix: AdaNode + + fun suffix_exprs(): Array[Entity[Expr]] = + self.suffix.as![AssocList].map( + (a) => a.as![ParamAssoc].expr() + ) + + |" Return the corresponding delta aggregate's ancestor expression type. + @memoized + fun delta_aggregate_ancestor_expr_type(): Entity[BaseTypeDecl] = + node.parents(with_self=false).find( + (p) => p is DeltaAggregate + ).as[DeltaAggregate].ancestor_expr.as_bare_entity.expression_type() + + fun ref_var(): LogicVar = + node.as_bare_entity.delta_aggregate_ancestor_expr_type().name.ref_var() + + fun name_symbol(): Symbol = + node.name.do( + (n) => n.name_symbol() + ) + + fun xref_equation(): Equation = + # Resolve name if any + self.name.do( + (n) => n.sub_equation(), default_val=%true + ) and ( + self.suffix_exprs().logic_all( + # Resolve all suffix's indexes/range independently + (a, i) => a.sub_equation() + and %eq(a.expected_type_var(), + node.delta_aggregate_ancestor_expr_type().index_type(i)) + and a.matches_expected_type() + )) and ( + # Self's type is bound to the component type of Self's name + # designated type if any (if name is null, the type is given by the + # delta aggregate itself). + if self.name is DottedName + then %eq(self.name.type_var(), self.type_var(), + conv_prop=BaseTypeDecl.comp_type) + else %eq(self.type_var(), + self.name.do( + (n) => n.name_designated_type().comp_type(), + default_val= + node.delta_aggregate_ancestor_expr_type().comp_type() + ) + ) + ) + + fun designated_type_impl(): Entity[BaseTypeDecl] = + self.name.do( + (n) => n.designated_type_impl(), + default_val=node.delta_aggregate_ancestor_expr_type().comp_type() + ) + + fun designated_env(): LexicalEnv = + self.name.do( + (n) => n.name_designated_type().defining_env(), + default_val={ + bind include_ud_indexing = false; + + node.delta_aggregate_ancestor_expr_type().defining_env() + } + ) +} + + |" self name in ``end ...;`` syntactic constructs. class EndName: Name { @parse_field name: Name diff --git a/ada/parser.lkt b/ada/parser.lkt index 0a4703908..feb319e5f 100644 --- a/ada/parser.lkt +++ b/ada/parser.lkt @@ -963,7 +963,13 @@ grammar ada_grammar { | DeltaAggregate( "(" expr - "with" "delta" / AssocList+(aggregate_assoc, ",") ")" + "with" "delta" + / + # TODO: We use a ?pick parser below only to satisfy unparsing + # because this is actually not optional in the case of delta + # aggregates. See langkit#816. + AssocList+(AggregateAssoc(?pick(delta_choice_list "=>") expr), ",") + ")" ) | Aggregate( "(" @@ -1158,6 +1164,12 @@ grammar ada_grammar { ) | name |> when(Name.is_range_attribute) ) + array_subcomponent_choice <- or( + | DottedName(array_subcomponent_choice "." direct_name) + | ArraySubcomponentChoiceName(array_subcomponent_choice + "(" call_suffix ")") + | ArraySubcomponentChoiceName(null(Name) "(" call_suffix ")") + ) choice <- or( | discrete_range | discrete_subtype_indication @@ -1165,6 +1177,15 @@ grammar ada_grammar { | others_designator ) choice_list <- AlternativesList+(choice, "|") + delta_choice_list <- AlternativesList+( + or( + | array_subcomponent_choice + | discrete_range + | expr + | others_designator + ), + "|" + ) rel_op <- or(Op.NotIn("not" "in") | Op.In("in")) membership_choice <- or( | discrete_range diff --git a/testsuite/tests/name_resolution/aggregates_ada2020/test.out b/testsuite/tests/name_resolution/aggregates_ada2020/test.out index 6f29fd252..cc526324f 100644 --- a/testsuite/tests/name_resolution/aggregates_ada2020/test.out +++ b/testsuite/tests/name_resolution/aggregates_ada2020/test.out @@ -75,7 +75,7 @@ Expr: expected type: None Expr: references: - type: None + type: expected type: None Expr: references: None @@ -98,7 +98,7 @@ Expr: expected type: None Expr: references: - type: None + type: expected type: None Expr: references: None diff --git a/testsuite/tests/name_resolution/deep_delta_aggregates/arr.adb b/testsuite/tests/name_resolution/deep_delta_aggregates/arr.adb new file mode 100644 index 000000000..81996e1ad --- /dev/null +++ b/testsuite/tests/name_resolution/deep_delta_aggregates/arr.adb @@ -0,0 +1,26 @@ +procedure Arr is + + type R is record + F, G, H : Integer; + end record; + + type My_Arr is array (Positive range <>) of R; + + procedure Test (X : in out My_Arr; I, J, K, L : Positive); + + procedure Test (X : in out My_Arr; I, J, K, L : Positive) is + begin + X := (X with delta + (I).F => 1, + (J).G => 2, + (K).F => 3, + (L).H => 4); + pragma Test_Statement; + + X := ((if True then X else X) with delta (I).F => 4); + pragma Test_Statement; + end Test; + +begin + null; +end Arr; diff --git a/testsuite/tests/name_resolution/deep_delta_aggregates/base.adb b/testsuite/tests/name_resolution/deep_delta_aggregates/base.adb new file mode 100644 index 000000000..12355018f --- /dev/null +++ b/testsuite/tests/name_resolution/deep_delta_aggregates/base.adb @@ -0,0 +1,95 @@ +procedure Base with SPARK_Mode is + + -- Handling of simple aggregates with only record components + + procedure Test_Record with Global => null is + type R1 is record + F1, F2, F3 : Integer; + end record; + type R2 is record + G1, G2, G3 : R1; + end record; + + X : R2 := (others => (others => 1)); + Y : R2 := (X with delta G1.F1 => 2, G2.F2 => 3, G3 => (others => 4)); + pragma Test_Statement; + begin + null; + end Test_Record; + + -- General case + + procedure Test_Array (I, J, C : Integer) with + Global => null, + Pre => I in 1 .. C and J in 1 .. C + is + type R1 is record + F1, F2, F3 : Integer; + end record; + type R2 is record + G1 : R1; + G2, G3 : Integer; + end record; + type R2_Arr is array (Integer range 1 .. C) of R2; + type R3 is record + H1 : R2_Arr; + H2 : Integer; + end record; + + X : R3 := (H1 => (others => (G1 => (others => 1), others => 1)), H2 => 1); + Y : R3 := (X with delta + H1 (I).G1 => (others => 2), + H1 (J).G1.F2 => 3, + H2 => 4); + pragma Test_Statement; + begin + null; + end Test_Array; + + -- Test with a nested array access + + procedure Test_Nested_Array (C : Integer) with + Global => null + is + type R1 is record + F1, F2, F3 : Integer; + end record; + type R1_Arr is array (Integer range 1 .. 10) of R1; + type R2 is record + G1 : R1_Arr; + G2, G3 : Integer; + end record; + type R2_Arr is array (Integer range 1 .. C) of R2; + type R3 is record + H1 : R2_Arr; + H2 : Integer; + end record; + + -- Test with possibly overlapping components + + procedure Test (I, J, K, L, M, N, P, Q : Integer) with + Global => C, + Pre => I in 1 .. C and J in 1 .. C and L in 1 .. C and N in 1 .. C + and K in 1 .. 10 and M in 1 .. 10 and P in 1 .. 10 and Q in 1 .. C + is + X : R3 := + (H1 => (others => (G1 => (others => (others => 1)), others => 1)), + H2 => 1); + Y : R3 := (X with delta + H1 (I).G1 => (others => (others => 2)), + H1 (J).G1 (K) => (others => 3), + H1 (L).G1 (M).F1 => 4, + H1 (N).G1 (P).F2 => 5, + H1 (Q).G2 => 6, + H2 => 7); + pragma Test_Statement; + begin + null; + end Test; + begin + null; + end Test_Nested_Array; + +begin + null; +end Base; diff --git a/testsuite/tests/name_resolution/deep_delta_aggregates/multidim.adb b/testsuite/tests/name_resolution/deep_delta_aggregates/multidim.adb new file mode 100644 index 000000000..b2772c591 --- /dev/null +++ b/testsuite/tests/name_resolution/deep_delta_aggregates/multidim.adb @@ -0,0 +1,17 @@ +procedure Multidim with SPARK_Mode is + type Segment is array (1 .. 2) of Integer; + S : Segment; + + type Point is record + X, Y : Segment; + end record; + + type Triangle is array (1 .. 3) of Point; + T : Triangle; + + type Multi is array (1 .. 3, Boolean) of Triangle; + M : Multi; +begin + M := (M with delta (1, True) (1).Y (2) => 1); + pragma Test_Statement; +end Multidim; diff --git a/testsuite/tests/name_resolution/deep_delta_aggregates/test.adb b/testsuite/tests/name_resolution/deep_delta_aggregates/test.adb new file mode 100644 index 000000000..d8ced6b0e --- /dev/null +++ b/testsuite/tests/name_resolution/deep_delta_aggregates/test.adb @@ -0,0 +1,31 @@ +pragma Extensions_Allowed (All_Extensions); + +procedure Test is + type R is record + F, G, H : Integer; + end record; + + type My_Arr is array (Positive range <>) of R; + + type S is record + A : My_Arr (1 .. 2); + B : Integer; + end record; + + A : My_Arr := ((1, 2, 3), (4, 5, 6)); + + B : S := (A => A, B => 1); + +begin + A := (A with delta (1) => (0,0,0)); + pragma Test_Statement; + + A := (A with delta (A (1).F) => (1,1,1)); + pragma Test_Statement; + + B := (B with delta A (1).F => 1); + pragma Test_Statement; + + B := (B with delta A (B.B).F => 1); + pragma Test_Statement; +end; diff --git a/testsuite/tests/name_resolution/deep_delta_aggregates/test.out b/testsuite/tests/name_resolution/deep_delta_aggregates/test.out new file mode 100644 index 000000000..919c7657e --- /dev/null +++ b/testsuite/tests/name_resolution/deep_delta_aggregates/test.out @@ -0,0 +1,1016 @@ +Analyzing base.adb +################## + +Resolving xrefs for node +*************************************************************** + +Expr: + references: + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +*************************************************************** + +Expr: + references: + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +**************************************************************** + +Expr: + references: + type: None + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: + + +Analyzing arr.adb +################# + +Resolving xrefs for node +******************************************************** + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +******************************************************** + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + type: + expected type: None +Expr: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: + + +Analyzing test_array.adb +######################## + +Resolving xrefs for node +*************************************************************** + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +*************************************************************** + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +*************************************************************** + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: + +Resolving xrefs for node +*************************************************************** + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: + +Resolving xrefs for node +*************************************************************** + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: + + +Analyzing multidim.adb +###################### + +Resolving xrefs for node +************************************************************* + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: + + +Analyzing test.adb +################## + +Resolving xrefs for node +********************************************************* + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +********************************************************* + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +********************************************************* + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +********************************************************* + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: None + type: + expected type: + + +Done. diff --git a/testsuite/tests/name_resolution/deep_delta_aggregates/test.yaml b/testsuite/tests/name_resolution/deep_delta_aggregates/test.yaml new file mode 100644 index 000000000..f96d6dbe0 --- /dev/null +++ b/testsuite/tests/name_resolution/deep_delta_aggregates/test.yaml @@ -0,0 +1,2 @@ +driver: name-resolution +input_sources: [base.adb, arr.adb, test_array.adb, multidim.adb, test.adb] diff --git a/testsuite/tests/name_resolution/deep_delta_aggregates/test_array.adb b/testsuite/tests/name_resolution/deep_delta_aggregates/test_array.adb new file mode 100644 index 000000000..bf2d41543 --- /dev/null +++ b/testsuite/tests/name_resolution/deep_delta_aggregates/test_array.adb @@ -0,0 +1,29 @@ +procedure Test_Array with SPARK_Mode is + type Point is record + X, Y : Integer; + end record; + + type Segment is array (1 .. 2) of Point; + S : Segment; + + type Triangle is array (1 .. 3) of Segment; + T : Triangle; + + type Cube is array (1 .. 3, 1 .. 4) of Segment; + C : Cube; +begin + S := (S with delta (1) => (1, 2)); + pragma Test_Statement; + + S := (S with delta (1).X => 1); + pragma Test_Statement; + + S := (S with delta (1).X | (2).Y => S(2).X, (1).Y => S(2).Y); + pragma Test_Statement; + + T := (T with delta (2)(1).Y => T(1)(2).X); + pragma Test_Statement; + + C := (C with delta (1, 2)(3).Y => 1); + pragma Test_Statement; +end Test_Array; diff --git a/testsuite/tests/name_resolution/delta_aggregate/arr.adb b/testsuite/tests/name_resolution/delta_aggregate/arr.adb new file mode 100644 index 000000000..8bd3c519a --- /dev/null +++ b/testsuite/tests/name_resolution/delta_aggregate/arr.adb @@ -0,0 +1,18 @@ +procedure Arr is + + type Int_Rec is record + I : Integer; + end record; + + type Vector is array(Integer range <>) of Float; + + I : Integer := 1; + R : Int_Rec := (I => 4); + Vec : Vector := (1.0, 2.0, 3.0); +begin + Vec := (Vec with delta I => 3.0); + pragma Test_Statement; + + Vec := (Vec with delta R.I => 3.0); + pragma Test_Statement; +end Arr; diff --git a/testsuite/tests/name_resolution/delta_aggregate/test.out b/testsuite/tests/name_resolution/delta_aggregate/test.out index f081dd729..6d8c68524 100644 --- a/testsuite/tests/name_resolution/delta_aggregate/test.out +++ b/testsuite/tests/name_resolution/delta_aggregate/test.out @@ -38,7 +38,7 @@ Expr: expected type: None Expr: references: - type: None + type: expected type: None Expr: references: @@ -68,7 +68,7 @@ Expr: expected type: None Expr: references: - type: None + type: expected type: None Expr: references: @@ -130,7 +130,7 @@ Expr: expected type: None Expr: references: - type: None + type: expected type: None Expr: references: None @@ -273,7 +273,7 @@ Expr: expected type: None Expr: references: - type: None + type: expected type: None Expr: references: None @@ -327,7 +327,7 @@ Expr: expected type: None Expr: references: - type: None + type: expected type: None Expr: references: None @@ -335,7 +335,7 @@ Expr: expected type: Expr: references: - type: None + type: expected type: None Expr: references: None @@ -343,4 +343,62 @@ Expr: expected type: +Analyzing arr.adb +################# + +Resolving xrefs for node +******************************************************** + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +******************************************************** + +Expr: + references: + type: + expected type: None +Expr: + type: + expected type: +Expr: + references: + type: + expected type: None +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: + type: + expected type: +Expr: + references: None + type: + expected type: + + Done. diff --git a/testsuite/tests/name_resolution/delta_aggregate/test.yaml b/testsuite/tests/name_resolution/delta_aggregate/test.yaml index a0a196441..7c9147a22 100644 --- a/testsuite/tests/name_resolution/delta_aggregate/test.yaml +++ b/testsuite/tests/name_resolution/delta_aggregate/test.yaml @@ -1,2 +1,2 @@ driver: name-resolution -input_sources: [foo.adb] +input_sources: [foo.adb, arr.adb] diff --git a/testsuite/tests/name_resolution/target_name/test.out b/testsuite/tests/name_resolution/target_name/test.out index 7a8d3c9bf..63034c29b 100644 --- a/testsuite/tests/name_resolution/target_name/test.out +++ b/testsuite/tests/name_resolution/target_name/test.out @@ -113,7 +113,7 @@ Expr: expected type: None Expr: references: - type: None + type: expected type: None Expr: type: diff --git a/testsuite/tests/parser/deep_delta_array_aggregate/input b/testsuite/tests/parser/deep_delta_array_aggregate/input new file mode 100644 index 000000000..e2f1bfead --- /dev/null +++ b/testsuite/tests/parser/deep_delta_array_aggregate/input @@ -0,0 +1 @@ +(T with delta (2)(1).Y => T(1)(2).X) diff --git a/testsuite/tests/parser/deep_delta_array_aggregate/test.out b/testsuite/tests/parser/deep_delta_array_aggregate/test.out new file mode 100644 index 000000000..5bf575fe2 --- /dev/null +++ b/testsuite/tests/parser/deep_delta_array_aggregate/test.out @@ -0,0 +1,50 @@ +DeltaAggregate[1:1-1:37] +|f_ancestor_expr: +| Id[1:2-1:3]: T +|f_assocs: +| AssocList[1:15-1:36] +| | AggregateAssoc[1:15-1:36] +| | |f_designators: +| | | AlternativesList[1:15-1:23] +| | | | DottedName[1:15-1:23] +| | | | |f_prefix: +| | | | | ArraySubcomponentChoiceName[1:15-1:21] +| | | | | |f_name: +| | | | | | ArraySubcomponentChoiceName[1:15-1:18] +| | | | | | |f_name: +| | | | | | |f_suffix: +| | | | | | | AssocList[1:16-1:17] +| | | | | | | | ParamAssoc[1:16-1:17] +| | | | | | | | |f_designator: +| | | | | | | | |f_r_expr: +| | | | | | | | | Int[1:16-1:17]: 2 +| | | | | |f_suffix: +| | | | | | AssocList[1:19-1:20] +| | | | | | | ParamAssoc[1:19-1:20] +| | | | | | | |f_designator: +| | | | | | | |f_r_expr: +| | | | | | | | Int[1:19-1:20]: 1 +| | | | |f_suffix: +| | | | | Id[1:22-1:23]: Y +| | |f_r_expr: +| | | DottedName[1:27-1:36] +| | | |f_prefix: +| | | | CallExpr[1:27-1:34] +| | | | |f_name: +| | | | | CallExpr[1:27-1:31] +| | | | | |f_name: +| | | | | | Id[1:27-1:28]: T +| | | | | |f_suffix: +| | | | | | AssocList[1:29-1:30] +| | | | | | | ParamAssoc[1:29-1:30] +| | | | | | | |f_designator: +| | | | | | | |f_r_expr: +| | | | | | | | Int[1:29-1:30]: 1 +| | | | |f_suffix: +| | | | | AssocList[1:32-1:33] +| | | | | | ParamAssoc[1:32-1:33] +| | | | | | |f_designator: +| | | | | | |f_r_expr: +| | | | | | | Int[1:32-1:33]: 2 +| | | |f_suffix: +| | | | Id[1:35-1:36]: X diff --git a/testsuite/tests/parser/deep_delta_array_aggregate/test.yaml b/testsuite/tests/parser/deep_delta_array_aggregate/test.yaml new file mode 100644 index 000000000..d8ab7a160 --- /dev/null +++ b/testsuite/tests/parser/deep_delta_array_aggregate/test.yaml @@ -0,0 +1,2 @@ +driver: parser +rule: aggregate