Unimplemented intrinsic: frem_fast #810
Description
In #804 I made an attempt to implement frem_fast (floating-point remainder) as %, but the test I wrote was failing even though the same expression is being used to codegen both:
#![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);
let z = unsafe { std::intrinsics::frem_fast(x, y) };
let w = x % y;
assert!(z == w);
}
Then I reflected on what this operation means in the case of floating point numbers and realized it needed more work. It is not clear to me what is the irep we should using to encode this operation, so we should find out and use that.