kani icon indicating copy to clipboard operation
kani copied to clipboard

Handle new `F16` and `F128` types

Open zhassan-aws opened this issue 1 year ago • 3 comments

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

zhassan-aws avatar Mar 11 '24 18:03 zhassan-aws

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!

tgross35 avatar Mar 26 '24 08:03 tgross35

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?

jaisnan avatar Jun 28 '24 21:06 jaisnan

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)

tgross35 avatar Jun 28 '24 21:06 tgross35

#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).

carolynzech avatar Mar 17 '25 18:03 carolynzech