Skip to content

add support for __builtin_fpclassify #2218

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
May 22, 2018
Merged

add support for __builtin_fpclassify #2218

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
52595bd
add support for __builtin_fpclassify
May 22, 2018
c3603e3
added a test for raw __builtin_fpclassify
May 22, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 45 additions & 0 deletions src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2195,6 +2195,51 @@ exprt c_typecheck_baset::do_special_functions(

return bswap_expr;
}
else if(
identifier == "__builtin_fpclassify" ||
identifier == CPROVER_PREFIX "fpclassify")
{
if(expr.arguments().size() != 6)
{
err_location(f_op);
error() << identifier << " expects six arguments" << eom;
throw 0;
}

// This gets 5 integers followed by a float or double.
// The five integers are the return values for the cases
// FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL and FP_ZERO.
// gcc expects this to be able to produce compile-time constants.

const exprt &fp_value = expr.arguments()[5];

if(fp_value.type().id() != ID_floatbv)
{
err_location(fp_value);
error() << "non-floating-point argument for " << identifier << eom;
throw 0;
}

const auto &floatbv_type = to_floatbv_type(fp_value.type());

const exprt zero = ieee_floatt::zero(floatbv_type).to_expr();

const auto &arguments = expr.arguments();

return if_exprt(
isnan_exprt(fp_value),
arguments[0],
if_exprt(
isinf_exprt(fp_value),
arguments[1],
if_exprt(
isnormal_exprt(fp_value),
arguments[2],
if_exprt(
ieee_float_equal_exprt(fp_value, zero),
arguments[4],
arguments[3])))); // subnormal
}
else if(identifier==CPROVER_PREFIX "isnanf" ||
identifier==CPROVER_PREFIX "isnand" ||
identifier==CPROVER_PREFIX "isnanld" ||
Expand Down
1 change: 1 addition & 0 deletions src/ansi-c/cprover_builtin_headers.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);
void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);

// float stuff
int __CPROVER_fpclassify(int, int, int, int, int, ...);
__CPROVER_bool __CPROVER_isnanf(float f);
__CPROVER_bool __CPROVER_isnand(double f);
__CPROVER_bool __CPROVER_isnanld(long double f);
Expand Down
1 change: 1 addition & 0 deletions src/ansi-c/library/cprover.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_
#endif

// float stuff
int __CPROVER_fpclassify(int, int, int, int, int, ...);
__CPROVER_bool __CPROVER_isfinite(double f);
__CPROVER_bool __CPROVER_isinf(double f);
__CPROVER_bool __CPROVER_isnormal(double f);
Expand Down
35 changes: 10 additions & 25 deletions src/ansi-c/library/math.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -287,11 +287,8 @@ inline short _fdclass(float f) {

inline int __fpclassifyd(double d) {
__CPROVER_HIDE:
return __CPROVER_isnand(d)?FP_NAN:
__CPROVER_isinfd(d)?FP_INFINITE:
d==0?FP_ZERO:
__CPROVER_isnormald(d)?FP_NORMAL:
FP_SUBNORMAL;
return __CPROVER_fpclassify(
FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
}

/* FUNCTION: __fpclassifyf */
Expand All @@ -303,11 +300,8 @@ inline int __fpclassifyd(double d) {

inline int __fpclassifyf(float f) {
__CPROVER_HIDE:
return __CPROVER_isnanf(f)?FP_NAN:
__CPROVER_isinff(f)?FP_INFINITE:
f==0?FP_ZERO:
__CPROVER_isnormalf(f)?FP_NORMAL:
FP_SUBNORMAL;
return __CPROVER_fpclassify(
FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f);
}

/* FUNCTION: __fpclassifyl */
Expand All @@ -319,11 +313,8 @@ inline int __fpclassifyf(float f) {

inline int __fpclassifyl(long double f) {
__CPROVER_HIDE:
return __CPROVER_isnanld(f)?FP_NAN:
__CPROVER_isinfld(f)?FP_INFINITE:
f==0?FP_ZERO:
__CPROVER_isnormalld(f)?FP_NORMAL:
FP_SUBNORMAL;
return __CPROVER_fpclassify(
FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f);
}

/* FUNCTION: __fpclassify */
Expand All @@ -339,20 +330,14 @@ inline int __fpclassifyl(long double f) {
#ifdef __APPLE__
inline int __fpclassify(long double d) {
__CPROVER_HIDE:
return __CPROVER_isnanld(d)?FP_NAN:
__CPROVER_isinfld(d)?FP_INFINITE:
d==0?FP_ZERO:
__CPROVER_isnormalld(d)?FP_NORMAL:
FP_SUBNORMAL;
return __CPROVER_fpclassify(
FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
}
#else
inline int __fpclassify(double d) {
__CPROVER_HIDE:
return __CPROVER_isnand(d)?FP_NAN:
__CPROVER_isinfd(d)?FP_INFINITE:
d==0?FP_ZERO:
__CPROVER_isnormald(d)?FP_NORMAL:
FP_SUBNORMAL;
return __CPROVER_fpclassify(
FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d);
}
#endif

Expand Down