Enable booster-only simplification via RPC flag, JSON logging on RPC, and standardize log forma

pyk/src/pyk/cli/utils.py

@@ -16,7 +16,7 @@
     T1 = TypeVar('T1')
     T2 = TypeVar('T2')
 
-LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
+LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s [%(process)d] - %(message)s'
 
 
 def loglevel(args: Namespace) -> int:

pyk/src/pyk/cterm/symbolic.py

@@ -73,6 +73,7 @@ class CTermSymbolic:
     _definition: KDefinition
     _log_succ_rewrites: bool
     _log_fail_rewrites: bool
+    _booster_only_simplify: bool
 
     def __init__(
         self,
@@ -81,11 +82,13 @@ def __init__(
         *,
         log_succ_rewrites: bool = True,
         log_fail_rewrites: bool = False,
+        booster_only_simplify: bool = False,
     ):
         self._kore_client = kore_client
         self._definition = definition
         self._log_succ_rewrites = log_succ_rewrites
         self._log_fail_rewrites = log_fail_rewrites
+        self._booster_only_simplify = booster_only_simplify
 
     def kast_to_kore(self, kinner: KInner) -> Pattern:
         return kast_to_kore(self._definition, kinner, sort=GENERATED_TOP_CELL)
@@ -100,6 +103,7 @@ def execute(
         cut_point_rules: Iterable[str] | None = None,
         terminal_rules: Iterable[str] | None = None,
         module_name: str | None = None,
+        booster_only_simplify: bool | None = None,
     ) -> CTermExecute:
 
         _LOGGER.debug(f'Executing: {cterm}')
@@ -113,6 +117,9 @@ def execute(
                 module_name=module_name,
                 log_successful_rewrites=self._log_succ_rewrites,
                 log_failed_rewrites=self._log_succ_rewrites and self._log_fail_rewrites,
+                booster_only_simplify=(
+                    booster_only_simplify if booster_only_simplify is not None else self._booster_only_simplify
+                ),
             )
         except SmtSolverError as err:
             raise self._smt_solver_error(err) from err
@@ -143,16 +150,28 @@ def execute(
             logs=response.logs,
         )
 
-    def simplify(self, cterm: CTerm, module_name: str | None = None) -> tuple[CTerm, tuple[LogEntry, ...]]:
+    def simplify(
+        self, cterm: CTerm, module_name: str | None = None, booster_only_simplify: bool | None = None
+    ) -> tuple[CTerm, tuple[LogEntry, ...]]:
         _LOGGER.debug(f'Simplifying: {cterm}')
-        kast_simplified, logs = self.kast_simplify(cterm.kast, module_name=module_name)
+        kast_simplified, logs = self.kast_simplify(
+            cterm.kast, module_name=module_name, booster_only_simplify=booster_only_simplify
+        )
         return CTerm.from_kast(kast_simplified), logs
 
-    def kast_simplify(self, kast: KInner, module_name: str | None = None) -> tuple[KInner, tuple[LogEntry, ...]]:
+    def kast_simplify(
+        self, kast: KInner, module_name: str | None = None, booster_only_simplify: bool | None = None
+    ) -> tuple[KInner, tuple[LogEntry, ...]]:
         _LOGGER.debug(f'Simplifying: {kast}')
         kore = self.kast_to_kore(kast)
         try:
-            kore_simplified, logs = self._kore_client.simplify(kore, module_name=module_name)
+            kore_simplified, logs = self._kore_client.simplify(
+                kore,
+                module_name=module_name,
+                booster_only_simplify=(
+                    booster_only_simplify if booster_only_simplify is not None else self._booster_only_simplify
+                ),
+            )
         except SmtSolverError as err:
             raise self._smt_solver_error(err) from err
 
@@ -194,6 +213,7 @@ def implies(
         failure_reason: bool = False,
         module_name: str | None = None,
         assume_defined: bool = False,
+        booster_only_simplify: bool | None = None,
     ) -> CTermImplies:
         _LOGGER.debug(f'Checking implication: {antecedent} #Implies {consequent}')
         _consequent = consequent.kast
@@ -211,7 +231,13 @@ def implies(
         consequent_kore = self.kast_to_kore(_consequent)
         try:
             result = self._kore_client.implies(
-                antecedent_kore, consequent_kore, module_name=module_name, assume_defined=assume_defined
+                antecedent_kore,
+                consequent_kore,
+                module_name=module_name,
+                assume_defined=assume_defined,
+                booster_only_simplify=(
+                    booster_only_simplify if booster_only_simplify is not None else self._booster_only_simplify
+                ),
             )
         except SmtSolverError as err:
             raise self._smt_solver_error(err) from err
@@ -231,6 +257,7 @@ def implies(
                     failure_reason=False,
                     module_name=module_name,
                     assume_defined=assume_defined,
+                    booster_only_simplify=booster_only_simplify,
                 )
                 config_match = _config_match.csubst
                 if config_match is None:
@@ -269,11 +296,17 @@ def implies(
         csubst = CSubst.from_pred(ml_subst_pred)
         return CTermImplies(csubst, (), None, result.logs)
 
-    def assume_defined(self, cterm: CTerm, module_name: str | None = None) -> CTerm:
+    def assume_defined(
+        self, cterm: CTerm, module_name: str | None = None, booster_only_simplify: bool = False
+    ) -> CTerm:
         _LOGGER.debug(f'Computing definedness condition for: {cterm}')
-        cterm_simplified, logs = self.simplify(cterm, module_name=module_name)
+        cterm_simplified, logs = self.simplify(
+            cterm, module_name=module_name, booster_only_simplify=booster_only_simplify
+        )
         kast = KApply(KLabel('#Ceil', [GENERATED_TOP_CELL, GENERATED_TOP_CELL]), [cterm_simplified.config])
-        kast_simplified, logs = self.kast_simplify(kast, module_name=module_name)
+        kast_simplified, logs = self.kast_simplify(
+            kast, module_name=module_name, booster_only_simplify=booster_only_simplify
+        )
         _LOGGER.debug(f'Definedness condition computed: {kast_simplified}')
         return cterm.add_constraint(kast_simplified)
 
@@ -305,6 +338,7 @@ def cterm_symbolic(
     log_axioms_file: Path | None = None,
     log_succ_rewrites: bool = True,
     log_fail_rewrites: bool = False,
+    booster_only_simplify: bool = False,
     start_server: bool = True,
     fallback_on: Iterable[FallbackReason] | None = None,
     interim_simplification: int | None = None,
@@ -333,7 +367,11 @@ def cterm_symbolic(
         ) as server:
             with KoreClient('localhost', server.port, bug_report=bug_report, bug_report_id=id) as client:
                 yield CTermSymbolic(
-                    client, definition, log_succ_rewrites=log_succ_rewrites, log_fail_rewrites=log_fail_rewrites
+                    client,
+                    definition,
+                    log_succ_rewrites=log_succ_rewrites,
+                    log_fail_rewrites=log_fail_rewrites,
+                    booster_only_simplify=booster_only_simplify,
                 )
     else:
         if port is None:

pyk/src/pyk/kdist/utils.py

@@ -13,7 +13,7 @@
     from typing import Any, Final
 
 
-LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
+LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s [%(process)d] - %(message)s'
 
 
 def package_path(obj: Any) -> Path:

pyk/src/pyk/kore/rpc.py

@@ -44,6 +44,7 @@
 class KoreExecLogFormat(Enum):
     STANDARD = 'standard'
     ONELINE = 'oneline'
+    JSON = 'json'
 
 
 @final
@@ -119,7 +120,8 @@ def _create_connection(host: str, port: int, timeout: int | None) -> socket.sock
             try:
                 sock = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
                 sock.connect((host, port))
-                _LOGGER.info(f'Connected to host: {host}:{port}')
+                local_port = sock.getsockname()[1]
+                _LOGGER.info(f'Connected to host: {host}:{port} (local port: {local_port})')
                 return sock
             except ConnectionRefusedError:
                 sock.close()
@@ -965,6 +967,7 @@ def execute(
         module_name: str | None = None,
         log_successful_rewrites: bool | None = None,
         log_failed_rewrites: bool | None = None,
+        booster_only_simplify: bool | None = None,
     ) -> ExecuteResult:
         params = filter_none(
             {
@@ -978,6 +981,7 @@ def execute(
                 'state': self._state(pattern),
                 'log-successful-rewrites': log_successful_rewrites,
                 'log-failed-rewrites': log_failed_rewrites,
+                'booster-only': booster_only_simplify,
             }
         )
 
@@ -991,13 +995,15 @@ def implies(
         *,
         module_name: str | None = None,
         assume_defined: bool = False,
+        booster_only_simplify: bool | None = None,
     ) -> ImpliesResult:
         params = filter_none(
             {
                 'antecedent': self._state(antecedent),
                 'consequent': self._state(consequent),
                 'module': module_name,
                 'assume-defined': assume_defined,
+                'booster-only': booster_only_simplify,
             }
         )
 
@@ -1009,11 +1015,13 @@ def simplify(
         pattern: Pattern,
         *,
         module_name: str | None = None,
+        booster_only_simplify: bool | None = None,
     ) -> tuple[Pattern, tuple[LogEntry, ...]]:
         params = filter_none(
             {
                 'state': self._state(pattern),
                 'module': module_name,
+                'booster-only': booster_only_simplify,
             }
         )
 

pyk/src/pyk/kore_exec_covr/__main__.py

@@ -16,7 +16,7 @@
     from typing import Final
 
 
-_LOG_FORMAT: Final = '%(levelname)s %(name)s - %(message)s'
+_LOG_FORMAT: Final = '%(levelname)s %(name)s [%(process)d] - %(message)s'
 
 
 def do_analyze(definition_dir: Path, input_file: Path) -> None:

pyk/src/pyk/kore_exec_covr/kore_exec_covr.py

@@ -15,7 +15,7 @@
     from ..kast.outer import KDefinition, KRule
 
 
-_LOG_FORMAT: Final = '%(levelname)s %(name)s - %(message)s'
+_LOG_FORMAT: Final = '%(levelname)s %(name)s [%(process)d] - %(message)s'
 _LOGGER: Final = logging.getLogger(__name__)
 
 _HASKELL_LOG_ENTRY_REGEXP: Final = re.compile(r'(kore-exec|kore-rpc): \[\d*\] Debug \(([a-zA-Z]*)\):(.*)')

pyk/src/pyk/ktool/kprint.py

@@ -219,6 +219,22 @@ def _temp_file(self, prefix: str | None = None, suffix: str | None = None) -> It
     def definition(self) -> KDefinition:
         return read_kast_definition(self.definition_dir / 'compiled.json')
 
+    @cached_property
+    def all_rules(self) -> dict[str, str]:
+        """Map from 12-char rule hash prefix to source location (file:line:col).
+
+        Parsed from allRules.txt in the kompiled definition directory.
+        Keyed by the first 12 hex characters of each rule's SHA-256 hash.
+        """
+        rules: dict[str, str] = {}
+        for line in (self.definition_dir / 'allRules.txt').read_text().splitlines():
+            line = line.strip()
+            if not line:
+                continue
+            full_hash, _, location = line.partition(' ')
+            rules[full_hash[:12]] = location
+        return rules
+
     @property
     def definition_hash(self) -> str:
         return self.definition.hash
@@ -233,7 +249,9 @@ def parse_token(self, ktoken: KToken, *, as_rule: bool = False) -> KInner:
         )
         return KInner.from_dict(kast_term(json.loads(proc_res.stdout)))
 
-    def kore_to_pretty(self, pattern: Pattern) -> str:
+    def kore_to_pretty(self, pattern: Pattern, *, pyk_print: bool = False) -> str:
+        if pyk_print:
+            return self.pretty_print(self.kore_to_kast(pattern))
         proc_res = self._expression_kast(
             pattern.text,
             input=KAstInput.KORE,