Display the final state in exec_prove_legacy (#1936)

* refactor exec_prove_legacy

* Set Version: 1.0.226

---------

Co-authored-by: devops <[email protected]>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.225"
+version = "1.0.226"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__main__.py

@@ -13,7 +13,7 @@
 from pyk.kcfg import KCFG, KCFGExplore
 from pyk.kore.prelude import int_dv
 from pyk.ktool.krun import KRunOutput, _krun
-from pyk.prelude.ml import is_bottom
+from pyk.prelude.ml import is_bottom, is_top
 from pyk.proof import APRProof
 from pyk.proof.show import APRProofShow
 from pyk.proof.tui import APRProofViewer
@@ -199,37 +199,24 @@ def exec_prove_legacy(
     **kwargs: Any,
 ) -> None:
     _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}')
-    md_selector = 'k & ! node'
-
     kevm = KEVM(definition_dir, use_directory=save_directory)
-    args: list[str] = []
-    haskell_args: list[str] = []
-    if claim_labels:
-        args += ['--claims', ','.join(claim_labels)]
-    if exclude_claim_labels:
-        args += ['--exclude', ','.join(exclude_claim_labels)]
-    if debug:
-        args.append('--debug')
-    if debugger:
-        args.append('--debugger')
-    if branching_allowed:
-        args += ['--branching-allowed', f'{branching_allowed}']
-    if max_counterexamples:
-        haskell_args += ['--max-counterexamples', f'{max_counterexamples}']
-    if bug_report:
-        haskell_args += ['--bug-report', f'kevm-bug-{spec_file.name.rstrip("-spec.k")}']
-    if haskell_backend_args:
-        haskell_args += list(haskell_backend_args)
-
-    kevm.prove(
+    final_state = kevm.prove_legacy(
         spec_file=spec_file,
-        spec_module_name=spec_module,
-        args=args,
-        include_dirs=[Path(i) for i in includes],
-        md_selector=md_selector,
-        haskell_args=haskell_args,
-        depth=max_depth,
+        includes=includes,
+        bug_report=bug_report,
+        spec_module=spec_module,
+        claim_labels=claim_labels,
+        exclude_claim_labels=exclude_claim_labels,
+        debug=debug,
+        debugger=debugger,
+        max_depth=max_depth,
+        max_counterexamples=max_counterexamples,
+        branching_allowed=branching_allowed,
+        haskell_backend_args=haskell_backend_args,
     )
+    print(kevm.pretty_print(final_state))
+    if not is_top(final_state):
+        raise SystemExit(1)
 
 
 def exec_prove(

kevm-pyk/src/kevm_pyk/kevm.py

@@ -1,6 +1,7 @@
 from __future__ import annotations
 
 import logging
+from pathlib import Path
 from typing import TYPE_CHECKING
 
 from pyk.cterm import CTerm
@@ -19,7 +20,6 @@
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
-    from pathlib import Path
     from typing import Final
 
     from pyk.kast import KInner
@@ -390,6 +390,52 @@ def _replace(term: KInner) -> KInner:
 
         return CTerm(config=bottom_up(_replace, cterm.config), constraints=cterm.constraints)
 
+    def prove_legacy(
+        self,
+        spec_file: Path,
+        includes: Iterable[str] = (),
+        bug_report: bool = False,
+        spec_module: str | None = None,
+        claim_labels: Iterable[str] | None = None,
+        exclude_claim_labels: Iterable[str] = (),
+        debug: bool = False,
+        debugger: bool = False,
+        max_depth: int | None = None,
+        max_counterexamples: int | None = None,
+        branching_allowed: int | None = None,
+        haskell_backend_args: Iterable[str] = (),
+    ) -> KInner:
+        md_selector = 'k & ! node'
+        args: list[str] = []
+        haskell_args: list[str] = []
+        if claim_labels:
+            args += ['--claims', ','.join(claim_labels)]
+        if exclude_claim_labels:
+            args += ['--exclude', ','.join(exclude_claim_labels)]
+        if debug:
+            args.append('--debug')
+        if debugger:
+            args.append('--debugger')
+        if branching_allowed:
+            args += ['--branching-allowed', f'{branching_allowed}']
+        if max_counterexamples:
+            haskell_args += ['--max-counterexamples', f'{max_counterexamples}']
+        if bug_report:
+            haskell_args += ['--bug-report', f'kevm-bug-{spec_file.name.rstrip("-spec.k")}']
+        if haskell_backend_args:
+            haskell_args += list(haskell_backend_args)
+
+        final_state = self.prove(
+            spec_file=spec_file,
+            spec_module_name=spec_module,
+            args=args,
+            include_dirs=[Path(i) for i in includes],
+            md_selector=md_selector,
+            haskell_args=haskell_args,
+            depth=max_depth,
+        )
+        return final_state
+
 
 class KEVMNodePrinter(NodePrinter):
     kevm: KEVM

package/debian/changelog

@@ -1,4 +1,4 @@
-kevm (1.0.225) unstable; urgency=medium
+kevm (1.0.226) unstable; urgency=medium
 
   * Initial Release.
 

package/version

@@ -1 +1 @@
-1.0.225
+1.0.226