kompilex command for pyk (#4342)

Implements the command `pyk kompilex` which uses pyk's outer parser to
parse in a K Definition and then hands it off to the java frontend to
handle the rest of the compilation.

Some bootstrapping is required because the conversions from the outer
parsed structures to something compatible with the java frontend aren't
fully implemented. For the integration tests, a `prelude-modules.json`
file is included in the test data folder which has the K prelude already
outer parsed.

This will only handle modules that are empty or import other modules.
The goal is to expand this capability until the full K language is
supported, and then the bootstrapping will no longer be necessary.

---------

Co-authored-by: Bruce Collie <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

pyk/src/pyk/__main__.py

@@ -6,6 +6,7 @@
 from collections.abc import Iterable
 from contextlib import contextmanager
 from pathlib import Path
+from tempfile import NamedTemporaryFile
 from typing import TYPE_CHECKING
 
 from graphviz import Digraph
@@ -15,6 +16,8 @@
 from .coverage import get_rule_by_id, strip_coverage_logger
 from .cterm import CTerm
 from .cterm.symbolic import cterm_symbolic
+from .kast import KAst
+from .kast.att import KAtt
 from .kast.inner import KInner
 from .kast.manip import (
     flatten_label,
@@ -24,7 +27,7 @@
     remove_source_map,
     split_config_and_constraints,
 )
-from .kast.outer import read_kast_definition
+from .kast.outer import KFlatModule, read_kast_definition
 from .kast.pretty import PrettyPrinter
 from .kast.utils import parse_outer
 from .kcfg import KCFGExplore
@@ -39,7 +42,7 @@
 from .prelude.ml import is_top, mlAnd, mlOr
 from .proof.reachability import APRFailureInfo, APRProof
 from .proof.show import APRProofNodePrinter, APRProofShow
-from .utils import check_dir_path, check_file_path, ensure_dir_path, exit_with_process_error
+from .utils import check_file_path, ensure_dir_path, exit_with_process_error
 
 if TYPE_CHECKING:
     from collections.abc import Iterator
@@ -50,6 +53,7 @@
         GraphImportsOptions,
         JsonToKoreOptions,
         KompileCommandOptions,
+        KompileXCommandOptions,
         KoreToJsonOptions,
         ParseOuterOptions,
         PrintOptions,
@@ -70,6 +74,8 @@ def main() -> None:
     # This change makes it so that in most cases, by default, pyk doesn't run out of stack space.
     sys.setrecursionlimit(10**7)
 
+    logging.basicConfig(format=LOG_FORMAT)
+
     cli_parser = create_argument_parser()
     args = cli_parser.parse_args()
     toml_args = parse_toml_args(args)
@@ -80,7 +86,7 @@ def main() -> None:
 
     options = generate_options(stripped_args)
 
-    logging.basicConfig(level=loglevel(args), format=LOG_FORMAT)
+    logging.basicConfig(level=loglevel(args), format=LOG_FORMAT, force=True)
 
     executor_name = 'exec_' + args.command.lower().replace('-', '_')
     if executor_name not in globals():
@@ -303,12 +309,13 @@ def exec_kompile(options: KompileCommandOptions) -> None:
         'syntax_module': options.syntax_module,
         'main_module': options.main_module,
         'md_selector': options.md_selector,
-        'include_dirs': (Path(include) for include in options.includes),
+        'include_dirs': options.includes,
         'emit_json': options.emit_json,
         'coverage': options.coverage,
         'gen_bison_parser': options.gen_bison_parser,
         'gen_glr_bison_parser': options.gen_glr_bison_parser,
         'bison_lists': options.bison_lists,
+        'outer_parsed_json': options.outer_parsed_json,
     }
     if options.backend == KompileBackend.LLVM:
         kompile_dict['ccopts'] = options.ccopts
@@ -404,21 +411,10 @@ def exec_json_to_kore(options: JsonToKoreOptions) -> None:
 
 def exec_parse_outer(options: ParseOuterOptions) -> None:
     definition_file = options.main_file.resolve()
