PPL  0.12.1
Float.inlines.hh
Go to the documentation of this file.
00001 /* IEC 559 floating point format related functions.
00002    Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
00003    Copyright (C) 2010-2012 BUGSENG srl (http://bugseng.com)
00004 
00005 This file is part of the Parma Polyhedra Library (PPL).
00006 
00007 The PPL is free software; you can redistribute it and/or modify it
00008 under the terms of the GNU General Public License as published by the
00009 Free Software Foundation; either version 3 of the License, or (at your
00010 option) any later version.
00011 
00012 The PPL is distributed in the hope that it will be useful, but WITHOUT
00013 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
00014 FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
00015 for more details.
00016 
00017 You should have received a copy of the GNU General Public License
00018 along with this program; if not, write to the Free Software Foundation,
00019 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
00020 
00021 For the most up-to-date information see the Parma Polyhedra Library
00022 site: http://bugseng.com/products/ppl/ . */
00023 
00024 #ifndef PPL_Float_inlines_hh
00025 #define PPL_Float_inlines_hh 1
00026 
00027 #include <climits>
00028 #include "Variable.defs.hh"
00029 #include "Linear_Form.defs.hh"
00030 
00031 namespace Parma_Polyhedra_Library {
00032 
00033 inline int
00034 float_ieee754_half::inf_sign() const {
00035   if (word == NEG_INF)
00036     return -1;
00037   if (word == POS_INF)
00038     return 1;
00039   return 0;
00040 }
00041 
00042 inline bool
00043 float_ieee754_half::is_nan() const {
00044   return (word & ~SGN_MASK) > POS_INF;
00045 }
00046 
00047 inline int
00048 float_ieee754_half::zero_sign() const {
00049   if (word == NEG_ZERO)
00050     return -1;
00051   if (word == POS_ZERO)
00052     return 1;
00053   return 0;
00054 }
00055 
00056 inline void
00057 float_ieee754_half::negate() {
00058   word ^= SGN_MASK;
00059 }
00060 
00061 inline bool
00062 float_ieee754_half::sign_bit() const {
00063   return (word & SGN_MASK) != 0;
00064 }
00065 
00066 inline void
00067 float_ieee754_half::dec() {
00068   --word;
00069 }
00070 
00071 inline void
00072 float_ieee754_half::inc() {
00073   ++word;
00074 }
00075 
00076 inline void
00077 float_ieee754_half::set_max(bool negative) {
00078   word = 0x7bffU;
00079   if (negative)
00080     word |= SGN_MASK;
00081 }
00082 
00083 inline void
00084 float_ieee754_half::build(bool negative, mpz_t mantissa, int exponent) {
00085   word = static_cast<uint16_t>(mpz_get_ui(mantissa)
00086                                & ((1UL << MANTISSA_BITS) - 1));
00087   if (negative)
00088     word |= SGN_MASK;
00089   int exponent_repr = exponent + EXPONENT_BIAS;
00090   PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
00091   word |= static_cast<uint16_t>(exponent_repr) << MANTISSA_BITS;
00092 }
00093 
00094 inline int
00095 float_ieee754_single::inf_sign() const {
00096   if (word == NEG_INF)
00097     return -1;
00098   if (word == POS_INF)
00099     return 1;
00100   return 0;
00101 }
00102 
00103 inline bool
00104 float_ieee754_single::is_nan() const {
00105   return (word & ~SGN_MASK) > POS_INF;
00106 }
00107 
00108 inline int
00109 float_ieee754_single::zero_sign() const {
00110   if (word == NEG_ZERO)
00111     return -1;
00112   if (word == POS_ZERO)
00113     return 1;
00114   return 0;
00115 }
00116 
00117 inline void
00118 float_ieee754_single::negate() {
00119   word ^= SGN_MASK;
00120 }
00121 
00122 inline bool
00123 float_ieee754_single::sign_bit() const {
00124   return (word & SGN_MASK) != 0;
00125 }
00126 
00127 inline void
00128 float_ieee754_single::dec() {
00129   --word;
00130 }
00131 
00132 inline void
00133 float_ieee754_single::inc() {
00134   ++word;
00135 }
00136 
00137 inline void
00138 float_ieee754_single::set_max(bool negative) {
00139   word = 0x7f7fffffU;
00140   if (negative)
00141     word |= SGN_MASK;
00142 }
00143 
00144 inline void
00145 float_ieee754_single::build(bool negative, mpz_t mantissa, int exponent) {
00146   word = static_cast<uint32_t>(mpz_get_ui(mantissa)
00147                                & ((1UL << MANTISSA_BITS) - 1));
00148   if (negative)
00149     word |= SGN_MASK;
00150   int exponent_repr = exponent + EXPONENT_BIAS;
00151   PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
00152   word |= static_cast<uint32_t>(exponent_repr) << MANTISSA_BITS;
00153 }
00154 
00155 inline int
00156 float_ieee754_double::inf_sign() const {
00157   if (lsp != LSP_INF)
00158     return 0;
00159   if (msp == MSP_NEG_INF)
00160     return -1;
00161   if (msp == MSP_POS_INF)
00162     return 1;
00163   return 0;
00164 }
00165 
00166 inline bool
00167 float_ieee754_double::is_nan() const {
00168   uint32_t a = msp & ~MSP_SGN_MASK;
00169   return a > MSP_POS_INF || (a == MSP_POS_INF && lsp != LSP_INF);
00170 }
00171 
00172 inline int
00173 float_ieee754_double::zero_sign() const {
00174   if (lsp != LSP_ZERO)
00175     return 0;
00176   if (msp == MSP_NEG_ZERO)
00177     return -1;
00178   if (msp == MSP_POS_ZERO)
00179     return 1;
00180   return 0;
00181 }
00182 
00183 inline void
00184 float_ieee754_double::negate() {
00185   msp ^= MSP_SGN_MASK;
00186 }
00187 
00188 inline bool
00189 float_ieee754_double::sign_bit() const {
00190   return (msp & MSP_SGN_MASK) != 0;
00191 }
00192 
00193 inline void
00194 float_ieee754_double::dec() {
00195   if (lsp == 0) {
00196     --msp;
00197     lsp = LSP_MAX;
00198   }
00199   else
00200     --lsp;
00201 }
00202 
00203 inline void
00204 float_ieee754_double::inc() {
00205   if (lsp == LSP_MAX) {
00206     ++msp;
00207     lsp = 0;
00208   }
00209   else
00210     ++lsp;
00211 }
00212 
00213 inline void
00214 float_ieee754_double::set_max(bool negative) {
00215   msp = 0x7fefffffU;
00216   lsp = 0xffffffffU;
00217   if (negative)
00218     msp |= MSP_SGN_MASK;
00219 }
00220 
00221 inline void
00222 float_ieee754_double::build(bool negative, mpz_t mantissa, int exponent) {
00223   unsigned long m;
00224 #if ULONG_MAX == 0xffffffffUL
00225   lsp = mpz_get_ui(mantissa);
00226   mpz_tdiv_q_2exp(mantissa, mantissa, 32);
00227   m = mpz_get_ui(mantissa);
00228 #else
00229   m = mpz_get_ui(mantissa);
00230   lsp = static_cast<uint32_t>(m & LSP_MAX);
00231   m >>= 32;
00232 #endif
00233   msp = static_cast<uint32_t>(m & ((1UL << (MANTISSA_BITS - 32)) - 1));
00234   if (negative)
00235     msp |= MSP_SGN_MASK;
00236   int exponent_repr = exponent + EXPONENT_BIAS;
00237   PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
00238   msp |= static_cast<uint32_t>(exponent_repr) << (MANTISSA_BITS - 32);
00239 }
00240 
00241 inline int
00242 float_ibm_single::inf_sign() const {
00243   if (word == NEG_INF)
00244     return -1;
00245   if (word == POS_INF)
00246     return 1;
00247   return 0;
00248 }
00249 
00250 inline bool
00251 float_ibm_single::is_nan() const {
00252   return (word & ~SGN_MASK) > POS_INF;
00253 }
00254 
00255 inline int
00256 float_ibm_single::zero_sign() const {
00257   if (word == NEG_ZERO)
00258     return -1;
00259   if (word == POS_ZERO)
00260     return 1;
00261   return 0;
00262 }
00263 
00264 inline void
00265 float_ibm_single::negate() {
00266   word ^= SGN_MASK;
00267 }
00268 
00269 inline bool
00270 float_ibm_single::sign_bit() const {
00271   return (word & SGN_MASK) != 0;
00272 }
00273 
00274 inline void
00275 float_ibm_single::dec() {
00276   --word;
00277 }
00278 
00279 inline void
00280 float_ibm_single::inc() {
00281   ++word;
00282 }
00283 
00284 inline void
00285 float_ibm_single::set_max(bool negative) {
00286   word = 0x7f000000U;
00287   if (negative)
00288     word |= SGN_MASK;
00289 }
00290 
00291 inline void
00292 float_ibm_single::build(bool negative, mpz_t mantissa, int exponent) {
00293   word = static_cast<uint32_t>(mpz_get_ui(mantissa)
00294                                & ((1UL << MANTISSA_BITS) - 1));
00295   if (negative)
00296     word |= SGN_MASK;
00297   int exponent_repr = exponent + EXPONENT_BIAS;
00298   PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
00299   word |= static_cast<uint32_t>(exponent_repr) << MANTISSA_BITS;
00300 }
00301 
00302 inline int
00303 float_intel_double_extended::inf_sign() const {
00304   if (lsp != LSP_INF)
00305     return 0;
00306   uint32_t a = msp & MSP_NEG_INF;
00307   if (a == MSP_NEG_INF)
00308     return -1;
00309   if (a == MSP_POS_INF)
00310     return 1;
00311   return 0;
00312 }
00313 
00314 inline bool
00315 float_intel_double_extended::is_nan() const {
00316   return (msp & MSP_POS_INF) == MSP_POS_INF
00317     && lsp != LSP_INF;
00318 }
00319 
00320 inline int
00321 float_intel_double_extended::zero_sign() const {
00322   if (lsp != LSP_ZERO)
00323     return 0;
00324   uint32_t a = msp & MSP_NEG_INF;
00325   if (a == MSP_NEG_ZERO)
00326     return -1;
00327   if (a == MSP_POS_ZERO)
00328     return 1;
00329   return 0;
00330 }
00331 
00332 inline void
00333 float_intel_double_extended::negate() {
00334   msp ^= MSP_SGN_MASK;
00335 }
00336 
00337 inline bool
00338 float_intel_double_extended::sign_bit() const {
00339   return (msp & MSP_SGN_MASK) != 0;
00340 }
00341 
00342 inline void
00343 float_intel_double_extended::dec() {
00344   if ((lsp & LSP_DMAX) == 0) {
00345     --msp;
00346     lsp = ((msp & MSP_NEG_INF) == 0) ? LSP_DMAX : LSP_NMAX;
00347   }
00348   else
00349     --lsp;
00350 }
00351 
00352 inline void
00353 float_intel_double_extended::inc() {
00354   if ((lsp & LSP_DMAX) == LSP_DMAX) {
00355     ++msp;
00356     lsp = LSP_DMAX + 1;
00357   }
00358   else
00359     ++lsp;
00360 }
00361 
00362 inline void
00363 float_intel_double_extended::set_max(bool negative) {
00364   msp = 0x00007ffeU;
00365   lsp = static_cast<uint64_t>(0xffffffffffffffffULL);
00366   if (negative)
00367     msp |= MSP_SGN_MASK;
00368 }
00369 
00370 inline void
00371 float_intel_double_extended::build(bool negative,
00372                                    mpz_t mantissa, int exponent) {
00373 #if ULONG_MAX == 0xffffffffUL
00374   mpz_export(&lsp, 0, -1, 8, 0, 0, mantissa);
00375 #else
00376   lsp = mpz_get_ui(mantissa);
00377 #endif
00378   msp = (negative ? MSP_SGN_MASK : 0);
00379   int exponent_repr = exponent + EXPONENT_BIAS;
00380   PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
00381   msp |= static_cast<uint32_t>(exponent_repr);
00382 }
00383 
00384 inline int
00385 float_ieee754_quad::inf_sign() const {
00386   if (lsp != LSP_INF)
00387     return 0;
00388   if (msp == MSP_NEG_INF)
00389     return -1;
00390   if (msp == MSP_POS_INF)
00391     return 1;
00392   return 0;
00393 }
00394 
00395 inline bool
00396 float_ieee754_quad::is_nan() const {
00397   return (msp & ~MSP_SGN_MASK) == MSP_POS_INF
00398     && lsp != LSP_INF;
00399 }
00400 
00401 inline int
00402 float_ieee754_quad::zero_sign() const {
00403   if (lsp != LSP_ZERO)
00404     return 0;
00405   if (msp == MSP_NEG_ZERO)
00406     return -1;
00407   if (msp == MSP_POS_ZERO)
00408     return 1;
00409   return 0;
00410 }
00411 
00412 inline void
00413 float_ieee754_quad::negate() {
00414   msp ^= MSP_SGN_MASK;
00415 }
00416 
00417 inline bool
00418 float_ieee754_quad::sign_bit() const {
00419   return (msp & MSP_SGN_MASK) != 0;
00420 }
00421 
00422 inline void
00423 float_ieee754_quad::dec() {
00424   if (lsp == 0) {
00425     --msp;
00426     lsp = LSP_MAX;
00427   }
00428   else
00429     --lsp;
00430 }
00431 
00432 inline void
00433 float_ieee754_quad::inc() {
00434   if (lsp == LSP_MAX) {
00435     ++msp;
00436     lsp = 0;
00437   }
00438   else
00439     ++lsp;
00440 }
00441 
00442 inline void
00443 float_ieee754_quad::set_max(bool negative) {
00444   msp = static_cast<uint64_t>(0x7ffeffffffffffffULL);
00445   lsp = static_cast<uint64_t>(0xffffffffffffffffULL);
00446   if (negative)
00447     msp |= MSP_SGN_MASK;
00448 }
00449 
00450 inline void
00451 float_ieee754_quad::build(bool negative, mpz_t mantissa, int exponent) {
00452   uint64_t parts[2];
00453   mpz_export(parts, 0, -1, 8, 0, 0, mantissa);
00454   lsp = parts[0];
00455   msp = parts[1];
00456   msp &= ((static_cast<uint64_t>(1) << (MANTISSA_BITS - 64)) - 1);
00457   if (negative)
00458     msp |= MSP_SGN_MASK;
00459   int exponent_repr = exponent + EXPONENT_BIAS;
00460   PPL_ASSERT(exponent_repr >= 0 && exponent_repr < (1 << EXPONENT_BITS));
00461   msp |= static_cast<uint64_t>(exponent_repr) << (MANTISSA_BITS - 64);
00462 }
00463 
00464 inline bool
00465 is_less_precise_than(Floating_Point_Format f1, Floating_Point_Format f2) {
00466   return f1 < f2;
00467 }
00468 
00469 inline unsigned int
00470 msb_position(unsigned long long v) {
00471   return static_cast<unsigned int>(sizeof_to_bits(sizeof(v))) - 1U - clz(v);
00472 }
00473 
00474 template <typename FP_Interval_Type>
00475 inline void
00476 affine_form_image(std::map<dimension_type,
00477                            Linear_Form<FP_Interval_Type> >& lf_store,
00478                   const Variable var,
00479                   const Linear_Form<FP_Interval_Type>& lf) {
00480   // Assign the new linear form for var.
00481   lf_store[var.id()] = lf;
00482   // Now invalidate all linear forms in which var occurs.
00483   discard_occurrences(lf_store, var);
00484 }
00485 
00486 #if PPL_SUPPORTED_FLOAT
00487 inline
00488 Float<float>::Float() {
00489 }
00490 
00491 inline
00492 Float<float>::Float(float v) {
00493   u.number = v;
00494 }
00495 
00496 inline float
00497 Float<float>::value() {
00498   return u.number;
00499 }
00500 #endif
00501 
00502 #if PPL_SUPPORTED_DOUBLE
00503 inline
00504 Float<double>::Float() {
00505 }
00506 
00507 inline
00508 Float<double>::Float(double v) {
00509   u.number = v;
00510 }
00511 
00512 inline double
00513 Float<double>::value() {
00514   return u.number;
00515 }
00516 #endif
00517 
00518 #if PPL_SUPPORTED_LONG_DOUBLE
00519 inline
00520 Float<long double>::Float() {
00521 }
00522 
00523 inline
00524 Float<long double>::Float(long double v) {
00525   u.number = v;
00526 }
00527 
00528 inline long double
00529 Float<long double>::value() {
00530   return u.number;
00531 }
00532 #endif
00533 
00534 } // namespace Parma_Polyhedra_Library
00535 
00536 #endif // !defined(PPL_Float_inlines_hh)