about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Context.cpp56
-rw-r--r--lib/Core/Context.h45
-rw-r--r--lib/Core/Executor.cpp23
-rw-r--r--lib/Core/ExecutorUtil.cpp1
-rw-r--r--lib/Core/ImpliedValue.cpp3
-rw-r--r--lib/Core/Memory.cpp26
-rw-r--r--lib/Core/Memory.h11
-rw-r--r--lib/Expr/Expr.cpp56
-rw-r--r--lib/Solver/FastCexSolver.cpp2
9 files changed, 155 insertions, 68 deletions
diff --git a/lib/Core/Context.cpp b/lib/Core/Context.cpp
new file mode 100644
index 00000000..590b2080
--- /dev/null
+++ b/lib/Core/Context.cpp
@@ -0,0 +1,56 @@
+//===-- Context.cpp -------------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "Context.h"
+
+#include "klee/Expr.h"
+
+#include "llvm/Type.h"
+#include "llvm/DerivedTypes.h"
+
+#include <cassert>
+
+using namespace klee;
+
+static bool Initialized = false;
+static Context TheContext;
+
+void Context::initialize(bool IsLittleEndian, Expr::Width PointerWidth) {
+  assert(!Initialized && "Duplicate context initialization!");
+  TheContext = Context(IsLittleEndian, PointerWidth);
+  Initialized = true;
+}
+
+const Context &Context::get() {
+  assert(Initialized && "Context has not been initialized!");
+  return TheContext;
+}
+
+// FIXME: This is a total hack, just to avoid a layering issue until this stuff
+// moves out of Expr.
+
+Expr::Width Expr::getWidthForLLVMType(const llvm::Type *t) {
+  switch (t->getTypeID()) {
+  default:
+    assert(0 && "non-primitive type argument to Expr::getTypeForLLVMType()\n");
+  case llvm::Type::IntegerTyID: return cast<llvm::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 Context::get().getPointerWidth();
+  }
+}
+
+ref<Expr> Expr::createCoerceToPointerType(ref<Expr> e) {
+  return ZExtExpr::create(e, Context::get().getPointerWidth());
+}
+
+ref<ConstantExpr> Expr::createPointer(uint64_t v) {
+  return ConstantExpr::create(v, Context::get().getPointerWidth());
+}
diff --git a/lib/Core/Context.h b/lib/Core/Context.h
new file mode 100644
index 00000000..af1ce8e7
--- /dev/null
+++ b/lib/Core/Context.h
@@ -0,0 +1,45 @@
+//===-- Context.h -----------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_CONTEXT_H
+#define KLEE_CONTEXT_H
+
+#include "klee/Expr.h"
+
+namespace klee {
+
+  /// Context - Helper class for storing global information about a KLEE run.
+  class Context {
+    /// Whether the target architecture is little endian or not.
+    bool IsLittleEndian;
+
+    /// The pointer width of the target architecture.
+    Expr::Width PointerWidth;
+
+  protected:
+    Context(bool _IsLittleEndian, Expr::Width _PointerWidth)
+      : IsLittleEndian(_IsLittleEndian), PointerWidth(_PointerWidth) {}
+    
+  public:
+    Context() {}
+    
+    /// initialize - Construct the global Context instance.
+    static void initialize(bool IsLittleEndian, Expr::Width PointerWidth);
+
+    /// get - Return the global singleton instance of the Context.
+    static const Context &get();
+
+    bool isLittleEndian() const { return IsLittleEndian; }
+
+    Expr::Width getPointerWidth() const { return PointerWidth; }
+  };
+  
+} // End klee namespace
+
+#endif
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index f007293a..0e2f7a8c 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -11,6 +11,7 @@
 
 #include "Executor.h"
  
+#include "Context.h"
 #include "CoreStats.h"
 #include "ExternalDispatcher.h"
 #include "ImpliedValue.h"
@@ -28,7 +29,6 @@
 #include "klee/ExecutionState.h"
 #include "klee/Expr.h"
 #include "klee/Interpreter.h"
-#include "klee/Machine.h"
 #include "klee/TimerStatIncrementer.h"
 #include "klee/util/Assignment.h"
 #include "klee/util/ExprPPrinter.h"
