Support for fast math intrinsics

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)`
@@ -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)

src/kani-compiler/cbmc/src/goto_program/stmt.rs

@@ -129,6 +129,14 @@ impl Stmt {
             _ => None,
         }
     }
+
+    // If self has a body of type `Block(stmts)`, return `stmts`; otherwise, None
+    pub fn get_stmts(&self) -> Option<&Vec<Stmt>> {
+        match self.body() {
+            Block(stmts) => Some(stmts),
+            _ => None,
+        }
+    }
 }
 
 /// Fluent builders

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(),

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",

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,

src/kani-compiler/rustc_codegen_kani/src/codegen/intrinsic.rs

@@ -391,11 +391,31 @@ 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_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_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),
             "fmaf32" => codegen_simple_intrinsic!(Fmaf),
             "fmaf64" => codegen_simple_intrinsic!(Fma),
+            "fmul_fast" => {
+                let fargs_clone = fargs.clone();
+                let binop_stmt = codegen_intrinsic_binop!(mul);
+                self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span)
+            }
             "forget" => Stmt::skip(loc),
+            "fsub_fast" => {
+                let fargs_clone = fargs.clone();
+                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),
             "log10f64" => codegen_simple_intrinsic!(Log10),
@@ -520,6 +540,28 @@ 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 statement which performs the
+    // operation and checks for overflow failures.
+    fn add_finite_args_checks(
+        &mut self,
+        intrinsic: &str,
+        mut fargs: Vec<Expr>,
+        stmt: Stmt,
+        span: Option<Span>,
+    ) -> 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());
+        Stmt::block(vec![finite_check1, finite_check2, stmt], loc)
+    }
+
     fn codegen_exact_div(&mut self, mut fargs: Vec<Expr>, p: &Place<'tcx>, loc: Location) -> Stmt {
         // Check for undefined behavior conditions defined in
         // https://doc.rust-lang.org/std/intrinsics/fn.exact_div.html

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);
+}

tests/kani/Intrinsics/FastMath/add_f64.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) };
+}

tests/kani/Intrinsics/FastMath/add_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 `fadd_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::fadd_fast(x, y) };
+}

tests/kani/Intrinsics/FastMath/add_overflow_f64.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) };
+}

tests/kani/Intrinsics/FastMath/div_f32.rs

@@ -0,0 +1,36 @@
+// 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: f32 = 0.1;
+const MAX_FP_VALUE: f32 = 100.0;
+
+fn assume_fp_range(val: f32) {
+    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: 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::fdiv_fast(x, y) };
+    // let w = x / y;
+    // assert!(z == w);
+}

tests/kani/Intrinsics/FastMath/div_f64.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) };
+}

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) };
+}

tests/kani/Intrinsics/FastMath/div_overflow_f64.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) };
+}

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);
+}

tests/kani/Intrinsics/FastMath/mul_f64.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) };
+}

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) };
+}