Improved show printing for leaves (#946)

### Short Version

This PR:
- Threads `Span`s through to `#setUpCalleeData` instead of being ignored
from the `Terminator`
- Modifies the python utility code that prints leaves for `kmir show
--leaves` to print function, call site, and error messages when possible
for `panic` and `assert_failed`
- Adds the ability to truncate a path for testing so CI is deterministic

### Long Version

In the event that a `panic` or `assert_failed` is reached in a proof, a
stuck leaf node will be present in the KCFG that calls `** UNKNOWN
FUNCTION **`. It is not clear exactly which function is being called,
where this is being called from, or what the error message is (if there
is one) as all the information is represented as interned data (`DefId`,
`Span`, `AllocId`).

The print out of the failing nodes is improved for `kmir show --leaves`
from:
```
Node 3:
  #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) )  .Operands) ~> .K
```
to:
```
Node 3:
  #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) )  .Operands , span ( 117 ) ) ~> .K
  >> function: core::panicking::panic::h941160ead03e2d54
  >> call span: /home/daniel/Applications/mir-semantics/kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs:53:5
  >> message: 'assertion failed: false'
``` 

This is achieved by taking advantage of the deterministic location of
the interned values, retrieving those values, and then consulting the
`.smir.json` to get the un-interned data associated with those interned
values.

Author: dkcumming

kmir/src/kmir/__main__.py

@@ -180,7 +180,7 @@ def _kmir_show(opts: ShowOpts) -> None:
     if opts.leaves:
         if lines and lines[-1] != '':
             lines.append('')
-        lines.extend(render_leaf_k_cells(proof, node_printer.cterm_show))
+        lines.extend(render_leaf_k_cells(proof, node_printer.cterm_show, smir_info=node_printer.smir_info))
 
     # Handle --to-module output
     if opts.to_module:

kmir/src/kmir/kdist/mir-semantics/intrinsics.md

@@ -23,7 +23,7 @@ its argument to the destination without modification.
 
 ```k
   // Black box intrinsic implementation - identity function
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("black_box")), ARG:Operand .Operands, DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("black_box")), ARG:Operand .Operands, DEST, _SPAN)
         => #setLocalValue(DEST, ARG)
        ... </k>
 ```
@@ -36,7 +36,7 @@ a NO OP for program semantics. `std::intrinsics::likely` and `std::intrinsics::u
 "normal" `MonoItemFn`s that call the `cold_path` intrinsic.
 
 ```k
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("cold_path")), .Operands, _DEST) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("cold_path")), .Operands, _DEST, _SPAN) => .K ... </k>
 ```
 
 #### Prefetch (`std::intrinsics::prefetch_*`)
@@ -46,11 +46,11 @@ intrinsics in Rust are performance hints that request the CPU to load or prepare
 before it's used. They have no effect on program semantics, and are implemented as a NO OP in this semantics.
 
 ```k
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_data")),  _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_data")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_data")),  _ARG1:Operand _ARG2:Operand .Operands, _DEST, _SPAN) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_data")), _ARG1:Operand _ARG2:Operand .Operands, _DEST, _SPAN) => .K ... </k>
 
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_instruction")),  _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_read_instruction")),  _ARG1:Operand _ARG2:Operand .Operands, _DEST, _SPAN) => .K ... </k>
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("prefetch_write_instruction")), _ARG1:Operand _ARG2:Operand .Operands, _DEST, _SPAN) => .K ... </k>
 ```
 
 #### Assert Inhabited (`std::intrinsics::assert_inhabited`)
@@ -63,13 +63,13 @@ error with `#AssertInhabitedFailure` if we see that following the intrinsic. Oth
 
 ```k
   syntax MIRError ::= "AssertInhabitedFailure"
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST, _SPAN)
             ~> #continueAt(noBasicBlockIdx)
         => AssertInhabitedFailure
        ...
       </k>
 
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("assert_inhabited")), .Operands, _DEST, _SPAN)
         => .K
        ...
       </k>
@@ -88,7 +88,7 @@ Execution gets stuck (no matching rule) when operands have different types or un
 
 ```k
   // Raw eq: dereference operands, extract types, and delegate to typed comparison
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("raw_eq")), ARG1:Operand ARG2:Operand .Operands, PLACE)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("raw_eq")), ARG1:Operand ARG2:Operand .Operands, PLACE, _SPAN)
         => #execRawEqTyped(PLACE, #withDeref(ARG1), #extractOperandType(#withDeref(ARG1), LOCALS),
                                   #withDeref(ARG2), #extractOperandType(#withDeref(ARG2), LOCALS))
        ... </k>
