Skip to content

Commit

Permalink
KCFG: Allow pretty printing (#2643)
Browse files Browse the repository at this point in the history 
* Import CFG printing from the erc20 repo

* Remove checking for loops. The backward reachability method returns false positives.

We don't care if a node can loop back to itself somehow, but only that it
completes a loop by reaching some previous instance of itself in the history displayed so far.

* Remove unnessesary empty line

* kprint.pretty_print: Overload to allow printing Substs

We don't add pretty print as a member to Subst since this causes a circular
dependency between kprint.py and kast.py

* Revert "kprint.pretty_print: Overload to allow printing Substs"

This reverts commit 8ad6728.

* kcfg: pretty_print: Convert Substs to Preds before printing

The expected output looks ugly, but when we're using a real KPrint it should be fine.

* kcfg: Keep track of previously visited nodes to detect loops

* isort

* flake8

* kcfg: to_dot: Don't remove leaf -- Its OK if we have an unused class for a node.

* flake8: Some of this indentation actually makes things uglier :-(

* Update pyk/src/pyk/tests/test_kcfg.py

Co-authored-by: Everett Hildenbrandt <[email protected]>

* kcfg: Mark internal functions with _

* visited_nodes => prior_on_trace

* extract pretty printers for nodes and edges

* pyk: Extract method edge_likes = edges+covers

* print_subgraph => _print_subgraph

Co-authored-by: Everett Hildenbrandt <[email protected]>
  • Loading branch information
@nishantjr @ehildenb
nishantjr and ehildenb authored Jun 7, 2022
1 parent 96568cc commit 35d68a4
Show file tree
Hide file tree
Showing 3 changed files with 184 additions and 24 deletions.
119 changes: 101 additions & 18 deletions pyk/src/pyk/kcfg.py
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
import json
from abc import ABC
from abc import ABC, abstractmethod
from dataclasses import dataclass
from functools import reduce
from itertools import chain
Expand All @@ -16,15 +16,22 @@
Set,
Tuple,
Union,
cast,
)

from graphviz import Digraph

from .cterm import CTerm
from .kast import KInner, KRuleLike, Subst
from .kastManip import buildRule, ml_pred_to_bool, mlAnd, simplifyBool
from .kastManip import (
buildRule,
ml_pred_to_bool,
mlAnd,
simplifyBool,
substToMlPred,
)
from .ktool import KPrint
from .utils import compare_short_hashes, shorten_hashes
from .utils import add_indent, compare_short_hashes, shorten_hashes


class KCFG(Container[Union['KCFG.Node', 'KCFG.Edge', 'KCFG.Cover']]):
Expand All @@ -47,6 +54,10 @@ class EdgeLike(ABC):
source: 'KCFG.Node'
target: 'KCFG.Node'

@abstractmethod
def pretty_print(self, kprint: KPrint) -> List[str]:
assert False, 'Must be overridden'

@dataclass(frozen=True)
class Edge(EdgeLike):
source: 'KCFG.Node'
Expand All @@ -64,6 +75,12 @@ def to_rule(self, claim=False, priority=50) -> KRuleLike:
rule, _ = buildRule(sentence_id, init_term, final_term, claim=claim, priority=priority)
return rule

def pretty_print(self, kprint: KPrint) -> List[str]:
if self.depth == 1:
return ['(' + str(self.depth) + ' step)']
else:
return ['(' + str(self.depth) + ' steps)']

@dataclass(frozen=True)
class Cover(EdgeLike):
source: 'KCFG.Node'
Expand All @@ -86,6 +103,13 @@ def __init__(self, source: 'KCFG.Node', target: 'KCFG.Node'):
def to_dict(self) -> Dict[str, Any]:
return {'source': self.source.id, 'target': self.target.id}

def pretty_print(self, kprint: KPrint) -> List[str]:
return [
'constraint: ' + kprint.pretty_print(self.constraint),
'subst:',
*add_indent(' ', kprint.pretty_print(substToMlPred(self.subst)).split('\n')),
]

_nodes: Dict[str, Node]
_edges: Dict[str, Dict[str, Edge]]
_covers: Dict[str, Dict[str, Cover]]
Expand Down Expand Up @@ -238,28 +262,66 @@ def to_json(self) -> str:
def from_json(s: str) -> 'KCFG':
return KCFG.from_dict(json.loads(s))

def to_dot(self, kprint: KPrint) -> str:
def _node_attrs(node_id: str) -> List[str]:
atts = []
if self.is_init(node_id):
atts.append('init')
if self.is_target(node_id):
atts.append('target')
if self.is_expanded(node_id):
atts.append('expanded')
if self.is_stuck(node_id):
atts.append('stuck')
if self.is_frontier(node_id):
atts.append('frontier')
return atts
def node_short_info(self, node: Node) -> str:
attrs = self.node_attrs(node.id)
attr_string = ' (' + ', '.join(attrs) + ')' if attrs else ''
return shorten_hashes(node.id) + attr_string

def pretty_print(self, kprint: KPrint) -> List[str]:

processed_nodes: List[KCFG.Node] = []

def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: List[KCFG.Node]) -> List[str]:
ret: List[str] = []

