Merge branch 'mr/pmderodat/3-pred-type-check' into 'master'

Predicate: type check nodes that come from logic variables

See merge request eng/libadalang/langkit!1209

Author: pmderodat

langkit/templates/properties/helpers.mako

@@ -207,10 +207,12 @@
       type_name = f"{pred.id}_Predicate"
       package_name = f"{pred.id}_Pred"
       formal_node_types = prop.get_concrete_node_types(pred)
+      enumerated_arg_types = list(enumerate(formal_node_types[1:], 1))
       arity = len(formal_node_types)
       has_refcounted_args = any(
          pa.type.is_refcounted for pa in pred.partial_args
       )
+      has_multiple_concrete_nodes = len(T.root_node.concrete_subclasses) > 1
    %>
 
    <%def name="call_profile()">
@@ -313,11 +315,11 @@
          Entity : ${T.entity.name} := Entities (1);
       % endif
       <% node0_type = formal_node_types[0] %>
-      Node : constant ${node0_type.name} := Entity.Node;
+      Node : ${node0_type.name};
    begin
       ## Here, we'll raise a property error, but only for dispatching
-      ## properties. For non dispatching properties we'll allow the user to
-      ## handle null however he wants.
+      ## properties. For non dispatching properties we'll allow the user
+      ## property to handle null however it wants.
       % if prop.dispatching and not ctx.no_property_checks:
          if Node_0.Node = null then
             Raise_Property_Exception
@@ -327,15 +329,44 @@
         end if;
       % endif
 
+      ## Type check nodes that come from logic vars to avoid Assertion_Error or
+      ## Assertion_Error in case of mismatch.
+      % if not ctx.emitter.no_property_checks:
+         <%
+            typed_nodes = (
+               [("Entity.Node", prop.struct)]
+               + [
+                  (f"Entities ({i + 1}).Node", t.element_type)
+                  for i, t in enumerated_arg_types
+               ]
+            )
+         %>
+         % for node_expr, node_type in typed_nodes:
+            % if has_multiple_concrete_nodes and not node_type.is_root_node:
+               if ${node_expr} /= null
+                  and then ${node_expr}.Kind
+                           not in ${node_type.ada_kind_range_name}
+               then
+                  Raise_Property_Exception
+                    (Node, Property_Error'Identity, "mismatching node type");
+               end if;
+            % endif
+         % endfor
+      % endif
+
+      Node := Entity.Node;
+
       ## Pass the "prefix" node (the one that owns the property to call) using
       ## the conventional bare node/entity_info arguments. Pass the other node
       ## arguments as entities directly.
       <%
          args = ['Node'] + [
             f"(Node => Entities ({i + 1}).Node,"
             f" Info => Entities ({i + 1}).Info)"
-            for i, formal_type in enumerate(formal_node_types[1:], 1)
-      ] + [f"{pa.name} => Self.Field_{pa.index}" for pa in pred.partial_args]
+            for i, formal_type in enumerated_arg_types
+         ] + [
+            f"{pa.name} => Self.Field_{pa.index}" for pa in pred.partial_args
+         ]
          if prop.uses_entity_info:
             args.append(f"{prop.entity_info_name} => Entity.Info")
          args_fmt = '({})'.format(', '.join(args)) if args else ''

testsuite/tests/properties/conv_prop_mistype/expected_concrete_syntax.lkt renamed to testsuite/tests/properties/logic_var_type_mismatch/expected_concrete_syntax.lkt

