Havoc-ing a FloatingPoint value does not assume NaN values

[leventeBajczi]

The following simple (C) program can violate the assertion, because NaN!=NaN:

int main()
{
  double x = __VERIFIER_nondet_double();
  assert(x==x);
}

Yet the (correctly translated) CFA is assumed to be safe.

[hajduakos]

I think the problem might lie here in the simplifier. If both the LHS and the RHS are the same reference then we assume the expression to be true, which makes sense for most of the types. If it's an exception for floats, because NaN does not equal NaN, then it should be fixed here I think.

Also, what does the solver think about this? Is it C specific or should it also be unsafe according to SMT theory of floats?

[leventeBajczi]

As both C and Z3 assume IEEE-754 fp arithmetic, and that standard is fortunately well-defined, there should not be any inconsistencies among them.

I think you are right about the simplification being wrong, I'll test this in a bit and report back.

[hajduakos]

Yeah. I'd first try removing that branch of the simplification completely, that should leave the expression as is and pass it to the solver. If that works, you can try actually implementing the proper simplification rule if possible.

[leventeBajczi]

Unfortunately this did not solve the problem, it is still reported as safe.

[hajduakos]

Interesting, then it needs some more debugging to see where the expression gets interpreted as true.

[leventeBajczi]

I think (but this is only an (un)educated guess) that the refinement strategy does not take it into account that two bit-perfect values might be unequal. I think this because while the algorithm is running, there are some unsafe nodes in the ARGs that disappear after a while (4-5th iteration, depending on the domain and refinement strategy). Is this a possible reason, or am I mistaken?

[hajduakos]

What refinement strategy are you using? The ones based on Z3 will use Z3 so they should be able to handle this case (but I assume you don't use those as those cannot interpolate over floats). If you are using Newton method then @as3810t might give you some hints on what operators it is using. Maybe some pre/post operators cannot handle this special case.

[leventeBajczi]

I am using the NWT_SP and NWT_IT_SP strategies, the former is producing the erroneous output and the latter is seemingly stuck in a loop where every ARG is only 1 incomplete node, without being able to progress.