Unimplemented intrinsic: frem_fast

[adpaco-aws]

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.

[tautschnig]

For floating point modulo/remainder operations, please use "floatbv_rem" as the expression id. All other binary arithmetic expressions will be rewritten from their usual operators to floating-point specific ones during GOTO conversion. This is not the case for modulo as that's not even permitted in C over floating point, and also there's no need to add a rounding mode.