@@ -60,6 +60,26 @@ class Examples: FooNode {
     fun fail_nprop_varargs(): Bool = (
         %propagate(node.pe.lvar, PlusExample.ncomb_prop, [node.pe.lvar, node.re.lvar]) and node.domains()
     ).solve()
+
+    @exported
+    fun ok_pred(): Bool = (
+        %predicate(PlusExample.pred_prop, node.pe.lvar, node.re.lvar, node.pe.lvar) and node.domains()
+    ).solve()
+
+    @exported
+    fun fail_pred_1(): Bool = (
+        %predicate(PlusExample.pred_prop, node.re.lvar, node.re.lvar, node.pe.lvar) and node.domains()
+    ).solve()
+
+    @exported
+    fun fail_pred_2(): Bool = (
+        %predicate(PlusExample.pred_prop, node.pe.lvar, node.pe.lvar, node.pe.lvar) and node.domains()
+    ).solve()
+
+    @exported
+    fun fail_pred_3(): Bool = (
+        %predicate(PlusExample.pred_prop, node.pe.lvar, node.re.lvar, node.re.lvar) and node.domains()
+    ).solve()
 }
 
 class PlusExample: FooNode {
@@ -70,6 +90,9 @@ class PlusExample: FooNode {
 
     fun ncomb_prop(pe_list: Array[Entity[PlusExample]]): Entity[PlusExample] =
         pe_list?[0]
+
+    fun pred_prop(@ignored re: Entity[RegularExample], @ignored pe: Entity[PlusExample]): Bool =
+        true
 }
 
 class RegularExample: FooNode {

testsuite/tests/properties/conv_prop_mistype/main.adb renamed to testsuite/tests/properties/logic_var_type_mismatch/main.adb

@@ -50,6 +50,10 @@ begin
    Check ("p_fail_nprop_multi_3", P_Fail_Nprop_Multi_3'Access);
    Check ("p_ok_nprop_varargs", P_Ok_Nprop_Varargs'Access);
    Check ("p_fail_nprop_varargs", P_Fail_Nprop_Varargs'Access);
+   Check ("p_ok_pred", P_Ok_Pred'Access);
+   Check ("p_fail_pred_1", P_Fail_Pred_1'Access);
+   Check ("p_fail_pred_2", P_Fail_Pred_2'Access);
+   Check ("p_fail_pred_3", P_Fail_Pred_3'Access);
 
    Put_Line ("main.adb: Done.");
 end Main;

testsuite/tests/properties/conv_prop_mistype/test.out renamed to testsuite/tests/properties/logic_var_type_mismatch/test.out

@@ -23,5 +23,17 @@ Result: TRUE
 Calling Examples.p_fail_nprop_varargs...
 Got a Property_Error: main.txt:1:1-1:8: mismatching node type for comb_prop
 
+Calling Examples.p_ok_pred...
+Result: TRUE
+
+Calling Examples.p_fail_pred_1...
+Got a Property_Error: mismatching node type
+
+Calling Examples.p_fail_pred_2...
+Got a Property_Error: mismatching node type
+
+Calling Examples.p_fail_pred_3...
+Got a Property_Error: mismatching node type
+
 main.adb: Done.
 Done

testsuite/tests/properties/conv_prop_mistype/test.py renamed to testsuite/tests/properties/logic_var_type_mismatch/test.py

@@ -8,6 +8,7 @@
     Bind,
     Entity,
     NPropagate,
+    Predicate,
     Self,
     ignore,
     langkit_property,
@@ -33,7 +34,7 @@ def domains():
         return Self.re.lvar.domain([Self.re]) & Self.pe.lvar.domain([Self.pe])
 
     # PropertyError expected when PlusExample.conv_prop is called on a
-    # RegularExample.
+    # RegularExample node.
 
     @langkit_property(public=True)
     def fail_bind_conv_prop():
@@ -65,7 +66,7 @@ def ok_nprop_multi():
         ).solve
 
     # PropertyError expected when PlusExample.comb_prop is called on a
-    # RegularExample.
+    # RegularExample node.
 
     @langkit_property(public=True)
     def fail_nprop_multi_1():
@@ -140,6 +141,65 @@ def fail_nprop_varargs():
             & Self.domains
         ).solve
 
+    # Successful example of a Predicate (as a sanity check)
+
+    @langkit_property(public=True)
+    def ok_pred():
+        return (
+            Predicate(
+                PlusExample.pred_prop,
+                Self.pe.lvar,
+                Self.re.lvar,
+                Self.pe.lvar,
+            )
+            & Self.domains
+        ).solve
+
+    # PropertyError expected when PlusExample.pred_prop is called on a
+    # RegularExample node.
+
+    @langkit_property(public=True)
+    def fail_pred_1():
+        return (
+            Predicate(
+                PlusExample.pred_prop,
+                Self.re.lvar,
+                Self.re.lvar,
+                Self.pe.lvar,
+            )
+            & Self.domains
+        ).solve
+
+    # PropertyError expected when PlusExample.pred_prop is called with a
+    # PlusExample for its "re" argument.
+
+    @langkit_property(public=True)
+    def fail_pred_2():
+        return (
+            Predicate(
+                PlusExample.pred_prop,
+                Self.pe.lvar,
+                Self.pe.lvar,
+                Self.pe.lvar,
+            )
+            & Self.domains
+        ).solve
+
+    # PropertyError expected when PlusExample.pred_prop is called with a
+    # RegularExample for its "pe" argument.
+
+    @langkit_property(public=True)
+    def fail_pred_3():
+        return (
+            Predicate(
+                PlusExample.pred_prop,
+                Self.pe.lvar,
+                Self.re.lvar,
+                Self.re.lvar,
+            )
+            & Self.domains
+        ).solve
+
 
 class RegularExample(FooNode):
     pass
@@ -160,6 +220,11 @@ def comb_prop(re=T.RegularExample.entity, pe=T.PlusExample.entity):
     def ncomb_prop(pe_list=T.PlusExample.entity.array):
         return pe_list.at(0)
 
+    @langkit_property()
+    def pred_prop(re=T.RegularExample.entity, pe=T.PlusExample.entity):
+        ignore(re, pe)
+        return True
+
 
 build_and_run(
     lkt_file="expected_concrete_syntax.lkt",