Add support for project files to code optimizer

Ref. eng/recordflux/RecordFlux#1766
AdaCore · Aug 29, 2024 · dfb5354 · dfb5354
1 parent 42ec1b0
commit dfb5354
Show file tree

Hide file tree

Showing 12 changed files with 369 additions and 196 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -10,11 +10,18 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Added
 
 - Vim and Neovim syntax highlighting support (eng/recordflux/RecordFlux#1749)
+- Project file support in code optimizer (eng/recordflux/RecordFlux#1766)
 
 ### Changed
 
+- CLI subcommand `rflx optimize` expects project file instead of directory containing generated code (eng/recordflux/RecordFlux#1766)
 - Improve generation of predicate for single-field messages (eng/recordflux/RecordFlux#1761)
 
+### Removed
+
+- CLI flag `--optimize` of `rflx generate` subcommand (eng/recordflux/RecordFlux#1766)
+- CLI option `--timeout` of `rflx generate` and `rflx optimize` subcommands (eng/recordflux/RecordFlux#1766)
+
 ## [0.23.0] - 2024-08-23
 
 ### Changed

diff --git a/doc/user_guide/20-overview.rst b/doc/user_guide/20-overview.rst
@@ -84,6 +84,9 @@ As only successfully verified specifications are guaranteed to lead to provable
 SPARK source files are generated into the directory specified by the `-d` switch on the command line.
 The result can be included in the list of source directories and analyzed by `gnatprove` as usual (see the `SPARK User’s Guide <https://docs.adacore.com/live/wave/spark2014/html/spark2014_ug/>`_ for details).
 
+The Optimizer reduces the size of the generated state machine code.
+In order to use the Optimizer, a project file for the SPARK code must be provided by the user and passed as an argument to `rflx optimize`.
+
 The Validator is available through the `rflx validate` subcommand on the command line.
 It can be used to check whether a message specification correctly formalizes real-world data, or vice versa, whether a given data sample corresponds to the specification.
 Two types of samples can be used: valid samples which must be accepted by a specification (passed with the `-v` option) and invalid samples which must be rejected (passed with the `-i` option).

diff --git a/doc/user_guide/90-rflx-generate--help.txt b/doc/user_guide/90-rflx-generate--help.txt
@@ -2,7 +2,7 @@ usage: rflx generate [-h] [-p PREFIX] [-n] [-d OUTPUT_DIRECTORY]
                      [--debug {built-in,external}]
                      [--ignore-unsupported-checksum]
                      [--integration-files-dir INTEGRATION_FILES_DIR]
-                     [--reproducible] [--optimize] [--timeout TIMEOUT]
+                     [--reproducible]
                      [SPECIFICATION_FILE ...]
 
 positional arguments:
@@ -21,7 +21,3 @@ options:
   --integration-files-dir INTEGRATION_FILES_DIR
                         directory for the .rfi files
   --reproducible        ensure reproducible output
-  --optimize            optimize generated state machine code (requires
-                        GNATprove)
-  --timeout TIMEOUT     prover timeout in seconds for code optimization
-                        (default: 1)
diff --git a/doc/user_guide/90-rflx-optimize--help.txt b/doc/user_guide/90-rflx-optimize--help.txt
@@ -1,8 +1,7 @@
-usage: rflx optimize [-h] [--timeout TIMEOUT] DIRECTORY
+usage: rflx optimize [-h] PROJECT_FILE
 
 positional arguments:
-  DIRECTORY          directory containing the generated code
+  PROJECT_FILE  project file
 
 options:
-  -h, --help         show this help message and exit
-  --timeout TIMEOUT  prover timeout in seconds (default: 1)
+  -h, --help    show this help message and exit
diff --git a/rflx/cli.py b/rflx/cli.py
@@ -233,17 +233,6 @@ def main(  # noqa: PLR0915
         action="store_true",
         help="ensure reproducible output",
     )
-    parser_generate.add_argument(
-        "--optimize",
-        action="store_true",
-        help="optimize generated state machine code (requires GNATprove)",
-    )
-    parser_generate.add_argument(
-        "--timeout",
-        type=int,
-        default=1,
-        help="prover timeout in seconds for code optimization (default: %(default)s)",
-    )
     parser_generate.add_argument(
         "files",
         metavar="SPECIFICATION_FILE",
@@ -258,18 +247,13 @@ def main(  # noqa: PLR0915
         help="optimize generated state machine code",
     )
     parser_optimize.add_argument(
-        "--timeout",
-        type=int,
-        default=1,
-        help="prover timeout in seconds (default: %(default)s)",
-    )
-    parser_optimize.add_argument(
-        "directory",
-        metavar="DIRECTORY",
+        "project_file",
+        metavar="PROJECT_FILE",
         type=Path,
-        help="directory containing the generated code",
+        help="project file",
     )
     parser_optimize.set_defaults(func=optimize)
+
     parser_graph = subparsers.add_parser("graph", help="generate graphs")
     parser_graph.add_argument(
         "-f",
@@ -523,15 +507,12 @@ def generate(args: argparse.Namespace) -> None:
         top_level_package=args.prefix == DEFAULT_PREFIX,
     )
 
-    if args.optimize:
-        optimizer.optimize(args.output_directory, args.workers, args.timeout)
-
 
 def optimize(args: argparse.Namespace) -> None:
-    if not args.directory.is_dir():
-        fail(f'directory not found: "{args.directory}"')
+    if not args.project_file.is_file():
+        fail(f'project file not found: "{args.project_file}"')
 
-    optimizer.optimize(args.directory, args.workers, args.timeout)
+    optimizer.optimize(args.project_file)
 
 
 def parse(

diff --git a/rflx/generator/const.py b/rflx/generator/const.py
@@ -7,7 +7,10 @@
 from rflx.common import file_name
 from rflx.identifier import ID
 
+GENERATED_BY_RECORDFLUX: Final = "Generated by RecordFlux"
+
 REFINEMENT_PACKAGE = ID("Contains")
+STATE_MACHINE_PACKAGE = ID("FSM")
 
 ARITHMETIC_PACKAGE = ID("RFLX_Arithmetic")
 BUILTIN_TYPES_CONVERSIONS_PACKAGE = ID("RFLX_Builtin_Types.Conversions")

diff --git a/rflx/generator/generator.py b/rflx/generator/generator.py
@@ -1575,7 +1575,7 @@ def _license_header(self) -> str:
                 common.comment_box(
                     [
                         "",
-                        "Generated by RecordFlux",
+                        const.GENERATED_BY_RECORDFLUX,
                         "",
                         "Copyright (C) AdaCore",
                         "",
@@ -1591,7 +1591,7 @@ def _license_header(self) -> str:
             common.comment_box(
                 [
                     "",
-                    f"Generated by RecordFlux {__version__} on {today}",
+                    f"{const.GENERATED_BY_RECORDFLUX} {__version__} on {today}",
                     "",
                     f"Copyright (C) 2018-{today.year} AdaCore",
                     "",