[mc] Only #include LivenessChecker.hpp in LivenessChecker.cpp

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

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 0d80488..6e9b7b6 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -9,6 +9,8 @@
 #include <cstddef>
 #include <cstdint>
 
+#include <cxxabi.h>
+
 #include <vector>
 
 #include "mc_base.h"
@@ -29,10 +31,10 @@
 #include "src/mc/mc_request.h"
 #include "src/mc/mc_safety.h"
 #include "src/mc/mc_snapshot.h"
-#include "src/mc/LivenessChecker.hpp"
 #include "src/mc/mc_private.h"
 #include "src/mc/mc_unw.h"
 #include "src/mc/mc_smx.h"
+#include "src/mc/Checker.hpp"
 #endif
 
 #include "src/mc/mc_record.h"
@@ -55,11 +57,10 @@ std::vector<double> processes_time;
 int user_max_depth_reached = 0;
 
 /* MC global data structures */
-mc_state_t mc_current_state = nullptr;
+simgrid::mc::State* mc_current_state = nullptr;
 char mc_replay_mode = false;
 
 mc_stats_t mc_stats = nullptr;
-mc_global_t initial_global_state = nullptr;
 xbt_fifo_t mc_stack = nullptr;
 
 /* Liveness */
@@ -67,6 +68,7 @@ xbt_fifo_t mc_stack = nullptr;
 namespace simgrid {
 namespace mc {
 
+std::unique_ptr<s_mc_global_t> initial_global_state = nullptr;
 xbt_automaton_t property_automaton = nullptr;
 
 }
@@ -120,14 +122,14 @@ void MC_replay(xbt_fifo_t stack)
   char *req_str;
   smx_simcall_t req = nullptr, saved_req = NULL;
   xbt_fifo_item_t item, start_item;
-  mc_state_t state;
+  simgrid::mc::State* state;
   
   XBT_DEBUG("**** Begin Replay ****");
 
   /* Intermediate backtracking */
   if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) {
     start_item = xbt_fifo_get_first_item(stack);
-    state = (mc_state_t)xbt_fifo_get_item_content(start_item);
+    state = (simgrid::mc::State*)xbt_fifo_get_item_content(start_item);
     if(state->system_state){
       simgrid::mc::restore_snapshot(state->system_state);
       if(_sg_mc_comms_determinism || _sg_mc_send_determinism) 
@@ -138,7 +140,7 @@ void MC_replay(xbt_fifo_t stack)
 
 
   /* Restore the initial state */
-  simgrid::mc::restore_snapshot(initial_global_state->snapshot);
+  simgrid::mc::restore_snapshot(simgrid::mc::initial_global_state->snapshot);
   /* At the moment of taking the snapshot the raw heap was set, so restoring
    * it will set it back again, we have to unset it to continue  */
 
@@ -160,7 +162,7 @@ void MC_replay(xbt_fifo_t stack)
        item != xbt_fifo_get_first_item(stack);
        item = xbt_fifo_get_prev_item(item)) {
 
-    state = (mc_state_t) xbt_fifo_get_item_content(item);
+    state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
     saved_req = MC_state_get_executed_request(state, &value);
     
     if (saved_req) {
@@ -215,16 +217,18 @@ void MC_show_deadlock(void)
 void MC_print_statistics(mc_stats_t stats)
 {
   if(_sg_mc_comms_determinism) {
-    if (!initial_global_state->recv_deterministic && initial_global_state->send_deterministic){
+    if (!simgrid::mc::initial_global_state->recv_deterministic &&
+        simgrid::mc::initial_global_state->send_deterministic){
       XBT_INFO("******************************************************");
       XBT_INFO("**** Only-send-deterministic communication pattern ****");
       XBT_INFO("******************************************************");
-      XBT_INFO("%s", initial_global_state->recv_diff);
-    }else if(!initial_global_state->send_deterministic && initial_global_state->recv_deterministic) {
+      XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
+    }else if(!simgrid::mc::initial_global_state->send_deterministic &&
+        simgrid::mc::initial_global_state->recv_deterministic) {
       XBT_INFO("******************************************************");
       XBT_INFO("**** Only-recv-deterministic communication pattern ****");
       XBT_INFO("******************************************************");
-      XBT_INFO("%s", initial_global_state->send_diff);
+      XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
     }
   }
 
@@ -240,10 +244,13 @@ void MC_print_statistics(mc_stats_t stats)
     fprintf(dot_output, "}\n");
     fclose(dot_output);
   }
-  if (initial_global_state != nullptr && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) {
-    XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes");
+  if (simgrid::mc::initial_global_state != nullptr
+      && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) {
+    XBT_INFO("Send-deterministic : %s",
+      !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes");
     if (_sg_mc_comms_determinism)
-      XBT_INFO("Recv-deterministic : %s", !initial_global_state->recv_deterministic ? "No" : "Yes");
+      XBT_INFO("Recv-deterministic : %s",
+        !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes");
   }
   if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
     int ret=system("free");
@@ -270,16 +277,24 @@ void dumpStack(FILE* file, unw_cursor_t cursor)
   unw_word_t off;
   do {
     const char * name = !unw_get_proc_name(&cursor, buffer, 100, &off) ? buffer : "?";
+
+    int status;
+
+    // Demangle C++ names:
+    char* realname = abi::__cxa_demangle(name, 0, 0, &status);
+
 #if defined(__x86_64__)
     unw_word_t rip = 0;
     unw_word_t rsp = 0;
     unw_get_reg(&cursor, UNW_X86_64_RIP, &rip);
     unw_get_reg(&cursor, UNW_X86_64_RSP, &rsp);
     fprintf(file, "  %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n",
-      nframe, name, (std::uint64_t) rip, (std::uint64_t) rsp);
+      nframe, realname ? realname : name, (std::uint64_t) rip, (std::uint64_t) rsp);
 #else
-    fprintf(file, "  %i: %s\n", nframe, name);
+    fprintf(file, "  %i: %s\n", nframe, realname ? realname : name);
 #endif
+
+    free(realname);
     ++nframe;
   } while(unw_step(&cursor));
 }