if curr_node in processed_nodes:
if len(self.edge_likes(source_id=curr_node.id)) == 0:
return ret
if curr_node in prior_on_trace:
ret.append(indent + '┊ (looped back)')
else:
ret.append(indent + '┊ (continues as previously)')
return ret
processed_nodes.append(curr_node)

num_children = len(self.edge_likes(source_id=curr_node.id))
is_branch = num_children > 1
for i, edge_like in enumerate(self.edge_likes(source_id=curr_node.id)):
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))
ret.extend(_print_subgraph(new_indent, edge_like.target, prior_on_trace + [edge_like.source]))
if is_branch:
ret.append(new_indent.rstrip())
return ret

return [self.node_short_info(self.init[0])] + _print_subgraph('', self.init[0], [self.init[0]])

def to_dot(self, kprint: KPrint) -> str:
def _short_label(label):
return '\n'.join([label_line if len(label_line) < 100 else (label_line[0:100] + ' ...') for label_line in label.split('\n')])

graph = Digraph()

for node in self.nodes:
classAttrs = ' '.join(_node_attrs(node.id))
nodeAttrs = self.node_attrs(node.id)
classAttrs = ' '.join(nodeAttrs)
label = shorten_hashes(node.id) + (classAttrs and ' ' + classAttrs)
attrs = {'class': classAttrs} if classAttrs else {}
graph.node(name=node.id, label=label, **attrs)
Expand Down Expand Up @@ -453,6 +515,11 @@ def remove_cover(self, source_id: str, target_id: str) -> None:
if not self._covers[source_id]:
self._covers.pop(source_id)

def edge_likes(self, *, source_id: Optional[str] = None, target_id: Optional[str] = None) -> List[EdgeLike]:
return \
cast(List[KCFG.EdgeLike], self.edges(source_id=source_id, target_id=target_id)) + \
cast(List[KCFG.EdgeLike], self.covers(source_id=source_id, target_id=target_id))

def add_init(self, node_id: str) -> None:
node_id = self._resolve(node_id)
self._init.add(node_id)
Expand Down Expand Up @@ -545,6 +612,22 @@ def is_verified(self, source_id: str, target_id: str) -> bool:
target_id = self._resolve(target_id)
return (source_id, target_id) in self._verified

def node_attrs(self, node_id: str) -> List[str]:
attrs = []
if self.is_init(node_id):
attrs.append('init')
if self.is_target(node_id):
attrs.append('target')
if self.is_expanded(node_id):
attrs.append('expanded')
if self.is_stuck(node_id):
attrs.append('stuck')
if self.is_frontier(node_id):
attrs.append('frontier')
if self.is_leaf(node_id):
attrs.append('leaf')
return attrs

def prune(self, node_id: str) -> None:
nodes = self.reachable_nodes(node_id)
for node in nodes:
Expand Down
85 changes: 79 additions & 6 deletions pyk/src/pyk/tests/test_kcfg.py
View file
Original file line number Diff line number Diff line change
@@ -1,16 +1,22 @@
from typing import Any, Dict, List, Tuple
from typing import Any, Dict, List, Tuple, cast
from unittest import TestCase

