[tautschnig]

IEEE 754 squareRoot is correctly rounded (C11 F.10.4.5), but the
sqrtf, sqrt and sqrtl models were not:

• They picked lower and upper = nextUp(lower) such that the rounded
  squares bracket the argument x, and in round-to-nearest returned
  lower iff x - lowerlower < upperupper - x, again with rounded
  squares and differences. Comparing distances between squares does
  not decide which root is nearer, and the rounding of the squares
  adds further errors. For example, sqrt(1.0 + DBL_EPSILON) yielded
  1.0 + DBL_EPSILON instead of 1.0. Emulating the sqrtf model
  natively for all 2^24 floats in [1, 4) gives the wrong result for
  2754580 of them (16%).
• In round-downward and round-toward-zero modes they returned upper
  unless the root was exact, i.e., almost always the wrong neighbour.
• In round-upward mode, exactness was tested via the rounded square.

Compute the squares exactly, using double for sqrtf, and a CBMC
floating-point type with a 112-bit fraction for sqrt (144 or 230
bits for sqrtl, depending on the precision of long double), so that
lower <= sqrt(x) < upper holds exactly. Then return lower when
rounding down or toward zero, lower when rounding upward if
lower * lower == x, and, when rounding to nearest, lower iff x is less
than the square of the midpoint of lower and upper (there are no
ties, as that square needs more bits than the format has).

The same native emulation, with exact squares and the new
round-to-nearest choice, yields no wrong results. In a differential
test against glibc of 190 sqrtf and sqrt calls on special and random
inputs in all four rounding modes, the previous models gave the wrong
result in 119 cases, and the new ones in none. The sqrt (double) model takes about 1.5 times as long
to verify as before; sqrtf is as fast as before.

Fixes #9299 (#9301 is an identical duplicate of #9299.)

Found by Jeroen Robben's specification-conformance pipeline (https://reports.robben.io/methodology/).

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• n/a My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing. Review the Copilot code review billing settings.