klee_assume(f == f) is not a good way to ignore paths where symbolics are NaN about fp-benchmarks-aachen HOT 4 CLOSED

Compilers may not optimize this scenario, as the result of f == f is not known at compile time (passing a pointer to the object that f refers to to an unknown function -- klee_make_symbolic -- changes the status of that value from "undefined" to "unknown", as the definition of klee_make_symbolic cannot be known to the compiler).

The case you are referring to, explicitly allows the compiler to ignore floating point rules to generate faster code. Allowing the compiler to make invalid assumptions, has the obvious drawback, that the compiler may generate invalid assumptions ;)

from fp-benchmarks-aachen.

@danielschemmel Sure what you mention above is all true but why not just use isnan()? It's a lot clearer and would do the right thing even if -ffast-math is being used.

from fp-benchmarks-aachen.

@delcypher There are a few reasons against using isnan:

• isnan is guaranteed to be a macro, one legal implementation of which is self comparison
• its implementation may actually be problematic for klee_assume
• We want to discourage simply recognizing the usage of a function, and instead promote relying on floating point semantics (in our tools at least)

I am aware that this is not a problem for either uclibc nor glibc, which use basically the same implementation that uses a type generic macro falling down to a builtin, and your argument for clarity does have its own merit. Personally, however I prefer a solution that is known to be correct w.r.t. any valid C compiler and library.

from fp-benchmarks-aachen.

Having discussed this in the conference call, our decision was to assume -ffast-math is disabled and floating point behavior is correct.

from fp-benchmarks-aachen.