OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/klee?expand=0&rev=37
147 lines
4.8 KiB
Diff
147 lines
4.8 KiB
Diff
From: Martin Nowack <martin@se.inf.tu-dresden.de>
|
|
Date: Tue, 25 Jul 2017 22:38:41 +0200
|
|
Subject: Track errno correctly
|
|
Patch-mainline: no
|
|
|
|
Reduce the time of reading the value of errno
|
|
and using it and writing it to the state space.
|
|
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
---
|
|
lib/Core/Executor.cpp | 26 +++++++++++++++++++++++++-
|
|
lib/Core/ExternalDispatcher.cpp | 11 ++++++++++-
|
|
lib/Core/ExternalDispatcher.h | 2 ++
|
|
lib/Core/Memory.h | 3 +++
|
|
4 files changed, 40 insertions(+), 2 deletions(-)
|
|
|
|
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
|
|
index efc59008e542..045e353ba932 100644
|
|
--- a/lib/Core/Executor.cpp
|
|
+++ b/lib/Core/Executor.cpp
|
|
@@ -531,7 +531,10 @@ void Executor::initializeGlobals(ExecutionState &state) {
|
|
#else
|
|
int *errno_addr = __error();
|
|
#endif
|
|
- addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, false);
|
|
+ MemoryObject *errnoObj =
|
|
+ addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, false);
|
|
+ // Copy values from and to program space explicitly
|
|
+ errnoObj->isUserSpecified = true;
|
|
#endif
|
|
|
|
// Disabled, we don't want to promote use of live externals.
|
|
@@ -2999,6 +3002,27 @@ void Executor::callExternalFunction(ExecutionState &state,
|
|
return;
|
|
}
|
|
|
|
+#ifndef WINDOWS
|
|
+#ifndef __APPLE__
|
|
+ /* From /usr/include/errno.h: it [errno] is a per-thread variable. */
|
|
+ int *errno_addr = __errno_location();
|
|
+#else
|
|
+ int *errno_addr = __error();
|
|
+#endif
|
|
+ // Update errno value explicitly
|
|
+ ObjectPair result;
|
|
+ bool resolved = state.addressSpace.resolveOne(
|
|
+ ConstantExpr::create((uint64_t)errno_addr, Expr::Int64), result);
|
|
+ if (!resolved)
|
|
+ klee_error("Could not resolve memory object for errno");
|
|
+ int error = externalDispatcher->getLastErrno();
|
|
+ if (memcmp(result.second->concreteStore, &error, result.first->size) != 0) {
|
|
+ ObjectState *wos =
|
|
+ state.addressSpace.getWriteable(result.first, result.second);
|
|
+ memcpy(wos->concreteStore, &error, result.first->size);
|
|
+ }
|
|
+#endif
|
|
+
|
|
Type *resultType = target->inst->getType();
|
|
if (resultType != Type::getVoidTy(function->getContext())) {
|
|
ref<Expr> e = ConstantExpr::fromMemory((void*) args,
|
|
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
|
|
index 6c54d34b82bb..28546915b539 100644
|
|
--- a/lib/Core/ExternalDispatcher.cpp
|
|
+++ b/lib/Core/ExternalDispatcher.cpp
|
|
@@ -65,6 +65,7 @@ private:
|
|
llvm::Module *singleDispatchModule;
|
|
std::vector<std::string> moduleIDs;
|
|
std::string &getFreshModuleID();
|
|
+ int lastErrno;
|
|
|
|
public:
|
|
ExternalDispatcherImpl(llvm::LLVMContext &ctx);
|
|
@@ -72,6 +73,7 @@ public:
|
|
bool executeCall(llvm::Function *function, llvm::Instruction *i,
|
|
uint64_t *args);
|
|
void *resolveSymbol(const std::string &name);
|
|
+ int getLastErrno();
|
|
};
|
|
|
|
std::string &ExternalDispatcherImpl::getFreshModuleID() {
|
|
@@ -114,7 +116,8 @@ void *ExternalDispatcherImpl::resolveSymbol(const std::string &name) {
|
|
return addr;
|
|
}
|
|
|
|
-ExternalDispatcherImpl::ExternalDispatcherImpl(LLVMContext &ctx) : ctx(ctx) {
|
|
+ExternalDispatcherImpl::ExternalDispatcherImpl(LLVMContext &ctx)
|
|
+ : ctx(ctx), lastErrno(0) {
|
|
std::string error;
|
|
singleDispatchModule = new Module(getFreshModuleID(), ctx);
|
|
#if LLVM_VERSION_CODE < LLVM_VERSION(3, 6)
|
|
@@ -253,6 +256,8 @@ bool ExternalDispatcherImpl::runProtectedCall(Function *f, uint64_t *args) {
|
|
res = false;
|
|
} else {
|
|
executionEngine->runFunction(f, gvArgs);
|
|
+ // Explicitly acquire errno information
|
|
+ lastErrno = errno;
|
|
res = true;
|
|
}
|
|
|
|
@@ -346,6 +351,8 @@ Function *ExternalDispatcherImpl::createDispatcher(Function *target,
|
|
return dispatcher;
|
|
}
|
|
|
|
+int ExternalDispatcherImpl::getLastErrno() { return lastErrno; }
|
|
+
|
|
ExternalDispatcher::ExternalDispatcher(llvm::LLVMContext &ctx)
|
|
: impl(new ExternalDispatcherImpl(ctx)) {}
|
|
|
|
@@ -359,4 +366,6 @@ bool ExternalDispatcher::executeCall(llvm::Function *function,
|
|
void *ExternalDispatcher::resolveSymbol(const std::string &name) {
|
|
return impl->resolveSymbol(name);
|
|
}
|
|
+
|
|
+int ExternalDispatcher::getLastErrno() { return impl->getLastErrno(); }
|
|
}
|
|
diff --git a/lib/Core/ExternalDispatcher.h b/lib/Core/ExternalDispatcher.h
|
|
index c64dc7d81b93..e407355d6692 100644
|
|
--- a/lib/Core/ExternalDispatcher.h
|
|
+++ b/lib/Core/ExternalDispatcher.h
|
|
@@ -40,6 +40,8 @@ public:
|
|
bool executeCall(llvm::Function *function, llvm::Instruction *i,
|
|
uint64_t *args);
|
|
void *resolveSymbol(const std::string &name);
|
|
+
|
|
+ int getLastErrno();
|
|
};
|
|
}
|
|
|
|
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
|
|
index 4e5c87346917..afb41390d071 100644
|
|
--- a/lib/Core/Memory.h
|
|
+++ b/lib/Core/Memory.h
|
|
@@ -153,7 +153,10 @@ private:
|
|
|
|
const MemoryObject *object;
|
|
|
|
+public:
|
|
uint8_t *concreteStore;
|
|
+
|
|
+private:
|
|
// XXX cleanup name of flushMask (its backwards or something)
|
|
BitArray *concreteMask;
|
|
|
|
--
|
|
2.15.1
|
|
|