Add llvm-kompile-type to target options (runtimeverification/pyk#289)

This PR threads the new options from
#3259 through `kbuild` and
`Kompile`.

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>

pyk/package/version

@@ -1 +1 @@
-0.1.246
+0.1.247

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.246"
+version = "0.1.247"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

pyk/src/pyk/kbuild/project.py

@@ -16,7 +16,7 @@
     check_relative_path,
     relative_path,
 )
-from ..ktool.kompile import KompileBackend
+from ..ktool.kompile import KompileBackend, LLVMKompileType
 from ..utils import FrozenDict, single
 from .config import PROJECT_FILE_NAME
 
@@ -82,11 +82,14 @@ class Target:
     hook_namespaces: tuple[str, ...] | None
     emit_json: bool | None
     gen_bison_parser: bool | None
+    bison_parser_library: bool | None
     # LLVM backend
     opt_level: int | None
     ccopts: tuple[str, ...] | None
     no_llvm_kompile: bool | None
     enable_search: bool | None
+    llvm_kompile_type: LLVMKompileType | None
+    llvm_kompile_output: str | None
     # Haskell backend
     concrete_rules: tuple[str, ...] | None
 
@@ -102,10 +105,13 @@ def __init__(
         hook_namespaces: Iterable[str] | None = None,
         emit_json: bool | None = None,
         gen_bison_parser: bool | None = None,
+        bison_parser_library: bool | None = None,
         opt_level: int | None = None,
         ccopts: Iterable[str] | None = None,
         no_llvm_kompile: bool | None = None,
         enable_search: bool | None = None,
+        llvm_kompile_type: LLVMKompileType | None = None,
+        llvm_kompile_output: str | None = None,
         concrete_rules: Iterable[str] | None = None,
     ):
         main_file = Path(main_file)
@@ -119,10 +125,13 @@ def __init__(
         object.__setattr__(self, 'hook_namespaces', tuple(hook_namespaces) if hook_namespaces is not None else None)
         object.__setattr__(self, 'emit_json', emit_json)
         object.__setattr__(self, 'gen_bison_parser', gen_bison_parser)
+        object.__setattr__(self, 'bison_parser_library', bison_parser_library)
         object.__setattr__(self, 'opt_level', opt_level)
         object.__setattr__(self, 'ccopts', tuple(ccopts) if ccopts is not None else None)
         object.__setattr__(self, 'no_llvm_kompile', no_llvm_kompile)
         object.__setattr__(self, 'enable_search', enable_search)
+        object.__setattr__(self, 'llvm_kompile_type', llvm_kompile_type)
+        object.__setattr__(self, 'llvm_kompile_output', llvm_kompile_output)
         object.__setattr__(self, 'concrete_rules', tuple(concrete_rules) if concrete_rules is not None else None)
 
     @staticmethod
@@ -137,10 +146,13 @@ def from_dict(name: str, dct: Mapping[str, Any]) -> Target:
             hook_namespaces=dct.get('hook-namespaces'),
             emit_json=dct.get('emit-json'),
             gen_bison_parser=dct.get('gen-bison-parser'),
+            bison_parser_library=dct.get('bison-parser-library'),
             opt_level=dct.get('opt-level'),
             ccopts=dct.get('ccopts'),
             no_llvm_kompile=dct.get('no-llvm-kompile'),
             enable_search=dct.get('enable-search'),
+            llvm_kompile_type=LLVMKompileType(dct['llvm-kompile-type']) if 'llvm-kompile-type' in dct else None,
+            llvm_kompile_output=dct.get('llvm-kompile-output'),
             concrete_rules=dct.get('concrete-rules'),
         )
 

pyk/src/pyk/ktool/kompile.py

