X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/c74cd8ff2a61ce60dcbb71c6b169c51c1085e059..2e501076bf39bf43b598954f040b453fedf49f4c:/src/mc/mc_global.cpp

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index d9680d80be..86891d46cb 100644
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -6,9 +6,10 @@
 
 #include <cinttypes>
 
-#include <assert.h>
-#include <string.h>
-#include <stdint.h>
+#include <cassert>
+#include <cstddef>
+#include <cstdint>
+#include <cstring>
 
 #include "mc_base.h"
 
@@ -27,7 +28,6 @@
 #include "mc_record.h"
 
 #ifdef HAVE_MC
-#include "mc_server.h"
 #include <libunwind.h>
 #include <xbt/mmalloc.h>
 #include "../xbt/mmalloc/mmprivate.h"
@@ -35,7 +35,6 @@
 #include "mc_comm_pattern.h"
 #include "mc_request.h"
 #include "mc_safety.h"
-#include "mc_memory_map.h"
 #include "mc_snapshot.h"
 #include "mc_liveness.h"
 #include "mc_private.h"
@@ -63,8 +62,6 @@ int user_max_depth_reached = 0;
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
 
-__thread mc_comparison_times_t mc_comp_times = NULL;
-__thread double mc_snapshot_comparison_time;
 mc_stats_t mc_stats = NULL;
 mc_global_t initial_global_state = NULL;
 xbt_fifo_t mc_stack = NULL;
@@ -80,7 +77,7 @@ const char *colors[13];
 /*******************************  Initialisation of MC *******************************/
 /*********************************************************************************/
 
-static void MC_init_dot_output()
+void MC_init_dot_output()
 {                               /* FIXME : more colors */
 
   colors[0] = "blue";
@@ -127,46 +124,6 @@ void MC_init()
   }
 }
 
-void MC_init_model_checker(pid_t pid, int socket)
-{
-  mc_model_checker = new simgrid::mc::ModelChecker(pid, socket);
-
-  mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
-
-  /* Initialize statistics */
-  mc_stats = xbt_new0(s_mc_stats_t, 1);
-  mc_stats->state_size = 1;
-
-  if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0'))
-    MC_init_dot_output();
-
-  /* Init parmap */
-  //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
-
-  /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
-  MC_ignore_local_variable("e", "*");
-  MC_ignore_local_variable("__ex_cleanup", "*");
-  MC_ignore_local_variable("__ex_mctx_en", "*");
-  MC_ignore_local_variable("__ex_mctx_me", "*");
-  MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
-  MC_ignore_local_variable("_log_ev", "*");
-  MC_ignore_local_variable("_throw_ctx", "*");
-  MC_ignore_local_variable("ctx", "*");
-
-  MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
-  MC_ignore_local_variable("next_cont"
-    "ext", "smx_ctx_sysv_suspend_serial");
-  MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
-
-  /* Ignore local variable about time used for tracing */
-  MC_ignore_local_variable("start_time", "*");
-
-  /* Static variable used for tracing */
-  MCer_ignore_global_variable("counter");
-
-  /* SIMIX */
-  MCer_ignore_global_variable("smx_total_comms");
-}
 #endif
 
 /*******************************  Core of MC *******************************/
@@ -304,7 +261,7 @@ void MC_replay(xbt_fifo_t stack)
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
         MC_handle_comm_pattern(call, req, value, NULL, 1);
 
-      MC_wait_for_requests();
+      mc_model_checker->wait_for_requests();
 
       count++;
     }
@@ -371,7 +328,7 @@ void MC_replay_liveness(xbt_fifo_t stack)
         }
 
         MC_simcall_handle(req, value);
-        MC_wait_for_requests();
+        mc_model_checker->wait_for_requests();
       }
 
       /* Update statistics */
@@ -507,8 +464,10 @@ void MC_print_statistics(mc_stats_t stats)
     if (_sg_mc_comms_determinism)
       XBT_INFO("Recv-deterministic : %s", !initial_global_state->recv_deterministic ? "No" : "Yes");
   }
-  if (getenv("SIMGRID_MC_SYSTEM_STATISTICS"))
-    system("free");
+  if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
+    int ret=system("free");
+    if(ret!=0)XBT_WARN("system call did not return 0, but %d",ret);
+  }
 }
 
 void MC_automaton_load(const char *file)
@@ -542,7 +501,7 @@ void MC_dump_stacks(FILE* file)
       unw_get_reg(&c, UNW_X86_64_RIP, &rip);
       unw_get_reg(&c, UNW_X86_64_RSP, &rsp);
       fprintf(file, "  %i: %s (RIP=0x%" PRIx64 " RSP=0x%" PRIx64 ")\n",
-        nframe, name, rip, rsp);
+        nframe, name, (std::uint64_t) rip, (std::uint64_t) rsp);
 #else
       fprintf(file, "  %i: %s\n", nframe, name);
 #endif
@@ -583,6 +542,25 @@ void MC_report_assertion_error(void)
   MC_print_statistics(mc_stats);
 }
 
+void MC_report_crash(int status)
+{
+  XBT_INFO("**************************");
+  XBT_INFO("** CRASH IN THE PROGRAM **");
+  XBT_INFO("**************************");
+  if (WIFSIGNALED(status))
+    XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
+  else if (WIFEXITED(status))
+    XBT_INFO("From exit: %i", WEXITSTATUS(status));
+  if (WCOREDUMP(status))
+    XBT_INFO("A core dump was generated by the system.");
+  else
+    XBT_INFO("No core dump was generated by the system.");
+  XBT_INFO("Counter-example execution trace:");
+  MC_record_dump_path(mc_stack);
+  MC_dump_stack_safety(mc_stack);
+  MC_print_statistics(mc_stats);
+}
+
 void MC_invalidate_cache(void)
 {
   if (mc_model_checker)