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