From e53511e3e4040e24269edc0a701b67be76c5b19e Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Wed, 27 Nov 2024 17:49:47 -0800 Subject: [PATCH] Add a Kani function that checks if the range of a float is valid for conversion to int (#3742) This introduces a new generic Kani function, `kani::float::float_to_int_in_range`, that can be used for checking if a floating-point value satisfies the range requirement of the `to_int_unchecked` methods, e.g https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked and https://doc.rust-lang.org/std/primitive.f64.html#method.to_int_unchecked. Resolves #3711 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../codegen_cprover_gotoc/overrides/hooks.rs | 51 ++++++++++++++++++- .../src/kani_middle/kani_functions.rs | 3 ++ kani_metadata/src/unstable.rs | 2 + library/kani/src/lib.rs | 1 + library/kani_core/src/float.rs | 43 ++++++++++++++++ library/kani_core/src/lib.rs | 9 ++++ .../invalid_float.expected | 5 ++ .../float-to-int-in-range/invalid_float.rs | 11 ++++ .../invalid_int.expected | 5 ++ .../float-to-int-in-range/invalid_int.rs | 11 ++++ tests/kani/FloatToIntInRange/test.rs | 26 ++++++++++ 11 files changed, 166 insertions(+), 1 deletion(-) 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..d228965f7633 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,53 @@ 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() 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 +711,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_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/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 new file mode 100644 index 000000000000..44475af80a51 --- /dev/null +++ b/library/kani_core/src/float.rs @@ -0,0 +1,43 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module contains functions useful for float-related checks + +#[allow(clippy::crate_in_macro_def)] +#[macro_export] +macro_rules! generate_float { + ($core:path) => { + 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` + /// + /// # 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); + /// ``` + #[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 + where + Float: FloatToInt, + { + 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..bb9d3a623997 --- /dev/null +++ b/tests/expected/float-to-int-in-range/invalid_float.expected @@ -0,0 +1,5 @@ +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_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..84c3d6fe29bf --- /dev/null +++ b/tests/expected/float-to-int-in-range/invalid_int.expected @@ -0,0 +1,5 @@ +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` +| 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..2fca679f477a --- /dev/null +++ b/tests/kani/FloatToIntInRange/test.rs @@ -0,0 +1,26 @@ +// 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 + +#[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); +}