refactor(tests): distinguish -fail from -unsupported, auto-detect show specs

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

@@ -0,0 +1,107 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: src/rust/library/std/src/rt.rs:194
+│
+│  (61 steps)
+├─ 3 (split)
+│   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
+│   function: eats_struct_args
+┃
+┃ (branch)
+┣━━┓ subst: .Subst
+┃  ┃ constraint:
+┃  ┃     notBool ARG_INT2:Int ==Int ARG_INT5:Int
+┃  │
+┃  ├─ 4
+┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
+┃  │   function: eats_struct_args
+┃  │
+┃  │  (96 steps)
+┃  ├─ 6 (split)
+┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 5 ) )
+┃  │   function: eats_struct_args
+┃  ┃
+┃  ┃ (branch)
+┃  ┣━━┓ subst: .Subst
+┃  ┃  ┃ constraint:
+┃  ┃  ┃     ARG_UINT3:Int ==Int ARG_UINT6:Int
+┃  ┃  │
+┃  ┃  ├─ 8
+┃  ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 5 ) )
+┃  ┃  │   function: eats_struct_args
+┃  ┃  │
+┃  ┃  │  (6 steps)
+┃  ┃  └─ 10 (stuck, leaf)
+┃  ┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>
+┃  ┃      span: no-location:0
+┃  ┃
+┃  ┗━━┓ subst: .Subst
+┃     ┃ constraint:
+┃     ┃     notBool ARG_UINT3:Int ==Int ARG_UINT6:Int
+┃     │
+┃     ├─ 9
+┃     │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 5 ) )
+┃     │   function: eats_struct_args
+┃     │
+┃     │  (6 steps)
+┃     ├─ 11 (terminal)
+┃     │   #EndProgram ~> .K
+┃     │   function: eats_struct_args
+┃     │
+┃     ┊  constraint: true
+┃     ┊  subst: ...
+┃     └─ 2 (leaf, target, terminal)
+┃         #EndProgram ~> .K
+┃
+┗━━┓ subst: .Subst
+   ┃ constraint:
+   ┃     ARG_INT2:Int ==Int ARG_INT5:Int
+   │
+   ├─ 5
+   │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 2 ) )
+   │   function: eats_struct_args
+   │
+   │  (66 steps)
+   ├─ 7 (terminal)
+   │   #EndProgram ~> .K
+   │   function: eats_struct_args
+   │
+   ┊  constraint: true
+   ┊  subst: ...
+   └─ 2 (leaf, target, terminal)
+       #EndProgram ~> .K
+
+
+
+
+STATISTICS
+-----------
+Total nodes: 10
+
+Node roles (exclusive):
+  target  : 1  ids: 2
+  terminal: 2  ids: 7, 11
+  failing : 1  ids: 10
+  split   : 2  ids: 3, 6
+  normal  : 4  ids: 4, 5, 8, 9
+  (root nodes omitted from totals: 1)
+
+Leaf paths from init:
+  total leaves (non-root): 2
+  reachable leaves       : 2
+  total steps            : 290
+
+  leaf 2 (path 1/2): steps 127, path 1 -> 3 -> 5 -> 7 -> 2
+  leaf 2 (path 2/2): steps 163, path 1 -> 3 -> 4 -> 6 -> 9 -> 11 -> 2
+  leaf 10: steps 163, path 1 -> 3 -> 4 -> 6 -> 8 -> 10
+
+LEAF <k> CELLS
+---------------
+Node 2:
+  #EndProgram ~> .K
+
+Node 10:
+  #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>E" ) , id: defId ( 27 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x008\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 0 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 28 ) , id: mirConstId ( 12 ) ) ) )  .Operands , span ( 65 ) ) ~> .K
+  >> function: core::panicking::panic::h<hash>
+  >> call span: <REPO>/kmir/src/tests/integration/data/prove-rs/symbolic-structs-fail.rs:29:5

kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs → kmir/src/tests/integration/data/prove-rs/symbolic-args-unsupported.rs

@@ -49,6 +49,4 @@ fn main() {
     let mut a1 = [1, 2, 3];
     let a2 = [1, 2, 3];
     eats_all_args(1, &mut x2, true, my1, e4, &mut a1, &a2, &mut [my2, my3], &my4 as *const MyStruct<'_>);
-
-    assert!(false); // makes the test with main fail, as the other one also fails
 }

kmir/src/tests/integration/test_cli.py

@@ -19,7 +19,7 @@
 PROVE_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True)
 MODULES_DIR = (Path(__file__).parent / 'data' / 'modules').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).
+# they don't differ between local checkouts and CI (e.g. symbolic-structs-fail.eats_struct_args.cli-stats-leaves).
 _REPO_ROOT = str(Path(__file__).resolve().parents[4])
 _PATH_REPLACEMENTS: dict[str, str] = {_REPO_ROOT + '/': '<REPO>/'}
 
