Enable use of externally defined debug output function

Ref. #1052

rflx/cli.py

@@ -13,7 +13,7 @@
 
 from rflx import __version__
 from rflx.error import ERROR_CONFIG, FatalError, RecordFluxError, Severity, Subsystem, fail
-from rflx.generator import Generator
+from rflx.generator import Debug, Generator
 from rflx.graph import Graph
 from rflx.identifier import ID
 from rflx.integration import Integration
@@ -77,8 +77,9 @@ def main(argv: List[str]) -> Union[int, str]:
     )
     parser_generate.add_argument(
         "--debug",
+        default=None,
+        choices=["built-in", "external"],
         help="enable adding of debug output to generated code",
-        action="store_true",
     )
     parser_generate.add_argument(
         "--ignore-unsupported-checksum",
@@ -262,14 +263,18 @@ def generate(args: argparse.Namespace) -> None:
         args.prefix,
         workers=args.workers,
         reproducible=os.environ.get("RFLX_REPRODUCIBLE") is not None,
-        debug=args.debug,
+        debug=Debug.BUILTIN
+        if args.debug == "built-in"
+        else Debug.EXTERNAL
+        if args.debug == "external"
+        else Debug.NONE,
         ignore_unsupported_checksum=args.ignore_unsupported_checksum,
     )
