Incorrect floating point result with remainder (%) operator

[reisnera]

I tried this code:

#[kani::proof]
fn test_rem() {
    let dividend: f32 = kani::any::<i8>().into();
    let divisor: f32 = kani::any::<i8>().into();
    kani::assume(divisor != 0.0);
    let result = dividend % divisor;
    assert!(result == 0.0 || result.is_normal());
}

using the following command line invocation:

kani <file>

with Kani version: 0.33

I expected to see this happen: proof should succeed

Instead, this happened: proof failed with the following output:

click to expand

Kani Rust Verifier 0.33.0 (standalone)
Checking harness test_rem...
CBMC 5.88.0 (cbmc-5.88.0)
CBMC version 5.88.0 (cbmc-5.88.0) 64-bit x86_64 linux
Reading GOTO program from file /home/alex/rust-projects/tmp/test__RNvCsd4v5NBjnlwJ_4test8test_rem.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.0122388s
size of program expression: 599 steps
slicing removed 328 assignments
Generated 3 VCC(s), 3 remaining after simplification
Runtime Postprocess Equation: 0.0002305s
Passing problem to propositional reduction
converting SSA
warning: ignoring mod
  * type: floatbv
      * width: 32
      * f: 23
      * #c_type: float
  0: symbol
      * type: floatbv
          * width: 32
          * f: 23
          * #c_type: float
      * identifier: _RNvCsd4v5NBjnlwJ_4test8test_rem::1::var_9!0@1#2
      * expression: symbol
          * type: floatbv
              * width: 32
              * f: 23
              * #c_type: float
          * identifier: _RNvCsd4v5NBjnlwJ_4test8test_rem::1::var_9
      * #SSA_symbol: 1
      * L0: 0
      * L1: 1
      * L2: 2
      * L1_object_identifier: _RNvCsd4v5NBjnlwJ_4test8test_rem::1::var_9!0@1
  1: symbol
      * type: floatbv
          * width: 32
          * f: 23
          * #c_type: float
      * identifier: _RNvCsd4v5NBjnlwJ_4test8test_rem::1::var_10!0@1#2
      * expression: symbol
          * type: floatbv
              * width: 32
              * f: 23
              * #c_type: float
          * identifier: _RNvCsd4v5NBjnlwJ_4test8test_rem::1::var_10
      * #SSA_symbol: 1
      * L0: 0
      * L1: 1
      * L2: 2
      * L1_object_identifier: _RNvCsd4v5NBjnlwJ_4test8test_rem::1::var_10!0@1
Runtime Convert SSA: 0.0018622s
Running propositional reduction
Post-processing
Runtime Post-process: 6.3e-06s
Solving with MiniSAT 2.2.1 with simplifier
881 variables, 2964 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0038988s
Runtime decision procedure: 0.0058917s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
881 variables, 376 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 1.41e-05s
Runtime decision procedure: 4.9e-05s

RESULTS:
Check 1: test_rem.assertion.1
         - Status: FAILURE
         - Description: "assertion failed: result == 0.0 || result.is_normal()"
         - Location: ../tmp/test.rs:40:5 in function test_rem

Check 2: test_rem.division-by-zero.1
         - Status: SUCCESS
         - Description: "division by zero"
         - Location: ../tmp/test.rs:39:18 in function test_rem


SUMMARY:
 ** 1 of 2 failed
Failed Checks: assertion failed: result == 0.0 || result.is_normal()
 File: "/home/alex/rust-projects/tmp/test.rs", line 40, in test_rem

VERIFICATION:- FAILED
Verification Time: 0.049368992s

Summary:
Verification failed for - test_rem
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

Also as a sanity check, I brute forced a quick double check of this on the Rust Playground here to prove to myself that this Kani result was unexpected.

[adpaco-aws]

Thanks for the issue, @reisnera !

It looks like the mod operation isn't available for floating point operations. Looking around CBMC's source code I could find these CPROVER builtins which take floating-point arguments. Most likely, we should be emitting those instead of the regular mod when the arguments are floating point. Another alternative is for CBMC to automatically transform mod operations into the CPROVER builtins.

@tautschnig can you provide some guidance here?

[celinval]

I believe CBMC doesn't support this because C/C++ also restricts mod operations to integer. If you try to compile following C program:

#include<assert.h>

int main() {
    float x = 2.0;
    float y = 1.0;
    float mod = x % y;
    assert(mod == 0.0);
}

using gcc, you get the following error

mod.c: In function ‘main’:
mod.c:6:19: error: invalid operands to binary % (have ‘float’ and ‘float’)
    6 |     float mod = x % y;
      |                   ^

[tautschnig]

