Merge branch 'master' into kcfg-key

Author: François Guyot

.github/workflows/test-pr.yml

@@ -58,16 +58,28 @@ jobs:
   profile:
     needs: code-quality-checks
     name: 'Profiling'
-    runs-on: ubuntu-latest
+    runs-on: [self-hosted, linux, normal-ephemeral]
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
+      - name: 'Install Python'
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.10'
       - name: 'Install Poetry'
         uses: Gr1N/setup-poetry@v8
+      - name: 'Install K'
+        run: |
+          K_VERSION=$(cat deps/k_release)
+          DEB_PACKAGE_NAME=kframework_${K_VERSION}_amd64_ubuntu_jammy.deb
+          wget https://github.com/runtimeverification/k/releases/download/v${K_VERSION}/${DEB_PACKAGE_NAME}
+          sudo apt-get update
+          sudo apt-get -y install ./${DEB_PACKAGE_NAME}
+          kompile --version
       - name: 'Run profiling'
         run: |
           make profile
-          find /tmp/pytest-of-${USER}/pytest-current/ -type f | sort | xargs tail -n +1
+          find /tmp/pytest-of-${USER}/pytest-current/ -type f -name '*.prof' | sort | xargs tail -n +1
 
   integration-tests:
     needs: code-quality-checks

deps/k_release

@@ -1 +1 @@
-5.6.114
+5.6.125

package/version

@@ -1 +1 @@
-0.1.320
+0.1.330

src/pyk/__init__.py

@@ -6,4 +6,4 @@
     from typing import Final
 
 
-K_VERSION: Final = '5.6.114'
+K_VERSION: Final = '5.6.125'

src/pyk/__main__.py

@@ -8,7 +8,8 @@
 
 from graphviz import Digraph
 
-from .cli_utils import dir_path
+from .cli.args import KCLIArgs
+from .cli.utils import LOG_FORMAT, dir_path, loglevel
 from .coverage import get_rule_by_id, strip_coverage_logger
 from .cterm import split_config_and_constraints
 from .kast.inner import KInner
@@ -27,7 +28,6 @@
     from typing import Any, Final
 
 
-_LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
 _LOGGER: Final = logging.getLogger(__name__)
 
 
@@ -40,12 +40,7 @@ def main() -> None:
     cli_parser = create_argument_parser()
     args = cli_parser.parse_args()
 
-    if not args.verbose:
-        logging.basicConfig(level=logging.WARNING, format=_LOG_FORMAT)
-    elif args.verbose == 1:
-        logging.basicConfig(level=logging.INFO, format=_LOG_FORMAT)
-    elif args.verbose > 1:
-        logging.basicConfig(level=logging.DEBUG, format=_LOG_FORMAT)
+    logging.basicConfig(level=loglevel(args), format=LOG_FORMAT)
 
     executor_name = 'exec_' + args.command.lower().replace('-', '_')
     if executor_name not in globals():
@@ -77,7 +72,7 @@ def exec_print(args: Namespace) -> None:
                     minimized = minimize_term(disjunct, abstract_labels=abstract_labels, keep_cells=keep_cells)
                     config, constraint = split_config_and_constraints(minimized)
                 except ValueError as err:
-                    raise ValueError('The minified term does not contain a config cell.') from err
+                    raise ValueError('The minimized term does not contain a config cell.') from err
 
                 if not is_top(constraint):
                     minimized_disjuncts.append(mlAnd([config, constraint], sort=GENERATED_TOP_CELL))
@@ -139,10 +134,7 @@ def exec_json_to_kore(args: dict[str, Any]) -> None:
 
 
 def create_argument_parser() -> ArgumentParser:
-    logging_args = ArgumentParser(add_help=False)
-    logging_args.add_argument(
-        '-v', '--verbose', action='count', help='Verbosity level, repeat for more verbosity (up to two times).'
-    )
+    k_cli_args = KCLIArgs()
 
     definition_args = ArgumentParser(add_help=False)
     definition_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
@@ -151,30 +143,21 @@ def create_argument_parser() -> ArgumentParser:
     pyk_args_command = pyk_args.add_subparsers(dest='command', required=True)
 
     print_args = pyk_args_command.add_parser(
-        'print', help='Pretty print a term.', parents=[logging_args, definition_args]
+        'print',
+        help='Pretty print a term.',
+        parents=[k_cli_args.logging_args, definition_args, k_cli_args.display_args],
     )
     print_args.add_argument('term', type=FileType('r'), help='Input term (in JSON).')
