ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
libm.h
Go to the documentation of this file.
1#ifndef _LIBM_H
2#define _LIBM_H
3
4#include <stdint.h>
5#include <float.h>
6#include <math.h>
7#include "endian.h"
8//#include "fp_arch.h"
9
10#if LDBL_MANT_DIG == 53 && LDBL_MAX_EXP == 1024
11#elif LDBL_MANT_DIG == 64 && LDBL_MAX_EXP == 16384 && __BYTE_ORDER == __LITTLE_ENDIAN
12union ldshape {
13 long double f;
14 struct {
15 uint64_t m;
16 uint16_t se;
17 } i;
18};
19#elif LDBL_MANT_DIG == 64 && LDBL_MAX_EXP == 16384 && __BYTE_ORDER == __BIG_ENDIAN
20/* This is the m68k variant of 80-bit long double, and this definition only works
21 * on archs where the alignment requirement of uint64_t is <= 4. */
22union ldshape {
23 long double f;
24 struct {
25 uint16_t se;
26 uint16_t pad;
27 uint64_t m;
28 } i;
29};
30#elif LDBL_MANT_DIG == 113 && LDBL_MAX_EXP == 16384 && __BYTE_ORDER == __LITTLE_ENDIAN
31union ldshape {
32 long double f;
33 struct {
34 uint64_t lo;
35 uint32_t mid;
36 uint16_t top;
37 uint16_t se;
38 } i;
39 struct {
40 uint64_t lo;
41 uint64_t hi;
42 } i2;
43};
44#elif LDBL_MANT_DIG == 113 && LDBL_MAX_EXP == 16384 && __BYTE_ORDER == __BIG_ENDIAN
45union ldshape {
46 long double f;
47 struct {
48 uint16_t se;
49 uint16_t top;
50 uint32_t mid;
51 uint64_t lo;
52 } i;
53 struct {
54 uint64_t hi;
55 uint64_t lo;
56 } i2;
57};
58#else
59#error Unsupported long double representation
60#endif
61
62/* Support non-nearest rounding mode. */
63#define WANT_ROUNDING 1
64/* Support signaling NaNs. */
65#define WANT_SNAN 0
66
67#if WANT_SNAN
68#error SNaN is unsupported
69#else
70#define issignalingf_inline(x) 0
71#define issignaling_inline(x) 0
72#endif
73
74#ifndef TOINT_INTRINSICS
75#define TOINT_INTRINSICS 0
76#endif
77
78#if TOINT_INTRINSICS
79/* Round x to nearest int in all rounding modes, ties have to be rounded
80 consistently with converttoint so the results match. If the result
81 would be outside of [-2^31, 2^31-1] then the semantics is unspecified. */
82static double_t roundtoint(double_t);
83
84/* Convert x to nearest int in all rounding modes, ties have to be rounded
85 consistently with roundtoint. If the result is not representible in an
86 int32_t then the semantics is unspecified. */
87static int32_t converttoint(double_t);
88#endif
89
90/* Helps static branch prediction so hot path can be better optimized. */
91#ifdef __GNUC__
92#define predict_true(x) __builtin_expect(!!(x), 1)
93#define predict_false(x) __builtin_expect(x, 0)
94#else
95#define predict_true(x) (x)
96#define predict_false(x) (x)
97#endif
98
99/* Evaluate an expression as the specified type. With standard excess
100 precision handling a type cast or assignment is enough (with
101 -ffloat-store an assignment is required, in old compilers argument
102 passing and return statement may not drop excess precision). */
103
104static inline float eval_as_float(float x)
105{
106 float y = x;
107 return y;
108}
109
110static inline double eval_as_double(double x)
111{
112 double y = x;
113 return y;
114}
115
116/* fp_barrier returns its input, but limits code transformations
117 as if it had a side-effect (e.g. observable io) and returned
118 an arbitrary value. */
119
120#ifndef fp_barrierf
121#define fp_barrierf fp_barrierf
122static inline float fp_barrierf(float x)
123{
124 volatile float y = x;
125 return y;
126}
127#endif
128
129#ifndef fp_barrier
130#define fp_barrier fp_barrier
131static inline double fp_barrier(double x)
132{
133 volatile double y = x;
134 return y;
135}
136#endif
137
138#ifndef fp_barrierl
139#define fp_barrierl fp_barrierl
140static inline long double fp_barrierl(long double x)
141{
142 volatile long double y = x;
143 return y;
144}
145#endif
146
147/* fp_force_eval ensures that the input value is computed when that's
148 otherwise unused. To prevent the constant folding of the input
149 expression, an additional fp_barrier may be needed or a compilation
150 mode that does so (e.g. -frounding-math in gcc). Then it can be
151 used to evaluate an expression for its fenv side-effects only. */
152
153/*
154 * Edoardo Manino: the three functions fp_force_evalf(),
155 * fp_force_eval() and fp_force_evall() throw an "unused variable"
156 * compiler warning due to variable y. I have added a hack to suppress
157 * the warning, as explained at the following link:
158 * https://stackoverflow.com/questions/1486904/how-do-i-best-silence-a-warning-about-unused-variables
159 */
160#define _UNUSED(expr) do { (void)(expr); } while (0)
161
162#ifndef fp_force_evalf
163#define fp_force_evalf fp_force_evalf
164static inline void fp_force_evalf(float x)
165{
166 volatile float y;
167 y = x;
168 _UNUSED(y); // avoid an "unused variable" compiler warning
169}
170#endif
171
172#ifndef fp_force_eval
173#define fp_force_eval fp_force_eval
174static inline void fp_force_eval(double x)
175{
176 volatile double y;
177 y = x;
178 _UNUSED(y); // avoid an "unused variable" compiler warning
179}
180#endif
181
182#ifndef fp_force_evall
183#define fp_force_evall fp_force_evall
184static inline void fp_force_evall(long double x)
185{
186 volatile long double y;
187 y = x;
188 _UNUSED(y); // avoid an "unused variable" compiler warning
189}
190#endif
191
192#define FORCE_EVAL(x) do { \
193 if (sizeof(x) == sizeof(float)) { \
194 fp_force_evalf(x); \
195 } else if (sizeof(x) == sizeof(double)) { \
196 fp_force_eval(x); \
197 } else { \
198 fp_force_evall(x); \
199 } \
200} while(0)
201
202#define asuint(f) ((union{float _f; uint32_t _i;}){f})._i
203#define asfloat(i) ((union{uint32_t _i; float _f;}){i})._f
204#define asuint64(f) ((union{double _f; uint64_t _i;}){f})._i
205#define asdouble(i) ((union{uint64_t _i; double _f;}){i})._f
206
207#define EXTRACT_WORDS(hi,lo,d) \
208do { \
209 uint64_t __u = asuint64(d); \
210 (hi) = __u >> 32; \
211 (lo) = (uint32_t)__u; \
212} while (0)
213
214#define GET_HIGH_WORD(hi,d) \
215do { \
216 (hi) = asuint64(d) >> 32; \
217} while (0)
218
219#define GET_LOW_WORD(lo,d) \
220do { \
221 (lo) = (uint32_t)asuint64(d); \
222} while (0)
223
224#define INSERT_WORDS(d,hi,lo) \
225do { \
226 (d) = asdouble(((uint64_t)(hi)<<32) | (uint32_t)(lo)); \
227} while (0)
228
229#define SET_HIGH_WORD(d,hi) \
230 INSERT_WORDS(d, hi, (uint32_t)asuint64(d))
231
232#define SET_LOW_WORD(d,lo) \
233 INSERT_WORDS(d, asuint64(d)>>32, lo)
234
235#define GET_FLOAT_WORD(w,d) \
236do { \
237 (w) = asuint(d); \
238} while (0)
239
240#define SET_FLOAT_WORD(d,w) \
241do { \
242 (d) = asfloat(w); \
243} while (0)
244
245int __rem_pio2_large(double*,double*,int,int,int);
246
247int __rem_pio2(double,double*);
248double __k_sin(double,double,int); // renamed: __sin() is a vector function in math.h
249double __k_cos(double,double); // renamed: __cos() is a vector function in math.h
250double __k_tan(double,double,int); // renamed: __tan() is a vector function in math.h
251double __expo2(double,double);
252
253int __rem_pio2f(float,double*);
254float __k_sindf(double); // renamed for consistency with double and long double
255float __k_cosdf(double); // renamed for consistency with double and long double
256float __k_tandf(double,int); // renamed for consistency with double and long double
257float __expo2f(float,float);
258
259int __rem_pio2l(long double, long double *);
260long double __k_sinl(long double, long double, int); // renamed: __sinl() is a vector function in math.h
261long double __k_cosl(long double, long double); // renamed: __cosl() is a vector function in math.h
262long double __k_tanl(long double, long double, int); // renamed: __tanl() is a vector function in math.h
263
264long double __polevll(long double, const long double *, int);
265long double __p1evll(long double, const long double *, int);
266
267extern int __signgam;
268double __lgamma_r(double, int *);
269float __lgammaf_r(float, int *);
270
271/* error handling functions */
272float __math_xflowf(uint32_t, float);
273float __math_uflowf(uint32_t);
274float __math_oflowf(uint32_t);
275float __math_divzerof(uint32_t);
276float __math_invalidf(float);
277double __math_xflow(uint32_t, double);
278double __math_uflow(uint32_t);
279double __math_oflow(uint32_t);
280double __math_divzero(uint32_t);
281double __math_invalid(double);
282#if LDBL_MANT_DIG != DBL_MANT_DIG
283long double __math_invalidl(long double);
284#endif
285
286/*
287 * Edoardo Manino: extra functions they may not be in math.h
288 */
289
290double j0(double x);
291double j1(double x);
292double y0(double x);
293double y1(double x);
294
295float j0f(float x);
296float y0f(float x);
297float j1f(float x);
298float y1f(float x);
299
300#endif
#define fp_force_evall
Definition libm.h:183
float __k_tandf(double, int)
float __math_divzerof(uint32_t)
Definition __math_divzerof.c:3
float __expo2f(float, float)
int __rem_pio2_large(double *, double *, int, int, int)
Definition __rem_pio2_large.c:273
int __rem_pio2f(float, double *)
Definition __rem_pio2f.c:43
double y1(double x)
#define fp_barrier
Definition libm.h:130
double __k_sin(double, double, int)
float j1f(float x)
float __math_invalidf(float)
Definition __math_invalidf.c:3
static double eval_as_double(double x)
Definition libm.h:110
double __math_uflow(uint32_t)
Definition __math_uflow.c:3
double __k_cos(double, double)
long double __k_sinl(long double, long double, int)
float __math_xflowf(uint32_t, float)
Definition __math_xflowf.c:3
float y1f(float x)
double __math_xflow(uint32_t, double)
Definition __math_xflow.c:3
float __math_oflowf(uint32_t)
Definition __math_oflowf.c:3
float __k_sindf(double)
Definition __sindf.c:30
#define fp_force_evalf
Definition libm.h:163
double __math_divzero(uint32_t)
Definition __math_divzero.c:3
double __k_tan(double, double, int)
int __rem_pio2l(long double, long double *)
long double __k_tanl(long double, long double, int)
float __k_cosdf(double)
Definition __cosdf.c:30
double __math_oflow(uint32_t)
Definition __math_oflow.c:3
double j1(double x)
double __expo2(double, double)
double __lgamma_r(double, int *)
#define fp_barrierl
Definition libm.h:139
static float eval_as_float(float x)
Definition libm.h:104
float __math_uflowf(uint32_t)
Definition __math_uflowf.c:3
float __lgammaf_r(float, int *)
float y0f(float x)
#define fp_barrierf
Definition libm.h:121
#define _UNUSED(expr)
Definition libm.h:160
long double __p1evll(long double, const long double *, int)
#define fp_force_eval
Definition libm.h:173
long double __k_cosl(long double, long double)
double __math_invalid(double)
Definition __math_invalid.c:3
float j0f(float x)
long double __polevll(long double, const long double *, int)
double y0(double x)
int __signgam
int __rem_pio2(double, double *)
double j0(double x)
static struct_typet::componentst::iterator pad(struct_typet::componentst &components, struct_typet::componentst::iterator where, std::size_t pad_bits)
Definition padding.cpp:48