Pyk: KCFG stores aliases for nodes

pyk/src/pyk/kcfg.py

@@ -31,7 +31,7 @@
     substToMlPred,
 )
 from .ktool import KPrint
-from .utils import add_indent, compare_short_hashes, shorten_hashes
+from .utils import add_indent, compare_short_hashes, shorten_hash
 
 
 class KCFG(Container[Union['KCFG.Node', 'KCFG.Edge', 'KCFG.Cover']]):
@@ -117,6 +117,7 @@ def pretty_print(self, kprint: KPrint) -> List[str]:
     _target: Set[str]
     _expanded: Set[str]
     _verified: Set[Tuple[str, str]]
+    _aliases: Dict[str, str]
     _lock: RLock
 
     def __init__(self):
@@ -127,6 +128,7 @@ def __init__(self):
         self._target = set()
         self._expanded = set()
         self._verified = set()
+        self._aliases = dict()
         self._lock = RLock()
 
     def __contains__(self, item: object) -> bool:
@@ -197,6 +199,7 @@ def to_dict(self) -> Dict[str, Any]:
         target = sorted(self._target)
         expanded = sorted(self._expanded)
         verified = [{"source": source_id, "target": target_id} for source_id, target_id in sorted(self._verified)]
+        aliases = self._aliases
 
         res = {
             'nodes': nodes,
@@ -206,6 +209,7 @@ def to_dict(self) -> Dict[str, Any]:
             'target': target,
             'expanded': expanded,
             'verified': verified,
+            'aliases': aliases
         }
         return {k: v for k, v in res.items() if v}
 
@@ -253,8 +257,37 @@ def resolve(node_id: str) -> str:
         for verified_ids in dct.get('verified') or []:
             cfg.add_verified(resolve(verified_ids['source']), resolve(verified_ids['target']))
 
+        for alias, id in (dct.get('aliases') or {}).items():
+            cfg.add_alias(name=alias, id=id)
+
         return cfg
 
+    def short_id(self, node: Node) -> str:
+        for alias, hash in self._aliases.items():
+            if node.id == hash:
+                return alias
+        return shorten_hash(node.id)
+
+    def short_names(self, value: Any, leftChars=6, rightChars=6) -> Any:
+        result: Any = None
+        if isinstance(value, KCFG.Node):
+            result = self.short_id(value)
+        elif type(value) is tuple:
+            result = tuple([self.short_names(item) for item in value])
+        elif type(value) is list:
+            result = [self.short_names(item) for item in value]
+        elif type(value) is dict:
+            result = {}
+            for (k, v) in value.items():
+                result[self.short_names(k)] = self.short_names(v)
+        elif type(value) is set:
+            result = set()
+            for item in value:
+                result.add(self.short_names(item))
+        else:
+            assert(False)
+        return result
+
     def to_json(self) -> str:
         return json.dumps(self.to_dict(), sort_keys=True)
 
@@ -265,7 +298,7 @@ def from_json(s: str) -> 'KCFG':
     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
+        return self.short_id(node) + attr_string
 
     def pretty_print(self, kprint: KPrint) -> List[str]:
 
@@ -322,7 +355,7 @@ def _short_label(label):
         for node in self.nodes:
             nodeAttrs = self.node_attrs(node.id)
             classAttrs = ' '.join(nodeAttrs)
-            label = shorten_hashes(node.id) + (classAttrs and ' ' + classAttrs)
+            label = self.short_id(node) + (classAttrs and ' ' + classAttrs)
             attrs = {'class': classAttrs} if classAttrs else {}
             graph.node(name=node.id, label=label, **attrs)
 
@@ -351,21 +384,23 @@ def _short_label(label):
 
         return graph.source
 
-    def _resolve_all(self, short_id: str) -> List[str]:
-        return [node_id for node_id in self._nodes if compare_short_hashes(short_id, node_id)]
+    def _resolve_all(self, id_like: str) -> List[str]:
+        if id_like in self._aliases:
+            return [self._aliases[id_like]]
+        return [node_id for node_id in self._nodes if compare_short_hashes(id_like, node_id)]
 
-    def _resolve_or_none(self, short_id: str) -> Optional[str]:
-        matches = self._resolve_all(short_id)
+    def _resolve_or_none(self, id_like: str) -> Optional[str]:
+        matches = self._resolve_all(id_like)
         if not matches:
             return None
         if len(matches) > 1:
-            raise ValueError(f'Multiple nodes for pattern: {short_id} (matches e.g. {matches[0]} and {matches[1]})')
+            raise ValueError(f'Multiple nodes for pattern: {id_like} (matches e.g. {matches[0]} and {matches[1]})')
         return matches[0]
 
