SafetyChecker::backtrack() calls mc_api functions

[simgrid.git] / src / mc / checker / CommunicationDeterminismChecker.cpp

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index cf114b11f5fd4804f4db85c5ffb417726790a150..d94b12ad286ac49fdad325da9d54f7b133e36fa4 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -106,7 +106,7 @@ static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern,
   comm_pattern->dst_proc = dst_proc->get_pid();
   comm_pattern->src_host = MC_smx_actor_get_host_name(src_proc);
   comm_pattern->dst_host = MC_smx_actor_get_host_name(dst_proc);
-  if (comm_pattern->data.size() == 0 && comm->src_buff_ != nullptr) {
+  if (comm_pattern->data.empty() && comm->src_buff_ != nullptr) {
     size_t buff_size;
     mc_model_checker->get_remote_simulation().read(&buff_size, remote(comm->dst_buff_size_));
     comm_pattern->data.resize(buff_size);
@@ -127,12 +127,12 @@ void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, co
 
     if (diff != NONE_DIFF) {
       if (comm->type == PatternCommunicationType::send) {
-        this->send_deterministic = 0;
+        this->send_deterministic = false;
         if (this->send_diff != nullptr)
           xbt_free(this->send_diff);
         this->send_diff = print_determinism_result(diff, process, comm, list.index_comm + 1);
       } else {
-        this->recv_deterministic = 0;
+        this->recv_deterministic = false;
         if (this->recv_diff != nullptr)
           xbt_free(this->recv_diff);
         this->recv_diff = print_determinism_result(diff, process, comm, list.index_comm + 1);
@@ -176,7 +176,7 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_
   const mc::PatternCommunicationList& initial_pattern          = initial_communications_pattern[issuer->get_pid()];
   const std::vector<PatternCommunication*>& incomplete_pattern = incomplete_communications_pattern[issuer->get_pid()];
 
-  std::unique_ptr<PatternCommunication> pattern(new PatternCommunication());
+  auto pattern   = std::make_unique<PatternCommunication>();
   pattern->index = initial_pattern.index_comm + incomplete_pattern.size();
 
   if (call_type == MC_CALL_TYPE_SEND) {
@@ -185,9 +185,8 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_
     pattern->comm_addr = static_cast<kernel::activity::CommImpl*>(simcall_comm_isend__getraw__result(request));
 
     Remote<kernel::activity::CommImpl> temp_synchro;
-    mc_model_checker->get_remote_simulation().read(
-        temp_synchro, remote(static_cast<kernel::activity::CommImpl*>(pattern->comm_addr)));
-    const kernel::activity::CommImpl* synchro = static_cast<kernel::activity::CommImpl*>(temp_synchro.get_buffer());
+    mc_model_checker->get_remote_simulation().read(temp_synchro, remote(pattern->comm_addr));
+    const kernel::activity::CommImpl* synchro = temp_synchro.get_buffer();
 
     char* remote_name = mc_model_checker->get_remote_simulation().read<char*>(RemotePtr<char*>(
         (uint64_t)(synchro->get_mailbox() ? &synchro->get_mailbox()->name_ : &synchro->mbox_cpy->name_)));
@@ -198,8 +197,8 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_
 
 #if HAVE_SMPI
     simgrid::smpi::Request mpi_request;
-    mc_model_checker->process().read(&mpi_request,
-                                     remote(static_cast<smpi::Request*>(simcall_comm_isend__get__data(request))));
+    mc_model_checker->get_remote_simulation().read(
+        &mpi_request, remote(static_cast<smpi::Request*>(simcall_comm_isend__get__data(request))));
     pattern->tag = mpi_request.tag();
 #endif
 
@@ -227,14 +226,13 @@ void CommunicationDeterminismChecker::get_comm_pattern(smx_simcall_t request, e_
 
 #if HAVE_SMPI
     smpi::Request mpi_request;
-    mc_model_checker->process().read(&mpi_request,
-                                     remote(static_cast<smpi::Request*>(simcall_comm_irecv__get__data(request))));
+    mc_model_checker->get_remote_simulation().read(
+        &mpi_request, remote(static_cast<smpi::Request*>(simcall_comm_irecv__get__data(request))));
     pattern->tag = mpi_request.tag();
 #endif
 
     Remote<kernel::activity::CommImpl> temp_comm;
-    mc_model_checker->get_remote_simulation().read(
-        temp_comm, remote(static_cast<kernel::activity::CommImpl*>(pattern->comm_addr)));
+    mc_model_checker->get_remote_simulation().read(temp_comm, remote(pattern->comm_addr));
     const kernel::activity::CommImpl* comm = temp_comm.get_buffer();
 
     char* remote_name;
@@ -335,7 +333,8 @@ void CommunicationDeterminismChecker::prepare()
   initial_communications_pattern.resize(maxpid);
   incomplete_communications_pattern.resize(maxpid);
 
-  std::unique_ptr<State> initial_state(new State(++expanded_states_count_));
+  ++expanded_states_count_;
+  auto initial_state = std::make_unique<State>(expanded_states_count_);
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
@@ -392,7 +391,7 @@ void CommunicationDeterminismChecker::restoreState()
        real one, pointed by the request field of the issuer process */
 
     const smx_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
-    smx_simcall_t req = &issuer->simcall;
+    smx_simcall_t req        = &issuer->simcall_;
 
     /* TODO : handle test and testany simcalls */
     e_mc_call_type_t call = MC_get_call_type(req);
@@ -453,7 +452,8 @@ void CommunicationDeterminismChecker::real_run()
       mc_model_checker->wait_for_requests();
 
       /* Create the new expanded state */
-      std::unique_ptr<State> next_state(new State(++expanded_states_count_));
+      ++expanded_states_count_;
+      auto next_state = std::make_unique<State>(expanded_states_count_);
 
       /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at
        * least, data are transferred). These communications  are incomplete and they cannot be analyzed and compared