Merge remote-tracking branch 'origin/master' into georgy/prettier-unk…

…nown

deps/k_release

@@ -1 +1 @@
-6.1.31
+6.1.52

package/version

@@ -1 +1 @@
-0.1.519
+0.1.543

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.519"
+version = "0.1.543"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
@@ -20,6 +20,7 @@ psutil = "5.9.5"
 pybind11 = "^2.10.3"
 textual = "^0.27.0"
 tomli = "^2.0.1"
+xdg-base-dirs = "^6.0.1"
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"
@@ -43,6 +44,7 @@ types-psutil = "^5.9.5.10"
 pyk = "pyk.__main__:main"
 pyk-covr = "pyk.kcovr:main"
 kbuild = "pyk.kbuild.__main__:main"
+kdist = "pyk.kdist.__main__:main"
 krepl = "pyk.krepl.__main__:main"
 kore-exec-covr = "pyk.kore_exec_covr.__main__:main"
 

src/pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-K_VERSION: Final = '6.1.31'
+K_VERSION: Final = '6.1.52'

src/pyk/kcfg/explore.py

@@ -3,7 +3,7 @@
 import logging
 from abc import ABC
 from dataclasses import dataclass, field
-from typing import TYPE_CHECKING, final
+from typing import TYPE_CHECKING, NamedTuple, final
 
 from ..cterm import CSubst, CTerm
 from ..kast.inner import KApply, KLabel, KRewrite, KVariable, Subst
@@ -47,6 +47,15 @@
 _LOGGER: Final = logging.getLogger(__name__)
 
 
+class CTermExecute(NamedTuple):
+    state: CTerm
+    unknown_predicate: KInner | None
+    next_states: tuple[CTerm, ...]
+    depth: int
+    vacuous: bool
+    logs: tuple[LogEntry, ...]
+
+
 class KCFGExplore:
     kprint: KPrint
     _kore_client: KoreClient
@@ -77,40 +86,42 @@ def cterm_execute(
         cut_point_rules: Iterable[str] | None = None,
         terminal_rules: Iterable[str] | None = None,
         module_name: str | None = None,
-    ) -> tuple[KInner | None, bool, int, CTerm, list[CTerm], tuple[LogEntry, ...]]:
+    ) -> CTermExecute:
         _LOGGER.debug(f'Executing: {cterm}')
         kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL)
-        er = self._kore_client.execute(
+        response = self._kore_client.execute(
             kore,
             max_depth=depth,
             cut_point_rules=cut_point_rules,
             terminal_rules=terminal_rules,
             module_name=module_name,
-            log_successful_rewrites=self._trace_rewrites if self._trace_rewrites else None,
-            log_failed_rewrites=self._trace_rewrites if self._trace_rewrites else None,
-            log_successful_simplifications=self._trace_rewrites if self._trace_rewrites else None,
-            log_failed_simplifications=self._trace_rewrites if self._trace_rewrites else None,
+            log_successful_rewrites=self._trace_rewrites,
+            log_failed_rewrites=self._trace_rewrites,
+            log_successful_simplifications=self._trace_rewrites,
+            log_failed_simplifications=self._trace_rewrites,
         )
 
-        _is_vacuous = er.reason is StopReason.VACUOUS
-        depth = er.depth
-        next_state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore))
-        _next_states = er.next_states if er.next_states is not None else []
-        next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in _next_states]
-        next_states = [cterm for cterm in next_states if not cterm.is_bottom]
-        if len(next_states) == 1 and len(next_states) < len(_next_states):
-            return None, _is_vacuous, depth + 1, next_states[0], [], er.logs
-        elif len(next_states) == 1:
-            if er.reason == StopReason.CUT_POINT_RULE:
-                return None, _is_vacuous, depth, next_state, next_states, er.logs
-            else:
-                next_states = []
         unknown_predicate = None
