Unexpected Alias type with -Z valid-value-checks

[adpaco-aws]

#3085 introduced the following test in tests/kani/ValidValues/write_invalid.rs:

use std::num::NonZeroU8;

#[kani::proof]
#[kani::should_panic]
pub fn write_invalid_bytes_no_ub_with_spurious_cex() {
    let mut non_zero: NonZeroU8 = kani::any();
    let dest = &mut non_zero as *mut _;
    unsafe { std::intrinsics::write_bytes(dest, 0, 1) };
}

#[kani::proof]
#[kani::should_panic]
pub fn write_valid_before_read() {
    let mut non_zero: NonZeroU8 = kani::any();
    let mut non_zero_2: NonZeroU8 = kani::any();
    let dest = &mut non_zero as *mut _;
    unsafe { std::intrinsics::write_bytes(dest, 0, 1) };
    unsafe { std::intrinsics::write_bytes(dest, non_zero_2.get(), 1) };
    assert_eq!(non_zero, non_zero_2)
}

#[kani::proof]
#[kani::should_panic]
pub fn read_invalid_is_ub() {
    let mut non_zero: NonZeroU8 = kani::any();
    let dest = &mut non_zero as *mut _;
    unsafe { std::intrinsics::write_bytes(dest, 0, 1) };
    assert_eq!(non_zero.get(), 0)
}

In the toolchain upgrade in #3102 we're getting an unexpected compilation error for this test (CI run here) which looks like this:

unexpected type: Ty { id: 14, kind: Alias(Projection, AliasTy { def_id: AliasDef(DefId { id: 11, name: "std::num::ZeroablePrimitive::NonZeroInner" }), args: GenericArgs([Type(Ty { id: 3, kind: RigidTy(Uint(U8)) }), Const(Const { kind: Allocated(Allocation { bytes: [Some(1)], provenance: ProvenanceMap { ptrs: [] }, align: 1, mutability: Mut }), ty: Ty { id: 9, kind: RigidTy(Bool) }, id: ConstId(4) })]) }) }

And it's coming from this function:

2024-03-27T14:52:39.487676Z TRACE visit_fn{function=Instance { kind: Item, def: "_RINvNtCsbLQVFf8BMTJ_4core10intrinsics11write_bytesINtNtNtB4_3num7nonzero7NonZerohEECsi8ET5SPUdoh_13write_invalid", args: GenericArgs([Type(Ty { id: 6, kind: RigidTy(Adt(AdtDef(DefId { id: 6, name: "std::num::NonZero" }), GenericArgs([Type(Ty { id: 3, kind: RigidTy(Uint(U8)) })]))) }), Const(Const { kind: Allocated(Allocation { bytes: [Some(1)], provenance: ProvenanceMap { ptrs: [] }, align: 1, mutability: Mut }), ty: Ty { id: 9, kind: RigidTy(Bool) }, id: ConstId(4) })]) }}: kani_compiler::kani_middle::transform::check_values: transform function="std::intrinsics::write_bytes::<std::num::NonZero<u8>>"

with Kani version: 0.48.0

We're going to change the test to be a "fixme" test. We should first fix avoid returning an Alias from StableMIR, and then restore the test.

[tautschnig]

Was fixed in #3127.