Skip to content

Commit 4d79325

Browse files
authored
Update features list (#1090)
This PR updates the features list using data from the UI test suite's LLVM run, the integration tests, plus specific targeted checks to update the Status and add a Notes column with high level info.
1 parent dcc97b0 commit 4d79325

1 file changed

Lines changed: 179 additions & 116 deletions

File tree

docs/feature-checklist.md

Lines changed: 179 additions & 116 deletions
Original file line numberDiff line numberDiff line change
@@ -4,137 +4,200 @@ which is available for use under [MIT](https://github.com/verus-lang/verus/blob/
44
license.
55
-->
66

7-
**Last Updated: 2025-04-10**
7+
**Last Updated: 2026-06-18**
8+
9+
Status reflects concrete execution against the Rust UI test suite. Many limitations trace back to a
10+
single missing component: an **address model** (a representation of addresses in memory). Types whose
11+
values own heap-allocated data (`Box`, `Vec`, etc.) additionally need dynamic (heap)
12+
allocation of that data, built on the address model. **A _Supported_ label can be followed by an
13+
address-model caveat** (e.g. references work, but not references into heap/static data, which are not modeled yet). Therefore, please read
14+
the *Notes* for a full description of the supported features.
15+
Such dependencies are flagged in bold as **Requires the address model** / **Requires heap allocation**.
816

917
## Items
10-
|Feature|Status|
11-
|-------|------|
12-
|Functions, methods, associated functions|Supported|
13-
|Associated constants|Not supported|
14-
|Structs|Partially supported|
15-
|Enums|Partially supported|
16-
|Const functions|Not supported|
17-
|Async functions|Not supported|
18-
|Macros|N/A (MIR)|
19-
|Type aliases|Not supported|
20-
|Const items|Not supported|
21-
|Static items|Not supported|
18+
|Feature|Status|Notes|
19+
|-------|------|-----|
20+
|Functions, methods, associated functions|Supported|indirect calls through a stored function pointer: see Function pointer types|
21+
|Associated constants|Supported||
22+
|Structs|Partially supported|construction and field access work; decoding reordered/padded layouts from raw bytes not yet|
23+
|Enums|Partially supported|construction and matching work; decoding with-field / niche-encoded variants from raw bytes not yet|
24+
|Const functions|Supported||
25+
|Async functions|Not supported|desugars to coroutines (also not supported)|
26+
|Macros|N/A (MIR)||
27+
|Type aliases|Supported|resolved before MIR|
28+
|Const items|Supported|value constants work; **Requires the address model** for constants holding references into data (`&str`, `&[T]`)|
29+
|Static items|Not supported|**Requires the address model**|
2230

2331
## Struct/enum definitions
24-
|Feature|Status|
25-
|-------|------|
26-
|Type parameters|Not supported|
27-
|Where clauses|Not supported|
28-
|Lifetime parameters|Not supported|
29-
|Const generics|Not supported|
30-
|Custom discriminants| Supported|
31-
|Public / private fields|N/A (MIR)|
32+
|Feature|Status|Notes|
33+
|-------|------|-----|
34+
|Type parameters|Supported|monomorphized before MIR|
35+
|Where clauses|Supported|resolved at type-check|
36+
|Lifetime parameters|Supported|erased in MIR|
37+
|Const generics|Supported|monomorphized; complex `generic_const_exprs` (unstable) not yet (see `impl` types)|
38+
|Custom discriminants|Supported||
39+
|Public / private fields|N/A (MIR)||
3240

3341
## Expressions and Statements
34-
|Feature|Status|
35-
|-------|------|
36-
|Variables, assignment, mutable variables|Supported|
37-
|`if`, `else`|Supported|
38-
|Patterns, `match`, `if let`, match guards|Supported|
39-
|Block expressions|Supported|
40-
|Items|Supported|
41-
|`loop`, `while`|Supported|
42-
|`for`|Not supported (`Range` not supported)|
43-
|`?`|Supported|
44-
|Async blocks|Not supported|
45-
|`await`|Not supported|
46-
|Unsafe blocks|Supported|
47-
|`&`|Supported|
48-
|`&mut`, place expressions|Supported|
49-
|`==`, `!=`|Supported|
50-
|Type cast (`as`)|Partially supported|
51-
|Compound assigments (`+=`, etc.)|Supported|
52-
|Array expressions|Not supported|
53-
|Range expressions|Not supported|
54-
|Index expressions|Not supported (Arrays not supported)|
55-
|Tuple expressions|Supported|
56-
|Struct/enum constructors|Not supported|
57-
|Field access|Supported|
58-
|Function and method calls|Supported|
59-
|Closures|Supported|
60-
|Labels, break, continue|Supported|
61-
|Return statements|Supported|
42+
|Feature|Status|Notes|
43+
|-------|------|-----|
44+
|Variables, assignment, mutable variables|Supported||
45+
|`if`, `else`|Supported||
46+
|Patterns, `match`, `if let`, match guards|Supported|slice rest-patterns (`[head, tail @ ..]`) not yet|
47+
|Block expressions|Supported||
48+
|Items|Supported||
49+
|`loop`, `while`|Supported||
50+
|`for`|Supported|desugars to iterators|
51+
|`?`|Supported||
52+
|Async blocks|Not supported|desugars to coroutines (also not supported)|
53+
|`await`|Not supported|desugars to coroutines (also not supported)|
54+
|Unsafe blocks|Supported||
55+
|`&`|Supported||
56+
|`&mut`, place expressions|Supported||
57+
|`==`, `!=`|Supported||
58+
|Type cast (`as`)|Partially supported|numeric and pointer casts work; **Requires the address model** for integer↔pointer casts; float casts not yet|
59+
|Compound assigments (`+=`, etc.)|Supported||
60+
|Array expressions|Supported|including multi-dimensional|
61+
|Range expressions|Supported||
62+
|Index expressions|Supported|element indexing works; range-indexing into a sub-slice: see Patterns|
63+
|Tuple expressions|Supported||
64+
|Struct/enum constructors|Supported||
65+
|Field access|Supported|union cross-field access: see Unions|
66+
|Function and method calls|Supported|indirect calls through a stored function pointer: see Function pointer types|
67+
|Closures|Supported||
68+
|Labels, break, continue|Supported||
69+
|Return statements|Supported||
6270

6371
## Integer arithmetic
64-
|Feature|Status|
65-
|-------|------|
66-
|Arithmetic for unsigned|Supported|
67-
|Arithmetic for signed (`+`, `-`, `*`, `/`, `%`)|Supported|
68-
|Bitwise operations (`&`, `\|`, `!`, `>>`, `<<`)|Supported|
69-
|Arch-dependent types (`usize`, `isize`)|Not supported (fixed width) |
72+
|Feature|Status|Notes|
73+
|-------|------|-----|
74+
|Arithmetic for unsigned|Supported||
75+
|Arithmetic for signed (`+`, `-`, `*`, `/`, `%`)|Supported||
76+
|Bitwise operations (`&`, `\|`, `!`, `>>`, `<<`)|Supported||
77+
|Arch-dependent types (`usize`, `isize`)|Not supported (fixed width)|`usize`/`isize` work as fixed 64-bit|
7078

7179
## Types and standard library functionality
72-
|Feature|Status|
73-
|-------|------|
74-
|Integer types|Supported|
75-
|`bool`|Supported|
76-
|Strings|Not supported|
77-
|`Vec`|Not supported|
78-
|`Option` / `Result`|Supported|
79-
|Floating point|Not supported|
80-
|Slices|Not supported|
81-
|Arrays|Not supported|
82-
|Pointers|Not supported|
83-
|References (`&`)|Supported|
84-
|Mutable references (`&mut`)|Supported|
85-
|Never type (`!`)|Not supported|
86-
|Function pointer types|Not supported|
87-
|Closure types|Supported|
88-
|Trait objects (`dyn`)|Not supported|
89-
|`impl` types|Not supported|
90-
|`Cell`, `RefCell`|Not supported|
91-
|Iterators|Not supported|
92-
|`HashMap`|Not supported|
93-
|Smart pointers (`Box`, `Rc`, `Arc`)|Not supported|
94-
|`Pin`|Not supported|
95-
|Hardware intrinsics|Not supported|
96-
|Printing, I/O|Not supported|
97-
|Panic-unwinding|Not supported|
80+
|Feature|Status|Notes|
81+
|-------|------|-----|
82+
|Integer types|Supported||
83+
|`bool`|Supported||
84+
|`char`|Not supported|char values not yet modeled|
85+
|Strings|Not supported|`str` not yet; `String` **Requires heap allocation**|
86+
|`Vec`|Not supported|**Requires heap allocation**|
87+
|`Option` / `Result`|Supported|construction and matching work; decoding niche/with-field variants from raw bytes not yet (see Enums)|
88+
|Floating point|Not supported|float decoding and arithmetic not yet implemented|
89+
|Slices|Partially supported|indexing and `split_at` work; slice rest-patterns and fat-pointer length metadata not yet|
90+
|Arrays|Partially supported|indexing and multi-dimensional arrays work; slice rest-patterns (`[head, tail @ ..]`) not yet|
91+
|Pointers|Partially supported|place-based pointers partly work (some pointer casts still produce thunks and fail); **Requires the address model** for integer↔pointer casts|
92+
|References (`&`)|Supported|references to stack data work; **Requires the address model** for references to constant/static/heap data|
93+
|Mutable references (`&mut`)|Supported|references to stack data work; **Requires the address model** for references to constant/static/heap data|
94+
|Never type (`!`)|Not supported||
95+
|Function pointer types|Partially supported|passing a function or closure as an argument works; calling indirectly through a stored function pointer not yet|
96+
|Closure types|Supported|`dyn Fn` dispatch: see Trait objects|
97+
|Coroutines / generators|Not supported|underlies async|
98+
|Trait objects (`dyn`)|Not supported|needs dynamic dispatch via vtables; `Box<dyn>` also **Requires heap allocation**|
99+
|`impl` types|Partially supported|return-position and argument `impl Trait` work; some opaque-type cases not yet|
100+
|`Cell`, `RefCell`|Partially supported|`Cell` works; `RefCell` (borrow tracking) not yet|
101+
|Iterators|Supported||
102+
|`HashMap`|Not supported|**Requires heap allocation**|
103+
|Smart pointers (`Box`, `Rc`, `Arc`)|Not supported|**Requires heap allocation**|
104+
|`Pin`|Not supported||
105+
|Hardware intrinsics|Partially supported|several implemented; many (including SIMD) not yet|
106+
|Printing, I/O|Not supported||
107+
|Panic-unwinding|Not supported|panics that abort are detected; unwinding / `catch_unwind` not yet|
98108

99109
## Traits
100-
|Feature|Status|
101-
|-------|------|
102-
|User-defined traits|Supported|
103-
|Default implementations|Supported|
104-
|Trait bounds on trait declarations|Supported|
105-
|Traits with type arguments|Supported|
106-
|Associated types|Supported|
107-
|Generic associated types|Supported|
108-
|Higher-ranked trait bounds|Supported|
109-
|`Clone`|Supported|
110-
|Marker traits (`Copy`)|Supported|
111-
|Marker traits (`Send`, `Sync`)|Not supported|
112-
|Standard traits (`Hash`, `Debug`)|Not supported|
113-
|User-defined destructors (`Drop`)|Not supported|
114-
|`Sized` (`size_of`, `align_of`)|Not supported|
115-
|`Deref`, `DerefMut`|Not supported|
110+
|Feature|Status|Notes|
111+
|-------|------|-----|
112+
|User-defined traits|Supported||
113+
|Default implementations|Supported||
114+
|Trait bounds on trait declarations|Supported||
115+
|Traits with type arguments|Supported||
116+
|Associated types|Supported||
117+
|Generic associated types|Supported||
118+
|Higher-ranked trait bounds|Supported||
119+
|`Clone`|Supported||
120+
|Marker traits (`Copy`)|Supported||
121+
|Marker traits (`Send`, `Sync`)|Not supported|markers erased in MIR; meaningful only with concurrency which is not supported|
122+
|Standard traits (`Hash`, `Debug`)|Not supported|formatting / hashing machinery not implemented|
123+
|User-defined destructors (`Drop`)|Not supported|destructors do not run (Drop is a no-op); control flow continues|
124+
|`Sized` (`size_of`, `align_of`)|Supported|`size_of_val` on unsized types: see Hardware intrinsics|
125+
|`Deref`, `DerefMut`|Partially supported|user `Deref`/`DerefMut` impls work; `Box`/`Rc` deref **Requires heap allocation**|
116126

117127
## Multi-threading
118-
|Feature|Status|
119-
|-------|------|
120-
|`Mutex`, `RwLock` (from standard library)|Not supported
121-
|Verified lock implementations|Not supported
122-
|Atomics|Not supported|
123-
|`spawn` and `join`|Not supported|
124-
|Interior mutability|Not supported|
128+
|Feature|Status|Notes|
129+
|-------|------|-----|
130+
|`Mutex`, `RwLock` (from standard library)|Not supported|**Requires heap allocation** and concurrency|
131+
|Verified lock implementations|Not supported||
132+
|Atomics|Not supported||
133+
|`spawn` and `join`|Not supported|no threading model|
134+
|Interior mutability|Partially supported|`Cell` works; `RefCell` not yet (see Cell/RefCell)|
125135

126136
## Unsafe
127-
|Feature|Status|
128-
|-------|------|
129-
|Raw pointers|Not supported|
130-
|Transmute|Not supported|
131-
|Unions|Not supported|
132-
|`UnsafeCell`|Not supported|
137+
|Feature|Status|Notes|
138+
|-------|------|-----|
139+
|Raw pointers|Partially supported|place-based pointers partly work (some pointer casts still produce thunks and fail); **Requires the address model** for integer↔pointer casts|
140+
|Transmute|Partially supported|byte / wrapper / enum transmutes work; **Requires the address model** for transmutes involving pointer/address values|
141+
|Unions|Partially supported|reading the field last written works; cross-field type-punning not yet|
142+
|`UnsafeCell`|Not supported|**Requires the address model**: direct use fails on a pointer-alignment check; `Cell`, built on it, works (see Cell/RefCell)|
143+
|FFI / `extern` functions|Not supported|external functions have no MIR body to execute|
133144

134145
## Crates and code organization
135-
|Feature|Status|
136-
|-------|------|
137-
|Multi-crate projects|Partially supported|
138-
|Verified crate + unverified crates|Not supported|
139-
|Modules|Supported|
140-
|rustdoc|Not supported|
146+
|Feature|Status|Notes|
147+
|-------|------|-----|
148+
|Multi-crate projects|Partially supported||
149+
|Verified crate + unverified crates|Not supported||
150+
|Modules|Supported||
151+
|rustdoc|Not supported||
152+
153+
## Methodology and evidence
154+
155+
The statuses above were derived from three sources, cross-checked:
156+
157+
1. A full run of the Rust **UI test suite** under the LLVM (concrete) backend (~2888 tests).
158+
2. The repository's **integration tests**: the curated `prove-rs` suite (each `*-fail.rs` is *expected* to fail), the `decode-value` cases, and `verify-rust-std`.
159+
3. **Targeted checks**: small programs run directly to probe a specific feature.
160+
161+
A feature is only marked **Supported** when it both has a passing test that exercises it *and* no failing
162+
test has it as the **root cause**. Distinguishing "root cause" from "where execution stops" matters: a test
163+
often gets stuck far from the real problem (e.g. an arithmetic test that fails only because it prints its
164+
result). To attribute correctly we **tracked thunks** (when the semantics cannot yet rewrite an evaluation it
165+
records it as a *thunk*, noting where that thunk was created) and traced each failure back to the thunk that
166+
caused it. This allows us to say that a feature works while its nominal-category failures are due to *other*
167+
unsupported features.
168+
169+
In the table below, *Passing* gives tests that exercise the feature and succeed (integration tests are under
170+
`kmir/src/tests/integration/data/`, UI tests under `tests/ui/`). *Failures attributed to* gives, for the
171+
not-fully-passing rows, representative failing tests in the same area with the **other** feature their failure
172+
actually traces to. UI directories are nominal groupings, so a directory rarely passes entirely even when the
173+
named feature works. A few directories do pass entirely, noted as such.
174+
175+
| Row | Status | Passing | Failures attributed to |
176+
|-----|--------|---------|-----------------------|
177+
| Iterators | Supported | `iterator-simple`, `iter_next_1/2/3`, `iter-eq-copied-take-dereftruncate`; `tests/ui/iterators/iter-map-fold-type-length` | `iter-sum-overflow` → panic-unwinding; `iter-count-overflow` → loop-to-2⁶⁴ timeout; `iter-range` → printing |
178+
| Arrays | Partially supported | `array_match`, `array_write`, `array_nest_compare` (nested `[[u16;3];2]`); `tests/ui/array-slice-vec/{array_const_index-2,copy-out-of-array-1}` | own gap: `tests/ui/array-slice-vec/{subslice-patterns-const-eval,vec-matching-fold}` (slice rest-patterns). Other fails → heap (`box-of-array-of-drop-1`) |
179+
| Slices | Partially supported | `slice-split-at` | same slice rest-pattern gap as Arrays |
180+
| `for` / Range / Index / Struct-enum constructors | Supported | `struct`, `enum`; `tests/ui/structs-enums/{class-methods,borrow-tuple-fields}`; `for`/range via `iterator-simple` + targeted `1..5` checks | `tests/ui/structs-enums/class-cast-to-trait` → heap (Vec alloc); `align-struct` → unimplemented `min_align_of_val` intrinsic |
181+
| Type/lifetime/const generics, where clauses | Supported | monomorphized/erased before MIR; 284 generics / 106 lifetimes / 46 const-generics passing UI tests, e.g. `tests/ui/generics/generic-fn-twice`, `tests/ui/lifetimes/issue-84604`, `tests/ui/const-generics/const-arg-in-fn` | `tests/ui/const-generics` fails → heap/transmute and unimplemented `generic_const_exprs` (`OpaqueCast`) |
182+
| Associated constants | Supported | `tests/ui/associated-consts/{assoc-const,associated-const-const-eval}` (19 passing in dir, 1 fail) | `associated-const-in-global-const` → constant-into-allocation (address model) |
183+
| Const functions | Supported | run like normal functions; `tests/ui/const-generics/min_const_generics/const_fn_in_generics`, targeted `const fn` checks | |
184+
| Type aliases | Supported | resolved before MIR; `tests/ui/type-alias-enum-variants/` (both tests pass) | |
185+
| Const items | Supported | value constants work (targeted `const C: u32` checks; no dedicated UI dir); constants holding references into data (`&str`, `&[T]`) need the address model | |
186+
| Function pointer types | Partially supported | fn-item/closure-as-argument: `488-support-function-pointer-calls` | calling indirectly through a stored/cast function pointer not yet (the `tests/ui/` indirect-call failures) |
187+
| `impl` types | Partially supported | `tests/ui/impl-trait/{closure-in-impl-trait-arg,example-st}`, targeted `impl Fn`/`impl Into` | `equality-rpass``OpaqueCast`/`Subtype` projection; others → heap/transmute |
188+
| Transmute | Partially supported | `transmute-bytes`, `transmute_transparent_wrapper_up/down`, `transmute-u8-to-enum`; `tests/ui/transmute/` (passes wholesale) | own gap: `transmute-maybe-uninit-fail`; pointer/address-typed transmutes → address model |
189+
| Unions | Partially supported | `tests/ui/union/{union-derive-rpass,union-inherent-method,union-backcomp}` | own gap: `union-pat-refutability`, `union-const-eval-field` (cross-field punning); `union-align` → unimplemented `min_align_of_val` |
190+
| `Cell` / Interior mutability | Partially supported | `Cell`: `interior-mut2` (no dedicated UI dir) | `RefCell`: `interior-mut-fail` (borrow tracking) |
191+
| Raw pointers / Pointers | Partially supported | place-based: `offset_read`, `pointer-cast` | `raw-ptr-cast-fail` → pointer-alignment check / `ptr as usize` (address model) |
192+
| `Sized` (`size_of`, `align_of`) | Supported | `align_and_size` (all integer widths; no dedicated UI dir) | |
193+
| `Deref`/`DerefMut` | Partially supported | user impls: `tests/ui/autoref-autoderef/autoderef-privacy` | `Box`/`Rc` deref → heap |
194+
| Hardware intrinsics | Partially supported | `intrinsics` (rotate_left, bswap, ctpop, ctlz_nonzero); `tests/ui/intrinsics/{intrinsic-assume,intrinsic-raw_eq-const}` | `const-eval-select-x86_64` → SIMD; `intrinsic-alignment` → unimplemented `pref_align_of` |
195+
| Smart pointers (`Box`/`Rc`/`Arc`) | Not supported | | `box_heap_alloc-fail` (expected fail) → heap |
196+
| Static items | Not supported | | `volatile_load_static-fail`, `volatile_store_static-fail` (expected fail) → address model |
197+
| `UnsafeCell` | Not supported | | `interior-mut3-fail` (expected fail) → pointer-alignment / address model |
198+
| Floating point | Not supported | | `verify-rust-std/0011-floats-ints` (`to_int_unchecked` parked); no passing float test |
199+
| Enums (decode of with-field/niche variants) | Partially supported | fieldless variants decode fine (`enum-direct-tag-decode`) | `decode-value` SKIP: `enum-1-variant-1-field`, `enum-option-nonzero-none`, … (with-field/niche decode) |
200+
| Strings | Not supported | | `decode-value` SKIP `str` |
201+
| `char` | Not supported | | no `char` value representation (decode rule unimplemented); only size/alignment known |
202+
| Coroutines / generators | Not supported | | `tests/ui/coroutine/` (all 33 fail, e.g. `addassign-yield`) → `aggregateKindCoroutine` unhandled |
203+
| FFI / `extern` functions | Not supported | | external functions have no MIR body (e.g. `tests/ui/abi/anon-extern-mod`) |

0 commit comments

Comments
 (0)