Skip to content

Commit 0f96555

Browse files
Stevengrejberthold
Stevengre
and
jberthold
authored
feat(show): --statistics support multi-branches to one node. (#754)
Co-authored-by: Jost Berthold <jost.berthold@gmail.com>
1 parent 0054ada commit 0f96555

4 files changed

Lines changed: 196 additions & 13 deletions

File tree

‎kmir/src/kmir/utils.py‎

Lines changed: 24 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -191,17 +191,34 @@ def _path_nodes(source_id: int, path: Sequence[KCFG.Successor]) -> list[int]:
191191
return node_ids
192192

193193
for leaf in sorted(leaves, key=lambda n: n.id):
194-
path = kcfg.shortest_path_between(proof.init, leaf.id)
195-
if path is None:
194+
paths = kcfg.paths_between(proof.init, leaf.id)
195+
if not paths:
196196
leaf_lines.append(f' leaf {leaf.id}: unreachable from init')
197197
continue
198198

199-
steps = kcfg.path_length(path)
200-
total_steps += steps
199+
path_infos: list[tuple[int, tuple[int, ...]]] = []
200+
seen_sequences: set[tuple[int, ...]] = set()
201+
202+
for path in paths:
203+
steps = kcfg.path_length(path)
204+
node_seq = tuple(_path_nodes(proof.init, path))
205+
if node_seq in seen_sequences:
206+
continue
207+
seen_sequences.add(node_seq)
208+
path_infos.append((steps, node_seq))
209+
210+
if not path_infos:
211+
leaf_lines.append(f' leaf {leaf.id}: unreachable from init')
212+
continue
213+
214+
total_steps += min(steps for steps, _ in path_infos)
201215
reachable_leaf_count += 1
202-
node_seq = _path_nodes(proof.init, path)
203-
seq_str = ' -> '.join(str(nid) for nid in node_seq)
204-
leaf_lines.append(f' leaf {leaf.id}: steps {steps}, path {seq_str}')
216+
path_infos.sort(key=lambda info: (info[0], info[1]))
217+
218+
for idx, (steps, node_seq) in enumerate(path_infos, start=1):
219+
suffix = '' if len(path_infos) == 1 else f' (path {idx}/{len(path_infos)})'
220+
seq_str = ' -> '.join(str(nid) for nid in node_seq)
221+
leaf_lines.append(f' leaf {leaf.id}{suffix}: steps {steps}, path {seq_str}')
205222

206223
lines.append(f' total leaves (non-root): {len(leaves)}')
207224
lines.append(f' reachable leaves : {reachable_leaf_count}')

‎kmir/src/tests/integration/data/prove-rs/show/enum.smir.main.cli-stats-leaves.expected‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: src/rust/library/std/src/rt.rs:194
5+
│
6+
│ (162 steps)
7+
├─ 3 (terminal)
8+
│ #EndProgram ~> .K
9+
│ function: main
10+
│
11+
┊ constraint: true
12+
┊ subst: ...
13+
└─ 2 (leaf, target, terminal)
14+
#EndProgram ~> .K
15+
16+
17+
18+
19+
STATISTICS
20+
-----------
21+
Total nodes: 2
22+
23+
Node roles (exclusive):
24+
target : 1 ids: 2
25+
terminal: 1 ids: 3
26+
(root nodes omitted from totals: 1)
27+
28+
Leaf paths from init:
29+
total leaves (non-root): 1
30+
reachable leaves : 1
31+
total steps : 162
32+
33+
leaf 2: steps 162, path 1 -> 3 -> 2
34+
35+
LEAF <k> CELLS
36+
---------------
37+
Node 2:
38+
#EndProgram ~> .K

‎kmir/src/tests/integration/data/prove-rs/show/niche-enum.smir.foo.cli-stats-leaves.expected‎

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
2+
┌─ 1 (root, init)
3+
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
4+
│ span: src/rust/library/std/src/rt.rs:194
5+
│
6+
│ (13 steps)
7+
├─ 3 (split)
8+
│ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 3 ) )
9+
│ function: foo
10+
┃
11+
┃ (branch)
12+
┣━━┓ subst: .Subst
13+
┃ ┃ constraint:
14+
┃ ┃ ARG_UINT1:Int ==Int 1
15+
┃ │
16+
┃ ├─ 4
17+
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 3 ) )
18+
┃ │ function: foo
19+
┃ │
20+
┃ │ (33 steps)
21+
┃ ├─ 6 (terminal)
22+
┃ │ #EndProgram ~> .K
23+
┃ │ function: foo
24+
┃ │
25+
┃ ┊ constraint: true
26+
┃ ┊ subst: ...
27+
┃ └─ 2 (leaf, target, terminal)
28+
┃ #EndProgram ~> .K
29+
┃
30+
┗━━┓ subst: .Subst
31+
┃ constraint:
32+
┃ notBool 1 ==Int ARG_UINT1:Int
33+
│
34+
├─ 5
35+
│ #selectBlock ( switchTargets ( ... branches: branch ( 1 , basicBlockIdx ( 3 ) )
36+
│ function: foo
37+
│
38+
│ (1 step)
39+
├─ 7 (split)
40+
│ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 2 ) )
41+
│ function: foo
42+
┃
43+
┃ (branch)
44+
┣━━┓ subst: .Subst
45+
┃ ┃ constraint:
46+
┃ ┃ ARG_UINT1:Int ==Int 2
47+
┃ │
48+
┃ ├─ 8
49+
┃ │ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 2 ) )
50+
┃ │ function: foo
51+
┃ │
52+
┃ │ (33 steps)
53+
┃ ├─ 10 (terminal)
54+
┃ │ #EndProgram ~> .K
55+
┃ │ function: foo
56+
┃ │
57+
┃ ┊ constraint: true
58+
┃ ┊ subst: ...
59+
┃ └─ 2 (leaf, target, terminal)
60+
┃ #EndProgram ~> .K
61+
┃
62+
┗━━┓ subst: .Subst
63+
┃ constraint:
64+
┃ notBool 2 ==Int ARG_UINT1:Int
65+
│
66+
├─ 9
67+
│ #selectBlock ( switchTargets ( ... branches: branch ( 2 , basicBlockIdx ( 2 ) )
68+
│ function: foo
69+
│
70+
│ (19 steps)
71+
├─ 11 (terminal)
72+
│ #EndProgram ~> .K
73+
│ function: foo
74+
│
75+
┊ constraint: true
76+
┊ subst: ...
77+
└─ 2 (leaf, target, terminal)
78+
#EndProgram ~> .K
79+
80+
81+
82+
83+
STATISTICS
84+
-----------
85+
Total nodes: 10
86+
87+
Node roles (exclusive):
88+
target : 1 ids: 2
89+
terminal: 3 ids: 6, 10, 11
90+
split : 2 ids: 3, 7
91+
normal : 4 ids: 4, 5, 8, 9
92+
(root nodes omitted from totals: 1)
93+
94+
Leaf paths from init:
95+
total leaves (non-root): 1
96+
reachable leaves : 1
97+
total steps : 33
98+
99+
leaf 2 (path 1/3): steps 33, path 1 -> 3 -> 5 -> 7 -> 9 -> 11 -> 2
100+
leaf 2 (path 2/3): steps 46, path 1 -> 3 -> 4 -> 6 -> 2
101+
leaf 2 (path 3/3): steps 47, path 1 -> 3 -> 5 -> 7 -> 8 -> 10 -> 2
102+
103+
LEAF <k> CELLS
104+
---------------
105+
Node 2:
106+
#EndProgram ~> .K