@@ -84,10 +84,10 @@ def test_cli_show_printers_snapshot(
     'src,start_symbol,is_smir',
     [
         pytest.param(
-            (PROVE_DIR / 'symbolic-args-fail.rs'),
-            'main',
+            (PROVE_DIR / 'symbolic-structs-fail.rs'),
+            'eats_struct_args',
             False,
-            id='symbolic-args-fail.main',
+            id='symbolic-structs-fail.eats_struct_args',
         ),
         pytest.param(
             (Path(__file__).parent / 'data' / 'exec-smir' / 'niche-enum' / 'niche-enum.smir.json').resolve(strict=True),
@@ -242,9 +242,9 @@ def test_cli_show_to_module(
 
 def test_cli_show_minimize_proof(kmir: KMIR, tmp_path: Path, capsys: pytest.CaptureFixture[str]) -> None:
     """Test --minimize-proof option."""
-    rs_file = PROVE_DIR / 'symbolic-args-fail.rs'
-    start_symbol = 'main'
-    # Use limited depth to create a partial proof with intermediate nodes that can be minimized
+    rs_file = PROVE_DIR / 'symbolic-structs-fail.rs'
+    start_symbol = 'eats_struct_args'
+    # Use a stable -fail test with symbolic branching so max_depth=5 creates intermediate nodes with splits
     apr_proof = _prove_and_store(kmir, rs_file, tmp_path, start_symbol=start_symbol, is_smir=False, max_depth=5)
 
     # Get initial node count

kmir/src/tests/integration/test_integration.py

@@ -28,63 +28,29 @@
 PROVE_DIR = (Path(__file__).parent / 'data' / 'prove-rs').resolve(strict=True)
 PROVE_FILES = list(PROVE_DIR.glob('*.*'))
 PROVE_START_SYMBOLS = {
-    'symbolic-args-fail': ['main', 'eats_all_args'],
+    'symbolic-args-unsupported': ['eats_all_args'],
     'symbolic-structs-fail': ['eats_struct_args'],
     'unchecked_arithmetic': ['unchecked_add_i32', 'unchecked_sub_usize', 'unchecked_mul_isize'],
     'checked_arithmetic-fail': ['checked_add_i32'],
     'pointer-cast': ['main', 'test'],
-    'pointer-cast-length-test-fail': ['array_cast_test'],
+    'pointer-cast-length-test-unsupported': ['array_cast_test'],
     'assume-cheatcode': ['check_assume'],
     'assume-cheatcode-conflict-fail': ['check_assume_conflict'],
     'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
     'test_offset_from-fail': ['testing'],
     'iter-eq-copied-take-dereftruncate': ['repro'],
     'spl-multisig-iter-eq-copied-next': ['repro'],
 }
-PROVE_SHOW_SPECS = [
-    'local-raw-fail',
-    'interior-mut-fail',
-    'interior-mut3-fail',
-    'iter_next_3',
-    'assert_eq_exp',
-    'bitwise-not-shift',
-    'symbolic-args-fail',
-    'symbolic-structs-fail',
-    'checked_arithmetic-fail',
-    'offset-u8-fail',
-    'pointer-cast-length-test-fail',
-    'niche-enum',
-    'assume-cheatcode-conflict-fail',
-    'raw-ptr-cast-fail',
-    'transmute-u8-to-enum-fail',
-    'assert-inhabited-fail',
-    'iterator-simple',
-    'unions-fail',
-    'transmute-maybe-uninit-fail',
-    'ptr-through-wrapper-fail',
-    'test_offset_from-fail',
-    'ref-ptr-cast-elem-fail',
-    'ref-ptr-cast-elem-offset-fail',
-    'volatile_store_static-fail',
-    'volatile_load_static-fail',
-    'box_heap_alloc-fail',
-    'ptr-cast-array-to-wrapper-fail',
-    'ptr-cast-array-to-nested-wrapper-fail',
-    'ptr-cast-array-to-singleton-wrapped-array-fail',
-]
-
-
 @pytest.mark.parametrize(
     'rs_file',
     PROVE_FILES,
     ids=[spec.stem for spec in PROVE_FILES],
 )
 def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None:
-    should_fail = rs_file.stem.endswith('fail')
-    should_show = rs_file.stem in PROVE_SHOW_SPECS
+    should_fail = rs_file.stem.endswith('fail') or rs_file.stem.endswith('unsupported')
     is_smir = rs_file.suffix == '.json'
 
-    if update_expected_output and not should_show:
+    if update_expected_output and not should_fail:
         pytest.skip()
 
     prove_opts = ProveOpts(rs_file, smir=is_smir, terminate_on_thunk=True)
@@ -99,7 +65,8 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None:
         prove_opts.start_symbol = start_symbol
         apr_proof = kmir.prove_program(prove_opts)
 
-        if should_show:
+        if should_fail:
+            assert apr_proof.failed
             display_opts = ShowOpts(
                 rs_file.parent, apr_proof.id, full_printer=False, smir_info=None, omit_current_body=False
             )
@@ -108,11 +75,8 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None:
             assert_or_update_show_output(
                 show_res, PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.expected', update=update_expected_output
             )
-
-        if not should_fail:
-            assert apr_proof.passed
         else:
-            assert apr_proof.failed
+            assert apr_proof.passed
 
 
 VERIFY_RUST_STD_DIR = (Path(__file__).parent / 'data' / 'verify-rust-std').resolve(strict=True)