IA32 for a non-SSE processor about compcert HOT 3 CLOSED

x87 floating point arithmetic has a major problem: it uses a precision of 80 bits (64 bits mantissa, 15 bits exponent, 1 bit sign, if I am not misleading). It is very complex to emulate double precision arithmetic from 80bits arithmetic.

This is the reason for one of the oldest bug of GCC : https://gcc.gnu.org/bugzilla/show_bug.cgi?id=323.

from compcert.

Indeed, for a moment I thought that maybe FPU registers "seen as" MMX could avoid that, but in fact there are no floating-point MMX instructions.
I guess that's pretty much a killer feature there! Certainly more trouble than I was expecting. Thank you for clarifying that!

from compcert.

Right, as jhjourdan wrote, the x87 FP stack is a poor match for CompCert. The issue with extended precision (80 bits) can be addressed to some extent by configuring the x87 in 53-bit mantissa mode. But the exponent range is still larger than that of IEEE binary64 format, so we'd need to store every intermediate result to the stack to force binary64 normalization of the exponent... That's neither pretty nor efficient!

from compcert.