Skip to content

Commit 25d3a4a

Browse files
Baltoliovatmangeo2agtreptarv-jenkins
authored
add toml support for pyk options (#4254)
Transfer of: runtimeverification/pyk#1008 --------- Co-authored-by: Tolga Ovatman <[email protected]> Co-authored-by: Tolga Ovatman <[email protected]> Co-authored-by: Georgy Lukyanov <[email protected]> Co-authored-by: gtrepta <[email protected]> Co-authored-by: rv-jenkins <[email protected]> Co-authored-by: devops <[email protected]>
1 parent b896d78 commit 25d3a4a

File tree

6 files changed

+428
-157
lines changed

6 files changed

+428
-157
lines changed

‎pyk/src/pyk/__main__.py

+5-156
Original file line numberDiff line numberDiff line change
@@ -3,17 +3,14 @@
33
import json
44
import logging
55
import sys
6-
from argparse import ArgumentParser, FileType
76
from collections.abc import Iterable
8-
from enum import Enum
97
from pathlib import Path
108
from typing import TYPE_CHECKING
119

1210
from graphviz import Digraph
1311

14-
from .cli.args import KCLIArgs
15-
from .cli.pyk import generate_options
16-
from .cli.utils import LOG_FORMAT, dir_path, loglevel
12+
from .cli.pyk import PrintInput, create_argument_parser, generate_options, parse_toml_args
13+
from .cli.utils import LOG_FORMAT, loglevel
1714
from .coverage import get_rule_by_id, strip_coverage_logger
1815
from .cterm import CTerm
1916
from .kast.inner import KInner
@@ -61,11 +58,6 @@
6158
_LOGGER: Final = logging.getLogger(__name__)
6259

6360

64-
class PrintInput(Enum):
65-
KORE_JSON = 'kore-json'
66-
KAST_JSON = 'kast-json'
67-
68-
6961
def main() -> None:
7062
# KAST terms can end up nested quite deeply, because of the various assoc operators (eg. _Map_, _Set_, ...).
7163
# Most pyk operations are defined recursively, meaning you get a callstack the same depth as the term.
@@ -74,10 +66,12 @@ def main() -> None:
7466

7567
cli_parser = create_argument_parser()
7668
args = cli_parser.parse_args()
69+
toml_args = parse_toml_args(args)
7770

78-
stripped_args = {
71+
stripped_args = toml_args | {
7972
key: val for (key, val) in vars(args).items() if val is not None and not (isinstance(val, Iterable) and not val)
8073
}
74+
8175
options = generate_options(stripped_args)
8276

8377
logging.basicConfig(level=loglevel(args), format=LOG_FORMAT)
@@ -389,150 +383,5 @@ def exec_json_to_kore(options: JsonToKoreOptions) -> None:
389383
sys.stdout.write('\n')
390384

391385

392-
def create_argument_parser() -> ArgumentParser:
393-
k_cli_args = KCLIArgs()
394-
395-
pyk_args = ArgumentParser()
396-
pyk_args_command = pyk_args.add_subparsers(dest='command', required=True)
397-
398-
print_args = pyk_args_command.add_parser(
399-
'print',
400-
help='Pretty print a term.',
401-
parents=[k_cli_args.logging_args, k_cli_args.display_args],
402-
)
403-
print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
404-
print_args.add_argument('term', type=FileType('r'), help='Input term (in format specified with --input).')
405-
print_args.add_argument('--input', type=PrintInput, choices=list(PrintInput))
406-
print_args.add_argument('--omit-labels', nargs='?', help='List of labels to omit from output.')
407-
print_args.add_argument('--keep-cells', nargs='?', help='List of cells with primitive values to keep in output.')
408-
print_args.add_argument('--output-file', type=FileType('w'))
409-
410-
rpc_print_args = pyk_args_command.add_parser(
411-
'rpc-print',
412-
help='Pretty-print an RPC request/response',
413-
parents=[k_cli_args.logging_args],
414-
)
415-
rpc_print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
416-
rpc_print_args.add_argument(
417-
'input_file',
418-
type=FileType('r'),
419-
help='An input file containing the JSON RPC request or response with KoreJSON payload.',
420-
)
421-
rpc_print_args.add_argument('--output-file', type=FileType('w'))
422-
423-
rpc_kast_args = pyk_args_command.add_parser(
424-
'rpc-kast',
425-
help='Convert an "execute" JSON RPC response to a new "execute" or "simplify" request, copying parameters from a reference request.',
426-
parents=[k_cli_args.logging_args],
427-
)
428-
rpc_kast_args.add_argument(
429-
'reference_request_file',
430-
type=FileType('r'),
431-
help='An input file containing a JSON RPC request to server as a reference for the new request.',
432-
)
433-
rpc_kast_args.add_argument(
434-
'response_file',
435-
type=FileType('r'),
436-
help='An input file containing a JSON RPC response with KoreJSON payload.',
437-
)
438-
rpc_kast_args.add_argument('--output-file', type=FileType('w'))
439-
440-
prove_legacy_args = pyk_args_command.add_parser(
441-
'prove-legacy',
442-
help='Prove an input specification (using kprovex).',
443-
parents=[k_cli_args.logging_args],
444-
)
445-
prove_legacy_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
446-
prove_legacy_args.add_argument('main_file', type=str, help='Main file used for kompilation.')
447-
prove_legacy_args.add_argument('spec_file', type=str, help='File with the specification module.')
448-
prove_legacy_args.add_argument('spec_module', type=str, help='Module with claims to be proven.')
449-
prove_legacy_args.add_argument('--output-file', type=FileType('w'))
450-
prove_legacy_args.add_argument('kArgs', nargs='*', help='Arguments to pass through to K invocation.')
451-
452-
kompile_args = pyk_args_command.add_parser(
453-
'kompile',
454-
help='Kompile the K specification.',
455-
parents=[k_cli_args.logging_args, k_cli_args.warning_args, k_cli_args.definition_args, k_cli_args.kompile_args],
456-
)
457-
kompile_args.add_argument('main_file', type=str, help='File with the specification module.')
458-
459-
run_args = pyk_args_command.add_parser(
460-
'run',
461-
help='Run a given program using the K definition.',
462-
parents=[k_cli_args.logging_args],
463-
)
464-
run_args.add_argument('pgm_file', type=str, help='File program to run in it.')
465-
run_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.')
466-
467-
prove_args = pyk_args_command.add_parser(
468-
'prove',
469-
help='Prove an input specification (using RPC based prover).',
470-
parents=[k_cli_args.logging_args, k_cli_args.spec_args],
471-
)
472-
prove_args.add_argument(
473-
'--failure-info',
474-
default=None,
475-
action='store_true',
476-
help='Print out more information about proof failures.',
477-
)
478-
prove_args.add_argument(
479-
'--show-kcfg',
480-
default=None,
481-
action='store_true',
482-
help='Display the resulting proof KCFG.',
483-
)
484-
prove_args.add_argument(
485-
'--max-depth',
486-
type=int,
487-
help='Maximum number of steps to take in symbolic execution per basic block.',
488-
)
489-
prove_args.add_argument(
490-
'--max-iterations',
491-
type=int,
492-
help='Maximum number of KCFG explorations to take in attempting to discharge proof.',
493-
)
494-
495-
show_args = pyk_args_command.add_parser(
496-
'show',
497-
help='Display the status of a given proof.',
498-
parents=[k_cli_args.logging_args, k_cli_args.spec_args],
499-
)
500-
show_args.add_argument(
501-
'--failure-info',
502-
default=None,
503-
action='store_true',
504-
help='Print out more information about proof failures.',
505-
)
506-
prove_args.add_argument(
507-
'--kore-rpc-command',
508-
dest='kore_rpc_command',
509-
type=str,
510-
default=None,
511-
help='Custom command to start RPC server.',
512-
)
513-
514-
graph_imports_args = pyk_args_command.add_parser(
515-
'graph-imports',
516-
help='Graph the imports of a given definition.',
517-
parents=[k_cli_args.logging_args],
518-
)
519-
graph_imports_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
520-
521-
coverage_args = pyk_args_command.add_parser(
522-
'coverage',
523-
help='Convert coverage file to human readable log.',
524-
parents=[k_cli_args.logging_args],
525-
)
526-
coverage_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
527-
coverage_args.add_argument('coverage_file', type=FileType('r'), help='Coverage file to build log for.')
528-
coverage_args.add_argument('-o', '--output', type=FileType('w'))
529-
530-
pyk_args_command.add_parser('kore-to-json', help='Convert textual KORE to JSON', parents=[k_cli_args.logging_args])
531-
532-
pyk_args_command.add_parser('json-to-kore', help='Convert JSON to textual KORE', parents=[k_cli_args.logging_args])
533-
534-
return pyk_args
535-
536-
537386
if __name__ == '__main__':
538387
main()

‎pyk/src/pyk/cli/args.py

+71
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,12 @@ def default() -> dict[str, Any]:
2727
'debug': False,
2828
}
2929

30+
@staticmethod
31+
def from_option_string() -> dict[str, Any]:
32+
return {
33+
'v': 'verbose',
34+
}
35+
3036

3137
class WarningOptions(Options):
3238
warnings: Warnings | None
@@ -39,6 +45,13 @@ def default() -> dict[str, Any]:
3945
'warnings_to_errors': False,
4046
}
4147

