From 61af0612fb0ddd711c6eed2a9b69b34d76242120 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 May 2018 15:11:14 +0100 Subject: [PATCH 1/5] added typecast_exprt::conditional_cast --- src/util/std_expr.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 5db74482034..8b9f2407cbb 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2111,6 +2111,15 @@ class typecast_exprt:public unary_exprt unary_exprt(ID_typecast, op, _type) { } + + // returns a typecast if the type doesn't already match + static exprt conditional_cast(const exprt &expr, const typet &type) + { + if(expr.type() == type) + return expr; + else + return typecast_exprt(expr, type); + } }; /*! \brief Cast a generic exprt to a \ref typecast_exprt From 87d467eb169c38df38c8f9557bdfe5634a7186c4 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 May 2018 14:42:32 +0100 Subject: [PATCH 2/5] fix return types of various __builtin_is* functions --- src/ansi-c/c_typecheck_expr.cpp | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index be086c56f4f..b6063c156a8 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2255,7 +2255,7 @@ exprt c_typecheck_baset::do_special_functions( isnan_exprt isnan_expr(expr.arguments().front()); isnan_expr.add_source_location()=source_location; - return isnan_expr; + return typecast_exprt::conditional_cast(isnan_expr, expr.type()); } else if(identifier==CPROVER_PREFIX "isfinitef" || identifier==CPROVER_PREFIX "isfinited" || @@ -2271,7 +2271,7 @@ exprt c_typecheck_baset::do_special_functions( isfinite_exprt isfinite_expr(expr.arguments().front()); isfinite_expr.add_source_location()=source_location; - return isfinite_expr; + return typecast_exprt::conditional_cast(isfinite_expr, expr.type()); } else if(identifier==CPROVER_PREFIX "inf" || identifier=="__builtin_inf") @@ -2343,14 +2343,14 @@ exprt c_typecheck_baset::do_special_functions( if(expr.arguments().size()!=1) { err_location(f_op); - error() << "isinf expects one operand" << eom; + error() << identifier << " expects one operand" << eom; throw 0; } isinf_exprt isinf_expr(expr.arguments().front()); isinf_expr.add_source_location()=source_location; - return isinf_expr; + return typecast_exprt::conditional_cast(isinf_expr, expr.type()); } else if(identifier==CPROVER_PREFIX "isnormalf" || identifier==CPROVER_PREFIX "isnormald" || @@ -2359,14 +2359,23 @@ exprt c_typecheck_baset::do_special_functions( if(expr.arguments().size()!=1) { err_location(f_op); - error() << "isnormal expects one operand" << eom; + error() << identifier << " expects one operand" << eom; + throw 0; + } + + const exprt &fp_value = expr.arguments()[0]; + + if(fp_value.type().id() != ID_floatbv) + { + err_location(fp_value); + error() << "non-floating-point argument for " << identifier << eom; throw 0; } isnormal_exprt isnormal_expr(expr.arguments().front()); isnormal_expr.add_source_location()=source_location; - return isnormal_expr; + return typecast_exprt::conditional_cast(isnormal_expr, expr.type()); } else if(identifier==CPROVER_PREFIX "signf" || identifier==CPROVER_PREFIX "signd" || @@ -2378,14 +2387,14 @@ exprt c_typecheck_baset::do_special_functions( if(expr.arguments().size()!=1) { err_location(f_op); - error() << "sign expects one operand" << eom; + error() << identifier << " expects one operand" << eom; throw 0; } sign_exprt sign_expr(expr.arguments().front()); sign_expr.add_source_location()=source_location; - return sign_expr; + return typecast_exprt::conditional_cast(sign_expr, expr.type()); } else if(identifier=="__builtin_popcount" || identifier=="__builtin_popcountl" || From 83aedddfdfc9027a71db461da5cc914a1d5964f1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 May 2018 14:43:54 +0100 Subject: [PATCH 3/5] added __builtin_isinf_sign --- src/ansi-c/c_typecheck_expr.cpp | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b6063c156a8..a80270ef486 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2352,6 +2352,30 @@ exprt c_typecheck_baset::do_special_functions( return typecast_exprt::conditional_cast(isinf_expr, expr.type()); } + else if(identifier == "__builtin_isinf_sign") + { + if(expr.arguments().size() != 1) + { + err_location(f_op); + error() << identifier << " expects one operand" << eom; + throw 0; + } + + // returns 1 for +inf and -1 for -inf, and 0 otherwise + + const exprt &fp_value = expr.arguments().front(); + + isinf_exprt isinf_expr(fp_value); + isinf_expr.add_source_location() = source_location; + + return if_exprt( + isinf_exprt(fp_value), + if_exprt( + sign_exprt(fp_value), + from_integer(-1, expr.type()), + from_integer(1, expr.type())), + from_integer(0, expr.type())); + } else if(identifier==CPROVER_PREFIX "isnormalf" || identifier==CPROVER_PREFIX "isnormald" || identifier==CPROVER_PREFIX "isnormalld") From a69c603922410e9113330cb7e8cf98d2cb0eca45 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 May 2018 14:42:54 +0100 Subject: [PATCH 4/5] add __builtin_isnormal --- src/ansi-c/c_typecheck_expr.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index a80270ef486..d31c7d242de 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2376,9 +2376,10 @@ exprt c_typecheck_baset::do_special_functions( from_integer(1, expr.type())), from_integer(0, expr.type())); } - else if(identifier==CPROVER_PREFIX "isnormalf" || - identifier==CPROVER_PREFIX "isnormald" || - identifier==CPROVER_PREFIX "isnormalld") + else if(identifier == CPROVER_PREFIX "isnormalf" || + identifier == CPROVER_PREFIX "isnormald" || + identifier == CPROVER_PREFIX "isnormalld" || + identifier == "__builtin_isnormal") { if(expr.arguments().size()!=1) { From 72a0379e8300f03eceb3fb1eb49c5b812fdc7662 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 May 2018 16:13:19 +0100 Subject: [PATCH 5/5] test __builtin_isinf, __builtin_isinf_sign, __builtin_isnormal --- regression/cbmc/Float_lib1/main.c | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/regression/cbmc/Float_lib1/main.c b/regression/cbmc/Float_lib1/main.c index 0db0db8363c..2ca1ed979f2 100644 --- a/regression/cbmc/Float_lib1/main.c +++ b/regression/cbmc/Float_lib1/main.c @@ -27,9 +27,27 @@ int main() { assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MIN/2)==3); assert(__builtin_fpclassify(0, 1, 2, 3, 4, -0.0)==4); + assert(__builtin_isinf(DBL_MAX+DBL_MAX)==1); + assert(__builtin_isinf(0.0)==0); + assert(__builtin_isinf(-(DBL_MAX+DBL_MAX))==1); + + assert(__builtin_isinf_sign(DBL_MAX+DBL_MAX)==1); + assert(__builtin_isinf_sign(0.0)==0); + assert(__builtin_isinf_sign(-(DBL_MAX+DBL_MAX))==-1); + // these are compile-time _Static_assert(__builtin_fpclassify(0, 1, 2, 3, 4, -0.0)==4, "__builtin_fpclassify is constant"); + + _Static_assert(__builtin_isnormal(DBL_MIN), + "__builtin_isnormal is constant"); + + _Static_assert(!__builtin_isinf(0), + "__builtin_isinf is constant"); + + _Static_assert(__builtin_isinf_sign(0)==0, + "__builtin_isinf_sign is constant"); + #endif assert(signbit(-1.0)!=0);