Skip to content

Commit 3f7685f

Browse files
kroeningkroening
authored
Merge pull request diffblue#2223 from diffblue/fp-builtins
gcc floating-point builtins
2 parents f156ef0 + 72a0379 commit 3f7685f

File tree

3 files changed

+72
-11
lines changed

3 files changed

+72
-11
lines changed

‎regression/cbmc/Float_lib1/main.c‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,9 +27,27 @@ int main() {
2727
assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MIN/2)==3);
2828
assert(__builtin_fpclassify(0, 1, 2, 3, 4, -0.0)==4);
2929

30+
assert(__builtin_isinf(DBL_MAX+DBL_MAX)==1);
31+
assert(__builtin_isinf(0.0)==0);
32+
assert(__builtin_isinf(-(DBL_MAX+DBL_MAX))==1);
33+
34+
assert(__builtin_isinf_sign(DBL_MAX+DBL_MAX)==1);
35+
assert(__builtin_isinf_sign(0.0)==0);
36+
assert(__builtin_isinf_sign(-(DBL_MAX+DBL_MAX))==-1);
37+
3038
// these are compile-time
3139
_Static_assert(__builtin_fpclassify(0, 1, 2, 3, 4, -0.0)==4,
3240
"__builtin_fpclassify is constant");
41+
42+
_Static_assert(__builtin_isnormal(DBL_MIN),
43+
"__builtin_isnormal is constant");
44+
45+
_Static_assert(!__builtin_isinf(0),
46+
"__builtin_isinf is constant");
47+
48+
_Static_assert(__builtin_isinf_sign(0)==0,
49+
"__builtin_isinf_sign is constant");
50+
3351
#endif
3452

3553
assert(signbit(-1.0)!=0);

‎src/ansi-c/c_typecheck_expr.cpp‎

Lines changed: 45 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -2255,7 +2255,7 @@ exprt c_typecheck_baset::do_special_functions(
22552255
isnan_exprt isnan_expr(expr.arguments().front());
22562256
isnan_expr.add_source_location()=source_location;
22572257

2258-
return isnan_expr;
2258+
return typecast_exprt::conditional_cast(isnan_expr, expr.type());
22592259
}
22602260
else if(identifier==CPROVER_PREFIX "isfinitef" ||
22612261
identifier==CPROVER_PREFIX "isfinited" ||
@@ -2271,7 +2271,7 @@ exprt c_typecheck_baset::do_special_functions(
22712271
isfinite_exprt isfinite_expr(expr.arguments().front());
22722272
isfinite_expr.add_source_location()=source_location;
22732273

2274-
return isfinite_expr;
2274+
return typecast_exprt::conditional_cast(isfinite_expr, expr.type());
22752275
}
22762276
else if(identifier==CPROVER_PREFIX "inf" ||
22772277
identifier=="__builtin_inf")
@@ -2343,30 +2343,64 @@ exprt c_typecheck_baset::do_special_functions(
23432343
if(expr.arguments().size()!=1)
23442344
{
23452345
err_location(f_op);
2346-
error() << "isinf expects one operand" << eom;
2346+
error() << identifier << " expects one operand" << eom;
23472347
throw 0;
23482348
}
23492349

23502350
isinf_exprt isinf_expr(expr.arguments().front());
23512351
isinf_expr.add_source_location()=source_location;
23522352

2353-
return isinf_expr;
2353+
return typecast_exprt::conditional_cast(isinf_expr, expr.type());
2354+
}
2355+
else if(identifier == "__builtin_isinf_sign")
2356+
{
2357+
if(expr.arguments().size() != 1)
2358+
{
2359+
err_location(f_op);
2360+
error() << identifier << " expects one operand" << eom;
2361+
throw 0;
2362+
}
2363+
2364+
// returns 1 for +inf and -1 for -inf, and 0 otherwise
2365+
2366+
const exprt &fp_value = expr.arguments().front();
2367+
2368+
isinf_exprt isinf_expr(fp_value);
2369+
isinf_expr.add_source_location() = source_location;
2370+
2371+
return if_exprt(
2372+
isinf_exprt(fp_value),
2373+
if_exprt(
2374+
sign_exprt(fp_value),
2375+
from_integer(-1, expr.type()),
2376+
from_integer(1, expr.type())),
2377+
from_integer(0, expr.type()));
23542378
}
2355-
else if(identifier==CPROVER_PREFIX "isnormalf" ||
2356-
identifier==CPROVER_PREFIX "isnormald" ||
2357-
identifier==CPROVER_PREFIX "isnormalld")
2379+
else if(identifier == CPROVER_PREFIX "isnormalf" ||
2380+
identifier == CPROVER_PREFIX "isnormald" ||
2381+
identifier == CPROVER_PREFIX "isnormalld" ||
2382+
identifier == "__builtin_isnormal")
23582383
{
23592384
if(expr.arguments().size()!=1)
23602385
{
23612386
err_location(f_op);
2362-
error() << "isnormal expects one operand" << eom;
2387+
error() << identifier << " expects one operand" << eom;
2388+
throw 0;
2389+
}
2390+
2391+
const exprt &fp_value = expr.arguments()[0];
2392+
2393+
if(fp_value.type().id() != ID_floatbv)
2394+
{
2395+
err_location(fp_value);
2396+
error() << "non-floating-point argument for " << identifier << eom;
23632397
throw 0;
23642398
}
23652399

23662400
isnormal_exprt isnormal_expr(expr.arguments().front());
23672401
isnormal_expr.add_source_location()=source_location;
23682402

2369-
return isnormal_expr;
2403+
return typecast_exprt::conditional_cast(isnormal_expr, expr.type());
23702404
}
23712405
else if(identifier==CPROVER_PREFIX "signf" ||
23722406
identifier==CPROVER_PREFIX "signd" ||
@@ -2378,14 +2412,14 @@ exprt c_typecheck_baset::do_special_functions(
23782412
if(expr.arguments().size()!=1)
23792413
{
23802414
err_location(f_op);
2381-
error() << "sign expects one operand" << eom;
2415+
error() << identifier << " expects one operand" << eom;
23822416
throw 0;
23832417
}
23842418

23852419
sign_exprt sign_expr(expr.arguments().front());
23862420
sign_expr.add_source_location()=source_location;
23872421

2388-
return sign_expr;
2422+
return typecast_exprt::conditional_cast(sign_expr, expr.type());
23892423
}
23902424
else if(identifier=="__builtin_popcount" ||
23912425
identifier=="__builtin_popcountl" ||

‎src/util/std_expr.h‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2111,6 +2111,15 @@ class typecast_exprt:public unary_exprt
21112111
unary_exprt(ID_typecast, op, _type)
21122112
{
21132113
}
2114+
2115+
// returns a typecast if the type doesn't already match
2116+
static exprt conditional_cast(const exprt &expr, const typet &type)
2117+
{
2118+
if(expr.type() == type)
2119+
return expr;
2120+
else
2121+
return typecast_exprt(expr, type);
2122+
}
21142123
};
21152124

21162125
/*! \brief Cast a generic exprt to a \ref typecast_exprt

0 commit comments

Comments
 (0)