fix(rt): handle zero-sized function types in decode and ZST recognition#813
Conversation
Stevengre
force-pushed
the
jh/zero-sized-decode
branch
4 times, most recently
from
6f0c0b9 to
3de1980
Compare
Rename closure-staged.rs → closure-staged-fail.rs and enable
terminate-on-thunk for this test. Without a #decodeConstant rule for
typeInfoFunType, the non-capturing closure passed as a constant operand
cannot be decoded and falls through to a thunk:
Node 3: #decodeConstant(constantKindZeroSized, ty(33), typeInfoFunType("..."))
Node 4: thunk(#decodeConstant(...)) ← proof terminates here
Also adds PROVE_TERMINATE_ON_THUNK list to test_integration.py for
per-test thunk termination control.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Two fixes for zero-sized function item types (closures without captures):
1. types.md: Add #zeroSizedType(typeInfoFunType(_)) => true
Function items are inherently zero-sized (#elemSize already returns 0),
but #zeroSizedType did not recognize them. This prevented rvalueRef
from materializing uninitialized zero-sized closure locals.
2. data.md: Add #decodeConstant rule for typeInfoFunType
Zero-sized function constants decode to Aggregate(variantIdx(0), .List),
matching the existing treatment of zero-sized structs and tuples.
RED → GREEN for closure-staged (with terminate-on-thunk):
Before: 44 steps → thunk(#decodeConstant(constantKindZeroSized, _,
typeInfoFunType(_))) — proof terminated on thunk
After: 266 steps → #EndProgram — proof passes, no thunks
Renames closure-staged-fail.rs back to closure-staged.rs.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The expected output was only needed to show the RED → GREEN transition in the commit history. Now that the fix is in place, closure-staged passes as a normal prove test without needing show output. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Stevengre
force-pushed
the
jh/zero-sized-decode
branch
from
3de1980 to
3aa012d
Compare
Stevengre
changed the title
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3aa012d252
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| rule #zeroSizedType(typeInfoVoidType) => true | ||
| // FIXME: Only unit tuples, empty structs, and void are recognized here; other | ||
| // zero-sized types (e.g. single-variant enums, function or closure items, | ||
| rule #zeroSizedType(typeInfoFunType(_)) => true |
There was a problem hiding this comment.
#zeroSizedType(typeInfoFunType(_)) => true now also matches the sentinel returned by lookupTy on missing entries (typeInfoFunType(" ** INVALID LOOKUP CALL **") in rt/value.md), so unresolved type IDs are silently treated as zero-sized. That changes behavior in places that gate on #zeroSizedType (notably pointer projection compatibility in #pointeeProjection and zero-sized local materialization in rvalueRef), allowing execution to proceed with fabricated ZST behavior instead of surfacing a missing-type-table condition; this can corrupt proof behavior when type extraction is incomplete.
Useful? React with 👍 / 👎.
jberthold
left a comment
jberthold
left a comment
There was a problem hiding this comment.
LGTM.
CI hits a timeout (20 minutes) , could it be caused by the change?
dkcumming
left a comment
dkcumming
left a comment
There was a problem hiding this comment.
Looks good. I think it is fine to add --terminate-on-thunk specifically for this for now. But that it had to be added to see that we were not decoding these functions in the test suite indicates to me we should add --terminate-on-thunk to all the tests (something I have been thinking for some time now). This will probably create a regression but it will also show us clearly what we are not handling. That time might not be now to swap but it would be good to understand how many tests regress with this.
automergerpr-permission-manager
bot
merged commit 9af0261
into
master
3 participants
Summary
Fix two issues preventing correct handling of zero-sized function item types (e.g., non-capturing closures):
#zeroSizedTypedid not recognizetypeInfoFunType(types.md)— Function items are inherently zero-sized (
#elemSizealready returns 0), but#zeroSizedTypereturnedfalse, preventingrvalueReffrom materializing uninitialized closure locals.#decodeConstanthad no rule fortypeInfoFunType(data.md)— Zero-sized function constants fell through to the
thunkwrapper instead of decoding toAggregate(variantIdx(0), .List).Evidence
closure-staged.rswithterminate-on-thunk:thunk(#decodeConstant(constantKindZeroSized, _, typeInfoFunType(_)))#EndProgram