Add integer overflow checking for simd_div and simd_rem

[reisnera]

Description of changes:

As described in #1970, the simd_div and simd_rem intrinsics lack overflow checking. This PR implements them. It also makes a minor (somewhat) related change of moving the check to before the expression in the returned Stmt of codegen_simd_op_with_overflow.

Resolved issues:

Resolves #1970

Related RFC:

n/a

Call-outs:

Testing:

• How is this change tested?
  Added new test to ensure that attempted overflow div or rem fails the check.

• Is this a refactor change?
  No

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix
  (Except for the minor change in codegen_simd_op_with_overflow)

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[celinval]

Thanks for doing this! Can you please add a test for float vector too? I'm worried that this could trigger similar failure to #2631.

[reisnera]

While writing a test to confirm that everything works as expected with float vectors, I found I can assert that simd_div and normal division produce the same results. However when I tried the same with % and simd_rem, I ran into an issue with test failures in kani that I wasn't able to reproduce with specific inputs after using --visualize. This was true on main as well. I think maybe I'm running into the same type of issue as #2049 and #1342 but I'm definitely not sure. Here's the test I tried:

Details

#![feature(repr_simd, platform_intrinsics)]

#[repr(simd)]
#[allow(non_camel_case_types)]
#[derive(Clone, Copy, PartialEq)]
pub struct f32x2(f32, f32);

extern "platform-intrinsic" {
    fn simd_rem<T>(x: T, y: T) -> T;
}

#[kani::proof]
fn test_simd_rem() {
    let dividend: f32 = kani::any::<i8>().into();
    let divisor: f32 = kani::any::<i8>().into();
    kani::assume(divisor != 0.0 && divisor.abs() < 5.0);
    let normal_result = dividend % divisor;
    let dividends = f32x2(dividend, dividend);
    let divisors = f32x2(divisor, divisor);
    let simd_result = unsafe { simd_rem(dividends, divisors) };
    assert_eq!(normal_result, simd_result.0);
}

This produces:

RESULTS:
Check 1: test_simd_rem.assertion.1
         - Status: FAILURE
         - Description: "assertion failed: normal_result == simd_result.0"
         - Location: ../tmp/test.rs:36:5 in function test_simd_rem

Check 2: test_simd_rem.division-by-zero.1
         - Status: SUCCESS
         - Description: "division by zero"
         - Location: ../tmp/test.rs:32:25 in function test_simd_rem

Check 3: division-by-zero.1
         - Status: SUCCESS
         - Description: "division by zero"

Check 4: division-by-zero.2
         - Status: SUCCESS
         - Description: "division by zero"

Also, as I started talking about here, I'm a bit lost with simd_rem. CBMC seems to only check if the divisor is 0 for simd_rem, but I'm not even sure now what should be checked for. Check to make sure a new NaN is not produced? Check for IEEE 754 overflow/underflow/invalid exceptions?

Regardless, this PR should still be useful even if nothing else was changed about the handling for simd_rem as it would fix the integer overflow issue and leave simd_rem untouched.

[celinval]

Hi @reisnera, is this ready for review?

[reisnera]

Hi @celinval, yes I believe so. I made a comment regarding simd_rem not checking for overflows. Did you see my comment above?

[adpaco-aws]

Hi @reisnera , thanks for your work on these intrinsics!

When checking if two floating point numbers are the same, we often allow a small amount (usually called "epsilon") to account for precision errors. For example, we use this fp_equals function in some of our tests (instead of ==):

fn fp_equals(value: f32, expected: f32) -> bool {
    let abs_diff = (value - expected).abs();
    abs_diff <= f32::EPSILON
}

Can you try that for the floating point tests? I can point you to specific tests that make use of it if you can't find them. You may also need to add assumptions that use the is_finite() or is_nan() methods.

Regarding the missing checks, we could ask CBMC if they're interested in adding them first. That way, both tools could benefit from the check. What do you think?

[reisnera]

Hi @adpaco-aws, thanks! I've enjoyed working on these!

For fp_equal, are you referring to using this in the division_float.rs test file to try to fix the issue I'm having with simd_rem? Or just in general?

I can see where some tests use the fp_equals function and I'm aware of the difficulties with equality comparison of floats, but in the case of the division_float.rs test file, don't we want to test that the results of normal division and SIMD division are bit-equal? (Unless the simd_rem issue is indeed a similar type of issue as with the trigonometric functions).

Regarding the missing checks, we could ask CBMC if they're interested in adding them first. That way, both tools could benefit from the check. What do you think?

I agree that this would be great if they could!

[adpaco-aws]

You're right in that we should directly be checking equality in this case. It just occurred to me that maybe both results end up being f32::NAN, and they're failing the assertion because comparisons with f32::NAN in Rust are always false.

Can you please check if that's the case? With something like this:

if (normal_result.is_nan()) {
    assert!(simd_result.0.is_nan());
} else {
    assert_eq!(normal_result, simd_result.0);
}

[reisnera]

@adpaco-aws So I tried your suggestion, and no luck. However this prompted me to investigate further and interestingly the problem might just be with %. I filed a separate issues with a non-SIMD example here: #2669

[adpaco-aws]

The issue you found means that you'll get nondeterministic values as a result of the mod operation, which makes clear why the comparison fails later.

But I don't that should be blocking this PR: we can put the cases which are currently failing into a fixme test and merge them once #2669 is resolved. What do you think @celinval ?

[celinval]

The issue you found means that you'll get nondeterministic values as a result of the mod operation, which makes clear why the comparison fails later.

But I don't that should be blocking this PR: we can put the cases which are currently failing into a fixme test and merge them once #2669 is resolved. What do you think @celinval ?

As I mentioned in #2669, I believe this is a Kani bug (hence the "ignored warning"). We might need to model floating point remainder operation on our side.

I do agree that this shouldn't block this PR, since the issue is consistent for SIMD and non-SIMD (i.e.: this PR is not introducing any bad behavior). @reisnera can you please add a fixme test to our suite either as part of this PR or a separate PR that reproduces the issue you created and also add a similar harness to the one you added to the division that checks that simd produces the same value as the non-simd one.

[reisnera]

@celinval and @adpaco-aws, I responded to the review above but FYI I'll also need some time to finish this up as I'll be working my usual job through the weekend into next week :)

[celinval]

Thank you!

[adpaco-aws]

Thanks, @reisnera ! With this contribution and #1963, I think we can update the documentation for platform intrinsic support. Would you mind doing that?

[reisnera]

@adpaco-aws Absolutely! I'm actually not sure if I should leave something in the notes column for simd_rem. I'm still trying to wrap my head around if #2669 affects simd_rem. I think it does?

[adpaco-aws]

@adpaco-aws Absolutely! I'm actually not sure if I should leave something in the notes column for simd_rem. I'm still trying to wrap my head around if #2669 affects simd_rem. I think it does?

Hey @reisnera , sorry for not getting back to you earlier.

If I'm not mistaken, we still need to open an issue in the CBMC repo to ask about the missing checks. We can note there's missing support for the operation with floating-point operand, and also the missing checks that should be coming from CBMC.

[reisnera]

@adpaco-aws I updated the docs. According to the comment here, it seems this is already doable on CBMC end unless I'm missing something. I'll work on a pull request for that issue separately.

[adpaco-aws]

Thanks @reisnera !