From 08fe4b69a943a59177de61bf7966e3639b94258a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 28 Jan 2022 22:09:11 +0000 Subject: [PATCH 1/8] Support for fast math intrinsics --- .../cbmc/src/goto_program/expr.rs | 12 ++++- .../cbmc/src/goto_program/stmt.rs | 7 +++ .../symtab_transformer/transformer.rs | 1 + src/kani-compiler/cbmc/src/irep/irep_id.rs | 4 +- src/kani-compiler/cbmc/src/irep/to_irep.rs | 1 + .../src/codegen/intrinsic.rs | 50 +++++++++++++++++++ 6 files changed, 71 insertions(+), 4 deletions(-) diff --git a/src/kani-compiler/cbmc/src/goto_program/expr.rs b/src/kani-compiler/cbmc/src/goto_program/expr.rs index b9a291a4d79f..7f6ae43e2430 100644 --- a/src/kani-compiler/cbmc/src/goto_program/expr.rs +++ b/src/kani-compiler/cbmc/src/goto_program/expr.rs @@ -209,6 +209,8 @@ pub enum UnaryOperand { Bswap, /// `__CPROVER_DYNAMIC_OBJECT(self)` IsDynamicObject, + /// `isfinite(self)` + IsFinite, /// `!self` Not, /// `__CPROVER_OBJECT_SIZE(self)` @@ -856,7 +858,7 @@ impl Expr { || (lhs.typ.is_pointer() && rhs.typ.is_integer()) } OverflowMult | OverflowPlus => { - (lhs.typ == rhs.typ && lhs.typ.is_integer()) + (lhs.typ == rhs.typ && lhs.typ.is_numeric()) || (lhs.typ.is_pointer() && rhs.typ.is_integer()) } } @@ -1091,6 +1093,7 @@ impl Expr { Bitnot | BitReverse | Bswap | Popcount => arg.typ.is_integer(), CountLeadingZeros { .. } | CountTrailingZeros { .. } => arg.typ.is_integer(), IsDynamicObject | ObjectSize | PointerObject => arg.typ().is_pointer(), + IsFinite => arg.typ().is_floating_point(), PointerOffset => arg.typ == Type::void_pointer(), Not => arg.typ.is_bool(), UnaryMinus => arg.typ().is_numeric(), @@ -1103,7 +1106,7 @@ impl Expr { CountLeadingZeros { .. } | CountTrailingZeros { .. } => arg.typ.clone(), ObjectSize | PointerObject => Type::size_t(), PointerOffset => Type::ssize_t(), - IsDynamicObject | Not => Type::bool(), + IsDynamicObject | IsFinite | Not => Type::bool(), Popcount => arg.typ.clone(), } } @@ -1134,6 +1137,11 @@ impl Expr { self.unop(IsDynamicObject) } + /// `isfinite(self)` + pub fn is_finite(self) -> Self { + self.unop(IsFinite) + } + /// `-self` pub fn neg(self) -> Expr { self.unop(UnaryMinus) diff --git a/src/kani-compiler/cbmc/src/goto_program/stmt.rs b/src/kani-compiler/cbmc/src/goto_program/stmt.rs index d55bf2fa7b66..731e5a029a76 100644 --- a/src/kani-compiler/cbmc/src/goto_program/stmt.rs +++ b/src/kani-compiler/cbmc/src/goto_program/stmt.rs @@ -129,6 +129,13 @@ impl Stmt { _ => None, } } + + pub fn get_stmts(&self) -> Option<&Vec> { + match self.body() { + Block(stmts) => Some(stmts), + _ => None, + } + } } /// Fluent builders diff --git a/src/kani-compiler/cbmc/src/goto_program/symtab_transformer/transformer.rs b/src/kani-compiler/cbmc/src/goto_program/symtab_transformer/transformer.rs index 3f347e85ea6c..1076292ee06a 100644 --- a/src/kani-compiler/cbmc/src/goto_program/symtab_transformer/transformer.rs +++ b/src/kani-compiler/cbmc/src/goto_program/symtab_transformer/transformer.rs @@ -479,6 +479,7 @@ pub trait Transformer: Sized { UnaryOperand::BitReverse => transformed_e.bitreverse(), UnaryOperand::Bswap => transformed_e.bswap(), UnaryOperand::IsDynamicObject => transformed_e.dynamic_object(), + UnaryOperand::IsFinite => transformed_e.is_finite(), UnaryOperand::Not => transformed_e.not(), UnaryOperand::ObjectSize => transformed_e.object_size(), UnaryOperand::PointerObject => transformed_e.pointer_object(), diff --git a/src/kani-compiler/cbmc/src/irep/irep_id.rs b/src/kani-compiler/cbmc/src/irep/irep_id.rs index dffa7f06802f..f8cf3cf74f85 100644 --- a/src/kani-compiler/cbmc/src/irep/irep_id.rs +++ b/src/kani-compiler/cbmc/src/irep/irep_id.rs @@ -314,7 +314,7 @@ pub enum IrepId { ConstraintSelectOne, Cond, BvLiterals, - Isfinite, + IsFinite, Isinf, Isnormal, Alignof, @@ -1153,7 +1153,7 @@ impl ToString for IrepId { IrepId::ConstraintSelectOne => "constraint_select_one", IrepId::Cond => "cond", IrepId::BvLiterals => "bv_literals", - IrepId::Isfinite => "isfinite", + IrepId::IsFinite => "isfinite", IrepId::Isinf => "isinf", IrepId::Isnormal => "isnormal", IrepId::Alignof => "alignof", diff --git a/src/kani-compiler/cbmc/src/irep/to_irep.rs b/src/kani-compiler/cbmc/src/irep/to_irep.rs index 3ad1bf41f7b0..11601e93b629 100644 --- a/src/kani-compiler/cbmc/src/irep/to_irep.rs +++ b/src/kani-compiler/cbmc/src/irep/to_irep.rs @@ -103,6 +103,7 @@ impl ToIrepId for UnaryOperand { UnaryOperand::CountLeadingZeros { .. } => IrepId::CountLeadingZeros, UnaryOperand::CountTrailingZeros { .. } => IrepId::CountTrailingZeros, UnaryOperand::IsDynamicObject => IrepId::IsDynamicObject, + UnaryOperand::IsFinite => IrepId::IsFinite, UnaryOperand::Not => IrepId::Not, UnaryOperand::ObjectSize => IrepId::ObjectSize, UnaryOperand::PointerObject => IrepId::PointerObject, diff --git a/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs b/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs index 29acadf54457..7e9db9365dee 100644 --- a/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs +++ b/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs @@ -391,11 +391,36 @@ impl<'tcx> GotocCtx<'tcx> { "expf64" => codegen_simple_intrinsic!(Exp), "fabsf32" => codegen_simple_intrinsic!(Fabsf), "fabsf64" => codegen_simple_intrinsic!(Fabs), + "fadd_fast" => { + let fargs_clone = fargs.clone(); + let binop_block = codegen_op_with_overflow_check!(add_overflow); + self.add_finite_args_checks(intrinsic, fargs_clone, binop_block, span) + } + "fdiv_fast" => { + let fargs_clone = fargs.clone(); + let binop_block = codegen_intrinsic_binop!(div); + self.add_finite_args_checks(intrinsic, fargs_clone, binop_block, span) + } "floorf32" => codegen_simple_intrinsic!(Floorf), "floorf64" => codegen_simple_intrinsic!(Floor), "fmaf32" => codegen_simple_intrinsic!(Fmaf), "fmaf64" => codegen_simple_intrinsic!(Fma), + "fmul_fast" => { + let fargs_clone = fargs.clone(); + let binop_block = codegen_op_with_overflow_check!(mul_overflow); + self.add_finite_args_checks(intrinsic, fargs_clone, binop_block, span) + } "forget" => Stmt::skip(loc), + "frem_fast" => { + let fargs_clone = fargs.clone(); + let binop_block = codegen_intrinsic_binop!(rem); + self.add_finite_args_checks(intrinsic, fargs_clone, binop_block, span) + } + "fsub_fast" => { + let fargs_clone = fargs.clone(); + let binop_block = codegen_op_with_overflow_check!(sub_overflow); + self.add_finite_args_checks(intrinsic, fargs_clone, binop_block, span) + } "likely" => self.codegen_expr_to_place(p, fargs.remove(0)), "log10f32" => codegen_simple_intrinsic!(Log10f), "log10f64" => codegen_simple_intrinsic!(Log10), @@ -520,6 +545,31 @@ impl<'tcx> GotocCtx<'tcx> { } } + // Fast math intrinsics for floating point operations like `fadd_fast` + // assume that their inputs are finite: + // https://doc.rust-lang.org/std/intrinsics/fn.fadd_fast.html + // This function adds assertions to the block statement which performs the + // operation and checks for overflow failures. + fn add_finite_args_checks( + &mut self, + intrinsic: &str, + mut fargs: Vec, + block: Stmt, + span: Option, + ) -> Stmt { + let arg1 = fargs.remove(0); + let arg2 = fargs.remove(0); + let msg1 = format!("first argument for {} is finite", intrinsic); + let msg2 = format!("second argument for {} is finite", intrinsic); + let loc = self.codegen_span_option(span); + let finite_check1 = Stmt::assert(arg1.is_finite(), msg1.as_str(), loc.clone()); + let finite_check2 = Stmt::assert(arg2.is_finite(), msg2.as_str(), loc.clone()); + let mut finite_checks = vec![finite_check1, finite_check2]; + let mut block_stmts = block.get_stmts().unwrap().clone(); + finite_checks.append(&mut block_stmts); + Stmt::block(finite_checks, loc) + } + fn codegen_exact_div(&mut self, mut fargs: Vec, p: &Place<'tcx>, loc: Location) -> Stmt { // Check for undefined behavior conditions defined in // https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html From ab753858263028de2a77863bda2b01fe092bcd24 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 1 Feb 2022 20:32:58 +0000 Subject: [PATCH 2/8] Add (failing) positive test for `fadd_fast` --- fast.rs | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 fast.rs diff --git a/fast.rs b/fast.rs new file mode 100644 index 000000000000..a5c87a3edc33 --- /dev/null +++ b/fast.rs @@ -0,0 +1,13 @@ +#![feature(core_intrinsics)] + +fn main() { + let x: f64 = kani::any(); + let y: f64 = kani::any(); + kani::assume(x.is_finite()); + kani::assume(y.is_finite()); + kani::assume(x + y < f64::MAX); + kani::assume(x + y > f64::MIN); + + let z = unsafe { std::intrinsics::fadd_fast(x, y) }; + let z2 = x + y; +} \ No newline at end of file From b4893e2bbc44f2aa8df82ff9a35cd8e7ac376445 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 4 Feb 2022 22:03:44 +0000 Subject: [PATCH 3/8] Undo change in `typecheck_binop_args` --- src/kani-compiler/cbmc/src/goto_program/expr.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kani-compiler/cbmc/src/goto_program/expr.rs b/src/kani-compiler/cbmc/src/goto_program/expr.rs index 7f6ae43e2430..ed4c9c89e987 100644 --- a/src/kani-compiler/cbmc/src/goto_program/expr.rs +++ b/src/kani-compiler/cbmc/src/goto_program/expr.rs @@ -858,7 +858,7 @@ impl Expr { || (lhs.typ.is_pointer() && rhs.typ.is_integer()) } OverflowMult | OverflowPlus => { - (lhs.typ == rhs.typ && lhs.typ.is_numeric()) + (lhs.typ == rhs.typ && lhs.typ.is_integer()) || (lhs.typ.is_pointer() && rhs.typ.is_integer()) } } From 38d030c1058628c03f9e3ccf89e1b6ee334d7279 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 7 Feb 2022 15:41:30 +0000 Subject: [PATCH 4/8] Encode fast math intrinsics as regular binops --- .../src/codegen/intrinsic.rs | 29 +++++++++---------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs b/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs index 7e9db9365dee..add7ed3b6764 100644 --- a/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs +++ b/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs @@ -393,13 +393,13 @@ impl<'tcx> GotocCtx<'tcx> { "fabsf64" => codegen_simple_intrinsic!(Fabs), "fadd_fast" => { let fargs_clone = fargs.clone(); - let binop_block = codegen_op_with_overflow_check!(add_overflow); - self.add_finite_args_checks(intrinsic, fargs_clone, binop_block, span) + let binop_stmt = codegen_intrinsic_binop!(plus); + self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) } "fdiv_fast" => { let fargs_clone = fargs.clone(); - let binop_block = codegen_intrinsic_binop!(div); - self.add_finite_args_checks(intrinsic, fargs_clone, binop_block, span) + let binop_stmt = codegen_intrinsic_binop!(div); + self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) } "floorf32" => codegen_simple_intrinsic!(Floorf), "floorf64" => codegen_simple_intrinsic!(Floor), @@ -407,19 +407,19 @@ impl<'tcx> GotocCtx<'tcx> { "fmaf64" => codegen_simple_intrinsic!(Fma), "fmul_fast" => { let fargs_clone = fargs.clone(); - let binop_block = codegen_op_with_overflow_check!(mul_overflow); - self.add_finite_args_checks(intrinsic, fargs_clone, binop_block, span) + let binop_stmt = codegen_intrinsic_binop!(mul); + self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) } "forget" => Stmt::skip(loc), "frem_fast" => { let fargs_clone = fargs.clone(); - let binop_block = codegen_intrinsic_binop!(rem); - self.add_finite_args_checks(intrinsic, fargs_clone, binop_block, span) + let binop_stmt = codegen_intrinsic_binop!(rem); + self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) } "fsub_fast" => { let fargs_clone = fargs.clone(); - let binop_block = codegen_op_with_overflow_check!(sub_overflow); - self.add_finite_args_checks(intrinsic, fargs_clone, binop_block, span) + let binop_stmt = codegen_intrinsic_binop!(sub); + self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) } "likely" => self.codegen_expr_to_place(p, fargs.remove(0)), "log10f32" => codegen_simple_intrinsic!(Log10f), @@ -548,13 +548,13 @@ impl<'tcx> GotocCtx<'tcx> { // Fast math intrinsics for floating point operations like `fadd_fast` // assume that their inputs are finite: // https://doc.rust-lang.org/std/intrinsics/fn.fadd_fast.html - // This function adds assertions to the block statement which performs the + // This function adds assertions to the statement which performs the // operation and checks for overflow failures. fn add_finite_args_checks( &mut self, intrinsic: &str, mut fargs: Vec, - block: Stmt, + stmt: Stmt, span: Option, ) -> Stmt { let arg1 = fargs.remove(0); @@ -564,10 +564,7 @@ impl<'tcx> GotocCtx<'tcx> { let loc = self.codegen_span_option(span); let finite_check1 = Stmt::assert(arg1.is_finite(), msg1.as_str(), loc.clone()); let finite_check2 = Stmt::assert(arg2.is_finite(), msg2.as_str(), loc.clone()); - let mut finite_checks = vec![finite_check1, finite_check2]; - let mut block_stmts = block.get_stmts().unwrap().clone(); - finite_checks.append(&mut block_stmts); - Stmt::block(finite_checks, loc) + Stmt::block(vec![finite_check1, finite_check2, stmt], loc) } fn codegen_exact_div(&mut self, mut fargs: Vec, p: &Place<'tcx>, loc: Location) -> Stmt { From 93586e86a370a58c7ed12c71c06855c0ebbb8e59 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 7 Feb 2022 23:18:15 +0000 Subject: [PATCH 5/8] Add all tests for fast math intrinsics --- fast.rs | 13 -------- tests/kani/Intrinsics/FastMath/add.rs | 19 +++++++++++ .../kani/Intrinsics/FastMath/add_overflow.rs | 12 +++++++ tests/kani/Intrinsics/FastMath/div.rs | 32 +++++++++++++++++++ .../kani/Intrinsics/FastMath/div_overflow.rs | 12 +++++++ tests/kani/Intrinsics/FastMath/mul.rs | 29 +++++++++++++++++ .../kani/Intrinsics/FastMath/mul_overflow.rs | 12 +++++++ tests/kani/Intrinsics/FastMath/rem.rs | 32 +++++++++++++++++++ .../kani/Intrinsics/FastMath/rem_overflow.rs | 12 +++++++ tests/kani/Intrinsics/FastMath/sub.rs | 19 +++++++++++ .../kani/Intrinsics/FastMath/sub_overflow.rs | 12 +++++++ 11 files changed, 191 insertions(+), 13 deletions(-) delete mode 100644 fast.rs create mode 100644 tests/kani/Intrinsics/FastMath/add.rs create mode 100644 tests/kani/Intrinsics/FastMath/add_overflow.rs create mode 100644 tests/kani/Intrinsics/FastMath/div.rs create mode 100644 tests/kani/Intrinsics/FastMath/div_overflow.rs create mode 100644 tests/kani/Intrinsics/FastMath/mul.rs create mode 100644 tests/kani/Intrinsics/FastMath/mul_overflow.rs create mode 100644 tests/kani/Intrinsics/FastMath/rem.rs create mode 100644 tests/kani/Intrinsics/FastMath/rem_overflow.rs create mode 100644 tests/kani/Intrinsics/FastMath/sub.rs create mode 100644 tests/kani/Intrinsics/FastMath/sub_overflow.rs diff --git a/fast.rs b/fast.rs deleted file mode 100644 index a5c87a3edc33..000000000000 --- a/fast.rs +++ /dev/null @@ -1,13 +0,0 @@ -#![feature(core_intrinsics)] - -fn main() { - let x: f64 = kani::any(); - let y: f64 = kani::any(); - kani::assume(x.is_finite()); - kani::assume(y.is_finite()); - kani::assume(x + y < f64::MAX); - kani::assume(x + y > f64::MIN); - - let z = unsafe { std::intrinsics::fadd_fast(x, y) }; - let z2 = x + y; -} \ No newline at end of file diff --git a/tests/kani/Intrinsics/FastMath/add.rs b/tests/kani/Intrinsics/FastMath/add.rs new file mode 100644 index 000000000000..e42afc3b7097 --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/add.rs @@ -0,0 +1,19 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fadd_fast` overflow checks pass with suitable assumptions + +#![feature(core_intrinsics)] + +fn main() { + let x: f64 = kani::any(); + let y: f64 = kani::any(); + + kani::assume(x.is_finite()); + kani::assume(y.is_finite()); + match (x.is_sign_positive(), y.is_sign_positive()) { + (true, true) => kani::assume(x < f64::MAX - y), + (false, false) => kani::assume(x > f64::MIN - y), + _ => (), + } + let _z = unsafe { std::intrinsics::fadd_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/add_overflow.rs b/tests/kani/Intrinsics/FastMath/add_overflow.rs new file mode 100644 index 000000000000..3c66ab537fa1 --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/add_overflow.rs @@ -0,0 +1,12 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fadd_fast` triggers overflow checks +// kani-verify-fail + +#![feature(core_intrinsics)] + +fn main() { + let x: f64 = kani::any(); + let y: f64 = kani::any(); + let _z = unsafe { std::intrinsics::fadd_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/div.rs b/tests/kani/Intrinsics/FastMath/div.rs new file mode 100644 index 000000000000..560a24fda991 --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/div.rs @@ -0,0 +1,32 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fdiv_fast` overflow checks pass with suitable assumptions + +#![feature(core_intrinsics)] + +// Unconstrained floating point values will cause performance issues in this +// operation. To avoid them, we assume values within a moderate range. +const MIN_FP_VALUE: f64 = 0.1; +const MAX_FP_VALUE: f64 = 100.0; + +fn assume_fp_range(val: f64) { + if val.is_sign_positive() { + kani::assume(val > MIN_FP_VALUE); + kani::assume(val < MAX_FP_VALUE); + } else { + kani::assume(val < -MIN_FP_VALUE); + kani::assume(val > -MAX_FP_VALUE); + } +} + +fn main() { + let x: f64 = kani::any(); + let y: f64 = kani::any(); + + kani::assume(x.is_finite()); + kani::assume(y.is_finite()); + assume_fp_range(x); + assume_fp_range(y); + + let _z = unsafe { std::intrinsics::fdiv_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/div_overflow.rs b/tests/kani/Intrinsics/FastMath/div_overflow.rs new file mode 100644 index 000000000000..a999f2140281 --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/div_overflow.rs @@ -0,0 +1,12 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fdiv_fast` triggers overflow checks +// kani-verify-fail + +#![feature(core_intrinsics)] + +fn main() { + let x: f64 = kani::any(); + let y: f64 = kani::any(); + let _z = unsafe { std::intrinsics::fdiv_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/mul.rs b/tests/kani/Intrinsics/FastMath/mul.rs new file mode 100644 index 000000000000..b9ee3acea464 --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/mul.rs @@ -0,0 +1,29 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fmul_fast` overflow checks pass with suitable assumptions + +#![feature(core_intrinsics)] + +// Unconstrained floating point values will cause performance issues in this +// operation. To avoid them, we assume values within a moderate range. +const MAX_FP_VALUE: f64 = 100.0; + +fn assume_fp_range(val: f64) { + if val.is_sign_positive() { + kani::assume(val < MAX_FP_VALUE); + } else { + kani::assume(val > -MAX_FP_VALUE); + } +} + +fn main() { + let x: f64 = kani::any(); + let y: f64 = kani::any(); + + kani::assume(x.is_finite()); + kani::assume(y.is_finite()); + assume_fp_range(x); + assume_fp_range(y); + + let _z = unsafe { std::intrinsics::fmul_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/mul_overflow.rs b/tests/kani/Intrinsics/FastMath/mul_overflow.rs new file mode 100644 index 000000000000..1cb7417dedb6 --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/mul_overflow.rs @@ -0,0 +1,12 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fmul_fast` triggers overflow checks +// kani-verify-fail + +#![feature(core_intrinsics)] + +fn main() { + let x: f64 = kani::any(); + let y: f64 = kani::any(); + let _z = unsafe { std::intrinsics::fmul_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/rem.rs b/tests/kani/Intrinsics/FastMath/rem.rs new file mode 100644 index 000000000000..a88ef013c209 --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/rem.rs @@ -0,0 +1,32 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `frem_fast` overflow checks pass with suitable assumptions + +#![feature(core_intrinsics)] + +// Unconstrained floating point values will cause performance issues in this +// operation. To avoid them, we assume values within a moderate range. +const MIN_FP_VALUE: f64 = 0.1; +const MAX_FP_VALUE: f64 = 100.0; + +fn assume_fp_range(val: f64) { + if val.is_sign_positive() { + kani::assume(val > MIN_FP_VALUE); + kani::assume(val < MAX_FP_VALUE); + } else { + kani::assume(val < -MIN_FP_VALUE); + kani::assume(val > -MAX_FP_VALUE); + } +} + +fn main() { + let x: f64 = kani::any(); + let y: f64 = kani::any(); + + kani::assume(x.is_finite()); + kani::assume(y.is_finite()); + assume_fp_range(x); + assume_fp_range(y); + + let _z = unsafe { std::intrinsics::frem_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/rem_overflow.rs b/tests/kani/Intrinsics/FastMath/rem_overflow.rs new file mode 100644 index 000000000000..d1ef37f33ebc --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/rem_overflow.rs @@ -0,0 +1,12 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `frem_fast` triggers overflow checks +// kani-verify-fail + +#![feature(core_intrinsics)] + +fn main() { + let x: f64 = kani::any(); + let y: f64 = kani::any(); + let _z = unsafe { std::intrinsics::frem_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/sub.rs b/tests/kani/Intrinsics/FastMath/sub.rs new file mode 100644 index 000000000000..49c4841e1371 --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/sub.rs @@ -0,0 +1,19 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fsub_fast` overflow checks pass with suitable assumptions + +#![feature(core_intrinsics)] + +fn main() { + let x: f64 = kani::any(); + let y: f64 = kani::any(); + + kani::assume(x.is_finite()); + kani::assume(y.is_finite()); + match (x.is_sign_positive(), y.is_sign_positive()) { + (true, false) => kani::assume(x < f64::MAX + y), + (false, true) => kani::assume(x > f64::MIN + y), + _ => (), + } + let _z = unsafe { std::intrinsics::fsub_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/sub_overflow.rs b/tests/kani/Intrinsics/FastMath/sub_overflow.rs new file mode 100644 index 000000000000..a2f8157bc7e6 --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/sub_overflow.rs @@ -0,0 +1,12 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fsub_fast` triggers overflow checks +// kani-verify-fail + +#![feature(core_intrinsics)] + +fn main() { + let x: f64 = kani::any(); + let y: f64 = kani::any(); + let _z = unsafe { std::intrinsics::fsub_fast(x, y) }; +} From c532dfc0050af52261b303ce99187c1fea496ea1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 8 Feb 2022 22:08:27 +0000 Subject: [PATCH 6/8] Add tests for 32-bit values and compare results --- tests/kani/Intrinsics/FastMath/add_f32.rs | 21 ++++++++++++ .../FastMath/{add.rs => add_f64.rs} | 0 .../{rem_overflow.rs => add_overflow_f32.rs} | 8 ++--- .../{add_overflow.rs => add_overflow_f64.rs} | 0 .../FastMath/{rem.rs => div_f32.rs} | 18 ++++++---- .../FastMath/{div.rs => div_f64.rs} | 0 .../Intrinsics/FastMath/div_overflow_f32.rs | 12 +++++++ .../{div_overflow.rs => div_overflow_f64.rs} | 0 tests/kani/Intrinsics/FastMath/mul_f32.rs | 33 +++++++++++++++++++ .../FastMath/{mul.rs => mul_f64.rs} | 0 .../Intrinsics/FastMath/mul_overflow_f32.rs | 12 +++++++ .../{mul_overflow.rs => mul_overflow_f64.rs} | 0 tests/kani/Intrinsics/FastMath/sub_f32.rs | 21 ++++++++++++ .../FastMath/{sub.rs => sub_f64.rs} | 0 .../Intrinsics/FastMath/sub_overflow_f32.rs | 12 +++++++ .../{sub_overflow.rs => sub_overflow_f64.rs} | 0 16 files changed, 126 insertions(+), 11 deletions(-) create mode 100644 tests/kani/Intrinsics/FastMath/add_f32.rs rename tests/kani/Intrinsics/FastMath/{add.rs => add_f64.rs} (100%) rename tests/kani/Intrinsics/FastMath/{rem_overflow.rs => add_overflow_f32.rs} (51%) rename tests/kani/Intrinsics/FastMath/{add_overflow.rs => add_overflow_f64.rs} (100%) rename tests/kani/Intrinsics/FastMath/{rem.rs => div_f32.rs} (59%) rename tests/kani/Intrinsics/FastMath/{div.rs => div_f64.rs} (100%) create mode 100644 tests/kani/Intrinsics/FastMath/div_overflow_f32.rs rename tests/kani/Intrinsics/FastMath/{div_overflow.rs => div_overflow_f64.rs} (100%) create mode 100644 tests/kani/Intrinsics/FastMath/mul_f32.rs rename tests/kani/Intrinsics/FastMath/{mul.rs => mul_f64.rs} (100%) create mode 100644 tests/kani/Intrinsics/FastMath/mul_overflow_f32.rs rename tests/kani/Intrinsics/FastMath/{mul_overflow.rs => mul_overflow_f64.rs} (100%) create mode 100644 tests/kani/Intrinsics/FastMath/sub_f32.rs rename tests/kani/Intrinsics/FastMath/{sub.rs => sub_f64.rs} (100%) create mode 100644 tests/kani/Intrinsics/FastMath/sub_overflow_f32.rs rename tests/kani/Intrinsics/FastMath/{sub_overflow.rs => sub_overflow_f64.rs} (100%) diff --git a/tests/kani/Intrinsics/FastMath/add_f32.rs b/tests/kani/Intrinsics/FastMath/add_f32.rs new file mode 100644 index 000000000000..daa972bd54f9 --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/add_f32.rs @@ -0,0 +1,21 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fadd_fast` overflow checks pass with suitable assumptions + +#![feature(core_intrinsics)] + +fn main() { + let x: f32 = kani::any(); + let y: f32 = kani::any(); + + kani::assume(x.is_finite()); + kani::assume(y.is_finite()); + match (x.is_sign_positive(), y.is_sign_positive()) { + (true, true) => kani::assume(x < f32::MAX - y), + (false, false) => kani::assume(x > f32::MIN - y), + _ => (), + } + let z = unsafe { std::intrinsics::fadd_fast(x, y) }; + let w = x + y; + assert!(z == w); +} diff --git a/tests/kani/Intrinsics/FastMath/add.rs b/tests/kani/Intrinsics/FastMath/add_f64.rs similarity index 100% rename from tests/kani/Intrinsics/FastMath/add.rs rename to tests/kani/Intrinsics/FastMath/add_f64.rs diff --git a/tests/kani/Intrinsics/FastMath/rem_overflow.rs b/tests/kani/Intrinsics/FastMath/add_overflow_f32.rs similarity index 51% rename from tests/kani/Intrinsics/FastMath/rem_overflow.rs rename to tests/kani/Intrinsics/FastMath/add_overflow_f32.rs index d1ef37f33ebc..3d7de403bba9 100644 --- a/tests/kani/Intrinsics/FastMath/rem_overflow.rs +++ b/tests/kani/Intrinsics/FastMath/add_overflow_f32.rs @@ -1,12 +1,12 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `frem_fast` triggers overflow checks +// Check that `fadd_fast` triggers overflow checks // kani-verify-fail #![feature(core_intrinsics)] fn main() { - let x: f64 = kani::any(); - let y: f64 = kani::any(); - let _z = unsafe { std::intrinsics::frem_fast(x, y) }; + let x: f32 = kani::any(); + let y: f32 = kani::any(); + let _z = unsafe { std::intrinsics::fadd_fast(x, y) }; } diff --git a/tests/kani/Intrinsics/FastMath/add_overflow.rs b/tests/kani/Intrinsics/FastMath/add_overflow_f64.rs similarity index 100% rename from tests/kani/Intrinsics/FastMath/add_overflow.rs rename to tests/kani/Intrinsics/FastMath/add_overflow_f64.rs diff --git a/tests/kani/Intrinsics/FastMath/rem.rs b/tests/kani/Intrinsics/FastMath/div_f32.rs similarity index 59% rename from tests/kani/Intrinsics/FastMath/rem.rs rename to tests/kani/Intrinsics/FastMath/div_f32.rs index a88ef013c209..18e898089afd 100644 --- a/tests/kani/Intrinsics/FastMath/rem.rs +++ b/tests/kani/Intrinsics/FastMath/div_f32.rs @@ -1,15 +1,15 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that `frem_fast` overflow checks pass with suitable assumptions +// Check that `fdiv_fast` overflow checks pass with suitable assumptions #![feature(core_intrinsics)] // Unconstrained floating point values will cause performance issues in this // operation. To avoid them, we assume values within a moderate range. -const MIN_FP_VALUE: f64 = 0.1; -const MAX_FP_VALUE: f64 = 100.0; +const MIN_FP_VALUE: f32 = 0.1; +const MAX_FP_VALUE: f32 = 100.0; -fn assume_fp_range(val: f64) { +fn assume_fp_range(val: f32) { if val.is_sign_positive() { kani::assume(val > MIN_FP_VALUE); kani::assume(val < MAX_FP_VALUE); @@ -20,13 +20,17 @@ fn assume_fp_range(val: f64) { } fn main() { - let x: f64 = kani::any(); - let y: f64 = kani::any(); + let x: f32 = kani::any(); + let y: f32 = kani::any(); kani::assume(x.is_finite()); kani::assume(y.is_finite()); assume_fp_range(x); assume_fp_range(y); - let _z = unsafe { std::intrinsics::frem_fast(x, y) }; + // Comparing `z` and `w` below causes serious performance issues + // https://github.com/model-checking/kani/issues/809 + let z = unsafe { std::intrinsics::fdiv_fast(x, y) }; + // let w = x / y; + // assert!(z == w); } diff --git a/tests/kani/Intrinsics/FastMath/div.rs b/tests/kani/Intrinsics/FastMath/div_f64.rs similarity index 100% rename from tests/kani/Intrinsics/FastMath/div.rs rename to tests/kani/Intrinsics/FastMath/div_f64.rs diff --git a/tests/kani/Intrinsics/FastMath/div_overflow_f32.rs b/tests/kani/Intrinsics/FastMath/div_overflow_f32.rs new file mode 100644 index 000000000000..9024e428093f --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/div_overflow_f32.rs @@ -0,0 +1,12 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fdiv_fast` triggers overflow checks +// kani-verify-fail + +#![feature(core_intrinsics)] + +fn main() { + let x: f32 = kani::any(); + let y: f32 = kani::any(); + let _z = unsafe { std::intrinsics::fdiv_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/div_overflow.rs b/tests/kani/Intrinsics/FastMath/div_overflow_f64.rs similarity index 100% rename from tests/kani/Intrinsics/FastMath/div_overflow.rs rename to tests/kani/Intrinsics/FastMath/div_overflow_f64.rs diff --git a/tests/kani/Intrinsics/FastMath/mul_f32.rs b/tests/kani/Intrinsics/FastMath/mul_f32.rs new file mode 100644 index 000000000000..9fee282ba7fa --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/mul_f32.rs @@ -0,0 +1,33 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fmul_fast` overflow checks pass with suitable assumptions + +#![feature(core_intrinsics)] + +// Unconstrained floating point values will cause performance issues in this +// operation. To avoid them, we assume values within a moderate range. +const MAX_FP_VALUE: f32 = 100.0; + +fn assume_fp_range(val: f32) { + if val.is_sign_positive() { + kani::assume(val < MAX_FP_VALUE); + } else { + kani::assume(val > -MAX_FP_VALUE); + } +} + +fn main() { + let x: f32 = kani::any(); + let y: f32 = kani::any(); + + kani::assume(x.is_finite()); + kani::assume(y.is_finite()); + assume_fp_range(x); + assume_fp_range(y); + + // Comparing `z` and `w` below causes serious performance issues + // https://github.com/model-checking/kani/issues/809 + let z = unsafe { std::intrinsics::fmul_fast(x, y) }; + // let w = x * y; + // assert!(z == w); +} diff --git a/tests/kani/Intrinsics/FastMath/mul.rs b/tests/kani/Intrinsics/FastMath/mul_f64.rs similarity index 100% rename from tests/kani/Intrinsics/FastMath/mul.rs rename to tests/kani/Intrinsics/FastMath/mul_f64.rs diff --git a/tests/kani/Intrinsics/FastMath/mul_overflow_f32.rs b/tests/kani/Intrinsics/FastMath/mul_overflow_f32.rs new file mode 100644 index 000000000000..92eb775b939f --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/mul_overflow_f32.rs @@ -0,0 +1,12 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fmul_fast` triggers overflow checks +// kani-verify-fail + +#![feature(core_intrinsics)] + +fn main() { + let x: f32 = kani::any(); + let y: f32 = kani::any(); + let _z = unsafe { std::intrinsics::fmul_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/mul_overflow.rs b/tests/kani/Intrinsics/FastMath/mul_overflow_f64.rs similarity index 100% rename from tests/kani/Intrinsics/FastMath/mul_overflow.rs rename to tests/kani/Intrinsics/FastMath/mul_overflow_f64.rs diff --git a/tests/kani/Intrinsics/FastMath/sub_f32.rs b/tests/kani/Intrinsics/FastMath/sub_f32.rs new file mode 100644 index 000000000000..0c5390edbc79 --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/sub_f32.rs @@ -0,0 +1,21 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fsub_fast` overflow checks pass with suitable assumptions + +#![feature(core_intrinsics)] + +fn main() { + let x: f32 = kani::any(); + let y: f32 = kani::any(); + + kani::assume(x.is_finite()); + kani::assume(y.is_finite()); + match (x.is_sign_positive(), y.is_sign_positive()) { + (true, false) => kani::assume(x < f32::MAX + y), + (false, true) => kani::assume(x > f32::MIN + y), + _ => (), + } + let z = unsafe { std::intrinsics::fsub_fast(x, y) }; + let w = x - y; + assert!(z == w); +} diff --git a/tests/kani/Intrinsics/FastMath/sub.rs b/tests/kani/Intrinsics/FastMath/sub_f64.rs similarity index 100% rename from tests/kani/Intrinsics/FastMath/sub.rs rename to tests/kani/Intrinsics/FastMath/sub_f64.rs diff --git a/tests/kani/Intrinsics/FastMath/sub_overflow_f32.rs b/tests/kani/Intrinsics/FastMath/sub_overflow_f32.rs new file mode 100644 index 000000000000..8291eae6fcdd --- /dev/null +++ b/tests/kani/Intrinsics/FastMath/sub_overflow_f32.rs @@ -0,0 +1,12 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Check that `fsub_fast` triggers overflow checks +// kani-verify-fail + +#![feature(core_intrinsics)] + +fn main() { + let x: f32 = kani::any(); + let y: f32 = kani::any(); + let _z = unsafe { std::intrinsics::fsub_fast(x, y) }; +} diff --git a/tests/kani/Intrinsics/FastMath/sub_overflow.rs b/tests/kani/Intrinsics/FastMath/sub_overflow_f64.rs similarity index 100% rename from tests/kani/Intrinsics/FastMath/sub_overflow.rs rename to tests/kani/Intrinsics/FastMath/sub_overflow_f64.rs From b074099cdd222c7a4fbaafd9803d4586c75acbb5 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 8 Feb 2022 22:11:59 +0000 Subject: [PATCH 7/8] Drop support for `frem_fast` --- .../rustc_codegen_kani/src/codegen/intrinsic.rs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs b/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs index add7ed3b6764..b7eb043fd29c 100644 --- a/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs +++ b/src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs @@ -411,11 +411,6 @@ impl<'tcx> GotocCtx<'tcx> { self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) } "forget" => Stmt::skip(loc), - "frem_fast" => { - let fargs_clone = fargs.clone(); - let binop_stmt = codegen_intrinsic_binop!(rem); - self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span) - } "fsub_fast" => { let fargs_clone = fargs.clone(); let binop_stmt = codegen_intrinsic_binop!(sub); From e76b8d4830d17f0cf057c79d44ab2d01193ecc17 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 8 Feb 2022 22:12:18 +0000 Subject: [PATCH 8/8] Add comment to `get_stmts` --- src/kani-compiler/cbmc/src/goto_program/stmt.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/kani-compiler/cbmc/src/goto_program/stmt.rs b/src/kani-compiler/cbmc/src/goto_program/stmt.rs index 731e5a029a76..62e7bdba20fc 100644 --- a/src/kani-compiler/cbmc/src/goto_program/stmt.rs +++ b/src/kani-compiler/cbmc/src/goto_program/stmt.rs @@ -130,6 +130,7 @@ impl Stmt { } } + // If self has a body of type `Block(stmts)`, return `stmts`; otherwise, None pub fn get_stmts(&self) -> Option<&Vec> { match self.body() { Block(stmts) => Some(stmts),