X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/6ae5ae138e9dd397b95d9e7741a5b28f194705d0..ccc29a54c4232f89ec04a60173b492bb26cb02ce:/src/mc/ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index d60341e051..338c107806 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -14,6 +14,7 @@
 #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");
@@ -71,7 +72,7 @@ void ModelChecker::start()
   // The model-checked process SIGSTOP itself to signal it's ready:
   const pid_t pid = process_->pid();
 
-  pid_t res = waitpid(pid, &status, WUNTRACED | WAITPID_CHECKED_FLAGS);
+  pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS);
   if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
     xbt_die("Could not wait model-checked process");
 
@@ -82,8 +83,14 @@ void ModelChecker::start()
 
   setup_ignore();
 
-  if (kill(pid, SIGCONT) != 0)
-    throw simgrid::xbt::errno_error("Could not wake up the model-checked process");
+#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
 }
 
 static const std::pair<const char*, const char*> ignored_local_variables[] = {
@@ -134,17 +141,19 @@ static void MC_report_crash(int status)
     XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
   else if (WIFEXITED(status))
     XBT_INFO("From exit: %i", WEXITSTATUS(status));
-  if (WCOREDUMP(status))
-    XBT_INFO("A core dump was generated by the system.");
-  else
-    XBT_INFO("No core dump was generated by the system.");
+  if (not xbt_log_no_loc)
+    XBT_INFO("%s core dump was generated by the system.", WCOREDUMP(status) ? "A" : "No");
   XBT_INFO("Counter-example execution trace:");
   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().dump_stack();
+  if (xbt_log_no_loc) {
+    XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
+  } else {
+    XBT_INFO("Stack trace:");
+    mc_model_checker->process().dump_stack();
+  }
 }
 
 static void MC_report_assertion_error()
@@ -303,9 +312,36 @@ void ModelChecker::handle_waitpid()
     }
 
     if (pid == this->process().pid()) {
-      xbt_assert(WIFEXITED(status) || WIFSIGNALED(status));
-      XBT_DEBUG("Child process is over");
-      this->process().terminate();
+
+      // 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();
+      }
     }
   }
 }