X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/1ee68a7d44ca89e57734578a1aa91c11ddb27de1..47fd440ad6382d295645c81ca4c5c09bd5d51cc6:/src/mc/mc_ignore.cpp diff --git a/src/mc/mc_ignore.cpp b/src/mc/mc_ignore.cpp index 5440faf703..f1ac12eee7 100644 --- a/src/mc/mc_ignore.cpp +++ b/src/mc/mc_ignore.cpp @@ -18,63 +18,6 @@ extern "C" { XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc, "Logging specific to MC ignore mechanism"); - -/**************************** 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 stacks_areas; - -/**************************** Structures ******************************/ -typedef struct s_mc_stack_ignore_variable { - char *var_name; - char *frame; -} s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t; - -/**************************** Free functions ******************************/ - -static void stack_ignore_variable_free(mc_stack_ignore_variable_t v) -{ - xbt_free(v->var_name); - xbt_free(v->frame); - xbt_free(v); -} - -static void stack_ignore_variable_free_voidp(void *v) -{ - stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v); -} - -void heap_ignore_region_free(mc_heap_ignore_region_t r) -{ - xbt_free(r); -} - -void heap_ignore_region_free_voidp(void *r) -{ - heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r); -} - -static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r) -{ - xbt_free(r); -} - -static void checkpoint_ignore_region_free_voidp(void *r) -{ - checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r); -} - -xbt_dynar_t MC_checkpoint_ignore_new(void) -{ - return xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), - checkpoint_ignore_region_free_voidp); -} - -/***********************************************************************/ - // ***** Model-checked void MC_ignore_heap(void *address, size_t size) @@ -82,21 +25,23 @@ void MC_ignore_heap(void *address, size_t size) if (mc_mode != MC_MODE_CLIENT) return; + xbt_mheap_t heap = mmalloc_get_current_heap(); + s_mc_heap_ignore_region_t region; memset(®ion, 0, sizeof(region)); region.address = address; region.size = size; region.block = ((char *) address - - (char *) std_heap->heapbase) / BLOCKSIZE + 1; - if (std_heap->heapinfo[region.block].type == 0) { + (char *) heap->heapbase) / BLOCKSIZE + 1; + if (heap->heapinfo[region.block].type == 0) { region.fragment = -1; - std_heap->heapinfo[region.block].busy_block.ignore++; + heap->heapinfo[region.block].busy_block.ignore++; } else { region.fragment = - ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >> std_heap-> - heapinfo[region.block].type; - std_heap->heapinfo[region.block].busy_frag.ignore[region.fragment]++; + ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >> + heap->heapinfo[region.block].type; + heap->heapinfo[region.block].busy_frag.ignore[region.fragment]++; } s_mc_ignore_heap_message_t message; @@ -118,138 +63,10 @@ void MC_remove_ignore_heap(void *address, size_t size) MC_client_send_message(&message, sizeof(message)); } -// ***** Model-checker: - void MC_ignore_global_variable(const char *name) { - mc_process_t process = &mc_model_checker->process(); - 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; - for (size_t i=0; i!=n; ++i) { - mc_object_info_t info = process->object_infos[i]; - - // Binary search: - int start = 0; - int end = xbt_dynar_length(info->global_variables) - 1; - while (start <= end) { - unsigned int cursor = (start + end) / 2; - dw_variable_t current_var = - (dw_variable_t) xbt_dynar_get_as(info->global_variables, - cursor, dw_variable_t); - if (strcmp(current_var->name, name) == 0) { - xbt_dynar_remove_at(info->global_variables, cursor, NULL); - start = 0; - end = xbt_dynar_length(info->global_variables) - 1; - } else if (strcmp(current_var->name, name) < 0) { - start = cursor + 1; - } else { - end = cursor - 1; - } - } - } - mmalloc_set_current_heap(heap); -} - -/** \brief Ignore a local variable in a scope - * - * Ignore all instances of variables with a given name in - * any (possibly inlined) subprogram with a given namespaced - * name. - * - * \param var_name Name of the local variable (or parameter to ignore) - * \param subprogram_name Name of the subprogram fo ignore (NULL for any) - * \param subprogram (possibly inlined) Subprogram of the scope - * \param scope Current scope - */ -static void mc_ignore_local_variable_in_scope(const char *var_name, - const char *subprogram_name, - dw_frame_t subprogram, - dw_frame_t scope) -{ - // Processing of direct variables: - - // If the current subprogram matches the given name: - if (!subprogram_name || - (subprogram->name && strcmp(subprogram_name, subprogram->name) == 0)) { - - // Try to find the variable and remove it: - int start = 0; - int end = xbt_dynar_length(scope->variables) - 1; - - // Dichotomic search: - while (start <= end) { - int cursor = (start + end) / 2; - dw_variable_t current_var = - (dw_variable_t) xbt_dynar_get_as(scope->variables, cursor, - dw_variable_t); - - int compare = strcmp(current_var->name, var_name); - if (compare == 0) { - // Variable found, remove it: - xbt_dynar_remove_at(scope->variables, cursor, NULL); - - // and start again: - start = 0; - end = xbt_dynar_length(scope->variables) - 1; - } else if (compare < 0) { - start = cursor + 1; - } else { - end = cursor - 1; - } - } - - } - // And recursive processing in nested scopes: - unsigned cursor = 0; - dw_frame_t nested_scope = NULL; - xbt_dynar_foreach(scope->scopes, cursor, nested_scope) { - // The new scope may be an inlined subroutine, in this case we want to use its - // namespaced name in recursive calls: - dw_frame_t nested_subprogram = - nested_scope->tag == - DW_TAG_inlined_subroutine ? nested_scope : subprogram; - - mc_ignore_local_variable_in_scope(var_name, subprogram_name, - nested_subprogram, nested_scope); - } -} - -static void MC_ignore_local_variable_in_object(const char *var_name, - const char *subprogram_name, - mc_object_info_t info) -{ - xbt_dict_cursor_t cursor2; - dw_frame_t frame; - char *key; - xbt_dict_foreach(info->subprograms, cursor2, key, frame) { - mc_ignore_local_variable_in_scope(var_name, subprogram_name, frame, frame); - } -} - -// MCer -void MC_ignore_local_variable(const char *var_name, const char *frame_name) -{ - mc_process_t process = &mc_model_checker->process(); - if (strcmp(frame_name, "*") == 0) - frame_name = NULL; - xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); - - size_t n = process->object_infos_size; - size_t i; - for (i=0; i!=n; ++i) { - MC_ignore_local_variable_in_object(var_name, frame_name, process->object_infos[i]); - } - - 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); + // TODO, send a message to the model_checker + xbt_die("Unimplemented"); } /** @brief Register a stack in the model checker @@ -263,87 +80,32 @@ void MC_stack_area_add(stack_region_t stack_area) * @param context * @param size Size of the stack */ -void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t size) +void MC_register_stack_area(void *stack, smx_process_t process, void *context, size_t size) { - xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap); + if (mc_mode != MC_MODE_CLIENT) + return; - stack_region_t region = xbt_new0(s_stack_region_t, 1); - region->address = stack; - region->context = context; - region->size = size; - region->block = + xbt_mheap_t heap = mmalloc_get_current_heap(); + + s_stack_region_t region; + memset(®ion, 0, sizeof(region)); + region.address = stack; + region.context = context; + region.size = size; + region.block = ((char *) stack - - (char *) std_heap->heapbase) / BLOCKSIZE + 1; + (char *) heap->heapbase) / BLOCKSIZE + 1; #ifdef HAVE_SMPI if (smpi_privatize_global_variables && process) { - region->process_index = smpi_process_index_of_smx_process(process); + region.process_index = smpi_process_index_of_smx_process(process); } else #endif - region->process_index = -1; - - 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); + region.process_index = -1; - mmalloc_set_current_heap(heap); -} - -void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size) -{ - xbt_dynar_t checkpoint_ignore = process->checkpoint_ignore; - mc_checkpoint_ignore_region_t region = - xbt_new0(s_mc_checkpoint_ignore_region_t, 1); - region->addr = addr; - region->size = size; - - if (xbt_dynar_is_empty(checkpoint_ignore)) { - xbt_dynar_push(checkpoint_ignore, ®ion); - } else { - - unsigned int cursor = 0; - int start = 0; - int end = xbt_dynar_length(checkpoint_ignore) - 1; - mc_checkpoint_ignore_region_t current_region = NULL; - - while (start <= end) { - cursor = (start + end) / 2; - current_region = - (mc_checkpoint_ignore_region_t) xbt_dynar_get_as(checkpoint_ignore, - cursor, - mc_checkpoint_ignore_region_t); - if (current_region->addr == addr) { - if (current_region->size == size) { - checkpoint_ignore_region_free(region); - return; - } else if (current_region->size < size) { - start = cursor + 1; - } else { - end = cursor - 1; - } - } else if (current_region->addr < addr) { - start = cursor + 1; - } else { - end = cursor - 1; - } - } - - if (current_region->addr == addr) { - if (current_region->size < size) { - xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, ®ion); - } else { - xbt_dynar_insert_at(checkpoint_ignore, cursor, ®ion); - } - } else if (current_region->addr < addr) { - xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, ®ion); - } else { - xbt_dynar_insert_at(checkpoint_ignore, cursor, ®ion); - } - } + s_mc_stack_region_message_t message; + message.type = MC_MESSAGE_STACK_REGION; + message.stack_region = region; + MC_client_send_message(&message, sizeof(message)); } }