Semantics of Floating Point Operations
SPARK assumes that floating point operations are carried out in single
precision (binary32), double precision (binary64) or extended precision
(binary80) as defined in the IEEE-754 standard for floating point
arithmetic. You should make sure that this is the case on your platform. For
example, on x86 platforms, by default some intermediate computations may be
carried out in extended precision, even if the type of the operands is of
single or double precision, leading to unexpected results. With GNAT/GCC, you
can specify the use of SSE arithmetic by using the compilation switches
-msse2 -mfpmath=sse
which cause all arithmetic to be done using the SSE
instruction set which only provides 32-bit and 64-bit IEEE types, and does not
provide extended precision. SSE arithmetic is also more efficient. Note that
the ABI allows free mixing of units using the three types of floating-point, so
it is not necessary to force all units in a program to use SSE arithmetic.
Several architectures also have fused-multiple-add (FMA) instructions, either
in the base set (PowerPC, Aarch64) or in extensions (SPARC, x86). You should
make sure that your compiler is instructed not to use such instructions, whose
effect on the program semantics cannot be taken into account by SPARK source
code analysis. On x86, such instructions are enabled in GNAT/GCC by means of an
explicit switch like -fma/-fma4
or by architecture switches like
-msse4.1
or -mavx512f
, so make sure you’re not using these. With
GNAT/GCC, it is recommended to use switch -ffp-contract=off
to disable all
floating-point expression contractions, including FMA.
SPARK considers the floating point values which represent positive, negative infinity or NaN as invalid. Proof obligations are generated that such values cannot occur.
SPARK considers rounding on floating point arithmetic operations to follow Round-Nearest-Even (RNE) mode, where a real result is rounded to the nearest floating point value, and ties are resolved to the floating-point with a zero in the last place. This mode of rounding (the default in GNAT) should be forced if needed on the hardware to be able to rely on the results of GNATprove regarding floating point arithmetic (e.g. when using SSE arithmetic, the MXCSR register should specify RNE mode, which it does by default).