kevm-pyk/__main__: no need to sanitize configuration

Author: ehildenb

kevm-pyk/src/kevm_pyk/__main__.py

@@ -372,13 +372,17 @@ def prove_it(id_and_cfg: Tuple[str, Tuple[KCFG, Path]]) -> bool:
             iterations += 1
             curr_node = cfg.frontier[0]
 
+            _LOGGER.info(
+                f'Checking subsumption into target state {cfgid}: {shorten_hashes((curr_node.id, target_node.id))}'
+            )
             if subst := foundry.check_implication(curr_node.cterm, target_node.cterm):
                 cfg.create_cover(curr_node.id, target_node.id, witness=(subst, mlTop()))
                 _LOGGER.info(f'Subsumed into target node: {shorten_hashes((curr_node.id, target_node.id))}')
                 continue
 
             cfg.add_expanded(curr_node.id)
 
+            _LOGGER.info(f'Checking terminal node {cfgid}: {shorten_hashes((curr_node.id))}')
             if KEVM.is_terminal(curr_node.cterm):
                 _LOGGER.info(f'Terminal node {cfgid}: {shorten_hashes((curr_node.id))}.')
                 continue
@@ -389,28 +393,27 @@ def prove_it(id_and_cfg: Tuple[str, Tuple[KCFG, Path]]) -> bool:
                 _LOGGER.info(f'Found stuck node {cfgid}: {shorten_hashes(curr_node.id)}')
                 continue
 
-            # next_state = CTerm(sanitize_config(foundry.definition, cterm.kast))
-            next_state = cterm
-            next_node = cfg.get_or_create_node(next_state)
+            next_node = cfg.get_or_create_node(cterm)
+            cfg.create_edge(curr_node.id, next_node.id, mlTop(), depth)
             _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 len(next_cterms) == 0:
                 continue
 
             if len(next_cterms) == 1:
                 raise ValueError(f'Found a single successor cterm: {(depth, cterm, next_cterms)}')
 
+            _LOGGER.info(f'Extracting branchings from node in {cfgid}: {shorten_hashes((curr_node.id))}')
             cfg.add_expanded(next_node.id)
-            branches = KEVM.extract_branches(next_state)
+            branches = KEVM.extract_branches(cterm)
             if len(list(branches)) > 0:
                 _LOGGER.info(
                     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_cterm = cterm.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 for {cfgid}: {shorten_hashes((next_node.id, branch_node.id))}')
@@ -419,9 +422,7 @@ def prove_it(id_and_cfg: Tuple[str, Tuple[KCFG, Path]]) -> bool:
                     # _LOGGER.info(f'Made cover: {shorten_hashes((branch_node.id, next_node.id))}')
             else:
                 _LOGGER.warning(f'Falling back to extracted next states for {cfgid}:\n{next_node.id}')
-                branch_constraints = [
-                    [c for c in s.constraints if c not in next_state.constraints] for s in next_cterms
-                ]
+                branch_constraints = [[c for c in s.constraints if c not in cterm.constraints] for s in next_cterms]
                 _LOGGER.info(
                     f'Found {len(list(next_cterms))} branches manually at depth 1 for {cfgid}: {[foundry.pretty_print(mlAnd(bc)) for bc in branch_constraints]}'
                 )