aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Core')
-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
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);
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-14 19:46:13 +0000