[mc] Add Factor some gorry code to State::getRecordElement()

Avoid using should-be-private-stuff oustside of State.

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index 3c0cd08..6b6a331 100644 (file)
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -305,13 +305,8 @@ CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
 {
   RecordTrace res;
-  for (auto const& state : stack_) {
-    int value = 0;
-    smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
-    const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
-    const int pid = issuer->pid;
-    res.push_back(RecordTraceElement(pid, value));
-  }
+  for (auto const& state : stack_)
+    res.push_back(state->getRecordElement());
   return res;
 }
 

diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index 8dcb3b9..2837d43 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -296,15 +296,8 @@ LivenessChecker::~LivenessChecker()
 RecordTrace LivenessChecker::getRecordTrace() // override
 {
   RecordTrace res;
-  for (std::shared_ptr<Pair> const& pair : explorationStack_) {
-    int value;
-    smx_simcall_t req = MC_state_get_executed_request(pair->graph_state.get(), &value);
-    if (req && req->call != SIMCALL_NONE) {
-      smx_process_t issuer = MC_smx_simcall_get_issuer(req);
-      const int pid = issuer->pid;
-      res.push_back(RecordTraceElement(pid, value));
-    }
-  }
+  for (std::shared_ptr<Pair> const& pair : explorationStack_)
+    res.push_back(pair->graph_state->getRecordElement());
   return res;
 }
 

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 62a4f5c..7cdceed 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -67,13 +67,8 @@ bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state)
 RecordTrace SafetyChecker::getRecordTrace() // override
 {
   RecordTrace res;
-  for (auto const& state : stack_) {
-    int value = 0;
-    smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
-    const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
-    const int pid = issuer->pid;
-    res.push_back(RecordTraceElement(pid, value));
-  }
+  for (auto const& state : stack_)
+    res.push_back(state->getRecordElement());
   return res;
 }
 

diff --git a/src/mc/mc_smx.cpp b/src/mc/mc_smx.cpp
index b904885..d17f2b0 100644 (file)
--- a/src/mc/mc_smx.cpp
+++ b/src/mc/mc_smx.cpp
@@ -111,7 +111,7 @@ void Process::refresh_simix()
  *  @param process the MCed process
  *  @param req     the simcall (copied in the local process)
  */
-smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req)
+smx_process_t MC_smx_simcall_get_issuer(s_smx_simcall_t const* req)
 {
   if (mc_mode == MC_MODE_CLIENT)
     return req->issuer;

diff --git a/src/mc/mc_smx.h b/src/mc/mc_smx.h
index ba19d94..31534c0 100644 (file)
--- a/src/mc/mc_smx.h
+++ b/src/mc/mc_smx.h
@@ -52,7 +52,7 @@ XBT_PRIVATE void MC_process_smx_refresh(simgrid::mc::Process* process);
  *  @param process the MCed process
  *  @param req     the simcall (copied in the local process)
  */
-XBT_PRIVATE smx_process_t MC_smx_simcall_get_issuer(smx_simcall_t req);
+XBT_PRIVATE smx_process_t MC_smx_simcall_get_issuer(s_smx_simcall_t const* req);
 
 XBT_PRIVATE const char* MC_smx_process_get_name(smx_process_t p);
 XBT_PRIVATE const char* MC_smx_process_get_host_name(smx_process_t p);

diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp
index 1a88fb1..7a164f8 100644 (file)
--- a/src/mc/mc_state.cpp
+++ b/src/mc/mc_state.cpp
@@ -59,6 +59,12 @@ std::size_t State::interleaveSize() const
     [](simgrid::mc::ProcessState const& state) { return state.isToInterleave(); });
 }
 
+RecordTraceElement State::getRecordElement() const
+{
+  smx_process_t issuer = MC_smx_simcall_get_issuer(&this->executed_req);
+  return RecordTraceElement(issuer->pid, this->req_num);
+}
+
 }
 }
 

diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h
index fa5ddb9..c3d6190 100644 (file)
--- a/src/mc/mc_state.h
+++ b/src/mc/mc_state.h
@@ -16,6 +16,7 @@
 #include <simgrid_config.h>
 #include "src/simix/smx_private.h"
 #include "src/mc/mc_snapshot.h"
+#include "src/mc/mc_record.h"
 
 namespace simgrid {
 namespace mc {
@@ -156,6 +157,7 @@ struct XBT_PRIVATE State {
   {
     this->processStates[process->pid].interleave();
   }
+  RecordTraceElement getRecordElement() const;
 };
 
 XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);