From 5fafc5f40cd388933bdfb5851216e912998b6c75 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Laurent=20Th=C3=A9venoux?= Date: Wed, 20 Sep 2023 16:09:45 +0200 Subject: [PATCH 1/2] Improve fixed-point subtype constraint definitions resolution This patch fixes a bug where fixed-point digits and delta constraint xref equations were not sufficiently defined to properly handle some ranges resolution. This patch also adds more constraints in the xref equations to ensure that resolved type are matching expected ones (the new equations have been derived from the `OrdinaryFixedPointDef` one). A small API change is also introduced by this patch. The `digits` field of `DeltaConstraint` has been renamed to `delta`. --- ada/ast.py | 54 +++++++++++++---- .../delta_digits_constraints/test.out | 4 +- .../fixed_point_subtype_constraints/test.adb | 11 ++++ .../fixed_point_subtype_constraints/test.out | 59 +++++++++++++++++++ .../fixed_point_subtype_constraints/test.yaml | 2 + .../tests/parser/full_type_decl_10/test.out | 2 +- user_manual/changes/libadalang/1085.yaml | 7 +++ 7 files changed, 125 insertions(+), 14 deletions(-) create mode 100644 testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.adb create mode 100644 testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.out create mode 100644 testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.yaml create mode 100644 user_manual/changes/libadalang/1085.yaml diff --git a/ada/ast.py b/ada/ast.py index 0eedb7dc4..6e180c5a2 100644 --- a/ada/ast.py +++ b/ada/ast.py @@ -8383,27 +8383,59 @@ class DigitsConstraint(Constraint): digits = Field(type=T.Expr) range = Field(type=T.RangeSpec) - xref_equation = Property( - Entity.digits.sub_equation & Entity.range.then( - lambda range: range.sub_equation, - default_val=LogicTrue() + @langkit_property() + def xref_equation(): + """ + Build an equation for a digits constraint definition. + """ + return And( + # As per :rmlink:`3.5.9`, the digits expression is expected to be + # of any integer type. + Entity.universal_int_bind(Entity.digits.expected_type_var), + Entity.digits.sub_equation, + Entity.digits.matches_expected_type, + + # Expressions from the range specification are expected to be of + # any real type, the types need not be the same. + Entity.range.then( + lambda r: + Entity.universal_real_bind(r.range.expected_type_var) + & r.range.sub_equation + & r.range.matches_expected_type, + default_val=LogicTrue() + ) ) - ) class DeltaConstraint(Constraint): """ Delta and range type constraint (:rmlink:`J.3`). """ - digits = Field(type=T.Expr) + delta = Field(type=T.Expr) range = Field(type=T.RangeSpec) - xref_equation = Property( - Entity.digits.sub_equation & Entity.range.then( - lambda range: range.sub_equation, - default_val=LogicTrue() + @langkit_property() + def xref_equation(): + """ + Build an equation for a delta constraint definition. + """ + return And( + # As per :rmlink:`J.3`, the delta expression is expected to be of + # any real type. + Entity.universal_real_bind(Entity.delta.expected_type_var), + Entity.delta.sub_equation, + Entity.delta.matches_expected_type, + + # Expressions from the range specification are expected to be of + # any real type, the types need not be the same. + Entity.range.then( + lambda r: + Entity.universal_real_bind(r.range.expected_type_var) + & r.range.sub_equation + & r.range.matches_expected_type, + default_val=LogicTrue() + ) ) - ) class CompositeConstraint(Constraint): diff --git a/testsuite/tests/name_resolution/delta_digits_constraints/test.out b/testsuite/tests/name_resolution/delta_digits_constraints/test.out index 0e1390a31..17cf0492c 100644 --- a/testsuite/tests/name_resolution/delta_digits_constraints/test.out +++ b/testsuite/tests/name_resolution/delta_digits_constraints/test.out @@ -11,7 +11,7 @@ Expr: Expr: references: None type: - expected type: None + expected type: Resolving xrefs for node ********************************************************************* @@ -23,7 +23,7 @@ Expr: Expr: references: None type: - expected type: None + expected type: Done. diff --git a/testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.adb b/testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.adb new file mode 100644 index 000000000..f5ed689f1 --- /dev/null +++ b/testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.adb @@ -0,0 +1,11 @@ +procedure Test is + type Fix_Delta is delta 0.5 range -3.0 .. 3.0; + subtype Sub_Delta is Fix_Delta delta 1.0 range 0.0 .. 2.0; + pragma Test_Statement; + + type Fix_Digits is digits 5 range -50.0 .. 50.0; + subtype Sub_Digits is Fix_Digits digits 1 range 0.0 .. 30.0; + pragma Test_Statement; +begin + null; +end Test; diff --git a/testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.out b/testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.out new file mode 100644 index 000000000..5fc56a9e4 --- /dev/null +++ b/testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.out @@ -0,0 +1,59 @@ +Analyzing test.adb +################## + +Resolving xrefs for node +********************************************************************** + +Expr: + references: + type: None + expected type: None +Expr: + references: None + type: + expected type: +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: None + type: + expected type: + +Resolving xrefs for node +*********************************************************************** + +Expr: + references: + type: None + expected type: None +Expr: + references: None + type: + expected type: +Expr: + type: + expected type: +Expr: + references: None + type: + expected type: +Expr: + references: None + type: None + expected type: None +Expr: + references: None + type: + expected type: + + +Done. diff --git a/testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.yaml b/testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.yaml new file mode 100644 index 000000000..173e325ff --- /dev/null +++ b/testsuite/tests/name_resolution/fixed_point_subtype_constraints/test.yaml @@ -0,0 +1,2 @@ +driver: name-resolution +input_sources: [test.adb] diff --git a/testsuite/tests/parser/full_type_decl_10/test.out b/testsuite/tests/parser/full_type_decl_10/test.out index c5a41735c..89bc29e4d 100644 --- a/testsuite/tests/parser/full_type_decl_10/test.out +++ b/testsuite/tests/parser/full_type_decl_10/test.out @@ -20,7 +20,7 @@ ConcreteTypeDecl[1:1-1:27] | | | Id[1:15-1:16]: A | | |f_constraint: | | | DeltaConstraint[1:17-1:26] -| | | |f_digits: +| | | |f_delta: | | | | Real[1:23-1:26]: 1.0 | | | |f_range: | |f_interfaces: diff --git a/user_manual/changes/libadalang/1085.yaml b/user_manual/changes/libadalang/1085.yaml new file mode 100644 index 000000000..4a4319616 --- /dev/null +++ b/user_manual/changes/libadalang/1085.yaml @@ -0,0 +1,7 @@ +type: api-change +title: Rename ``F_Digits`` field of ``Ada_Delta_Constraint`` +description: | + The field `F_Digits` of the node `Ada_Delta_Constraint` has been renamed to + `F_Delta` to correctly match the definition of a delta constraint (which + doesn't specify `digits` but `delta`). +date: 2023-09-20 From 1deda7216985707b3386b4c305eca21dda1ebd2a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Laurent=20Th=C3=A9venoux?= Date: Mon, 9 Oct 2023 14:41:58 +0200 Subject: [PATCH 2/2] Factorize float type definitions/constraints RangeSpec equation --- ada/ast.py | 52 +++++++++++++--------------------------------------- 1 file changed, 13 insertions(+), 39 deletions(-) diff --git a/ada/ast.py b/ada/ast.py index 6e180c5a2..466d34008 100644 --- a/ada/ast.py +++ b/ada/ast.py @@ -8199,15 +8199,7 @@ def xref_equation(): Entity.delta.sub_equation, Entity.delta.matches_expected_type, - # Expressions from the range specification are expected to be of - # any real type, the types need not be the same. - Entity.range.then( - lambda r: - Entity.universal_real_bind(r.range.expected_type_var) - & r.range.sub_equation - & r.range.matches_expected_type, - default_val=LogicTrue() - ) + If(Self.range.is_null, LogicTrue(), Entity.range.sub_equation) ) @langkit_property(memoized=True) @@ -8267,15 +8259,7 @@ def xref_equation(): Entity.digits.sub_equation, Entity.digits.matches_expected_type, - # Expressions from the range specification are expected to be of - # any real type, the types need not be the same. - Entity.range.then( - lambda r: - Entity.universal_real_bind(r.range.expected_type_var) - & r.range.sub_equation - & r.range.matches_expected_type, - default_val=LogicTrue() - ) + If(Self.range.is_null, LogicTrue(), Entity.range.sub_equation) ) @langkit_property(memoized=True) @@ -8394,16 +8378,7 @@ def xref_equation(): Entity.universal_int_bind(Entity.digits.expected_type_var), Entity.digits.sub_equation, Entity.digits.matches_expected_type, - - # Expressions from the range specification are expected to be of - # any real type, the types need not be the same. - Entity.range.then( - lambda r: - Entity.universal_real_bind(r.range.expected_type_var) - & r.range.sub_equation - & r.range.matches_expected_type, - default_val=LogicTrue() - ) + If(Self.range.is_null, LogicTrue(), Entity.range.sub_equation) ) @@ -8425,16 +8400,7 @@ def xref_equation(): Entity.universal_real_bind(Entity.delta.expected_type_var), Entity.delta.sub_equation, Entity.delta.matches_expected_type, - - # Expressions from the range specification are expected to be of - # any real type, the types need not be the same. - Entity.range.then( - lambda r: - Entity.universal_real_bind(r.range.expected_type_var) - & r.range.sub_equation - & r.range.matches_expected_type, - default_val=LogicTrue() - ) + If(Self.range.is_null, LogicTrue(), Entity.range.sub_equation) ) @@ -22521,7 +22487,7 @@ class RangeSpec(AdaNode): range = Field(type=Expr) xref_stop_resolution = Property(Self.parent.is_a(ComponentClause)) - xref_equation = Property(Entity.range.xref_equation & If( + xref_equation = Property(Entity.range.xref_equation & Cond( # Ada RM says that for component clauses and signed int type # definitions, the expected type is any integer type. Self.parent.is_a(ComponentClause, SignedIntTypeDef), @@ -22529,6 +22495,14 @@ class RangeSpec(AdaNode): Self.universal_int_bind(Self.range.expected_type_var) & Entity.range.matches_expected_type, + # In the following cases, expressions from the range specification are + # expected to be of any real type, the types need not be the same. + Self.parent.is_a(DeltaConstraint, DigitsConstraint, + OrdinaryFixedPointDef, DecimalFixedPointDef), + + Self.universal_real_bind(Self.range.expected_type_var) + & Entity.range.matches_expected_type, + LogicTrue() ))