bin/kevm, kevm-pyk/__main__: add foundry-list command for seeing KCFG information

Author: ehildenb

bin/kevm

@@ -298,6 +298,10 @@ run_foundry_show_cfg() {
     run_kevm_pyk foundry-show-cfg "$@"
 }
 
+run_foundry_list() {
+    run_kevm_pyk foundry-list "$@"
+}
+
 # Main
 # ----
 
@@ -313,8 +317,10 @@ if [[ "$run_command" == 'help' ]] || [[ "$run_command" == '--help' ]] ; then
                ${KEVM} kompile      [--backend (java|llvm|haskell)]           [--profile|--debug]             <main> <K arg>*
                ${KEVM} klab-view                                              [--profile|--debug]             <spec>
                ${KEVM} solc-to-k                                              [--profile|--debug]             <sol-file> <contract-name> <solc-arg>*
-               ${KEVM} foundry-kompile
-               ${KEVM} foundry-prove
+               ${KEVM} foundry-list         # see dedicated help menu
+               ${KEVM} foundry-cfg          # see dedicated help menu
+               ${KEVM} foundry-kompile      # see dedicated help menu
+               ${KEVM} foundry-prove        # see dedicated help menu
 
                ${KEVM} [help|--help|version|--version]
 
@@ -438,7 +444,7 @@ if ${pyk}; then
 fi
 
 # get the run file
-if [[ "${run_command}" != 'foundry-kompile' ]] && [[ "${run_command}" != 'foundry-prove' ]] && [[ "${run_command}" != 'foundry-show-cfg' ]]; then
+if [[ "${run_command}" != 'foundry-kompile' ]] && [[ "${run_command}" != 'foundry-prove' ]] && [[ "${run_command}" != 'foundry-show-cfg' ]] && [[ "${run_command}" != 'foundry-list' ]]; then
     run_file="$1" ; shift
     if [[ "${run_file}" == '-' ]]; then
         tmp_input="$(mktemp)"
@@ -471,5 +477,6 @@ case "$run_command-$backend" in
     foundry-kompile-*                         ) run_foundry_kompile  "$@" ;;
     foundry-prove-*                           ) run_foundry_prove    "$@" ;;
     foundry-show-cfg-*                        ) run_foundry_show_cfg "$@" ;;
+    foundry-list-*                            ) run_foundry_list     "$@" ;;
     *) ${KEVM} help ; fatal "Unknown command on backend: $run_command $backend" ;;
 esac

kevm-pyk/src/kevm_pyk/__main__.py

@@ -492,6 +492,30 @@ def exec_foundry_show_cfg(
         print(f'\n\nState Delta {node_id_1} => {node_id_2}:\n\n{foundry.pretty_print(config_delta)}\n')
 
 
+def exec_foundry_list(
+    profile: bool,
+    foundry_out: Path,
+    details: bool = True,
+    **kwargs: Any,
+) -> None:
+    kcfgs_dir = foundry_out / 'kcfgs'
+    pattern = '*.json'
+    paths = kcfgs_dir.glob(pattern)
+    for kcfg_file in paths:
+        with open(kcfg_file, 'r') as kf:
+            kcfg = KCFG.from_dict(json.loads(kf.read()))
+        total_nodes = len(kcfg.nodes)
+        frontier_nodes = len(kcfg.frontier)
+        stuck_nodes = len(kcfg.stuck)
+        proven = 'passed' if frontier_nodes + stuck_nodes == 0 else 'failed'
+        print(f'{kcfg_file}: {proven}')
+        if details:
+            print(f'    nodes: {total_nodes}')
+            print(f'    frontier: {frontier_nodes}')
+            print(f'    stuck: {stuck_nodes}')
+            print()
+
+
 def exec_run(
     definition_dir: Path,
     profile: bool,
@@ -790,6 +814,17 @@ def parse(s: str) -> List[T]:
         '--no-minimize', dest='minimize', action='store_false', help='Do not minimize output.'
     )
 
+    foundry_list_args = command_parser.add_parser(
+        'foundry-list',
+        help='List information about KCFGs on disk',
+        parents=[shared_args, k_args],
+    )
+    foundry_list_args.add_argument('foundry_out', type=dir_path, help='Path to Foundry output directory.')
+    foundry_list_args.add_argument(
+        '--details', dest='details', default=True, action='store_true', help='Information about progress on each KCFG.'
+    )
+    foundry_list_args.add_argument('--no-details', dest='details', action='store_false', help='Just list the KCFGs.')
+
     return parser