From e6067e9dc0009c30ac101734bdadc563fbfb10fe Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 26 Nov 2024 16:11:01 -0800 Subject: [PATCH] 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); +}