Fix memory leaks in quantifier expressions early exits

TN: UB12-016

Author: pmderodat

langkit/expressions/collections.py

@@ -620,6 +620,12 @@ class Expr(ComputingExpr):
         static_type = T.Bool
         pretty_class_name = 'Quantifier'
 
+        serial_generator = iter(count(1))
+        """
+        Generator of unique IDs for this expression. Used to create unique
+        labels in the generated code.
+        """
+
         def __init__(self, kind, collection, expr, element_vars, index_var,
                      iter_scope, abstract_expr=None):
             """
@@ -655,6 +661,11 @@ def __init__(self, kind, collection, expr, element_vars, index_var,
             self.iter_scope = iter_scope
             self.static_type = T.Bool
 
+            self.exit_label = f"Exit_{next(self.serial_generator)}"
+            """
+            Exit label for early loop exits in the generated code.
+            """
+
             with iter_scope.parent.use():
                 super().__init__(
                     'Quantifier_Result', abstract_expr=abstract_expr

langkit/templates/properties/quantifier_ada.mako

@@ -52,24 +52,36 @@ ${result_var} := ${'False' if quantifier.kind == ANY else 'True'};
          ${quantifier.expr.render_pre()}
 
          ## Depending on the kind of the quantifier, we want to abort as soon
-         ## as the predicate holds or as soon as it does not hold.
+         ## as the predicate holds or as soon as it does not hold. To exit the
+         ## loop, go to the exit label, so that scope finalizers are called
+         ## before actually leaving the loop.
          % if quantifier.kind == ANY:
             if ${quantifier.expr.render_expr()} then
                ${result_var} := True;
-               exit;
+               goto ${quantifier.exit_label};
             end if;
          % else:
             if not (${quantifier.expr.render_expr()}) then
                ${result_var} := False;
-               exit;
+               goto ${quantifier.exit_label};
             end if;
          % endif
 
          % if quantifier.index_var:
             ${quantifier.index_var.name} := ${quantifier.index_var.name} + 1;
          % endif
 
+         <<${quantifier.exit_label}>> null;
          ${scopes.finalize_scope(quantifier.iter_scope)}
+
+         ## If we decided after this iteration to exit the loop, we can do it
+         ## now that the iteration scope it finalized.
+         exit when
+            % if quantifier.kind == ALL:
+               not
+            % endif
+            ${result_var}
+         ;
       end loop;
    end;
 </%def>

testsuite/tests/properties/quantifier_refcount/expected_concrete_syntax.lkt

@@ -0,0 +1,22 @@
+import lexer_example
+@with_lexer(foo_lexer)
+grammar foo_grammar {
+    @main_rule main_rule <- list+(Example(@example))
+
+}
+
+@abstract class FooNode implements Node[FooNode] {
+
+    fun get_bigint(): BigInt = BigInt(1)
+
+    @export fun check(): Bool = node.children.all(
+        (c) => # This condition is always False, so we have a loop early exit,
+        # which used to leave the result of "c.get_bigint" (big integers
+        # are ref-counted) allocated when exitting the scope: the finalizer
+        # for that scope was not called in that case.
+        c.get_bigint() = BigInt(0)
+    )
+}
+
+class Example : FooNode implements TokenNode {
+}

testsuite/tests/properties/quantifier_refcount/main.adb

@@ -0,0 +1,21 @@
+with Ada.Text_IO; use Ada.Text_IO;
+
+with Libfoolang.Analysis; use Libfoolang.Analysis;
+
+procedure Main is
+   Ctx : constant Analysis_Context := Create_Context;
+   U   : constant Analysis_Unit := Ctx.Get_From_Buffer
+     (Filename => "main.txt",
+      Buffer   => "example");
+   N   : constant Foo_Node := U.Root;
+
+begin
+   if U.Has_Diagnostics then
+      for D of U.Diagnostics loop
+         Put_Line (U.Format_GNU_Diagnostic (D));
+      end loop;
+      raise Program_Error;
+   end if;
+
+   Put_Line ("P_Check (" & N.Image & ") = " & N.P_Check'Image);
+end Main;

testsuite/tests/properties/quantifier_refcount/test.out

@@ -0,0 +1,2 @@
+P_Check (<ExampleList main.txt:1:1-1:8>) = FALSE
+Done

testsuite/tests/properties/quantifier_refcount/test.py

@@ -0,0 +1,35 @@
+"""
+Check that the scope of a Qualifier expression is correctly finalized on early
+exit.
+"""
+
+from langkit.dsl import ASTNode
+from langkit.expressions import BigIntLiteral, Self, langkit_property
+
+from utils import build_and_run
+
+
+class FooNode(ASTNode):
+
+    @langkit_property()
+    def get_bigint():
+        return BigIntLiteral(1)
+
+    @langkit_property(public=True)
+    def check():
+        return Self.children.all(
+            # This condition is always False, so we have a loop early exit,
+            # which used to leave the result of "c.get_bigint" (big integers
+            # are ref-counted) allocated when exitting the scope: the finalizer
+            # for that scope was not called in that case.
+            lambda c: c.get_bigint() == BigIntLiteral(0)
+        )
+
+
+class Example(FooNode):
+    token_node = True
+
+
+build_and_run(lkt_file='expected_concrete_syntax.lkt', ada_main="main.adb",
+              types_from_lkt=False)
+print('Done')

testsuite/tests/properties/quantifier_refcount/test.yaml

@@ -0,0 +1 @@
+driver: python