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

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 8804000bfe..10f0ba30c6 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -69,8 +69,6 @@ void ModelChecker::start()
   xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
              "Could not wait model-checked process");
 
-  setup_ignore();
-
   errno = 0;
 #ifdef __linux__
   ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
@@ -87,59 +85,6 @@ void ModelChecker::start()
              errno);
 }
 
-static constexpr auto ignored_local_variables = {
-    std::make_pair("e", "*"),
-    std::make_pair("_log_ev", "*"),
-
-    /* Ignore local variable about time used for tracing */
-    std::make_pair("start_time", "*"),
-};
-
-void ModelChecker::setup_ignore()
-{
-  const RemoteProcessMemory& process = this->get_remote_process_memory();
-  for (auto const& [var, frame] : ignored_local_variables)
-    process.ignore_local_variable(var, frame);
-
-  /* Static variable used for tracing */
-  process.ignore_global_variable("counter");
-}
-
-void ModelChecker::resume()
-{
-  if (checker_side_.get_channel().send(MessageType::CONTINUE) != 0)
-    throw xbt::errno_error();
-  remote_process_memory_->clear_cache();
-}
-
-static void MC_report_crash(Exploration* explorer, int status)
-{
-  XBT_INFO("**************************");
-  XBT_INFO("** CRASH IN THE PROGRAM **");
-  XBT_INFO("**************************");
-  if (WIFSIGNALED(status))
-    XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
-  else if (WIFEXITED(status))
-    XBT_INFO("From exit: %i", WEXITSTATUS(status));
-  if (not xbt_log_no_loc)
-    XBT_INFO("%s core dump was generated by the system.", WCOREDUMP(status) ? "A" : "No");
-  if (explorer) {
-    XBT_INFO("Counter-example execution trace:");
-    for (auto const& s : explorer->get_textual_trace())
-      XBT_INFO("  %s", s.c_str());
-    XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
-             "--cfg=model-check/replay:'%s'",
-             explorer->get_record_trace().to_string().c_str());
-    explorer->log_state();
-    if (xbt_log_no_loc) {
-      XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
-    } else {
-      XBT_INFO("Stack trace:");
-      explorer->get_remote_app().get_remote_process_memory().dump_stack();
-    }
-  }
-}
-
 bool ModelChecker::handle_message(const char* buffer, ssize_t size)
 {
   s_mc_message_t base_message;
@@ -209,18 +154,8 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       return false;
 
     case MessageType::ASSERTION_FAILED:
-      XBT_INFO("**************************");
-      XBT_INFO("*** PROPERTY NOT VALID ***");
-      XBT_INFO("**************************");
-      XBT_INFO("Counter-example execution trace:");
-      for (auto const& s : get_exploration()->get_textual_trace())
-        XBT_INFO("  %s", s.c_str());
-      XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
-               "--cfg=model-check/replay:'%s'",
-               get_exploration()->get_record_trace().to_string().c_str());
-      exploration_->log_state();
-
-      this->exit(SIMGRID_MC_EXIT_SAFETY);
+      exploration_->report_assertion_failure();
+      break;
 
     default:
       xbt_die("Unexpected message from model-checked application");
@@ -228,13 +163,6 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
   return true;
 }
 
-/** Terminate the model-checker application */
-void ModelChecker::exit(int status)
-{
-  get_exploration()->get_remote_app().shutdown();
-  ::exit(status);
-}
-
 void ModelChecker::handle_waitpid()
 {
   XBT_DEBUG("Check for wait event");
@@ -260,11 +188,8 @@ void ModelChecker::handle_waitpid()
         xbt_assert(ptrace(PTRACE_GETEVENTMSG, get_remote_process_memory().pid(), 0, &eventmsg) != -1,
                    "Could not get exit status");
         status = static_cast<int>(eventmsg);
-        if (WIFSIGNALED(status)) {
-          MC_report_crash(exploration_, status);
-          this->get_remote_process_memory().terminate();
-          this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
-        }
+        if (WIFSIGNALED(status))
+          exploration_->report_crash(status);
       }
 #endif
 
@@ -281,9 +206,7 @@ void ModelChecker::handle_waitpid()
       }
 
       else if (WIFSIGNALED(status)) {
-        MC_report_crash(exploration_, status);
-        this->get_remote_process_memory().terminate();
-        this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+        exploration_->report_crash(status);
       } else if (WIFEXITED(status)) {
         XBT_DEBUG("Child process is over");
         this->get_remote_process_memory().terminate();
@@ -292,13 +215,6 @@ void ModelChecker::handle_waitpid()
   }
 }
 
-void ModelChecker::wait_for_requests()
-{
-  this->resume();
-  if (this->get_remote_process_memory().running())
-    checker_side_.dispatch();
-}
-
 Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition)
 {
   s_mc_message_simcall_execute_t m = {};