-    search_paths = [definition_file.parent]
-    for include in getattr(options, 'includes', []):
-        include_path = Path(include)
-        try:
-            check_dir_path(include_path)
-        except ValueError:
-            _LOGGER.warning(f"Could not find directory '{include}' passed to -I")
-        search_paths.append(include_path.resolve())
-
-    main_module_name = getattr(options, 'main_module', definition_file.stem.upper())
-    try:
-        final_definition = parse_outer(definition_file, main_module_name, search_paths, options.md_selector)
-    except Exception as e:
-        _LOGGER.critical(e)
-        exit(1)
+    search_paths = [definition_file.parent, *options.includes]
+    main_module_name = options.main_module or definition_file.stem.upper()
+
+    final_definition = parse_outer(definition_file, main_module_name, search_paths, options.md_selector)
 
     result_text = json.dumps(final_definition.to_dict())
     try:
@@ -427,5 +423,44 @@ def exec_parse_outer(options: ParseOuterOptions) -> None:
         sys.stdout.write(f'{result_text}\n')
 
 
+def exec_kompilex(options: KompileXCommandOptions) -> None:
+    definition_file = Path(options.main_file).resolve()
+    search_paths = [definition_file.parent, *options.includes]
+    main_module_name = options.main_module or definition_file.stem.upper()
+
+    final_definition = parse_outer(definition_file, main_module_name, search_paths, options.md_selector)
+
+    if options.pre_parsed_prelude:
+        prelude_json = json.loads(options.pre_parsed_prelude.read())
+        prelude_modules = tuple(KFlatModule.from_dict(mod) for mod in prelude_json)
+        final_definition = final_definition.let(all_modules=final_definition.all_modules + prelude_modules)
+
+    syntax_module_name = options.syntax_module or main_module_name + '-SYNTAX'
+    if syntax_module_name not in [m.name for m in final_definition.all_modules]:
+        base_msg = f'Could not find main syntax module with name {syntax_module_name} in definition.'
+        if options.syntax_module:
+            _LOGGER.error(base_msg)
+            exit(1)
+        else:
+            _LOGGER.warn(f'{base_msg} Use --syntax-module to specify one. Using {main_module_name} as default.')
+        syntax_module_name = main_module_name
+    syntax_att = KAtt.parse({'syntaxModule': main_module_name})
+
+    final_definition = final_definition.let_att(syntax_att)
+
+    kast_json = {'format': 'KAST', 'version': KAst.version(), 'term': final_definition.to_dict()}
+
+    with NamedTemporaryFile('w', prefix='pyk_kompilex_', delete=not options.debug) as ntf:
+        ntf.write(json.dumps(kast_json))
+        ntf.flush()
+
+        options.main_file = ntf.name
+        options.outer_parsed_json = True
+        if options.definition_dir is None:
+            options.definition_dir = Path(f'{definition_file.stem}-kompiled')
+
+        exec_kompile(options)
+
+
 if __name__ == '__main__':
     main()

pyk/src/pyk/cli/args.py

@@ -1,5 +1,6 @@
 from __future__ import annotations
 
+import logging
 import sys
 from argparse import ArgumentParser, FileType
 from functools import cached_property
@@ -12,9 +13,12 @@
 
 if TYPE_CHECKING:
     from collections.abc import Callable, Iterable
+    from typing import Final
 
     from ..utils import BugReport
 
+_LOGGER: Final = logging.getLogger(__name__)
+
 
 class LoggingOptions(Options):
     debug: bool
@@ -99,12 +103,24 @@ def default() -> dict[str, Any]:
 
 
 class KDefinitionOptions(Options):
-    includes: list[str]
+    includes: list[Path]
     main_module: str | None
     syntax_module: str | None
     spec_module: str | None
     md_selector: str
 