@@ -134,11 +134,11 @@ through a dereferenced pointer. We extract the place from the pointer operand, a
 write the value to that location.
 
 ```k
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandCopy(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandCopy(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST, _SPAN)
         => #setLocalValue(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)), ARG2)
        ... </k>
 
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandMove(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_store")), operandMove(place(LOCAL, PROJ)) ARG2:Operand .Operands, _DEST, _SPAN)
         => #setLocalValue(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems)), ARG2)
        ... </k>
 ```
@@ -153,12 +153,12 @@ the second argument, so the returned difference is always positive.
 
 
 ```k
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from")), ARG1:Operand ARG2:Operand .Operands, DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from")), ARG1:Operand ARG2:Operand .Operands, DEST, _SPAN)
         => #ptrOffsetDiff(ARG1, ARG2, true, DEST)
         ...
        </k>
 
-  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from_unsigned")), ARG1:Operand ARG2:Operand .Operands, DEST)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("ptr_offset_from_unsigned")), ARG1:Operand ARG2:Operand .Operands, DEST, _SPAN)
         => #ptrOffsetDiff(ARG1, ARG2, false, DEST)
         ...
        </k>

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -306,30 +306,30 @@ The call stack is not necessarily empty at this point so it is left untouched.
 where the returned result should go.
 
 ```k
-  syntax KItem ::= #execTerminatorCall(fty: Ty, func: MonoItemKind, args: Operands, destination: Place, target: MaybeBasicBlockIdx, unwind: UnwindAction)
+  syntax KItem ::= #execTerminatorCall(fty: Ty, func: MonoItemKind, args: Operands, destination: Place, target: MaybeBasicBlockIdx, unwind: UnwindAction, Span)
 
-  rule <k> #execTerminator(terminator(terminatorKindCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _))), ARGS, DEST, TARGET, UNWIND), _SPAN))
-        => #execTerminatorCall(Ty, lookupFunction(Ty), ARGS, DEST, TARGET, UNWIND)
+  rule <k> #execTerminator(terminator(terminatorKindCall(operandConstant(constOperand(_, _, mirConst(constantKindZeroSized, Ty, _))), ARGS, DEST, TARGET, UNWIND), SPAN))
+        => #execTerminatorCall(Ty, lookupFunction(Ty), ARGS, DEST, TARGET, UNWIND, SPAN)
         ...
        </k>
 
-  rule <k> #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), .ProjectionElems)), ARGS, DEST, TARGET, UNWIND), _SPAN))
-        => #execTerminatorCall(tyOfLocal(getLocal(LOCALS, I)), lookupFunction(tyOfLocal(getLocal(LOCALS, I))), ARGS, DEST, TARGET, UNWIND)
+  rule <k> #execTerminator(terminator(terminatorKindCall(operandMove(place(local(I), .ProjectionElems)), ARGS, DEST, TARGET, UNWIND), SPAN))
+        => #execTerminatorCall(tyOfLocal(getLocal(LOCALS, I)), lookupFunction(tyOfLocal(getLocal(LOCALS, I))), ARGS, DEST, TARGET, UNWIND, SPAN)
         ...
        </k>
       <locals> LOCALS </locals>
 
   // Intrinsic function call - execute directly without state switching
   rule [termCallIntrinsic]:
-        <k> #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND) ~> _
-         => #execIntrinsic(FUNC, ARGS, DEST) ~> #continueAt(TARGET)
+        <k> #execTerminatorCall(_, FUNC, ARGS, DEST, TARGET, _UNWIND, SPAN) ~> _
+         => #execIntrinsic(FUNC, ARGS, DEST, SPAN) ~> #continueAt(TARGET)
         </k>
     requires isIntrinsicFunction(FUNC)
 
   // Regular function call - full state switching and stack setup
   rule [termCallFunction]:
-       <k> #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND) ~> _
-        => #setUpCalleeData(FUNC, ARGS)
+       <k> #execTerminatorCall(FTY, FUNC, ARGS, DEST, TARGET, UNWIND, SPAN) ~> _
+        => #setUpCalleeData(FUNC, ARGS, SPAN)
        </k>
        <currentFunc> CALLER => FTY </currentFunc>
        <currentFrame>