-    generator.write_units(args.output_directory)
-    if not args.no_library:
-        generator.write_library_files(args.output_directory)
-    if args.prefix == DEFAULT_PREFIX:
-        generator.write_top_level_package(args.output_directory)
+    generator.write_files(
+        args.output_directory,
+        library_files=not args.no_library,
+        top_level_package=args.prefix == DEFAULT_PREFIX,
+    )
 
 
 def parse(

rflx/generator/__init__.py

@@ -1 +1,2 @@
+from .common import Debug as Debug  # noqa: F401
 from .generator import Generator as Generator  # noqa: F401

rflx/generator/common.py

@@ -1,5 +1,6 @@
 # pylint: disable = too-many-lines
 
+import enum
 from typing import Callable, List, Mapping, Optional, Sequence, Tuple
 
 from rflx import expression as expr, identifier as rid, model
@@ -54,6 +55,12 @@
 EMPTY_ARRAY = NamedAggregate((ValueRange(Number(1), Number(0)), Number(0)))
 
 
+class Debug(enum.Enum):
+    NONE = enum.auto()
+    BUILTIN = enum.auto()
+    EXTERNAL = enum.auto()
+
+
 def substitution(
     message: model.Message,
     prefix: str,

rflx/generator/generator.py

@@ -122,7 +122,7 @@ def __init__(
         prefix: str = "",
         workers: int = 1,
         reproducible: bool = False,
-        debug: bool = False,
+        debug: common.Debug = common.Debug.NONE,
         ignore_unsupported_checksum: bool = False,
     ) -> None:
         self.__prefix = str(ID(prefix)) if prefix else ""
@@ -140,6 +140,15 @@ def __init__(
 
         self.__generate(model, integration)
 
+    def write_files(
+        self, directory: Path, library_files: bool = True, top_level_package: bool = True
+    ) -> None:
+        self.write_units(directory)
+        if library_files:
+            self.write_library_files(directory)
+        if top_level_package:
+            self.write_top_level_package(directory)
+
     def write_library_files(self, directory: Path) -> None:
         for template_filename in const.LIBRARY_FILES:
             self.__check_template_file(template_filename)
@@ -160,6 +169,34 @@ def write_library_files(self, directory: Path) -> None:
                 ),
             )
 
+        if self.__debug == common.Debug.EXTERNAL:
+            debug_package_id = self.__prefix * ID("RFLX_Debug")
+            create_file(
+                directory / f"{file_name(str(debug_package_id))}.ads",
+                self.__license_header()
+                + PackageUnit(
+                    [],
+                    PackageDeclaration(
+                        debug_package_id,
+                        [
+                            SubprogramDeclaration(
+                                ProcedureSpecification(
+                                    "Print",
+                                    [
+                                        Parameter(["Message"], "String"),
+                                    ],
+                                )
+                            )
+                        ],
+                        aspects=[
+                            SparkMode(),
+                        ],
+                    ),
+                    [],
+                    PackageBody(debug_package_id),
+                ).ads,
+            )
+
     def write_top_level_package(self, directory: Path) -> None:
         if self.__prefix:
             create_file(

rflx/generator/session.py

@@ -102,7 +102,7 @@
 from rflx.error import Location, Subsystem, fail, fatal_fail
 from rflx.model import declaration as decl, statement as stmt
 
-from . import const
+from . import common, const
 from .allocator import AllocatorGenerator
 
 
@@ -206,7 +206,7 @@ def __init__(
         session: model.Session,
         allocator: AllocatorGenerator,
         prefix: str = "",
-        debug: bool = False,
+        debug: common.Debug = common.Debug.NONE,
     ) -> None:
         self._session = session
         self._prefix = prefix
@@ -262,7 +262,15 @@ def _create_context(self) -> Tuple[List[ContextItem], List[ContextItem]]:
             declaration_context.append(WithClause(self._prefix * const.TYPES_PACKAGE))
 
         body_context: List[ContextItem] = [
-            *([WithClause("Ada.Text_IO")] if self._debug else []),
+            *(
+                [
+                    WithClause(self._prefix * ID("RFLX_Debug"))
+                    if self._debug == common.Debug.EXTERNAL
+                    else WithClause("Ada.Text_IO")
+                ]
+                if self._debug != common.Debug.NONE
+                else []
+            ),
         ]
 
         for referenced_types, context in [
@@ -4636,7 +4644,18 @@ def _convert_type(
         return expr.Conversion(target_type.identifier, expression)
 
     def _debug_output(self, string: str) -> List[CallStatement]:
-        return [CallStatement("Ada.Text_IO.Put_Line", [String(string)])] if self._debug else []
+        return (
+            [
+                CallStatement(
+                    self._prefix * ID("RFLX_Debug.Print")
+                    if self._debug == common.Debug.EXTERNAL
+                    else "Ada.Text_IO.Put_Line",
+                    [String(string)],
+                )
+            ]
+            if self._debug != common.Debug.NONE
+            else []
+        )
 
 
 def copy_id(identifier: ID) -> ID:

tests/integration/specification_model_generator_test.py

@@ -1,7 +1,9 @@
+import textwrap
 from pathlib import Path
 
 import pytest
 
+from rflx.generator import Debug
 from rflx.integration import Integration
 from rflx.specification import Parser
 from tests import utils
@@ -786,3 +788,73 @@ def test_session_single_channel(mode: str, action: str, tmp_path: Path) -> None:
         end Test;
     """
     utils.assert_compilable_code_string(spec, tmp_path)
+
+
+@pytest.mark.parametrize(
+    "debug, expected",
+    [
+        (Debug.NONE, ""),
+        (Debug.BUILTIN, "State: A\nState: B\nState: C\n"),
+        (Debug.EXTERNAL, "XState: A\nXState: B\nXState: C\n"),
+    ],
+)
+def test_session_external_debug_output(debug: Debug, expected: str, tmp_path: Path) -> None:
+    spec = """
+        package Test is
+
+           generic
+           session Session with
+              Initial => A,
+              Final => D
+           is
+           begin
+              state A is
+              begin
+              transition
+                 goto B
+              end A;
+
+              state B is
+              begin
+              transition
+                 goto C
+              end B;
+
+              state C is
+              begin
+              transition
+                 goto D
+              end C;
+
+              state D is null state;
+           end Session;
+
+        end Test;
+    """
+    parser = Parser()
+    parser.parse_string(spec)
+    model = parser.create_model()
+    integration = parser.get_integration()
+
+    for filename, content in utils.session_main().items():
+        (tmp_path / filename).write_text(content)
+
+    (tmp_path / "rflx-rflx_debug.adb").write_text(
+        textwrap.dedent(
+            """\
+            with Ada.Text_IO;
+
+            package body RFLX.RFLX_Debug with
+               SPARK_Mode
+            is
+
+               procedure Print (Message : String) is
+               begin
+                  Ada.Text_IO.Put_Line ("X" & Message);
+               end Print;
+
+            end RFLX.RFLX_Debug;"""
+        )
+    )
+
+    assert utils.assert_executable_code(model, integration, tmp_path, debug=debug) == expected

tests/unit/cli_test.py

@@ -1,3 +1,5 @@
+from __future__ import annotations
+
 import re
 from pathlib import Path
 from typing import Callable
@@ -6,7 +8,7 @@
 from _pytest.monkeypatch import MonkeyPatch
 
 import rflx.specification
-from rflx import cli, validator
+from rflx import cli, generator, validator
 from rflx.error import Location, Severity, Subsystem, fail, fatal_fail
 from rflx.pyrflx import PyRFLXError
 from tests.const import SPEC_DIR
@@ -133,6 +135,37 @@ def test_main_generate_non_existent_directory() -> None:
     )
 
 
+@pytest.mark.parametrize(
+    "args, expected",
+    [
+        ([], generator.Debug.NONE),
+        (["--debug", "built-in"], generator.Debug.BUILTIN),
+        (["--debug", "external"], generator.Debug.EXTERNAL),
+    ],
+)
+def test_main_generate_debug(
+    args: list[str], expected: generator.Debug, monkeypatch: MonkeyPatch, tmp_path: Path
+) -> None:
+    result = []
+
+    def generator_mock(  # pylint: disable = too-many-arguments, unused-argument
+        self: object,
+        model: object,
+        integration: object,
+        prefix: str,
+        workers: int,
+        reproducible: bool,
+        debug: generator.Debug,
+        ignore_unsupported_checksum: bool,
+    ) -> None:
+        result.append(debug)
+
+    monkeypatch.setattr(generator.Generator, "__init__", generator_mock)
+    monkeypatch.setattr(generator.Generator, "write_files", lambda x: None)
+    cli.main(["rflx", "generate", "-d", str(tmp_path), *args, SPEC_FILE])
+    assert result == [expected]
+
+
 def test_main_graph(tmp_path: Path) -> None:
     assert cli.main(["rflx", "graph", "-d", str(tmp_path), SPEC_FILE]) == 0