about summary refs log tree commit diff homepage
path: root/include
diff options
context:
space:
mode:
authorDaniel Schemmel <daniel@schemmel.net>2023-03-22 23:41:24 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2023-03-23 17:27:39 +0000
commita91be77e800510db50444b3e1f5ef20dbca0260c (patch)
treeb657364f9ead493daf12986bcf604e432df75d07 /include
parent91468cf16fb158cd6be5eb9d9c5259f7f88bdf9a (diff)
downloadklee-a91be77e800510db50444b3e1f5ef20dbca0260c.tar.gz
remove obsolete header
Diffstat (limited to 'include')
-rw-r--r--include/klee/Support/FloatEvaluation.h264
1 files changed, 0 insertions, 264 deletions
diff --git a/include/klee/Support/FloatEvaluation.h b/include/klee/Support/FloatEvaluation.h
deleted file mode 100644
index d6fcc73c..00000000
--- a/include/klee/Support/FloatEvaluation.h
+++ /dev/null
@@ -1,264 +0,0 @@
-//===-- FloatEvaluation.h ---------------------------------------*- C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-// FIXME: Ditch this and use APFloat.
-
-#ifndef KLEE_FLOATEVALUATION_H
-#define KLEE_FLOATEVALUATION_H
-
-#include "IntEvaluation.h" // ints::sext
-
-#include "klee/ADT/Bits.h" // bits64::truncateToNBits
-
-#include "llvm/Support/ErrorHandling.h"
-#include "llvm/Support/MathExtras.h"
-
-#include <cassert>
-
-namespace klee {
-namespace floats {
-
-// ********************************** //
-// *** Pack uint64_t into FP types ** //
-// ********************************** //
-
-// interpret the 64 bits as a double instead of a uint64_t
-inline double UInt64AsDouble( uint64_t bits ) {
-  double ret;
-  assert( sizeof(bits) == sizeof(ret) );
-  memcpy( &ret, &bits, sizeof bits );
-  return ret;
-}
-
-// interpret the first 32 bits as a float instead of a uint64_t
-inline float UInt64AsFloat( uint64_t bits ) {
-  uint32_t tmp = bits; // ensure that we read correct bytes
-  float ret;
-  assert( sizeof(tmp) == sizeof(ret) );
-  memcpy( &ret, &tmp, sizeof tmp );
-  return ret;
-}
-
-
-// ********************************** //
-// *** Pack FP types into uint64_t ** //
-// ********************************** //
-
-// interpret the 64 bits as a uint64_t instead of a double
-inline uint64_t DoubleAsUInt64( double d ) {
-  uint64_t ret;
-  assert( sizeof(d) == sizeof(ret) );
-  memcpy( &ret, &d, sizeof d );
-  return ret;
-}
-
-// interpret the 32 bits as a uint64_t instead of as a float (add 32 0s)
-inline uint64_t FloatAsUInt64( float f ) {
-  uint32_t tmp;
-  assert( sizeof(tmp) == sizeof(f) );
-  memcpy( &tmp, &f, sizeof f );
-  return (uint64_t)tmp;
-}
-
-
-// ********************************** //
-// ************ Constants *********** //
-// ********************************** //
-
-const unsigned FLT_BITS = 32;
-const unsigned DBL_BITS = 64;
-
-
-
-// ********************************** //
-// ***** LLVM Binary Operations ***** //
-// ********************************** //
-
-// add of l and r
-inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  + UInt64AsFloat(r)),  FLT_BITS);
-  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) + UInt64AsDouble(r)), DBL_BITS);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-// difference of l and r
-inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  - UInt64AsFloat(r)),  FLT_BITS);
-  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) - UInt64AsDouble(r)), DBL_BITS);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-// product of l and r
-inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  * UInt64AsFloat(r)),  FLT_BITS);
-  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) * UInt64AsDouble(r)), DBL_BITS);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-// signed divide of l by r
-inline uint64_t div(uint64_t l, uint64_t r, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l)  / UInt64AsFloat(r)),  FLT_BITS);
-  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) / UInt64AsDouble(r)), DBL_BITS);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-// signed modulo of l by r
-inline uint64_t mod(uint64_t l, uint64_t r, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64( fmod(UInt64AsFloat(l),  UInt64AsFloat(r)) ), FLT_BITS);
-  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64( fmod(UInt64AsDouble(l), UInt64AsDouble(r)) ), DBL_BITS);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-
-// ********************************** //
-// *** LLVM Comparison Operations *** //
-// ********************************** //
-
-// determine if l represents NaN
-inline bool isNaN(uint64_t l, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS:
-    return std::isnan(UInt64AsFloat(l));
-  case DBL_BITS:
-    return std::isnan(UInt64AsDouble(l));
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS: return UInt64AsFloat(l)  == UInt64AsFloat(r);
-  case DBL_BITS: return UInt64AsDouble(l) == UInt64AsDouble(r);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS: return UInt64AsFloat(l)  != UInt64AsFloat(r);
-  case DBL_BITS: return UInt64AsDouble(l) != UInt64AsDouble(r);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-inline uint64_t lt(uint64_t l, uint64_t r, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS: return UInt64AsFloat(l)  < UInt64AsFloat(r);
-  case DBL_BITS: return UInt64AsDouble(l) < UInt64AsDouble(r);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-inline uint64_t le(uint64_t l, uint64_t r, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS: return UInt64AsFloat(l)  <= UInt64AsFloat(r);
-  case DBL_BITS: return UInt64AsDouble(l) <= UInt64AsDouble(r);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-inline uint64_t gt(uint64_t l, uint64_t r, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS: return UInt64AsFloat(l)  > UInt64AsFloat(r);
-  case DBL_BITS: return UInt64AsDouble(l) > UInt64AsDouble(r);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-inline uint64_t ge(uint64_t l, uint64_t r, unsigned inWidth) {
-  switch( inWidth ) {
-  case FLT_BITS: return UInt64AsFloat(l)  >= UInt64AsFloat(r);
-  case DBL_BITS: return UInt64AsDouble(l) >= UInt64AsDouble(r);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-
-// ********************************** //
-// *** LLVM Conversion Operations *** //
-// ********************************** //
-
-// truncation of l (which must be a double) to float (casts a double to a float)
-inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) {
-  // FIXME: Investigate this, should this not happen? Was a quick
-  // patch for busybox.
-  if (inWidth==64 && outWidth==64) {
-    return l;
-  } else {
-    assert(inWidth==64 && "can only truncate from a 64-bit double");
-    assert(outWidth==32 && "can only truncate to a 32-bit float");
-    float trunc = (float)UInt64AsDouble(l);
-    return bits64::truncateToNBits(FloatAsUInt64(trunc), outWidth);
-  }
-}
-
-// extension of l (which must be a float) to double (casts a float to a double)
-inline uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth) {
-  // FIXME: Investigate this, should this not happen? Was a quick
-  // patch for busybox.
-  if (inWidth==64 && outWidth==64) {
-    return l;
-  } else {
-    assert(inWidth==32 && "can only extend from a 32-bit float");
-    assert(outWidth==64 && "can only extend to a 64-bit double");
-    double ext = (double)UInt64AsFloat(l);
-    return bits64::truncateToNBits(DoubleAsUInt64(ext), outWidth);
-  }
-}
-
-// conversion of l to an unsigned integer, rounding towards zero
-inline uint64_t toUnsignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) {
-  switch( inWidth ) {
-  case FLT_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsFloat(l),  outWidth );
-  case DBL_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsDouble(l), outWidth );
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-// conversion of l to a signed integer, rounding towards zero
-inline uint64_t toSignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) {
-  switch( inWidth ) {
-  case FLT_BITS: return bits64::truncateToNBits((int64_t)UInt64AsFloat(l),  outWidth);
-  case DBL_BITS: return bits64::truncateToNBits((int64_t)UInt64AsDouble(l), outWidth);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-// conversion of l, interpreted as an unsigned int, to a floating point number
-inline uint64_t UnsignedIntToFP( uint64_t l, unsigned outWidth ) {
-  switch( outWidth ) {
-  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)l),  outWidth);
-  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)l), outWidth);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-// conversion of l, interpreted as a signed int, to a floating point number
-inline uint64_t SignedIntToFP( uint64_t l, unsigned outWidth, unsigned inWidth ) {
-  switch( outWidth ) {
-  case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)(int64_t)ints::sext(l, 64, inWidth)), outWidth);
-  case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)(int64_t)ints::sext(l,64, inWidth)), outWidth);
-  default: llvm::report_fatal_error("unsupported floating point width");
-  }
-}
-
-} // end namespace ints
-} // end namespace klee
-
-#endif /* KLEE_FLOATEVALUATION_H */