[mc] Move stacks_areas into Process

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 30d1a54..7fb1dba 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -58,7 +58,6 @@ extern XBT_PRIVATE int _sg_mc_snapshot_fds;
 extern XBT_PRIVATE int _sg_mc_termination;
 
 extern XBT_PRIVATE xbt_dynar_t mc_heap_comparison_ignore;
-extern XBT_PRIVATE xbt_dynar_t stacks_areas;
 
 /********************************* Global *************************************/
 
@@ -79,7 +78,6 @@ XBT_PRIVATE void _mc_cfg_cb_send_determinism(const char *name, int pos);
 XBT_PRIVATE void _mc_cfg_cb_termination(const char *name, int pos);
 
 extern xbt_dynar_t mc_heap_comparison_ignore;
-extern xbt_dynar_t stacks_areas;
 
 XBT_PUBLIC(void) MC_run(void);
 XBT_PUBLIC(void) MC_init(void);

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index 2a870fa..ac7f0fd 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -236,9 +236,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;
 

diff --git a/src/mc/Process.hpp b/src/mc/Process.hpp
index 7cb054d..bb8c478 100644 (file)
--- a/src/mc/Process.hpp
+++ b/src/mc/Process.hpp
@@ -168,6 +168,15 @@ public:
       info->remove_global_variable(name);
   }
 
+  std::vector<s_stack_region_t>& stack_areas()
+  {
+    return stack_areas_;
+  }
+  std::vector<s_stack_region_t> const& stack_areas() const
+  {
+    return stack_areas_;
+  }
+
 private:
   void init_memory_map_info();
   void refresh_heap();
@@ -183,6 +192,8 @@ private:
   int clear_refs_fd_;
   int pagemap_fd_;
   bool privatized_;
+  std::vector<s_stack_region_t> stack_areas_;
+
 public: // object info
   // TODO, make private (first, objectify simgrid::mc::ObjectInformation*)
   std::vector<std::shared_ptr<simgrid::mc::ObjectInformation>> object_infos;

