There is an excellent recent work to translate floating point instructions to LLVM bitecode language, the project is called McSema and is managed by people at TrailOfBits.
One of the developer promised to get it OpenSource once the code will get in a good shape.
EDIT: I just saw the answer from Ed McMan. I totally agree with him about the fact that the lack of tools handling this kind of problem makes it quite hard to integrate into binary program analysis framework. But, this is already a consequence of the problem, not a cause.
In fact, in my humble opinion, what is making this problem extremely tedious is its own nature. You have to deal with a continuous problem (logic on floating point numbers) and transform it into a discrete one (propositional logic).
The mix of these two models makes it very difficult to handle because a small difference in the input may end-up in a drastically different output (the bit-vector size may also have a big impact on the output). This kind of behavior is quite close to what you encounter in cryptographic hash functions, where a small modification of the input will result in a complete change of the output.
And, this high variability of the output doesn't help tools to wrap all the behaviors into a meaningful logic formula that could be expressed in propositional logic along with the others.
There is maybe some hope if SMT-solvers start to consider mixing usual
QF_AUFBV logic (often used for program simulation) and floating point logic (