Repository navigation
Model SIMD pointer lanes as integers of the same width - #4869
Merged
feliperodri merged 3 commits intoSep 29, 2026
Merged
Conversation
Declaring any `Simd<*const T, N>` took the compiler down before a harness ran:
assertion failed: typ.is_numeric()
[Kani] current codegen item: declare_function: std::simd::Simd::<*const i32, 2>::as_array
CBMC vectors require a numeric element type, and `portable_simd`'s pointer
vectors have been around for a while, so every `Simd<*const T, N>` and
`Simd<*mut T, N>` was unreachable. `core` declares
`transmute_copy::<Simd<usize, 2>, Simd<*const i32, 2>>`, which is what blocks
the unfiltered autoharness path over the standard library.
Model a pointer lane as an unsigned integer of the same width. Rust's SIMD
types are array-based, so a value is built and read through a byte-level
reinterpretation of the whole vector rather than lane by lane, and nothing
accesses a lane as a pointer at the goto level.
The test checks that an address survives the round trip rather than only that
codegen succeeds: `addr()` agrees across lanes, a dereference through a lane
reads the right value, a write through a `*mut` lane is observed, and the
`transmute_copy` shape from `core` verifies.
Resolves model-checking#4867
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
Direct simd_extract of a pointer lane still causes a codegen type mismatch and panic.
Get a fresh assessment by requesting another Copilot review.
Review effort: Balanced
Findings: 1
Open (1)
What changed in this PR
Models SIMD pointer lanes as pointer-width integers to prevent the compiler crash reported in #4867.
Changes:
- Adds pointer-aware SIMD type lowering.
- Adds pointer SIMD round-trip and mutation regression harnesses.
| File | Description |
|---|---|
kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs |
Lowers pointer lanes to unsigned integers. |
tests/kani/SIMD/ptr_elements.rs |
Tests pointer SIMD construction and access. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
The previous commit claimed nothing reaches a single lane of a pointer
vector, so modeling a lane as an integer needed no conversion. That is
wrong for `simd_extract`: it assigns the indexed lane straight to the
destination place, and `Stmt::assign` requires identical types, so any
`simd_extract::<Simd<*const T, N>, *const T>` took the compiler down
instead:
assign statement with unequal types
lhs Pointer { typ: Signedbv { width: 32 } } rhs Unsignedbv { width: 64 }
Cast the extracted lane to the return type, which is a no-op for every
other element type because the lane type already is the return type.
This mirrors `simd_insert` and `simd_splat`, which already cast the
incoming value to the lane type and therefore worked for pointers all
along, and it matches how Kani models `usize as *const T` elsewhere
(`codegen_misc_cast`). `simd_shuffle` keeps the element type, so it also
needed no change, and `simd_extract_dyn`/`simd_insert_dyn` are rejected
as unsupported before codegen for every element type.
Extend the regression test with the lane-wise paths: a pointer extracted
from a vector dereferences to the right object, the two lanes of a
two-element vector stay distinct, a write through an extracted `*mut`
lane is observed on the original variable, and an inserted pointer shows
up in the requested lane only. Each of these fails if the asserted value
is changed, so they are not vacuous.
Also correct the comment in `codegen_vector`, which described the lanes
as never being accessed as pointers.
9 of 42 tasks
tautschnig
approved these changes
Sep 29, 2026
tautschnig
left a comment
tautschnig
left a comment
Member
There was a problem hiding this comment.
Copilot's simd_extract finding is fixed by the second commit and the thread is resolved. The PR description still says nothing accesses a lane as a pointer and asks for a second opinion on that; the second commit already retracts it, so the description should be updated to match the code comment.
Co-authored-by: Michael Tautschnig <mt@debian.org>
feliperodri
enabled auto-merge
September 29, 2026 17:01
Merged
via the queue into
model-checking:main
with commit Sep 29, 2026
b1bdd18
21 of 22 checks passed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Declaring any
Simd<*const T, N>took the compiler down before a harness ran:CBMC vectors require a numeric element type.
portable_simd's pointer vectors have been around for a while, so this closed off everySimd<*const T, N>andSimd<*mut T, N>— and it isn't only reachable by writing one yourself:coredeclarestransmute_copy::<Simd<usize, 2>, Simd<*const i32, 2>>, which is what stops the unfiltered autoharness run over the standard library.The fix: model a pointer lane as an unsigned integer of the same width. Rust's SIMD types are array-based, so a value is built and read through a byte-level reinterpretation of the whole vector rather than lane by lane, and nothing accesses a lane as a pointer at the goto level.
Where I'd want a second opinion: that last sentence is the load-bearing one. If a future lane-wise operation reads an element as a pointer, an integer lane would be wrong, and the assertion that used to catch this is gone. I looked at the two places that touch lanes today (
codegen_rvalue_aggregateandcodegen_simd_field) and both go through a whole-vector reinterpretation, but I'd rather someone who has spent time in the SIMD intrinsics agree than take my reading of it.Risk: low and narrow. Non-pointer lanes take the same path as before, so nothing that verifies today changes; the new branch only applies where codegen previously aborted.
The test checks that an address actually survives the round trip rather than only that codegen succeeds:
addr()agrees across lanes, a dereference through a lane reads the right value, a write through a*mutlane is observed afterwards, and thetransmute_copyshape fromcoreverifies. I also confirmed the harnesses aren't vacuous — a false claim about a lane (is_null()on a non-null splat) still fails.Resolves #4867
Also resolves #2252, which is the same assertion reached through
Simd<*mut i8, 4>(verified on this branch: the crash is gone and the reproducer now reportssimd_scatter/simd_asas unsupported).