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


% 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) = %fn", r1);
printf("2a = %fn", 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) = %fn", r1);
printf("2a = %fn", r2);
}

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

谁能帮助我理解第一个示例中的内部表示如何舍入到不同的值并在第二个示例中舍入到相同的值。指向论文的链接,我在下面找到了上述示例。

各种静态分析仪:与ASTREE的比较

原因是内部的浮点数必须使用精度有限的尾数表示。首先,如果您存储的实际十进制数无法使用实际二进制数表示,则根据某些 IEEE-754 规则,将其舍入到下一个最接近的二进制值。接下来,如果实际十进制数的位数超过浮点类型的精度允许的位数,则必须对其进行舍入,即使您使用的是十进制浮点类型也是如此。

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

十进制数 |最接近的小数点,精度为 10 位 ------------------ |--------------------------------------- 123450000149997.0 |123450000100000 123450000149998.0 |123450000100000 123450000149999.0 |123450000100000 123450000150000.0 |123450000200000 123450000150001.0 |123450000200000 123450000150002.0 |123450000200000

在您的情况下,舍入点正好在11258999739514881125899973951489之间。由于 32 位浮点数具有 24 位精度(为尾数保留的 23 位 + 隐式前导位设置为 1(,因此它可以具有 ~7.22 个十进制数字的近似十进制精度。这是示例中数字的存储方式:

十进制数 |实际 IEEE-754 值 |IEEE-754 位(符号、指数、尾数( ------------------ |----------------------|----------------------------------------- 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 n = 0.0f;
uint32_t k;
while (1) 
{
n += 1.0f; k++;
if (k == 10000)
{
printf("%fn", n);
k = 0;
}
};

最新更新