Execute concrete programs more eagerly

3 files changed, 13 insertions, 11 deletions

diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index d6639208..f3214fab 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -429,6 +429,8 @@ void ExecutionState::addConstraint(ref<Expr> e) {
   auto v = extractMetaEnvVar(e);
   if (!v.empty()) {
     this->patchLocs++;
+    if (!this->metaEnvVar.empty())
+      return; // one revision at once
     if (v.substr(v.size() - 2) != "=0")
       this->metaEnvVar = v;
     return;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index d26e5d04..056c6aad 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -489,8 +489,9 @@ unsigned dumpStates = 0, dumpExecutionTree = 0;
 Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
                    InterpreterHandler *ih)
     : Interpreter(opts), interpreterHandler(ih), searcher(0),
-      externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
-      pathWriter(0), symPathWriter(0), specialFunctionHandler(0), timers{time::Span(TimerInterval)},
+      externalDispatcher(new ExternalDispatcher(ctx)),
+      metaEnvVars{{0, ""}}, statsTracker(0), pathWriter(0), symPathWriter(0),
+      specialFunctionHandler(0), timers{time::Span(TimerInterval)},
       replayKTest(0), replayPath(0), usingSeeds(0),
       atMemoryLimit(false), inhibitForking(false), haltExecution(false),
       ivcEnabled(false), debugLogBuffer(debugBufferString),
@@ -3934,7 +3935,7 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
     }
   }
 
-  char buffer[128];
+  char buffer[128]; // output buffer for concrete execution
   for (const auto& rev : this->metaEnvVars) {
     auto& envs = rev.second;
     pid_t pid;
@@ -3956,12 +3957,12 @@ void Executor::extractDifferentiator(ExecutionState* a, ExecutionState* b,
                       envs.empty() ? NULL : envp);
     assert(!err);
     close(fildes[1]);
-    for (ssize_t n; n = read(fildes[0], buffer, 127);) {
+    for (unsigned char n; n = read(fildes[0], buffer, sizeof(buffer));) {
       assert(n >= 0);
-      buffer[n] = 0;
-      for (const unsigned char c : buffer)
-        outputs[rev.first].second.push_back(c);
+      for (unsigned char i = 0; i < n; ++i)
+        outputs[rev.first].second.push_back(buffer[i]);
     }
+    outputs[rev.first].second.push_back(0); // null termination
     posix_spawn_file_actions_destroy(&action);
   }
   this->diffTests[argv] = outputs;
@@ -4062,7 +4063,6 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
         terminationTypeFileExtension(StateTerminationType::Exit).c_str());
 
   interpreterHandler->incPathsCompleted();
-  metaEnvVars[state.patchNo] = state.metaEnvVar;
   if (exitStates[state.patchNo].insert(&state).second)
     searchDifferentiators(&state);
   terminateState(state, StateTerminationType::Exit);
@@ -4190,7 +4190,6 @@ void Executor::terminateStateOnError(ExecutionState &state,
     interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix);
   }
 
-  metaEnvVars[state.patchNo] = state.metaEnvVar;
   if (exitStates[state.patchNo].insert(&state).second)
     searchDifferentiators(&state);
   terminateState(state, terminationType);
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index 784bb8f1..8484a8a7 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -849,9 +849,10 @@ void SpecialFunctionHandler::handleMarkPatch(ExecutionState &state,
          "invalid number of arguments to klee_mark_patch");
   assert(isa<ConstantExpr>(arguments[0]) &&
          "expect constant patch number argument to klee_mark_patch");
-  if (state.patchNo)
+  auto patchNo = cast<ConstantExpr>(arguments[0])->getLimitedValue();
+  if (state.patchNo && patchNo != state.patchNo)
     executor.terminateStateEarly(state, "ignore patch combination",
                                  StateTerminationType::SilentExit);
   else
-    state.patchNo = cast<ConstantExpr>(arguments[0])->getLimitedValue();
+    executor.metaEnvVars[state.patchNo = patchNo] = state.metaEnvVar;
 }