-    def _resolve(self, short_id: str) -> str:
-        match = self._resolve_or_none(short_id)
+    def _resolve(self, id_like: str) -> str:
+        match = self._resolve_or_none(id_like)
         if not match:
-            raise ValueError(f'Unknown node: {short_id}')
+            raise ValueError(f'Unknown node: {id_like}')
         return match
 
     def node(self, node_id: str) -> Node:
@@ -419,6 +454,10 @@ def remove_node(self, node_id: str) -> None:
         self._expanded.discard(node_id)
         self._verified = set((source_id, target_id) for source_id, target_id in self._verified if source_id != node_id and target_id != node_id)
 
+        del_aliases = [alias for alias, id in self._aliases.items() if id == node_id]
+        for a in del_aliases:
+            del self._aliases[a]
+
     def edge(self, source_id: str, target_id: str) -> Optional[Edge]:
         source_id = self._resolve(source_id)
         target_id = self._resolve(target_id)
@@ -537,6 +576,13 @@ def add_verified(self, source_id: str, target_id: str) -> None:
         target_id = self._resolve(target_id)
         self._verified.add((source_id, target_id))
 
+    def add_alias(self, name: str, id: str) -> None:
+        id = self._resolve(id)
+        self._aliases[name] = id
+
+    def remove_alias(self, name: str, alias: str) -> None:
+        self._aliases.pop(name)
+
     def remove_init(self, node_id: str) -> None:
         node_id = self._resolve(node_id)
         if node_id not in self._init:

pyk/src/pyk/tests/test_kcfg.py

@@ -6,17 +6,12 @@
 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)
@@ -263,11 +258,75 @@ def test_paths_between(self):
             },
         )
 
