X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2f2db04b850386899392bc06568f17f071f8620f..32b33834115ef974885e0227b9f47a1e756ee04c:/src/mc/ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 10f0ba30c6..cec73c6b33 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -23,66 +23,11 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
 
 ::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
 
-#ifdef __linux__
-# define WAITPID_CHECKED_FLAGS __WALL
-#else
-# define WAITPID_CHECKED_FLAGS 0
-#endif
-
 namespace simgrid::mc {
 
-ModelChecker::ModelChecker(std::unique_ptr<RemoteProcessMemory> remote_memory, int sockfd)
-    : checker_side_(sockfd), remote_process_memory_(std::move(remote_memory))
-{
-}
-
-void ModelChecker::start()
+ModelChecker::ModelChecker(std::unique_ptr<RemoteProcessMemory> remote_memory)
+    : remote_process_memory_(std::move(remote_memory))
 {
-  checker_side_.start(
-      [](evutil_socket_t sig, short events, void* arg) {
-        auto mc = static_cast<simgrid::mc::ModelChecker*>(arg);
-        if (events == EV_READ) {
-          std::array<char, MC_MESSAGE_LENGTH> buffer;
-          ssize_t size = mc->checker_side_.get_channel().receive(buffer.data(), buffer.size(), false);
-          if (size == -1 && errno != EAGAIN)
-            throw simgrid::xbt::errno_error();
-
-          if (not mc->handle_message(buffer.data(), size))
-            mc->checker_side_.break_loop();
-        } else if (events == EV_SIGNAL) {
-          if (sig == SIGCHLD)
-            mc->handle_waitpid();
-          else
-            xbt_die("Unexpected signal: %d", sig);
-        } else {
-          xbt_die("Unexpected event");
-        }
-      },
-      this);
-
-  XBT_DEBUG("Waiting for the model-checked process");
-  int status;
-
-  // The model-checked process SIGSTOP itself to signal it's ready:
-  const pid_t pid = remote_process_memory_->pid();
-
-  xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
-             "Could not wait model-checked process");
-
-  errno = 0;
-#ifdef __linux__
-  ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
-  ptrace(PTRACE_CONT, pid, 0, 0);
-#elif defined BSD
-  ptrace(PT_CONTINUE, pid, (caddr_t)1, 0);
-#else
-# error "no ptrace equivalent coded for this platform"
-#endif
-  xbt_assert(errno == 0,
-             "Ptrace does not seem to be usable in your setup (errno: %d). "
-             "If you run from within a docker, adding `--cap-add SYS_PTRACE` to the docker line may help. "
-             "If it does not help, please report this bug.",
-             errno);
 }
 
 bool ModelChecker::handle_message(const char* buffer, ssize_t size)
@@ -163,15 +108,14 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
   return true;
 }
 
-void ModelChecker::handle_waitpid()
+void ModelChecker::handle_waitpid(pid_t pid_to_wait)
 {
   XBT_DEBUG("Check for wait event");
   int status;
   pid_t pid;
   while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
     if (pid == -1) {
-      if (errno == ECHILD) {
-        // No more children:
+      if (errno == ECHILD) { // No more children:
         xbt_assert(not this->get_remote_process_memory().running(), "Inconsistent state");
         break;
       } else {
@@ -180,13 +124,12 @@ void ModelChecker::handle_waitpid()
       }
     }
 
-    if (pid == this->get_remote_process_memory().pid()) {
+    if (pid == pid_to_wait) {
       // From PTRACE_O_TRACEEXIT:
 #ifdef __linux__
       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
         unsigned long eventmsg;
-        xbt_assert(ptrace(PTRACE_GETEVENTMSG, get_remote_process_memory().pid(), 0, &eventmsg) != -1,
-                   "Could not get exit status");
+        xbt_assert(ptrace(PTRACE_GETEVENTMSG, pid_to_wait, 0, &eventmsg) != -1, "Could not get exit status");
         status = static_cast<int>(eventmsg);
         if (WIFSIGNALED(status))
           exploration_->report_crash(status);
@@ -198,9 +141,9 @@ void ModelChecker::handle_waitpid()
         XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
         errno = 0;
 #ifdef __linux__
-        ptrace(PTRACE_CONT, get_remote_process_memory().pid(), 0, WSTOPSIG(status));
+        ptrace(PTRACE_CONT, pid_to_wait, 0, WSTOPSIG(status));
 #elif defined BSD
-        ptrace(PT_CONTINUE, get_remote_process_memory().pid(), (caddr_t)1, WSTOPSIG(status));
+        ptrace(PT_CONTINUE, pid_to_wait, (caddr_t)1, WSTOPSIG(status));
 #endif
         xbt_assert(errno == 0, "Could not PTRACE_CONT");
       }
@@ -215,31 +158,4 @@ void ModelChecker::handle_waitpid()
   }
 }
 
-Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition)
-{
-  s_mc_message_simcall_execute_t m = {};
-  m.type              = MessageType::SIMCALL_EXECUTE;
-  m.aid_              = aid;
-  m.times_considered_ = times_considered;
-  checker_side_.get_channel().send(m);
-
-  this->remote_process_memory_->clear_cache();
-  if (this->remote_process_memory_->running())
-    checker_side_.dispatch(); // The app may send messages while processing the transition
-
-  s_mc_message_simcall_execute_answer_t answer;
-  ssize_t s = checker_side_.get_channel().receive(answer);
-  xbt_assert(s != -1, "Could not receive message");
-  xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer);
-  xbt_assert(answer.type == MessageType::SIMCALL_EXECUTE_ANSWER,
-             "Received unexpected message %s (%i); expected MessageType::SIMCALL_EXECUTE_ANSWER (%i)",
-             to_c_str(answer.type), (int)answer.type, (int)MessageType::SIMCALL_EXECUTE_ANSWER);
-
-  if (new_transition) {
-    std::stringstream stream(answer.buffer.data());
-    return deserialize_transition(aid, times_considered, stream);
-  } else
-    return nullptr;
-}
-
 } // namespace simgrid::mc