src/mc/explo/Exploration.cpp

   1 /* Copyright (c) 2016-2023. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "src/mc/explo/Exploration.hpp"
   7 #include "src/mc/mc_config.hpp"
   8 #include "src/mc/mc_exit.hpp"
   9 #include "src/mc/mc_private.hpp"
  10 #include "src/mc/sosp/RemoteProcessMemory.hpp"
  11
  12 #include <sys/wait.h>
  13
  14 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_explo, mc, "Generic exploration algorithm of the model-checker");
  15
  16 namespace simgrid::mc {
  17
  18 static simgrid::config::Flag<std::string> cfg_dot_output_file{
  19     "model-check/dot-output", "Name of dot output file corresponding to graph state", ""};
  20
  21 Exploration* Exploration::instance_ = nullptr; // singleton instance
  22
  23 Exploration::Exploration(const std::vector<char*>& args, bool need_memory_introspection)
  24     : remote_app_(std::make_unique<RemoteApp>(args, need_memory_introspection))
  25 {
  26   xbt_assert(instance_ == nullptr, "Cannot have more than one exploration instance");
  27   instance_ = this;
  28
  29   if (not cfg_dot_output_file.get().empty()) {
  30     dot_output_ = fopen(cfg_dot_output_file.get().c_str(), "w");
  31     xbt_assert(dot_output_ != nullptr, "Error open dot output file: %s", strerror(errno));
  32
  33     fprintf(dot_output_, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node "
  34                          "[fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
  35   }
  36 }
  37
  38 Exploration::~Exploration()
  39 {
  40   if (dot_output_ != nullptr)
  41     fclose(dot_output_);
  42   instance_ = nullptr;
  43 }
  44
  45 void Exploration::dot_output(const char* fmt, ...)
  46 {
  47   if (dot_output_ != nullptr) {
  48     va_list ap;
  49     va_start(ap, fmt);
  50     vfprintf(dot_output_, fmt, ap);
  51     va_end(ap);
  52     fflush(dot_output_);
  53   }
  54 }
  55
  56 void Exploration::log_state()
  57 {
  58   if (not cfg_dot_output_file.get().empty()) {
  59     dot_output("}\n");
  60     fclose(dot_output_);
  61   }
  62   if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")) {
  63     int ret = system("free");
  64     if (ret != 0)
  65       XBT_WARN("Call to system(free) did not return 0, but %d", ret);
  66   }
  67 }
  68
  69 void Exploration::report_crash(int status)
  70 {
  71   XBT_INFO("**************************");
  72   XBT_INFO("** CRASH IN THE PROGRAM **");
  73   XBT_INFO("**************************");
  74   if (WIFSIGNALED(status))
  75     XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
  76   else if (WIFEXITED(status))
  77     XBT_INFO("From exit: %i", WEXITSTATUS(status));
  78   if (not xbt_log_no_loc)
  79     XBT_INFO("%s core dump was generated by the system.", WCOREDUMP(status) ? "A" : "No");
  80
  81   XBT_INFO("Counter-example execution trace:");
  82   for (auto const& s : get_textual_trace())
  83     XBT_INFO("  %s", s.c_str());
  84   XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
  85            "--cfg=model-check/replay:'%s'",
  86            get_record_trace().to_string().c_str());
  87   log_state();
  88   if (xbt_log_no_loc) {
  89     XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
  90   } else {
  91     auto* memory = get_remote_app().get_remote_process_memory();
  92     if (memory) {
  93       XBT_INFO("Stack trace:");
  94       memory->dump_stack();
  95     } else {
  96       XBT_INFO("Stack trace not shown because there is no memory introspection.");
  97     }
  98   }
  99
 100   system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
 101 }
 102 void Exploration::report_assertion_failure()
 103 {
 104   XBT_INFO("**************************");
 105   XBT_INFO("*** PROPERTY NOT VALID ***");
 106   XBT_INFO("**************************");
 107   XBT_INFO("Counter-example execution trace:");
 108   for (auto const& s : get_textual_trace())
 109     XBT_INFO("  %s", s.c_str());
 110   XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
 111            "--cfg=model-check/replay:'%s'",
 112            get_record_trace().to_string().c_str());
 113   log_state();
 114   system_exit(SIMGRID_MC_EXIT_SAFETY);
 115 }
 116
 117 void Exploration::system_exit(int status)
 118 {
 119   ::exit(status);
 120 }
 121
 122 }; // namespace simgrid::mc