Refactors to simplify import structure (#1019)

* src/kontrol/{utils,solc_to_k,state_record,prove}: move hex_string_to_int from solc_to_k to utils

* kontrol/cli: direct imports instead of through prove

* kontrol/{options,cli,__main__}: remove kontrol compile command

* kontrol/solc_to_k: remove now unused method

* kontrol/{cli,options,foundry,__main__}: remove kontrol to-dot command

* kontrol/{foundry,__main__}: factor out foundry_view command similar to foundry_show

* kontrol/{foundry,__main__}: demote hevm import to foundry instead of __main__ with refactor

* kontrol/{hevm,foundry}: inline Hevm.help_info into Foundry.help_info

* kontrol/{hevm,prove,foundry}: inline Hevm.{success,fail} directly into Foundry class

* kontrol/foundry: use Foundry directly for parsing instead of buliding foundry_node_printer

Author: ehildenb

src/kontrol/__main__.py

@@ -1,6 +1,5 @@
 from __future__ import annotations
 
-import json
 import logging
 import sys
 from collections.abc import Iterable
@@ -9,7 +8,6 @@
 from pyk.cli.pyk import parse_toml_args
 from pyk.cterm.symbolic import CTermSMTError
 from pyk.proof.reachability import APRFailureInfo, APRProof
-from pyk.proof.tui import APRProofViewer
 
 from . import VERSION
 from .cli import _create_argument_parser, generate_options, get_argument_type_setter, get_option_string_destination
@@ -20,7 +18,6 @@
     foundry_list,
     foundry_merge_nodes,
     foundry_minimize_proof,
-    foundry_node_printer,
     foundry_refute_node,
     foundry_remove_node,
     foundry_section_edge,
@@ -29,30 +26,25 @@
     foundry_split_node,
     foundry_state_load,
     foundry_step_node,
-    foundry_to_dot,
     foundry_unrefute_node,
+    foundry_view,
     init_project,
     read_recorded_state_diff,
     read_recorded_state_dump,
 )
-from .hevm import Hevm
 from .kompile import foundry_kompile
 from .prove import foundry_prove
-from .solc import CompilationUnit
-from .solc_to_k import solc_compile
 from .utils import _LOG_FORMAT, _rv_blue, _rv_yellow, check_k_version, config_file_path, console, loglevel
 
 if TYPE_CHECKING:
     from pathlib import Path
     from typing import Final, TypeVar
 
-    from pyk.kcfg.tui import KCFGElem
     from pyk.utils import BugReport
 
     from .options import (
         BuildOptions,
         CleanOptions,
-        CompileOptions,
         GetModelOptions,
         InitOptions,
         ListOptions,
@@ -67,7 +59,6 @@
         SimplifyNodeOptions,
         SplitNodeOptions,
         StepNodeOptions,
-        ToDotOptions,
         UnrefuteNodeOptions,
         VersionOptions,
         ViewKcfgOptions,
@@ -142,11 +133,6 @@ def exec_version(options: VersionOptions) -> None:
     print(f'Kontrol version: {VERSION}')
 
 
-def exec_compile(options: CompileOptions) -> None:
-    res = solc_compile(options.contract_file)
-    print(json.dumps(res))
-
-
 def exec_build(options: BuildOptions) -> None:
     _LOGGER.debug(options)
 
@@ -228,7 +214,7 @@ def exec_prove(options: ProveOptions) -> None:
             if isinstance(proof, APRProof) and isinstance(proof.failure_info, APRFailureInfo):
                 failure_log = proof.failure_info
             if options.failure_info and failure_log is not None:
-                log = failure_log.print() + (Foundry.help_info() if not options.hevm else Hevm.help_info(proof.id))
+                log = failure_log.print() + Foundry.help_info(proof.id, options.hevm)
                 for line in log:
                     print(line)
             refuted_nodes = list(proof.node_refutations.keys())
@@ -281,13 +267,6 @@ def exec_split_node(options: SplitNodeOptions) -> None:
     print(f'Node {options.node} has been split into {node_ids} on condition {options.branch_condition}.')
 
 
-def exec_to_dot(options: ToDotOptions) -> None:
-    foundry_to_dot(
-        foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints),
-        options=options,
-    )
-
-
 def exec_list(options: ListOptions) -> None:
     stats = foundry_list(foundry=_load_foundry(options.foundry_root, add_enum_constraints=options.enum_constraints))
     print('\n'.join(stats))
@@ -297,18 +276,7 @@ def exec_view_kcfg(options: ViewKcfgOptions) -> None:
     foundry = _load_foundry(
         options.foundry_root, use_hex_encoding=options.use_hex_encoding, add_enum_constraints=options.enum_constraints
     )
