kevm-pyk/__main__: better logging/error messages

Author: ehildenb

kevm-pyk/src/kevm_pyk/__main__.py

@@ -371,7 +371,7 @@ def prove_it(id_and_cfg: Tuple[str, Tuple[KCFG, Path]]) -> bool:
             iterations += 1
             curr_node = cfg.frontier[0]
             cfg.add_expanded(curr_node.id)
-            _LOGGER.info(f'Advancing proof from node: {shorten_hashes(curr_node.id)}')
+            _LOGGER.info(f'Advancing proof from node {cfgid}: {shorten_hashes(curr_node.id)}')
             edge = KCFG.Edge(curr_node, target_node, mlTop(), -1)
             claim = edge.to_claim()
             claim_id = f'gen-{curr_node.id}-to-{target_node.id}'
@@ -382,35 +382,35 @@ def prove_it(id_and_cfg: Tuple[str, Tuple[KCFG, Path]]) -> bool:
             if result == mlTop():
                 cfg.create_edge(curr_node.id, target_node.id, mlTop(), depth)
                 _LOGGER.info(
-                    f'Target state reached at depth {depth}, inserted edge from {shorten_hashes((curr_node.id))} to {shorten_hashes((target_node.id))}.'
+                    f'Target state reached at depth {depth} for {cfgid}: {shorten_hashes((curr_node.id, target_node.id))}.'
                 )
 
             else:
                 next_state = CTerm(sanitize_config(foundry.definition, result))
                 next_node = cfg.get_or_create_node(next_state)
                 if next_node != curr_node:
-                    _LOGGER.info(f'Found basic block at depth {depth}: {shorten_hashes((curr_node.id, next_node.id))}.')
+                    _LOGGER.info(f'Found basic block at depth {depth} for {cfgid}: {shorten_hashes((curr_node.id, next_node.id))}.')
                     cfg.create_edge(curr_node.id, next_node.id, mlTop(), depth)
 
                 if KEVM.is_terminal(next_node.cterm):
                     cfg.add_expanded(next_node.id)
-                    _LOGGER.info(f'Terminal node: {shorten_hashes((curr_node.id))}.')
+                    _LOGGER.info(f'Terminal node {cfgid}: {shorten_hashes((curr_node.id))}.')
 
                 elif branching:
                     branches = KEVM.extract_branches(next_state)
                     if not branches:
                         raise ValueError(
-                            f'Could not extract branch condition:\n{foundry.pretty_print(minimize_term(result))}'
+                            f'Could not extract branch condition {cfgid}:\n{foundry.pretty_print(minimize_term(result))}'
                         )
                     cfg.add_expanded(next_node.id)
                     _LOGGER.info(
-                        f'Found {len(list(branches))} branches at depth {depth}: {[foundry.pretty_print(b) for b in branches]}'
+                        f'Found {len(list(branches))} branches at depth {depth} for {cfgid}: {[foundry.pretty_print(b) for b in branches]}'
                     )
                     for branch in branches:
                         branch_cterm = next_state.add_constraint(branch)
                         branch_node = cfg.get_or_create_node(branch_cterm)
                         cfg.create_edge(next_node.id, branch_node.id, branch, 0)
-                        _LOGGER.info(f'Made split: {shorten_hashes((next_node.id, branch_node.id))}')
+                        _LOGGER.info(f'Made split for {cfgid}: {shorten_hashes((next_node.id, branch_node.id))}')
                         # TODO: have to store case splits as rewrites because of how frontier is handled for covers
                         # cfg.create_cover(branch_node.id, next_node.id)
                         # _LOGGER.info(f'Made cover: {shorten_hashes((branch_node.id, next_node.id))}')