+    def __init__(self, args: dict[str, Any]) -> None:
+        if 'includes' in args:
+            include_paths = []
+            for include in args['includes']:
+                include_path = Path(include)
+                if include_path.is_dir():
+                    include_paths.append(include_path.resolve())
+                else:
+                    _LOGGER.warning(f"Could not find directory '{include}' passed to -I")
+            args['includes'] = include_paths
+        super().__init__(args)
+
     @staticmethod
     def default() -> dict[str, Any]:
         return {
@@ -189,6 +205,7 @@ class KompileOptions(Options):
     gen_glr_bison_parser: bool
     bison_lists: bool
     no_exc_wrap: bool
+    outer_parsed_json: bool
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -212,6 +229,7 @@ def default() -> dict[str, Any]:
             'gen_glr_bison_parser': False,
             'bison_lists': False,
             'no_exc_wrap': False,
+            'outer_parsed_json': False,
         }
 
     @staticmethod

pyk/src/pyk/cli/pyk.py

@@ -58,6 +58,8 @@ def generate_options(args: dict[str, Any]) -> LoggingOptions:
             return ProveOptions(args)
         case 'kompile':
             return KompileCommandOptions(args)
+        case 'kompilex':
+            return KompileXCommandOptions(args)
         case 'run':
             return RunOptions(args)
         case 'parse-outer':
@@ -89,6 +91,8 @@ def get_option_string_destination(command: str, option_string: str) -> str:
             option_string_destinations = ProveOptions.from_option_string()
         case 'kompile':
             option_string_destinations = KompileCommandOptions.from_option_string()
+        case 'kompilex':
+            option_string_destinations = KompileXCommandOptions.from_option_string()
         case 'run':
             option_string_destinations = RunOptions.from_option_string()
 
@@ -299,6 +303,16 @@ def get_argument_type() -> dict[str, Callable]:
         )
 
 
+class KompileXCommandOptions(KompileCommandOptions):
+    pre_parsed_prelude: IO[Any] | None
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'pre_parsed_prelude': None,
+        }
+
+
 class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions):
     definition_dir: Path | None
     type_inference_mode: TypeInferenceMode | None
@@ -358,16 +372,17 @@ def get_argument_type() -> dict[str, Callable]:
         return LoggingOptions.get_argument_type() | {'definition': dir_path}
 
 
-class ParseOuterOptions(LoggingOptions):
+class ParseOuterOptions(LoggingOptions, KDefinitionOptions):
     main_file: Path
-    md_selector: str
-    includes: Iterable[str]
     output_file: IO[Any]
-    main_module: str
 
     @staticmethod
     def get_argument_type() -> dict[str, Callable]:
-        return LoggingOptions.get_argument_type() | {'main_file': dir_path, 'output-file': FileType('w')}
+        return (
+            LoggingOptions.get_argument_type()
+            | KDefinitionOptions.get_argument_type()
+            | {'main_file': file_path, 'output_file': FileType('w')}
+        )
 
 
 def create_argument_parser() -> ArgumentParser:
@@ -444,6 +459,25 @@ def create_argument_parser() -> ArgumentParser:
     )
     kompile_args.add_argument('main_file', type=str, help='File with the specification module.')
 
