X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/90136cb8268510961005b533a970c61282a1f37c..a45a65d79c6316b4bf515722f53d85a7080eeeb6:/src/mc/ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 7bc9774812..eb12028b75 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -38,7 +38,6 @@ ModelChecker::ModelChecker(std::unique_ptr<RemoteClient> process)
     , signal_event_(nullptr)
     , page_store_(500)
     , process_(std::move(process))
-    , parent_snapshot_(nullptr)
 {
 
 }
@@ -54,17 +53,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,6 +70,8 @@ void ModelChecker::start()
   int status;
 
   // The model-checked process SIGSTOP itself to signal it's ready:
+  const pid_t pid = process_->pid();
+
   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");
@@ -130,7 +126,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();
@@ -145,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().dumpStack();
+  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()
@@ -173,8 +171,7 @@ static void MC_report_assertion_error()
 bool ModelChecker::handle_message(char* buffer, ssize_t size)
 {
   s_mc_message_t base_message;
-  if (size < (ssize_t) sizeof(base_message))
-    xbt_die("Broken message");
+  xbt_assert(size >= (ssize_t)sizeof(base_message), "Broken message");
   memcpy(&base_message, buffer, sizeof(base_message));
 
   switch(base_message.type) {
@@ -182,8 +179,7 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
   case MC_MESSAGE_IGNORE_HEAP:
     {
     s_mc_message_ignore_heap_t message;
-    if (size != sizeof(message))
-      xbt_die("Broken messsage");
+    xbt_assert(size == sizeof(message), "Broken messsage");
     memcpy(&message, buffer, sizeof(message));
 
     IgnoredHeapRegion region;
@@ -198,8 +194,7 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
   case MC_MESSAGE_UNIGNORE_HEAP:
     {
     s_mc_message_ignore_memory_t message;
-    if (size != sizeof(message))
-      xbt_die("Broken messsage");
+    xbt_assert(size == sizeof(message), "Broken messsage");
     memcpy(&message, buffer, sizeof(message));
     process().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
     break;
@@ -208,8 +203,7 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
   case MC_MESSAGE_IGNORE_MEMORY:
     {
     s_mc_message_ignore_memory_t message;
-    if (size != sizeof(message))
-      xbt_die("Broken messsage");
+    xbt_assert(size == sizeof(message), "Broken messsage");
     memcpy(&message, buffer, sizeof(message));
     this->process().ignore_region(message.addr, message.size);
     break;
@@ -218,8 +212,7 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
   case MC_MESSAGE_STACK_REGION:
     {
     s_mc_message_stack_region_t message;
-    if (size != sizeof(message))
-      xbt_die("Broken messsage");
+    xbt_assert(size == sizeof(message), "Broken messsage");
     memcpy(&message, buffer, sizeof(message));
     this->process().stack_areas().push_back(message.stack_region);
     }
@@ -228,11 +221,9 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
   case MC_MESSAGE_REGISTER_SYMBOL:
     {
     s_mc_message_register_symbol_t message;
-    if (size != sizeof(message))
-      xbt_die("Broken message");
+    xbt_assert(size == sizeof(message), "Broken message");
     memcpy(&message, buffer, sizeof(message));
-    if (message.callback)
-      xbt_die("Support for client-side function proposition is not implemented.");
+    xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
     XBT_DEBUG("Received symbol: %s", message.name);
 
     if (simgrid::mc::property_automaton == nullptr)
@@ -273,7 +264,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)) {
@@ -303,10 +294,8 @@ void ModelChecker::handle_waitpid()
     if (pid == -1) {
       if (errno == ECHILD) {
         // No more children:
-        if (this->process().running())
-          xbt_die("Inconsistent state");
-        else
-          break;
+        xbt_assert(not this->process().running(), "Inconsistent state");
+        break;
       } else {
         XBT_ERROR("Could not wait for pid");
         throw simgrid::xbt::errno_error();
@@ -318,8 +307,7 @@ void ModelChecker::handle_waitpid()
       // 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");
+        xbt_assert(ptrace(PTRACE_GETEVENTMSG, this->process().pid(), 0, &status) != -1, "Could not get exit status");
         if (WIFSIGNALED(status)) {
           MC_report_crash(status);
           mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
@@ -336,11 +324,13 @@ void ModelChecker::handle_waitpid()
 #elif defined BSD
         ptrace(PT_CONTINUE, this->process().pid(), (caddr_t)1, WSTOPSIG(status));
 #endif
-        if (errno != 0)
-          xbt_die("Could not PTRACE_CONT");
+        xbt_assert(errno == 0, "Could not PTRACE_CONT");
       }
 
-      else if (WIFEXITED(status) || WIFSIGNALED(status)) {
+      else if (WIFSIGNALED(status)) {
+        MC_report_crash(status);
+        mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+      } else if (WIFEXITED(status)) {
         XBT_DEBUG("Child process is over");
         this->process().terminate();
       }
@@ -366,9 +356,9 @@ void ModelChecker::handle_simcall(Transition const& transition)
   s_mc_message_simcall_handle_t m;
   memset(&m, 0, sizeof(m));
   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
-  m.pid   = transition.pid;
-  m.value = transition.argument;
-  this->process_->getChannel().send(m);
+  m.pid   = transition.pid_;
+  m.value = transition.argument_;
+  this->process_->get_channel().send(m);
   this->process_->clear_cache();
   if (this->process_->running())
     event_base_dispatch(base_);
@@ -376,19 +366,16 @@ void ModelChecker::handle_simcall(Transition const& transition)
 
 bool ModelChecker::checkDeadlock()
 {
-  int res;
-  if ((res = this->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK)))
-    xbt_die("Could not check deadlock state");
+  int res = this->process().get_channel().send(MC_MESSAGE_DEADLOCK_CHECK);
+  xbt_assert(res == 0, "Could not check deadlock state");
   s_mc_message_int_t message;
-  ssize_t s = mc_model_checker->process().getChannel().receive(message);
-  if (s == -1)
-    xbt_die("Could not receive message");
-  if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
-    xbt_die("Received unexpected message %s (%i, size=%i) "
-      "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
-      MC_message_type_name(message.type), (int) message.type, (int) s,
-      (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
-      );
+  ssize_t s = mc_model_checker->process().get_channel().receive(message);
+  xbt_assert(s != -1, "Could not receive message");
+  xbt_assert(s == sizeof(message) && message.type == MC_MESSAGE_DEADLOCK_CHECK_REPLY,
+             "Received unexpected message %s (%i, size=%i) "
+             "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
+             MC_message_type_name(message.type), (int)message.type, (int)s, (int)MC_MESSAGE_DEADLOCK_CHECK_REPLY,
+             (int)sizeof(message));
   return message.value != 0;
 }