-    test_id = foundry.get_test_id(options.test, options.version)
-    contract_name, _ = test_id.split('.')
-    proof = foundry.get_apr_proof(test_id)
-
-    compilation_unit = CompilationUnit.load_build_info(foundry.build_info)
-
-    def _custom_view(elem: KCFGElem) -> Iterable[str]:
-        return foundry.custom_view(contract_name, elem, compilation_unit)
-
-    node_printer = foundry_node_printer(foundry, contract_name, proof)
-    viewer = APRProofViewer(proof, foundry.kevm, node_printer=node_printer, custom_view=_custom_view)
-    viewer.run()
+    foundry_view(foundry, options)
 
 
 def exec_minimize_proof(options: MinimizeProofOptions) -> None:

src/kontrol/cli.py

@@ -13,7 +13,7 @@
 from .options import (
     BuildOptions,
     CleanOptions,
-    CompileOptions,
+    ConfigType,
     GetModelOptions,
     InitOptions,
     ListOptions,
@@ -28,12 +28,11 @@
     SimplifyNodeOptions,
     SplitNodeOptions,
     StepNodeOptions,
-    ToDotOptions,
     UnrefuteNodeOptions,
     VersionOptions,
     ViewKcfgOptions,
 )
-from .prove import ConfigType, parse_test_version_tuple
+from .utils import parse_test_version_tuple
 
 if TYPE_CHECKING:
     from collections.abc import Callable
