test(prove-rs): add subslice-drop-unsupported-fail repro

Add integration test for Subslice projection on an owned array of Drop
types. The `let [first, rest @ ..]` pattern generates a Subslice that
changes the type from [Droppable; 3] to [Droppable; 2], exercising an
unsupported code path in _projected_ty() and K semantics.

Marked as expected-fail with show snapshot.

Author: Stevengre

kmir/src/tests/integration/data/prove-rs/show/subslice-drop-unsupported-fail.main.expected

@@ -0,0 +1,56 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (90 steps)
+├─ 3
+│   #setLocalValue ( place ( ... local: local ( 1 ) , projection: .ProjectionElems )
+│   function: main
+│   span: 64
+│
+│  (4 steps)
+├─ 4
+│   #execStmt ( statement ( ... kind: statementKindAssign ( ... place: place ( ... l
+│   function: main
+│   span: 64
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 5
+┃  │   #setLocalValue ( place ( ... local: local ( 7 ) , projection: .ProjectionElems )
+┃  │   function: main
+┃  │   span: 54
+┃  │
+┃  │  (2 steps)
+┃  └─ 8 (vacuous, leaf)
+┃      operandCopy ( place ( ... local: local ( 5 ) , projection: projectionElemField (
+┃      function: main
+┃      span: 54
+┃
+┣━━┓
+┃  │
+┃  ├─ 6
+┃  │   #setLocalValue ( place ( ... local: local ( 7 ) , projection: .ProjectionElems )
+┃  │   function: main
+┃  │   span: 54
+┃  │
+┃  │  (1 step)
+┃  └─ 9 (vacuous, leaf)
+┃      #evalUnion ( rvalueUse ( operandCopy ( place ( ... local: local ( 5 ) , projecti
+┃      function: main
+┃      span: 54
+┃
+┗━━┓
+   │
+   └─ 7 (stuck, leaf)
+       #execStmt ( statement ( ... kind: statementKindAssign ( ... place: place ( ... l
+       function: main
+       span: 64
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+

kmir/src/tests/integration/data/prove-rs/subslice-drop-unsupported-fail.rs

@@ -0,0 +1,21 @@
+// Reproducer: Subslice projection on an array of Drop types.
+//
+// `let [first, rest @ ..] = arr` generates a Subslice projection that
+// changes the type from [Droppable; 3] to [Droppable; 2]. The SMIR
+// linker's _projected_ty() currently returns the original array type
+// for Subslice, which could cause drop-glue mis-resolution when
+// Subslice projections appear in Drop terminator places.
+
+struct Droppable(u8);
+
+impl Drop for Droppable {
+    fn drop(&mut self) {}
+}
+
+fn main() {
+    let arr = [Droppable(1), Droppable(2), Droppable(3)];
+    let [first, rest @ ..] = arr;
+    assert!(first.0 == 1);
+    assert!(rest[0].0 == 2);
+    assert!(rest[1].0 == 3);
+}

kmir/src/tests/integration/test_integration.py

@@ -70,6 +70,7 @@
     'ptr-cast-array-to-nested-wrapper-fail',
     'ptr-cast-array-to-singleton-wrapped-array-fail',
     'iterator-simple-fail',
+    'subslice-drop-unsupported-fail',
 ]
 
 

kmir/src/tests/unit/test_smir.py

@@ -258,3 +258,110 @@ def test_drop_function_tys_accept_core_drop_in_place_names() -> None:
     )
 
     assert smir_info.drop_function_tys == {2: 12}
+
+
+def test_call_edges_preserve_drop_glue_for_subslice_projection() -> None:
+    # This SMIR models:
+    #   local 1: [Inner; 3]   (ty 1, ArrayType with elem_type 2)
+    #   Drop(local 1 . Subslice { from: 1, to: 3, from_end: false })
+    #
+    # The Subslice produces [Inner; 2] (ty 5), NOT the original [Inner; 3].
+    # _projected_ty() currently returns the original array type (ty 1),
+    # so drop_in_place::<[Inner; 2]> is not found and the edge is lost.
+    smir_info = SMIRInfo(
+        {
+            'name': 'drop-subslice',
+            'allocs': [],
+            'types': [
+                [1, {'ArrayType': {'elem_type': 2, 'size': None}}],  # [Inner; 3]
+                [
+                    2,
+                    {
+                        'StructType': {
+                            'name': 'Inner',
+                            'adt_def': 2,
+                            'fields': [],
+                            'layout': None,
+                        }
+                    },
+                ],
+                [3, {'PtrType': {'pointee_type': 2}}],
+                [5, {'ArrayType': {'elem_type': 2, 'size': None}}],  # [Inner; 2]
+                [6, {'PtrType': {'pointee_type': 5}}],
+            ],
+            'functions': [
+                [10, {'NormalSym': 'caller'}],
+                [12, {'NormalSym': 'drop_inner'}],
+                [14, {'NormalSym': 'drop_inner_array2'}],
+            ],
+            'items': [
+                {
+                    'symbol_name': 'caller',
+                    'mono_item_kind': {
+                        'MonoItemFn': {
+                            'name': 'caller',
+                            'body': {
+                                'arg_count': 0,
+                                'locals': [{'ty': 0}, {'ty': 1}],
+                                'blocks': [
+                                    {
+                                        'terminator': {
+                                            'kind': {
+                                                'Drop': {
+                                                    'place': {
+                                                        'local': 1,
+                                                        'projection': [
+                                                            {'Subslice': {'from': 1, 'to': 3, 'from_end': False}}
+                                                        ],
+                                                    },
+                                                    'target': 0,
+                                                    'unwind': 'Continue',
+                                                }
+                                            }
+                                        }
+                                    }
+                                ],
+                            },
+                        }
+                    },
+                },
+                {
+                    'symbol_name': 'drop_inner',
+                    'mono_item_kind': {
+                        'MonoItemFn': {
+                            'name': 'std::ptr::drop_in_place::<Inner>',
+                            'body': {
+                                'arg_count': 1,
+                                'locals': [{'ty': 0}, {'ty': 3}],
+                                'blocks': [],
+                            },
+                        }
+                    },
+                },
+                {
+                    'symbol_name': 'drop_inner_array2',
+                    'mono_item_kind': {
+                        'MonoItemFn': {
+                            'name': 'std::ptr::drop_in_place::<[Inner; 2]>',
+                            'body': {
+                                'arg_count': 1,
+                                'locals': [{'ty': 0}, {'ty': 6}],
+                                'blocks': [],
+                            },
+                        }
+                    },
+                },
+            ],
+            'spans': [],
+        }
+    )
+
+    # BUG: _projected_ty returns ty 1 ([Inner; 3]) for the Subslice, so
+    # call_edges looks up drop_function_tys[1] instead of [5]. Since
+    # drop_in_place::<[Inner; 3]> doesn't exist (only drop_in_place::<[Inner; 2]>
+    # does), the edge is lost.
+    #
+    # When this is fixed, the assertion should become:
+    #   assert smir_info.call_edges == {10: {14}, 12: set(), 14: set()}
+    # For now, document the current (buggy) behavior:
+    assert smir_info.call_edges == {10: set(), 12: set(), 14: set()}