Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Message is retrieved as an unsigned long (according to the manual).
[simgrid.git] / src / mc / ModelChecker.cpp
index 9e24ee20f2e3de22060eea7e6752df722df1d2fa..051a8462d8be5ad40c65f35aa5bfbfb1d11d0b64 100644 (file)
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2022. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved.          */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
@@ -67,8 +67,13 @@ void ModelChecker::start()
   xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
              "Could not wait model-checked process");
 
-  if (not _sg_mc_dot_output_file.get().empty())
-    MC_init_dot_output();
+  if (not _sg_mc_dot_output_file.get().empty()) {
+    dot_output_ = fopen(_sg_mc_dot_output_file.get().c_str(), "w");
+    xbt_assert(dot_output_ != nullptr, "Error open dot output file: %s", strerror(errno));
+
+    fprintf(dot_output_, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node "
+                         "[fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
+  }
 
   setup_ignore();
 
@@ -88,6 +93,16 @@ void ModelChecker::start()
              errno);
 }
 
+void ModelChecker::dot_output(const char* fmt, ...)
+{
+  if (dot_output_ != nullptr) {
+    va_list ap;
+    va_start(ap, fmt);
+    vfprintf(dot_output_, fmt, ap);
+    va_end(ap);
+  }
+}
+
 static constexpr auto ignored_local_variables = {
     std::make_pair("e", "*"),
     std::make_pair("_log_ev", "*"),
@@ -141,7 +156,9 @@ static void MC_report_crash(Exploration* explorer, int status)
     XBT_INFO("Counter-example execution trace:");
     for (auto const& s : explorer->get_textual_trace())
       XBT_INFO("  %s", s.c_str());
-    XBT_INFO("Path = %s", explorer->get_record_trace().to_string().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");
@@ -226,7 +243,9 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       XBT_INFO("Counter-example execution trace:");
       for (auto const& s : get_exploration()->get_textual_trace())
         XBT_INFO("  %s", s.c_str());
-      XBT_INFO("Path = %s", get_exploration()->get_record_trace().to_string().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);
@@ -265,7 +284,9 @@ void ModelChecker::handle_waitpid()
       // From PTRACE_O_TRACEEXIT:
 #ifdef __linux__
       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
-        xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &status) != -1, "Could not get exit status");
+        unsigned long eventmsg;
+        xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->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().terminate();
@@ -307,8 +328,7 @@ void ModelChecker::wait_for_requests()
 
 Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition)
 {
-  s_mc_message_simcall_execute_t m;
-  memset(&m, 0, sizeof(m));
+  s_mc_message_simcall_execute_t m = {};
   m.type              = MessageType::SIMCALL_EXECUTE;
   m.aid_              = aid;
   m.times_considered_ = times_considered;
@@ -336,8 +356,7 @@ Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool n
 
 void ModelChecker::finalize_app(bool terminate_asap)
 {
-  s_mc_message_int_t m;
-  memset(&m, 0, sizeof m);
+  s_mc_message_int_t m = {};
   m.type  = MessageType::FINALIZE;
   m.value = terminate_asap;
   xbt_assert(checker_side_.get_channel().send(m) == 0, "Could not ask the app to finalize on need");