Incorrect results of floating-point operations

[lukfried]

When Comparing two f64::NAN values, some results are wrong. In particular:

assert!(f64::NAN == f64::NAN)

verifies, even though the specifications define the expression to be false. With f32::NAN things behave correctly. But there is no relevant difference in the viper code generated in the two cases.

Here you find individual tests for Eq, Geq, Leq where the error occurs. A comprehensive test including all cases can be found here.

Below is a table of how things evaluate currently with (!!!) noting the cases where it deviates from the specifications.

cmp	f32::NAN	f64::NAN
==	F	T (!!!)
!=	T	F (!!!)
>=	F	T (!!!)
>	F	F
<=	F	T (!!!)
<	F	F

[Patrick-6]

Here is a summary of the current state of floating point support by Prusti:

use prusti_contracts::*;

fn test_0() {
    prusti_assert!(f64::NAN == f64::NAN); // Passes, but shouldn't
    prusti_assert!(f64::NAN === f64::NAN); // [Prusti: unsupported feature] unsupported constant type Ref(ReErased, f64, Not)
}

fn test_1() {
    let x: f64 = 0.1;
    let y = 0.2;
    let z = x + y;
    assert!(z == y + x); // works
    prusti_assert!(z == y + x); // works
    // prusti_assert!(z == y + x + 10.0); // Correctly fails
    prusti_assert!(z === x + y); // Should verify, but doesn't
    prusti_assert!(z === y + x); // Should verify, but doesn't
}

/*
[Prusti internal error] Prusti encountered an unexpected internal error
  floating_point_values.rs(27, 1):
    We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  floating_point_values.rs(27, 1):
    Details: cannot generate fold-unfold Viper statements.
    The required permission Acc(_3.val_float64, read) cannot be obtained.
*/
fn test_2() {
    let x: f64 = 0.1;
    prusti_assert!(x + x === x + x);
}

// [Prusti: unsupported feature] unsupported constant type Ref(ReErased, f64, Not)
fn test_3() {
    let x: f64 = 0.1;
    let y = 0.2;
    prusti_assert!(x - y === 0.1 - 0.2);
}

// All these functions are missing their external specifications
#[requires(x.is_finite())]
fn missing_extern_spec(x: f64) {
    prusti_assert!(!x.is_infinite());
    prusti_assert!(!x.is_nan());
    prusti_assert!(x.is_normal() != x.is_subnormal());
}

fn test_working() {
    let x: f64 = 0.1;
    let y = 0.2;
    let z = x - y;
    prusti_assert!(x - y === z);
}