From: Marion Guthmuller Date: Tue, 5 Mar 2013 20:24:45 +0000 (+0100) Subject: model-checker : get hash of local and global variables which are not pointers X-Git-Tag: v3_9_90~454 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/f0e89ec6fd6ecb2a6171da22d3ccc88a24cf5ba1 model-checker : get hash of local and global variables which are not pointers --- diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 46b70965a3..6fa1de34d1 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -39,6 +39,9 @@ static void *get_stack_pointer(void *stack_context, void *heap); static void snapshot_stack_free(mc_snapshot_stack_t s); static xbt_dynar_t take_snapshot_ignore(void); +static void get_hash_global(char *snapshot_hash, void *data1, void *data2); +static void get_hash_local(char *snapshot_hash, xbt_dynar_t stacks); + static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size) { mc_mem_region_t new_reg = xbt_new0(s_mc_mem_region_t, 1); @@ -200,9 +203,12 @@ mc_snapshot_t MC_take_snapshot() snapshot->to_ignore = take_snapshot_ignore(); - if(_sg_mc_visited > 0 || strcmp(_sg_mc_property_file,"")) + if(_sg_mc_visited > 0 || strcmp(_sg_mc_property_file,"")){ snapshot->stacks = take_snapshot_stacks(&snapshot, heap); - + get_hash_global(snapshot->hash_global, snapshot->regions[2]->data, snapshot->regions[1]->data); + get_hash_local(snapshot->hash_local, snapshot->stacks); + } + free_memory_map(maps); MC_UNSET_RAW_MEM; @@ -458,13 +464,13 @@ static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap) return variables; } - to_append = bprintf("ip=%lx\n", ip); + to_append = bprintf("frame_name=%s\n", frame_name); xbt_strbuff_append(variables, to_append); xbt_free(to_append); - to_append = bprintf("frame_name=%s\n", frame_name); + to_append = bprintf("ip=%lx\n", ip); xbt_strbuff_append(variables, to_append); xbt_free(to_append); - + true_ip = (long)frame->low_pc + (long)off; /* Get frame pointer */ @@ -631,6 +637,103 @@ void variable_value_free_voidp(void* v){ variable_value_free((variable_value_t) * (void **)v); } +static void get_hash_global(char *snapshot_hash, void *data1, void *data2){ + + unsigned int cursor = 0; + size_t offset; + global_variable_t current_var; + void *addr_pointed = NULL; + + void *res; + + xbt_strbuff_t clear = xbt_strbuff_new(); + + xbt_dynar_foreach(mc_global_variables, cursor, current_var){ + if(current_var->address < start_data_libsimgrid) + continue; + offset = (char *)current_var->address - (char *)start_data_libsimgrid; + addr_pointed = *((void **)((char *)data2 + offset)); + if((addr_pointed > start_plt_libsimgrid && addr_pointed < end_plt_libsimgrid) || (addr_pointed > std_heap && (char *)addr_pointed < (char *)std_heap + STD_HEAP_SIZE )) + continue; + res = xbt_malloc0(current_var->size);; + memcpy(res, (char*)data2 + offset, current_var->size); + xbt_strbuff_append(clear, (const char*)res); + xbt_free(res); + } + + xbt_dynar_foreach(mc_global_variables, cursor, current_var){ + if(current_var->address > start_data_libsimgrid) + break; + offset = (char *)current_var->address - (char *)start_data_binary; + addr_pointed = *((void **)((char *)data1 + offset)); + if((addr_pointed > start_plt_binary && addr_pointed < end_plt_binary) || (addr_pointed > std_heap && (char *)addr_pointed < (char *)std_heap + STD_HEAP_SIZE )) + continue; + res = xbt_malloc0(current_var->size);; + memcpy(res, (char*)data1 + offset, current_var->size); + xbt_strbuff_append(clear, (const char*)res); + xbt_free(res); + } + + xbt_sha(clear->data, snapshot_hash); + + xbt_strbuff_free(clear); + +} + +static void get_hash_local(char *snapshot_hash, xbt_dynar_t stacks){ + + xbt_dynar_t tokens = NULL, s_tokens = NULL; + unsigned int cursor1 = 0, cursor2 = 0; + mc_snapshot_stack_t current_stack; + char *frame_name = NULL; + void *addr; + + xbt_strbuff_t clear = xbt_strbuff_new(); + + while(cursor1 < xbt_dynar_length(stacks)){ + current_stack = xbt_dynar_get_as(stacks, cursor1, mc_snapshot_stack_t); + tokens = xbt_str_split(current_stack->local_variables->data, NULL); + cursor2 = 0; + while(cursor2 < xbt_dynar_length(tokens)){ + s_tokens = xbt_str_split(xbt_dynar_get_as(tokens, cursor2, char *), "="); + if(xbt_dynar_length(s_tokens) > 1){ + if(strcmp(xbt_dynar_get_as(s_tokens, 0, char *), "frame_name") == 0){ + xbt_free(frame_name); + frame_name = xbt_strdup(xbt_dynar_get_as(s_tokens, 1, char *)); + xbt_strbuff_append(clear, (const char*)xbt_dynar_get_as(tokens, cursor2, char *)); + cursor2++; + xbt_dynar_free(&s_tokens); + continue; + } + addr = (void *) strtoul(xbt_dynar_get_as(s_tokens, 1, char *), NULL, 16); + if(addr > std_heap && (char *)addr <= (char *)std_heap + STD_HEAP_SIZE){ + cursor2++; + xbt_dynar_free(&s_tokens); + continue; + } + if(is_stack_ignore_variable(frame_name, xbt_dynar_get_as(s_tokens, 0, char *))){ + cursor2++; + xbt_dynar_free(&s_tokens); + continue; + } + xbt_strbuff_append(clear, (const char *)xbt_dynar_get_as(tokens, cursor2, char *)); + } + xbt_dynar_free(&s_tokens); + cursor2++; + } + xbt_dynar_free(&tokens); + cursor1++; + } + + xbt_free(frame_name); + + xbt_sha(clear->data, snapshot_hash); + + xbt_strbuff_free(clear); + +} + + static xbt_dynar_t take_snapshot_ignore(){ if(mc_heap_comparison_ignore == NULL) diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 29c8420972..6ee254a08f 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -287,6 +287,66 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ xbt_os_timer_start(timer); #endif + /* Compare hash of global variables */ + if(s1->hash_global != NULL && s2->hash_global != NULL){ + if(strcmp(s1->hash_global, s2->hash_global) != 0){ + #ifdef MC_DEBUG + xbt_os_timer_stop(timer); + mc_comp_times->hash_global_variables_comparison_time = xbt_os_timer_elapsed(timer); + XBT_DEBUG("Different hash of global variables : %s - %s", s1->hash_global, s2->hash_global); + errors++; + #else + #ifdef MC_VERBOSE + XBT_VERB("Different hash of global variables : %s - %s", s1->hash_global, s2->hash_global); + #endif + + xbt_os_timer_free(timer); + xbt_os_timer_stop(global_timer); + mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); + xbt_os_timer_free(global_timer); + + if(!raw_mem) + MC_UNSET_RAW_MEM; + + return 1; + #endif + } + } + + #ifdef MC_DEBUG + xbt_os_timer_start(timer); + #endif + + /* Compare hash of local variables */ + if(s1->hash_local != NULL && s2->hash_local != NULL){ + if(strcmp(s1->hash_local, s2->hash_local) != 0){ + #ifdef MC_DEBUG + xbt_os_timer_stop(timer); + mc_comp_times->hash_local_variables_comparison_time = xbt_os_timer_elapsed(timer); + XBT_DEBUG("Different hash of local variables : %s - %s", s1->hash_local, s2->hash_local); + errors++; + #else + #ifdef MC_VERBOSE + XBT_VERB("Different hash of local variables : %s - %s", s1->hash_local, s2->hash_local); + #endif + + xbt_os_timer_free(timer); + xbt_os_timer_stop(global_timer); + mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer); + xbt_os_timer_free(global_timer); + + if(!raw_mem) + MC_UNSET_RAW_MEM; + + return 1; + #endif + } + } + + #ifdef MC_DEBUG + xbt_os_timer_start(timer); + #endif + /* Init heap information used in heap comparison algorithm */ init_heap_information((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data, s1->to_ignore, s2->to_ignore); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 0d55eef8e3..7292fe9b4d 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -41,6 +41,8 @@ typedef struct s_mc_snapshot{ size_t *stack_sizes; xbt_dynar_t stacks; xbt_dynar_t to_ignore; + char hash_global[41]; + char hash_local[41]; } s_mc_snapshot_t, *mc_snapshot_t; typedef struct s_mc_snapshot_stack{ @@ -222,6 +224,8 @@ typedef struct s_mc_comparison_times{ double libsimgrid_global_variables_comparison_time; double heap_comparison_time; double stacks_comparison_time; + double hash_global_variables_comparison_time; + double hash_local_variables_comparison_time; }s_mc_comparison_times_t, *mc_comparison_times_t; extern mc_comparison_times_t mc_comp_times;