Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add a Kani function that checks if the range of a float is valid for conversion to int #3742

Merged
merged 7 commits into from
Nov 28, 2024
Merged
Show file tree
Hide file tree
Changes from 2 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
52 changes: 51 additions & 1 deletion kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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<Expr>,
assign_to: &Place,
target: Option<BasicBlockIdx>,
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()
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
else {
unreachable!()
};
let integral_ty = generic_args[1].expect_ty().kind().rigid().unwrap().clone();
celinval marked this conversation as resolved.
Show resolved Hide resolved

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!(
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
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 {
Expand Down Expand Up @@ -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),
Expand Down
3 changes: 3 additions & 0 deletions kani-compiler/src/kani_middle/kani_functions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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")]
Expand Down
32 changes: 31 additions & 1 deletion kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
};
Expand All @@ -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,
Expand Down Expand Up @@ -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)
}
Expand Down Expand Up @@ -606,6 +618,24 @@ impl IntrinsicGeneratorPass {
Place::from(RETURN_LOCAL),
);
}

fn check_float_to_int_in_range_valid_types(tcx: TyCtxt, instance: Instance) {
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
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)`.
Expand Down
33 changes: 33 additions & 0 deletions library/kani_core/src/float.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
// 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) => {
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`
///
/// # Example:
///
/// ```no_run
/// let f: f32 = 145.7;
/// let fits_in_i8 = kani::float::float_to_int_in_range::<f32, i8>(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::<f64, u32>(f);
/// // fits in `u32` because the value after truncation (`1e6`) is smaller than `u32::MAX`
/// assert!(fits_in_u32);
/// ```
#[kanitool::fn_marker = "FloatToIntInRangeHook"]
#[inline(never)]
pub fn float_to_int_in_range<Float, Int>(value: Float) -> bool {
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
zhassan-aws marked this conversation as resolved.
Show resolved Hide resolved
kani_intrinsic()
}
};
}
9 changes: 9 additions & 0 deletions library/kani_core/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@
#![feature(f128)]

mod arbitrary;
mod float;
mod mem;
mod mem_init;
mod models;
Expand All @@ -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);
}
Expand All @@ -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);
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
error: Invalid type for first argument of `float_to_int_in_range` intrinsic. Expected a float type. Got `i32`
11 changes: 11 additions & 0 deletions tests/expected/float-to-int-in-range/invalid_float.rs
Original file line number Diff line number Diff line change
@@ -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::<i32, u8>(i);
}
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
error: Invalid type for second argument of `float_to_int_in_range` intrinsic. Expected an integer type. Got `bool`
11 changes: 11 additions & 0 deletions tests/expected/float-to-int-in-range/invalid_int.rs
Original file line number Diff line number Diff line change
@@ -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::<f32, bool>(f);
}
25 changes: 25 additions & 0 deletions tests/kani/FloatToIntInRange/test.rs
Original file line number Diff line number Diff line change
@@ -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::<f32, u16>(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::<f32, i8>(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::<f64, u32>(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);
}
Loading