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/Executor.cpp52
-rw-r--r--lib/Core/Executor.h3
-rw-r--r--lib/Core/ExternalDispatcher.cpp19
-rw-r--r--lib/Core/ExternalDispatcher.h3
-rw-r--r--lib/Core/Memory.h1
-rw-r--r--lib/Core/SpecialFunctionHandler.cpp40
-rw-r--r--lib/Core/SpecialFunctionHandler.h1
7 files changed, 112 insertions, 7 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 81b9ec3c..7b054e5b 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -524,14 +524,18 @@ void Executor::initializeGlobals(ExecutionState &state) {
     globalAddresses.insert(std::make_pair(f, addr));
   }
 
+#ifndef WINDOWS
+  int *errno_addr = getErrnoLocation(state);
+  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.
 #ifdef HAVE_CTYPE_EXTERNALS
 #ifndef WINDOWS
 #ifndef DARWIN
-  /* From /usr/include/errno.h: it [errno] is a per-thread variable. */
-  int *errno_addr = __errno_location();
-  addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, false);
-
   /* from /usr/include/ctype.h:
        These point into arrays of 384, so they can be indexed by any `unsigned
        char' value [0,255]; by EOF (-1); or by any `signed char' value
@@ -3035,7 +3039,28 @@ void Executor::callExternalFunction(ExecutionState &state,
     }
   }
 
+  // Prepare external memory for invoking the function
   state.addressSpace.copyOutConcretes();
+#ifndef WINDOWS
+  // Update external errno state with local state value
+  int *errno_addr = getErrnoLocation(state);
+  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");
+  ref<Expr> errValueExpr = result.second->read(0, sizeof(*errno_addr) * 8);
+  ConstantExpr *errnoValue = dyn_cast<ConstantExpr>(errValueExpr);
+  if (!errnoValue) {
+    terminateStateOnExecError(state,
+                              "external call with errno value symbolic: " +
+                                  function->getName());
+    return;
+  }
+
+  externalDispatcher->setLastErrno(
+      errnoValue->getZExtValue(sizeof(*errno_addr) * 8));
+#endif
 
   if (!SuppressExternalWarnings) {
 
@@ -3055,6 +3080,7 @@ void Executor::callExternalFunction(ExecutionState &state,
     else
       klee_warning_once(function, "%s", os.str().c_str());
   }
+
   bool success = externalDispatcher->executeCall(function, target->inst, args);
   if (!success) {
     terminateStateOnError(state, "failed external call: " + function->getName(),
@@ -3068,6 +3094,13 @@ void Executor::callExternalFunction(ExecutionState &state,
     return;
   }
 
+#ifndef WINDOWS
+  // Update errno memory object with the errno value from the call
+  int error = externalDispatcher->getLastErrno();
+  state.addressSpace.copyInConcrete(result.first, result.second,
+                                    (uint64_t)&error);
+#endif
+
   Type *resultType = target->inst->getType();
   if (resultType != Type::getVoidTy(function->getContext())) {
     ref<Expr> e = ConstantExpr::fromMemory((void*) args, 
@@ -3814,6 +3847,17 @@ void Executor::prepareForEarlyExit() {
     statsTracker->done();
   }
 }
+
+/// Returns the errno location in memory
+int *Executor::getErrnoLocation(const ExecutionState &state) const {
+#ifndef __APPLE__
+  /* From /usr/include/errno.h: it [errno] is a per-thread variable. */
+  return __errno_location();
+#else
+  return __error();
+#endif
+}
+
 ///
 
 Interpreter *Interpreter::create(LLVMContext &ctx, const InterpreterOptions &opts,
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 71b1f5f7..1bc91be0 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -525,6 +525,9 @@ public:
 
   Expr::Width getWidthForLLVMType(llvm::Type *type) const;
   size_t getAllocationAlignment(const llvm::Value *allocSite) const;
+
+  /// Returns the errno location in memory of the state
+  int *getErrnoLocation(const ExecutionState &state) const;
 };
   
 } // End klee namespace
diff --git a/lib/Core/ExternalDispatcher.cpp b/lib/Core/ExternalDispatcher.cpp
index 6c54d34b..70c14050 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,8 @@ public:
   bool executeCall(llvm::Function *function, llvm::Instruction *i,
                    uint64_t *args);
   void *resolveSymbol(const std::string &name);
