X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/de0765cca8da736799b534113602a9cb8bc32809..a28f8d4f0a7734d65dafa41486ca0ab78038a975:/src/mc/ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 785d614320..4411458d65 100644
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -22,14 +22,13 @@
 
 #include "simgrid/sg_config.h"
 
-#include "ModelChecker.hpp"
-#include "PageStore.hpp"
-#include "ModelChecker.hpp"
-#include "mc_protocol.h"
-#include "mc_private.h"
-#include "mc_ignore.h"
-#include "mcer_ignore.h"
-#include "mc_exit.h"
+#include "src/mc/ModelChecker.hpp"
+#include "src/mc/PageStore.hpp"
+#include "src/mc/ModelChecker.hpp"
+#include "src/mc/mc_protocol.h"
+#include "src/mc/mc_private.h"
+#include "src/mc/mc_ignore.h"
+#include "src/mc/mc_exit.h"
 #include "src/mc/mc_liveness.h"
 
 extern "C" {
@@ -55,6 +54,7 @@ ModelChecker::ModelChecker(pid_t pid, int socket) :
   page_store_(500),
   parent_snapshot_(nullptr)
 {
+
 }
 
 ModelChecker::~ModelChecker()
@@ -74,6 +74,14 @@ const char* ModelChecker::get_host_name(const char* hostname)
   return elt->key;
 }
 
+// HACK, for the unit test only
+void ModelChecker::init_process()
+{
+  // TODO, avoid direct dependency on sg_cfg
+  process_ = std::unique_ptr<Process>(new Process(pid_, socket_));
+  process_->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
+}
+
 void ModelChecker::start()
 {
   // Block SIGCHLD (this will be handled with accept/signalfd):
@@ -110,12 +118,7 @@ void ModelChecker::start()
   if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
     xbt_die("Could not wait model-checked process");
 
-  assert(process_ == nullptr);
-  process_ = std::unique_ptr<Process>(new Process(pid_, socket_));
-  // TODO, avoid direct dependency on sg_cfg
-  process_->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
-
-  mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
+  this->init_process();
 
   /* Initialize statistics */
   mc_stats = xbt_new0(s_mc_stats_t, 1);
@@ -133,31 +136,36 @@ void ModelChecker::start()
   ptrace(PTRACE_CONT, pid_, 0, 0);
 }
 
-void ModelChecker::setup_ignore()
-{
-  /* 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");
+static const std::pair<const char*, const char*> ignored_local_variables[] = {
+  std::pair<const char*, const char*>{  "e", "*" },
+  std::pair<const char*, const char*>{ "__ex_cleanup", "*" },
+  std::pair<const char*, const char*>{ "__ex_mctx_en", "*" },
+  std::pair<const char*, const char*>{ "__ex_mctx_me", "*" },
+  std::pair<const char*, const char*>{ "__xbt_ex_ctx_ptr", "*" },
+  std::pair<const char*, const char*>{ "_log_ev", "*" },
+  std::pair<const char*, const char*>{ "_throw_ctx", "*" },
+  std::pair<const char*, const char*>{ "ctx", "*" },
+
+  std::pair<const char*, const char*>{ "self", "simcall_BODY_mc_snapshot" },
+  std::pair<const char*, const char*>{ "next_context", "smx_ctx_sysv_suspend_serial" },
+  std::pair<const char*, const char*>{ "i", "smx_ctx_sysv_suspend_serial" },
 
   /* Ignore local variable about time used for tracing */
-  MC_ignore_local_variable("start_time", "*");
+  std::pair<const char*, const char*>{ "start_time", "*" },
+};
+
+void ModelChecker::setup_ignore()
+{
+  Process& process = this->process();
+  for (std::pair<const char*, const char*> const& var :
+      ignored_local_variables)
+    process.ignore_local_variable(var.first, var.second);
 
   /* Static variable used for tracing */
-  MCer_ignore_global_variable("counter");
+  process.ignore_global_variable("counter");
 
   /* SIMIX */
-  MCer_ignore_global_variable("smx_total_comms");
+  process.ignore_global_variable("smx_total_comms");
 }
 
 void ModelChecker::shutdown()
@@ -205,9 +213,13 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
       if (size != sizeof(message))
         xbt_die("Broken messsage");
       memcpy(&message, buffer, sizeof(message));
-      mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
-      *region = message.region;
-      MC_heap_region_ignore_insert(region);
+
+      IgnoredHeapRegion region;
+      region.block = message.block;
+      region.fragment = message.fragment;
+      region.address = message.address;
+      region.size = message.size;
+      process().ignore_heap(region);
       break;
     }
 
@@ -217,7 +229,7 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
       if (size != sizeof(message))
         xbt_die("Broken messsage");
       memcpy(&message, buffer, sizeof(message));
-      MC_heap_region_ignore_remove(
+      process().unignore_heap(
         (void *)(std::uintptr_t) message.addr, message.size);
       break;
     }
@@ -238,9 +250,7 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size)
       if (size != sizeof(message))
         xbt_die("Broken messsage");
       memcpy(&message, buffer, sizeof(message));
-      stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
-      *stack_region = message.stack_region;
-      MC_stack_area_add(stack_region);
+      this->process().stack_areas().push_back(message.stack_region);
     }
     break;