diff options
author | Daniel Dunbar <daniel@zuster.org> | 2009-07-28 07:59:09 +0000 |
---|---|---|
committer | Daniel Dunbar <daniel@zuster.org> | 2009-07-28 07:59:09 +0000 |
commit | f5e6b462646f5a20dd0e5f6c4befaa7b72d1e1ff (patch) | |
tree | 8c3a622ce7955e304134b2175813721b30a99005 /lib/Core | |
parent | 4fcf6a3c9b87b02d73b6a2f55c17573ca7fc5bbc (diff) | |
download | klee-f5e6b462646f5a20dd0e5f6c4befaa7b72d1e1ff.tar.gz |
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
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Context.cpp | 56 | ||||
-rw-r--r-- | lib/Core/Context.h | 45 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 23 | ||||
-rw-r--r-- | lib/Core/ExecutorUtil.cpp | 1 | ||||
-rw-r--r-- | lib/Core/ImpliedValue.cpp | 3 | ||||
-rw-r--r-- | lib/Core/Memory.cpp | 26 | ||||
-rw-r--r-- | lib/Core/Memory.h | 11 |
7 files changed, 138 insertions, 27 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); } |