Skip to content

Commit 45d7f08

Browse files
tautschnigtautschnig
committed
Support "polymorphic" floating-point functions, fix typos
make -C ansi-c library_check is now happy again.
1 parent e821efe commit 45d7f08

File tree

4 files changed

+152
-24
lines changed

4 files changed

+152
-24
lines changed

‎src/ansi-c/ansi_c_internal_additions.cpp

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -197,6 +197,18 @@ void ansi_c_internal_additions(std::string &code)
197197
"long double __CPROVER_infl(void);\n"
198198
"int __CPROVER_thread_local __CPROVER_rounding_mode="+
199199
std::to_string(config.ansi_c.rounding_mode)+";\n"
200+
"int __CPROVER_isgreaterf(float f, float g);\n"
201+
"int __CPROVER_isgreaterd(double f, double g);\n"
202+
"int __CPROVER_isgreaterequalf(float f, float g);\n"
203+
"int __CPROVER_isgreaterequald(double f, double g);\n"
204+
"int __CPROVER_islessf(float f, float g);\n"
205+
"int __CPROVER_islessd(double f, double g);\n"
206+
"int __CPROVER_islessequalf(float f, float g);\n"
207+
"int __CPROVER_islessequald(double f, double g);\n"
208+
"int __CPROVER_islessgreaterf(float f, float g);\n"
209+
"int __CPROVER_islessgreaterd(double f, double g);\n"
210+
"int __CPROVER_isunorderedf(float f, float g);\n"
211+
"int __CPROVER_isunorderedd(double f, double g);\n"
200212

201213
// absolute value
202214
"int __CPROVER_abs(int x);\n"

‎src/ansi-c/library/cprover.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,7 @@ double __CPROVER_inf(void);
9292
float __CPROVER_inff(void);
9393
long double __CPROVER_infl(void);
9494
//extern int __CPROVER_thread_local __CPROVER_rounding_mode;
95+
int __CPROVER_isgreaterd(double f, double g);
9596

9697
// absolute value
9798
int __CPROVER_abs(int);

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

Lines changed: 68 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -22,33 +22,69 @@ inline long double __builtin_fabsl(long double d) { return __CPROVER_fabsl(d); }
2222

2323
inline float __builtin_fabsf(float f) { return __CPROVER_fabsf(f); }
2424

25-
/* FUNCTION: __builtin_isgreater */
25+
/* FUNCTION: __CPROVER_isgreaterf */
2626

27-
int __builtin_isgreater(double f, double g) { return f > g; }
27+
int __CPROVER_isgreaterf(float f, float g) { return f > g; }
2828

29-
/* FUNCTION: __builtin_isgreaterequal */
29+
/* FUNCTION: __CPROVER_isgreaterd */
3030

31-
int __builtin_isgreaterequal(float f, float g) { return f >= g; }
31+
int __CPROVER_isgreaterd(double f, double g) { return f > g; }
3232

33-
/* FUNCTION: __builtin_isless */
33+
/* FUNCTION: __CPROVER_isgreaterequalf */
3434

35-
int __builtin_isless(float f, float g) { return f < g;}
35+
int __CPROVER_isgreaterequalf(float f, float g) { return f >= g; }
3636

37-
/* FUNCTION: __builtin_islessequal */
37+
/* FUNCTION: __CPROVER_isgreaterequald */
3838

39-
int __builtin_islessequal(float f, float g) { return f <= g; }
39+
int __CPROVER_isgreaterequald(double f, double g) { return f >= g; }
4040

41-
/* FUNCTION: __builtin_islessgreater */
41+
/* FUNCTION: __CPROVER_islessf */
4242

43-
int __builtin_islessgreater(float f, float g) { return (f < g) || (f > g); }
43+
int __CPROVER_islessf(float f, float g) { return f < g;}
4444

45-
/* FUNCTION: __builtin_isunordered */
45+
/* FUNCTION: __CPROVER_islessd */
4646

47-
int __builtin_isunordered(float f, float g) { return isnan(f) || isnan(g); }
47+
int __CPROVER_islessd(double f, double g) { return f < g;}
48+
49+
/* FUNCTION: __CPROVER_islessequalf */
50+
51+
int __CPROVER_islessequalf(float f, float g) { return f <= g; }
52+
53+
/* FUNCTION: __CPROVER_islessequald */
54+
55+
int __CPROVER_islessequald(double f, double g) { return f <= g; }
56+
57+
/* FUNCTION: __CPROVER_islessgreaterf */
58+
59+
int __CPROVER_islessgreaterf(float f, float g) { return (f < g) || (f > g); }
60+
61+
/* FUNCTION: __CPROVER_islessgreaterd */
62+
63+
int __CPROVER_islessgreaterd(double f, double g) { return (f < g) || (f > g); }
64+
65+
/* FUNCTION: __CPROVER_isunorderedf */
66+
67+
#ifndef __CPROVER_MATH_H_INCLUDED
68+
#include <math.h>
69+
#define __CPROVER_MATH_H_INCLUDED
70+
#endif
71+
72+
int __CPROVER_isunorderedf(float f, float g) { return isnanf(f) || isnanf(g); }
73+
74+
/* FUNCTION: __CPROVER_isunorderedd */
75+
76+
#ifndef __CPROVER_MATH_H_INCLUDED
77+
#include <math.h>
78+
#define __CPROVER_MATH_H_INCLUDED
79+
#endif
80+
81+
int __CPROVER_isunorderedd(double f, double g) { return isnan(f) || isnan(g); }
4882

