X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e920a5835d1d64051bb56c25d5ed9f3e0665c0fa..497aee08bf8b36b4981083b79d8473991db1ccde:/src/mc/ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 2dccd7abdd..17e2bce738 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -4,8 +4,8 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "src/mc/ModelChecker.hpp"
-#include "src/mc/Session.hpp"
-#include "src/mc/checker/Checker.hpp"
+#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/LivenessChecker.hpp"
 #include "src/mc/mc_config.hpp"
 #include "src/mc/mc_exit.hpp"
 #include "src/mc/mc_private.hpp"
@@ -23,16 +23,13 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
 
 ::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
 
-using simgrid::mc::remote;
-
 #ifdef __linux__
 # define WAITPID_CHECKED_FLAGS __WALL
 #else
 # define WAITPID_CHECKED_FLAGS 0
 #endif
 
-namespace simgrid {
-namespace mc {
+namespace simgrid::mc {
 
 ModelChecker::ModelChecker(std::unique_ptr<RemoteProcess> remote_simulation, int sockfd)
     : checker_side_(sockfd), remote_process_(std::move(remote_simulation))
@@ -70,11 +67,17 @@ 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();
 
+  errno = 0;
 #ifdef __linux__
   ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
   ptrace(PTRACE_CONT, pid, 0, 0);
@@ -83,6 +86,21 @@ void ModelChecker::start()
 #else
 # error "no ptrace equivalent coded for this platform"
 #endif
+  xbt_assert(errno == 0,
+             "Ptrace does not seem to be usable in your setup (errno: %d). "
+             "If you run from within a docker, adding `--cap-add SYS_PTRACE` to the docker line may help. "
+             "If it does not help, please report this bug.",
+             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 = {
@@ -96,8 +114,8 @@ static constexpr auto ignored_local_variables = {
 void ModelChecker::setup_ignore()
 {
   const RemoteProcess& process = this->get_remote_process();
-  for (auto const& var : ignored_local_variables)
-    process.ignore_local_variable(var.first, var.second);
+  for (auto const& [var, frame] : ignored_local_variables)
+    process.ignore_local_variable(var, frame);
 
   /* Static variable used for tracing */
   process.ignore_global_variable("counter");
@@ -118,13 +136,12 @@ void ModelChecker::shutdown()
 
 void ModelChecker::resume()
 {
-  int res = checker_side_.get_channel().send(MessageType::CONTINUE);
-  if (res)
+  if (checker_side_.get_channel().send(MessageType::CONTINUE) != 0)
     throw xbt::errno_error();
   remote_process_->clear_cache();
 }
 
-static void MC_report_crash(int status)
+static void MC_report_crash(Exploration* explorer, int status)
 {
   XBT_INFO("**************************");
   XBT_INFO("** CRASH IN THE PROGRAM **");
@@ -135,16 +152,18 @@ static void MC_report_crash(int 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");
-  XBT_INFO("Counter-example execution trace:");
-  for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
-    XBT_INFO("  %s", s.c_str());
-  XBT_INFO("Path = %s", mc_model_checker->getChecker()->get_record_trace().to_string().c_str());
-  session_singleton->log_state();
-  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->get_remote_process().dump_stack();
+  if (explorer) {
+    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());
+    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:");
+      mc_model_checker->get_remote_process().dump_stack();
+    }
   }
 }
 
@@ -160,7 +179,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message));
       memcpy(&message, buffer, sizeof(message));
 
-      get_remote_process().init(message.mmalloc_default_mdp, message.maxpid, message.actors, message.dead_actors);
+      get_remote_process().init(message.mmalloc_default_mdp, message.maxpid);
       break;
     }
 
@@ -208,14 +227,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
       XBT_DEBUG("Received symbol: %s", message.name.data());
 
-      if (property_automaton == nullptr)
-        property_automaton = xbt_automaton_new();
-
-      const RemoteProcess* process    = &this->get_remote_process();
-      RemotePtr<int> address          = remote((int*)message.data);
-      xbt::add_proposition(property_automaton, message.name.data(),
-                           [process, address]() { return process->read(address); });
-
+      LivenessChecker::automaton_register_symbol(get_remote_process(), message.name.data(), remote((int*)message.data));
       break;
     }
 
@@ -227,10 +239,10 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       XBT_INFO("*** PROPERTY NOT VALID ***");
       XBT_INFO("**************************");
       XBT_INFO("Counter-example execution trace:");
-      for (auto const& s : getChecker()->get_textual_trace())
+      for (auto const& s : get_exploration()->get_textual_trace())
         XBT_INFO("  %s", s.c_str());
-      XBT_INFO("Path = %s", getChecker()->get_record_trace().to_string().c_str());
-      session_singleton->log_state();
+      XBT_INFO("Path = %s", get_exploration()->get_record_trace().to_string().c_str());
+      exploration_->log_state();
 
       this->exit(SIMGRID_MC_EXIT_SAFETY);
 
@@ -270,7 +282,7 @@ void ModelChecker::handle_waitpid()
       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
         xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &status) != -1, "Could not get exit status");
         if (WIFSIGNALED(status)) {
-          MC_report_crash(status);
+          MC_report_crash(exploration_, status);
           this->get_remote_process().terminate();
           this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
         }
@@ -290,7 +302,7 @@ void ModelChecker::handle_waitpid()
       }
 
       else if (WIFSIGNALED(status)) {
-        MC_report_crash(status);
+        MC_report_crash(exploration_, status);
         this->get_remote_process().terminate();
         this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
       } else if (WIFEXITED(status)) {
@@ -346,22 +358,11 @@ void ModelChecker::finalize_app(bool terminate_asap)
   xbt_assert(checker_side_.get_channel().send(m) == 0, "Could not ask the app to finalize on need");
 
   s_mc_message_t answer;
-  xbt_assert(checker_side_.get_channel().receive(answer) != -1, "Could not receive answer to FINALIZE");
-}
-
-bool ModelChecker::checkDeadlock()
-{
-  xbt_assert(checker_side_.get_channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state");
-  s_mc_message_int_t message;
-  ssize_t s = checker_side_.get_channel().receive(message);
-  xbt_assert(s != -1, "Could not receive message");
-  xbt_assert(s == sizeof(message) && message.type == MessageType::DEADLOCK_CHECK_REPLY,
-             "Received unexpected message %s (%i, size=%i) "
-             "expected MessageType::DEADLOCK_CHECK_REPLY (%i, size=%i)",
-             to_c_str(message.type), (int)message.type, (int)s, (int)MessageType::DEADLOCK_CHECK_REPLY,
-             (int)sizeof(message));
-  return message.value != 0;
+  ssize_t s = checker_side_.get_channel().receive(answer);
+  xbt_assert(s != -1, "Could not receive answer to FINALIZE");
+  xbt_assert(s == sizeof(answer) && answer.type == MessageType::FINALIZE_REPLY,
+             "Received unexpected message %s (%i, size=%i) expected MessageType::FINALIZE_REPLY (%i, size=%i)",
+             to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::FINALIZE_REPLY, (int)sizeof(answer));
 }
 
-} // namespace mc
-} // namespace simgrid
+} // namespace simgrid::mc