Fix ICE on pattern types over wide pointers under -Z valid-value-checks

[Tianshu-Huang]

ty_validity_per_offset asserted that a pattern type has a Scalar layout. NonNull<[u8]>'s field is pattern_type!(*const [u8] is !null), a wide pointer with a ScalarPair layout, and every allocation reaches it, so -Z valid-value-checks ICE'd on any program using Box/Vec/String.

Accept ScalarPair alongside Scalar. try_from_ty already takes the first scalar's valid_range for a pair, which is the data pointer's !null, the same way &[u8] is checked. Any other layout is reported as unsupported instead of asserted on.

The regression test uses the issue's reproducer: Box::new now verifies, and a second harness that transmutes a null data pointer into NonNull<[u8]> fails with Invalid value of type NonNull<[u8]>, so the check is enforced rather than skipped.

Resolves #4829

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Copilot review overview

🟡 Changes recommended

Existing comments still incorrectly state that all pattern types have scalar ABIs.

Get a fresh assessment by requesting another Copilot review.

Review effort: Balanced
Findings: 1

Open (1)

• Update pattern type comments to reflect rejected non-scalar patterns · New

What changed in this PR

Prevents -Z valid-value-checks from crashing on wide-pointer pattern types.

Changes:

• Returns an unsupported-check error for non-scalar pattern types.
• Adds an allocation regression test and expected diagnostic.

File	Description
kani-compiler/​src/​kani_middle/​transform/​check_values.rs	Replaces the scalar-ABI assertion with graceful rejection.
tests/​expected/​valid-value-checks/​fat_pointer_pattern.rs	Adds the allocation regression case.
tests/​expected/​valid-value-checks/​fat_pointer_pattern.expected	Captures the expected unsupported-check result.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Thanks for picking this up. The crash is gone, but the fix trades it for a spurious failure. Every allocation reaches NonNull<[u8]>, so reporting it as unsupported makes every allocating program fail verification under -Z valid-value-checks. The new test shows it: a correct Box program is expected to FAIL. The flag stays unusable on real code, which was #4829's impact.

The pass already knows how to check wide pointers. try_from_ty reads the first scalar of a ScalarPair, which is the data pointer and its valid range, and that's how &[u8] and *const [u8] are handled today. The !null of *const [u8] is !null is exactly that range, so accepting ScalarPair here is enough:

-        if !matches!(layout.value_repr, ValueRepr::Scalar(..)) {
+        if !matches!(layout.value_repr, ValueRepr::Scalar(..) | ValueRepr::ScalarPair { .. }) {

I tried it: Box::new, Vec::push, and a non-null NonNull<[u8]> transmute all verify, and a transmute with a null data pointer is still caught as Undefined Behavior: Invalid value of type NonNull<[u8]>. The other 10 tests using -Z valid-value-checks are unchanged.

What would flip this to approval: that change, with fat_pointer_pattern expecting SUCCESSFUL, plus a harness with a null data pointer that must FAIL, so the test shows the requirement is enforced and not skipped. Box<dyn Debug> and Rc<str> then stop at other, pre-existing unsupported constructs (fmt::rt, copy_nonoverlapping on *const u8). Those are separate issues, not this PR's.

[feliperodri]

Thanks for the quick turnaround — this addresses everything from my earlier review. Accepting ScalarPair lets allocating code verify under -Z valid-value-checks. null_data_pointer shows the !null requirement is enforced rather than skipped. Unknown layouts now return an unsupported-check error instead of asserting, so the pass can't ICE here. The note on why assert_eq!(nn.len(), 3) is there is helpful too.

I checked it locally, merged with current main. All 10 valid-value-checks tests pass. Vec::push and NonNull::from(&a[..]) verify, and a NonNull<[u8]> whose data pointer is kani::any() is correctly reported as invalid.

One non-blocking note: only the first scalar of the pair is checked. For NonNull<dyn Trait> that means a null vtable isn't caught, the same as for &dyn Trait today. That gap is #3738, not this PR.