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`.
AdaCore · Oct 18, 2023 · 5fafc5f · 5fafc5f
1 parent 89490ec
commit 5fafc5f
Show file tree

Hide file tree

Showing 7 changed files with 125 additions and 14 deletions.
diff --git 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
@@ -11,7 +11,7 @@ Expr: <Id "Fixed_T" test.adb:5:24-5:31>
 Expr: <Real test.adb:5:38-5:41>
   references:    None
   type:          <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
-  expected type: None
+  expected type: <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
 
 Resolving xrefs for node <SubtypeDecl ["Float_ST"] test.adb:7:4-7:41>
 *********************************************************************
@@ -23,7 +23,7 @@ Expr: <Id "Float_T" test.adb:7:24-7:31>
 Expr: <Int test.adb:7:39-7:40>
   references:    None
   type:          <ConcreteTypeDecl ["Universal_Int_Type_"] __standard:116:3-116:45>
-  expected type: None
+  expected type: <ConcreteTypeDecl ["Universal_Int_Type_"] __standard:116:3-116:45>
 
 
 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
@@ -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
@@ -0,0 +1,59 @@
+Analyzing test.adb
+##################
+
+Resolving xrefs for node <SubtypeDecl ["Sub_Delta"] test.adb:3:4-3:62>
+**********************************************************************
+
+Expr: <Id "Fix_Delta" test.adb:3:25-3:34>
+  references:    <DefiningName "Fix_Delta" test.adb:2:9-2:18>
+  type:          None
+  expected type: None
+Expr: <Real test.adb:3:41-3:44>
+  references:    None
+  type:          <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+  expected type: <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+Expr: <BinOp test.adb:3:51-3:61>
+  type:          <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+  expected type: <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+Expr: <Real test.adb:3:51-3:54>
+  references:    None
+  type:          <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+  expected type: <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+Expr: <OpDoubleDot ".." test.adb:3:55-3:57>
+  references:    None
+  type:          None
+  expected type: None
+Expr: <Real test.adb:3:58-3:61>
+  references:    None
+  type:          <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+  expected type: <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+
+Resolving xrefs for node <SubtypeDecl ["Sub_Digits"] test.adb:7:4-7:64>
+***********************************************************************
+
+Expr: <Id "Fix_Digits" test.adb:7:26-7:36>
+  references:    <DefiningName "Fix_Digits" test.adb:6:9-6:19>
+  type:          None
+  expected type: None
+Expr: <Int test.adb:7:44-7:45>
+  references:    None
+  type:          <ConcreteTypeDecl ["Universal_Int_Type_"] __standard:116:3-116:45>
+  expected type: <ConcreteTypeDecl ["Universal_Int_Type_"] __standard:116:3-116:45>
+Expr: <BinOp test.adb:7:52-7:63>
+  type:          <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+  expected type: <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+Expr: <Real test.adb:7:52-7:55>
+  references:    None
+  type:          <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+  expected type: <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+Expr: <OpDoubleDot ".." test.adb:7:56-7:58>
+  references:    None
+  type:          None
+  expected type: None
+Expr: <Real test.adb:7:59-7:63>
+  references:    None
+  type:          <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+  expected type: <ConcreteTypeDecl ["Universal_Real_Type_"] __standard:117:3-117:42>
+
+
+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
@@ -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
@@ -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: <null>
 |  |f_interfaces:

diff --git a/user_manual/changes/libadalang/1085.yaml 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
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		driver: name-resolution
		input_sources: [test.adb]