4983

5084
/* FUNCTION: isfinite */
5185

86+
#undef isfinite
87+
5288
int isfinite(double d) { return __CPROVER_isfinited(d); }
5389

5490
/* FUNCTION: __finite */
@@ -65,6 +101,8 @@ int __finitel(long double ld) { return __CPROVER_isfiniteld(ld); }
65101

66102
/* FUNCTION: isinf */
67103

104+
#undef isinf
105+
68106
inline int isinf(double d) { return __CPROVER_isinfd(d); }
69107

70108
/* FUNCTION: __isinf */
@@ -89,6 +127,8 @@ inline int __isinfl(long double ld) { return __CPROVER_isinfld(ld); }
89127

90128
/* FUNCTION: isnan */
91129

130+
#undef isnan
131+
92132
inline int isnan(double d) { return __CPROVER_isnand(d); }
93133

94134
/* FUNCTION: __isnan */
@@ -113,6 +153,8 @@ inline int __isnanl(long double ld) { return __CPROVER_isnanld(ld); }
113153

114154
/* FUNCTION: isnormal */
115155

156+
#undef isnormal
157+
116158
inline int isnormal(double d) { return __CPROVER_isnormald(d); }
117159

118160
/* FUNCTION: __isnormalf */
@@ -177,6 +219,8 @@ inline int _fdsign(float f) { return __CPROVER_signf(f); }
177219

178220
/* FUNCTION: signbit */
179221

222+
#undef signbit
223+
180224
inline int signbit(double d) { return __CPROVER_signd(d); }
181225

182226
/* FUNCTION: __signbitd */
@@ -1032,7 +1076,7 @@ float fdimf(float f, float g) { return ((f > g) ? f - g : +0.0f); }
10321076
#define __CPROVER_MATH_H_INCLUDED
10331077
#endif
10341078

1035-
long double fdim(long double f, long double g) { return ((f > g) ? f - g : +0.0); }
1079+
long double fdiml(long double f, long double g) { return ((f > g) ? f - g : +0.0); }
10361080

10371081

10381082

@@ -1130,7 +1174,7 @@ float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d)
11301174

11311175
long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d)
11321176
{
1133-
long double magicConst = 0x1.0p+64d;
1177+
long double magicConst = 0x1.0p+64;
11341178
long double return_value;
11351179
int saved_rounding_mode = fegetround();
11361180
fesetround(rounding_mode);
@@ -1421,7 +1465,7 @@ float roundf(float x)
14211465
xp = x;
14221466
}
14231467

1424-
fegetround(FE_TOWARDZERO);
1468+
fesetround(saved_rounding_mode);
14251469

14261470
return __sort_of_CPROVER_round_to_integralf(FE_TOWARDZERO, xp);
14271471
}
@@ -1643,7 +1687,7 @@ long int lrint(double x)
16431687

16441688
float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
16451689