@@ -357,12 +357,13 @@ The local data has to be set up for the call, which requires information about t
 An operand may be a `Reference` (the only way a function could access another function call's `local` variables). For this case, the stack height in the `Reference` must be incremented because a stack frame is added.
 
 ```k
-  syntax KItem ::= #setUpCalleeData(MonoItemKind, Operands)
+  syntax KItem ::= #setUpCalleeData(MonoItemKind, Operands, Span)
 
   // reserve space for local variables and copy/move arguments from old locals into their place
   rule [setupCalleeData]: <k> #setUpCalleeData(
               monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))),
-              ARGS
+              ARGS,
+              _SPAN
               )
          =>
            #setArgsFromStack(1, ARGS) ~> #execBlock(FIRST)
@@ -391,7 +392,7 @@ An operand may be a `Reference` (the only way a function could access another fu
 
   syntax KItem ::= #setArgsFromStack ( Int, Operands)
                  | #setArgFromStack ( Int, Operand)
-                 | #execIntrinsic ( MonoItemKind, Operands, Place )
+                 | #execIntrinsic ( MonoItemKind, Operands, Place, Span )
 
   // once all arguments have been retrieved, execute
   rule <k> #setArgsFromStack(_, .Operands) ~> CONT => CONT </k>
@@ -453,7 +454,8 @@ Therefore a heuristics is used here:
               monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))),
                 operandMove(place(local(CLOSURE:Int), .ProjectionElems))
                 operandMove(place(local(TUPLE), .ProjectionElems))
-                .Operands
+                .Operands,
+                _SPAN
               )
          =>
            #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST)
@@ -482,7 +484,8 @@ Therefore a heuristics is used here:
               monoItemFn(_, _, someBody(body((FIRST:BasicBlock _) #as BLOCKS, NEWLOCALS, _, _, _, _))),
                 operandMove(place(local(CLOSURE:Int), .ProjectionElems))
                 operandMove(place(local(TUPLE), .ProjectionElems))
-                .Operands
+                .Operands,
+                _SPAN
               )
          =>
            #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST)

kmir/src/kmir/testing/fixtures.py

@@ -20,7 +20,12 @@ def pytest_configure(config) -> None:
     sys.setrecursionlimit(1000000)
 
 
-def assert_or_update_show_output(actual_text: str, expected_file: Path, *, update: bool) -> None:
+def assert_or_update_show_output(
+    actual_text: str, expected_file: Path, *, update: bool, path_replacements: dict[str, str] | None = None
+) -> None:
+    if path_replacements:
+        for old, new in path_replacements.items():
+            actual_text = actual_text.replace(old, new)
     if update:
         expected_file.write_text(actual_text)
     else:

kmir/src/kmir/utils.py

@@ -4,11 +4,16 @@
 from pathlib import Path
 from typing import TYPE_CHECKING, Sequence
 
+from pyk.kast.inner import KApply, KLabel, KSequence, KToken
+
 if TYPE_CHECKING:
     from pyk.cterm.show import CTermShow
+    from pyk.kast.inner import KInner
     from pyk.kcfg.kcfg import KCFG
     from pyk.proof.reachability import APRProof
 
+    from .smir import SMIRInfo
+
 
 def _rule_to_markdown_link(rule: object) -> str:
     """Render a single rule as a Markdown file link if possible.
@@ -231,7 +236,123 @@ def _path_nodes(source_id: int, path: Sequence[KCFG.Successor]) -> list[int]:
     return lines
 
 
-def render_leaf_k_cells(proof: APRProof, cterm_show: CTermShow) -> list[str]:
+def _drill(term: KInner, *path: tuple[str, int]) -> KInner | None:
+    """Navigate a nested KApply by a sequence of (label_name, arg_index) steps.
+
+    Returns the nested KInner at the end of the path, or None if any step
+    doesn't match (wrong label, insufficient args, or not a KApply).
+    """
+
+    current: KInner = term
+    for label, index in path:
+        match current:
+            case KApply(label=KLabel(name=name), args=args) if name == label and index < len(args):
+                current = args[index]
+            case _:
+                return None
+    return current
+
+
+def _extract_alloc_id(operands: KInner) -> int | None:
+    """Extract allocId from the first constant operand's provenance, if present."""
+
+    const_operand = 'constOperand(_,_,_)_BODY_ConstOperand_Span_MaybeUserTypeAnnotationIndex_MirConst'
+    mir_const = 'mirConst(_,_,_)_TYPES_MirConst_ConstantKind_Ty_MirConstId'
+
+    ptrs = _drill(
+        operands,
+        ('Operands::append', 0),  # first operand
+        ('Operand::Constant', 0),  # constOperand
+        (const_operand, 2),  # mirConst  (3rd arg)
+        (mir_const, 0),  # ConstantKind::Allocated
+        ('ConstantKind::Allocated', 0),  # allocation
+        ('allocation', 1),  # provenanceMap  (2nd arg)
+        ('provenanceMap', 0),  # provenance entries
+    )
+    if ptrs is None:
+        return None
+
+    match ptrs:
+        case KApply(
+            label=KLabel(name='ProvenanceMapEntries::append'),
+            args=[
+                KApply(
+                    label=KLabel(name='provenanceMapEntry'),
+                    args=[_, KApply(label=KLabel(name='allocId'), args=[KToken(token=n)])],
+                ),
+                *_,
+            ],
+        ):
+            return int(n)
+        case _:
+            return None
+
+
+def _annotate_unknown_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]:
+    """If the k cell is `#setUpCalleeData` for `** UNKNOWN FUNCTION **`, return annotation lines with decoded info."""
+
+    from .alloc import Allocation, AllocId, AllocInfo, Memory
+    from .linker import _demangle
+
+    setup_call_label = '#setUpCalleeData(_,_,_)_KMIR-CONTROL-FLOW_KItem_MonoItemKind_Operands_Span'
+
+    annotations: list[str] = []
+
+    match k_cell:
+        case KSequence(items=(KApply(label=KLabel(name=label_name), args=args), *_)) | KApply(
+            label=KLabel(name=label_name), args=args
+        ) if (label_name == setup_call_label):
+            match args:
+                case [
+                    KApply(
+                        label=KLabel(name='MonoItemKind::MonoItemFn'),
+                        args=[
+                            KApply(args=[KToken(token=symbol_name)]),
+                            KApply(label=KLabel(name='defId(_)_BODY_DefId_Int'), args=[KToken(token=def_id_str)]),
+                            _,
+                        ],
+                    ),
+                    operands,
+                    KApply(label=KLabel(name='span'), args=[KToken(token=span_str)]),
+                ] if (
+                    symbol_name == '\"** UNKNOWN FUNCTION **\"'
+                ):
+                    def_id = int(def_id_str)
+                    span = int(span_str)
+                case _:
+                    return []
+        case _:
+            return []
+
+    # Use extracted DefId for function name
+    func_sym = smir_info.function_symbols.get(def_id, {})
+    if name := func_sym.get('NormalSym') or func_sym.get('IntrinsicSym'):
+        try:
+            name = _demangle(name)
+        except Exception:
+            pass
+        annotations.append(f'  >> function: {name}')
+
+    # Use extracted Span for call site
+    if span in smir_info.spans:
+        path, start_row, start_col, _, _ = smir_info.spans[span]
+        annotations.append(f'  >> call span: {path}:{start_row}:{start_col}')
+
+    # Extract allocId from provenance and try to decode the referenced string
+    alloc_id = _extract_alloc_id(operands)
+    if alloc_id is not None:
+        match smir_info.allocs.get(AllocId(alloc_id)):
+            case AllocInfo(global_alloc=Memory(allocation=Allocation(bytez=bytez))):
+                try:
+                    message = bytes(b for b in bytez if b is not None).decode('utf-8')
+                    annotations.append(f'  >> message: {message!r}')
+                except ValueError:
+                    pass
+
+    return annotations
+
+
+def render_leaf_k_cells(proof: APRProof, cterm_show: CTermShow, smir_info: SMIRInfo | None = None) -> list[str]:
     """Render the <k> cell for every leaf node in the proof."""
 
     leaves = sorted(
@@ -249,13 +370,18 @@ def render_leaf_k_cells(proof: APRProof, cterm_show: CTermShow) -> list[str]:
             k_cell = leaf.cterm.cell('K_CELL')
             k_lines = cterm_show.print_lines(k_cell)
         except KeyError:
+            k_cell = None
             k_lines = ['<K_CELL unavailable>']
 
         if not k_lines:
             lines.append('  (empty)')
         else:
             lines.extend(f'  {k_line}' for k_line in k_lines)
 
+        if smir_info is not None and k_cell is not None:
+            annotations = _annotate_unknown_function(k_cell, smir_info)
+            lines.extend(annotations)
+
         if idx != len(leaves) - 1:
             lines.append('')
 

kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected

@@ -32,4 +32,7 @@ Leaf paths from init:
 LEAF <k> CELLS
 ---------------
 Node 3:
-  #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) )  .Operands ) ~> .K
+  #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) )  .Operands , span ( 117 ) ) ~> .K
+  >> function: core::panicking::panic::h941160ead03e2d54
+  >> call span: <REPO>/kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs:53:5
+  >> message: 'assertion failed: false'

kmir/src/tests/integration/test_cli.py

@@ -17,6 +17,10 @@
     from kmir.kmir import KMIR
 
 PROVE_RS_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True)
+# Repo root: used to normalise absolute paths in expected-output snapshots so
+# they don't differ between local checkouts and CI (e.g. symbolic-args-fail.main.cli-stats-leaves).
+_REPO_ROOT = str(Path(__file__).resolve().parents[4])
+_PATH_REPLACEMENTS: dict[str, str] = {_REPO_ROOT + '/': '<REPO>/'}
 
 
 def _prove_and_store(
@@ -120,6 +124,7 @@ def test_cli_show_statistics_and_leaves(
         out,
         PROVE_RS_DIR / f'show/{src.stem}.{start_symbol}.cli-stats-leaves.expected',
         update=update_expected_output,
+        path_replacements=_PATH_REPLACEMENTS,
     )