From ba251bf6a4b23fbf4c5c65c5020f246755a62417 Mon Sep 17 00:00:00 2001 From: Alex Reisner <1683937+reisnera@users.noreply.github.com> Date: Fri, 18 Aug 2023 16:34:54 -0500 Subject: [PATCH] Add integer overflow checking for simd_div and simd_rem (#2645) Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- docs/src/rust-feature-support/intrinsics.md | 8 ++-- .../codegen/intrinsic.rs | 46 ++++++++++++++++--- .../intrinsics/simd-div-rem-overflow/expected | 8 ++++ .../intrinsics/simd-div-rem-overflow/main.rs | 44 ++++++++++++++++++ .../SIMD/Operators/division_float.rs | 39 ++++++++++++++++ .../SIMD/Operators/remainder_float_fixme.rs | 39 ++++++++++++++++ 6 files changed, 173 insertions(+), 11 deletions(-) create mode 100644 tests/expected/intrinsics/simd-div-rem-overflow/expected create mode 100644 tests/expected/intrinsics/simd-div-rem-overflow/main.rs create mode 100644 tests/kani/Intrinsics/SIMD/Operators/division_float.rs create mode 100644 tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 73cb23aea34b..0705d3b00f1b 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -258,7 +258,7 @@ Name | Support | Notes | --- | --- | --- | `simd_add` | Yes | | `simd_and` | Yes | | -`simd_div` | Yes | Doesn't check for overflow cases [#1970](https://github.com/model-checking/kani/issues/1970) | +`simd_div` | Yes | | `simd_eq` | Yes | | `simd_extract` | Yes | | `simd_ge` | Yes | | @@ -269,9 +269,9 @@ Name | Support | Notes | `simd_mul` | Yes | | `simd_ne` | Yes | | `simd_or` | Yes | | -`simd_rem` | Yes | Doesn't check for overflow cases [#1970](https://github.com/model-checking/kani/issues/1970) | -`simd_shl` | Yes | Doesn't check for overflow cases [#1963](https://github.com/model-checking/kani/issues/1963) | -`simd_shr` | Yes | Doesn't check for overflow cases [#1963](https://github.com/model-checking/kani/issues/1963) | +`simd_rem` | Yes | Doesn't check for floating point overflow [#2669](https://github.com/model-checking/kani/issues/2669) | +`simd_shl` | Yes | | +`simd_shr` | Yes | | `simd_shuffle*` | Yes | | `simd_sub` | Yes | | `simd_xor` | Yes | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 8fc2742f2824..1f3134aa7d67 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -511,9 +511,11 @@ impl<'tcx> GotocCtx<'tcx> { loc, ), "simd_and" => codegen_intrinsic_binop!(bitand), - // TODO: `simd_div` and `simd_rem` don't check for overflow cases. - // - "simd_div" => codegen_intrinsic_binop!(div), + // TODO: `simd_rem` doesn't check for overflow cases for floating point operands. + // + "simd_div" | "simd_rem" => { + self.codegen_simd_div_with_overflow(fargs, intrinsic, p, loc) + } "simd_eq" => self.codegen_simd_cmp(Expr::vector_eq, fargs, p, span, farg_types, ret_ty), "simd_extract" => { self.codegen_intrinsic_simd_extract(fargs, p, farg_types, ret_ty, span) @@ -537,9 +539,6 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_simd_cmp(Expr::vector_neq, fargs, p, span, farg_types, ret_ty) } "simd_or" => codegen_intrinsic_binop!(bitor), - // TODO: `simd_div` and `simd_rem` don't check for overflow cases. - // - "simd_rem" => codegen_intrinsic_binop!(rem), "simd_shl" | "simd_shr" => { self.codegen_simd_shift_with_distance_check(fargs, intrinsic, p, loc) } @@ -1552,6 +1551,39 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_expr_to_place(p, e) } + /// Codegen for `simd_div` and `simd_rem` intrinsics. + /// This checks for overflow in signed integer division (i.e. when dividing the minimum integer + /// for the type by -1). Overflow checks on floating point division are handled by CBMC, as is + /// division by zero for both integers and floats. + fn codegen_simd_div_with_overflow( + &mut self, + fargs: Vec, + intrinsic: &str, + p: &Place<'tcx>, + loc: Location, + ) -> Stmt { + let op_fun = match intrinsic { + "simd_div" => Expr::div, + "simd_rem" => Expr::rem, + _ => unreachable!("expected simd_div or simd_rem"), + }; + let base_type = fargs[0].typ().base_type().unwrap().clone(); + if base_type.is_integer() && base_type.is_signed(self.symbol_table.machine_model()) { + let min_int_expr = base_type.min_int_expr(self.symbol_table.machine_model()); + let negative_one = Expr::int_constant(-1, base_type); + self.codegen_simd_op_with_overflow( + op_fun, + |a, b| a.eq(min_int_expr.clone()).and(b.eq(negative_one.clone())), + fargs, + intrinsic, + p, + loc, + ) + } else { + self.binop(p, fargs, op_fun) + } + } + /// Intrinsics which encode a SIMD arithmetic operation with overflow check. /// We expand the overflow check because CBMC overflow operations don't accept array as /// argument. @@ -1587,7 +1619,7 @@ impl<'tcx> GotocCtx<'tcx> { ); let res = op_fun(a, b); let expr_place = self.codegen_expr_to_place(p, res); - Stmt::block(vec![expr_place, check_stmt], loc) + Stmt::block(vec![check_stmt, expr_place], loc) } /// Intrinsics which encode a SIMD bitshift. diff --git a/tests/expected/intrinsics/simd-div-rem-overflow/expected b/tests/expected/intrinsics/simd-div-rem-overflow/expected new file mode 100644 index 000000000000..156854c7dcdc --- /dev/null +++ b/tests/expected/intrinsics/simd-div-rem-overflow/expected @@ -0,0 +1,8 @@ +FAILURE\ +attempt to compute simd_div which would overflow +UNREACHABLE\ +assertion failed: quotients.0 == quotients.1 +FAILURE\ +attempt to compute simd_rem which would overflow +UNREACHABLE\ +assertion failed: remainders.0 == remainders.1 \ No newline at end of file diff --git a/tests/expected/intrinsics/simd-div-rem-overflow/main.rs b/tests/expected/intrinsics/simd-div-rem-overflow/main.rs new file mode 100644 index 000000000000..e7f2e9fbc48f --- /dev/null +++ b/tests/expected/intrinsics/simd-div-rem-overflow/main.rs @@ -0,0 +1,44 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that the `simd_div` and `simd_rem` intrinsics check for integer overflows. + +#![feature(repr_simd, platform_intrinsics)] + +#[repr(simd)] +#[allow(non_camel_case_types)] +#[derive(Clone, Copy, PartialEq, Eq)] +pub struct i32x2(i32, i32); + +extern "platform-intrinsic" { + fn simd_div(x: T, y: T) -> T; + fn simd_rem(x: T, y: T) -> T; +} + +unsafe fn do_simd_div(dividends: i32x2, divisors: i32x2) -> i32x2 { + simd_div(dividends, divisors) +} + +unsafe fn do_simd_rem(dividends: i32x2, divisors: i32x2) -> i32x2 { + simd_rem(dividends, divisors) +} + +#[kani::proof] +fn test_simd_div_overflow() { + let dividend = i32::MIN; + let dividends = i32x2(dividend, dividend); + let divisor = -1; + let divisors = i32x2(divisor, divisor); + let quotients = unsafe { do_simd_div(dividends, divisors) }; + assert_eq!(quotients.0, quotients.1); +} + +#[kani::proof] +fn test_simd_rem_overflow() { + let dividend = i32::MIN; + let dividends = i32x2(dividend, dividend); + let divisor = -1; + let divisors = i32x2(divisor, divisor); + let remainders = unsafe { do_simd_rem(dividends, divisors) }; + assert_eq!(remainders.0, remainders.1); +} diff --git a/tests/kani/Intrinsics/SIMD/Operators/division_float.rs b/tests/kani/Intrinsics/SIMD/Operators/division_float.rs new file mode 100644 index 000000000000..97ea2e6e7ca7 --- /dev/null +++ b/tests/kani/Intrinsics/SIMD/Operators/division_float.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that the `simd_div` intrinsic returns the expected results for floating point numbers. +#![feature(repr_simd, platform_intrinsics)] + +#[repr(simd)] +#[allow(non_camel_case_types)] +#[derive(Clone, Copy, PartialEq, kani::Arbitrary)] +pub struct f32x2(f32, f32); + +impl f32x2 { + fn new_with(f: impl Fn() -> f32) -> Self { + f32x2(f(), f()) + } + + fn non_simd_div(self, divisors: Self) -> Self { + f32x2(self.0 / divisors.0, self.1 / divisors.1) + } +} + +extern "platform-intrinsic" { + fn simd_div(x: T, y: T) -> T; +} + +#[kani::proof] +fn test_simd_div() { + let dividends = f32x2::new_with(|| { + let multiplier = kani::any_where(|&n: &i8| n >= -5 && n <= 5); + 0.5 * f32::from(multiplier) + }); + let divisors = f32x2::new_with(|| { + let multiplier = kani::any_where(|&n: &i8| n != 0 && n >= -5 && n <= 5); + 0.5 * f32::from(multiplier) + }); + let normal_results = dividends.non_simd_div(divisors); + let simd_results = unsafe { simd_div(dividends, divisors) }; + assert_eq!(normal_results, simd_results); +} diff --git a/tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs b/tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs new file mode 100644 index 000000000000..c97e96896bcf --- /dev/null +++ b/tests/kani/Intrinsics/SIMD/Operators/remainder_float_fixme.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that the `simd_rem` intrinsic returns the expected results for floating point numbers. +#![feature(repr_simd, platform_intrinsics)] + +#[repr(simd)] +#[allow(non_camel_case_types)] +#[derive(Clone, Copy, PartialEq, kani::Arbitrary)] +pub struct f32x2(f32, f32); + +impl f32x2 { + fn new_with(f: impl Fn() -> f32) -> Self { + f32x2(f(), f()) + } + + fn non_simd_rem(self, divisors: Self) -> Self { + f32x2(self.0 % divisors.0, self.1 % divisors.1) + } +} + +extern "platform-intrinsic" { + fn simd_rem(x: T, y: T) -> T; +} + +#[kani::proof] +fn test_simd_rem() { + let dividends = f32x2::new_with(|| { + let multiplier = kani::any_where(|&n: &i8| n >= -5 && n <= 5); + 0.5 * f32::from(multiplier) + }); + let divisors = f32x2::new_with(|| { + let multiplier = kani::any_where(|&n: &i8| n != 0 && n >= -5 && n <= 5); + 0.5 * f32::from(multiplier) + }); + let normal_results = dividends.non_simd_rem(divisors); + let simd_results = unsafe { simd_rem(dividends, divisors) }; + assert_eq!(normal_results, simd_results); +}