From e08b9e4755c66abf0af0e710484f445a2a5748d3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 13 Nov 2024 11:50:43 +0000 Subject: [PATCH 1/6] Remove `krun` --- examples/specs/imp-sum-spec.k | 2 +- kimp/src/kimp/kimp.py | 7 +------ 2 files changed, 2 insertions(+), 7 deletions(-) diff --git a/examples/specs/imp-sum-spec.k b/examples/specs/imp-sum-spec.k index 389005b..4c44ac2 100644 --- a/examples/specs/imp-sum-spec.k +++ b/examples/specs/imp-sum-spec.k @@ -42,4 +42,4 @@ module IMP-SUM-SPEC requires N >=Int 0 andBool M >=Int 0 -endmodule \ No newline at end of file +endmodule diff --git a/kimp/src/kimp/kimp.py b/kimp/src/kimp/kimp.py index 4109305..4ede177 100644 --- a/kimp/src/kimp/kimp.py +++ b/kimp/src/kimp/kimp.py @@ -23,7 +23,7 @@ from pyk.kore.rpc import KoreClient, kore_server from pyk.ktool.claim_loader import ClaimLoader from pyk.ktool.kprove import KProve -from pyk.ktool.krun import KRun, KRunOutput, _krun +from pyk.ktool.krun import KRunOutput, _krun from pyk.proof.reachability import APRProof, APRProver from pyk.proof.show import APRProofShow from pyk.proof.tui import APRProofViewer @@ -122,11 +122,6 @@ def format(self) -> Formatter: def kprove(self) -> KProve: return KProve(definition_dir=self.haskell_dir, use_directory=self.proof_dir) - @cached_property - def krun(self) -> KRun: - krun = KRun(definition_dir=self.llvm_dir) - return krun - def run_program( self, program_file: str | Path, From cd0e764c18da1f8425e6ef29cfc9eb844ae14b13 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 13 Nov 2024 11:57:45 +0000 Subject: [PATCH 2/6] Rename `KIMP` to `KImp` --- kimp/src/kimp/__main__.py | 13 ++++++------- kimp/src/kimp/kimp.py | 14 +++++++------- 2 files changed, 13 insertions(+), 14 deletions(-) diff --git a/kimp/src/kimp/__main__.py b/kimp/src/kimp/__main__.py index c43b598..ef2738b 100644 --- a/kimp/src/kimp/__main__.py +++ b/kimp/src/kimp/__main__.py @@ -11,7 +11,7 @@ from pyk.ktool.kprint import KAstOutput from pyk.ktool.krun import KRunOutput -from .kimp import KIMP +from .kimp import KImp if TYPE_CHECKING: from argparse import Namespace @@ -77,7 +77,7 @@ def exec_run( krun_output = KRunOutput[output.upper()] definition_dir_path = find_target('llvm') if definition_dir is None else Path(definition_dir) - kimp = KIMP(definition_dir_path, definition_dir_path) + kimp = KImp(definition_dir_path, definition_dir_path) try: with NamedTemporaryFile(mode='w') as f: @@ -114,7 +114,7 @@ def exec_prove( definition_dir = str(find_target('haskell')) k_src_dir = str(find_target('source') / 'imp-semantics') - kimp = KIMP(definition_dir, definition_dir) + kimp = KImp(definition_dir, definition_dir) try: kimp.prove( @@ -128,7 +128,6 @@ def exec_prove( ) except ValueError as err: _LOGGER.critical(err.args) - # exit(1) raise except RuntimeError as err: if ignore_return_code: @@ -147,7 +146,7 @@ def exec_show( **kwargs: Any, ) -> None: definition_dir = str(find_target('haskell')) - kimp = KIMP(definition_dir, definition_dir) + kimp = KImp(definition_dir, definition_dir) kimp.show_kcfg(spec_module, claim_id) @@ -158,7 +157,7 @@ def exec_view( **kwargs: Any, ) -> None: definition_dir = str(find_target('haskell')) - kimp = KIMP(definition_dir, definition_dir) + kimp = KImp(definition_dir, definition_dir) kimp.view_kcfg(spec_module, claim_id) @@ -218,7 +217,7 @@ def create_argument_parser() -> ArgumentParser: help='Store every Nth state in the CFG for inspection.', ) - parser = ArgumentParser(prog='kimp', description='KIMP command line tool') + parser = ArgumentParser(prog='kimp', description='KImp command line tool') command_parser = parser.add_subparsers(dest='command', required=True, help='Command to execute') # Run diff --git a/kimp/src/kimp/kimp.py b/kimp/src/kimp/kimp.py index 4ede177..10f6020 100644 --- a/kimp/src/kimp/kimp.py +++ b/kimp/src/kimp/kimp.py @@ -2,7 +2,7 @@ from pyk.kcfg.show import NodePrinter -__all__ = ['KIMP'] +__all__ = ['KImp'] import logging from contextlib import contextmanager @@ -87,7 +87,7 @@ def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool: @final @dataclass(frozen=True) -class KIMP: +class KImp: llvm_dir: Path haskell_dir: Path proof_dir: Path @@ -217,7 +217,7 @@ def view_kcfg( claim_id: str, ) -> None: proof = APRProof.read_proof_data(proof_dir=self.proof_dir, id=f'{spec_module}.{claim_id}') - kcfg_viewer = APRProofViewer(proof, self.kprove, node_printer=KIMPNodePrinter(kimp=self)) + kcfg_viewer = APRProofViewer(proof, self.kprove, node_printer=ImpNodePrinter(kimp=self)) kcfg_viewer.run() def show_kcfg( @@ -226,7 +226,7 @@ def show_kcfg( claim_id: str, ) -> None: proof = APRProof.read_proof_data(proof_dir=self.proof_dir, id=f'{spec_module}.{claim_id}') - proof_show = APRProofShow(self.kprove, node_printer=KIMPNodePrinter(kimp=self)) + proof_show = APRProofShow(self.kprove, node_printer=ImpNodePrinter(kimp=self)) res_lines = proof_show.show( proof, ) @@ -298,10 +298,10 @@ def legacy_explore( ) -class KIMPNodePrinter(NodePrinter): - kimp: KIMP +class ImpNodePrinter(NodePrinter): + kimp: KImp - def __init__(self, kimp: KIMP): + def __init__(self, kimp: KImp): NodePrinter.__init__(self, kimp.kprove) self.kimp = kimp From 151e167b028d265a1836240780019815085aa923 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 13 Nov 2024 14:15:05 +0000 Subject: [PATCH 3/6] Simplify `exec_run` --- kimp/src/kimp/__main__.py | 68 +++------------- .../src/kimp/kdist/imp-semantics/statements.k | 3 +- kimp/src/kimp/kimp.py | 77 ++++++++++--------- package/smoke-test.sh | 2 +- 4 files changed, 52 insertions(+), 98 deletions(-) diff --git a/kimp/src/kimp/__main__.py b/kimp/src/kimp/__main__.py index ef2738b..27d8eef 100644 --- a/kimp/src/kimp/__main__.py +++ b/kimp/src/kimp/__main__.py @@ -4,12 +4,9 @@ import os from argparse import ArgumentParser from pathlib import Path -from tempfile import NamedTemporaryFile from typing import TYPE_CHECKING, Any, Final from pyk.cli.utils import dir_path, file_path -from pyk.ktool.kprint import KAstOutput -from pyk.ktool.krun import KRunOutput from .kimp import KImp @@ -66,37 +63,17 @@ def main() -> None: def exec_run( - input_file: str, - definition_dir: str, - input_term: str | None = None, - output: str = 'none', - ignore_return_code: bool = False, + input_file: Path, + definition_dir: Path | None, depth: int | None = None, **kwargs: Any, ) -> None: - krun_output = KRunOutput[output.upper()] - - definition_dir_path = find_target('llvm') if definition_dir is None else Path(definition_dir) - kimp = KImp(definition_dir_path, definition_dir_path) - - try: - with NamedTemporaryFile(mode='w') as f: - temp_file = Path(f.name) - if input_term is not None: - temp_file.write_text(input_term) - else: - temp_file.write_text(Path(input_file).read_text()) - proc_res = kimp.run_program(temp_file, output=krun_output, depth=depth) - if output != KAstOutput.NONE: - print(proc_res.stdout) - except RuntimeError as err: - if ignore_return_code: - msg, stdout, stderr = err.args - print(stdout) - print(stderr) - print(msg) - else: - raise + definition_dir = find_target('llvm') if definition_dir is None else definition_dir + kimp = KImp(definition_dir, definition_dir) + pgm = input_file.read_text() + pattern = kimp.pattern(pgm=pgm, env={}) + output = kimp.run(pattern, depth=depth) + print(kimp.pretty(output)) def exec_prove( @@ -169,7 +146,6 @@ def create_argument_parser() -> ArgumentParser: shared_args.add_argument( '--definition', dest='definition_dir', - nargs='?', type=dir_path, help='Path to compiled K definition to use.', ) @@ -222,33 +198,7 @@ def create_argument_parser() -> ArgumentParser: # Run run_subparser = command_parser.add_parser('run', help='Run an IMP program', parents=[shared_args]) - input_group = run_subparser.add_mutually_exclusive_group(required=True) - input_group.add_argument( - '--input-file', - type=file_path, - help='Path to .imp file', - ) - input_group.add_argument( - '--input-term', - dest='input_term', - type=str, - help='Program to run, as a literal string', - ) - run_subparser.add_argument( - '--output', - dest='output', - type=str, - default='pretty', - help='Output mode', - choices=['pretty', 'program', 'json', 'kore', 'kast', 'none'], - required=False, - ) - run_subparser.add_argument( - '--ignore-return-code', - action='store_true', - default=False, - help='Ignore return code of krun, alwasys return 0 (use for debugging only)', - ) + run_subparser.add_argument('input_file', metavar='INPUT_FILE', type=file_path, help='Path to .imp file') run_subparser.add_argument( '--depth', dest='depth', diff --git a/kimp/src/kimp/kdist/imp-semantics/statements.k b/kimp/src/kimp/kdist/imp-semantics/statements.k index f498362..58395eb 100644 --- a/kimp/src/kimp/kdist/imp-semantics/statements.k +++ b/kimp/src/kimp/kdist/imp-semantics/statements.k @@ -40,14 +40,13 @@ module STATEMENTS-RULES endmodule module STATEMENTS - imports EXPRESSIONS imports VARIABLES-SYNTAX imports STATEMENTS-RULES configuration $PGM:Stmt // changed! - .Map + $ENV:Map // changed configuration, need to repeat the variable rule rule diff --git a/kimp/src/kimp/kimp.py b/kimp/src/kimp/kimp.py index 10f6020..dee3433 100644 --- a/kimp/src/kimp/kimp.py +++ b/kimp/src/kimp/kimp.py @@ -9,10 +9,9 @@ from dataclasses import dataclass from functools import cached_property from pathlib import Path -from tempfile import NamedTemporaryFile from typing import TYPE_CHECKING, final -from pyk.cli.utils import check_dir_path, check_file_path +from pyk.cli.utils import check_dir_path from pyk.cterm.symbolic import CTermSymbolic from pyk.kast.formatter import Formatter from pyk.kast.inner import KApply, KLabel, KSequence, KVariable @@ -23,21 +22,20 @@ from pyk.kore.rpc import KoreClient, kore_server from pyk.ktool.claim_loader import ClaimLoader from pyk.ktool.kprove import KProve -from pyk.ktool.krun import KRunOutput, _krun from pyk.proof.reachability import APRProof, APRProver from pyk.proof.show import APRProofShow from pyk.proof.tui import APRProofViewer from pyk.utils import single if TYPE_CHECKING: - from collections.abc import Iterable, Iterator - from subprocess import CompletedProcess + from collections.abc import Iterable, Iterator, Mapping from typing import Final from pyk.cterm.cterm import CTerm from pyk.kast.outer import KDefinition from pyk.kcfg.kcfg import KCFG, KCFGExtendResult from pyk.kore.rpc import FallbackReason + from pyk.kore.syntax import Pattern from pyk.ktool.kprint import KPrint from pyk.utils import BugReport @@ -106,10 +104,6 @@ def __init__(self, llvm_dir: str | Path, haskell_dir: str | Path): object.__setattr__(self, 'haskell_dir', haskell_dir) object.__setattr__(self, 'proof_dir', proof_dir) - @cached_property - def parser(self) -> Path: - return self.llvm_dir / 'parser_PGM' - @cached_property def definition(self) -> KDefinition: return read_kast_definition(self.llvm_dir / 'compiled.json') @@ -122,40 +116,51 @@ def format(self) -> Formatter: def kprove(self) -> KProve: return KProve(definition_dir=self.haskell_dir, use_directory=self.proof_dir) - def run_program( + def run( self, - program_file: str | Path, + pattern: Pattern, *, - output: KRunOutput = KRunOutput.NONE, - check: bool = True, - temp_file: str | Path | None = None, - depth: int | None, - ) -> CompletedProcess: - def run(program_file: Path) -> CompletedProcess: - return _krun( - input_file=program_file, - definition_dir=self.llvm_dir, - output=output, - check=check, - depth=depth, - pipe_stderr=True, - pmap={'PGM': str(self.parser)}, + depth: int | None = None, + ) -> Pattern: + from pyk.ktool.krun import llvm_interpret + + return llvm_interpret(definition_dir=self.llvm_dir, pattern=pattern, depth=depth) + + def pattern(self, *, pgm: str, env: Mapping[str, int]) -> Pattern: + from pyk.kore.prelude import ID, INT, SORT_K_ITEM, inj, map_pattern, top_cell_initializer + from pyk.kore.syntax import DV, SortApp, String + + pgm_pattern = self.parse(pgm) + env_pattern = map_pattern( + *( + ( + inj(ID, SORT_K_ITEM, DV(ID, String(var))), + inj(INT, SORT_K_ITEM, DV(INT, String(str(val)))), + ) + for var, val in env.items() ) + ) + return top_cell_initializer( + { + '$PGM': inj(SortApp('SortStmt'), SORT_K_ITEM, pgm_pattern), + '$ENV': inj(SortApp('SortMap'), SORT_K_ITEM, env_pattern), + } + ) + + def parse(self, pgm: str) -> Pattern: + from pyk.kore.parser import KoreParser + from pyk.utils import run_process_2 - def preprocess_and_run(program_file: Path, temp_file: Path) -> CompletedProcess: - temp_file.write_text(program_file.read_text()) - return run(temp_file) + parser = self.llvm_dir / 'parser_PGM' + args = [str(parser), '/dev/stdin'] - program_file = Path(program_file) - check_file_path(program_file) + kore_text = run_process_2(args, input=pgm).stdout + return KoreParser(kore_text).pattern() - if temp_file is None: - with NamedTemporaryFile(mode='w') as f: - temp_file = Path(f.name) - return preprocess_and_run(program_file, temp_file) + def pretty(self, pattern: Pattern) -> str: + from pyk.kore.tools import kore_print - temp_file = Path(temp_file) - return preprocess_and_run(program_file, temp_file) + return kore_print(pattern, definition_dir=self.llvm_dir) def prove( self, diff --git a/package/smoke-test.sh b/package/smoke-test.sh index 6be4246..d5c756e 100755 --- a/package/smoke-test.sh +++ b/package/smoke-test.sh @@ -4,7 +4,7 @@ set -euxo pipefail kimp --help -kimp run --verbose --input-file examples/sumto10.imp +kimp run --verbose examples/sumto10.imp kimp prove --verbose examples/specs/imp-sum-spec.k IMP-SUM-SPEC sum-spec From 4955c559f0cd4841fe469c112a8036b495ec7f2b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 13 Nov 2024 15:02:20 +0000 Subject: [PATCH 4/6] Add `--env` to `run` argument parser --- kimp/src/kimp/__main__.py | 18 +++++++++++++----- package/smoke-test.sh | 2 +- 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/kimp/src/kimp/__main__.py b/kimp/src/kimp/__main__.py index 27d8eef..3b7ba72 100644 --- a/kimp/src/kimp/__main__.py +++ b/kimp/src/kimp/__main__.py @@ -64,6 +64,7 @@ def main() -> None: def exec_run( input_file: Path, + env_list: list[list[tuple[str, int]]] | None, definition_dir: Path | None, depth: int | None = None, **kwargs: Any, @@ -71,7 +72,8 @@ def exec_run( definition_dir = find_target('llvm') if definition_dir is None else definition_dir kimp = KImp(definition_dir, definition_dir) pgm = input_file.read_text() - pattern = kimp.pattern(pgm=pgm, env={}) + env = {var: val for assign in env_list for var, val in assign} if env_list else {} + pattern = kimp.pattern(pgm=pgm, env=env) output = kimp.run(pattern, depth=depth) print(kimp.pretty(output)) @@ -173,21 +175,18 @@ def create_argument_parser() -> ArgumentParser: explore_args = ArgumentParser(add_help=False) explore_args.add_argument( '--reinit', - dest='reinit', default=False, action='store_true', help='Reinitialize proof even if it already exists.', ) explore_args.add_argument( '--max-depth', - dest='max_depth', default=100, type=int, help='Max depth of execution', ) explore_args.add_argument( '--max-iterations', - dest='max_iterations', default=1000, type=int, help='Store every Nth state in the CFG for inspection.', @@ -197,11 +196,20 @@ def create_argument_parser() -> ArgumentParser: command_parser = parser.add_subparsers(dest='command', required=True, help='Command to execute') # Run + def env(s: str) -> list[tuple[str, int]]: + return [(var.strip(), int(val)) for var, val in (assign.split('=') for assign in s.split(','))] + run_subparser = command_parser.add_parser('run', help='Run an IMP program', parents=[shared_args]) run_subparser.add_argument('input_file', metavar='INPUT_FILE', type=file_path, help='Path to .imp file') + run_subparser.add_argument( + '--env', + dest='env_list', + action='append', + type=env, + help='Assigments of initial values in form x=0,y=1,...', + ) run_subparser.add_argument( '--depth', - dest='depth', type=int, help='Execute at most DEPTH rewrite steps', ) diff --git a/package/smoke-test.sh b/package/smoke-test.sh index d5c756e..69a4ca1 100755 --- a/package/smoke-test.sh +++ b/package/smoke-test.sh @@ -4,7 +4,7 @@ set -euxo pipefail kimp --help -kimp run --verbose examples/sumto10.imp +kimp run --verbose examples/sumto10.imp --env 'x=0,y=1' --env z=2 kimp prove --verbose examples/specs/imp-sum-spec.k IMP-SUM-SPEC sum-spec From a517d336ec7a369f25c4d2ea2d6dc6286c56dc64 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 13 Nov 2024 15:23:03 +0000 Subject: [PATCH 5/6] Add color support to `run` output --- kimp/src/kimp/__main__.py | 2 +- kimp/src/kimp/kdist/imp-semantics/statements.k | 4 ++-- kimp/src/kimp/kimp.py | 4 ++-- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/kimp/src/kimp/__main__.py b/kimp/src/kimp/__main__.py index 3b7ba72..9b83b36 100644 --- a/kimp/src/kimp/__main__.py +++ b/kimp/src/kimp/__main__.py @@ -75,7 +75,7 @@ def exec_run( env = {var: val for assign in env_list for var, val in assign} if env_list else {} pattern = kimp.pattern(pgm=pgm, env=env) output = kimp.run(pattern, depth=depth) - print(kimp.pretty(output)) + print(kimp.pretty(output, color=True)) def exec_prove( diff --git a/kimp/src/kimp/kdist/imp-semantics/statements.k b/kimp/src/kimp/kdist/imp-semantics/statements.k index 58395eb..3c60f83 100644 --- a/kimp/src/kimp/kdist/imp-semantics/statements.k +++ b/kimp/src/kimp/kdist/imp-semantics/statements.k @@ -45,8 +45,8 @@ module STATEMENTS imports STATEMENTS-RULES configuration - $PGM:Stmt // changed! - $ENV:Map + $PGM:Stmt // changed! + $ENV:Map // changed configuration, need to repeat the variable rule rule diff --git a/kimp/src/kimp/kimp.py b/kimp/src/kimp/kimp.py index dee3433..460643d 100644 --- a/kimp/src/kimp/kimp.py +++ b/kimp/src/kimp/kimp.py @@ -157,10 +157,10 @@ def parse(self, pgm: str) -> Pattern: kore_text = run_process_2(args, input=pgm).stdout return KoreParser(kore_text).pattern() - def pretty(self, pattern: Pattern) -> str: + def pretty(self, pattern: Pattern, color: bool | None = None) -> str: from pyk.kore.tools import kore_print - return kore_print(pattern, definition_dir=self.llvm_dir) + return kore_print(pattern, definition_dir=self.llvm_dir, color=bool(color)) def prove( self, From 3594c0ff970b90ce617a65e9d50d87ec4cd9b714 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 13 Nov 2024 15:36:42 +0000 Subject: [PATCH 6/6] Label each rule --- .../src/kimp/kdist/imp-semantics/statements.k | 23 ++++++++++--------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/kimp/src/kimp/kdist/imp-semantics/statements.k b/kimp/src/kimp/kdist/imp-semantics/statements.k index 3c60f83..529c94b 100644 --- a/kimp/src/kimp/kdist/imp-semantics/statements.k +++ b/kimp/src/kimp/kdist/imp-semantics/statements.k @@ -19,17 +19,18 @@ endmodule module STATEMENTS-RULES imports STATEMENTS-SYNTAX - rule if ( true ) E1 else _ => E1 - rule if ( false ) _ else E2 => E2 + rule [if-true]: if ( true ) E1 else _ => E1 + rule [if-false]: if ( false ) _ else E2 => E2 - rule if ( C ) E => if ( C ) E else {} + rule [if-else]: if ( C ) E => if ( C ) E else {} rule [while]: while ( C ) E - => if ( C ) { - E - while ( C ) E - } + => + if ( C ) { + E + while ( C ) E + } rule [block]: { E } => E ~> {} @@ -45,16 +46,16 @@ module STATEMENTS imports STATEMENTS-RULES configuration - $PGM:Stmt // changed! - $ENV:Map + $PGM:Stmt // changed! + $ENV:Map // changed configuration, need to repeat the variable rule - rule + rule [var]: X:Id => V ... X |-> V ... // assignment rule accesses configuration - rule + rule [assign]: X = V:Value ; => .K ... E => E [ X <- V ] endmodule