@@ -46,10 +46,12 @@ def kompile(
     hook_namespaces: Iterable[str] = (),
     emit_json: bool = True,
     gen_bison_parser: bool = False,
+    bison_parser_library: bool = False,
     debug: bool = False,
     post_process: str | None = None,
     # LLVM backend
     llvm_kompile_type: LLVMKompileType | None = None,
+    llvm_kompile_output: str | None = None,
     opt_level: int | None = None,
     ccopts: Iterable[str] = (),
     no_llvm_kompile: bool = False,
@@ -71,6 +73,7 @@ def kompile(
 
     if backend and backend != KompileBackend.LLVM:
         _check_backend_param(llvm_kompile_type is None, 'llvm_kompile_type', backend)
+        _check_backend_param(llvm_kompile_output is None, 'llvm_kompile_output', backend)
         _check_backend_param(opt_level is None, 'opt_level', backend)
         _check_backend_param(not list(ccopts), 'ccopts', backend)
         _check_backend_param(not no_llvm_kompile, 'no_llvm_kompile', backend)
@@ -96,9 +99,11 @@ def kompile(
         hook_namespaces=hook_namespaces,
         emit_json=emit_json,
         gen_bison_parser=gen_bison_parser,
+        bison_parser_library=bison_parser_library,
         debug=debug,
         post_process=post_process,
         llvm_kompile_type=llvm_kompile_type,
+        llvm_kompile_output=llvm_kompile_output,
         enable_search=enable_search,
         opt_level=opt_level,
         ccopts=ccopts,
@@ -133,6 +138,7 @@ def llvm_kompile(
     hook_namespaces: Iterable[str] = (),
     emit_json: bool = True,
     gen_bison_parser: bool = False,
+    bison_parser_library: bool = False,
     debug: bool = False,
     post_process: str | None = None,
     llvm_kompile_type: LLVMKompileType | None = None,
@@ -156,6 +162,7 @@ def llvm_kompile(
         hook_namespaces=hook_namespaces,
         emit_json=emit_json,
         gen_bison_parser=gen_bison_parser,
+        bison_parser_library=bison_parser_library,
         debug=debug,
         post_process=post_process,
         opt_level=opt_level,
@@ -181,6 +188,7 @@ def haskell_kompile(
     hook_namespaces: Iterable[str] = (),
     emit_json: bool = True,
     gen_bison_parser: bool = False,
+    bison_parser_library: bool = False,
     debug: bool = False,
     post_process: str | None = None,
     concrete_rules: Iterable[str] = (),
@@ -200,6 +208,7 @@ def haskell_kompile(
         hook_namespaces=hook_namespaces,
         emit_json=emit_json,
         gen_bison_parser=gen_bison_parser,
+        bison_parser_library=bison_parser_library,
         debug=debug,
         post_process=post_process,
         concrete_rules=concrete_rules,
@@ -226,9 +235,11 @@ def _build_arg_list(
     hook_namespaces: Iterable[str],
     emit_json: bool,
     gen_bison_parser: bool,
+    bison_parser_library: bool,
     debug: bool = False,
     post_process: str | None,
     llvm_kompile_type: LLVMKompileType | None = None,
+    llvm_kompile_output: str | None = None,
     opt_level: int | None,
     ccopts: Iterable[str],
     no_llvm_kompile: bool,
@@ -264,6 +275,9 @@ def _build_arg_list(
     if gen_bison_parser:
         args.append('--gen-bison-parser')
 
+    if bison_parser_library:
+        args.append('--bison-parser-library')
+
     if debug:
         args.append('--debug')
 
@@ -273,6 +287,9 @@ def _build_arg_list(
     if llvm_kompile_type is not None:
         args.extend(['--llvm-kompile-type', llvm_kompile_type.value])
 
+    if llvm_kompile_output is not None:
+        args.extend(['--llvm-kompile-output', llvm_kompile_output])
+
     if opt_level:
         args.append(f'-O{opt_level}')
 

pyk/src/tests/unit/ktool/test_kompile.py

@@ -36,6 +36,7 @@ def test_all_args_1() -> None:
         hook_namespaces=['JSON', 'KRYPTO', 'BLOCKCHAIN'],
         emit_json=True,
         gen_bison_parser=False,
+        bison_parser_library=False,
         post_process='echo "hello"',
         opt_level=None,
         ccopts=(),
@@ -82,6 +83,7 @@ def test_all_args_2() -> None:
         hook_namespaces=['JSON', 'KRYPTO', 'BLOCKCHAIN'],
         emit_json=True,
         gen_bison_parser=False,
+        bison_parser_library=False,
         post_process='echo "hello"',
         opt_level=None,
         ccopts=(),