Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Incorrect floating point result with remainder (%) operator #2669

Open
reisnera opened this issue Aug 9, 2023 · 14 comments
Open

Incorrect floating point result with remainder (%) operator #2669

reisnera opened this issue Aug 9, 2023 · 14 comments
Assignees
Labels
[C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue

Comments

@reisnera
Copy link
Contributor

reisnera commented Aug 9, 2023

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.

@reisnera reisnera added the [C] Bug This is a bug. Something isn't working. label Aug 9, 2023
@adpaco-aws
Copy link
Contributor

adpaco-aws commented Aug 10, 2023

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
Copy link
Contributor

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;
      |                   ^

reisnera added a commit to reisnera/kani that referenced this issue Aug 12, 2023
reisnera added a commit to reisnera/kani that referenced this issue Aug 12, 2023
@tautschnig
Copy link
Member

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

@reisnera
Copy link
Contributor Author

@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
Copy link
Contributor

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

@reisnera
Copy link
Contributor Author

reisnera commented Aug 30, 2023

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
Copy link
Contributor

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
Copy link
Contributor Author

reisnera commented Sep 7, 2023

@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
Copy link
Contributor

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
Copy link
Member

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?

@tautschnig tautschnig self-assigned this Sep 8, 2023
@reisnera
Copy link
Contributor Author

reisnera commented Sep 8, 2023

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
Copy link
Contributor

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
Copy link
Member

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
Copy link
Contributor Author

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?

@celinval celinval added the [F] Soundness Kani failed to detect an issue label Oct 15, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Soundness Kani failed to detect an issue
Projects
None yet
Development

No branches or pull requests

4 participants