Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into release
Browse files Browse the repository at this point in the history
  • Loading branch information
@rv-jenkins
rv-jenkins committed Jul 1, 2022
2 parents cb37f88 + 2a5080c commit deddbe4
Show file tree
Hide file tree
Showing 2 changed files with 43 additions and 23 deletions.
33 changes: 24 additions & 9 deletions pyk/src/pyk/kcfg.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)']
Expand Down Expand Up @@ -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] = []

Expand All @@ -309,25 +320,29 @@ 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 + ' '
else:
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())
Expand All @@ -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
Expand Down
33 changes: 19 additions & 14 deletions pyk/src/pyk/tests/test_kcfg.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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


Expand Down Expand Up @@ -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]

Expand Down Expand Up @@ -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]],
Expand All @@ -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"
)

0 comments on commit deddbe4

Please sign in to comment.