From: Marion Guthmuller Date: Wed, 31 Oct 2012 17:45:34 +0000 (+0100) Subject: model-checker : add ignore mechanism for comparison of local variables X-Git-Tag: v3_9_rc1~91^2~126^2~27 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/fe93dd78e64c2374403b3f1ac084155756837b38 model-checker : add ignore mechanism for comparison of local variables --- diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h index 61cef5d85c..06a4cbf003 100644 --- a/src/include/mc/datatypes.h +++ b/src/include/mc/datatypes.h @@ -18,12 +18,17 @@ typedef struct s_mc_transition *mc_transition_t; /*********** Structures for snapshot comparison **************************/ -typedef struct s_mc_ignore_region{ +typedef struct s_mc_heap_ignore_region{ int block; int fragment; void *address; size_t size; -}s_mc_ignore_region_t, *mc_ignore_region_t; +}s_mc_heap_ignore_region_t, *mc_heap_ignore_region_t; + +typedef struct s_mc_stack_ignore_variable{ + char *var_name; + char *frame; +}s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t; typedef struct s_stack_region{ void *address; diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 4ae4edc174..b03df527c1 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -22,7 +22,7 @@ SG_BEGIN_DECL() extern char*_surf_mc_property_file; /* fixme: better location? */ -extern xbt_dynar_t mc_comparison_ignore; +extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; /********************************* Global *************************************/ @@ -41,7 +41,9 @@ XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double); XBT_PUBLIC(double) MC_process_clock_get(smx_process_t); void MC_automaton_load(const char *file); -XBT_PUBLIC(void) MC_ignore(void *address, size_t size); +/****************************** MC ignore **********************************/ +XBT_PUBLIC(void) MC_ignore_heap(void *address, size_t size); +XBT_PUBLIC(void) MC_ignore_stack(const char *var_name, const char *frame); void MC_new_stack_area(void *stack, char *name, void *context); /********************************* Memory *************************************/ diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 6007680788..2bae1f4d22 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -16,22 +16,23 @@ static int heap_region_compare(void *d1, void *d2, size_t size); static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void *sp2, void *heap1, void *heap2, xbt_dynar_t equals); static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2); -static size_t ignore(void *address); +static size_t heap_ignore_size(void *address); static void stack_region_free(stack_region_t s); static void heap_equality_free(heap_equality_t e); +static int is_stack_ignore_variable(char *frame, char *var_name); static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals); -static size_t ignore(void *address){ +static size_t heap_ignore_size(void *address){ unsigned int cursor = 0; int start = 0; - int end = xbt_dynar_length(mc_comparison_ignore) - 1; - mc_ignore_region_t region; + int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1; + mc_heap_ignore_region_t region; while(start <= end){ cursor = (start + end) / 2; - region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t); + region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t); if(region->address == address) return region->size; if(region->address < address) @@ -76,7 +77,7 @@ static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){ for(i=0; i 0){ + if((ignore_size = heap_ignore_size((char *)start_data_libsimgrid+i)) > 0){ i = i + ignore_size; continue; } @@ -304,6 +305,33 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ } +static int is_stack_ignore_variable(char *frame, char *var_name){ + + unsigned int cursor = 0; + int start = 0; + int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1; + mc_stack_ignore_variable_t current_var; + + while(start <= end){ + cursor = (start + end) / 2; + current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t); + if(strcmp(current_var->frame, frame) == 0){ + if(strcmp(current_var->var_name, var_name) == 0) + return 1; + if(strcmp(current_var->var_name, var_name) < 0) + start = cursor + 1; + if(strcmp(current_var->var_name, var_name) > 0) + end = cursor - 1; + } + if(strcmp(current_var->frame, frame) < 0) + start = cursor + 1; + if(strcmp(current_var->frame, frame) > 0) + end = cursor - 1; + } + + return 0; +} + static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals){ xbt_dynar_t tokens1 = xbt_str_split(s1, NULL); @@ -312,6 +340,7 @@ static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals){ xbt_dynar_t s_tokens1, s_tokens2; unsigned int cursor = 0; void *addr1, *addr2; + char *ip1, *ip2; int diff = 0; @@ -319,7 +348,18 @@ static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals){ s_tokens1 = xbt_str_split(xbt_dynar_get_as(tokens1, cursor, char *), "="); s_tokens2 = xbt_str_split(xbt_dynar_get_as(tokens2, cursor, char *), "="); if(xbt_dynar_length(s_tokens1) > 1 && xbt_dynar_length(s_tokens2) > 1){ - if(strcmp(xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *)) != 0){ + if((strcmp(xbt_dynar_get_as(s_tokens1, 0, char *), "ip") == 0) && (strcmp(xbt_dynar_get_as(s_tokens2, 0, char *), "ip") == 0)){ + ip1 = strdup(xbt_dynar_get_as(s_tokens1, 1, char *)); + ip2 = strdup(xbt_dynar_get_as(s_tokens2, 1, char *)); + } + if(strcmp(xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *)) != 0){ + /* Ignore this variable ? */ + if(is_stack_ignore_variable(ip1, xbt_dynar_get_as(s_tokens1, 0, char *)) && is_stack_ignore_variable(ip2, xbt_dynar_get_as(s_tokens2, 0, char *))){ + xbt_dynar_free(&s_tokens1); + xbt_dynar_free(&s_tokens2); + cursor++; + continue; + } addr1 = (void *) strtoul(xbt_dynar_get_as(s_tokens1, 1, char *), NULL, 16); addr2 = (void *) strtoul(xbt_dynar_get_as(s_tokens2, 1, char *), NULL, 16); if(is_heap_equality(heap_equals, addr1, addr2) == 0){ diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 2dd304fe6f..990799806c 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -80,7 +80,8 @@ int compare; xbt_dict_t mc_local_variables = NULL; /* Ignore mechanism */ -extern xbt_dynar_t mc_comparison_ignore; +xbt_dynar_t mc_stack_comparison_ignore; +extern xbt_dynar_t mc_heap_comparison_ignore; extern xbt_dynar_t stacks_areas; xbt_automaton_t _mc_property_automaton = NULL; @@ -172,7 +173,7 @@ void MC_init_liveness(){ /* mc_time refers to clock for each process -> ignore it for heap comparison */ int i; for(i = 0; iaddress = address; region->size = size; @@ -705,13 +706,13 @@ void MC_ignore(void *address, size_t size){ } unsigned int cursor = 0; - mc_ignore_region_t current_region; - xbt_dynar_foreach(mc_comparison_ignore, cursor, current_region){ + mc_heap_ignore_region_t current_region; + xbt_dynar_foreach(mc_heap_comparison_ignore, cursor, current_region){ if(current_region->address > address) break; } - xbt_dynar_insert_at(mc_comparison_ignore, cursor, ®ion); + xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion); MC_UNSET_RAW_MEM; @@ -719,12 +720,76 @@ void MC_ignore(void *address, size_t size){ MC_SET_RAW_MEM; } +void MC_ignore_stack(const char *var_name, const char *frame){ + + raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + + MC_SET_RAW_MEM; + + if(mc_stack_comparison_ignore == NULL) + mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), NULL); + + if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){ + + mc_stack_ignore_variable_t var = NULL; + var = xbt_new0(s_mc_stack_ignore_variable_t, 1); + var->var_name = strdup(var_name); + var->frame = strdup(frame); + + xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var); + + }else{ + + unsigned int cursor = 0; + int start = 0; + int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1; + mc_stack_ignore_variable_t current_var = NULL; + + while(start <= end){ + cursor = (start + end) / 2; + current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t); + if(strcmp(current_var->frame, frame) == 0){ + if(strcmp(current_var->var_name, var_name) == 0){ + MC_UNSET_RAW_MEM; + if(raw_mem_set) + MC_SET_RAW_MEM; + return; + } + if(strcmp(current_var->var_name, var_name) < 0) + start = cursor + 1; + if(strcmp(current_var->var_name, var_name) > 0) + end = cursor - 1; + } + if(strcmp(current_var->frame, frame) < 0) + start = cursor + 1; + if(strcmp(current_var->frame, frame) > 0) + end = cursor - 1; + } + + mc_stack_ignore_variable_t var = NULL; + var = xbt_new0(s_mc_stack_ignore_variable_t, 1); + var->var_name = strdup(var_name); + var->frame = strdup(frame); + + if(strcmp(current_var->frame, frame) < 0) + xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var); + else + xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var); + + } + + MC_UNSET_RAW_MEM; + + if(raw_mem_set) + MC_SET_RAW_MEM; + +} + void MC_new_stack_area(void *stack, char *name, void* context){ raw_mem_set = (mmalloc_get_current_heap() == raw_heap); MC_SET_RAW_MEM; - if(stacks_areas == NULL) stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 808f36c729..c16fec2ac9 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -224,6 +224,7 @@ extern void *start_plt_libsimgrid; extern void *end_plt_libsimgrid; extern void *start_plt_binary; extern void *end_plt_binary; +extern xbt_dynar_t mc_stack_comparison_ignore; typedef struct s_mc_pair{ mc_snapshot_t system_state; diff --git a/src/msg/msg_global.c b/src/msg/msg_global.c index d333f8aa6b..81abae0fdf 100644 --- a/src/msg/msg_global.c +++ b/src/msg/msg_global.c @@ -61,7 +61,7 @@ void MSG_init_nocheck(int *argc, char **argv) { if(MC_is_active()){ /* Ignore total amount of messages sent during the simulation for heap comparison */ - MC_ignore(&(msg_global->sent_msg), sizeof(msg_global->sent_msg)); + MC_ignore_heap(&(msg_global->sent_msg), sizeof(msg_global->sent_msg)); } #ifdef HAVE_TRACING diff --git a/src/simix/smx_context_base.c b/src/simix/smx_context_base.c index 1f3161b08f..97cbb0ca6f 100644 --- a/src/simix/smx_context_base.c +++ b/src/simix/smx_context_base.c @@ -49,7 +49,7 @@ smx_ctx_base_factory_create_context_sized(size_t size, /* Store the address of the stack in heap to compare it apart of heap comparison */ if(MC_is_active()) - MC_ignore(context, size); + MC_ignore_heap(context, size); /* If the user provided a function for the process then use it. Otherwise, it is the context for maestro and we should set it as the diff --git a/src/simix/smx_context_raw.c b/src/simix/smx_context_raw.c index c89d70655e..fd9058e7ce 100644 --- a/src/simix/smx_context_raw.c +++ b/src/simix/smx_context_raw.c @@ -328,7 +328,7 @@ smx_ctx_raw_create_context(xbt_main_func_t code, int argc, char **argv, raw_maestro_context = context; if(MC_is_active()) - MC_ignore(&(raw_maestro_context->stack_top), sizeof(raw_maestro_context->stack_top)); + MC_ignore_heap(&(raw_maestro_context->stack_top), sizeof(raw_maestro_context->stack_top)); } diff --git a/src/simix/smx_context_sysv.c b/src/simix/smx_context_sysv.c index 7bdcfc3f37..63a0b660a9 100644 --- a/src/simix/smx_context_sysv.c +++ b/src/simix/smx_context_sysv.c @@ -232,6 +232,11 @@ static void smx_ctx_sysv_suspend_serial(smx_context_t context) smx_context_t next_context; unsigned long int i = sysv_process_index++; + if(MC_is_active()){ + MC_ignore_stack("next_context", "smx_ctx_sysv_suspend_serial"); + MC_ignore_stack("i", "smx_ctx_sysv_suspend_serial"); + } + if (i < xbt_dynar_length(simix_global->process_to_run)) { /* execute the next process */ XBT_DEBUG("Run next process"); diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c index 8d9e915f3b..c22ed83155 100644 --- a/src/simix/smx_network.c +++ b/src/simix/smx_network.c @@ -31,7 +31,7 @@ void SIMIX_network_init(void) { rdv_points = xbt_dict_new_homogeneous(SIMIX_rdv_free); if(MC_is_active()) - MC_ignore(&smx_total_comms, sizeof(smx_total_comms)); + MC_ignore_heap(&smx_total_comms, sizeof(smx_total_comms)); } void SIMIX_network_exit(void) diff --git a/src/simix/smx_process.c b/src/simix/smx_process.c index 95bf7c79b7..6a3ca375cf 100644 --- a/src/simix/smx_process.c +++ b/src/simix/smx_process.c @@ -709,6 +709,9 @@ void SIMIX_process_yield(smx_process_t self) self->doexception = 0; SMX_THROW(); } + + if(MC_is_active()) + MC_ignore_stack("ctx", "SIMIX_process_yield"); } /* callback: context fetching */ diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c index 2e0cf4c1df..ab71565b07 100644 --- a/src/xbt/mmalloc/mm_diff.c +++ b/src/xbt/mmalloc/mm_diff.c @@ -15,7 +15,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mm_diff, xbt, extern char *xbt_binary_name; -xbt_dynar_t mc_comparison_ignore; +xbt_dynar_t mc_heap_comparison_ignore; xbt_dynar_t stacks_areas; static void heap_area_pair_free(heap_area_pair_t pair); @@ -28,7 +28,7 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ static void match_equals(xbt_dynar_t list, xbt_dynar_t *equals); static int in_mc_comparison_ignore(int block, int fragment); -static size_t heap_comparison_ignore(void *address); +static size_t heap_comparison_ignore_size(void *address); static void add_heap_equality(xbt_dynar_t *equals, void *a1, void *a2); static void remove_heap_equality(xbt_dynar_t *equals, int address, void *a); @@ -263,7 +263,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac add_heap_area_pair(previous, current_block, -1, current_block, -1); - if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){ + if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){ if(in_mc_comparison_ignore((int)current_block, -1)) res_compare = compare_area(addr_block1, addr_block2, heapinfo1[current_block].busy_block.busy_size, previous, 1); else @@ -331,7 +331,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac /* Comparison */ add_heap_area_pair(previous, i1, -1, i2, -1); - if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){ + if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){ if(in_mc_comparison_ignore((int)i1, -1)) res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 1); else @@ -388,7 +388,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac add_heap_area_pair(previous, current_block, current_fragment, current_block, current_fragment); - if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){ + if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){ if(in_mc_comparison_ignore((int)current_block, (int)current_fragment)) res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[current_block].busy_frag.frag_size[current_fragment], previous, 1); else @@ -435,7 +435,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac /* Comparison */ add_heap_area_pair(previous, i1, j1, i2, j2); - if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){ + if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){ if(in_mc_comparison_ignore((int)i1, (int)j1)) res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[i1].busy_frag.frag_size[j1], previous, 1); else @@ -565,12 +565,12 @@ static int in_mc_comparison_ignore(int block, int fragment){ unsigned int cursor = 0; int start = 0; - int end = xbt_dynar_length(mc_comparison_ignore) - 1; - mc_ignore_region_t region; + int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1; + mc_heap_ignore_region_t region; while(start <= end){ cursor = (start + end) / 2; - region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t); + region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t); if(region->block == block){ if(region->fragment == fragment) return 1; @@ -588,15 +588,15 @@ static int in_mc_comparison_ignore(int block, int fragment){ return 0; } -static size_t heap_comparison_ignore(void *address){ +static size_t heap_comparison_ignore_size(void *address){ unsigned int cursor = 0; int start = 0; - int end = xbt_dynar_length(mc_comparison_ignore) - 1; - mc_ignore_region_t region; + int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1; + mc_heap_ignore_region_t region; while(start <= end){ cursor = (start + end) / 2; - region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t); + region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t); if(region->address == address) return region->size; if(region->address < address) @@ -622,9 +622,9 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ if(check_ignore){ current_area1 = (char*)((xbt_mheap_t)s_heap)->heapbase + ((((char *)area1) + i) - (char *)heapbase1); - if((ignore1 = heap_comparison_ignore(current_area1)) > 0){ + if((ignore1 = heap_comparison_ignore_size(current_area1)) > 0){ current_area2 = (char*)((xbt_mheap_t)s_heap)->heapbase + ((((char *)area2) + i) - (char *)heapbase2); - if((ignore2 = heap_comparison_ignore(current_area2)) == ignore1){ + if((ignore2 = heap_comparison_ignore_size(current_area2)) == ignore1){ i = i + ignore2; ignore_done++; continue; @@ -665,7 +665,7 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ if(add_heap_area_pair(previous, block_pointed1, -1, block_pointed2, -1)){ - if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){ + if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){ if(in_mc_comparison_ignore(block_pointed1, -1)) res_compare = compare_area(addr_block_pointed1, addr_block_pointed2, heapinfo1[block_pointed1].busy_block.busy_size, previous, 1); else @@ -693,7 +693,7 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ if(add_heap_area_pair(previous, block_pointed1, frag_pointed1, block_pointed2, frag_pointed2)){ - if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){ + if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){ if(in_mc_comparison_ignore(block_pointed1, frag_pointed1)) res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 1); else @@ -727,7 +727,7 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ if(add_heap_area_pair(previous, block_pointed1, frag_pointed1, block_pointed2, frag_pointed2)){ - if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){ + if(ignore_done < xbt_dynar_length(mc_heap_comparison_ignore)){ if(in_mc_comparison_ignore(block_pointed1, frag_pointed1)) res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 1); else @@ -1016,12 +1016,12 @@ static char * is_stack(void *address){ static void add_heap_equality(xbt_dynar_t *equals, void *a1, void *a2){ - heap_equality_t he = xbt_new0(s_heap_equality_t, 1); - he->address1 = a1; - he->address2 = a2; - if(xbt_dynar_is_empty(*equals)){ + heap_equality_t he = xbt_new0(s_heap_equality_t, 1); + he->address1 = a1; + he->address2 = a2; + xbt_dynar_insert_at(*equals, 0, &he); }else{ @@ -1047,6 +1047,10 @@ static void add_heap_equality(xbt_dynar_t *equals, void *a1, void *a2){ if(current_equality->address1 > a1) end = cursor - 1; } + + heap_equality_t he = xbt_new0(s_heap_equality_t, 1); + he->address1 = a1; + he->address2 = a2; if(current_equality->address1 < a1) xbt_dynar_insert_at(*equals, cursor + 1 , &he);