diff --git a/src/mc/mc_checkpoint.cpp b/src/mc/mc_checkpoint.cpp
index 97ca4ec..62902b2 100644 (file)
--- a/src/mc/mc_checkpoint.cpp
+++ b/src/mc/mc_checkpoint.cpp
@@ -417,32 +417,28 @@ static std::vector<s_mc_snapshot_stack_t> MC_take_snapshot_stacks(mc_snapshot_t
 {
   std::vector<s_mc_snapshot_stack_t> res;
 
-  unsigned int cursor = 0;
-  stack_region_t current_stack;
-
-  // FIXME, cross-process support (stack_areas)
-  xbt_dynar_foreach(stacks_areas, cursor, current_stack) {
+  for (auto const& stack : mc_model_checker->process().stack_areas()) {
     s_mc_snapshot_stack_t st;
 
     // Read the context from remote process:
     unw_context_t context;
     mc_model_checker->process().read_bytes(
-      &context, sizeof(context), remote(current_stack->context));
+      &context, sizeof(context), remote(stack.context));
 
     if (mc_unw_init_context(&st.context, &mc_model_checker->process(),
       &context) < 0) {
       xbt_die("Could not initialise the libunwind context.");
     }
     st.stack_frames = MC_unwind_stack_frames(&st.context);
-    st.local_variables = MC_get_local_variables_values(st.stack_frames, current_stack->process_index);
-    st.process_index = current_stack->process_index;
+    st.local_variables = MC_get_local_variables_values(st.stack_frames, stack.process_index);
+    st.process_index = stack.process_index;
 
     unw_word_t sp = st.stack_frames[0].sp;
 
     res.push_back(std::move(st));
 
     size_t stack_size =
-      (char*) current_stack->address + current_stack->size - (char*) sp;
+      (char*) stack.address + stack.size - (char*) sp;
     (*snapshot)->stack_sizes.push_back(stack_size);
   }
 

diff --git a/src/mc/mc_diff.cpp b/src/mc/mc_diff.cpp
index 782cf23..6cf5993 100644 (file)
--- a/src/mc/mc_diff.cpp
+++ b/src/mc/mc_diff.cpp
@@ -25,7 +25,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_diff, xbt,
                                 "Logging specific to mc_diff in mc");
 
 xbt_dynar_t mc_heap_comparison_ignore;
-xbt_dynar_t stacks_areas;
 
 /*********************************** Heap comparison ***********************************/
 /***************************************************************************************/
@@ -140,31 +139,21 @@ static ssize_t heap_comparison_ignore_size(std::vector<s_mc_heap_ignore_region_t
   return -1;
 }
 
-static int is_stack(const void *address)
+static bool is_stack(const void *address)
 {
-  unsigned int cursor = 0;
-  stack_region_t stack;
-
-  xbt_dynar_foreach(stacks_areas, cursor, stack) {
-    if (address == stack->address)
-      return 1;
-  }
-
-  return 0;
+  for (auto const& stack : mc_model_checker->process().stack_areas())
+    if (address == stack.address)
+      return true;
+  return false;
 }
 
 // TODO, this should depend on the snapshot?
-static int is_block_stack(int block)
+static bool is_block_stack(int block)
 {
-  unsigned int cursor = 0;
-  stack_region_t stack;
-
-  xbt_dynar_foreach(stacks_areas, cursor, stack) {
-    if (block == stack->block)
-      return 1;
-  }
-
-  return 0;
+  for (auto const& stack : mc_model_checker->process().stack_areas())
+    if (block == stack.block)
+      return true;
+  return false;
 }
 
 static void match_equals(struct s_mc_diff *state, xbt_dynar_t list)

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 8733d76..2c484c1 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -482,10 +482,10 @@ void MC_automaton_load(const char *file)
 void MC_dump_stacks(FILE* file)
 {
   int nstack = 0;
-  stack_region_t current_stack;
-  unsigned cursor;
-  xbt_dynar_foreach(stacks_areas, cursor, current_stack) {
-    unw_context_t * context = (unw_context_t *)current_stack->context;
+  for (auto const& stack : mc_model_checker->process().stack_areas()) {
+
+    xbt_die("Fix cross-process access to the context");
+    unw_context_t * context = (unw_context_t *)stack.context;
     fprintf(file, "Stack %i:\n", nstack);
 
     int nframe = 0;

diff --git a/src/mc/mc_ignore.h b/src/mc/mc_ignore.h
index c1a2aeb..4824094 100644 (file)
--- a/src/mc/mc_ignore.h
+++ b/src/mc/mc_ignore.h
@@ -16,8 +16,6 @@
 
 SG_BEGIN_DECL();
 
-XBT_PRIVATE void MC_stack_area_add(stack_region_t stack_area);
-
 XBT_PRIVATE xbt_dynar_t MC_checkpoint_ignore_new(void);
 
 SG_END_DECL();

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 2584801..fbd845a 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -98,8 +98,6 @@ XBT_PRIVATE int snapshot_compare(void *state1, void *state2);
 
 /********************************** Miscellaneous **********************************/
 
-XBT_PRIVATE void MC_dump_stacks(FILE* file);
-
 XBT_PRIVATE void MC_report_assertion_error(void);
 XBT_PRIVATE void MC_report_crash(int status);
 

diff --git a/src/mc/mcer_ignore.cpp b/src/mc/mcer_ignore.cpp
index bbcef78..838e5c4 100644 (file)
--- a/src/mc/mcer_ignore.cpp
+++ b/src/mc/mcer_ignore.cpp
@@ -203,13 +203,4 @@ static void mc_ignore_local_variable_in_scope(const char *var_name,
   }
 }
 
-extern XBT_PRIVATE xbt_dynar_t stacks_areas;
-
-XBT_PRIVATE void MC_stack_area_add(stack_region_t stack_area)
-{
-  if (stacks_areas == NULL)
-    stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
-  xbt_dynar_push(stacks_areas, &stack_area);
-}
-
 }