Overflow in FP operators

[fontainep]

Levent Erkok suggested to introduce FP overflow operators (as a reaction to an email about BV overflow operators on 22 Dec 2022):

These predicates are indeed very welcome. Unlike Florian, however, I think it'd also be good to add similar functionality to float conversion functions:

; from another floating point sort
((_ to_fp eb sb) RoundingMode (_ FloatingPoint mb nb) (_ FloatingPoint eb sb))

; from real
((_ to_fp eb sb) RoundingMode Real (_ FloatingPoint eb sb))

; from signed machine integer, represented as a 2's complement bit vector
((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))

; from unsigned machine integer, represented as bit vector
((_ to_fp_unsigned eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))

; to unsigned machine integer, represented as a bit vector
((_ fp.to_ubv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))

; to signed machine integer, represented as a 2's complement bit vector
((_ fp.to_sbv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))

; to real
(fp.to_real (_ FloatingPoint eb sb) Real)

For naming: If a solver wants to provide individual overflow/underflow checking, maybe it's best to name these similar to bvsadd_out_of_range; then the names bvsaddo/bvsaddu can remain free for individual solver use to indicate overflow/underflow conditions.

[fontainep]

Then Martin Brain reacted:
In principle, yes, this could be good. However some thought may be
required over semantics. Off the top of my head:

• Do you want to distinguish between early and late overflow? I.E.
  before or after rounding. There has been some ambiguity over this in
  the past.

• How do these connect with the type of float produced? Is producing a
  subnormal / zero underflow? Can you overflow and not get infinity (for
  example, in directed rounding modes)?

[fontainep]

With Levent additional remarks:
My motivation for overflow checking is to be able to model x86 instructions faithfully. For float-to-float conversions, I think a good example is to use CVTSD2SS instruction. (See Table D-16, Vol 1. D13 of Intel® 64 and IA-32 Architectures Software Developer’s Manual Combined Volumes: 1, 2A, 2B, 2C, 2D, 3A, 3B, 3C, 3D, and 4 You can see how CVTSD2SS is treated in the masked response cases with differing rounding-modes.)

Based on this, I think the specific answers are:

• No need to distinguish early/late overflow; late is sufficient. That is, overflow is detected after rounding.
• Since we’re considering after rounding, I think the overflow result will directly correspond to the conversion:
  * If you get overflow/underflow, then the result should be +/- infinity.
  * If the result is a subnormal, no overflow really exists. This is a precision loss, not overflow/underflow.

As I mentioned, the overriding goal is the ease of modeling of the conversion operators as found in x86/ARM etc. (Which I admit can be rather confusing themselves.) So, if anyone can come up with a notion of overflow that differs from the above but still allows simple modeling of what x86/ARM does, I think that should still be just fine as well.