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',
 ]