Skip to content

Commit f38addb

Browse files
Stevengreclaudedkcumming
authored
test: enable --terminate-on-thunk for all prove tests (#1009)
## Summary - Make `--terminate-on-thunk` the default for all prove tests instead of per-test opt-in via `PROVE_TERMINATE_ON_THUNK` - This exposes unresolved thunks (from incomplete semantics) that were previously silently propagated through proof execution - All 110 prove tests pass with this change on master — no regressions - Update 13 show expected files whose proof trees changed due to earlier thunk termination ## Context First introduced in PR #813, `--terminate-on-thunk` makes the prover treat any `thunk(...)` in the K cell as a terminal state, immediately stopping proof exploration. Previously only `closure-staged` opted in. Enabling it globally ensures we catch any test that silently relies on thunk propagation. ## Test plan - [x] All 110 `test_prove` parametrizations pass locally - [x] CI passes 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com> Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>
1 parent 2d66d8f commit f38addb

14 files changed

Lines changed: 140 additions & 374 deletions

‎kmir/src/tests/integration/data/prove-rs/show/box_heap_alloc-fail.main.expected‎

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,15 @@
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
44
│ span: 0
55
│
6-
│ (199 steps)
7-
└─ 3 (stuck, leaf)
8-
#execIntrinsic ( IntrinsicFunction ( symbol ( "volatile_load" ) ) , operandConst
9-
span: 32
6+
│ (73 steps)
7+
├─ 3
8+
│ #cast ( Integer ( 4 , 64 , false ) , castKindTransmute , ty ( 29 ) , ty ( 50 ) )
9+
│ span: 186
10+
│
11+
│ (1 step)
12+
└─ 4 (leaf, terminal)
13+
thunk ( #cast ( Integer ( 4 , 64 , false ) , castKindTransmute , ty ( 29 ) , ty
14+
span: 186
1015

1116

1217
┌─ 2 (root, leaf, target, terminal)

‎kmir/src/tests/integration/data/prove-rs/show/interior-mut3-fail.main.expected‎

Lines changed: 12 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -3,61 +3,20 @@
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
44
│ span: 0
55
│
6-
│ (154 steps)
6+
│ (94 steps)
77
├─ 3
8-
│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
8+
│ #cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: projectionEl
99
│ function: main
10-
┃
11-
┃ (1 step)
12-
┣━━┓
13-
┃ │
14-
┃ ├─ 4
15-
┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
16-
┃ │ function: main
17-
┃ │
18-
┃ │ (1 step)
19-
┃ └─ 6 (stuck, leaf)
20-
┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
21-
┃ function: main
22-
┃
23-
┗━━┓
24-
│
25-
├─ 5
26-
│ #execBlockIdx ( basicBlockIdx ( 8 ) ) ~> .K
27-
│ function: main
28-
│
29-
│ (111 steps)
30-
├─ 7
31-
│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
32-
│ function: main
33-
┃
34-
┃ (1 step)
35-
┣━━┓
36-
┃ │
37-
┃ ├─ 8
38-
┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
39-
┃ │ function: main
40-
┃ │
41-
┃ │ (1 step)
42-
┃ └─ 10 (stuck, leaf)
43-
┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
44-
┃ function: main
45-
┃
46-
┗━━┓
47-
│
48-
├─ 9
49-
│ #execBlockIdx ( basicBlockIdx ( 7 ) ) ~> .K
50-
│ function: main
51-
│
52-
│ (66 steps)
53-
├─ 11 (terminal)
54-
│ #EndProgram ~> .K
55-
│ function: main
56-
│
57-
┊ constraint: true
58-
┊ subst: ...
59-
└─ 2 (leaf, target, terminal)
60-
#EndProgram ~> .K
10+
│ span: 73
11+
│
12+
│ (1 step)
13+
└─ 4 (leaf, terminal)
14+
thunk ( #cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: proj
15+
function: main
16+
span: 73
17+
6118

19+
┌─ 2 (root, leaf, target, terminal)
20+
│ #EndProgram ~> .K
6221

6322

‎kmir/src/tests/integration/data/prove-rs/show/local-raw-fail.main.expected‎

Lines changed: 12 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -3,38 +3,20 @@
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
44
│ span: 0
55
│
6-
│ (106 steps)
6+
│ (46 steps)
77
├─ 3
8-
│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
8+
│ #cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: projectionEl
99
│ function: main
10-
┃
11-
┃ (1 step)
12-
┣━━┓
13-
┃ │
14-
┃ ├─ 4
15-
┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
16-
┃ │ function: main
17-
┃ │
18-
┃ │ (1 step)
19-
┃ └─ 6 (stuck, leaf)
20-
┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
21-
┃ function: main
22-
┃
23-
┗━━┓
24-
│
25-
├─ 5
26-
│ #execBlockIdx ( basicBlockIdx ( 1 ) ) ~> .K
27-
│ function: main
28-
│
29-
│ (16 steps)
30-
├─ 7 (terminal)
31-
│ #EndProgram ~> .K
32-
│ function: main
33-
│
34-
┊ constraint: true
35-
┊ subst: ...
36-
└─ 2 (leaf, target, terminal)
37-
#EndProgram ~> .K
10+
│ span: 50
11+
│
12+
│ (1 step)
13+
└─ 4 (leaf, terminal)
14+
thunk ( #cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: proj
15+
function: main
16+
span: 50
17+
3818

19+
┌─ 2 (root, leaf, target, terminal)
20+
│ #EndProgram ~> .K
3921

4022

‎kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-fail.main.expected‎

Lines changed: 9 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -3,34 +3,17 @@
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
44
│ span: 0
55
│
6-
│ (128 steps)
6+
│ (68 steps)
77
├─ 3
8-
│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
8+
│ #cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: projectionEl
99
│ function: main
10-
┃
11-
┃ (1 step)
12-
┣━━┓
13-
┃ │
14-
┃ ├─ 4
15-
┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
16-
┃ │ function: main
17-
┃ │
18-
┃ │ (1 step)
19-
┃ └─ 6 (stuck, leaf)
20-
┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
21-
┃ function: main
22-
┃
23-
┗━━┓
24-
│
25-
├─ 5
26-
│ #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
27-
│ function: main
28-
│
29-
│ (11 steps)
30-
└─ 7 (stuck, leaf)
31-
#traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
32-
function: main
33-
span: 282
10+
│ span: 270
11+
│
12+
│ (1 step)
13+
└─ 4 (leaf, terminal)
14+
thunk ( #cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: proj
15+
function: main
16+
span: 270
3417

3518

3619
┌─ 2 (root, leaf, target, terminal)

‎kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-fail.main.expected‎

Lines changed: 9 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -3,34 +3,17 @@
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
44
│ span: 0
55
│
6-
│ (128 steps)
6+
│ (68 steps)
77
├─ 3
8-
│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
8+
│ #cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: projectionEl
99
│ function: main
10-
┃
11-
┃ (1 step)
12-
┣━━┓
13-
┃ │
14-
┃ ├─ 4
15-
┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
16-
┃ │ function: main
17-
┃ │
18-
┃ │ (1 step)
19-
┃ └─ 6 (stuck, leaf)
20-
┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
21-
┃ function: main
22-
┃
23-
┗━━┓
24-
│
25-
├─ 5
26-
│ #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
27-
│ function: main
28-
│
29-
│ (10 steps)
30-
└─ 7 (stuck, leaf)
31-
#traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
32-
function: main
33-
span: 282
10+
│ span: 270
11+
│
12+
│ (1 step)
13+
└─ 4 (leaf, terminal)
14+
thunk ( #cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: proj
15+
function: main
16+
span: 270
3417

3518

3619
┌─ 2 (root, leaf, target, terminal)

‎kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected‎

Lines changed: 12 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -3,38 +3,20 @@
33
│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
44
│ span: 0
55
│
6-
│ (128 steps)
6+
│ (68 steps)
77
├─ 3
8-
│ #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
8+
│ #cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: projectionEl
99
│ function: main
10-
┃
11-
┃ (1 step)
12-
┣━━┓
13-
┃ │
14-
┃ ├─ 4
15-
┃ │ AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
16-
┃ │ function: main
17-
┃ │
18-
┃ │ (1 step)
19-
┃ └─ 6 (stuck, leaf)
20-
┃ #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
21-
┃ function: main
22-
┃
23-
┗━━┓
24-
│
25-
├─ 5
26-
│ #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
27-
│ function: main
28-
│
29-
│ (154 steps)
30-
├─ 7 (terminal)
31-
│ #EndProgram ~> .K
32-
│ function: main
33-
│
34-
┊ constraint: true
35-
┊ subst: ...
36-
└─ 2 (leaf, target, terminal)
37-
#EndProgram ~> .K
10+
│ span: 270
11+
│
12+
│ (1 step)
13+
└─ 4 (leaf, terminal)
14+
thunk ( #cast ( PtrLocal ( 0 , place ( ... local: local ( 1 ) , projection: proj
15+
function: main
16+
span: 270
17+
3818

19+
┌─ 2 (root, leaf, target, terminal)
20+
│ #EndProgram ~> .K
3921

4022

0 commit comments

Comments
 (0)