@@ -49,14 +48,12 @@ def generate_options(args: dict[str, Any]) -> LoggingOptions:
     options = {
         'load-state': LoadStateOptions(args),
         'version': VersionOptions(args),
-        'compile': CompileOptions(args),
         'build': BuildOptions(args),
         'prove': ProveOptions(args),
         'show': ShowOptions(args),
         'refute-node': RefuteNodeOptions(args),
         'unrefute-node': UnrefuteNodeOptions(args),
         'split-node': SplitNodeOptions(args),
-        'to-dot': ToDotOptions(args),
         'list': ListOptions(args),
         'view-kcfg': ViewKcfgOptions(args),
         'remove-node': RemoveNodeOptions(args),
@@ -80,14 +77,12 @@ def get_option_string_destination(command: str, option_string: str) -> str:
     options = {
         'load-state': LoadStateOptions.from_option_string(),
         'version': VersionOptions.from_option_string(),
-        'compile': CompileOptions.from_option_string(),
         'build': BuildOptions.from_option_string(),
         'prove': ProveOptions.from_option_string(),
         'show': ShowOptions.from_option_string(),
         'refute-node': RefuteNodeOptions.from_option_string(),
         'unrefute-node': UnrefuteNodeOptions.from_option_string(),
         'split-node': SplitNodeOptions.from_option_string(),
-        'to-dot': ToDotOptions.from_option_string(),
         'list': ListOptions.from_option_string(),
         'view-kcfg': ViewKcfgOptions.from_option_string(),
         'remove-node': RemoveNodeOptions.from_option_string(),
@@ -109,14 +104,12 @@ def get_argument_type_setter(command: str, option_string: str) -> Callable[[str]
     options = {
         'load-state': LoadStateOptions.get_argument_type(),
         'version': VersionOptions.get_argument_type(),
-        'compile': CompileOptions.get_argument_type(),
         'build': BuildOptions.get_argument_type(),
         'prove': ProveOptions.get_argument_type(),
         'show': ShowOptions.get_argument_type(),
         'refute-node': RefuteNodeOptions.get_argument_type(),
         'unrefute-node': UnrefuteNodeOptions.get_argument_type(),
         'split-node': SplitNodeOptions.get_argument_type(),
-        'to-dot': ToDotOptions.get_argument_type(),
         'list': ListOptions.get_argument_type(),
         'view-kcfg': ViewKcfgOptions.get_argument_type(),
         'remove-node': RemoveNodeOptions.get_argument_type(),
@@ -249,9 +242,6 @@ def parse(s: str) -> list[T]:
 
     command_parser.add_parser('version', help='Print out version of Kontrol command.')
 
-    solc_args = command_parser.add_parser('compile', help='Generate combined JSON with solc compilation results.')
-    solc_args.add_argument('contract_file', type=file_path, help='Path to contract file.')
-
     build = command_parser.add_parser(
         'build',
         help='Kompile K definition corresponding to given output directory.',
@@ -644,17 +634,6 @@ def parse(s: str) -> list[T]:
         help='Run KCFG minimization routine before displaying it.',
     )
 
-    command_parser.add_parser(
-        'to-dot',
-        help='Dump the given CFG for the test as DOT for visualization.',
-        parents=[
-            kontrol_cli_args.foundry_test_args,
-            kontrol_cli_args.logging_args,
-            kontrol_cli_args.foundry_args,
-            config_args.config_args,
-        ],
-    )
-
     command_parser.add_parser(
         'list',
         help='List information about CFGs on disk',

src/kontrol/foundry.py

@@ -44,6 +44,7 @@
 from pyk.proof.proof import Proof
 from pyk.proof.reachability import APRFailureInfo, APRProof
 from pyk.proof.show import APRProofNodePrinter, APRProofShow
+from pyk.proof.tui import APRProofViewer
 from pyk.utils import ensure_dir_path, hash_str, run_process_2, single, unique
 
 from . import VERSION
@@ -86,8 +87,8 @@
         SimplifyNodeOptions,
         SplitNodeOptions,
         StepNodeOptions,
-        ToDotOptions,
         UnrefuteNodeOptions,
+        ViewKcfgOptions,
     )
 
 _LOGGER: Final = logging.getLogger(__name__)
@@ -670,6 +671,14 @@ def success(s: KInner, dst: KInner, r: KInner, c: KInner, e1: KInner, e2: KInner
     def fail(s: KInner, dst: KInner, r: KInner, c: KInner, e1: KInner, e2: KInner) -> KApply:
         return notBool(Foundry.success(s, dst, r, c, e1, e2))
 
+    @staticmethod
+    def hevm_success(s: KInner, dst: KInner, out: KInner) -> KApply:
+        return KApply('hevm_success', [s, dst, out])
+
+    @staticmethod
+    def hevm_fail(s: KInner, dst: KInner) -> KApply:
+        return KApply('hevm_fail', [s, dst])
+
     # address(uint160(uint256(keccak256("foundry default caller"))))
 
     @staticmethod
@@ -735,13 +744,28 @@ def symbolic_account(prefix: str, program: KInner, storage: KInner | None = None
         )
 
     @staticmethod
-    def help_info() -> list[str]:
+    def help_info(proof_id: str, hevm: bool) -> list[str]:
         res_lines: list[str] = []
-        res_lines.append('')
-        res_lines.append('See `foundry_success` predicate for more information:')
-        res_lines.append(
-            'https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/foundry.md#foundry-success-predicate'
-        )
+        if hevm:
+            _, test = proof_id.split('.')
+            if not any(test.startswith(prefix) for prefix in ['testFail', 'checkFail', 'proveFail']):
+                res_lines.append('')
+                res_lines.append('See `hevm_success` predicate for more information:')
+                res_lines.append(
+                    'https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/hevm.md#hevm-success-predicate'
+                )
+            else:
+                res_lines.append('')
+                res_lines.append('See `hevm_fail` predicate for more information:')
+                res_lines.append(
+                    'https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/hevm.md#hevm-fail-predicate'
+                )
+        else:
+            res_lines.append('')
+            res_lines.append('See `foundry_success` predicate for more information:')
+            res_lines.append(
+                'https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/foundry.md#foundry-success-predicate'
+            )
         res_lines.append('')
         res_lines.append('Access documentation for Kontrol at https://docs.runtimeverification.com/kontrol')
         return res_lines
@@ -990,7 +1014,7 @@ def foundry_show(
             extra_module=foundry.load_lemmas(options.lemmas),
         ) as kcfg_explore:
             res_lines += print_failure_info(proof, kcfg_explore, options.counterexample_info)
-            res_lines += Foundry.help_info()
+            res_lines += Foundry.help_info(proof.id, False)
 
     if options.to_kevm_claims or options.to_kevm_rules:
         _foundry_labels = [
@@ -1070,16 +1094,19 @@ def _collect_klabel(_k: KInner) -> None:
     return '\n'.join([line.rstrip() for line in res_lines])
 
 
-def foundry_to_dot(foundry: Foundry, options: ToDotOptions) -> None:
-    dump_dir = foundry.proofs_dir / 'dump'
+def foundry_view(foundry: Foundry, options: ViewKcfgOptions) -> None:
     test_id = foundry.get_test_id(options.test, options.version)
-    contract_name, _ = single(foundry.matching_tests([options.test])).split('.')
+    contract_name, _ = test_id.split('.')
     proof = foundry.get_apr_proof(test_id)
 
-    node_printer = foundry_node_printer(foundry, contract_name, proof)
-    proof_show = APRProofShow(foundry.kevm, node_printer=node_printer)
+    compilation_unit = CompilationUnit.load_build_info(foundry.build_info)
+
+    def _custom_view(elem: KCFGElem) -> Iterable[str]:
+        return foundry.custom_view(contract_name, elem, compilation_unit)
 
-    proof_show.dump(proof, dump_dir, dot=True)
+    node_printer = foundry_node_printer(foundry, contract_name, proof)
+    viewer = APRProofViewer(proof, foundry.kevm, node_printer=node_printer, custom_view=_custom_view)
+    viewer.run()
 
 
 def foundry_list(foundry: Foundry) -> list[str]:
@@ -1212,8 +1239,7 @@ def foundry_split_node(
     proof = foundry.get_apr_proof(test_id)
 
     token = KToken(options.branch_condition, 'Bool')
-    node_printer = foundry_node_printer(foundry, contract_name, proof)
-    parsed_condition = node_printer.kprint.parse_token(token, as_rule=True)
+    parsed_condition = foundry.kevm.parse_token(token, as_rule=True)
 
     split_nodes = proof.kcfg.split_on_constraints(
         options.node, [mlEqualsTrue(parsed_condition), mlEqualsFalse(parsed_condition)]