+    def test_resolve(self):
+        # Given
+        d = {
+            'nodes': node_dicts(4),
+            'edges': edge_dicts((0, 1), (0, 2), (1, 2), (1, 3), (2, 3), (3, 0)),
+        }
+        cfg = KCFG.from_dict(d)
+
+        self.assertEqual(node(1), cfg.node('d33...d8'))
+        self.assertEqual(node(1), cfg.node('d33..d8'))
+        self.assertEqual(node(1), cfg.node(node(1).id))
+
+        # Matches no nodes
+        with self.assertRaisesRegex(ValueError, 'Unknown node: deadbeef\\.\\.\\.d8'):
+            self.assertEqual(node(1), cfg.node('deadbeef...d8'))
+
+        # Bad short hash: Has digits between dots
+        with self.assertRaisesRegex(ValueError, 'Bad short hash: 3\\.c62e73544\\.\\.\\.'):
+            cfg.node('3.c62e73544...')
+
+        # Bad short hash: Has non hex digits
+        with self.assertRaisesRegex(ValueError, 'Bad short hash: 3\\.\\.\\.XXX'):
+            cfg.node('3...XXX')
+
+        # Bad short hash: Has more than three dots
+        with self.assertRaisesRegex(ValueError, 'Bad short hash: 3\\.\\.\\.\\.\\.adf'):
+            cfg.node('3.....adf')
+
+        # Matches all nodes
+        with self.assertRaisesRegex(ValueError, 'Multiple nodes for pattern: ...'):
+            cfg.node('...')
+
+        # Matches node(0) and node(2)
+        with self.assertRaisesRegex(ValueError, 'Multiple nodes for pattern: ...'):
+            cfg.node('3...')
+
+    def test_aliases(self):
+        # Given
+        d = {
+            'nodes': node_dicts(2),
+            'edges': edge_dicts((0, 1)),
+            'aliases': {'foo': nid(1)}
+        }
+
+        cfg = KCFG.from_dict(d)
+        self.assertEqual(cfg.node('foo'), node(1))
+        self.assertEqual(cfg.short_id(node(1)), 'foo')
+
+        self.assertNotEqual(cfg.short_id(node(0)), 'bar')
+        cfg.add_alias('bar', node(0).id)
+        self.assertEqual(cfg.node('bar'), node(0))
+        cfg.remove_alias('bar', node(0).id)
+        with self.assertRaisesRegex(ValueError, 'Bad short hash: bar'):
+            cfg.node('bar')
+        self.assertNotEqual(cfg.short_id(node(0)), 'bar')
+
+        with self.assertRaisesRegex(ValueError, 'Unknown node: '):
+            cfg.add_alias('buzz', node(3).id)
+
+        cfg.remove_node(nid(1))
+        cfg.create_node(term(1))
+        self.assertNotEqual(cfg.short_id(node(1)), 'foo')
+
     def test_pretty_print(self):
         d = {
             'init': [nid(0)],
             'target': [nid(6)],
             'nodes': node_dicts(12),
+            'aliases': {'foo': 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
@@ -276,46 +335,47 @@ def test_pretty_print(self):
                                 (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
+            '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))))
+        def _short_id(i) -> str:
+            return cfg.short_id(node(i))
 
         # 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"{_short_id(0)} (init, frontier)\n"
                                   f"│  (1 step)\n"
-                                  f"├  {short_id(1)} (frontier)\n"
+                                  f"├  {_short_id(1)} (frontier)\n"
                                   f"│  (5 steps)\n"
-                                  f"├  {short_id(2)} (frontier)\n"
+                                  f"├  {_short_id(2)} (frontier)\n"
                                   f"│  (1 step)\n"
-                                  f"├  {short_id(3)} (frontier)\n"
-                                  f"┢━ {short_id(4)} (frontier)\n"
+                                  f"├  {_short_id(3)} (frontier)\n"
+                                  f"┢━ {_short_id(4)} (frontier)\n"
                                   f"┃   │  (1 step)\n"
-                                  f"┃   ├  {short_id(5)} (frontier)\n"
+                                  f"┃   ├  {_short_id(5)} (frontier)\n"
                                   f"┃   │  (1 step)\n"
-                                  f"┃   ├  {short_id(2)} (frontier)\n"
+                                  f"┃   ├  {_short_id(2)} (frontier)\n"
                                   f"┃   ┊ (looped back)\n"
                                   f"┃\n"
-                                  f"┣━ {short_id(5)} (frontier)\n"
+                                  f"┣━ {_short_id(5)} (frontier)\n"
                                   f"┃   ┊ (continues as previously)\n"
                                   f"┃\n"
-                                  f"┣━ {short_id(6)} (target, leaf)\n"
+                                  f"┣━ {_short_id(6)} (target, leaf)\n"
                                   f"┃\n"
-                                  f"┣━ {short_id(7)} (frontier)\n"
+                                  f"┣━ {_short_id(7)} (frontier)\n"
                                   f"┃   │  (1 step)\n"
-                                  f"┃   └  {short_id(6)} (target, leaf)\n"
+                                  f"┃   └  {_short_id(6)} (target, leaf)\n"
                                   f"┃\n"
-                                  f"┗━ {short_id(11)} (frontier)\n"
+                                  f"┗━ {_short_id(11)} (frontier)\n"
                                   f"    │  (1 step)\n"
-                                  f"    ├  {short_id(8)} (leaf)\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"    ├  {_short_id(11)} (frontier)\n"
                                   f"    ┊ (looped back)\n\n"
                                   )

pyk/src/pyk/utils.py

@@ -117,6 +117,10 @@ def add_indent(indent: str, lines: List[str]) -> List[str]:
     return list(map(lambda line: indent + line, lines))
 
 
+def is_hexstring(x: str) -> bool:
+    return all(c in string.hexdigits for c in x)
+
+
 # Hashes
 
 def hash_str(x: Any) -> str:
@@ -129,7 +133,7 @@ def is_hash(x: Any) -> bool:
     # NB! currently only sha256 in hexdec form is detected
     # 2b9e b7c5 441e 9f7e 97f9 a4e5 fc04 a0f7 9f62 c8e9 605a ad1e 02db e8de 3c21 0422
     # 1    2    3    4    5    6    7    8    9    10   11   12   13   14   15   16
-    return type(x) is str and len(x) == 64 and all(c in string.hexdigits for c in x)
+    return type(x) is str and len(x) == 64 and is_hexstring(x)
 
 
 def shorten_hash(h: str, leftChars=6, rightChars=6) -> str:
@@ -159,7 +163,20 @@ def shorten_hashes(value: Any, leftChars=6, rightChars=6) -> Any:
     return result
 
 
+def deconstruct_short_hash(h: str) -> Tuple[str, str]:
+    x = h.lower()
+    if is_hash(x):
+        return (x, x)
+    (l, sep, r) = x.partition('...')
+    if sep == '...' and is_hexstring(l) and is_hexstring(r):
+        return (l, r)
+    (l, sep, r) = x.partition('..')
+    if sep == '..' and is_hexstring(l) and is_hexstring(r):
+        return (l, r)
+    raise ValueError(f'Bad short hash: {h}')
+
+
 def compare_short_hashes(lhs: str, rhs: str):
-    left, right = lhs.split('.'), rhs.split('.')
-    (l0, l1, r0, r1) = (left[0].upper(), left[-1].upper(), right[0].upper(), right[-1].upper())
+    (l0, l1) = deconstruct_short_hash(lhs)
+    (r0, r1) = deconstruct_short_hash(rhs)
     return (l0.startswith(r0) or r0.startswith(l0)) and (l1.endswith(r1) or r1.endswith(l1))