Skip to content

Commit 0777675

Browse files
martintautschnig
martin
authored and
tautschnig
committed
An alternative implementation to avoid the difference between RNE and RNA.
1 parent 9f23c25 commit 0777675

File tree

1 file changed

+152
-25
lines changed

1 file changed

+152
-25
lines changed

‎src/ansi-c/library/math.c‎

Lines changed: 152 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1370,8 +1370,24 @@ double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
13701370

13711371
double round(double x)
13721372
{
1373-
// TODO : Should be RNA not RNE, needs a new rounding mode
1374-
return __sort_of_CPROVER_round_to_integral(FE_TONEAREST, x);
1373+
// Tempting but RNE not RNA
1374+
// return __sort_of_CPROVER_round_to_integral(FE_TONEAREST, x);
1375+
1376+
int saved_rounding_mode = fegetround();
1377+
fesetround(FE_TOWARDZERO);
1378+
1379+
double xp;
1380+
if (x > 0.0) {
1381+
xp = x + 0.5;
1382+
} else if (x < 0.0) {
1383+
xp = x - 0.5;
1384+
} else {
1385+
xp = x;
1386+
}
1387+
1388+
fesetround(saved_rounding_mode);
1389+
1390+
return __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, xp);
13751391
}
13761392

13771393
/* FUNCTION: roundf */
@@ -1390,8 +1406,24 @@ float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
13901406

13911407
float roundf(float x)
13921408
{
1393-
// TODO : Should be RNA not RNE, needs a new rounding mode
1394-
return __sort_of_CPROVER_round_to_integralf(FE_TONEAREST, x);
1409+
// Tempting but RNE not RNA
1410+
// return __sort_of_CPROVER_round_to_integralf(FE_TONEAREST, x);
1411+
1412+
int saved_rounding_mode = fegetround();
1413+
fesetround(FE_TOWARDZERO);
1414+
1415+
float xp;
1416+
if (x > 0.0f) {
1417+
xp = x + 0.5f;
1418+
} else if (x < 0.0f) {
1419+
xp = x - 0.5f;
1420+
} else {
1421+
xp = x;
1422+
}
1423+
1424+
fegetround(FE_TOWARDZERO);
1425+
1426+
return __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, xp);
13951427
}
13961428

13971429

@@ -1411,8 +1443,24 @@ long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double
14111443

14121444
long double roundl(long double x)
14131445
{
1414-
// TODO : Should be RNA not RNE, needs a new rounding mode
1415-
return __sort_of_CPROVER_round_to_integrall(FE_TONEAREST, x);
1446+
// Tempting but RNE not RNA
1447+
// return __sort_of_CPROVER_round_to_integrall(FE_TONEAREST, x);
1448+
1449+
int saved_rounding_mode = fegetround();
1450+
fesetround(FE_TOWARDZERO);
1451+
1452+
long double xp;
1453+
if (x > 0.0) {
1454+
xp = x + 0.5;
1455+
} else if (x < 0.0) {
1456+
xp = x - 0.5;
1457+
} else {
1458+
xp = x;
1459+
}
1460+
1461+
fesetround(saved_rounding_mode);
1462+
1463+
return __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, xp);
14161464
}
14171465

14181466

@@ -1721,9 +1769,23 @@ double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
17211769
long int lround(double x)
17221770
{
17231771
// TODO : should be an all-in-one __CPROVER function to allow
1724-
// conversion to SMT
1725-
// TODO : Should be RNA not RNE, needs a new rounding mode
1726-
double rti = __sort_of_CPROVER_round_to_integral(FE_TONEAREST, x);
1772+
// conversion to SMT, plus should use RNA
1773+
1774+
int saved_rounding_mode = fegetround();
1775+
fesetround(FE_TOWARDZERO);
1776+
1777+
double xp;
1778+
if (x > 0.0) {
1779+
xp = x + 0.5;
1780+
} else if (x < 0.0) {
1781+
xp = x - 0.5;
1782+
} else {
1783+
xp = x;
1784+
}
1785+
1786+
fesetround(saved_rounding_mode);
1787+
1788+
double rti = __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, xp);
17271789
return (long int)rti;
17281790
}
17291791