-    print_args.add_argument(
-        '--minimize',
-        dest='minimize',
-        default=True,
-        action='store_true',
-        help='Minimize the JSON configuration before printing.',
-    )
-    print_args.add_argument(
-        '--no-minimize',
-        dest='minimize',
-        action='store_false',
-        help='Do not minimize the JSON configuration before printing.',
-    )
     print_args.add_argument('--omit-labels', default='', nargs='?', help='List of labels to omit from output.')
     print_args.add_argument(
         '--keep-cells', default='', nargs='?', help='List of cells with primitive values to keep in output.'
     )
     print_args.add_argument('--output-file', type=FileType('w'), default='-')
 
     prove_args = pyk_args_command.add_parser(
-        'prove', help='Prove an input specification (using kprovex).', parents=[logging_args, definition_args]
+        'prove',
+        help='Prove an input specification (using kprovex).',
+        parents=[k_cli_args.logging_args, definition_args],
     )
     prove_args.add_argument('main_file', type=str, help='Main file used for kompilation.')
     prove_args.add_argument('spec_file', type=str, help='File with the specification module.')
@@ -183,18 +166,22 @@ def create_argument_parser() -> ArgumentParser:
     prove_args.add_argument('kArgs', nargs='*', help='Arguments to pass through to K invocation.')
 
     pyk_args_command.add_parser(
-        'graph-imports', help='Graph the imports of a given definition.', parents=[logging_args, definition_args]
+        'graph-imports',
+        help='Graph the imports of a given definition.',
+        parents=[k_cli_args.logging_args, definition_args],
     )
 
     coverage_args = pyk_args_command.add_parser(
-        'coverage', help='Convert coverage file to human readable log.', parents=[logging_args, definition_args]
+        'coverage',
+        help='Convert coverage file to human readable log.',
+        parents=[k_cli_args.logging_args, definition_args],
     )
     coverage_args.add_argument('coverage_file', type=FileType('r'), help='Coverage file to build log for.')
     coverage_args.add_argument('-o', '--output', type=FileType('w'), default='-')
 
-    pyk_args_command.add_parser('kore-to-json', help='Convert textual KORE to JSON', parents=[logging_args])
+    pyk_args_command.add_parser('kore-to-json', help='Convert textual KORE to JSON', parents=[k_cli_args.logging_args])
 
-    pyk_args_command.add_parser('json-to-kore', help='Convert JSON to textual KORE', parents=[logging_args])
+    pyk_args_command.add_parser('json-to-kore', help='Convert JSON to textual KORE', parents=[k_cli_args.logging_args])
 
     return pyk_args
 

src/pyk/cli/args.py

