From 97f40d972d23527482afcd3cdc0b8ac2bd7960aa Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Tue, 18 Apr 2023 16:27:26 +0100 Subject: [PATCH] Add llvm-kompile-type to target options (https://github.com/runtimeverification/pyk/pull/289) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR threads the new options from https://github.com/runtimeverification/k/pull/3259 through `kbuild` and `Kompile`. --------- Co-authored-by: devops Co-authored-by: Tamás Tóth --- pyk/package/version | 2 +- pyk/pyproject.toml | 2 +- pyk/src/pyk/kbuild/project.py | 14 +++++++++++++- pyk/src/pyk/ktool/kompile.py | 17 +++++++++++++++++ pyk/src/tests/unit/ktool/test_kompile.py | 2 ++ 5 files changed, 34 insertions(+), 3 deletions(-) diff --git a/pyk/package/version b/pyk/package/version index e1762ed856e..e60ec70e78a 100644 --- a/pyk/package/version +++ b/pyk/package/version @@ -1 +1 @@ -0.1.246 +0.1.247 diff --git a/pyk/pyproject.toml b/pyk/pyproject.toml index 6950c84d96e..fab9d254fdf 100644 --- a/pyk/pyproject.toml +++ b/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. ", diff --git a/pyk/src/pyk/kbuild/project.py b/pyk/src/pyk/kbuild/project.py index 7636d613e91..6b7517e5719 100644 --- a/pyk/src/pyk/kbuild/project.py +++ b/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'), ) diff --git a/pyk/src/pyk/ktool/kompile.py b/pyk/src/pyk/ktool/kompile.py index 2268cf28cd6..ea2cc857265 100644 --- a/pyk/src/pyk/ktool/kompile.py +++ b/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}') diff --git a/pyk/src/tests/unit/ktool/test_kompile.py b/pyk/src/tests/unit/ktool/test_kompile.py index 54112b64882..40eb79a8fd7 100644 --- a/pyk/src/tests/unit/ktool/test_kompile.py +++ b/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=(),