[mc] Let the Checker give us the current trace

[simgrid.git] / src / mc / SafetyChecker.cpp

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index cccde0d..2c9ca22 100644 (file)
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -33,6 +33,26 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
 namespace simgrid {
 namespace mc {
 
+static void MC_show_non_termination(void)
+{
+  XBT_INFO("******************************************");
+  XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
+  XBT_INFO("******************************************");
+  XBT_INFO("Counter-example execution trace:");
+  for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+    XBT_INFO("%s", s.c_str());
+  MC_print_statistics(mc_stats);
+}
+
+static int snapshot_compare(mc_state_t state1, mc_state_t state2)
+{
+  simgrid::mc::Snapshot* s1 = state1->system_state;
+  simgrid::mc::Snapshot* s2 = state2->system_state;
+  int num1 = state1->num;
+  int num2 = state2->num;
+  return snapshot_compare(num1, s1, num2, s2);
+}
+
 static int is_exploration_stack_state(mc_state_t current_state){
 
   xbt_fifo_item_t item;
@@ -47,6 +67,44 @@ static int is_exploration_stack_state(mc_state_t current_state){
   return 0;
 }
 
+RecordTrace SafetyChecker::getRecordTrace() // override
+{
+  RecordTrace res;
+
+  xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack);
+  for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
+
+    // Find (pid, value):
+    mc_state_t state = (mc_state_t) xbt_fifo_get_item_content(item);
+    int value = 0;
+    smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
+    const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+    const int pid = issuer->pid;
+
+    res.push_back(RecordTraceElement(pid, value));
+  }
+
+  return std::move(res);
+}
+
+std::vector<std::string> SafetyChecker::getTextualTrace() // override
+{
+  std::vector<std::string> trace;
+  for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+       item; item = xbt_fifo_get_prev_item(item)) {
+    mc_state_t state = (mc_state_t)xbt_fifo_get_item_content(item);
+    int value;
+    smx_simcall_t req = MC_state_get_executed_request(state, &value);
+    if (req) {
+      char* req_str = simgrid::mc::request_to_string(
+        req, value, simgrid::mc::RequestType::executed);
+      trace.push_back(req_str);
+      xbt_free(req_str);
+    }
+  }
+  return std::move(trace);
+}
+
 int SafetyChecker::run()
 {
   this->init();
@@ -150,7 +208,7 @@ int SafetyChecker::run()
 
       /* Check for deadlocks */
       if (mc_model_checker->checkDeadlock()) {
-        MC_show_deadlock(nullptr);
+        MC_show_deadlock();
         return SIMGRID_MC_EXIT_DEADLOCK;
       }