@@ -1744,9 +1806,22 @@ float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
17441806
float lroundf(float x)
17451807
{
17461808
// TODO : should be an all-in-one __CPROVER function to allow
1747-
// conversion to SMT
1748-
// TODO : Should be RNA not RNE, needs a new rounding mode
1749-
float rti = __sort_of_CPROVER_round_to_integralf(FE_TONEAREST, x);
1809+
// conversion to SMT, plus should use RNA
1810+
int saved_rounding_mode = fegetround();
1811+
fesetround(FE_TOWARDZERO);
1812+
1813+
float xp;
1814+
if (x > 0.0f) {
1815+
xp = x + 0.5f;
1816+
} else if (x < 0.0f) {
1817+
xp = x - 0.5f;
1818+
} else {
1819+
xp = x;
1820+
}
1821+
1822+
fesetround(saved_rounding_mode);
1823+
1824+
float rti = __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, xp);
17501825
return (long int)rti;
17511826
}
17521827

@@ -1767,10 +1842,23 @@ long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double
17671842

17681843
long double lroundl(long double x)
17691844
{
1845+
int saved_rounding_mode = fegetround();
1846+
fesetround(FE_TOWARDZERO);
1847+
17701848
// TODO : should be an all-in-one __CPROVER function to allow
1771-
// conversion to SMT
1772-
// TODO : Should be RNA not RNE, needs a new rounding mode
1773-
long double rti = __sort_of_CPROVER_round_to_integrall(FE_TONEAREST, x);
1849+
// conversion to SMT, plus should use RNA
1850+
long double xp;
1851+
if (x > 0.0) {
1852+
xp = x + 0.5;
1853+
} else if (x < 0.0) {
1854+
xp = x - 0.5;
1855+
} else {
1856+
xp = x;
1857+
}
1858+
1859+
fesetround(saved_rounding_mode);
1860+
1861+
long double rti = __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, xp);
17741862
return (long int)rti;
17751863
}
17761864

@@ -1792,9 +1880,22 @@ double __sort_of_CPROVER_round_to_integral (int rounding_mode, double d);
17921880
long long int llround(double x)
17931881
{
17941882
// TODO : should be an all-in-one __CPROVER function to allow
1795-
// conversion to SMT
1796-
// TODO : Should be RNA not RNE, needs a new rounding mode
1797-
double rti = __sort_of_CPROVER_round_to_integral(FE_TONEAREST, x);
1883+
// conversion to SMT, plus should use RNA
1884+
int saved_rounding_mode = fegetround();
1885+
fesetround(FE_TOWARDZERO);
1886+
1887+
double xp;
1888+
if (x > 0.0) {
1889+
xp = x + 0.5;
1890+
} else if (x < 0.0) {
1891+
xp = x - 0.5;
1892+
} else {
1893+
xp = x;
1894+
}
1895+
1896+
fesetround(saved_rounding_mode);
1897+
1898+
double rti = __sort_of_CPROVER_round_to_integral(FE_TOWARDZERO, xp);
17981899
return (long long int)rti;
17991900
}
18001901

@@ -1815,9 +1916,22 @@ float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
18151916
float llroundf(float x)
18161917
{
18171918
// TODO : should be an all-in-one __CPROVER function to allow
1818-
// conversion to SMT
1819-
// TODO : Should be RNA not RNE, needs a new rounding mode
1820-
float rti = __sort_of_CPROVER_round_to_integralf(FE_TONEAREST, x);
1919+
// conversion to SMT, plus should use RNA
1920+
int saved_rounding_mode = fegetround();
1921+
fesetround(FE_TOWARDZERO);
1922+
1923+
float xp;
1924+
if (x > 0.0f) {
1925+
xp = x + 0.5f;
1926+
} else if (x < 0.0f) {
1927+
xp = x - 0.5f;
1928+
} else {
1929+
xp = x;
1930+
}
1931+
1932+
fesetround(saved_rounding_mode);
1933+
1934+
float rti = __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, xp);
18211935
return (long long int)rti;
18221936
}
18231937

@@ -1839,10 +1953,23 @@ long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double
18391953
long double llroundl(long double x)
18401954
{
18411955
// TODO : should be an all-in-one __CPROVER function to allow
1842-
// conversion to SMT
1843-
// TODO : Should be RNA not RNE, needs a new rounding mode
1844-
long double rti = __sort_of_CPROVER_round_to_integrall(FE_TONEAREST, x);
1845-
return (long long int)rti;
1956+
// conversion to SMT, plus should use RNA
1957+
int saved_rounding_mode = fegetround();
1958+
fesetround(FE_TOWARDZERO);
1959+
1960+
long double xp;
1961+
if (x > 0.0) {
1962+
xp = x + 0.5;
1963+
} else if (x < 0.0) {
1964+
xp = x - 0.5;
1965+
} else {
1966+
xp = x;
1967+
}
1968+
1969+
fesetround(saved_rounding_mode);
1970+
1971+
long double rti = __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, xp);
1972+
return (long int)rti;
18461973
}
18471974

18481975

0 commit comments

Comments
 (0)