@@ -0,0 +1,127 @@
+from __future__ import annotations
+
+from argparse import ArgumentParser
+from functools import cached_property
+from typing import TYPE_CHECKING
+
+from ..utils import ensure_dir_path
+from .utils import dir_path, file_path
+
+if TYPE_CHECKING:
+    from typing import TypeVar
+
+    T = TypeVar('T')
+
+
+class KCLIArgs:
+    @cached_property
+    def logging_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument('--verbose', '-v', default=False, action='store_true', help='Verbose output.')
+        args.add_argument('--debug', default=False, action='store_true', help='Debug output.')
+        return args
+
+    @cached_property
+    def parallel_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument('--workers', '-j', default=1, type=int, help='Number of processes to run in parallel.')
+        return args
+
+    @cached_property
+    def kompile_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument(
+            '--emit-json',
+            dest='emit_json',
+            default=True,
+            action='store_true',
+            help='Emit JSON definition after compilation.',
+        )
+        args.add_argument(
+            '--no-emit-json', dest='emit_json', action='store_false', help='Do not JSON definition after compilation.'
+        )
+        args.add_argument(
+            '-ccopt',
+            dest='ccopts',
+            default=[],
+            action='append',
+            help='Additional arguments to pass to llvm-kompile.',
+        )
+        args.add_argument(
+            '--no-llvm-kompile',
+            dest='llvm_kompile',
+            default=True,
+            action='store_false',
+            help='Do not run llvm-kompile process.',
+        )
+        args.add_argument(
+            '--with-llvm-library',
+            dest='llvm_library',
+            default=False,
+            action='store_true',
+            help='Make kompile generate a dynamic llvm library.',
+        )
+        args.add_argument(
+            '--enable-llvm-debug',
+            dest='enable_llvm_debug',
+            default=False,
+            action='store_true',
+            help='Make kompile generate debug symbols for llvm.',
+        )
+        args.add_argument(
+            '--read-only-kompiled-directory',
+            dest='read_only',
+            default=False,
+            action='store_true',
+            help='Generated a kompiled directory that K will not attempt to write to afterwards.',
+        )
+        args.add_argument('-O0', dest='o0', default=False, action='store_true', help='Optimization level 0.')
+        args.add_argument('-O1', dest='o1', default=False, action='store_true', help='Optimization level 1.')
+        args.add_argument('-O2', dest='o2', default=False, action='store_true', help='Optimization level 2.')
+        args.add_argument('-O3', dest='o3', default=False, action='store_true', help='Optimization level 3.')
+        return args
+
+    @cached_property
+    def display_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument('--minimize', dest='minimize', default=True, action='store_true', help='Minimize output.')
+        args.add_argument('--no-minimize', dest='minimize', action='store_false', help='Do not minimize output.')
+        return args
+
+    @cached_property
+    def definition_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument(
+            '-I', type=str, dest='includes', default=[], action='append', help='Directories to lookup K definitions in.'
+        )
+        args.add_argument('--main-module', default=None, type=str, help='Name of the main module.')
+        args.add_argument('--syntax-module', default=None, type=str, help='Name of the syntax module.')
+        args.add_argument('--spec-module', default=None, type=str, help='Name of the spec module.')
+        args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.')
+        args.add_argument(
+            '--md-selector',
+            type=str,
+            help='Code selector expression to use when reading markdown.',
+        )
+        return args
+
+    @cached_property
+    def spec_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument('spec_file', type=file_path, help='Path to spec file.')
+        args.add_argument('--save-directory', type=ensure_dir_path, help='Path to where CFGs are stored.')
+        args.add_argument(
+            '--claim',
+            type=str,
+            dest='claim_labels',
+            action='append',
+            help='Only prove listed claims, MODULE_NAME.claim-id',
+        )
+        args.add_argument(
+            '--exclude-claim',
+            type=str,
+            dest='exclude_claim_labels',
+            action='append',
+            help='Skip listed claims, MODULE_NAME.claim-id',
+        )
+        return args

src/pyk/cli/utils.py

@@ -0,0 +1,75 @@
+from __future__ import annotations
+
+import logging
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+from ..utils import check_dir_path, check_file_path, check_relative_path
+
+if TYPE_CHECKING:
+    from argparse import Namespace
+    from collections.abc import Callable
+    from typing import Final, TypeVar
+
+    from ..kcfg.kcfg import NodeIdLike
+
+    T1 = TypeVar('T1')
+    T2 = TypeVar('T2')
+
+LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
+
+
+def loglevel(args: Namespace) -> int:
+    if args.debug:
+        return logging.DEBUG
+
+    if args.verbose:
+        return logging.INFO
+
+    return logging.WARNING
+
+
+def dir_path(s: str | Path) -> Path:
+    path = Path(s)
+    check_dir_path(path)
+    return path
+
+
+def file_path(s: str) -> Path:
+    path = Path(s)
+    check_file_path(path)
+    return path
+
+
+def relative_path(path: str | Path) -> Path:
+    path = Path(path)
+    check_relative_path(path)
+    return path
+
+
+def list_of(elem_type: Callable[[str], T1], delim: str = ';') -> Callable[[str], list[T1]]:
+    def parse(s: str) -> list[T1]:
+        return [elem_type(elem) for elem in s.split(delim)]
+
+    return parse
+
+
+def node_id_like(s: str) -> NodeIdLike:
+    try:
+        return int(s)
+    except ValueError:
+        return s
+
+
+def arg_pair_of(
+    fst_type: Callable[[str], T1], snd_type: Callable[[str], T2], delim: str = ','
+) -> Callable[[str], tuple[T1, T2]]:
+    def parse(s: str) -> tuple[T1, T2]:
+        elems = s.split(delim)
+        length = len(elems)
+        if length != 2:
+            raise ValueError(f'Expected 2 elements, found {length}')
+
+        return fst_type(elems[0]), snd_type(elems[1])
+
+    return parse