1 /* Declarations for the Floating_Point_Expression class and its constituents. 2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it> 3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com) 4 5 This file is part of the Parma Polyhedra Library (PPL). 6 7 The PPL is free software; you can redistribute it and/or modify it 8 under the terms of the GNU General Public License as published by the 9 Free Software Foundation; either version 3 of the License, or (at your 10 option) any later version. 11 12 The PPL is distributed in the hope that it will be useful, but WITHOUT 13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 15 for more details. 16 17 You should have received a copy of the GNU General Public License 18 along with this program; if not, write to the Free Software Foundation, 19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. 20 21 For the most up-to-date information see the Parma Polyhedra Library 22 site: http://bugseng.com/products/ppl/ . */ 23 24 #ifndef PPL_Floating_Point_Expression_defs_hh 25 #define PPL_Floating_Point_Expression_defs_hh 1 26 27 #include "Floating_Point_Expression_types.hh" 28 #include "globals_defs.hh" 29 #include "Linear_Form_types.hh" 30 #include "Box_types.hh" 31 #include <cmath> 32 #include <map> 33 34 namespace Parma_Polyhedra_Library { 35 36 /*! \ingroup PPL_CXX_Interface \brief 37 A floating point expression on a given format. 38 39 This class represents a concrete <EM>floating point expression</EM>. This 40 includes constants, floating point variables, binary and unary 41 arithmetic operators. 42 43 \par Template type parameters 44 45 - The class template type parameter \p FP_Interval_Type represents the type 46 of the intervals used in the abstract domain. The interval bounds 47 should have a floating point type. 48 - The class template type parameter \p FP_Format represents the floating 49 point format used in the concrete domain. 50 This parameter must be a struct similar to the ones defined in file 51 Float_defs.hh, even though it is sufficient to define the three 52 fields BASE, MANTISSA_BITS and EXPONENT_BIAS. 53 */ 54 template <typename FP_Interval_Type, typename FP_Format> 55 class Floating_Point_Expression { 56 57 public: 58 59 //! Alias for a linear form with template argument \p FP_Interval_Type. 60 typedef Linear_Form<FP_Interval_Type> FP_Linear_Form; 61 62 //! Alias for a map that associates a variable index to an interval. 63 /*! \brief 64 Alias for a Box storing lower and upper bounds for floating point 65 variables. 66 67 The type a linear form abstract store associating each variable with an 68 interval that correctly approximates its value. 69 */ 70 typedef Box<FP_Interval_Type> FP_Interval_Abstract_Store; 71 72 //! Alias for a map that associates a variable index to a linear form. 73 /*! 74 The type a linear form abstract store associating each variable with a 75 linear form that correctly approximates its value. 76 */ 77 typedef std::map<dimension_type, FP_Linear_Form> 78 FP_Linear_Form_Abstract_Store; 79 80 //! The floating point format used by the analyzer. 81 typedef typename FP_Interval_Type::boundary_type boundary_type; 82 83 //! The interval policy used by \p FP_Interval_Type. 84 typedef typename FP_Interval_Type::info_type info_type; 85 86 //! Destructor. 87 virtual ~Floating_Point_Expression(); 88 89 //! Linearizes a floating point expression. 90 /*! \brief 91 Makes \p result become a linear form that correctly approximates the 92 value of the floating point expression in the given composite 93 abstract store. 94 95 \param int_store The interval abstract store. 96 \param lf_store The linear form abstract store. 97 \param result Becomes the linearized expression. 98 99 \return <CODE>true</CODE> if the linearization succeeded, 100 <CODE>false</CODE> otherwise. 101 102 Formally, if \p *this represents the expression \f$e\f$, 103 \p int_store represents the interval abstract store \f$\rho^{\#}\f$ and 104 \p lf_store represents the linear form abstract store \f$\rho^{\#}_l\f$, 105 then \p result will become 106 \f$\linexprenv{e}{\rho^{\#}}{\rho^{\#}_l}\f$ 107 if the linearization succeeds. 108 109 All variables occurring in the floating point expression MUST have 110 an associated interval in \p int_store. 111 If this precondition is not met, calling the method causes an 112 undefined behavior. 113 */ 114 virtual bool linearize(const FP_Interval_Abstract_Store& int_store, 115 const FP_Linear_Form_Abstract_Store& lf_store, 116 FP_Linear_Form& result) const = 0; 117 118 /*! \brief 119 Absolute error. 120 121 Represents the interval \f$[-\omega, \omega]\f$ where \f$\omega\f$ is the 122 smallest non-zero positive number in the less precise floating point 123 format between the analyzer format and the analyzed format. 124 125 */ 126 static FP_Interval_Type absolute_error; 127 128 // FIXME: this may not be the best place for them. 129 /*! \brief 130 Verifies if a given linear form overflows. 131 \param lf The linear form to verify. 132 \return 133 Returns <CODE>false</CODE> if all coefficients in \p lf are bounded, 134 <CODE>true</CODE> otherwise. 135 */ 136 static bool overflows(const FP_Linear_Form& lf); 137 138 /*! \brief 139 Computes the relative error of a given linear form. 140 141 Static helper method that is used by <CODE>linearize</CODE> 142 to account for the relative errors on \p lf. 143 \param lf The linear form used to compute the relative error. 144 \param result Becomes the linear form corresponding to a relative 145 error committed on \p lf. 146 147 This method makes <CODE>result</CODE> become a linear form 148 obtained by evaluating the function \f$\varepsilon_{\mathbf{f}}(l)\f$ 149 on the linear form \p lf. This function is defined 150 such as: 151 \f[ 152 \varepsilon_{\mathbf{f}}\left([a, b]+\sum_{v \in \cV}[a_{v}, b_{v}]v\right) 153 \defeq 154 (\textrm{max}(|a|, |b|) \amifp [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}]) 155 + 156 \sum_{v \in \cV}(\textrm{max}(|a_{v}|,|b_{v}|) 157 \amifp 158 [-\beta^{-\textrm{p}}, \beta^{-\textrm{p}}])v 159 \f] 160 where p is the fraction size in bits for the format \f$\mathbf{f}\f$ and 161 \f$\beta\f$ the base. 162 */ 163 static void relative_error(const FP_Linear_Form& lf, 164 FP_Linear_Form& result); 165 166 /*! \brief 167 Makes \p result become an interval that overapproximates all the 168 possible values of \p lf in the interval abstract store \p store. 169 170 \param lf The linear form to aproximate. 171 \param store The abstract store. 172 \param result The linear form that will be modified. 173 174 This method makes <CODE>result</CODE> become 175 \f$\iota(lf)\rho^{\#}\f$, that is an interval defined as: 176 \f[ 177 \iota\left(i + \sum_{v \in \cV}i_{v}v\right)\rho^{\#} 178 \defeq 179 i \asifp \left(\bigoplus_{v \in \cV}{}^{\#}i_{v} \amifp 180 \rho^{\#}(v)\right) 181 \f] 182 */ 183 static void intervalize(const FP_Linear_Form& lf, 184 const FP_Interval_Abstract_Store& store, 185 FP_Interval_Type& result); 186 187 private: 188 189 /*! \brief 190 Computes the absolute error. 191 192 Static helper method that is used to compute the value of the public 193 static field <CODE>absolute_error</CODE>. 194 195 \return The interval \f$[-\omega, \omega]\f$ corresponding to the value 196 of <CODE>absolute_error</CODE> 197 */ 198 static FP_Interval_Type compute_absolute_error(); 199 200 }; // class Floating_Point_Expression 201 202 203 template <typename FP_Interval_Type, typename FP_Format> 204 FP_Interval_Type Floating_Point_Expression<FP_Interval_Type, FP_Format> 205 ::absolute_error = compute_absolute_error(); 206 207 } // namespace Parma_Polyhedra_Library 208 209 #include "Floating_Point_Expression_inlines.hh" 210 #include "Floating_Point_Expression_templates.hh" 211 212 #endif // !defined(PPL_Floating_Point_Expression_defs_hh) 213