+  int getLastErrno();
+  void setLastErrno(int newErrno);
 };
 
 std::string &ExternalDispatcherImpl::getFreshModuleID() {
@@ -114,7 +117,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)
@@ -252,7 +256,10 @@ bool ExternalDispatcherImpl::runProtectedCall(Function *f, uint64_t *args) {
   if (setjmp(escapeCallJmpBuf)) {
     res = false;
   } else {
+    errno = lastErrno;
     executionEngine->runFunction(f, gvArgs);
+    // Explicitly acquire errno information
+    lastErrno = errno;
     res = true;
   }
 
@@ -346,6 +353,11 @@ Function *ExternalDispatcherImpl::createDispatcher(Function *target,
   return dispatcher;
 }
 
+int ExternalDispatcherImpl::getLastErrno() { return lastErrno; }
+void ExternalDispatcherImpl::setLastErrno(int newErrno) {
+  lastErrno = newErrno;
+}
+
 ExternalDispatcher::ExternalDispatcher(llvm::LLVMContext &ctx)
     : impl(new ExternalDispatcherImpl(ctx)) {}
 
@@ -359,4 +371,9 @@ bool ExternalDispatcher::executeCall(llvm::Function *function,
 void *ExternalDispatcher::resolveSymbol(const std::string &name) {
   return impl->resolveSymbol(name);
 }
+
+int ExternalDispatcher::getLastErrno() { return impl->getLastErrno(); }
+void ExternalDispatcher::setLastErrno(int newErrno) {
+  impl->setLastErrno(newErrno);
+}
 }
diff --git a/lib/Core/ExternalDispatcher.h b/lib/Core/ExternalDispatcher.h
index c64dc7d8..7c3a1d79 100644
--- a/lib/Core/ExternalDispatcher.h
+++ b/lib/Core/ExternalDispatcher.h
@@ -40,6 +40,9 @@ public:
   bool executeCall(llvm::Function *function, llvm::Instruction *i,
                    uint64_t *args);
   void *resolveSymbol(const std::string &name);
+
+  int getLastErrno();
+  void setLastErrno(int newErrno);
 };
 }
 
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index 3084cf32..e854502c 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -154,6 +154,7 @@ private:
   const MemoryObject *object;
 
   uint8_t *concreteStore;
+
   // XXX cleanup name of flushMask (its backwards or something)
   BitArray *concreteMask;
 
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 6587c30b..75456856 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -91,6 +91,11 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
   add("klee_define_fixed_object", handleDefineFixedObject, false),
   add("klee_get_obj_size", handleGetObjSize, true),
   add("klee_get_errno", handleGetErrno, true),
+#ifndef __APPLE__
+  add("__errno_location", handleErrnoLocation, true),
+#else
+  add("__error", handleErrnoLocation, true),
+#endif
   add("klee_is_symbolic", handleIsSymbolic, true),
   add("klee_make_symbolic", handleMakeSymbolic, false),
   add("klee_mark_global", handleMarkGlobal, false),
@@ -578,10 +583,41 @@ void SpecialFunctionHandler::handleGetErrno(ExecutionState &state,
   // XXX should type check args
   assert(arguments.size()==0 &&
          "invalid number of arguments to klee_get_errno");
-  executor.bindLocal(target, state,
-                     ConstantExpr::create(errno, Expr::Int32));
+#ifndef WINDOWS
+  int *errno_addr = executor.getErrnoLocation(state);
+#else
+  int *errno_addr = nullptr;
+#endif
+
+  // Retrieve the memory object of the errno variable
+  ObjectPair result;
+  bool resolved = state.addressSpace.resolveOne(
+      ConstantExpr::create((uint64_t)errno_addr, Expr::Int64), result);
+  if (!resolved)
+    executor.terminateStateOnError(state, "Could not resolve address for errno",
+                                   Executor::User);
+  executor.bindLocal(target, state, result.second->read(0, Expr::Int32));
 }
 
+void SpecialFunctionHandler::handleErrnoLocation(
+    ExecutionState &state, KInstruction *target,
+    std::vector<ref<Expr> > &arguments) {
+  // Returns the address of the errno variable
+  assert(arguments.size() == 0 &&
+         "invalid number of arguments to __errno_location/__error");
+
+#ifndef WINDOWS
+  int *errno_addr = executor.getErrnoLocation(state);
+#else
+  int *errno_addr = nullptr;
+#endif
+
+  executor.bindLocal(
+      target, state,
+      ConstantExpr::create((uint64_t)errno_addr,
+                           executor.kmodule->targetData->getTypeSizeInBits(
+                               target->inst->getType())));
+}
 void SpecialFunctionHandler::handleCalloc(ExecutionState &state,
                             KInstruction *target,
                             std::vector<ref<Expr> > &arguments) {
diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h
index 7e58018f..b11a4974 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -107,6 +107,7 @@ namespace klee {
     HANDLER(handleDelete);    
     HANDLER(handleDeleteArray);
     HANDLER(handleExit);
+    HANDLER(handleErrnoLocation);
     HANDLER(handleAliasFunction);
     HANDLER(handleFree);
     HANDLER(handleGetErrno);
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-25 13:23:23 +0000