Kani just needs to create an floatbv_mod expression instead of a mod expression when the operands are of floating-point type.

[reisnera]

@adpaco-aws @celinval , I can work on this if you like! Do you want the rem method of Expr to deal with both integers and floats, or do you want me to make another method (e.g. float_rem) and make it the responsibility of the caller to choose the right one?

[celinval]

Hi @reisnera, both seem reasonable. I would probably add a rem to expression, unless there's a float_div operation.

[reisnera]

So I finally got a chance to actually work on this, sorry about the delay @adpaco-aws and @celinval.

It was straightforward to use floatbv_mod for floating point operands as suggested by @tautschnig, and while the original test above now passes, the following harness does not:

#[kani::proof]
fn rem_float_correct() {
    let a: u8 = kani::any();
    let b: u8 = kani::any_where(|&n: &u8| n != 0);
    let a_float: f32 = a.into();
    let b_float: f32 = b.into();
    assert_eq!(a % b, (a_float % b_float) as u8);
}

I verified that this doesn't panic in the playground.

I also tried using floatbv_rem based on the CBMC comments here and here, as they seem to suggest that floatbv_rem might be more appropriate, however I got the same results.

It does work now in the sense that I can assert that floating point % by 0 produces a NaN, for example, though I note that the harness doesn't fail in this case without an explicit assertion (unlike e.g. floating point division). I believe I could insert checks for production of a new NaN value for floating point remainder (I think...).

Questions:

1. Should the above harness pass? If so, this would require a fix in CBMC, no?
2. Which is more correct here: floatbv_mod or floatbv_rem?
3. Do you want me to insert checks for production of new NaN values in floating point remainder?

Edit: Instead of checking for a new NaN, I could also just directly check for invalid cases, which I believe is only if the divisor is 0 or the dividend is infinite.

[adpaco-aws]

Hey @reisnera , sorry about our delay in getting back to you and thanks for your work on this.

Here's my answers/questions:

1. Not clear to me. I'd suggest you use concrete playback or --visualize to find out the cases that are failing.
2. I recall us emitting the rem operator for mod expressions, so I'd say the right thing to do is using floatbv_rem (@tautschnig is this OK?)
3. NaN checks come from CBMC in most cases if I'm not mistaken. I'd first focus on debugging this example and then we can talk about how to improve it.

[reisnera]

@adpaco-aws not a problem! Hope I'm helping more than I'm giving you extra work :)

Regarding the remainder operation, kani currently uses mod and it actually looks like there is no plain rem in CBMC (there's no irep ID entry for it, for example). I agree that it was unexpected that NaN checks aren't happening on the CBMC side. I'll try to investigate this failing test more.

[adpaco-aws]

Hope I'm helping more than I'm giving you extra work :)

Of course, we really appreciate your contributions! And I acknowledge that implementing models for Rust is not straightforward in many cases.

[tautschnig]

Looking at CBMC's code base, it certainly seems that we've got a bit of a mess of ID_floatbv_rem vs ID_floatbv_mod. This needs looking into. What isn't clear to me is what the desired semantics on the Rust side are. Should it be IEEE-compatible remainder, or should it be a Rust variant of fmod?

[reisnera]

So concrete playback and --visualize produced two different failing test cases, but neither of them causes the equivalent Rust code to panic, and on inspection neither is notable to me. (e.g. one failing case was a = 70 and b = 40).

@tautschnig According to this issue, floating point % in Rust lowers to LLVM frem which according to LLVM produces "the same output as a libm ‘fmod’ function, but without any possibility of setting errno."

I also came across the following regarding non-deterministic NaN bit patterns in the Rust Docs, which may be relevant?

Lastly, there are multiple bit patterns that are considered NaN. Rust does not currently guarantee that the bit patterns of NaN are preserved over arithmetic operations, and they are not guaranteed to be portable or even fully deterministic! This means that there may be some surprising results upon inspecting the bit patterns, as the same calculations might produce NaNs with different bit patterns.

See this recent pre-RFC by Ralf Jung and this issue.

[adpaco-aws]

So concrete playback and --visualize produced two different failing test cases, but neither of them causes the equivalent Rust code to panic, and on inspection neither is notable to me. (e.g. one failing case was a = 70 and b = 40).

Then CBMC is producing non-equivalent results, which as @tautschnig mentioned needs looking into.

[tautschnig]

diffblue/cbmc#7885 is to eventually fix the issues on the CBMC side. It might also give an idea for tests that we could use in Kani to convince ourselves of the semantics in Rust (fmod vs remainder).

[reisnera]

Great! @tautschnig I struggle to understand the CBMC codebase, so question: will this mean that CBMC floatbv_mod will handle SIMD vectors in the same way that mod currently does for integers?