1from __future__ import annotations
2
3import logging
4from typing import TYPE_CHECKING
5
6from ..kcfg.show import KCFGShow, NodePrinter
7from ..utils import ensure_dir_path
8
9if TYPE_CHECKING:
10 from collections.abc import Iterable
11 from pathlib import Path
12 from typing import Final
13
14 from graphviz import Digraph
15
16 from ..cterm.show import CTermShow
17 from ..kast.outer import KDefinition
18 from ..kcfg import KCFG
19 from ..kcfg.kcfg import NodeIdLike
20 from .reachability import APRProof
21
22_LOGGER: Final = logging.getLogger(__name__)
23
24
[docs]
25class APRProofNodePrinter(NodePrinter):
26 proof: APRProof
27
28 def __init__(self, proof: APRProof, cterm_show: CTermShow, full_printer: bool = False):
29 super().__init__(cterm_show, full_printer=full_printer)
30 self.proof = proof
31
[docs]
32 def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
33 attrs = super().node_attrs(kcfg, node)
34 if self.proof.is_init(node.id):
35 attrs.append('init')
36 if self.proof.is_target(node.id):
37 attrs.append('target')
38 if self.proof.is_pending(node.id):
39 attrs.append('pending')
40 if self.proof.is_refuted(node.id):
41 attrs.append('refuted')
42 if self.proof.is_terminal(node.id):
43 attrs.append('terminal')
44 if 'stuck' in attrs:
45 attrs.remove('stuck')
46 if self.proof.is_bounded(node.id):
47 attrs.append('bounded')
48 if 'stuck' in attrs:
49 attrs.remove('stuck')
50 return attrs
51
52
[docs]
53class APRProofShow:
54 kcfg_show: KCFGShow
55
56 def __init__(self, definition: KDefinition, node_printer: NodePrinter | None = None):
57 self.kcfg_show = KCFGShow(definition, node_printer=node_printer)
58
[docs]
59 def pretty_segments(self, proof: APRProof, minimize: bool = True) -> Iterable[tuple[str, Iterable[str]]]:
60 ret_lines = list(self.kcfg_show.pretty_segments(proof.kcfg, minimize=minimize))
61 if len(proof.pending) > 0:
62 target_node_lines = ['', 'Target Node:']
63 target_node_lines += self.kcfg_show.node_printer.print_node(proof.kcfg, proof.kcfg.node(proof.target))
64 ret_lines.append((f'node_{proof.target}', target_node_lines))
65 return KCFGShow.make_unique_segments(ret_lines)
66
[docs]
67 def pretty(self, proof: APRProof, minimize: bool = True) -> Iterable[str]:
68 return (line for _, seg_lines in self.pretty_segments(proof, minimize=minimize) for line in seg_lines)
69
[docs]
70 def show(
71 self,
72 proof: APRProof,
73 nodes: Iterable[NodeIdLike] = (),
74 node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (),
75 to_module: bool = False,
76 minimize: bool = True,
77 omit_cells: Iterable[str] = (),
78 ) -> list[str]:
79 res_lines = self.kcfg_show.show(
80 proof.kcfg,
81 nodes=nodes,
82 node_deltas=node_deltas,
83 to_module=to_module,
84 minimize=minimize,
85 omit_cells=omit_cells,
86 module_name=f'SUMMARY-{proof.id.upper().replace("_", "-")}',
87 )
88 return res_lines
89
[docs]
90 def dot(self, proof: APRProof) -> Digraph:
91 graph = self.kcfg_show.dot(proof.kcfg)
92 attrs = {'class': 'target', 'style': 'solid'}
93 for node in proof.pending:
94 graph.edge(tail_name=node.id, head_name=proof.target, label=' ???', **attrs)
95 for node in proof.kcfg.stuck:
96 graph.edge(tail_name=node.id, head_name=proof.target, label=' false', **attrs)
97 return graph
98
[docs]
99 def dump(self, proof: APRProof, dump_dir: Path, dot: bool = False) -> None:
100 ensure_dir_path(dump_dir)
101
102 proof_file = dump_dir / f'{proof.id}.json'
103 proof_file.write_text(proof.json)
104 _LOGGER.info(f'Wrote CFG file {proof.id}: {proof_file}')
105
106 if dot:
107 proof_dot = self.dot(proof)
108 dot_file = dump_dir / f'{proof.id}.dot'
109 dot_file.write_text(proof_dot.source)
110 _LOGGER.info(f'Wrote DOT file {proof.id}: {dot_file}')
111
112 self.kcfg_show.dump(f'{proof.id}_cfg', proof.kcfg, dump_dir, dot=False)