1646-
float lrintf(float x)
1690+
long int lrintf(float x)
16471691
{
16481692
// TODO : should be an all-in-one __CPROVER function to allow
16491693
// conversion to SMT
@@ -1666,7 +1710,7 @@ float lrintf(float x)
16661710

16671711
long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
16681712

1669-
long double lrintl(long double x)
1713+
long int lrintl(long double x)
16701714
{
16711715
// TODO : should be an all-in-one __CPROVER function to allow
16721716
// conversion to SMT
@@ -1711,7 +1755,7 @@ long long int llrint(double x)
17111755

17121756
float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
17131757

1714-
float llrintf(float x)
1758+
long long int llrintf(float x)
17151759
{
17161760
// TODO : should be an all-in-one __CPROVER function to allow
17171761
// conversion to SMT
@@ -1734,7 +1778,7 @@ float llrintf(float x)
17341778

17351779
long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
17361780

1737-
long double llrintl(long double x)
1781+
long long int llrintl(long double x)
17381782
{
17391783
// TODO : should be an all-in-one __CPROVER function to allow
17401784
// conversion to SMT
@@ -1803,7 +1847,7 @@ long int lround(double x)
18031847

18041848
float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
18051849

1806-
float lroundf(float x)
1850+
long int lroundf(float x)
18071851
{
18081852
// TODO : should be an all-in-one __CPROVER function to allow
18091853
// conversion to SMT, plus should use RNA
@@ -1840,7 +1884,7 @@ float lroundf(float x)
18401884

18411885
long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
18421886

1843-
long double lroundl(long double x)
1887+
long int lroundl(long double x)
18441888
{
18451889
int saved_rounding_mode = fegetround();
18461890
fesetround(FE_TOWARDZERO);
@@ -1913,7 +1957,7 @@ long long int llround(double x)
19131957

19141958
float __sort_of_CPROVER_round_to_integralf (int rounding_mode, float d);
19151959

1916-
float llroundf(float x)
1960+
long long int llroundf(float x)
19171961
{
19181962
// TODO : should be an all-in-one __CPROVER function to allow
19191963
// conversion to SMT, plus should use RNA
@@ -1950,7 +1994,7 @@ float llroundf(float x)
19501994

19511995
long double __sort_of_CPROVER_round_to_integrall (int rounding_mode, long double d);
19521996

1953-
long double llroundl(long double x)
1997+
long long int llroundl(long double x)
19541998
{
19551999
// TODO : should be an all-in-one __CPROVER function to allow
19562000
// conversion to SMT, plus should use RNA
@@ -1969,7 +2013,7 @@ long double llroundl(long double x)
19692013
fesetround(saved_rounding_mode);
19702014

19712015
long double rti = __sort_of_CPROVER_round_to_integrall(FE_TOWARDZERO, xp);
1972-
return (long int)rti;
2016+
return (long long int)rti;
19732017
}
19742018

19752019

‎src/goto-programs/builtin_functions.cpp

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1767,6 +1767,77 @@ void goto_convertt::do_function_call_symbol(
17671767

17681768
// void __sync_lock_release (type *ptr, ...)
17691769
}
1770+
else if(identifier=="__builtin_isgreater" ||
1771+
identifier=="__builtin_isgreater" ||
1772+
identifier=="__builtin_isgreaterequal" ||
1773+
identifier=="__builtin_isless" ||
1774+
identifier=="__builtin_islessequal" ||
1775+
identifier=="__builtin_islessgreater" ||
1776+
identifier=="__builtin_isunordered")
1777+
{
1778+
// these support two double or two float arguments; we call the
1779+
// appropriate internal version
1780+
if(arguments.size()!=2 ||
1781+
(arguments[0].type()!=double_type() &&
1782+
arguments[0].type()!=float_type()) ||
1783+
(arguments[1].type()!=double_type() &&
1784+
arguments[1].type()!=float_type()))
1785+
{
1786+
error().source_location=function.find_source_location();
1787+
error() << "`" << identifier
1788+
<< "' expected to have two float/double arguments"
1789+
<< eom;
1790+
throw 0;
1791+
}
1792+
1793+
exprt::operandst new_arguments=arguments;
1794+
1795+
bool use_double=arguments[0].type()==double_type();
1796+
if(arguments[0].type()!=arguments[1].type())
1797+
{
1798+
if(use_double)
1799+
new_arguments[1].make_typecast(arguments[0].type());
1800+
else
1801+
{
1802+
new_arguments[0].make_typecast(arguments[1].type());
1803+
use_double=true;
1804+
}
1805+
}
1806+
1807+
code_typet f_type=to_code_type(function.type());
1808+
f_type.remove_ellipsis();
1809+
const typet &a_t=new_arguments[0].type();
1810+
f_type.parameters()=
1811+
code_typet::parameterst(2, code_typet::parametert(a_t));
1812+
1813+
// replace __builtin_ by CPROVER_PREFIX
1814+
std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
1815+
// append d or f for double/float
1816+
name+=use_double?'d':'f';
1817+
1818+
symbol_exprt new_function=function;
1819+
new_function.set_identifier(name);
1820+
new_function.type()=f_type;
1821+
1822+
code_function_callt function_call;
1823+
function_call.lhs()=lhs;
1824+
function_call.function()=new_function;
1825+
function_call.arguments()=new_arguments;
1826+
function_call.add_source_location()=function.source_location();
1827+
1828+
if(!symbol_table.has_symbol(name))
1829+
{
1830+
code_typet();
1831+
symbolt new_symbol;
1832+
new_symbol.base_name=name;
1833+
new_symbol.name=name;
1834+
new_symbol.type=f_type;
1835+
new_symbol.location=function.source_location();
1836+
symbol_table.add(new_symbol);
1837+
}
1838+
1839+
copy(function_call, FUNCTION_CALL, dest);
1840+
}
17701841
else
17711842
{
17721843
do_function_call_symbol(*symbol);

0 commit comments

Comments
 (0)