Skip to content

Commit

Permalink
Add a Kani function that checks if the range of a float is valid for …
Browse files Browse the repository at this point in the history
…conversion to int
  • Loading branch information
zhassan-aws committed Nov 27, 2024
1 parent 0ebf089 commit eaafa13
Show file tree
Hide file tree
Showing 10 changed files with 159 additions and 2 deletions.
42 changes: 41 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,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};
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,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<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() 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 {
Expand Down Expand Up @@ -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),
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
26 changes: 25 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,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,
Expand All @@ -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;
Expand Down Expand Up @@ -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)
}
Expand Down Expand Up @@ -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)`.
Expand Down
32 changes: 32 additions & 0 deletions library/kani_core/src/float.rs
Original file line number Diff line number Diff line change
@@ -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::<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"]
pub fn float_to_int_in_range<Float, Int>(value: Float) -> bool {
kani::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);
}
1 change: 1 addition & 0 deletions tests/expected/float-to-int-in-range/invalid_int.expected
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);
}

0 comments on commit eaafa13

Please sign in to comment.