[EVA] Unconventional hexadecimal display for 0

[MercierCorentin]

I found an unexpected hexadecimal display while using Frama-C version 20.0 (Calcium). Here's what I found :

result ∈ [0x0.0000000000000p-1022 .. 0x1.0000000000000p4]

As result is a single precision floating-point, it's exponent should be upper or equal than -127. This doesn't prevent from using Frama-C but it might hide another issue.

How to reproduce:

My C file example.c :

#ifdef FRAMA_C
    #include "__fc_builtin.h"
#else
    #include <stdio.h>
#endif

#define FLT_MAX 0xFFFFFEp+127

void add(float x, float y, float *result){
    double xDouble = 0, yDouble = 0, tmp = 0;

    xDouble = (double)x;
    yDouble = (double)y;
    tmp = xDouble + yDouble;

    if ( tmp < (double)-FLT_MAX )
    {
        *result = -FLT_MAX;
    }else if (tmp > (double)FLT_MAX )
    {
        *result = FLT_MAX;
    }else
    {
        *result = (float)tmp;
    }
}

int main( void ){

#ifdef FRAMA_C
    float x = Frama_C_float_interval(0x1.0p2, 0x1.4p4),
#else
    float x = 0x1.0p2,
#endif
    y = -0x1.0p2,
    result = 0;

    add(x, y, &result);

#ifndef FRAMA_C
    printf("Result:\t%a\n", result); 
#endif
}

The small script I launched :

printf "Example compiling\n\n" > log.txt
gcc -o main example.c
printf "\n" >> log.txt

printf "Example execution\n\n" >> log.txt
./main >> log.txt
printf "\n" >> log.txt

printf "EVA ANALYSIS\n\n" >> log.txt
frama-c -cpp-extra-args="-D FRAMA_C" -eva -float-hex example.c >> log.txt

And the result:

Example compiling

Example execution

Result: 0x0p+0

EVA ANALYSIS

[kernel] Parsing example.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva] using specification for function Frama_C_float_interval
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function add2:
  xDouble ∈ [0x1.0000000000000p2 .. 0x1.4000000000000p4]
  yDouble ∈ {-0x1.0000000000000p2}
  tmp ∈ [0x0.0000000000000p-1022 .. 0x1.0000000000000p4]
  result ∈ [0x0.0000000000000p-1022 .. 0x1.0000000000000p4]
[eva:final-states] Values at end of function main:
  Frama_C_entropy_source ∈ [--..--]
  x ∈ [0x1.0000000000000p2 .. 0x1.4000000000000p4]
  y ∈ {-0x1.0000000000000p2}
  result ∈ [0x0.0000000000000p-1022 .. 0x1.0000000000000p4]
  __retres ∈ {0}
[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  2 functions analyzed (out of 2): 100% coverage.
  In these functions, 16 statements reached (out of 18): 88% coverage.
  ----------------------------------------------------------------------------
  No errors or warnings raised during the analysis.
  ----------------------------------------------------------------------------
  0 alarms generated by the analysis.
  ----------------------------------------------------------------------------
  Evaluation of the logical properties reached by the analysis:
    Assertions        0 valid     0 unknown     0 invalid      0 total
    Preconditions     2 valid     0 unknown     0 invalid      2 total
  100% of the logical properties reached have been proven.
  ----------------------------------------------------------------------------

[vprevosto]

Thanks for your report. Actually, since the mantissa is exactly 0, it could be argued that the exponent doesn't matter much 😉. However, displaying the value should indeed be done in a better way.

[maroneze]

Indeed, this is a "known feature" of -float-hex, since at least 2011 and likely older than that.

Although unintuitive at first, the format chosen by -float-hex has some advantages, such as uniformity, which is helpful at times.

Also, you'll notice that both floats and doubles are printed using the same number of hexadecimal places; this is because, internally, Eva uses OCaml floats, which are double-precision floating-point values, even when representing single-precision float intervals (truncation and consistency checks are performed to ensure only the corresponding amount of significant bits are used in single-precision float computations). That explains why the p-1022 is there, even when handling floats.

Anyway, since 0 is a special case, it might make sense to follow the convention that is used by the libc when printing it with the %a modifier (0x0p+0), or e.g. as in Java (0x0.0p0).

[MercierCorentin]

Thanks for both these aswers and explanations! I've changed the issue's title according to new pieces of information you gave me.

[maroneze]

Fixed in commit e04ad237. You can already try it using the public Frama-C master branch; otherwise, the fix will be available in the next Frama-C release.

[MercierCorentin]

By using the same script with an instance of frama-c compiled from the public master branch, I got the following result:

Example compiling

Example execution

Result: 0x0p+0

EVA ANALYSIS

[kernel] Parsing example.c (with preprocessing)
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva] using specification for function Frama_C_float_interval
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function add:
  xDouble ∈ [0x1.0000000000000p2 .. 0x1.4000000000000p4]
  yDouble ∈ {-0x1.0000000000000p2}
  tmp ∈ [0x0.0000000000000p0 .. 0x1.0000000000000p4]
  result ∈ [0x0.0000000000000p0 .. 0x1.0000000000000p4]
[eva:final-states] Values at end of function main:
  Frama_C_entropy_source ∈ [--..--]
  x ∈ [0x1.0000000000000p2 .. 0x1.4000000000000p4]
  y ∈ {-0x1.0000000000000p2}
  result ∈ [0x0.0000000000000p0 .. 0x1.0000000000000p4]
  __retres ∈ {0}
[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  2 functions analyzed (out of 2): 100% coverage.
  In these functions, 16 statements reached (out of 18): 88% coverage.
  ----------------------------------------------------------------------------
  No errors or warnings raised during the analysis.
  ----------------------------------------------------------------------------
  0 alarms generated by the analysis.
  ----------------------------------------------------------------------------
  Evaluation of the logical properties reached by the analysis:
    Assertions        0 valid     0 unknown     0 invalid      0 total
    Preconditions     2 valid     0 unknown     0 invalid      2 total
  100% of the logical properties reached have been proven.
  ----------------------------------------------------------------------------

Thanks for fixing this detail!

[maroneze]

Thanks for confirming it works for you!