Move Machine constants into Context object, initialized based on the target

data.
 - This is the first step towards having KLEE be fully target independent, its not
   particularly beautiful but its expedient.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@77306 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 16 insertions, 40 deletions

diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 4d9e5abe..3820fd32 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -9,9 +9,6 @@
 
 #include "klee/Expr.h"
 
-#include "klee/Machine.h"
-#include "llvm/Type.h"
-#include "llvm/DerivedTypes.h"
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/Streams.h"
 // FIXME: We shouldn't need this once fast constant support moves into
@@ -43,42 +40,42 @@ ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) {
   default: assert(0 && "invalid width");
   case Expr::Bool: 
     return ZExtExpr::create(ReadExpr::create(ul, 
-                                             ConstantExpr::alloc(0,kMachinePointerType)),
+                                             ConstantExpr::alloc(0, Expr::Int32)),
                             Expr::Bool);
   case Expr::Int8: 
     return ReadExpr::create(ul, 
-                            ConstantExpr::alloc(0,kMachinePointerType));
+                            ConstantExpr::alloc(0,Expr::Int32));
   case Expr::Int16: 
     return ConcatExpr::create(ReadExpr::create(ul, 
-                                               ConstantExpr::alloc(1,kMachinePointerType)),
+                                               ConstantExpr::alloc(1,Expr::Int32)),
                               ReadExpr::create(ul, 
-                                               ConstantExpr::alloc(0,kMachinePointerType)));
+                                               ConstantExpr::alloc(0,Expr::Int32)));
   case Expr::Int32: 
     return ConcatExpr::create4(ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(3,kMachinePointerType)),
+                                                ConstantExpr::alloc(3,Expr::Int32)),
                                ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(2,kMachinePointerType)),
+                                                ConstantExpr::alloc(2,Expr::Int32)),
                                ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(1,kMachinePointerType)),
+                                                ConstantExpr::alloc(1,Expr::Int32)),
                                ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(0,kMachinePointerType)));
+                                                ConstantExpr::alloc(0,Expr::Int32)));
   case Expr::Int64: 
     return ConcatExpr::create8(ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(7,kMachinePointerType)),
+                                                ConstantExpr::alloc(7,Expr::Int32)),
                                ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(6,kMachinePointerType)),
+                                                ConstantExpr::alloc(6,Expr::Int32)),
                                ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(5,kMachinePointerType)),
+                                                ConstantExpr::alloc(5,Expr::Int32)),
                                ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(4,kMachinePointerType)),
+                                                ConstantExpr::alloc(4,Expr::Int32)),
                                ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(3,kMachinePointerType)),
+                                                ConstantExpr::alloc(3,Expr::Int32)),
                                ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(2,kMachinePointerType)),
+                                                ConstantExpr::alloc(2,Expr::Int32)),
                                ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(1,kMachinePointerType)),
+                                                ConstantExpr::alloc(1,Expr::Int32)),
                                ReadExpr::create(ul, 
-                                                ConstantExpr::alloc(0,kMachinePointerType)));
+                                                ConstantExpr::alloc(0,Expr::Int32)));
   }
 }
 
@@ -281,19 +278,6 @@ void Expr::printWidth(std::ostream &os, Width width) {
   }
 }
 
-Expr::Width Expr::getWidthForLLVMType(const llvm::Type *t) {
-  switch (t->getTypeID()) {
-  case llvm::Type::IntegerTyID: return cast<IntegerType>(t)->getBitWidth();
-  case llvm::Type::FloatTyID: return Expr::Int32;
-  case llvm::Type::DoubleTyID: return Expr::Int64;
-  case llvm::Type::X86_FP80TyID: return 80;
-  case llvm::Type::PointerTyID: return kMachinePointerType;
-  default:
-    cerr << "non-primitive type argument to Expr::getTypeForLLVMType()\n";
-    abort();
-  }
-}
-
 ref<Expr> Expr::createImplies(ref<Expr> hyp, ref<Expr> conc) {
   return OrExpr::create(Expr::createIsZero(hyp), conc);
 }
@@ -302,14 +286,6 @@ ref<Expr> Expr::createIsZero(ref<Expr> e) {
   return EqExpr::create(e, ConstantExpr::create(0, e->getWidth()));
 }
 
-ref<Expr> Expr::createCoerceToPointerType(ref<Expr> e) {
-  return ZExtExpr::create(e, kMachinePointerType);
-}
-
-ref<ConstantExpr> Expr::createPointer(uint64_t v) {
-  return ConstantExpr::create(v, kMachinePointerType);
-}
-
 void Expr::print(std::ostream &os) const {
   ExprPPrinter::printSingleExpr(os, (Expr*)this);
 }