c - 需要帮助理解 "Varieties of Static Analyzers: A Comparison with ASTREE"中呈现的浮点舍入

Question

% cat double-float1.c

 int main () {
 double x; float a, y, z, r1, r2;
 a = 1.0; x = 1125899973951488.0; y = (x + a); z = (x - a);
 r1 = y - z; r2 = 2 * a;
 printf("(x + a) - (x - a) = %f\n", r1);
 printf("2a = %f\n", r2);
 }



% gcc double-float1.c >& /dev/null; ./a.out
 (x + a) - (x - a) = 134217728.000000
 2a = 2.000000

更改最低有效数字后

% cat double-float2.c



int main () {
 double x; float a, y, z, r1, r2;
 a = 1.0; x = 1125899973951487.0; y = (x + a); z = (x - a);
 r1 = y - z; r2 = 2 * a;
 printf("(x + a) - (x - a) = %f\n", r1);
 printf("2a = %f\n", r2);
 }



% gcc double-float2.c >& /dev/null; ./a.out
 (x + a) - (x - a) = 0.000000
 2a = 2.000000

任何人都可以帮助我理解第一个示例中的内部表示如何舍入为不同的值以及第二个示例中的内部表示如何舍入为相同的值。我在其中找到了上述示例的论文链接如下。

Varieties of Static Analyzers: A Comparison with ASTREE

Answer 1

原因是 float 内部必须使用精度有限的尾数来表示。首先，如果您存储的实际十进制数无法使用实际二进制数表示，则根据特定的IEEE-754 rules，它会四舍五入到下一个最接近的二进制值。 。接下来，如果实际十进制数的位数超出了浮点类型允许的精度，则即使您使用的是十进制浮点类型，也必须对其进行舍入。

请注意，在这种情况下，根本原因是精度，而不是二进制格式，尽管二进制格式会增加额外的困惑，因为它四舍五入到可以用 24 个二进制数字表示的最接近的数字。如果您的语言具有 10 位精度的 native 十进制浮点类型，它仍然需要对内存中的数字进行舍入:

Decimal number     | Nearest decimal with 10 digits precision 
------------------ | ---------------------------------------
123450000149997.0  | 123450000100000
123450000149998.0  | 123450000100000
123450000149999.0  | 123450000100000
123450000150000.0  | 123450000200000
123450000150001.0  | 123450000200000
123450000150002.0  | 123450000200000

就您而言，舍入点恰好位于 1125899973951488 和 1125899973951489 之间。自32-bit float has 24 bits of precision (为尾数保留的 23 位 + 隐式前导位设置为 1)，它的十进制精度约为 7.22 位十进制数字。这就是您的示例中数字的存储方式:

Decimal number     | Actual IEEE-754 value | IEEE-754 bits (sign, exponent, mantissa)
------------------ | ----------------------|-----------------------------------------
1125899973951486.0 | 1125899906842624      | 0 10110001 00000000000000000000000
1125899973951487.0 | 1125899906842624      | 0 10110001 00000000000000000000000
1125899973951488.0 | 1125899906842624      | 0 10110001 00000000000000000000000
1125899973951489.0 | 1125900041060352      | 0 10110001 00000000000000000000001
1125899973951490.0 | 1125900041060352      | 0 10110001 00000000000000000000001
1125899973951491.0 | 1125900041060352      | 0 10110001 00000000000000000000001

因此，(x - 1) 和 (x + 1) 将舍入为相同的值，直到达到 1125899973951488.0。要探索如何使用 IEEE-754 在内部存储 float ，有一个有用的 online calculator你可以使用。