Add support for some missing Booster options (runtimeverification/pyk#826)

Fixes #816

Adds
* `--fallback-on`
* `--interim-simplification`
* `--no-post-exec-simplify`

---------

Co-authored-by: devops <[email protected]>

Author: 2 people

pyk/docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.590'
-release = '0.1.590'
+version = '0.1.591'
+release = '0.1.591'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

pyk/package/version

@@ -1 +1 @@
-0.1.590
+0.1.591

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.590"
+version = "0.1.591"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

pyk/src/pyk/kore/rpc.py

@@ -1163,8 +1163,17 @@ def _get_host_and_port(pid: int) -> tuple[str, int]:
         return conn.laddr
 
 
-class BoosterServerArgs(KoreServerArgs):
+class FallbackReason(Enum):
+    BRANCHING = 'Branching'
+    STUCK = 'Stuck'
+    ABORTED = 'Aborted'
+
+
+class BoosterServerArgs(KoreServerArgs, total=False):
     llvm_kompiled_dir: Required[str | Path]
+    fallback_on: Iterable[str | FallbackReason] | None
+    interim_simplification: int | None
+    no_post_exec_simplify: bool | None
 
 
 class BoosterServer(KoreServer):
@@ -1173,6 +1182,10 @@ class BoosterServer(KoreServer):
     _llvm_definition: Path
     _llvm_dt: Path
 
+    _fallback_on: list[FallbackReason] | None
+    _interim_simplification: int | None
+    _no_post_exec_simplify: bool
+
     def __init__(self, args: BoosterServerArgs):
         self._llvm_kompiled_dir = Path(args['llvm_kompiled_dir'])
 
@@ -1189,6 +1202,14 @@ def __init__(self, args: BoosterServerArgs):
         self._llvm_definition = self._llvm_kompiled_dir / 'definition.kore'
         self._llvm_dt = self._llvm_kompiled_dir / 'dt'
 
+        if fallback_on := args.get('fallback_on'):
+            self._fallback_on = [FallbackReason(reason) for reason in fallback_on]
+        else:
+            self._fallback_on = None
+
+        self._interim_simplification = args.get('interim_simplification')
+        self._no_post_exec_simplify = bool(args.get('no_post_exec_simplify'))
+
         if not args.get('command'):
             args['command'] = 'kore-rpc-booster'
 
@@ -1200,9 +1221,21 @@ def _validate(self) -> None:
         check_file_path(self._llvm_definition)
         check_dir_path(self._llvm_dt)
 
+        if self._fallback_on is not None and not self._fallback_on:
+            raise ValueError("'fallback_on' must not be empty")
+
+        if self._interim_simplification and self._interim_simplification < 0:
+            raise ValueError(f"'interim_simplification' must not be negative, got: {self._interim_simplification}")
+
     def _extra_args(self) -> list[str]:
         res = super()._extra_args()
         res += ['--llvm-backend-library', str(self._dylib)]
+        if self._fallback_on is not None:
+            res += ['--fallback-on', ','.join(reason.value for reason in self._fallback_on)]
+        if self._interim_simplification is not None:
+            res += ['--interim-simplification', str(self._interim_simplification)]
+        if self._no_post_exec_simplify:
+            res += ['--no-post-exec-simplify']
         return res
 
     def _populate_bug_report(self, bug_report: BugReport) -> None:
@@ -1217,7 +1250,6 @@ def kore_server(
     definition_dir: str | Path,
     module_name: str,
     *,
-    llvm_definition_dir: Path | None = None,
     port: int | None = None,
     command: str | Iterable[str] | None = None,
     smt_timeout: int | None = None,
@@ -1226,6 +1258,12 @@ def kore_server(
     log_axioms_file: Path | None = None,
     haskell_log_format: KoreExecLogFormat | None = None,
     haskell_log_entries: Iterable[str] | None = None,
+    # booster
+    llvm_definition_dir: Path | None = None,
+    fallback_on: Iterable[str | FallbackReason] | None,
+    interim_simplification: int | None,
+    no_post_exec_simplify: bool | None,
+    # ---
     bug_report: BugReport | None = None,
 ) -> KoreServer:
     kore_args: KoreServerArgs = {
@@ -1242,6 +1280,12 @@ def kore_server(
         'bug_report': bug_report,
     }
     if llvm_definition_dir:
-        booster_args: BoosterServerArgs = {'llvm_kompiled_dir': llvm_definition_dir, **kore_args}
+        booster_args: BoosterServerArgs = {
+            'llvm_kompiled_dir': llvm_definition_dir,
+            'fallback_on': fallback_on,
+            'interim_simplification': interim_simplification,
+            'no_post_exec_simplify': no_post_exec_simplify,
+            **kore_args,
+        }
         return BoosterServer(booster_args)
     return KoreServer(kore_args)

pyk/src/tests/integration/kore/test_kore_client.py

@@ -1,6 +1,7 @@
 from __future__ import annotations
 
 from dataclasses import asdict
+from itertools import count
 from string import Template
 from typing import TYPE_CHECKING
 
@@ -9,6 +10,7 @@
 from pyk.kore.parser import KoreParser
 from pyk.kore.prelude import BOOL, INT, TRUE, and_bool, eq_int, gt_int, int_dv, le_int
 from pyk.kore.rpc import (
+    BoosterServer,
     BranchingResult,
     CutPointResult,
     DepthBoundResult,
@@ -30,10 +32,12 @@
 
 if TYPE_CHECKING:
     from collections.abc import Mapping
+    from pathlib import Path
     from typing import Any, Final
 
-    from pyk.kore.rpc import ExecuteResult, GetModelResult, KoreClient
+    from pyk.kore.rpc import BoosterServerArgs, ExecuteResult, GetModelResult, KoreClient
     from pyk.kore.syntax import Pattern
+    from pyk.testing import Kompiler
 
 int_top = Top(INT)
 int_bottom = Bottom(INT)
@@ -372,3 +376,36 @@ def test_get_model_with_smt(
 
         # Then
         assert actual == expected
+
+
+START_BOOSTER_SERVER_TEST_DATA: Final[tuple[dict[str, Any], ...]] = (
+    {},
+    {'fallback_on': ['Aborted', 'Stuck']},
+    {'interim_simplification': 3},
+    {'no_post_exec_simpify': True},
+)
+
+
+@pytest.fixture(scope='module')
+def imp_dir(kompile: Kompiler) -> Path:
+    return kompile(K_FILES / 'imp.k', backend='haskell')
+
+
+@pytest.fixture(scope='module')
+def imp_llvm_dir(kompile: Kompiler) -> Path:
+    return kompile(K_FILES / 'imp.k', backend='llvm', llvm_kompile_type='c')
+
+
+@pytest.mark.parametrize('args', START_BOOSTER_SERVER_TEST_DATA, ids=count())
+def test_start_booster_server(imp_dir: Path, imp_llvm_dir: Path, args: dict) -> None:
+    # Given
+    booster_args: BoosterServerArgs = {
+        'kompiled_dir': imp_dir,
+        'llvm_kompiled_dir': imp_llvm_dir,
+        'module_name': 'IMP',
+        **args,
+    }
+
+    # When
+    with BoosterServer(booster_args):
+        pass