‎kmir/src/tests/integration/test_cli.py‎

Lines changed: 28 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,13 +4,14 @@
44
from pathlib import Path
55
from typing import TYPE_CHECKING
66

7+
import pytest
8+
79
from kmir.__main__ import _kmir_info, _kmir_link, _kmir_prune, _kmir_show
810
from kmir.options import InfoOpts, LinkOpts, ProveRSOpts, PruneOpts, ShowOpts
911
from kmir.smir import SMIRInfo
1012
from kmir.testing.fixtures import assert_or_update_show_output
1113

1214
if TYPE_CHECKING:
13-
import pytest
1415
from pyk.proof import APRProof
1516

1617
from kmir.kmir import KMIR
@@ -69,12 +70,33 @@ def test_cli_show_printers_snapshot(
6970
)
7071

7172

73+
@pytest.mark.parametrize(
74+
'src,start_symbol,is_smir',
75+
[
76+
pytest.param(
77+
(PROVE_RS_DIR / 'symbolic-args-fail.rs'),
78+
'main',
79+
False,
80+
id='symbolic-args-fail.main',
81+
),
82+
pytest.param(
83+
(Path(__file__).parent / 'data' / 'exec-smir' / 'niche-enum' / 'niche-enum.smir.json').resolve(strict=True),
84+
'foo',
85+
True,
86+
id='niche-enum.smir.foo',
87+
),
88+
],
89+
)
7290
def test_cli_show_statistics_and_leaves(
73-
kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str], update_expected_output: bool
91+
src: Path,
92+
start_symbol: str,
93+
is_smir: bool,
94+
kmir: KMIR,
95+
tmp_path: Path,
96+
capsys: pytest.CaptureFixture[str],
97+
update_expected_output: bool,
7498
) -> None:
75-
rs_file = PROVE_RS_DIR / 'symbolic-args-fail.rs'
76-
start_symbol = 'main'
77-
apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False)
99+
apr_proof = _prove_and_store(kmir, src, tmp_path, start_symbol=start_symbol, is_smir=is_smir)
78100

79101
show_opts = ShowOpts(
80102
proof_dir=tmp_path,
@@ -91,7 +113,7 @@ def test_cli_show_statistics_and_leaves(
91113

92114
assert_or_update_show_output(
93115
out,
94-
PROVE_RS_DIR / f'show/{rs_file.stem}.{start_symbol}.cli-stats-leaves.expected',
116+
PROVE_RS_DIR / f'show/{src.stem}.{start_symbol}.cli-stats-leaves.expected',
95117
update=update_expected_output,
96118
)
97119

0 commit comments

Comments
 (0)