From 3aa0203856e09e896ea86631f52779903dafde75 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Laurent=20Th=C3=A9venoux?= <thevenoux@adacore.com>
Date: Tue, 24 Oct 2023 08:43:56 +0200
Subject: [PATCH] Fix access-to-object membership test

As specified in ARM 4.5.2 - 30.3/4, when the tested type is a general
access-to-object, the type of the tested expression is convertible to
the tested type.
---
 ada/ast.py                                    | 29 +++++++++++++++++--
 .../membership_expr_4/test.adb                | 13 +++++++++
 .../membership_expr_4/test.out                | 24 +++++++++++++++
 .../membership_expr_4/test.yaml               |  2 ++
 4 files changed, 66 insertions(+), 2 deletions(-)
 create mode 100644 testsuite/tests/name_resolution/membership_expr_4/test.adb
 create mode 100644 testsuite/tests/name_resolution/membership_expr_4/test.out
 create mode 100644 testsuite/tests/name_resolution/membership_expr_4/test.yaml

diff --git a/ada/ast.py b/ada/ast.py
index 596b53844..2ad37ebec 100644
--- a/ada/ast.py
+++ b/ada/ast.py
@@ -7096,9 +7096,19 @@ def matching_formal_type(formal_type=T.BaseTypeDecl.entity):
             Entity.matching_formal_type_impl(formal_type)
         )
 
+    @langkit_property(return_type=Bool, dynamic_vars=[origin])
+    def matching_membership_type(formal_type=T.BaseTypeDecl.entity):
+        return And(
+            Not(formal_type.is_null),
+            Not(Self.is_null),
+            Entity.matching_formal_type_impl(formal_type,
+                                             accept_root_types=True)
+        )
+
     @langkit_property(return_type=Bool, dynamic_vars=[origin])
     def matching_formal_type_impl(formal_type=T.BaseTypeDecl.entity,
-                                  accept_derived=(Bool, False)):
+                                  accept_derived=(Bool, False),
+                                  accept_root_types=(Bool, False)):
         actual_type = Var(Entity)
         return Or(
             And(formal_type.is_classwide | accept_derived,
@@ -7120,6 +7130,13 @@ def matching_formal_type_impl(formal_type=T.BaseTypeDecl.entity,
                         And(actual_accessed_type.is_classwide,
                             actual_accessed_type.specific_type.matching_type(
                                 formal_accessed_type)),
+
+                        # In a MembershipExpr, if formal_type is a general
+                        # access-to-object type, actual_type is convertible to
+                        # formal_type (:rmlink:`4.5.2` 30.3/4).
+                        And(accept_root_types,
+                            formal_accessed_type.specific_type
+                            .is_derived_type(actual_accessed_type))
                     )
                 )
             ),
@@ -12736,6 +12753,14 @@ def matches_expected_formal_type():
             Self.expected_type_var
         )
 
+    @langkit_property(return_type=T.Equation, dynamic_vars=[origin])
+    def matches_expected_membership_type():
+        return Predicate(
+            BaseTypeDecl.matching_membership_type,
+            Self.type_var,
+            Self.expected_type_var
+        )
+
     @langkit_property(return_type=T.Equation, dynamic_vars=[origin])
     def matches_expected_formal_prim_type():
         return Predicate(
@@ -13942,7 +13967,7 @@ class MembershipExpr(Expr):
                     # type of the tested expression is the subtype's base type.
                     Bind(Self.expr.expected_type_var,
                          typ.base_subtype)
-                    & Self.expr.matches_expected_formal_type
+                    & Self.expr.matches_expected_membership_type
                 ),
 
                 # Regular membership check
diff --git a/testsuite/tests/name_resolution/membership_expr_4/test.adb b/testsuite/tests/name_resolution/membership_expr_4/test.adb
new file mode 100644
index 000000000..9e20d8327
--- /dev/null
+++ b/testsuite/tests/name_resolution/membership_expr_4/test.adb
@@ -0,0 +1,13 @@
+procedure Test is
+   type T is (A, B, C, D);
+   type U is new T;
+   type U_Ptr is access U;
+
+   function F (O : access T) return Boolean is
+   begin
+      return O in U_Ptr;
+      pragma Test_Statement;
+   end F;
+begin
+   null;
+end Test;
diff --git a/testsuite/tests/name_resolution/membership_expr_4/test.out b/testsuite/tests/name_resolution/membership_expr_4/test.out
new file mode 100644
index 000000000..aa9d88579
--- /dev/null
+++ b/testsuite/tests/name_resolution/membership_expr_4/test.out
@@ -0,0 +1,24 @@
+Analyzing test.adb
+##################
+
+Resolving xrefs for node <ReturnStmt test.adb:8:7-8:25>
+*******************************************************
+
+Expr: <MembershipExpr test.adb:8:14-8:24>
+  type:          <ConcreteTypeDecl ["Boolean"] __standard:3:3-3:33>
+  expected type: <ConcreteTypeDecl ["Boolean"] __standard:3:3-3:33>
+Expr: <Id "O" test.adb:8:14-8:15>
+  references:    <DefiningName "O" test.adb:6:16-6:17>
+  type:          <AnonymousTypeDecl ["None"] test.adb:6:20-6:28>
+  expected type: <ConcreteTypeDecl ["U_Ptr"] test.adb:4:4-4:27>
+Expr: <OpIn "in" test.adb:8:16-8:18>
+  references:    None
+  type:          None
+  expected type: None
+Expr: <Id "U_Ptr" test.adb:8:19-8:24>
+  references:    <DefiningName "U_Ptr" test.adb:4:9-4:14>
+  type:          None
+  expected type: None
+
+
+Done.
diff --git a/testsuite/tests/name_resolution/membership_expr_4/test.yaml b/testsuite/tests/name_resolution/membership_expr_4/test.yaml
new file mode 100644
index 000000000..173e325ff
--- /dev/null
+++ b/testsuite/tests/name_resolution/membership_expr_4/test.yaml
@@ -0,0 +1,2 @@
+driver: name-resolution
+input_sources: [test.adb]