Dereferencing a larger bit-width pointer is not caught by property checks (was: CBMC fails to prove trivial inverse square root floating point property)

[esteffin]

I run cbmc on the code attached (part of my graphic library) that should be SAFE.
However cbmc returns assertion Q_rsqrt(f) > 0: FAILURE.

Why?

#include <assert.h>
#include <math.h>

float nondet_float (void);

float Q_rsqrt( float number )
{
	long i;
	float x2, y;
	const float threehalfs = 1.5F;

	x2 = number * 0.5F;
	y  = number;
	i  = * ( long * ) &y;
	i  = 0x5f3759df - ( i >> 1 );
	y  = * ( float * ) &i;
	y  = y * ( threehalfs - ( x2 * y * y ) );

	return y;
}

int main (void) {
	float f = nondet_float();
        // Everything in this range hits the bug
	__CPROVER_assume(f < +INFINITY);
	__CPROVER_assume(f > 0.0f);

        // Should pass ass 1/sqrt(f) is always > 0 when f > 0
        assert(Q_rsqrt(f) > 0);

	return 1;
}

CBMC version: 5.80
Operating system: MacOS
Exact command line resulting in the issue: cbmc main.c
What behaviour did you expect: Verification SUCCESS
What happened instead: Verification FAILURE

[tautschnig]

It seems that byte-extracting from and to float values is not doing the right thing. Run the following with -DDEBUG and compare to CBMC's trace to see the (unexpected) difference:

#include <assert.h>
#include <math.h>
#ifdef DEBUG
#include <stdio.h>
#define debug_printf(format, value) printf(format, value)
#else
#define debug_printf(format, value) (void)0
#endif

float nondet_float (void);

float Q_rsqrt( float number )
{
  long i;
  float x2, y;
  const float threehalfs = 1.5F;

  x2 = number * 0.5F;
  debug_printf("x2=%f\n", x2);
  y  = number;
  debug_printf("y=%f\n", y);
  i  = * ( long * ) &y;
  debug_printf("i=%ld\n", i);
  i  = 0x5f3759dfL - ( i >> 1 );
  debug_printf("i=%ld\n", i);
  y  = * ( float * ) &i;
  debug_printf("y=%f\n", y);
  y  = y * ( threehalfs - ( x2 * y * y ) );
  debug_printf("y=%f\n", y);

  return y;
}

int main (void)
{
#ifdef DEBUG
  // value taken from https://en.wikipedia.org/wiki/Fast_inverse_square_root
  float f = 0.15625;
#else
  float f = nondet_float();
  // Everything in this range hits the bug
  __CPROVER_assume(f < +INFINITY);
  __CPROVER_assume(f > 0.0f);
#endif

  // Should pass ass 1/sqrt(f) is always > 0 when f > 0
  assert(Q_rsqrt(f) > 0);

  return 1;
}

[tautschnig]

Oh, well, the problem is actually a very different one: why does none of our property checks (try --pointer-check --bounds-check) catch that you are using long when the type of i should be int (on a 64-bit Unix system)? Byte-extracting 8 bytes out of a 4-byte value is undefined. (Edit: This 32bit/64bit incompatibility has been fixed in forks like https://github.com/ec-/Quake3e.)