Skip to content

Commit 17fb23c

Browse files
ehildenbrv-auditor
ehildenb
and
rv-auditor
authored
Revert changes to options (runtimeverification/pyk#956)
Two changes to options are reverted, which weren't able to be pushed through KEVM: - runtimeverification/pyk#955 - runtimeverification/pyk#916 --------- Co-authored-by: devops <[email protected]>
1 parent fe7b775 commit 17fb23c

File tree

9 files changed

+510
-895
lines changed

9 files changed

+510
-895
lines changed

‎pyk/docs/conf.py

+2-2
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@
99
project = 'pyk'
1010
author = 'Runtime Verification, Inc'
1111
copyright = '2024, Runtime Verification, Inc'
12-
version = '0.1.690'
13-
release = '0.1.690'
12+
version = '0.1.691'
13+
release = '0.1.691'
1414

1515
# -- General configuration ---------------------------------------------------
1616
# https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

‎pyk/package/version

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.1.690
1+
0.1.691

‎pyk/pyproject.toml

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "pyk"
7-
version = "0.1.690"
7+
version = "0.1.691"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

‎pyk/src/pyk/__main__.py

+322-29
Original file line numberDiff line numberDiff line change
@@ -1,52 +1,345 @@
11
from __future__ import annotations
22

3+
import json
34
import logging
45
import sys
6+
from argparse import ArgumentParser, FileType
7+
from enum import Enum
8+
from pathlib import Path
59
from typing import TYPE_CHECKING
610

7-
from .cli.args import LoggingOptions
8-
from .cli.cli import CLI
9-
from .cli.pyk import (
10-
CoverageCommand,
11-
GraphImportsCommand,
12-
JsonToKoreCommand,
13-
KoreToJsonCommand,
14-
PrintCommand,
15-
ProveCommand,
16-
RPCKastCommand,
17-
RPCPrintCommand,
11+
from graphviz import Digraph
12+
13+
from pyk.kast.inner import KInner
14+
from pyk.kore.rpc import ExecuteResult
15+
16+
from .cli.args import KCLIArgs
17+
from .cli.utils import LOG_FORMAT, dir_path, loglevel
18+
from .coverage import get_rule_by_id, strip_coverage_logger
19+
from .cterm import CTerm
20+
from .kast.manip import (
21+
flatten_label,
22+
minimize_rule,
23+
minimize_term,
24+
propagate_up_constraints,
25+
remove_source_map,
26+
split_config_and_constraints,
1827
)
19-
from .cli.utils import LOG_FORMAT, loglevel
28+
from .kast.outer import read_kast_definition
29+
from .kast.pretty import PrettyPrinter
30+
from .kore.parser import KoreParser
31+
from .kore.rpc import StopReason
32+
from .kore.syntax import Pattern, kore_term
33+
from .ktool.kprint import KPrint
34+
from .ktool.kprove import KProve
35+
from .prelude.k import GENERATED_TOP_CELL
36+
from .prelude.ml import is_top, mlAnd, mlOr
2037

2138
if TYPE_CHECKING:
22-
from typing import Final
39+
from argparse import Namespace
40+
from typing import Any, Final
2341

2442

2543
_LOGGER: Final = logging.getLogger(__name__)
2644

2745

46+
class PrintInput(Enum):
47+
KORE_JSON = 'kore-json'
48+
KAST_JSON = 'kast-json'
49+
50+
2851
def main() -> None:
2952
# KAST terms can end up nested quite deeply, because of the various assoc operators (eg. _Map_, _Set_, ...).
3053
# Most pyk operations are defined recursively, meaning you get a callstack the same depth as the term.
3154
# This change makes it so that in most cases, by default, pyk doesn't run out of stack space.
3255
sys.setrecursionlimit(10**7)
3356

34-
cli = CLI(
35-
[
36-
CoverageCommand,
37-
GraphImportsCommand,
38-
JsonToKoreCommand,
39-
KoreToJsonCommand,
40-
PrintCommand,
41-
ProveCommand,
42-
RPCKastCommand,
43-
RPCPrintCommand,
44-
]
45-
)
46-
command = cli.get_command()
47-
assert isinstance(command, LoggingOptions)
48-
logging.basicConfig(level=loglevel(command), format=LOG_FORMAT)
49-
command.exec()
57+
cli_parser = create_argument_parser()
58+
args = cli_parser.parse_args()
59+
60+
logging.basicConfig(level=loglevel(args), format=LOG_FORMAT)
61+
62+
executor_name = 'exec_' + args.command.lower().replace('-', '_')
63+
if executor_name not in globals():
64+
raise AssertionError(f'Unimplemented command: {args.command}')
65+
66+
execute = globals()[executor_name]
67+
execute(args)
68+
69+
70+
def exec_print(args: Namespace) -> None:
71+
kompiled_dir: Path = args.definition_dir
72+
printer = KPrint(kompiled_dir)
73+
if args.input == PrintInput.KORE_JSON:
74+
_LOGGER.info(f'Reading Kore JSON from file: {args.term.name}')
75+
kore = Pattern.from_json(args.term.read())
76+
term = printer.kore_to_kast(kore)
77+
else:
78+
_LOGGER.info(f'Reading Kast JSON from file: {args.term.name}')
79+
term = KInner.from_json(args.term.read())
80+
if is_top(term):
81+
args.output_file.write(printer.pretty_print(term))
82+
_LOGGER.info(f'Wrote file: {args.output_file.name}')
83+
else:
84+
if args.minimize:
85+
if args.omit_labels != '' and args.keep_cells != '':
86+
raise ValueError('You cannot use both --omit-labels and --keep-cells.')
87+
88+
abstract_labels = args.omit_labels.split(',') if args.omit_labels != '' else []
89+
keep_cells = args.keep_cells.split(',') if args.keep_cells != '' else []
90+
minimized_disjuncts = []
91+
92+
for disjunct in flatten_label('#Or', term):
93+
try:
94+
minimized = minimize_term(disjunct, abstract_labels=abstract_labels, keep_cells=keep_cells)
95+
config, constraint = split_config_and_constraints(minimized)
96+
except ValueError as err:
97+
raise ValueError('The minimized term does not contain a config cell.') from err
98+
99+
if not is_top(constraint):
100+
minimized_disjuncts.append(mlAnd([config, constraint], sort=GENERATED_TOP_CELL))
101+
else:
102+
minimized_disjuncts.append(config)
103+
term = propagate_up_constraints(mlOr(minimized_disjuncts, sort=GENERATED_TOP_CELL))
104+
105+
args.output_file.write(printer.pretty_print(term))
106+
_LOGGER.info(f'Wrote file: {args.output_file.name}')
107+
108+
109+
def exec_rpc_print(args: Namespace) -> None:
110+
kompiled_dir: Path = args.definition_dir
111+
printer = KPrint(kompiled_dir)
112+
input_dict = json.loads(args.input_file.read())
113+
output_buffer = []
114+
115+
def pretty_print_request(request_params: dict[str, Any]) -> list[str]:
116+
output_buffer = []
117+
non_state_keys = set(request_params.keys()).difference(['state'])
118+
for key in non_state_keys:
119+
output_buffer.append(f'{key}: {request_params[key]}')
120+
state = CTerm.from_kast(printer.kore_to_kast(kore_term(request_params['state'])))
121+
output_buffer.append('State:')
122+
output_buffer.append(printer.pretty_print(state.kast, sort_collections=True))
123+
return output_buffer
124+
125+
def pretty_print_execute_response(execute_result: ExecuteResult) -> list[str]:
126+
output_buffer = []
127+
output_buffer.append(f'Depth: {execute_result.depth}')
128+
output_buffer.append(f'Stop reason: {execute_result.reason.value}')
129+
if execute_result.reason == StopReason.TERMINAL_RULE or execute_result.reason == StopReason.CUT_POINT_RULE:
130+
output_buffer.append(f'Stop rule: {execute_result.rule}')
131+
output_buffer.append(
132+
f'Number of next states: {len(execute_result.next_states) if execute_result.next_states is not None else 0}'
133+
)
134+
state = CTerm.from_kast(printer.kore_to_kast(execute_result.state.kore))
135+
output_buffer.append('State:')
136+
output_buffer.append(printer.pretty_print(state.kast, sort_collections=True))
137+
if execute_result.next_states is not None:
138+
next_states = [CTerm.from_kast(printer.kore_to_kast(s.kore)) for s in execute_result.next_states]
139+
for i, s in enumerate(next_states):
140+
output_buffer.append(f'Next state #{i}:')
141+
output_buffer.append(printer.pretty_print(s.kast, sort_collections=True))
142+
return output_buffer
143+
144+
try:
145+
if 'method' in input_dict:
146+
output_buffer.append('JSON RPC request')
147+
output_buffer.append(f'id: {input_dict["id"]}')
148+
output_buffer.append(f'Method: {input_dict["method"]}')
149+
try:
150+
if 'state' in input_dict['params']:
151+
output_buffer += pretty_print_request(input_dict['params'])
152+
else: # this is an "add-module" request, skip trying to print state
153+
for key in input_dict['params'].keys():
154+
output_buffer.append(f'{key}: {input_dict["params"][key]}')
155+
except KeyError as e:
156+
_LOGGER.critical(f'Could not find key {str(e)} in input JSON file')
157+
exit(1)
158+
else:
159+
if not 'result' in input_dict:
160+
_LOGGER.critical('The input is neither a request not a resonse')
161+
exit(1)
162+
output_buffer.append('JSON RPC Response')
163+
output_buffer.append(f'id: {input_dict["id"]}')
164+
if list(input_dict['result'].keys()) == ['state']: # this is a "simplify" response
165+
output_buffer.append('Method: simplify')
166+
state = CTerm.from_kast(printer.kore_to_kast(kore_term(input_dict['result']['state'])))
167+
output_buffer.append('State:')
168+
output_buffer.append(printer.pretty_print(state.kast, sort_collections=True))
169+
elif list(input_dict['result'].keys()) == ['module']: # this is an "add-module" response
170+
output_buffer.append('Method: add-module')
171+
output_buffer.append('Module:')
172+
output_buffer.append(input_dict['result']['module'])
173+
else:
174+
try: # assume it is an "execute" response
175+
output_buffer.append('Method: execute')
176+
execute_result = ExecuteResult.from_dict(input_dict['result'])
177+
output_buffer += pretty_print_execute_response(execute_result)
178+
except KeyError as e:
179+
_LOGGER.critical(f'Could not find key {str(e)} in input JSON file')
180+
exit(1)
181+
if args.output_file is not None:
182+
args.output_file.write('\n'.join(output_buffer))
183+
else:
184+
print('\n'.join(output_buffer))
185+
except ValueError as e:
186+
# shorten and print the error message in case kore_to_kast throws ValueError
187+
_LOGGER.critical(str(e)[:200])
188+
exit(1)
189+
190+
191+
def exec_rpc_kast(args: Namespace) -> None:
192+
"""
193+
Convert an 'execute' JSON RPC response to a new 'execute' or 'simplify' request,
194+
copying parameters from a reference request.
195+
"""
196+
reference_request = json.loads(args.reference_request_file.read())
197+
input_dict = json.loads(args.response_file.read())
198+
execute_result = ExecuteResult.from_dict(input_dict['result'])
199+
non_state_keys = set(reference_request['params'].keys()).difference(['state'])
200+
request_params = {}
201+
for key in non_state_keys:
202+
request_params[key] = reference_request['params'][key]
203+
request_params['state'] = {'format': 'KORE', 'version': 1, 'term': execute_result.state.kore.dict}
204+
request = {
205+
'jsonrpc': reference_request['jsonrpc'],
206+
'id': reference_request['id'],
207+
'method': reference_request['method'],
208+
'params': request_params,
209+
}
210+
args.output_file.write(json.dumps(request))
211+
212+
213+
def exec_prove(args: Namespace) -> None:
214+
kompiled_dir: Path = args.definition_dir
215+
kprover = KProve(kompiled_dir, args.main_file)
216+
final_state = kprover.prove(Path(args.spec_file), spec_module_name=args.spec_module, args=args.kArgs)
217+
args.output_file.write(json.dumps(mlOr([state.kast for state in final_state]).to_dict()))
218+
_LOGGER.info(f'Wrote file: {args.output_file.name}')
219+
220+
221+
def exec_graph_imports(args: Namespace) -> None:
222+
kompiled_dir: Path = args.definition_dir
223+
kprinter = KPrint(kompiled_dir)
224+
definition = kprinter.definition
225+
import_graph = Digraph()
226+
graph_file = kompiled_dir / 'import-graph'
227+
for module in definition.modules:
228+
module_name = module.name
229+
import_graph.node(module_name)
230+
for module_import in module.imports:
231+
import_graph.edge(module_name, module_import.name)
232+
import_graph.render(graph_file)
233+
_LOGGER.info(f'Wrote file: {graph_file}')
234+
235+
236+
def exec_coverage(args: Namespace) -> None:
237+
kompiled_dir: Path = args.definition_dir
238+
definition = remove_source_map(read_kast_definition(kompiled_dir / 'compiled.json'))
239+
pretty_printer = PrettyPrinter(definition)
240+
for rid in args.coverage_file:
241+
rule = minimize_rule(strip_coverage_logger(get_rule_by_id(definition, rid.strip())))
242+
args.output.write('\n\n')
243+
args.output.write('Rule: ' + rid.strip())
244+
args.output.write('\nUnparsed:\n')
245+
args.output.write(pretty_printer.print(rule))
246+
_LOGGER.info(f'Wrote file: {args.output.name}')
247+
248+
249+
def exec_kore_to_json(args: Namespace) -> None:
250+
text = sys.stdin.read()
251+
kore = KoreParser(text).pattern()
252+
print(kore.json)
253+
254+
255+
def exec_json_to_kore(args: dict[str, Any]) -> None:
256+
text = sys.stdin.read()
257+
kore = Pattern.from_json(text)
258+
kore.write(sys.stdout)
259+
sys.stdout.write('\n')
260+
261+
262+
def create_argument_parser() -> ArgumentParser:
263+
k_cli_args = KCLIArgs()
264+
265+
definition_args = ArgumentParser(add_help=False)
266+
definition_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
267+
268+
pyk_args = ArgumentParser()
269+
pyk_args_command = pyk_args.add_subparsers(dest='command', required=True)
270+
271+
print_args = pyk_args_command.add_parser(
272+
'print',
273+
help='Pretty print a term.',
274+
parents=[k_cli_args.logging_args, definition_args, k_cli_args.display_args],
275+
)
276+
print_args.add_argument('term', type=FileType('r'), help='Input term (in format specified with --input).')
277+
print_args.add_argument('--input', default=PrintInput.KAST_JSON, type=PrintInput, choices=list(PrintInput))
278+
print_args.add_argument('--omit-labels', default='', nargs='?', help='List of labels to omit from output.')
279+
print_args.add_argument(
280+
'--keep-cells', default='', nargs='?', help='List of cells with primitive values to keep in output.'
281+
)
282+
print_args.add_argument('--output-file', type=FileType('w'), default='-')
283+
284+
rpc_print_args = pyk_args_command.add_parser(
285+
'rpc-print',
286+
help='Pretty-print an RPC request/response',
287+
parents=[k_cli_args.logging_args, definition_args],
288+
)
289+
rpc_print_args.add_argument(
290+
'input_file',
291+
type=FileType('r'),
292+
help='An input file containing the JSON RPC request or response with KoreJSON payload.',
293+
)
294+
rpc_print_args.add_argument('--output-file', type=FileType('w'), default='-')
295+
296+
rpc_kast_args = pyk_args_command.add_parser(
297+
'rpc-kast',
298+
help='Convert an "execute" JSON RPC response to a new "execute" or "simplify" request, copying parameters from a reference request.',
299+
parents=[k_cli_args.logging_args],
300+
)
301+
rpc_kast_args.add_argument(
302+
'reference_request_file',
303+
type=FileType('r'),
304+
help='An input file containing a JSON RPC request to server as a reference for the new request.',
305+
)
306+
rpc_kast_args.add_argument(
307+
'response_file',
308+
type=FileType('r'),
309+
help='An input file containing a JSON RPC response with KoreJSON payload.',
310+
)
311+
rpc_kast_args.add_argument('--output-file', type=FileType('w'), default='-')
312+
313+
prove_args = pyk_args_command.add_parser(
314+
'prove',
315+
help='Prove an input specification (using kprovex).',
316+
parents=[k_cli_args.logging_args, definition_args],
317+
)
318+
prove_args.add_argument('main_file', type=str, help='Main file used for kompilation.')
319+
prove_args.add_argument('spec_file', type=str, help='File with the specification module.')
320+
prove_args.add_argument('spec_module', type=str, help='Module with claims to be proven.')
321+
prove_args.add_argument('--output-file', type=FileType('w'), default='-')
322+
prove_args.add_argument('kArgs', nargs='*', help='Arguments to pass through to K invocation.')
323+
324+
pyk_args_command.add_parser(
325+
'graph-imports',
326+
help='Graph the imports of a given definition.',
327+
parents=[k_cli_args.logging_args, definition_args],
328+
)
329+
330+
coverage_args = pyk_args_command.add_parser(
331+
'coverage',
332+
help='Convert coverage file to human readable log.',
333+
parents=[k_cli_args.logging_args, definition_args],
334+
)
335+
coverage_args.add_argument('coverage_file', type=FileType('r'), help='Coverage file to build log for.')
336+
coverage_args.add_argument('-o', '--output', type=FileType('w'), default='-')
337+
338+
pyk_args_command.add_parser('kore-to-json', help='Convert textual KORE to JSON', parents=[k_cli_args.logging_args])
339+
340+
pyk_args_command.add_parser('json-to-kore', help='Convert JSON to textual KORE', parents=[k_cli_args.logging_args])
341+
342+
return pyk_args
50343

51344

52345
if __name__ == '__main__':

0 commit comments

Comments
 (0)