sqrt2.c is illegal

[andrew-appel]

The sqrt2 benchmark has undefined semantics in C:

#define BITS(x) (*((unsigned *) &x))
#define FLOAT(x) (*((float *) &x))
float sqrt_approx(float x) {  
  float one = 1;
  unsigned i = (BITS(x) >> 1) + BITS(one) - (BITS(one) >> 1);
  return FLOAT(i);
}

According to paragraph 6.5.7 of the C17 standard, it is illegal to load from a pointer that is cast in that way. The reason is explained in footnote 91, "The intent of this list is to specify those circumstances in which an object can or cannot be aliased."

Indeed, Section 6.3 of "A benchmark for C program verication" says this explicitly: sqrt2.c "violates effective types". The approved way to accomplish this store-float-load-int or store-int-load-float is with a union, exactly as demonstrated in the sqrt3 benchmark, explained in Section 6.3 of the paper.

I propose that the sqrt2 benchmark be removed from the suite.