48+
@staticmethod
49+
def from_option_string() -> dict[str, Any]:
50+
return {
51+
'w': 'warnings',
52+
'w2e': 'warning_to_error',
53+
}
54+
4255

4356
class OutputFileOptions(Options):
4457
output_file: IO[Any]
@@ -53,6 +66,13 @@ def default() -> dict[str, Any]:
5366
class DefinitionOptions(Options):
5467
definition_dir: Path
5568

69+
@staticmethod
70+
def default() -> dict[str, Any]:
71+
return {
72+
'output-definition': 'definition_dir',
73+
'definition': 'definition_dir',
74+
}
75+
5676

5777
class DisplayOptions(Options):
5878
minimize: bool
@@ -81,6 +101,12 @@ def default() -> dict[str, Any]:
81101
'includes': [],
82102
}
83103

104+
@staticmethod
105+
def from_option_string() -> dict[str, str]:
106+
return {
107+
'includes': 'includes',
108+
}
109+
84110

85111
class SaveDirOptions(Options):
86112
save_directory: Path | None
@@ -108,6 +134,13 @@ def default() -> dict[str, Any]:
108134
'exclude_claim_labels': None,
109135
}
110136

137+
@staticmethod
138+
def from_option_string() -> dict[str, str]:
139+
return SaveDirOptions.from_option_string() | {
140+
'claim': 'claim_labels',
141+
'exclude-claim': 'exclude_claim_labels',
142+
}
143+
111144

