Re-implement kimp (#8)

* Update pyk * Work in upgrading pyk * Implement `kimp run` * Implement `kimp prove`, drop dead code * Fix sum spec * . -> .K * Use `statements.k` in `kimp prove` * Update `pyk`
runtimeverification · Mar 5, 2024 · 377448f · 377448f
1 parent 2888d35
commit 377448f
Show file tree

Hide file tree

Showing 8 changed files with 556 additions and 837 deletions.
diff --git a/kimp/k-src/imp-verification.k b/kimp/k-src/imp-verification.k
@@ -1,4 +1,4 @@
-requires "calls.k"
+requires "statements.k"
 
 module IMP-VERIFICATION-SYNTAX
     imports ID-SYNTAX
@@ -13,7 +13,7 @@ endmodule
 
 module IMP-VERIFICATION
     imports IMP-VERIFICATION-SYNTAX
-    imports CALLS
+    imports STATEMENTS
 
     // inequality sign normalization
     rule          A  >Int B  => B  <Int A [simplification]

diff --git a/kimp/kbuild.toml b/kimp/kbuild.toml
@@ -5,9 +5,9 @@ source = "k-src"
 
 [targets.llvm]
 backend = "llvm"
-main-file = "imp.k"
-main-module = "IMP"
-syntax-module = "IMP-SYNTAX"
+main-file = "statements.k"
+main-module = "STATEMENTS"
+syntax-module = "STATEMENTS-SYNTAX"
 
 [targets.haskell]
 backend = "haskell"

diff --git a/kimp/poetry.lock b/kimp/poetry.lock
diff --git a/kimp/pyproject.toml b/kimp/pyproject.toml
@@ -12,7 +12,7 @@ authors = [
 
 [tool.poetry.dependencies]
 python = "^3.10"
-pyk = { git = "https://github.com/runtimeverification/pyk.git", branch="subproofs" }
+pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.679" }
 
 [tool.poetry.scripts]
 kimp = "kimp.__main__:main"

diff --git a/kimp/src/kimp/__main__.py b/kimp/src/kimp/__main__.py
@@ -6,8 +6,8 @@
 from pathlib import Path
 from typing import TYPE_CHECKING, Any, Final
 
-from pyk.cli_utils import dir_path, file_path
-from pyk.ktool.kprint import KAstInput, KAstOutput
+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
@@ -46,23 +46,6 @@ def main() -> None:
     execute(**vars(args))
 
 
-def exec_parse(
-    input_file: str,
-    definition_dir: str,
-    input: str = 'program',
-    output: str = 'kore',
-    **kwargs: Any,
-) -> None:
-    kast_input = KAstInput[input.upper()]
-    kast_output = KAstOutput[output.upper()]
-
-    kimp = KIMP(definition_dir, definition_dir)
-    proc_res = kimp.parse_program_raw(input_file, input=kast_input, output=kast_output)
-
-    if output != KAstOutput.NONE:
-        print(proc_res.stdout)
-
-
 def exec_run(
     input_file: str,
     definition_dir: str,
@@ -72,6 +55,8 @@ def exec_run(
 ) -> None:
     krun_output = KRunOutput[output.upper()]
 
+    definition_dir = str(kbuild_definition_dir('llvm'))
+
     kimp = KIMP(definition_dir, definition_dir)
 
     try:
@@ -93,14 +78,13 @@ def exec_prove(
     spec_file: str,
     spec_module: str,
     claim_id: str,
-    # output: str = 'none',
     max_iterations: int,
     max_depth: int,
-    reinit: bool,
     ignore_return_code: bool = False,
-    # output: str = 'none',
     **kwargs: Any,
 ) -> None:
+    definition_dir = str(kbuild_definition_dir('haskell'))
+
     kimp = KIMP(definition_dir, definition_dir)
 
     try:
@@ -110,38 +94,12 @@ def exec_prove(
             claim_id=claim_id,
             max_iterations=max_iterations,
             max_depth=max_depth,
-            reinit=reinit,
+            includes=['k-src'],  # TODO this needs to be more rubust
         )
     except ValueError as err:
         _LOGGER.critical(err.args)
-        exit(1)
-    except RuntimeError as err:
-        if ignore_return_code:
-            msg, stdout, stderr = err.args
-            print(stdout)
-            print(stderr)
-            print(msg)
-        else:
-            raise
-
-
-def exec_summarize(
-    definition_dir: str,
-    spec_file: str,
-    spec_module: str,
-    claim_id: str,
-    max_iterations: int = 20,
-    ignore_return_code: bool = False,
-    # output: str = 'none',
-    **kwargs: Any,
-) -> None:
-    kimp = KIMP(definition_dir, definition_dir)
-
-    try:
-        kimp.summarize(spec_file=spec_file, spec_module=spec_module, claim_id=claim_id, max_iterations=max_iterations)
-    except ValueError as err:
-        _LOGGER.critical(err.args)
-        exit(1)
+        # exit(1)
+        raise
     except RuntimeError as err:
         if ignore_return_code:
             msg, stdout, stderr = err.args
@@ -152,129 +110,26 @@ def exec_summarize(
             raise
 
 
-def exec_bmc_prove(
-    definition_dir: str,
-    spec_file: str,
-    spec_module: str,
-    claim_id: str,
-    max_iterations: int,
-    max_depth: int,
-    reinit: bool,
-    bmc_depth: int,
-    # output: str = 'none',
-    ignore_return_code: bool = False,
-    **kwargs: Any,
-) -> None:
-    kimp = KIMP(definition_dir, definition_dir)
-
-    try:
-        kimp.bmc_prove(
-            spec_file=spec_file,
-            spec_module=spec_module,
-            claim_id=claim_id,
-            max_iterations=max_iterations,
-            max_depth=max_depth,
-            reinit=reinit,
-            bmc_depth=bmc_depth,
-        )
-    except ValueError as err:
-        _LOGGER.critical(err.args)
-        exit(1)
-    except RuntimeError as err:
-        if ignore_return_code:
-            msg, stdout, stderr = err.args
-            print(stdout)
-            print(stderr)
-            print(msg)
-        else:
-            raise
+# def exec_show_kcfg(
+#     definition_dir: str,
+#     spec_module: str,
+#     claim_id: str,
+#     to_module: bool = False,
+#     inline_nodes: bool = False,
+#     **kwargs: Any,
+# ) -> None:
+#     kimp = KIMP(definition_dir, definition_dir)
+#     kimp.show_kcfg(spec_module, claim_id, to_module=to_module, inline_nodes=inline_nodes)
 
 
-def exec_eq_prove(
-    definition_dir: str,
-    proof_id: str,
-    # output: str = 'none',
-    ignore_return_code: bool = False,
-    **kwargs: Any,
-) -> None:
-    kimp = KIMP(definition_dir, definition_dir)
-
-    try:
-        kimp.eq_prove(proof_id)
-    except RuntimeError as err:
-        if ignore_return_code:
-            msg, stdout, stderr = err.args
-            print(stdout)
-            print(stderr)
-            print(msg)
-        else:
-            raise
-
-
-def exec_refute_node(
-    definition_dir: str,
-    spec_module: str,
-    claim_id: str,
-    node: str,
-    # output: str = 'none',
-    ignore_return_code: bool = False,
-    **kwargs: Any,
-) -> None:
-    kimp = KIMP(definition_dir, definition_dir)
-
-    try:
-        kimp.kcfg_refute_node(spec_module=spec_module, claim_id=claim_id, node_short_hash=node)
-    except RuntimeError as err:
-        if ignore_return_code:
-            msg, stdout, stderr = err.args
-            print(stdout)
-            print(stderr)
-            print(msg)
-        else:
-            raise
-
-
-def exec_show_kcfg(
-    definition_dir: str,
-    spec_module: str,
-    claim_id: str,
-    to_module: bool = False,
-    inline_nodes: bool = False,
-    **kwargs: Any,
-) -> None:
-    kimp = KIMP(definition_dir, definition_dir)
-    kimp.show_kcfg(spec_module, claim_id, to_module=to_module, inline_nodes=inline_nodes)
-
-
-def exec_view_kcfg(
-    definition_dir: str,
-    spec_module: str,
-    claim_id: str,
-    **kwargs: Any,
-) -> None:
-    kimp = KIMP(definition_dir, definition_dir)
-    kimp.view_kcfg(spec_module, claim_id)
-
-
-def exec_show_refutation(
-    definition_dir: str,
-    spec_module: str,
-    claim_id: str,
-    node: str,
-    **kwargs: Any,
-) -> None:
-    kimp = KIMP(definition_dir, definition_dir)
-    kimp.show_refutation(spec_module, claim_id, node=node)
-
-
-def exec_kcfg_to_dot(
-    definition_dir: str,
-    spec_module: str,
-    claim_id: str,
-    **kwargs: Any,
-) -> None:
-    kimp = KIMP(definition_dir, definition_dir)
-    kimp.kcfg_to_dot(spec_module, claim_id)
+# def exec_view_kcfg(
+#     definition_dir: str,
+#     spec_module: str,
+#     claim_id: str,
+#     **kwargs: Any,
+# ) -> None:
+#     kimp = KIMP(definition_dir, definition_dir)
+#     kimp.view_kcfg(spec_module, claim_id)
 
 
 def create_argument_parser() -> ArgumentParser:
@@ -286,7 +141,6 @@ def create_argument_parser() -> ArgumentParser:
         '--definition-dir',
         dest='definition_dir',
         nargs='?',
-        default=kbuild_definition_dir('haskell'),
         type=dir_path,
         help='Path to compiled K definition to use.',
     )
@@ -373,7 +227,7 @@ def create_argument_parser() -> ArgumentParser:
         '--output',
         dest='output',
         type=str,
-        default='kast',
+        default='pretty',
         help='Output mode',
         choices=['pretty', 'program', 'json', 'kore', 'kast', 'none'],
         required=False,