Reduce dependency on ptrace.

[simgrid.git] / src / mc / ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 874875a..d60341e 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -14,7 +14,6 @@
 #include "xbt/automaton.hpp"
 #include "xbt/system_error.hpp"
 
-#include <sys/ptrace.h>
 #include <sys/wait.h>
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
@@ -38,7 +37,6 @@ ModelChecker::ModelChecker(std::unique_ptr<RemoteClient> process)
     , signal_event_(nullptr)
     , page_store_(500)
     , process_(std::move(process))
-    , parent_snapshot_(nullptr)
 {
 
 }
@@ -54,17 +52,12 @@ ModelChecker::~ModelChecker() {
 
 void ModelChecker::start()
 {
-  const pid_t pid = process_->pid();
-
   base_ = event_base_new();
   event_callback_fn event_callback = [](evutil_socket_t fd, short events, void *arg)
   {
     ((ModelChecker *)arg)->handle_events(fd, events);
   };
-  socket_event_ = event_new(base_,
-                            process_->getChannel().getSocket(),
-                            EV_READ|EV_PERSIST,
-                            event_callback, this);
+  socket_event_ = event_new(base_, process_->get_channel().get_socket(), EV_READ | EV_PERSIST, event_callback, this);
   event_add(socket_event_, NULL);
   signal_event_ = event_new(base_,
                             SIGCHLD,
@@ -76,7 +69,9 @@ void ModelChecker::start()
   int status;
 
   // The model-checked process SIGSTOP itself to signal it's ready:
-  pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS);
+  const pid_t pid = process_->pid();
+
+  pid_t res = waitpid(pid, &status, WUNTRACED | WAITPID_CHECKED_FLAGS);
   if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
     xbt_die("Could not wait model-checked process");
 
@@ -87,14 +82,8 @@ void ModelChecker::start()
 
   setup_ignore();
 
-#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
+  if (kill(pid, SIGCONT) != 0)
+    throw simgrid::xbt::errno_error("Could not wake up the model-checked process");
 }
 
 static const std::pair<const char*, const char*> ignored_local_variables[] = {
@@ -130,7 +119,7 @@ void ModelChecker::shutdown()
 
 void ModelChecker::resume(simgrid::mc::RemoteClient& process)
 {
-  int res = process.getChannel().send(MC_MESSAGE_CONTINUE);
+  int res = process.get_channel().send(MC_MESSAGE_CONTINUE);
   if (res)
     throw simgrid::xbt::errno_error();
   process.clear_cache();
@@ -150,12 +139,12 @@ static void MC_report_crash(int status)
   else
     XBT_INFO("No core dump was generated by the system.");
   XBT_INFO("Counter-example execution trace:");
-  for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
+  for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
   simgrid::mc::dumpRecordPath();
   simgrid::mc::session->log_state();
   XBT_INFO("Stack trace:");
-  mc_model_checker->process().dumpStack();
+  mc_model_checker->process().dump_stack();
 }
 
 static void MC_report_assertion_error()
@@ -164,7 +153,7 @@ static void MC_report_assertion_error()
   XBT_INFO("*** PROPERTY NOT VALID ***");
   XBT_INFO("**************************");
   XBT_INFO("Counter-example execution trace:");
-  for (auto const& s : mc_model_checker->getChecker()->getTextualTrace())
+  for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
     XBT_INFO("  %s", s.c_str());
   simgrid::mc::dumpRecordPath();
   simgrid::mc::session->log_state();
@@ -273,7 +262,7 @@ void ModelChecker::handle_events(int fd, short events)
 {
   if (events == EV_READ) {
     char buffer[MC_MESSAGE_LENGTH];
-    ssize_t size = process_->getChannel().receive(buffer, sizeof(buffer), false);
+    ssize_t size = process_->get_channel().receive(buffer, sizeof(buffer), false);
     if (size == -1 && errno != EAGAIN)
       throw simgrid::xbt::errno_error();
     if (not handle_message(buffer, size)) {
@@ -314,36 +303,9 @@ void ModelChecker::handle_waitpid()
     }
 
     if (pid == this->process().pid()) {
-
-      // From PTRACE_O_TRACEEXIT:
-#ifdef __linux__
-      if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
-        if (ptrace(PTRACE_GETEVENTMSG, this->process().pid(), 0, &status) == -1)
-          xbt_die("Could not get exit status");
-        if (WIFSIGNALED(status)) {
-          MC_report_crash(status);
-          mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
-        }
-      }
-#endif
-
-      // We don't care about signals, just reinject them:
-      if (WIFSTOPPED(status)) {
-        XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
-        errno = 0;
-#ifdef __linux__
-        ptrace(PTRACE_CONT, this->process().pid(), 0, WSTOPSIG(status));
-#elif defined BSD
-        ptrace(PT_CONTINUE, this->process().pid(), (caddr_t)1, WSTOPSIG(status));
-#endif
-        if (errno != 0)
-          xbt_die("Could not PTRACE_CONT");
-      }
-
-      else if (WIFEXITED(status) || WIFSIGNALED(status)) {
-        XBT_DEBUG("Child process is over");
-        this->process().terminate();
-      }
+      xbt_assert(WIFEXITED(status) || WIFSIGNALED(status));
+      XBT_DEBUG("Child process is over");
+      this->process().terminate();
     }
   }
 }
@@ -368,7 +330,7 @@ void ModelChecker::handle_simcall(Transition const& transition)
   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
   m.pid   = transition.pid;
   m.value = transition.argument;
-  this->process_->getChannel().send(m);
+  this->process_->get_channel().send(m);
   this->process_->clear_cache();
   if (this->process_->running())
     event_base_dispatch(base_);
@@ -377,10 +339,10 @@ void ModelChecker::handle_simcall(Transition const& transition)
 bool ModelChecker::checkDeadlock()
 {
   int res;
-  if ((res = this->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK)))
+  if ((res = this->process().get_channel().send(MC_MESSAGE_DEADLOCK_CHECK)))
     xbt_die("Could not check deadlock state");
   s_mc_message_int_t message;
-  ssize_t s = mc_model_checker->process().getChannel().receive(message);
+  ssize_t s = mc_model_checker->process().get_channel().receive(message);
   if (s == -1)
     xbt_die("Could not receive message");
   if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)