transmute_unchecked with different-sized inputs not compiling #3839
Description
Hello, I've noticed a bug in Kani (v0.56.0) where calling transmute_unchecked() on two variables of different sizes leads to an error, despite the fact that transmute_unchecked() would normally allow this (but would consider this to be UB). For instance, the following compiles with rustc:
#![feature(core_intrinsics)]
use std::intrinsics::transmute_unchecked;
fn main() {
let a: u32 = 10;
let b: u16 = unsafe { transmute_unchecked(a) };
}However, when using same code in a harness (see the following transmute_diff_size() harness, which would go in library/core/src/intrinsics/mod.rs) with command ./scripts/run-kani.sh --path . --kani-args --harness intrinsics::transmute_diff_size, I get an error.
#[cfg(kani)]
#[kani::proof]
fn transmute_diff_size() {
let a: u32 = 10;
let b: u16 = unsafe { transmute_unchecked(a) };
}Here is the full output from running the run-kani script, including the error:
warning: /home/alex/Documents/verify-rust-std/target/kani_verify_std/Cargo.toml: no edition set: defaulting to the 2015 edition while the latest is 2021
Updating crates.io index
Compiling proc-macro2 v1.0.93
Compiling unicode-ident v1.0.14
Compiling version_check v0.9.5
Compiling syn v1.0.109
Compiling safety v0.1.0 (/home/alex/Documents/verify-rust-std/library/contracts/safety)
Compiling compiler_builtins v0.1.138
Compiling libc v0.2.162
Compiling std v0.0.0 (/home/alex/Documents/verify-rust-std/library/std)
Compiling proc-macro-error-attr v1.0.4
Compiling proc-macro-error v1.0.4
Compiling quote v1.0.38
Compiling syn v2.0.96
Compiling core v0.0.0 (/home/alex/Documents/verify-rust-std/library/core)
Compiling rustc-std-workspace-core v1.99.0 (/home/alex/Documents/verify-rust-std/library/rustc-std-workspace-core)
Compiling alloc v0.0.0 (/home/alex/Documents/verify-rust-std/library/alloc)
Compiling cfg-if v1.0.0
Compiling memchr v2.7.4
Compiling adler v1.0.2
Compiling rustc-demangle v0.1.24
Compiling unwind v0.0.0 (/home/alex/Documents/verify-rust-std/library/unwind)
Compiling rustc-std-workspace-alloc v1.99.0 (/home/alex/Documents/verify-rust-std/library/rustc-std-workspace-alloc)
Compiling panic_unwind v0.0.0 (/home/alex/Documents/verify-rust-std/library/panic_unwind)
Compiling panic_abort v0.0.0 (/home/alex/Documents/verify-rust-std/library/panic_abort)
Compiling gimli v0.29.0
Compiling hashbrown v0.15.0
Compiling miniz_oxide v0.7.4
Compiling object v0.36.5
Compiling std_detect v0.1.5 (/home/alex/Documents/verify-rust-std/library/stdarch/crates/std_detect)
Compiling addr2line v0.22.0
Compiling proc_macro v0.0.0 (/home/alex/Documents/verify-rust-std/library/proc_macro)
Compiling dummy v0.1.0 (/home/alex/Documents/verify-rust-std/target/kani_verify_std)
thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:946:9:
assertion `left == right` failed
left: 32
right: 16
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md
[Kani] current codegen item: codegen_function: intrinsics::transmute_diff_size
_RNvNtCsfBtlgdCIO7g_4core10intrinsics19transmute_diff_size
[Kani] current codegen location: Loc { file: "/home/alex/Documents/verify-rust-std/library/core/src/intrinsics/mod.rs", function: None, start_line: 4627, start_col: Some(1), end_line: 4627, end_col: Some(25), pragmas: [] }
error: could not compile `core` (lib)
Caused by:
process didn't exit successfully: `/home/alex/Documents/verify-rust-std/kani_build/target/kani/bin/kani-compiler --crate-name core --edition=2021 /home/alex/Documents/verify-rust-std/library/core/src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=94 --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --warn=unexpected_cfgs --check-cfg 'cfg(bootstrap)' --check-cfg 'cfg(no_fp_fmt_parse)' --check-cfg 'cfg(stdarch_intel_sde)' --check-cfg 'cfg(target_os, values("rtems"))' --check-cfg 'cfg(feature, values(any()))' --check-cfg 'cfg(docsrs)' --check-cfg 'cfg(feature, values("debug_refcell", "optimize_for_size", "panic_immediate_abort"))' -C metadata=0479e265945e2b67 -C extra-filename=-0479e265945e2b67 --out-dir /home/alex/Documents/verify-rust-std/target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -Z force-unstable-if-unmarked -L dependency=/home/alex/Documents/verify-rust-std/target/kani_verify_std/target/x86_64-unknown-linux-gnu/debug/deps -L dependency=/home/alex/Documents/verify-rust-std/target/kani_verify_std/target/debug/deps --extern safety=/home/alex/Documents/verify-rust-std/target/kani_verify_std/target/debug/deps/libsafety-2115ed584053727e.so --cap-lints allow -C overflow-checks=on -Z unstable-options -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -Z always-encode-mir --cfg=kani -Z 'crate-attr=feature(register_tool)' -Z 'crate-attr=register_tool(kanitool)' -L /home/alex/Documents/verify-rust-std/kani_build/target/kani/no_core/lib --extern kani_core -C panic=abort -C symbol-mangling-version=v0 -Z panic_abort_tests=yes -Z mir-enable-passes=-RemoveStorageMarkers '--check-cfg=cfg(kani)' --kani-compiler '-Cllvm-args=--check-version=0.56.0 --log-level=warn --assertion-reach-checks --enable-stubbing -Z unstable-options -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts' -Cllvm-args=--reachability=harnesses -Cllvm-args=--ignore-global-asm` (exit status: 101)