@@ -336,9 +336,14 @@ Executor::Executor(const InterpreterOptions &opts,
 const Module *Executor::setModule(llvm::Module *module, 
                                   const ModuleOptions &opts) {
   assert(!kmodule && module && "can only register one module"); // XXX gross
-
+  
   kmodule = new KModule(module);
 
+  // Initialize the context.
+  TargetData *TD = kmodule->targetData;
+  Context::initialize(TD->isLittleEndian(),
+                      (Expr::Width) TD->getPointerSizeInBits());
+
   specialFunctionHandler = new SpecialFunctionHandler(*this);
 
   specialFunctionHandler->prepare();
@@ -2617,7 +2622,8 @@ void Executor::executeAlloc(ExecutionState &state,
     MemoryObject *mo = memory->allocate(CE->getZExtValue(), isLocal, false, 
                                         state.prevPC->inst);
     if (!mo) {
-      bindLocal(target, state, ConstantExpr::alloc(0, kMachinePointerType));
+      bindLocal(target, state, 
+                ConstantExpr::alloc(0, Context::get().getPointerWidth()));
     } else {
       ObjectState *os = bindObjectInState(state, mo, isLocal);
       if (zeroMemory) {
@@ -2692,7 +2698,7 @@ void Executor::executeAlloc(ExecutionState &state,
         if (hugeSize.first) {
           klee_message("NOTE: found huge malloc, returing 0");
           bindLocal(target, *hugeSize.first, 
-                    ConstantExpr::alloc(0, kMachinePointerType));
+                    ConstantExpr::alloc(0, Context::get().getPointerWidth()));
         }
         
         if (hugeSize.second) {
@@ -2999,6 +3005,7 @@ void Executor::runFunctionAsMain(Function *f,
   int envc;
   for (envc=0; envp[envc]; ++envc) ;
 
+  unsigned NumPtrBytes = Context::get().getPointerWidth() / 8;
   KFunction *kf = kmodule->functionMap[f];
   assert(kf);
   Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end();
@@ -3006,13 +3013,13 @@ void Executor::runFunctionAsMain(Function *f,
     arguments.push_back(ConstantExpr::alloc(argc, Expr::Int32));
 
     if (++ai!=ae) {
-      argvMO = memory->allocate((argc+1+envc+1+1) * kMachinePointerSize, false, true,
+      argvMO = memory->allocate((argc+1+envc+1+1) * NumPtrBytes, false, true,
                                 f->begin()->begin());
       
       arguments.push_back(argvMO->getBaseExpr());
 
       if (++ai!=ae) {
-        uint64_t envp_start = argvMO->address + (argc+1)*kMachinePointerSize;
+        uint64_t envp_start = argvMO->address + (argc+1)*NumPtrBytes;
         arguments.push_back(Expr::createPointer(envp_start));
 
         if (++ai!=ae)
@@ -3055,9 +3062,9 @@ void Executor::runFunctionAsMain(Function *f,
       }
 
       if (arg) {
-        argvOS->write(i * kMachinePointerSize, arg->getBaseExpr());
+        argvOS->write(i * NumPtrBytes, arg->getBaseExpr());
       } else {
-        argvOS->write(i * kMachinePointerSize, Expr::createPointer(0));
+        argvOS->write(i * NumPtrBytes, Expr::createPointer(0));
       }
     }
   }
diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp
index 3bb8a0b0..a2cfa0ae 100644
--- a/lib/Core/ExecutorUtil.cpp
+++ b/lib/Core/ExecutorUtil.cpp
@@ -11,7 +11,6 @@
 
 #include "klee/Expr.h"
 #include "klee/Interpreter.h"
-#include "klee/Machine.h"
 #include "klee/Solver.h"
 
 #include "klee/Internal/Module/KModule.h"
diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp
index 8fb84edd..a3d30f76 100644
--- a/lib/Core/ImpliedValue.cpp
+++ b/lib/Core/ImpliedValue.cpp
@@ -9,6 +9,7 @@
 
 #include "ImpliedValue.h"
 
+#include "Context.h"
 #include "klee/Constraints.h"
 #include "klee/Expr.h"
 #include "klee/Solver.h"
@@ -223,7 +224,7 @@ void ImpliedValue::checkForImpliedValues(Solver *S, ref<Expr> e,
     ReadExpr *re = i->get();
     assumption.push_back(UltExpr::create(re->index, 
                                          ConstantExpr::alloc(re->updates.root->size, 
-                                                             kMachinePointerType)));
+                                                             Context::get().getPointerWidth())));
   }
 
   ConstraintManager assume(assumption);
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index 2032fd53..34aeeff5 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -11,8 +11,8 @@
 
 #include "Memory.h"
 
+#include "Context.h"
 #include "klee/Expr.h"
-#include "klee/Machine.h"
 #include "klee/Solver.h"
 #include "klee/util/BitArray.h"
 
@@ -265,11 +265,11 @@ void ObjectState::flushRangeForRead(unsigned rangeBase,
   for (unsigned offset=rangeBase; offset<rangeBase+rangeSize; offset++) {
     if (!isByteFlushed(offset)) {
       if (isByteConcrete(offset)) {
-        updates.extend(ConstantExpr::create(offset, kMachinePointerType),
+        updates.extend(ConstantExpr::create(offset, Context::get().getPointerWidth()),
                        ConstantExpr::create(concreteStore[offset], Expr::Int8));
       } else {
         assert(isByteKnownSymbolic(offset) && "invalid bit set in flushMask");
-        updates.extend(ConstantExpr::create(offset, kMachinePointerType),
+        updates.extend(ConstantExpr::create(offset, Context::get().getPointerWidth()),
                        knownSymbolics[offset]);
       }
 
@@ -285,12 +285,12 @@ void ObjectState::flushRangeForWrite(unsigned rangeBase,
   for (unsigned offset=rangeBase; offset<rangeBase+rangeSize; offset++) {
     if (!isByteFlushed(offset)) {
       if (isByteConcrete(offset)) {
-        updates.extend(ConstantExpr::create(offset, kMachinePointerType),
+        updates.extend(ConstantExpr::create(offset, Context::get().getPointerWidth()),
                        ConstantExpr::create(concreteStore[offset], Expr::Int8));
         markByteSymbolic(offset);
       } else {
         assert(isByteKnownSymbolic(offset) && "invalid bit set in flushMask");
-        updates.extend(ConstantExpr::create(offset, kMachinePointerType),
+        updates.extend(ConstantExpr::create(offset, Context::get().getPointerWidth()),
                        knownSymbolics[offset]);
         setKnownSymbolic(offset, 0);
       }
@@ -367,7 +367,7 @@ ref<Expr> ObjectState::read8(unsigned offset) const {
     assert(isByteFlushed(offset) && "unflushed byte without cache value");
     
     return ReadExpr::create(getUpdates(), 
-                            ConstantExpr::create(offset, kMachinePointerType));
+                            ConstantExpr::create(offset, Context::get().getPointerWidth()));
   }    
 }
 
@@ -444,7 +444,7 @@ ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
   assert(width == NumBytes * 8 && "Invalid write size!");
   ref<Expr> Res(0);
   for (unsigned i = 0; i != NumBytes; ++i) {
-    unsigned idx = (kMachineByteOrder == machine::MSB) ? (NumBytes - i - 1) : i;
+    unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
     ref<Expr> Byte = read8(AddExpr::create(offset, 
                                            ConstantExpr::create(idx, 
                                                                 IndexWidth)));
@@ -464,7 +464,7 @@ ref<Expr> ObjectState::read(unsigned offset, Expr::Width width) const {
   assert(width == NumBytes * 8 && "Invalid write size!");
   ref<Expr> Res(0);
   for (unsigned i = 0; i != NumBytes; ++i) {
-    unsigned idx = (kMachineByteOrder == machine::MSB) ? (NumBytes - i - 1) : i;
+    unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
     ref<Expr> Byte = read8(offset + idx);
     Res = idx ? ConcatExpr::create(Byte, Res) : Byte;
   }
@@ -491,7 +491,7 @@ void ObjectState::write(ref<Expr> offset, ref<Expr> value) {
   unsigned NumBytes = w / 8;
   assert(w == NumBytes * 8 && "Invalid write size!");
   for (unsigned i = 0; i != NumBytes; ++i) {
-    unsigned idx = (kMachineByteOrder == machine::MSB) ? (NumBytes - i - 1) : i;
+    unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
     write8(AddExpr::create(offset, ConstantExpr::create(idx, IndexWidth)),
            ExtractExpr::create(value, 8 * i, Expr::Int8));
   }
@@ -525,7 +525,7 @@ void ObjectState::write(unsigned offset, ref<Expr> value) {
   unsigned NumBytes = w / 8;
   assert(w == NumBytes * 8 && "Invalid write size!");
   for (unsigned i = 0; i != NumBytes; ++i) {
-    unsigned idx = (kMachineByteOrder == machine::MSB) ? (NumBytes - i - 1) : i;
+    unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
     write8(offset + idx, ExtractExpr::create(value, 8 * i, Expr::Int8));
   }
 } 
@@ -533,7 +533,7 @@ void ObjectState::write(unsigned offset, ref<Expr> value) {
 void ObjectState::write16(unsigned offset, uint16_t value) {
   unsigned NumBytes = 2;
   for (unsigned i = 0; i != NumBytes; ++i) {
-    unsigned idx = (kMachineByteOrder == machine::MSB) ? (NumBytes - i - 1) : i;
+    unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
     write8(offset + idx, (uint8_t) (value >> (8 * i)));
   }
 }
@@ -541,7 +541,7 @@ void ObjectState::write16(unsigned offset, uint16_t value) {
 void ObjectState::write32(unsigned offset, uint32_t value) {
   unsigned NumBytes = 4;
   for (unsigned i = 0; i != NumBytes; ++i) {
-    unsigned idx = (kMachineByteOrder == machine::MSB) ? (NumBytes - i - 1) : i;
+    unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
     write8(offset + idx, (uint8_t) (value >> (8 * i)));
   }
 }
@@ -549,7 +549,7 @@ void ObjectState::write32(unsigned offset, uint32_t value) {
 void ObjectState::write64(unsigned offset, uint64_t value) {
   unsigned NumBytes = 8;
   for (unsigned i = 0; i != NumBytes; ++i) {
-    unsigned idx = (kMachineByteOrder == machine::MSB) ? (NumBytes - i - 1) : i;
+    unsigned idx = Context::get().isLittleEndian() ? i : (NumBytes - i - 1);
     write8(offset + idx, (uint8_t) (value >> (8 * i)));
   }
 }
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 3179c267..7f7b86a8 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_MEMORY_H
 #define KLEE_MEMORY_H
 
+#include "Context.h"
 #include "klee/Expr.h"
 
 #include "llvm/ADT/StringExtras.h"
@@ -100,10 +101,10 @@ public:
   }
 
   ref<ConstantExpr> getBaseExpr() const { 
-    return ConstantExpr::create(address, kMachinePointerType);
+    return ConstantExpr::create(address, Context::get().getPointerWidth());
   }
   ref<ConstantExpr> getSizeExpr() const { 
-    return ConstantExpr::create(size, kMachinePointerType);
+    return ConstantExpr::create(size, Context::get().getPointerWidth());
   }
   ref<Expr> getOffsetExpr(ref<Expr> pointer) const {
     return SubExpr::create(pointer, getBaseExpr());
@@ -117,7 +118,8 @@ public:
 
   ref<Expr> getBoundsCheckOffset(ref<Expr> offset) const {
     if (size==0) {
-      return EqExpr::create(offset, ConstantExpr::alloc(0, kMachinePointerType));
+      return EqExpr::create(offset, 
+                            ConstantExpr::alloc(0, Context::get().getPointerWidth()));
     } else {
       return UltExpr::create(offset, getSizeExpr());
     }
@@ -125,7 +127,8 @@ public:
   ref<Expr> getBoundsCheckOffset(ref<Expr> offset, unsigned bytes) const {
     if (bytes<=size) {
       return UltExpr::create(offset, 
-                             ConstantExpr::alloc(size - bytes + 1, kMachinePointerType));
+                             ConstantExpr::alloc(size - bytes + 1, 
+                                                 Context::get().getPointerWidth()));
     } else {
       return ConstantExpr::alloc(0, Expr::Bool);
     }
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);
 }
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index fbf2ecf2..b7a7f4fc 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -1115,7 +1115,7 @@ FastCexSolver::computeInitialValues(const Query& query,
     for (unsigned i=0; i < array->size; i++) {
       ref<Expr> read = 
         ReadExpr::create(UpdateList(array, 0),
-                         ConstantExpr::create(i, kMachinePointerType));
+                         ConstantExpr::create(i, Expr::Int32));
       ref<Expr> value = cd.evaluatePossible(read);
       
       if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-12-14 23:51:21 +0000