Skip to content

Commit a31c7ca

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

File tree

4 files changed

+152
-24
lines changed

4 files changed

+152
-24
lines changed

‎src/ansi-c/ansi_c_internal_additions.cpp

+12
Original file line numberDiff line numberDiff line change
@@ -199,6 +199,18 @@ void ansi_c_internal_additions(std::string &code)
199199
"long double __CPROVER_infl(void);\n"
200200
"int __CPROVER_thread_local __CPROVER_rounding_mode="+
201201
std::to_string(config.ansi_c.rounding_mode)+";\n"
202+
"int __CPROVER_isgreaterf(float f, float g);\n"
203+
"int __CPROVER_isgreaterd(double f, double g);\n"
204+
"int __CPROVER_isgreaterequalf(float f, float g);\n"
205+
"int __CPROVER_isgreaterequald(double f, double g);\n"
206+
"int __CPROVER_islessf(float f, float g);\n"
207+
"int __CPROVER_islessd(double f, double g);\n"
208+
"int __CPROVER_islessequalf(float f, float g);\n"
209+
"int __CPROVER_islessequald(double f, double g);\n"
210+
"int __CPROVER_islessgreaterf(float f, float g);\n"
211+
"int __CPROVER_islessgreaterd(double f, double g);\n"
212+
"int __CPROVER_isunorderedf(float f, float g);\n"
213+
"int __CPROVER_isunorderedd(double f, double g);\n"
202214

203215
// absolute value
204216
"int __CPROVER_abs(int x);\n"

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

+1
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,7 @@ double __CPROVER_inf(void);
7979
float __CPROVER_inff(void);
8080
long double __CPROVER_infl(void);
8181
//extern int __CPROVER_thread_local __CPROVER_rounding_mode;
82+
int __CPROVER_isgreaterd(double f, double g);
8283

8384
// absolute value
8485
int __CPROVER_abs(int);

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

+68-24
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

+71
Original file line numberDiff line numberDiff line change
@@ -1990,6 +1990,77 @@ void goto_convertt::do_function_call_symbol(
19901990

19911991
// void __sync_lock_release (type *ptr, ...)
19921992
}
1993+
else if(identifier=="__builtin_isgreater" ||
1994+
identifier=="__builtin_isgreater" ||
1995+
identifier=="__builtin_isgreaterequal" ||
1996+
identifier=="__builtin_isless" ||
1997+
identifier=="__builtin_islessequal" ||
1998+
identifier=="__builtin_islessgreater" ||
1999+
identifier=="__builtin_isunordered")
2000+
{
2001+
// these support two double or two float arguments; we call the
2002+
// appropriate internal version
2003+
if(arguments.size()!=2 ||
2004+
(arguments[0].type()!=double_type() &&
2005+
arguments[0].type()!=float_type()) ||
2006+
(arguments[1].type()!=double_type() &&
2007+
arguments[1].type()!=float_type()))
2008+
{
2009+
error().source_location=function.find_source_location();
2010+
error() << "`" << identifier
2011+
<< "' expected to have two float/double arguments"
2012+
<< eom;
2013+
throw 0;
2014+
}
2015+
2016+
exprt::operandst new_arguments=arguments;
2017+
2018+
bool use_double=arguments[0].type()==double_type();
2019+
if(arguments[0].type()!=arguments[1].type())
2020+
{
2021+
if(use_double)
2022+
new_arguments[1].make_typecast(arguments[0].type());
2023+
else
2024+
{
2025+
new_arguments[0].make_typecast(arguments[1].type());
2026+
use_double=true;
2027+
}
2028+
}
2029+
2030+
code_typet f_type=to_code_type(function.type());
2031+
f_type.remove_ellipsis();
2032+
const typet &a_t=new_arguments[0].type();
2033+
f_type.parameters()=
2034+
code_typet::parameterst(2, code_typet::parametert(a_t));
2035+
2036+
// replace __builtin_ by CPROVER_PREFIX
2037+
std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
2038+
// append d or f for double/float
2039+
name+=use_double?'d':'f';
2040+
2041+
symbol_exprt new_function=function;
2042+
new_function.set_identifier(name);
2043+
new_function.type()=f_type;
2044+
2045+
code_function_callt function_call;
2046+
function_call.lhs()=lhs;
2047+
function_call.function()=new_function;
2048+
function_call.arguments()=new_arguments;
2049+
function_call.add_source_location()=function.source_location();
2050+
2051+
if(!symbol_table.has_symbol(name))
2052+
{
2053+
code_typet();
2054+
symbolt new_symbol;
2055+
new_symbol.base_name=name;
2056+
new_symbol.name=name;
2057+
new_symbol.type=f_type;
2058+
new_symbol.location=function.source_location();
2059+
symbol_table.add(new_symbol);
2060+
}
2061+
2062+
copy(function_call, FUNCTION_CALL, dest);
2063+
}
19932064
else
19942065
{
19952066
do_function_call_symbol(*symbol);

0 commit comments

Comments
 (0)