Kill mc::api::get_remote_app()

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 9a22666..d09a9ad 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -125,7 +125,7 @@ void ModelChecker::resume()
   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 **");
@@ -136,12 +136,12 @@ 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");
-  if (mc_model_checker->get_exploration()) {
+  if (explorer) {
     XBT_INFO("Counter-example execution trace:");
-    for (auto const& s : mc_model_checker->get_exploration()->get_textual_trace())
+    for (auto const& s : explorer->get_textual_trace())
       XBT_INFO("  %s", s.c_str());
-    XBT_INFO("Path = %s", mc_model_checker->get_exploration()->get_record_trace().to_string().c_str());
-    Api::get().get_remote_app().log_state();
+    XBT_INFO("Path = %s", explorer->get_record_trace().to_string().c_str());
+    explorer->get_remote_app().log_state();
     if (xbt_log_no_loc) {
       XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
     } else {
@@ -233,7 +233,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       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());
-      Api::get().get_remote_app().log_state();
+      exploration_->get_remote_app().log_state();
 
       this->exit(SIMGRID_MC_EXIT_SAFETY);
 
@@ -273,7 +273,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);
         }
@@ -293,7 +293,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)) {

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 346ed7e..fda31aa 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -71,7 +71,6 @@ public:
   simgrid::mc::Snapshot* take_snapshot(long num_state) const;
 
   // SESSION APIs
-  simgrid::mc::RemoteApp const& get_remote_app() const { return *remote_app_; }
   void s_close();
 
   // AUTOMATION APIs

diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp
index 1099126..24b2227 100644 (file)
--- a/src/mc/explo/CommunicationDeterminismChecker.cpp
+++ b/src/mc/explo/CommunicationDeterminismChecker.cpp
@@ -60,9 +60,14 @@ struct PatternCommunicationList {
 
 /********** Checker extension **********/
 
-struct CommDetExtension {
+class CommDetExtension {
+  Exploration& exploration_;
+
+public:
   static simgrid::xbt::Extension<simgrid::mc::Exploration, CommDetExtension> EXTENSION_ID;
 
+  explicit CommDetExtension(Exploration& explo) : exploration_(explo) {}
+
   std::vector<simgrid::mc::PatternCommunicationList> initial_communications_pattern;
   std::vector<std::vector<simgrid::mc::PatternCommunication*>> incomplete_communications_pattern;
 
@@ -72,9 +77,9 @@ struct CommDetExtension {
   std::string send_diff;
   std::string recv_diff;
 
-  void exploration_start(RemoteApp& remote_app)
+  void exploration_start()
   {
-    const unsigned long maxpid = remote_app.get_maxpid();
+    const unsigned long maxpid = exploration_.get_remote_app().get_maxpid();
 
     initial_communications_pattern.resize(maxpid);
     incomplete_communications_pattern.resize(maxpid);
@@ -202,7 +207,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC
       XBT_INFO("***** Non-send-deterministic communications pattern *****");
       XBT_INFO("*********************************************************");
       XBT_INFO("%s", send_diff.c_str());
-      Api::get().get_remote_app().log_state();
+      exploration_.get_remote_app().log_state();
       mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
     } else if (_sg_mc_comms_determinism && (not send_deterministic && not recv_deterministic)) {
       XBT_INFO("****************************************************");
@@ -212,7 +217,7 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC
         XBT_INFO("%s", send_diff.c_str());
       if (not recv_diff.empty())
         XBT_INFO("%s", recv_diff.c_str());
-      Api::get().get_remote_app().log_state();
+      exploration_.get_remote_app().log_state();
       mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
     }
   }
@@ -321,11 +326,12 @@ Exploration* create_communication_determinism_checker(RemoteApp& remote_app)
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
-  auto extension = new CommDetExtension();
+  auto base      = new DFSExplorer(remote_app);
+  auto extension = new CommDetExtension(*base);
 
-  DFSExplorer::on_exploration_start([extension, &remote_app]() {
+  DFSExplorer::on_exploration_start([extension]() {
     XBT_INFO("Check communication determinism");
-    extension->exploration_start(remote_app);
+    extension->exploration_start();
   });
   DFSExplorer::on_backtracking([extension]() { extension->initial_communications_pattern_done = true; });
   DFSExplorer::on_state_creation(
@@ -368,7 +374,7 @@ Exploration* create_communication_determinism_checker(RemoteApp& remote_app)
     delete extension;
   });
 
-  return new DFSExplorer(remote_app);
+  return base;
 }
 
 } // namespace simgrid::mc