+    kompilex_args = pyk_args_command.add_parser(
+        'kompilex',
+        help='Kompile the K specification.',
+        parents=[
+            k_cli_args.logging_args,
+            k_cli_args.warning_args,
+            k_cli_args.definition_args,
+            k_cli_args.kompile_args,
+            config_args.config_args,
+        ],
+    )
+    kompilex_args.add_argument('main_file', type=str, help='File with the specification module.')
+    kompilex_args.add_argument(
+        '--pre-parsed-prelude',
+        dest='pre_parsed_prelude',
+        type=FileType('r'),
+        help='File with outer parsed modules from the prelude in JSON',
+    )
+
     run_args = pyk_args_command.add_parser(
         'run',
         help='Run a given program using the K definition.',
@@ -526,21 +560,10 @@ def create_argument_parser() -> ArgumentParser:
     parse_outer_args = pyk_args_command.add_parser(
         'parse-outer',
         help='Parse an outer K definition into JSON',
-        parents=[k_cli_args.logging_args, config_args.config_args],
+        parents=[k_cli_args.logging_args, k_cli_args.definition_args, config_args.config_args],
     )
     parse_outer_args.add_argument('main_file', type=file_path, help='File with the K definition')
-    parse_outer_args.add_argument(
-        '--md-selector', default='k', help='Code selector expression to use when reading markdown.'
-    )
     parse_outer_args.add_argument('--output-file', type=FileType('w'), help='Write output to file instead of stdout.')
-    parse_outer_args.add_argument(
-        '-I',
-        type=str,
-        dest='includes',
-        action='append',
-        help='Directories to lookup K definitions in.',
-    )
-    parse_outer_args.add_argument('--main-module', type=str, help='The name of the main module for the definition')
 
     return pyk_args
 

pyk/src/pyk/kast/att.py

@@ -108,6 +108,8 @@ def _freeze(obj: Any) -> Any:
 
     @staticmethod
     def _unfreeze(value: Any) -> Any:
+        if isinstance(value, tuple):
+            return [AnyType._unfreeze(v) for v in value]
         if isinstance(value, FrozenDict):
             return {k: AnyType._unfreeze(v) for (k, v) in value.items()}
         return value
@@ -339,6 +341,7 @@ class Atts:
     SOURCE: Final = AttKey('org.kframework.attributes.Source', type=_PATH)
     STRICT: Final = AttKey('strict', type=_ANY)
     SYMBOL: Final = AttKey('symbol', type=OptionalType(_STR))
+    SYNTAX_MODULE: Final = AttKey('syntaxModule', type=_STR)
     TERMINALS: Final = AttKey('terminals', type=_STR)
     TOKEN: Final = AttKey('token', type=_NONE)
     TOTAL: Final = AttKey('total', type=_NONE)

pyk/src/pyk/kast/outer.py

@@ -570,35 +570,35 @@ class KBubble(KSentence):
     """Represents an unparsed chunk of AST in user-defined syntax."""
 
     sentence_type: str
-    content: str
+    contents: str
     att: KAtt
 
-    def __init__(self, sentence_type: str, content: str, att: KAtt = EMPTY_ATT):
+    def __init__(self, sentence_type: str, contents: str, att: KAtt = EMPTY_ATT):
         object.__setattr__(self, 'sentence_type', sentence_type)
-        object.__setattr__(self, 'content', content)
+        object.__setattr__(self, 'contents', contents)
         object.__setattr__(self, 'att', att)
 
     @classmethod
     def _from_dict(cls: type[KBubble], d: Mapping[str, Any]) -> KBubble:
         return KBubble(
             sentence_type=d['sentenceType'],
-            content=d['content'],
+            contents=d['contents'],
             att=KAtt.from_dict(d['att']) if d.get('att') else EMPTY_ATT,
         )
 
     def to_dict(self) -> dict[str, Any]:
         return {
             'node': 'KBubble',
             'sentenceType': self.sentence_type,
-            'content': self.content,
+            'contents': self.contents,
             'att': self.att.to_dict(),
         }
 
-    def let(self, *, sentence_type: str | None = None, content: str | None = None, att: KAtt | None = None) -> KBubble:
+    def let(self, *, sentence_type: str | None = None, contents: str | None = None, att: KAtt | None = None) -> KBubble:
         sentence_type = sentence_type if sentence_type is not None else self.sentence_type
-        content = content if content is not None else self.content
+        contents = contents if contents is not None else self.contents
         att = att if att is not None else self.att
-        return KBubble(sentence_type=sentence_type, content=content, att=att)
+        return KBubble(sentence_type=sentence_type, contents=contents, att=att)
 
     def let_att(self, att: KAtt) -> KBubble:
         return self.let(att=att)

pyk/src/pyk/kast/pretty.py

@@ -253,7 +253,7 @@ def _print_ksyntaxpriority(self, ksyntaxpriority: KSyntaxPriority) -> str:
         return 'syntax priority ' + priorities_str + ' ' + att_str
 
     def _print_kbubble(self, kbubble: KBubble) -> str:
-        body = '// KBubble(' + kbubble.sentence_type + ', ' + kbubble.content + ')'
+        body = '// KBubble(' + kbubble.sentence_type + ', ' + kbubble.contents + ')'
         att_str = self.print(kbubble.att)
         return body + ' ' + att_str