112145
class KompileOptions(Options):
113146
emit_json: bool
@@ -154,6 +187,18 @@ def default() -> dict[str, Any]:
154187
'no_exc_wrap': False,
155188
}
156189

190+
@staticmethod
191+
def from_option_string() -> dict[str, str]:
192+
return {
193+
'with-llvm-library': 'llvm_library',
194+
'read-only-kompiled-directory': 'read_only',
195+
'ccopt': 'ccopts',
196+
'O0': 'o0',
197+
'O1': 'o1',
198+
'O2': 'o2',
199+
'O3': 'o3',
200+
}
201+
157202

158203
class ParallelOptions(Options):
159204
workers: int
@@ -164,6 +209,12 @@ def default() -> dict[str, Any]:
164209
'workers': 1,
165210
}
166211

212+
@staticmethod
213+
def from_option_string() -> dict[str, str]:
214+
return {
215+
'j': 'workers',
216+
}
217+
167218

168219
class BugReportOptions(Options):
169220
bug_report: BugReport | None
@@ -187,6 +238,26 @@ def default() -> dict[str, Any]:
187238
}
188239

189240

241+
class ConfigArgs:
242+
@cached_property
243+
def config_args(self) -> ArgumentParser:
244+
args = ArgumentParser(add_help=False)
245+
args.add_argument(
246+
'--config-file',
247+
dest='config_file',
248+
type=file_path,
249+
default=Path('./pyk.toml'),
250+
help='Path to Pyk config file.',
251+
)
252+
args.add_argument(
253+
'--config-profile',
254+
dest='config_profile',
255+
default='default',
256+
help='Config profile to be used.',
257+
)
258+
return args
259+
260+
190261
class KCLIArgs:
191262
@cached_property
192263
def logging_args(self) -> ArgumentParser:

‎pyk/src/pyk/cli/cli.py

+4
Original file line numberDiff line numberDiff line change
@@ -16,3 +16,7 @@ def __init__(self, args: dict[str, Any]) -> None:
1616

1717
for attr, val in _args.items():
1818
self.__setattr__(attr, val)
19+
20+
@staticmethod
21+
def from_option_string() -> dict[str, str]:
22+
return {}

0 commit comments

Comments
 (0)