klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
FloatEvaluation.h
Go to the documentation of this file.
1 //===-- FloatEvaluation.h ---------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 // FIXME: Ditch this and use APFloat.
11 
12 #ifndef KLEE_UTIL_FLOATS_H
13 #define KLEE_UTIL_FLOATS_H
14 
15 #include "klee/util/Bits.h" //bits64::truncateToNBits
16 #include "IntEvaluation.h" //ints::sext
17 
18 #include "llvm/Support/MathExtras.h"
19 
20 #include <cassert>
21 
22 namespace klee {
23 namespace floats {
24 
25 // ********************************** //
26 // *** Pack uint64_t into FP types ** //
27 // ********************************** //
28 
29 // interpret the 64 bits as a double instead of a uint64_t
30 inline double UInt64AsDouble( uint64_t bits ) {
31  double ret;
32  assert( sizeof(bits) == sizeof(ret) );
33  memcpy( &ret, &bits, sizeof bits );
34  return ret;
35 }
36 
37 // interpret the first 32 bits as a float instead of a uint64_t
38 inline float UInt64AsFloat( uint64_t bits ) {
39  uint32_t tmp = bits; // ensure that we read correct bytes
40  float ret;
41  assert( sizeof(tmp) == sizeof(ret) );
42  memcpy( &ret, &tmp, sizeof tmp );
43  return ret;
44 }
45 
46 
47 // ********************************** //
48 // *** Pack FP types into uint64_t ** //
49 // ********************************** //
50 
51 // interpret the 64 bits as a uint64_t instead of a double
52 inline uint64_t DoubleAsUInt64( double d ) {
53  uint64_t ret;
54  assert( sizeof(d) == sizeof(ret) );
55  memcpy( &ret, &d, sizeof d );
56  return ret;
57 }
58 
59 // interpret the 32 bits as a uint64_t instead of as a float (add 32 0s)
60 inline uint64_t FloatAsUInt64( float f ) {
61  uint32_t tmp;
62  assert( sizeof(tmp) == sizeof(f) );
63  memcpy( &tmp, &f, sizeof f );
64  return (uint64_t)tmp;
65 }
66 
67 
68 // ********************************** //
69 // ************ Constants *********** //
70 // ********************************** //
71 
72 const unsigned FLT_BITS = 32;
73 const unsigned DBL_BITS = 64;
74 
75 
76 
77 // ********************************** //
78 // ***** LLVM Binary Operations ***** //
79 // ********************************** //
80 
81 // add of l and r
82 inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) {
83  switch( inWidth ) {
86  default: assert(0 && "invalid floating point width");
87  }
88 }
89 
90 // difference of l and r
91 inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) {
92  switch( inWidth ) {
95  default: assert(0 && "invalid floating point width");
96  }
97 }
98 
99 // product of l and r
100 inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) {
101  switch( inWidth ) {
104  default: assert(0 && "invalid floating point width");
105  }
106 }
107 
108 // signed divide of l by r
109 inline uint64_t div(uint64_t l, uint64_t r, unsigned inWidth) {
110  switch( inWidth ) {
113  default: assert(0 && "invalid floating point width");
114  }
115 }
116 
117 // signed modulo of l by r
118 inline uint64_t mod(uint64_t l, uint64_t r, unsigned inWidth) {
119  switch( inWidth ) {
122  default: assert(0 && "invalid floating point width");
123  }
124 }
125 
126 
127 // ********************************** //
128 // *** LLVM Comparison Operations *** //
129 // ********************************** //
130 
131 // determine if l represents NaN
132 inline bool isNaN(uint64_t l, unsigned inWidth) {
133  switch( inWidth ) {
134  case FLT_BITS: return llvm::IsNAN( UInt64AsFloat(l) );
135  case DBL_BITS: return llvm::IsNAN( UInt64AsDouble(l) );
136  default: assert(0 && "invalid floating point width");
137  }
138 }
139 
140 inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) {
141  switch( inWidth ) {
142  case FLT_BITS: return UInt64AsFloat(l) == UInt64AsFloat(r);
143  case DBL_BITS: return UInt64AsDouble(l) == UInt64AsDouble(r);
144  default: assert(0 && "invalid floating point width");
145  }
146 }
147 
148 inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) {
149  switch( inWidth ) {
150  case FLT_BITS: return UInt64AsFloat(l) != UInt64AsFloat(r);
151  case DBL_BITS: return UInt64AsDouble(l) != UInt64AsDouble(r);
152  default: assert(0 && "invalid floating point width");
153  }
154 }
155 
156 inline uint64_t lt(uint64_t l, uint64_t r, unsigned inWidth) {
157  switch( inWidth ) {
158  case FLT_BITS: return UInt64AsFloat(l) < UInt64AsFloat(r);
159  case DBL_BITS: return UInt64AsDouble(l) < UInt64AsDouble(r);
160  default: assert(0 && "invalid floating point width");
161  }
162 }
163 
164 inline uint64_t le(uint64_t l, uint64_t r, unsigned inWidth) {
165  switch( inWidth ) {
166  case FLT_BITS: return UInt64AsFloat(l) <= UInt64AsFloat(r);
167  case DBL_BITS: return UInt64AsDouble(l) <= UInt64AsDouble(r);
168  default: assert(0 && "invalid floating point width");
169  }
170 }
171 
172 inline uint64_t gt(uint64_t l, uint64_t r, unsigned inWidth) {
173  switch( inWidth ) {
174  case FLT_BITS: return UInt64AsFloat(l) > UInt64AsFloat(r);
175  case DBL_BITS: return UInt64AsDouble(l) > UInt64AsDouble(r);
176  default: assert(0 && "invalid floating point width");
177  }
178 }
179 
180 inline uint64_t ge(uint64_t l, uint64_t r, unsigned inWidth) {
181  switch( inWidth ) {
182  case FLT_BITS: return UInt64AsFloat(l) >= UInt64AsFloat(r);
183  case DBL_BITS: return UInt64AsDouble(l) >= UInt64AsDouble(r);
184  default: assert(0 && "invalid floating point width");
185  }
186 }
187 
188 
189 // ********************************** //
190 // *** LLVM Conversion Operations *** //
191 // ********************************** //
192 
193 // truncation of l (which must be a double) to float (casts a double to a float)
194 inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) {
195  // FIXME: Investigate this, should this not happen? Was a quick
196  // patch for busybox.
197  if (inWidth==64 && outWidth==64) {
198  return l;
199  } else {
200  assert(inWidth==64 && "can only truncate from a 64-bit double");
201  assert(outWidth==32 && "can only truncate to a 32-bit float");
202  float trunc = (float)UInt64AsDouble(l);
203  return bits64::truncateToNBits(FloatAsUInt64(trunc), outWidth);
204  }
205 }
206 
207 // extension of l (which must be a float) to double (casts a float to a double)
208 inline uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth) {
209  // FIXME: Investigate this, should this not happen? Was a quick
210  // patch for busybox.
211  if (inWidth==64 && outWidth==64) {
212  return l;
213  } else {
214  assert(inWidth==32 && "can only extend from a 32-bit float");
215  assert(outWidth==64 && "can only extend to a 64-bit double");
216  double ext = (double)UInt64AsFloat(l);
217  return bits64::truncateToNBits(DoubleAsUInt64(ext), outWidth);
218  }
219 }
220 
221 // conversion of l to an unsigned integer, rounding towards zero
222 inline uint64_t toUnsignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) {
223  switch( inWidth ) {
224  case FLT_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsFloat(l), outWidth );
225  case DBL_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsDouble(l), outWidth );
226  default: assert(0 && "invalid floating point width");
227  }
228 }
229 
230 // conversion of l to a signed integer, rounding towards zero
231 inline uint64_t toSignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) {
232  switch( inWidth ) {
233  case FLT_BITS: return bits64::truncateToNBits((int64_t)UInt64AsFloat(l), outWidth);
234  case DBL_BITS: return bits64::truncateToNBits((int64_t)UInt64AsDouble(l), outWidth);
235  default: assert(0 && "invalid floating point width");
236  }
237 }
238 
239 // conversion of l, interpreted as an unsigned int, to a floating point number
240 inline uint64_t UnsignedIntToFP( uint64_t l, unsigned outWidth ) {
241  switch( outWidth ) {
242  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)l), outWidth);
243  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)l), outWidth);
244  default: assert(0 && "invalid floating point width");
245  }
246 }
247 
248 // conversion of l, interpreted as a signed int, to a floating point number
249 inline uint64_t SignedIntToFP( uint64_t l, unsigned outWidth, unsigned inWidth ) {
250  switch( outWidth ) {
251  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)(int64_t)ints::sext(l, 64, inWidth)), outWidth);
252  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)(int64_t)ints::sext(l,64, inWidth)), outWidth);
253  default: assert(0 && "invalid floating point width");
254  }
255 }
256 
257 } // end namespace ints
258 } // end namespace klee
259 
260 #endif //KLEE_UTIL_FLOATS_H
uint64_t UnsignedIntToFP(uint64_t l, unsigned outWidth)
bool isNaN(uint64_t l, unsigned inWidth)
uint64_t FloatAsUInt64(float f)
uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth)
uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t ge(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t add(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t le(uint64_t l, uint64_t r, unsigned inWidth)
double UInt64AsDouble(uint64_t bits)
uint64_t DoubleAsUInt64(double d)
uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t mod(uint64_t l, uint64_t r, unsigned inWidth)
const unsigned FLT_BITS
uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth)
uint64_t div(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t toUnsignedInt(uint64_t l, unsigned outWidth, unsigned inWidth)
uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth)
float UInt64AsFloat(uint64_t bits)
const unsigned DBL_BITS
uint64_t toSignedInt(uint64_t l, unsigned outWidth, unsigned inWidth)
uint64_t lt(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t sext(uint64_t l, unsigned outWidth, unsigned inWidth)
Definition: IntEvaluation.h:50
uint64_t truncateToNBits(uint64_t x, unsigned N)
Definition: Bits.h:71
uint64_t SignedIntToFP(uint64_t l, unsigned outWidth, unsigned inWidth)
uint64_t gt(uint64_t l, uint64_t r, unsigned inWidth)
uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth)