diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 39 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 9 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 26 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.h | 1 | ||||
| -rw-r--r-- | runtime/Runtest/intrinsics.c | 15 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 1 |
6 files changed, 0 insertions, 91 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index f17b4062..9c6d84cd 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1617,9 +1617,6 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { FP_CONSTANT_BINOP(floats::sub, type, left, right, ki, state); } -sfdrunk -airbedandbreakfast - break; } @@ -2622,42 +2619,6 @@ ObjectState *Executor::bindObjectInState(ExecutionState &state, const MemoryObje return os; } -void Executor::executeAllocN(ExecutionState &state, - uint64_t nelems, - uint64_t size, - uint64_t alignment, - bool isLocal, - KInstruction *target) { -#if 0 - // over-allocate so that we can properly align the whole buffer - uint64_t address = (uint64_t) (unsigned) malloc(nelems * size + alignment - 1); - address += (alignment - address % alignment); -#else - theMMap = - mmap((void*) 0x90000000, - nelems*size, PROT_READ|PROT_WRITE, - MAP_PRIVATE -#ifdef MAP_ANONYMOUS - |MAP_ANONYMOUS -#endif - , 0, 0); - uint64_t address = (uintptr_t) theMMap; - theMMapSize = nelems*size; -#endif - - for (unsigned i = 0; i < nelems; i++) { - MemoryObject *mo = memory->allocateFixed(address + i*size, size, state.prevPC->inst); - ObjectState *os = bindObjectInState(state, mo, isLocal); - os->initializeToRandom(); - - // bind the local to the first memory object in the whole array - if (i == 0) - bindLocal(target, state, mo->getBaseExpr()); - } - - llvm::cerr << "KLEE: allocN at: " << address << "\n"; -} - void Executor::executeAlloc(ExecutionState &state, ref<Expr> size, bool isLocal, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 852d4cc6..2619e786 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -237,15 +237,6 @@ private: bool zeroMemory=false, const ObjectState *reallocFrom=0); - /// XXX not for public use (this is for histar, it allocations a - /// contiguous set of objects, while guaranteeing page alignment) - void executeAllocN(ExecutionState &state, - uint64_t nelems, - uint64_t size, - uint64_t alignment, - bool isLocal, - KInstruction *target); - /// Free the given address with checking for errors. If target is /// given it will be bound to 0 in the resulting states (this is a /// convenience for realloc). Note that this function can cause the diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 2e423785..3f7c442e 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -74,7 +74,6 @@ HandlerInfo handlerInfo[] = { add("klee_is_symbolic", handleIsSymbolic, true), add("klee_make_symbolic", handleMakeSymbolic, false), add("klee_mark_global", handleMarkGlobal, false), - add("klee_malloc_n", handleMallocN, true), add("klee_merge", handleMerge, false), add("klee_prefer_cex", handlePreferCex, false), add("klee_print_expr", handlePrintExpr, false), @@ -348,31 +347,6 @@ void SpecialFunctionHandler::handleMalloc(ExecutionState &state, executor.executeAlloc(state, arguments[0], false, target); } -void SpecialFunctionHandler::handleMallocN(ExecutionState &state, - KInstruction *target, - std::vector<ref<Expr> > &arguments) { - - // XXX should type check args - assert(arguments.size() == 3 && "invalid number of arguments to malloc"); - - // mallocn(number, size, alignment) - ref<Expr> numElems = executor.toUnique(state, arguments[0]); - ref<Expr> elemSize = executor.toUnique(state, arguments[1]); - ref<Expr> elemAlignment = executor.toUnique(state, arguments[2]); - - assert(numElems.isConstant() && - elemSize.isConstant() && - elemAlignment.isConstant() && - "symbolic arguments passed to klee_mallocn"); - - executor.executeAllocN(state, - numElems.getConstantValue(), - elemSize.getConstantValue(), - elemAlignment.getConstantValue(), - false, - target); -} - void SpecialFunctionHandler::handleAssume(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index d5d1af93..37792faf 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -82,7 +82,6 @@ namespace klee { HANDLER(handleIsSymbolic); HANDLER(handleMakeSymbolic); HANDLER(handleMalloc); - HANDLER(handleMallocN); HANDLER(handleMarkGlobal); HANDLER(handleMerge); HANDLER(handleNew); diff --git a/runtime/Runtest/intrinsics.c b/runtime/Runtest/intrinsics.c index bcd072ac..7ec21901 100644 --- a/runtime/Runtest/intrinsics.c +++ b/runtime/Runtest/intrinsics.c @@ -94,21 +94,6 @@ void klee_make_symbolic(void *array, unsigned nbytes, const char *name) { } } -void *klee_malloc_n(unsigned nelems, unsigned size, unsigned alignment) { -#if 1 - return mmap((void*) 0x90000000, nelems*size, PROT_READ|PROT_WRITE, - MAP_PRIVATE -#ifdef MAP_ANONYMOUS - |MAP_ANONYMOUS -#endif - , 0, 0); -#else - char *buffer = malloc(nelems*size + alignment - 1); - buffer += (alignment - (long)buffer % alignment); - return buffer; -#endif -} - void klee_silent_exit(int x) { exit(x); } diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 97911759..de18edcc 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -663,7 +663,6 @@ static const char *modelledExternals[] = { "klee_is_symbolic", "klee_make_symbolic", "klee_mark_global", - "klee_malloc_n", "klee_merge", "klee_prefer_cex", "klee_print_expr", |