From 2a5080c119e8ea636e631184aa669b910b378573 Mon Sep 17 00:00:00 2001 From: Nishant Rodrigues Date: Fri, 1 Jul 2022 16:32:32 -0500 Subject: [PATCH] Make frontier nodes bold, use dotted lines for covers, display conditions for split-case (#2697) --- pyk/src/pyk/kcfg.py | 33 ++++++++++++++++++++++++--------- pyk/src/pyk/tests/test_kcfg.py | 33 +++++++++++++++++++-------------- 2 files changed, 43 insertions(+), 23 deletions(-) diff --git a/pyk/src/pyk/kcfg.py b/pyk/src/pyk/kcfg.py index 1daa977254b..afc1373d069 100644 --- a/pyk/src/pyk/kcfg.py +++ b/pyk/src/pyk/kcfg.py @@ -86,7 +86,9 @@ def to_rule(self, claim=False, priority=50) -> KRuleLike: return rule def pretty_print(self, kprint: KPrint) -> List[str]: - if self.depth == 1: + if self.depth == 0: + return ['\nandBool'.join(kprint.pretty_print(self.condition).split(' andBool'))] + elif self.depth == 1: return ['(' + str(self.depth) + ' step)'] else: return ['(' + str(self.depth) + ' steps)'] @@ -292,6 +294,15 @@ def pretty_print(self, kprint: KPrint) -> List[str]: processed_nodes: List[KCFG.Node] = [] + def _bold(text: str) -> str: + return '\033[1m' + text + '\033[0m' + + def _print_node(node: KCFG.Node) -> str: + short_info = self.node_short_info(node) + if self.is_frontier(node.id): + short_info = _bold(short_info) + return short_info + def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: List[KCFG.Node]) -> List[str]: ret: List[str] = [] @@ -309,15 +320,11 @@ def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: List[KCFG num_children = len(edges_from) is_branch = num_children > 1 for i, edge_like in enumerate(edges_from): - is_first_child = i == 0 is_last_child = i == num_children - 1 if not is_branch: elbow = '├ ' if len(self.edge_likes(source_id=edge_like.target.id)) else '└ ' new_indent = indent - elif is_first_child: - elbow = '┢━' - new_indent = indent + '┃ ' elif is_last_child: elbow = '┗━' new_indent = indent + ' ' @@ -325,9 +332,17 @@ def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: List[KCFG elbow = '┣━' new_indent = indent + '┃ ' - if not(isinstance(edge_like, KCFG.Edge) and edge_like.depth == 0): - ret.extend(add_indent(indent + '│ ', edge_like.pretty_print(kprint))) - ret.append(indent + elbow + ' ' + self.node_short_info(edge_like.target)) + extension_char = '' + if isinstance(edge_like, KCFG.Edge): + if edge_like.depth == 0: + extension_char = '┃' + else: + extension_char = '│' + elif isinstance(edge_like, KCFG.Cover): + extension_char = '┊' + ret.extend(add_indent(indent + extension_char + ' ', edge_like.pretty_print(kprint))) + + ret.append(indent + elbow + ' ' + _print_node(edge_like.target)) ret.extend(_print_subgraph(new_indent, edge_like.target, prior_on_trace + [edge_like.source])) if is_branch: ret.append(new_indent.rstrip()) @@ -336,7 +351,7 @@ def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: List[KCFG ret = [] init = sorted(self.init) while init: - ret.append(self.node_short_info(init[0])) + ret.append(_print_node(init[0])) ret.extend(_print_subgraph('', init[0], [init[0]])) init = sorted(node for node in self.nodes if node not in processed_nodes) return ret diff --git a/pyk/src/pyk/tests/test_kcfg.py b/pyk/src/pyk/tests/test_kcfg.py index cc5eabcf0c7..c0ab980c98e 100644 --- a/pyk/src/pyk/tests/test_kcfg.py +++ b/pyk/src/pyk/tests/test_kcfg.py @@ -5,7 +5,7 @@ from ..kast import TRUE, KApply, KAst, KInner, KVariable from ..kcfg import KCFG from ..ktool import KPrint -from ..prelude import token +from ..prelude import mlEquals, token from ..utils import shorten_hash @@ -35,8 +35,8 @@ def node_dicts(n: int) -> List[Dict[str, Any]]: def edge_dicts(*edges: Tuple[int, int]) -> List[Dict[str, Any]]: - def _make_edge_dict(i, j, depth=1): - return {'source': nid(i), 'target': nid(j), 'condition': TRUE.to_dict(), 'depth': depth} + def _make_edge_dict(i, j, depth=1, condition=TRUE): + return {'source': nid(i), 'target': nid(j), 'condition': condition.to_dict(), 'depth': depth} return [_make_edge_dict(*edge) for edge in edges] @@ -319,11 +319,11 @@ def test_pretty_print(self): 'aliases': {'foo': nid(3), 'bar': nid(3)}, # Each of the branching edges have given depth=0 # noqa: E131 'edges': edge_dicts((0, 1), (1, 2, 5), (2, 3), # Initial Linear segment - (3, 4, 0), (4, 5), (5, 2), # Loops back - (3, 5, 0), # Go to previous non-terminal node not as loop - (3, 6, 0), # Terminates - (3, 7, 0), (7, 6), # Go to previous terminal node not as loop - (3, 11, 0), (11, 8) # Covered + (3, 4, 0, mlEquals(KVariable('x'), token(4))), (4, 5), (5, 2), # Loops back + (3, 5, 0, mlEquals(KVariable('x'), token(5))), # Go to previous non-terminal node not as loop + (3, 6, 0, mlEquals(KVariable('x'), token(6))), # Terminates + (3, 7, 0, mlEquals(KVariable('x'), token(7))), (7, 6), # Go to previous terminal node not as loop + (3, 11, 0, mlEquals(KVariable('x'), token(11))), (11, 8) # Covered ), 'covers': cover_dicts((8, 11)), # Loops back 'expanded': [nid(i) for i in [0, 1, 2, 3, 4, 5, 7, 11]], @@ -343,31 +343,36 @@ def _short_hash(i) -> str: f"├ {_short_hash(2)} (expanded)\n" f"│ (1 step)\n" f"├ {_short_hash(3)} (expanded, @bar, @foo)\n" - f"┢━ {_short_hash(6)} (target, leaf)\n" + f"┃ KApply(label=KLabel(name='#Equals', params=(KSort(name='K'), KSort(name='K'))), args=(KVariable(name='x'), KToken(token='6', sort=KSort(name='Int'))))\n" + f"┣━ {_short_hash(6)} (target, leaf)\n" f"┃\n" + f"┃ KApply(label=KLabel(name='#Equals', params=(KSort(name='K'), KSort(name='K'))), args=(KVariable(name='x'), KToken(token='5', sort=KSort(name='Int'))))\n" f"┣━ {_short_hash(5)} (expanded)\n" f"┃ │ (1 step)\n" f"┃ ├ {_short_hash(2)} (expanded)\n" f"┃ ┊ (looped back)\n" f"┃\n" + f"┃ KApply(label=KLabel(name='#Equals', params=(KSort(name='K'), KSort(name='K'))), args=(KVariable(name='x'), KToken(token='11', sort=KSort(name='Int'))))\n" f"┣━ {_short_hash(11)} (expanded)\n" f"┃ │ (1 step)\n" f"┃ ├ {_short_hash(8)} (leaf)\n" - f"┃ │ constraint: KApply(label=KLabel(name='#Top', params=(KSort(name='GeneratedTopCell'),)), args=())\n" - f"┃ │ subst:\n" - f"┃ │ KApply(label=KLabel(name='#Equals', params=(KSort(name='K'), KSort(name='K'))), args=(KVariable(name='V11'), KToken(token='8', sort=KSort(name='Int'))))\n" + f"┃ ┊ constraint: KApply(label=KLabel(name='#Top', params=(KSort(name='GeneratedTopCell'),)), args=())\n" + f"┃ ┊ subst:\n" + f"┃ ┊ KApply(label=KLabel(name='#Equals', params=(KSort(name='K'), KSort(name='K'))), args=(KVariable(name='V11'), KToken(token='8', sort=KSort(name='Int'))))\n" f"┃ ├ {_short_hash(11)} (expanded)\n" f"┃ ┊ (looped back)\n" f"┃\n" + f"┃ KApply(label=KLabel(name='#Equals', params=(KSort(name='K'), KSort(name='K'))), args=(KVariable(name='x'), KToken(token='4', sort=KSort(name='Int'))))\n" f"┣━ {_short_hash(4)} (expanded)\n" f"┃ │ (1 step)\n" f"┃ ├ {_short_hash(5)} (expanded)\n" f"┃ ┊ (continues as previously)\n" f"┃\n" + f"┃ KApply(label=KLabel(name='#Equals', params=(KSort(name='K'), KSort(name='K'))), args=(KVariable(name='x'), KToken(token='7', sort=KSort(name='Int'))))\n" f"┗━ {_short_hash(7)} (expanded)\n" f" │ (1 step)\n" f" └ {_short_hash(6)} (target, leaf)\n" f"\n" - f"{_short_hash(9)} (frontier, leaf)\n" - f"{_short_hash(10)} (frontier, leaf)\n" + f"\033[1m{_short_hash(9)} (frontier, leaf)\033[0m\n" + f"\033[1m{_short_hash(10)} (frontier, leaf)\033[0m\n" )