from ..cterm import CTerm
from ..kast import TRUE, KApply, KInner, KVariable
from ..kast import TRUE, KApply, KAst, KInner, KVariable
from ..kcfg import KCFG
from ..ktool import KPrint
from ..prelude import token
from ..utils import shorten_hashes


def nid(i: int) -> str:
return node(i).id


def short_id(i: int) -> str:
return shorten_hashes(nid(i))


# over 10 is variables
def term(i: int) -> CTerm:
inside: KInner = token(i)
Expand All @@ -32,10 +38,11 @@ def node_dicts(n: int) -> List[Dict[str, Any]]:


def edge_dicts(*edges: Tuple[int, int]) -> List[Dict[str, Any]]:
return [
{'source': nid(i), 'target': nid(j), 'condition': TRUE.to_dict(), 'depth': 1}
for i, j in edges
]

def _make_edge_dict(i, j, depth=1):
return {'source': nid(i), 'target': nid(j), 'condition': TRUE.to_dict(), 'depth': depth}

return [_make_edge_dict(*edge) for edge in edges]


def cover_dicts(*edges: Tuple[int, int]) -> List[Dict[str, Any]]:
Expand All @@ -45,6 +52,15 @@ def cover_dicts(*edges: Tuple[int, int]) -> List[Dict[str, Any]]:
]


class MockKPrint:
def pretty_print(self, term: KAst) -> str:
return str(term)


def mock_kprint() -> KPrint:
return cast(KPrint, MockKPrint())


class KCFGTestCase(TestCase):

def test_from_dict_single_node(self):
Expand Down Expand Up @@ -246,3 +262,60 @@ def test_paths_between(self):
(edge(0, 1), edge(1, 2), edge(2, 3)),
},
)

def test_pretty_print(self):
d = {
'init': [nid(0)],
'target': [nid(6)],
'nodes': node_dicts(12),
# 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
),
'covers': cover_dicts((8, 11)) # Loops back
}
cfg = KCFG.from_dict(d)

print(set(map(lambda node: node.id, cfg.reachable_nodes(nid(5), reverse=True, traverse_covers=True))))

# TODO: Why are all nodes (besides the target) frontiers?
# TODO: Add a cover
self.maxDiff = None
actual = '\n'.join(cfg.pretty_print(mock_kprint())) + '\n'
self.assertMultiLineEqual(actual,
f"{short_id(0)} (init, frontier)\n"
f"│ (1 step)\n"
f"├ {short_id(1)} (frontier)\n"
f"│ (5 steps)\n"
f"├ {short_id(2)} (frontier)\n"
f"│ (1 step)\n"
f"├ {short_id(3)} (frontier)\n"
f"┢━ {short_id(4)} (frontier)\n"
f"┃ │ (1 step)\n"
f"┃ ├ {short_id(5)} (frontier)\n"
f"┃ │ (1 step)\n"
f"┃ ├ {short_id(2)} (frontier)\n"
f"┃ ┊ (looped back)\n"
f"┃\n"
f"┣━ {short_id(5)} (frontier)\n"
f"┃ ┊ (continues as previously)\n"
f"┃\n"
f"┣━ {short_id(6)} (target, leaf)\n"
f"┃\n"
f"┣━ {short_id(7)} (frontier)\n"
f"┃ │ (1 step)\n"
f"┃ └ {short_id(6)} (target, leaf)\n"
f"┃\n"
f"┗━ {short_id(11)} (frontier)\n"
f" │ (1 step)\n"
f" ├ {short_id(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" ├ {short_id(11)} (frontier)\n"
f" ┊ (looped back)\n\n"
)
4 changes: 4 additions & 0 deletions pyk/src/pyk/utils.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -113,6 +113,10 @@ def nonempty_str(x: Any) -> str:
return x


def add_indent(indent: str, lines: List[str]) -> List[str]:
return list(map(lambda line: indent + line, lines))


# Hashes

def hash_str(x: Any) -> str:
Expand Down

0 comments on commit 35d68a4

Please sign in to comment.