From e6067e9dc0009c30ac101734bdadc563fbfb10fe Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 26 Nov 2024 16:11:01 -0800 Subject: [PATCH 1/6] Add a Kani function that checks if the range of a float is valid for conversion to int --- .../codegen_cprover_gotoc/overrides/hooks.rs | 52 ++++++++++++++++++- .../src/kani_middle/kani_functions.rs | 3 ++ .../kani_middle/transform/kani_intrinsics.rs | 32 +++++++++++- library/kani_core/src/float.rs | 31 +++++++++++ library/kani_core/src/lib.rs | 9 ++++ .../invalid_float.expected | 1 + .../float-to-int-in-range/invalid_float.rs | 11 ++++ .../invalid_int.expected | 1 + .../float-to-int-in-range/invalid_int.rs | 11 ++++ tests/kani/FloatToIntInRange/test.rs | 25 +++++++++ 10 files changed, 174 insertions(+), 2 deletions(-) create mode 100644 library/kani_core/src/float.rs create mode 100644 tests/expected/float-to-int-in-range/invalid_float.expected create mode 100644 tests/expected/float-to-int-in-range/invalid_float.rs create mode 100644 tests/expected/float-to-int-in-range/invalid_int.expected create mode 100644 tests/expected/float-to-int-in-range/invalid_int.rs create mode 100644 tests/kani/FloatToIntInRange/test.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 75943b23a392..47856fde7cb8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -8,8 +8,8 @@ //! It would be too nasty if we spread around these sort of undocumented hooks in place, so //! this module addresses this issue. -use crate::codegen_cprover_gotoc::GotocCtx; use crate::codegen_cprover_gotoc::codegen::{PropertyClass, bb_label}; +use crate::codegen_cprover_gotoc::{GotocCtx, utils}; use crate::kani_middle::attributes; use crate::kani_middle::kani_functions::{KaniFunction, KaniHook}; use crate::unwrap_or_return_codegen_unimplemented_stmt; @@ -19,6 +19,7 @@ use rustc_middle::ty::TyCtxt; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::{BasicBlockIdx, Place}; +use stable_mir::ty::RigidTy; use stable_mir::{CrateDef, ty::Span}; use std::collections::HashMap; use std::rc::Rc; @@ -315,6 +316,54 @@ impl GotocHook for IsAllocated { } } +/// This is the hook for the `kani::float::float_to_int_in_range` intrinsic +/// TODO: This should be replaced by a Rust function instead so that it's +/// independent of the backend +struct FloatToIntInRange; +impl GotocHook for FloatToIntInRange { + fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { + unreachable!("{UNEXPECTED_CALL}") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + instance: Instance, + mut fargs: Vec, + assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 1); + let float = fargs.remove(0); + let target = target.unwrap(); + let loc = gcx.codegen_span_stable(span); + + let generic_args = instance.args().0; + let RigidTy::Float(float_ty) = generic_args[0].expect_ty().kind().rigid().unwrap().clone() + else { + unreachable!() + }; + let integral_ty = generic_args[1].expect_ty().kind().rigid().unwrap().clone(); + + let is_in_range = utils::codegen_in_range_expr( + &float, + float_ty, + integral_ty, + gcx.symbol_table.machine_model(), + ) + .cast_to(Type::CInteger(CIntType::Bool)); + + let pe = unwrap_or_return_codegen_unimplemented_stmt!( + gcx, + gcx.codegen_place_stable(assign_to, loc) + ) + .goto_expr; + + Stmt::block(vec![pe.assign(is_in_range, loc), Stmt::goto(bb_label(target), loc)], loc) + } +} + /// Encodes __CPROVER_pointer_object(ptr) struct PointerObject; impl GotocHook for PointerObject { @@ -663,6 +712,7 @@ pub fn fn_hooks() -> GotocHooks { (KaniHook::PointerOffset, Rc::new(PointerOffset)), (KaniHook::UntrackedDeref, Rc::new(UntrackedDeref)), (KaniHook::InitContracts, Rc::new(InitContracts)), + (KaniHook::FloatToIntInRange, Rc::new(FloatToIntInRange)), ]; GotocHooks { kani_lib_hooks: HashMap::from(kani_lib_hooks), diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 20d0b9219b20..6a136f1a5647 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -125,6 +125,9 @@ pub enum KaniHook { Check, #[strum(serialize = "CoverHook")] Cover, + // TODO: this is temporarily implemented as a hook, but should be implemented as an intrinsic + #[strum(serialize = "FloatToIntInRangeHook")] + FloatToIntInRange, #[strum(serialize = "InitContractsHook")] InitContracts, #[strum(serialize = "IsAllocatedHook")] diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 206c0160a80d..fa74d17a5822 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -10,7 +10,7 @@ use crate::args::ExtraChecks; use crate::kani_middle::abi::LayoutOf; use crate::kani_middle::attributes::KaniAttributes; -use crate::kani_middle::kani_functions::{KaniFunction, KaniIntrinsic, KaniModel}; +use crate::kani_middle::kani_functions::{KaniFunction, KaniHook, KaniIntrinsic, KaniModel}; use crate::kani_middle::transform::body::{ CheckType, InsertPosition, MutableBody, SourceInstruction, }; @@ -22,6 +22,8 @@ use crate::kani_middle::transform::check_values::{build_limits, ty_validity_per_ use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; +use stable_mir::CrateDef; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ AggregateKind, BasicBlock, BinOp, Body, ConstOperand, Local, Mutability, Operand, Place, @@ -77,6 +79,16 @@ impl TransformPass for IntrinsicGeneratorPass { // This is handled in contracts pass for now. KaniIntrinsic::WriteAny | KaniIntrinsic::AnyModifies => (false, body), } + } else if let Some(kani_hook) = + attributes.fn_marker().and_then(|name| KaniHook::from_str(name.as_str()).ok()) + { + match kani_hook { + KaniHook::FloatToIntInRange => { + IntrinsicGeneratorPass::check_float_to_int_in_range_valid_types(tcx, instance); + (false, body) + } + _ => (false, body), + } } else { (false, body) } @@ -606,6 +618,24 @@ impl IntrinsicGeneratorPass { Place::from(RETURN_LOCAL), ); } + + fn check_float_to_int_in_range_valid_types(tcx: TyCtxt, instance: Instance) { + let generic_args = instance.args().0; + let arg0 = generic_args[0].expect_ty(); + if !arg0.kind().is_float() { + let msg = format!( + "Invalid type for first argument of `float_to_int_in_range` intrinsic. Expected a float type. Got `{arg0}`" + ); + tcx.dcx().span_err(rustc_internal::internal(tcx, instance.def.span()), msg); + } + let arg1 = generic_args[1].expect_ty(); + if !arg1.kind().is_integral() { + let msg = format!( + "Invalid type for second argument of `float_to_int_in_range` intrinsic. Expected an integer type. Got `{arg1}`" + ); + tcx.dcx().span_err(rustc_internal::internal(tcx, instance.def.span()), msg); + } + } } /// Build an Rvalue `Some(val)`. diff --git a/library/kani_core/src/float.rs b/library/kani_core/src/float.rs new file mode 100644 index 000000000000..2d88917cc58c --- /dev/null +++ b/library/kani_core/src/float.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module contains functions useful for float-related checks + +#[macro_export] +macro_rules! generate_float { + ($core:path) => { + /// Returns whether the given float `value` satisfies the range + /// condition of the `to_int_unchecked` methods, namely that the `value` + /// after truncation is in range of the target `Int` + /// + /// # Example: + /// + /// ```no_run + /// let f: f32 = 145.7; + /// let fits_in_i8 = kani::float::float_to_int_in_range::(f); + /// // doesn't fit in `i8` because the value after truncation (`145.0`) is larger than `i8::MAX` + /// assert!(!fits_in_i8); + /// + /// let f: f64 = 1e6; + /// let fits_in_u32 = kani::float::float_to_int_in_range::(f); + /// // fits in `u32` because the value after truncation (`1e6`) is smaller than `u32::MAX` + /// assert!(fits_in_u32); + /// ``` + #[kanitool::fn_marker = "FloatToIntInRangeHook"] + pub fn float_to_int_in_range(value: Float) -> bool { + kani::kani_intrinsic() + } + }; +} diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 551d522ba7e2..0a9a5b56ee9d 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -21,6 +21,7 @@ #![feature(f128)] mod arbitrary; +mod float; mod mem; mod mem_init; mod models; @@ -45,6 +46,10 @@ macro_rules! kani_lib { kani_core::generate_arbitrary!(core); kani_core::generate_models!(); + pub mod float { + kani_core::generate_float!(core); + } + pub mod mem { kani_core::kani_mem!(core); } @@ -61,6 +66,10 @@ macro_rules! kani_lib { kani_core::generate_arbitrary!(std); kani_core::generate_models!(); + pub mod float { + kani_core::generate_float!(std); + } + pub mod mem { kani_core::kani_mem!(std); } diff --git a/tests/expected/float-to-int-in-range/invalid_float.expected b/tests/expected/float-to-int-in-range/invalid_float.expected new file mode 100644 index 000000000000..c52939f7c145 --- /dev/null +++ b/tests/expected/float-to-int-in-range/invalid_float.expected @@ -0,0 +1 @@ +error: Invalid type for first argument of `float_to_int_in_range` intrinsic. Expected a float type. Got `i32` diff --git a/tests/expected/float-to-int-in-range/invalid_float.rs b/tests/expected/float-to-int-in-range/invalid_float.rs new file mode 100644 index 000000000000..8a148f335f34 --- /dev/null +++ b/tests/expected/float-to-int-in-range/invalid_float.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks that Kani emits an error when +//! `kani::float::float_to_int_in_range` is instantiated with a non-float type + +#[kani::proof] +fn check_invalid_float() { + let i: i32 = 5; + let _c = kani::float::float_to_int_in_range::(i); +} diff --git a/tests/expected/float-to-int-in-range/invalid_int.expected b/tests/expected/float-to-int-in-range/invalid_int.expected new file mode 100644 index 000000000000..fcf5d394714f --- /dev/null +++ b/tests/expected/float-to-int-in-range/invalid_int.expected @@ -0,0 +1 @@ +error: Invalid type for second argument of `float_to_int_in_range` intrinsic. Expected an integer type. Got `bool` diff --git a/tests/expected/float-to-int-in-range/invalid_int.rs b/tests/expected/float-to-int-in-range/invalid_int.rs new file mode 100644 index 000000000000..34a8e1069a8e --- /dev/null +++ b/tests/expected/float-to-int-in-range/invalid_int.rs @@ -0,0 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks that Kani emits an error when +//! `kani::float::float_to_int_in_range` is instantiated with a non-integer type + +#[kani::proof] +fn check_invalid_integer() { + let f: f32 = kani::any(); + let _c = kani::float::float_to_int_in_range::(f); +} diff --git a/tests/kani/FloatToIntInRange/test.rs b/tests/kani/FloatToIntInRange/test.rs new file mode 100644 index 000000000000..ff790d4bf4e3 --- /dev/null +++ b/tests/kani/FloatToIntInRange/test.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks that `kani::float::float_to_int_in_range` works as expected + +#[kani::proof] +fn check_float_to_int_in_range() { + let f: f32 = 5.6; + let fits_in_u16 = kani::float::float_to_int_in_range::(f); + assert!(fits_in_u16); + let i: u16 = unsafe { f.to_int_unchecked() }; + assert_eq!(i, 5); + + let f: f32 = 145.7; + let fits_in_i8 = kani::float::float_to_int_in_range::(f); + // doesn't fit in `i8` because the value after truncation (`145.0`) is larger than `i8::MAX` + assert!(!fits_in_i8); + + let f: f64 = 1e6; + let fits_in_u32 = kani::float::float_to_int_in_range::(f); + // fits in `u32` because the value after truncation (`1e6`) is smaller than `u32::MAX` + assert!(fits_in_u32); + let i: u32 = unsafe { f.to_int_unchecked() }; + assert_eq!(i, 1_000_000); +} From 1523ad1bf5a5f5d5977a2f6cbe93b33e7d9b09e4 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 26 Nov 2024 20:55:08 -0800 Subject: [PATCH 2/6] Fix import --- library/kani_core/src/float.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/library/kani_core/src/float.rs b/library/kani_core/src/float.rs index 2d88917cc58c..409bf09eac6a 100644 --- a/library/kani_core/src/float.rs +++ b/library/kani_core/src/float.rs @@ -6,6 +6,7 @@ #[macro_export] macro_rules! generate_float { ($core:path) => { + use super::kani_intrinsic; /// Returns whether the given float `value` satisfies the range /// condition of the `to_int_unchecked` methods, namely that the `value` /// after truncation is in range of the target `Int` @@ -24,8 +25,9 @@ macro_rules! generate_float { /// assert!(fits_in_u32); /// ``` #[kanitool::fn_marker = "FloatToIntInRangeHook"] + #[inline(never)] pub fn float_to_int_in_range(value: Float) -> bool { - kani::kani_intrinsic() + kani_intrinsic() } }; } From 788d5d8d4421154df4509d05177fcaf0fbbd0df0 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Wed, 27 Nov 2024 15:46:59 -0800 Subject: [PATCH 3/6] Address PR comments --- .../codegen_cprover_gotoc/overrides/hooks.rs | 5 ++- .../kani_middle/transform/kani_intrinsics.rs | 32 +------------------ library/kani/src/lib.rs | 1 + library/kani_core/src/float.rs | 8 +++-- .../invalid_float.expected | 6 +++- .../invalid_int.expected | 6 +++- 6 files changed, 20 insertions(+), 38 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 47856fde7cb8..0a9e4e9e3d6d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -340,11 +340,10 @@ impl GotocHook for FloatToIntInRange { let loc = gcx.codegen_span_stable(span); let generic_args = instance.args().0; - let RigidTy::Float(float_ty) = generic_args[0].expect_ty().kind().rigid().unwrap().clone() - else { + let RigidTy::Float(float_ty) = *generic_args[0].expect_ty().kind().rigid().unwrap() else { unreachable!() }; - let integral_ty = generic_args[1].expect_ty().kind().rigid().unwrap().clone(); + let integral_ty = *generic_args[1].expect_ty().kind().rigid().unwrap(); let is_in_range = utils::codegen_in_range_expr( &float, diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index fa74d17a5822..206c0160a80d 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -10,7 +10,7 @@ use crate::args::ExtraChecks; use crate::kani_middle::abi::LayoutOf; use crate::kani_middle::attributes::KaniAttributes; -use crate::kani_middle::kani_functions::{KaniFunction, KaniHook, KaniIntrinsic, KaniModel}; +use crate::kani_middle::kani_functions::{KaniFunction, KaniIntrinsic, KaniModel}; use crate::kani_middle::transform::body::{ CheckType, InsertPosition, MutableBody, SourceInstruction, }; @@ -22,8 +22,6 @@ use crate::kani_middle::transform::check_values::{build_limits, ty_validity_per_ use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; -use rustc_smir::rustc_internal; -use stable_mir::CrateDef; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ AggregateKind, BasicBlock, BinOp, Body, ConstOperand, Local, Mutability, Operand, Place, @@ -79,16 +77,6 @@ impl TransformPass for IntrinsicGeneratorPass { // This is handled in contracts pass for now. KaniIntrinsic::WriteAny | KaniIntrinsic::AnyModifies => (false, body), } - } else if let Some(kani_hook) = - attributes.fn_marker().and_then(|name| KaniHook::from_str(name.as_str()).ok()) - { - match kani_hook { - KaniHook::FloatToIntInRange => { - IntrinsicGeneratorPass::check_float_to_int_in_range_valid_types(tcx, instance); - (false, body) - } - _ => (false, body), - } } else { (false, body) } @@ -618,24 +606,6 @@ impl IntrinsicGeneratorPass { Place::from(RETURN_LOCAL), ); } - - fn check_float_to_int_in_range_valid_types(tcx: TyCtxt, instance: Instance) { - let generic_args = instance.args().0; - let arg0 = generic_args[0].expect_ty(); - if !arg0.kind().is_float() { - let msg = format!( - "Invalid type for first argument of `float_to_int_in_range` intrinsic. Expected a float type. Got `{arg0}`" - ); - tcx.dcx().span_err(rustc_internal::internal(tcx, instance.def.span()), msg); - } - let arg1 = generic_args[1].expect_ty(); - if !arg1.kind().is_integral() { - let msg = format!( - "Invalid type for second argument of `float_to_int_in_range` intrinsic. Expected an integer type. Got `{arg1}`" - ); - tcx.dcx().span_err(rustc_internal::internal(tcx, instance.def.span()), msg); - } - } } /// Build an Rvalue `Some(val)`. diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index fc47f8fec423..b284a3544b67 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -20,6 +20,7 @@ #![feature(ptr_metadata)] #![feature(f16)] #![feature(f128)] +#![feature(convert_float_to_int)] // Allow us to use `kani::` to access crate features. extern crate self as kani; diff --git a/library/kani_core/src/float.rs b/library/kani_core/src/float.rs index 409bf09eac6a..fb18d75d0fcd 100644 --- a/library/kani_core/src/float.rs +++ b/library/kani_core/src/float.rs @@ -5,8 +5,9 @@ #[macro_export] macro_rules! generate_float { - ($core:path) => { + ($core:tt) => { use super::kani_intrinsic; + use $core::convert::FloatToInt; /// Returns whether the given float `value` satisfies the range /// condition of the `to_int_unchecked` methods, namely that the `value` /// after truncation is in range of the target `Int` @@ -26,7 +27,10 @@ macro_rules! generate_float { /// ``` #[kanitool::fn_marker = "FloatToIntInRangeHook"] #[inline(never)] - pub fn float_to_int_in_range(value: Float) -> bool { + pub fn float_to_int_in_range(value: Float) -> bool + where + Float: FloatToInt, + { kani_intrinsic() } }; diff --git a/tests/expected/float-to-int-in-range/invalid_float.expected b/tests/expected/float-to-int-in-range/invalid_float.expected index c52939f7c145..bb9d3a623997 100644 --- a/tests/expected/float-to-int-in-range/invalid_float.expected +++ b/tests/expected/float-to-int-in-range/invalid_float.expected @@ -1 +1,5 @@ -error: Invalid type for first argument of `float_to_int_in_range` intrinsic. Expected a float type. Got `i32` +error[E0277]: the trait bound `i32: std::convert::FloatToInt` is not satisfied +invalid_float.rs: +| let _c = kani::float::float_to_int_in_range::(i); +| ^^^ the trait `std::convert::FloatToInt` is not implemented for `i32` +| diff --git a/tests/expected/float-to-int-in-range/invalid_int.expected b/tests/expected/float-to-int-in-range/invalid_int.expected index fcf5d394714f..84c3d6fe29bf 100644 --- a/tests/expected/float-to-int-in-range/invalid_int.expected +++ b/tests/expected/float-to-int-in-range/invalid_int.expected @@ -1 +1,5 @@ -error: Invalid type for second argument of `float_to_int_in_range` intrinsic. Expected an integer type. Got `bool` +error[E0277]: the trait bound `f32: std::convert::FloatToInt` is not satisfied +invalid_int.rs: +| let _c = kani::float::float_to_int_in_range::(f); +| ^^^ the trait `std::convert::FloatToInt` is not implemented for `f32` +| From be2eae3b347340f4a7f7a05f0b0cc75747a43228 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Wed, 27 Nov 2024 15:57:33 -0800 Subject: [PATCH 4/6] Mark API as unstable --- kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs | 2 +- kani_metadata/src/unstable.rs | 2 ++ library/kani_core/src/float.rs | 5 +++++ tests/kani/FloatToIntInRange/test.rs | 1 + 4 files changed, 9 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 0a9e4e9e3d6d..d228965f7633 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -343,7 +343,7 @@ impl GotocHook for FloatToIntInRange { let RigidTy::Float(float_ty) = *generic_args[0].expect_ty().kind().rigid().unwrap() else { unreachable!() }; - let integral_ty = *generic_args[1].expect_ty().kind().rigid().unwrap(); + let integral_ty = generic_args[1].expect_ty().kind().rigid().unwrap().clone(); let is_in_range = utils::codegen_in_range_expr( &float, diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index ff2ca5c4830a..e4f5bcaadd57 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -100,6 +100,8 @@ pub enum UnstableFeature { UnstableOptions, /// The list subcommand [RFC 13](https://model-checking.github.io/kani/rfc/rfcs/0013-list.html) List, + /// Kani APIs related to floating-point operations (e.g. `float_to_int_in_range`) + FloatLib, } impl UnstableFeature { diff --git a/library/kani_core/src/float.rs b/library/kani_core/src/float.rs index fb18d75d0fcd..d04088d9824f 100644 --- a/library/kani_core/src/float.rs +++ b/library/kani_core/src/float.rs @@ -25,6 +25,11 @@ macro_rules! generate_float { /// // fits in `u32` because the value after truncation (`1e6`) is smaller than `u32::MAX` /// assert!(fits_in_u32); /// ``` + #[crate::kani::unstable_feature( + feature = "float-lib", + issue = "none", + reason = "experimental floating-point API" + )] #[kanitool::fn_marker = "FloatToIntInRangeHook"] #[inline(never)] pub fn float_to_int_in_range(value: Float) -> bool diff --git a/tests/kani/FloatToIntInRange/test.rs b/tests/kani/FloatToIntInRange/test.rs index ff790d4bf4e3..2fca679f477a 100644 --- a/tests/kani/FloatToIntInRange/test.rs +++ b/tests/kani/FloatToIntInRange/test.rs @@ -1,5 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfloat-lib //! This test checks that `kani::float::float_to_int_in_range` works as expected From 895a01fd16512a1d83b1b0f9e019487d8fd0d12b Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Wed, 27 Nov 2024 16:04:52 -0800 Subject: [PATCH 5/6] Clippy fix --- library/kani_core/src/float.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/kani_core/src/float.rs b/library/kani_core/src/float.rs index d04088d9824f..77ce8f91ece6 100644 --- a/library/kani_core/src/float.rs +++ b/library/kani_core/src/float.rs @@ -3,6 +3,7 @@ //! This module contains functions useful for float-related checks +#[allow(clippy::crate_in_macro_def)] #[macro_export] macro_rules! generate_float { ($core:tt) => { From 9cd21f3355ae01f99303dcdef4e3d3d3aa03cd88 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Wed, 27 Nov 2024 16:36:03 -0800 Subject: [PATCH 6/6] Use core directly --- library/kani_core/src/float.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/kani_core/src/float.rs b/library/kani_core/src/float.rs index 77ce8f91ece6..44475af80a51 100644 --- a/library/kani_core/src/float.rs +++ b/library/kani_core/src/float.rs @@ -6,9 +6,9 @@ #[allow(clippy::crate_in_macro_def)] #[macro_export] macro_rules! generate_float { - ($core:tt) => { + ($core:path) => { use super::kani_intrinsic; - use $core::convert::FloatToInt; + use core::convert::FloatToInt; /// Returns whether the given float `value` satisfies the range /// condition of the `to_int_unchecked` methods, namely that the `value` /// after truncation is in range of the target `Int`