Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions kmir/src/kmir/kdist/mir-semantics/rt/data.md
Original file line number Diff line number Diff line change
Expand Up @@ -1921,6 +1921,9 @@ Zero-sized types can be decoded trivially into their respective representation.
// zero-sized array
rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoArrayType(_, _))
=> Range(.List) ... </k>
// zero-sized function item (e.g., closures without captures)
rule <k> #decodeConstant(constantKindZeroSized, _TY, typeInfoFunType(_))
=> Aggregate(variantIdx(0), .List) ... </k>
```

Allocated constants of reference type with a single provenance map entry are decoded as references
Expand Down
5 changes: 3 additions & 2 deletions kmir/src/kmir/kdist/mir-semantics/rt/types.md
Original file line number Diff line number Diff line change
Expand Up @@ -348,8 +348,9 @@ Slices, `str`s and dynamic types require it, and any `Ty` that `is_sized` does
rule #zeroSizedType(typeInfoTupleType(.Tys, _)) => true
rule #zeroSizedType(typeInfoStructType(_, _, .Tys, _)) => true
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
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Exclude invalid lookup sentinel from ZST function rule

#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 👍 / 👎.

// FIXME: Only unit tuples, empty structs, void, and function items are
// recognized here; other zero-sized types (e.g. single-variant enums,
// newtype wrappers around ZSTs) still fall through because we do not consult
// the layout metadata yet. Update once we rely on machineSize(0).
rule #zeroSizedType(_) => false [owise]
Expand Down
6 changes: 5 additions & 1 deletion kmir/src/tests/integration/test_integration.py
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,9 @@
'iter-eq-copied-take-dereftruncate': ['repro'],
'spl-multisig-iter-eq-copied-next': ['repro'],
}
PROVE_TERMINATE_ON_THUNK = [
'closure-staged',
]
PROVE_SHOW_SPECS = [
'local-raw-fail',
'interior-mut-fail',
Expand Down Expand Up @@ -87,7 +90,8 @@ def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None:
if update_expected_output and not should_show:
pytest.skip()

prove_opts = ProveOpts(rs_file, smir=is_smir)
should_terminate_on_thunk = rs_file.stem in PROVE_TERMINATE_ON_THUNK
prove_opts = ProveOpts(rs_file, smir=is_smir, terminate_on_thunk=should_terminate_on_thunk)
printer = PrettyPrinter(kmir.definition)
cterm_show = CTermShow(printer.print)

Expand Down
Loading