Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' into mc-process
[simgrid.git] / src / mc / mc_ignore.c
index d80a130..051a1f4 100644 (file)
@@ -18,6 +18,9 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc,
 
 
 /**************************** Global variables ******************************/
+// Those structures live with the MCer and should be moved in the model_checker
+// structure but they are currently used before the MC initialisation
+// (in standalone mode).
 
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
@@ -70,6 +73,7 @@ xbt_dynar_t MC_checkpoint_ignore_new(void)
 
 /***********************************************************************/
 
+// Mcer
 void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
 {
   if (mc_heap_comparison_ignore == NULL) {
@@ -109,27 +113,22 @@ void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
 }
 
-void MC_heap_region_ignore_send(mc_heap_ignore_region_t region)
+// MCed:
+static void MC_heap_region_ignore_send(mc_heap_ignore_region_t region)
 {
-  s_mc_ignore_region_message_t message;
-  message.type = MC_MESSAGE_IGNORE_REGION;
+  s_mc_ignore_heap_message_t message;
+  message.type = MC_MESSAGE_IGNORE_HEAP;
   message.region = *region;
   if (MC_protocol_send(mc_client->fd, &message, sizeof(message)))
     xbt_die("Could not send ignored region to MCer");
-  XBT_DEBUG("Sent ignored region to the model-checker");
 }
 
-// FIXME, cross-process support? (or make this it is used on the app-side)
+// MCed:
 void MC_ignore_heap(void *address, size_t size)
 {
-  if(!std_heap)
-    return;
-
-  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-  MC_SET_MC_HEAP;
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
-  mc_heap_ignore_region_t region = NULL;
-  region = xbt_new0(s_mc_heap_ignore_region_t, 1);
+  mc_heap_ignore_region_t region = xbt_new0(s_mc_heap_ignore_region_t, 1);
   region->address = address;
   region->size = size;
 
@@ -153,17 +152,20 @@ void MC_ignore_heap(void *address, size_t size)
   if (mc_mode == MC_MODE_CLIENT)
     MC_heap_region_ignore_send(region);
 #endif
-
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;
+  mmalloc_set_current_heap(heap);
 }
 
 void MC_remove_ignore_heap(void *address, size_t size)
 {
+  if (mc_mode == MC_MODE_CLIENT) {
+    s_mc_ignore_memory_message_t message;
+    message.type = MC_MESSAGE_UNIGNORE_HEAP;
+    message.addr = address;
+    message.size = size;
+    MC_client_send_message(&message, sizeof(message));
+  }
 
-  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
-  MC_SET_MC_HEAP;
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   unsigned int cursor = 0;
   int start = 0;
@@ -196,20 +198,14 @@ void MC_remove_ignore_heap(void *address, size_t size)
     xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
     MC_remove_ignore_heap(address, size);
   }
-
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;
-
+  mmalloc_set_current_heap(heap);
 }
 
-// FIXME, cross-process support?
+// MCer
 void MC_ignore_global_variable(const char *name)
 {
   mc_process_t process = &mc_model_checker->process;
-  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
-  MC_SET_MC_HEAP;
-
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
   xbt_assert(process->object_infos, "MC subsystem not initialized");
 
   size_t n = process->object_infos_size;
@@ -235,9 +231,7 @@ void MC_ignore_global_variable(const char *name)
       }
     }
   }
-
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;
+  mmalloc_set_current_heap(heap);
 }
 
 /** \brief Ignore a local variable in a scope
@@ -251,7 +245,6 @@ void MC_ignore_global_variable(const char *name)
  *  \param subprogram      (possibly inlined) Subprogram of the scope
  *  \param scope           Current scope
  */
- // FIXME, cross-process support (messaging?)
 static void mc_ignore_local_variable_in_scope(const char *var_name,
                                               const char *subprogram_name,
                                               dw_frame_t subprogram,
@@ -317,17 +310,13 @@ static void MC_ignore_local_variable_in_object(const char *var_name,
   }
 }
 
+// MCer
 void MC_ignore_local_variable(const char *var_name, const char *frame_name)
 {
   mc_process_t process = &mc_model_checker->process;
-
-
-  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
   if (strcmp(frame_name, "*") == 0)
     frame_name = NULL;
-
-  MC_SET_MC_HEAP;
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   size_t n = process->object_infos_size;
   size_t i;
@@ -335,9 +324,14 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name)
     MC_ignore_local_variable_in_object(var_name, frame_name, process->object_infos[i]);
   }
 
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;
+  mmalloc_set_current_heap(heap);
+}
 
+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);
 }
 
 /** @brief Register a stack in the model checker
@@ -353,18 +347,10 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name)
  */
 void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t size)
 {
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
-  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
-  MC_SET_MC_HEAP;
-
-  if (stacks_areas == NULL)
-    stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
-
-  stack_region_t region = NULL;
-  region = xbt_new0(s_stack_region_t, 1);
+  stack_region_t region = xbt_new0(s_stack_region_t, 1);
   region->address = stack;
-  region->process_name = process && process->name ? strdup(process->name) : NULL;
   region->context = context;
   region->size = size;
   region->block =
@@ -377,10 +363,16 @@ void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t
 #endif
   region->process_index = -1;
 
-  xbt_dynar_push(stacks_areas, &region);
+  if (mc_mode == MC_MODE_CLIENT) {
+    s_mc_stack_region_message_t message;
+    message.type = MC_MESSAGE_STACK_REGION;
+    message.stack_region = *region;
+    MC_client_send_message(&message, sizeof(message));
+  }
+
+  MC_stack_area_add(region);
 
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;
+  mmalloc_set_current_heap(heap);
 }
 
 void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size)