-        if isinstance(er, AbortedResult):
+        if isinstance(response, AbortedResult):
             unknown_predicate = (
-                self.kprint.kore_to_kast(er.unknown_predicate) if er.unknown_predicate is not None else None
+                self.kprint.kore_to_kast(response.unknown_predicate) if response.unknown_predicate is not None else None
             )
-        return unknown_predicate, _is_vacuous, depth, next_state, next_states, er.logs
+
+        state = CTerm.from_kast(self.kprint.kore_to_kast(response.state.kore))
+        resp_next_states = response.next_states or ()
+        next_states = tuple(CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in resp_next_states)
+
+        assert all(not cterm.is_bottom for cterm in next_states)
+        assert len(next_states) != 1 or response.reason is StopReason.CUT_POINT_RULE
+
+        return CTermExecute(
+            state=state,
+            unknown_predicate=unknown_predicate,
+            next_states=next_states,
+            depth=response.depth,
+            vacuous=response.reason is StopReason.VACUOUS,
+            logs=response.logs,
+        )
 
     def cterm_simplify(self, cterm: CTerm) -> tuple[KInner | None, CTerm, tuple[LogEntry, ...]]:
         _LOGGER.debug(f'Simplifying: {cterm}')
@@ -319,16 +330,14 @@ def step(
         if len(successors) != 0 and type(successors[0]) is KCFG.Split:
             raise ValueError(f'Cannot take step from split node {self.id}: {shorten_hashes(node.id)}')
         _LOGGER.info(f'Taking {depth} steps from node {self.id}: {shorten_hashes(node.id)}')
-        _, _, actual_depth, cterm, next_cterms, next_node_logs = self.cterm_execute(
-            node.cterm, depth=depth, module_name=module_name
-        )
-        if actual_depth != depth:
-            raise ValueError(f'Unable to take {depth} steps from node, got {actual_depth} steps {self.id}: {node.id}')
-        if len(next_cterms) > 0:
+        exec_res = self.cterm_execute(node.cterm, depth=depth, module_name=module_name)
+        if exec_res.depth != depth:
+            raise ValueError(f'Unable to take {depth} steps from node, got {exec_res.depth} steps {self.id}: {node.id}')
+        if len(exec_res.next_states) > 0:
             raise ValueError(f'Found branch within {depth} steps {self.id}: {node.id}')
-        new_node = cfg.create_node(cterm)
+        new_node = cfg.create_node(exec_res.state)
         _LOGGER.info(f'Found new node at depth {depth} {self.id}: {shorten_hashes((node.id, new_node.id))}')
-        logs[new_node.id] = next_node_logs
+        logs[new_node.id] = exec_res.logs
         out_edges = cfg.edges(source_id=node.id)
         if len(out_edges) == 0:
             cfg.create_edge(node.id, new_node.id, depth=depth)
@@ -424,7 +433,7 @@ def extend_cterm(
         if len(branches) > 1:
             return Branch(branches, heuristic=True)
 
-        unknown_predicate, _is_vacuous, depth, cterm, next_cterms, next_node_logs = self.cterm_execute(
+        cterm, unknown_predicate, next_cterms, depth, vacuous, next_node_logs = self.cterm_execute(
             _cterm,
             depth=execute_depth,
             cut_point_rules=cut_point_rules,
@@ -438,7 +447,7 @@ def extend_cterm(
 
         # Stuck, Vacuous or Undecided
         if not next_cterms:
-            if _is_vacuous:
+            if vacuous:
                 return Vacuous()
             if unknown_predicate is not None:
                 return Undecided(unknown_predicate)

src/pyk/kdist/__init__.py

@@ -0,0 +1,2 @@
+from ._cache import target_ids
+from ._kdist import KDIST_DIR, KDist, kdist

src/pyk/kdist/__main__.py

@@ -0,0 +1,146 @@
+from __future__ import annotations
+
+import fnmatch
+import logging
+from argparse import ArgumentParser
+from typing import TYPE_CHECKING
+
+from pyk.cli.args import KCLIArgs
+from pyk.cli.utils import loglevel
+
+from ..kdist import kdist, target_ids
+
+if TYPE_CHECKING:
+    from argparse import Namespace
+    from typing import Final
+
+
+_LOGGER: Final = logging.getLogger(__name__)
+_LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
+
+
+def main() -> None:
+    args = _parse_arguments()
+
+    logging.basicConfig(level=loglevel(args), format=_LOG_FORMAT)
+
+    if args.command == 'build':
+        _exec_build(**vars(args))
+
+    elif args.command == 'clean':
+        _exec_clean(args.target)
+
+    elif args.command == 'which':
+        _exec_which(args.target)
+
+    elif args.command == 'list':
+        _exec_list()
+
+    else:
+        raise AssertionError()
+
+
+def _exec_build(
+    command: str,
+    targets: list[str],
+    args: list[str],
+    jobs: int,
+    force: bool,
+    verbose: bool,
+    debug: bool,
+) -> None:
+    kdist.build(
+        target_ids=_process_targets(targets),
+        args=_process_args(args),
+        jobs=jobs,
+        force=force,
+        verbose=verbose or debug,
+    )
+
+
+def _process_targets(targets: list[str]) -> list[str]:
+    all_target_fqns = [target_id.full_name for target_id in target_ids()]
+    res = []
+    for pattern in targets:
+        matches = fnmatch.filter(all_target_fqns, pattern)
+        if not matches:
+            raise ValueError(f'No target matches pattern: {pattern!r}')
+        res += matches
+    return res
+
+
+def _process_args(args: list[str]) -> dict[str, str]:
+    res: dict[str, str] = {}
+    for arg in args:
+        segments = arg.split('=')
+        if len(segments) < 2:
+            raise ValueError(f"Expected assignment of the form 'arg=value', got: {arg!r}")
+        key, *values = segments
+        res[key] = '='.join(values)
+    return res
+
+
+def _exec_clean(target: str | None) -> None:
+    res = kdist.clean(target)
+    print(res)
+
+
+def _exec_which(target: str | None) -> None:
+    res = kdist.which(target)
+    print(res)
+
+
+def _exec_list() -> None:
+    targets_by_plugin: dict[str, list[str]] = {}
+    for plugin_name, target_name in target_ids():
+        targets = targets_by_plugin.get(plugin_name, [])
+        targets.append(target_name)
+        targets_by_plugin[plugin_name] = targets
+
+    for plugin_name in targets_by_plugin:
+        print(plugin_name)
+        for target_name in targets_by_plugin[plugin_name]:
+            print(f'* {target_name}')
+
+
+def _parse_arguments() -> Namespace:
+    def add_target_arg(parser: ArgumentParser, help_text: str) -> None:
+        parser.add_argument(
+            'target',
+            metavar='TARGET',
+            nargs='?',
+            help=help_text,
+        )
+
+    k_cli_args = KCLIArgs()
+
+    parser = ArgumentParser(prog='kdist', parents=[k_cli_args.logging_args])
+    command_parser = parser.add_subparsers(dest='command', required=True)
+
+    build_parser = command_parser.add_parser('build', help='build targets')
+    build_parser.add_argument('targets', metavar='TARGET', nargs='*', default='*', help='target to build')
+    build_parser.add_argument(
+        '-a',
+        '--arg',
+        dest='args',
+        metavar='ARG',
+        action='append',
+        default=[],
+        help='build with argument',
+    )
+    build_parser.add_argument('-f', '--force', action='store_true', default=False, help='force build')
+    build_parser.add_argument('-j', '--jobs', metavar='N', type=int, default=1, help='maximal number of build jobs')
+
+    clean_parser = command_parser.add_parser('clean', help='clean targets')
+    add_target_arg(clean_parser, 'target to clean')
+
+    which_parser = command_parser.add_parser('which', help='print target location')
+    add_target_arg(which_parser, 'target to print directory for')
+
+    command_parser.add_parser('list', help='print list of available targets')
+
+    return parser.parse_args()
+
+
+if __name__ == '__main__':
+    main()