Handle new `F16` and `F128` types
This is a tracking issue for adding support for the new 16-bit and 128-bit floating-point types that are being added to Rust.
Upstream tracking issue: https://github.com/rust-lang/rust/issues/116909
Just FYI these are super unstable and will basically ICE if you do anything at all with them. Hopefully that will change in a couple weeks.
Thanks for being on top of it!
Some support is being added as of this PR: https://github.com/model-checking/kani/pull/3306. @zhassan-aws is this enough to close the issue or should we keep the issue open till they're fully stable?
FYI most of the ICE paths have been removed (const time as casting being the last thing until https://github.com/rust-lang/rust/pull/127032). Platform support is still weak though, we're having some problems getting compiler_builtins updated.
See https://github.com/rust-lang/rust/blob/c4c0897a262d42f26f89aaca16ed52457f6a4f05/library/std/build.rs#L78-L127 if you need a rough estimate of what works where (I'll be keeping that up to date as more support gets added)
#3306 missed: https://github.com/model-checking/kani/blob/ce89f616e4e9de6746a1095d7e873c3f2404dff2/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs#L1405-L1407
which were added to TyCtxt in
https://github.com/rust-lang/rust/commit/e3f63d93755f2f62b4a52686f608b9664e87f092#diff-0c8c9cf0c0f8cda43eb64bbe5ef63c3239b0cf25901587b3c1f2b1d97a7e8441R340
Here's a minimal reproducer for this crash:
#![feature(f16)]
#![feature(repr_simd)]
#[repr(simd)]
struct f16x16([f16; 16]);
fn foo() -> f16x16 {
f16x16([1.0; 16])
}
(The simd layout ensures we get to this line:https://github.com/model-checking/kani/blob/ce89f616e4e9de6746a1095d7e873c3f2404dff2/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs#L1481 and thereby hit the ICE).