test(integration): add thunk frontier red baselines and shows

Author: Stevengre

kmir/src/tests/integration/data/prove-rs/closure-fnonce-single-arg.rs

@@ -0,0 +1,12 @@
+fn apply<F: FnOnce(u8) -> u8>(f: F, v: u8) -> u8 {
+    f(v)
+}
+
+fn main() {
+    let _ = repro();
+}
+
+fn repro() -> u8 {
+    let f = |x: u8| x + 1;
+    apply(f, 41u8)
+}

kmir/src/tests/integration/data/prove-rs/iter-copied-take-next-thunk-regression.rs

@@ -0,0 +1,19 @@
+#[derive(Copy, Clone)]
+struct Pubkey([u8; 32]);
+
+fn main() {
+    let _keep: fn(usize) -> u8 = repro;
+}
+
+#[no_mangle]
+pub fn repro(n: usize) -> u8 {
+    let keys = [Pubkey([1; 32]); 11];
+    let mut it = keys.iter().take(n).copied();
+
+    if 1 <= n && n <= 11 {
+        let first = it.next().unwrap();
+        first.0[0]
+    } else {
+        0
+    }
+}

kmir/src/tests/integration/data/prove-rs/iter-map-eq-copied-take-thunk-frontier-fail.rs

@@ -0,0 +1,21 @@
+const TAKE_N: usize = 3;
+
+fn main() {
+    let _keep: fn(&[AccountInfo<'_>; 5], [Pubkey; 11]) -> bool = repro;
+}
+
+#[no_mangle]
+pub fn repro(accounts: &[AccountInfo<'_>; 5], signers: [Pubkey; 11]) -> bool {
+    accounts[2..]
+        .iter()
+        .map(|signer| *signer.key)
+        .eq(signers.iter().take(TAKE_N).copied())
+}
+
+#[derive(Clone)]
+struct AccountInfo<'a> {
+    key: &'a Pubkey,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+struct Pubkey([u8; 32]);

kmir/src/tests/integration/data/prove-rs/show/closure-fnonce-single-arg.repro.expected

@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (126 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+

kmir/src/tests/integration/data/prove-rs/show/iter-copied-take-next-thunk-regression.repro.expected

@@ -0,0 +1,72 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (337 steps)
+├─ 3 (split)
+│   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+┃
+┃ (branch)
+┣━━┓ subst: .Subst
+┃  ┃ constraint:
+┃  ┃     notBool 1 <=Int ARG_UINT1:Int
+┃  │
+┃  ├─ 4
+┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+┃  │
+┃  │  (17 steps)
+┃  ├─ 6 (terminal)
+┃  │   #EndProgram ~> .K
+┃  │
+┃  ┊  constraint: true
+┃  ┊  subst: ...
+┃  └─ 2 (leaf, target, terminal)
+┃      #EndProgram ~> .K
+┃
+┗━━┓ subst: .Subst
+   ┃ constraint:
+   ┃     1 <=Int ARG_UINT1:Int
+   │
+   ├─ 5
+   │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+   │
+   │  (27 steps)
+   ├─ 7 (split)
+   │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+   ┃
+   ┃ (branch)
+   ┣━━┓ subst: .Subst
+   ┃  ┃ constraint:
+   ┃  ┃     notBool ARG_UINT1:Int <=Int 11
+   ┃  │
+   ┃  ├─ 8
+   ┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+   ┃  │
+   ┃  │  (17 steps)
+   ┃  ├─ 10 (terminal)
+   ┃  │   #EndProgram ~> .K
+   ┃  │
+   ┃  ┊  constraint: true
+   ┃  ┊  subst: ...
+   ┃  └─ 2 (leaf, target, terminal)
+   ┃      #EndProgram ~> .K
+   ┃
+   ┗━━┓ subst: .Subst
+      ┃ constraint:
+      ┃     ARG_UINT1:Int <=Int 11
+      │
+      ├─ 9
+      │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 9 ) )
+      │
+      │  (706 steps)
+      ├─ 11 (terminal)
+      │   #EndProgram ~> .K
+      │
+      ┊  constraint: true
+      ┊  subst: ...
+      └─ 2 (leaf, target, terminal)
+          #EndProgram ~> .K
+
+
+

kmir/src/tests/integration/data/prove-rs/show/iter-map-eq-copied-take-thunk-frontier-fail.repro.expected

@@ -0,0 +1,15 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (867 steps)
+└─ 3 (stuck, leaf)
+    ListItem ( thunk ( #decodeConstant ( constantKindZeroSized , ty ( 88 ) , typeInf
+    span: 273
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+

kmir/src/tests/integration/test_integration.py

@@ -38,6 +38,9 @@
     'assume-cheatcode-conflict-fail': ['check_assume_conflict'],
     'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
     'test_offset_from-fail': ['testing'],
+    'closure-fnonce-single-arg': ['repro'],
+    'iter-copied-take-next-thunk-regression': ['repro'],
+    'iter-map-eq-copied-take-thunk-frontier-fail': ['repro'],
 }
 PROVE_RS_SHOW_SPECS = [
     'local-raw-fail',
@@ -65,6 +68,9 @@
     'ref-ptr-cast-elem-offset-fail',
     'and_then_closure-fail',
     'closure_access_struct-fail',
+    'closure-fnonce-single-arg',
+    'iter-copied-take-next-thunk-regression',
+    'iter-map-eq-copied-take-thunk-frontier-fail',
 ]