diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 75943b23a392..701ad5bcaa26 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -8,7 +8,7 @@ //! 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::{utils, GotocCtx}; use crate::codegen_cprover_gotoc::codegen::{PropertyClass, bb_label}; use crate::kani_middle::attributes; use crate::kani_middle::kani_functions::{KaniFunction, KaniHook}; @@ -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,44 @@ 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 +702,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..b433f5b347c1 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,7 @@ 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::mir::mono::Instance; use stable_mir::mir::{ AggregateKind, BasicBlock, BinOp, Body, ConstOperand, Local, Mutability, Operand, Place, @@ -31,6 +32,7 @@ use stable_mir::target::MachineInfo; use stable_mir::ty::{ AdtDef, FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyKind, UintTy, }; +use stable_mir::CrateDef; use std::collections::HashMap; use std::fmt::Debug; use std::str::FromStr; @@ -77,6 +79,14 @@ 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 +616,20 @@ 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..9470db9447ac --- /dev/null +++ b/library/kani_core/src/float.rs @@ -0,0 +1,32 @@ +// 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..2bcecab154f7 --- /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..7ee96d550b3b --- /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); +}