From: Marion Guthmuller Date: Fri, 5 Oct 2012 11:20:34 +0000 (+0200) Subject: model-checker : extend MC_ignore mechanism for global variables in libsimgrid X-Git-Tag: v3_8~118 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/3227570daf9d253c6d0a79f3c20c04e50e33146c?ds=sidebyside model-checker : extend MC_ignore mechanism for global variables in libsimgrid --- diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index 7a7956fa34..3d4647f379 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 mmalloc_ignore; +extern xbt_dynar_t mc_comparison_ignore; extern xbt_dynar_t stacks_areas; /********************************* Global *************************************/ @@ -41,7 +41,6 @@ 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); -void MC_ignore_init(void); XBT_PUBLIC(void) MC_ignore(void *address, size_t size); void MC_new_stack_area(void *stack, char *name); diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 26b56fbe88..6f815ccd81 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -17,6 +17,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc, void *start_text_libsimgrid; void *start_plt, *end_plt; char *libsimgrid_path; +void *start_data_libsimgrid; static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size); static void MC_region_restore(mc_mem_region_t reg); @@ -116,6 +117,7 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot) if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){ MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); nb_reg++; + start_data_libsimgrid = reg.start_addr; } else { if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){ MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr); diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 6ae4bb8332..36ce55730c 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -17,6 +17,27 @@ static int heap_region_compare(void *d1, void *d2, size_t size); static int compare_local_variables(xbt_strbuff_t s1, xbt_strbuff_t s2); 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 ignore(void *address){ + unsigned int cursor = 0; + int start = 0; + int end = xbt_dynar_length(mc_comparison_ignore) - 1; + mc_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); + if(region->address == address) + return region->size; + if(region->address < address) + start = cursor + 1; + if(region->address > address) + end = cursor - 1; + } + + return 0; +} static int data_program_region_compare(void *d1, void *d2, size_t size){ int distance = 0; @@ -36,12 +57,16 @@ static int data_program_region_compare(void *d1, void *d2, size_t size){ static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){ int distance = 0; - size_t i = 0; + size_t i = 0, ignore_size = 0; int pointer_align; void *addr_pointed1 = NULL, *addr_pointed2 = NULL; for(i=0; i 0){ + i = i + ignore_size; + continue; + } pointer_align = (i / sizeof(void*)) * sizeof(void*); addr_pointed1 = *((void **)((char *)d1 + pointer_align)); addr_pointed2 = *((void **)((char *)d2 + pointer_align)); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 03d05a0a48..a0906644cd 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -73,18 +73,21 @@ mc_stats_pair_t mc_stats_pair = NULL; xbt_fifo_t mc_stack_liveness = NULL; mc_snapshot_t initial_snapshot_liveness = NULL; int compare; -xbt_dynar_t mc_binary_local_variables = NULL; -extern xbt_dynar_t mmalloc_ignore; +/* Local */ +xbt_dict_t mc_local_variables = NULL; + +/* Ignore mechanism */ +extern xbt_dynar_t mc_comparison_ignore; extern xbt_dynar_t stacks_areas; xbt_automaton_t _mc_property_automaton = NULL; -static void MC_assert_pair(int prop); -static e_dw_location_type get_location(char *expr, dw_location_t entry); +/* Static functions */ -static void MC_get_binary_local_variables(void); -static void print_local_variables(xbt_dynar_t list); +static void MC_assert_pair(int prop); +static dw_location_t get_location(xbt_dict_t location_list, char *expr); +static dw_frame_t get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset); void MC_do_the_modelcheck_for_real() { if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') { @@ -651,42 +654,47 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) { /************ MC_ignore ***********/ -void MC_ignore_init(){ - MC_SET_RAW_MEM; - mmalloc_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL); - stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL); - MC_UNSET_RAW_MEM; -} - void MC_ignore(void *address, size_t size){ MC_SET_RAW_MEM; + + if(mc_comparison_ignore == NULL) + mc_comparison_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL); mc_ignore_region_t region = NULL; region = xbt_new0(s_mc_ignore_region_t, 1); region->address = address; region->size = size; - region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1; - if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){ - region->fragment = -1; - }else{ - region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type; + if((address >= std_heap) && (address <= (void*)((char *)std_heap + STD_HEAP_SIZE))){ + + region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1; + + if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){ + region->fragment = -1; + }else{ + region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type; + } + } unsigned int cursor = 0; mc_ignore_region_t current_region; - xbt_dynar_foreach(mmalloc_ignore, cursor, current_region){ + xbt_dynar_foreach(mc_comparison_ignore, cursor, current_region){ if(current_region->address > address) break; } - xbt_dynar_insert_at(mmalloc_ignore, cursor, ®ion); + xbt_dynar_insert_at(mc_comparison_ignore, cursor, ®ion); MC_UNSET_RAW_MEM; } void MC_new_stack_area(void *stack, char *name){ + + if(stacks_areas == NULL) + stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL); + MC_SET_RAW_MEM; stack_region_t region = NULL; region = xbt_new0(s_stack_region_t, 1); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index fbca8a57ef..3172c25673 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -191,6 +191,7 @@ memory_map_t get_memory_map(void); void free_memory_map(memory_map_t map); void get_plt_section(void); +extern void *start_data_libsimgrid; /********************************** DPOR for safety **************************************/ typedef enum { diff --git a/src/msg/msg_global.c b/src/msg/msg_global.c index 9daa413d49..4bd4eb59d4 100644 --- a/src/msg/msg_global.c +++ b/src/msg/msg_global.c @@ -38,9 +38,6 @@ void MSG_init_nocheck(int *argc, char **argv) { s_msg_vm_t vm; // to compute the offset SIMIX_global_init(argc, argv); - - if(MC_IS_ENABLED && mmalloc_ignore == NULL) - MC_ignore_init(); msg_global = xbt_new0(s_MSG_Global_t, 1); diff --git a/src/simix/smx_context_base.c b/src/simix/smx_context_base.c index c934a08e4b..d7f1a79867 100644 --- a/src/simix/smx_context_base.c +++ b/src/simix/smx_context_base.c @@ -48,15 +48,9 @@ smx_ctx_base_factory_create_context_sized(size_t size, smx_context_t context = xbt_malloc0(size); /* Store the address of the stack in heap to compare it apart of heap comparison */ - if(MC_IS_ENABLED){ - - if(mmalloc_ignore == NULL) - MC_ignore_init(); - + if(MC_IS_ENABLED) MC_ignore(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 current context */ diff --git a/src/simix/smx_context_raw.c b/src/simix/smx_context_raw.c index 2b941040d6..c78a6f8510 100644 --- a/src/simix/smx_context_raw.c +++ b/src/simix/smx_context_raw.c @@ -228,11 +228,6 @@ static void smx_ctx_raw_runall(void); void SIMIX_ctx_raw_factory_init(smx_context_factory_t *factory) { - if(MC_IS_ENABLED && mmalloc_ignore == NULL){ - /* Create list of elements to ignore for heap comparison algorithm */ - MC_ignore_init(); - } - XBT_VERB("Using raw contexts. Because the glibc is just not good enough for us."); smx_ctx_base_factory_init(factory); diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c index 8059ee7754..9886e65e8b 100644 --- a/src/simix/smx_network.c +++ b/src/simix/smx_network.c @@ -30,6 +30,8 @@ static void SIMIX_rdv_free(void *data); void SIMIX_network_init(void) { rdv_points = xbt_dict_new_homogeneous(SIMIX_rdv_free); + if(MC_IS_ENABLED) + MC_ignore(&smx_total_comms, sizeof(smx_total_comms)); } void SIMIX_network_exit(void) diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c index f32cb5da21..bf9fb0d73d 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 mmalloc_ignore; +xbt_dynar_t mc_comparison_ignore; xbt_dynar_t stacks_areas; static void heap_area_pair_free(heap_area_pair_t pair); @@ -27,7 +27,7 @@ static heap_area_t new_heap_area(int block, int fragment); static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previous, int check_ignore); static void match_equals(xbt_dynar_t list, xbt_dynar_t *equals); -static int in_mmalloc_ignore(int block, int fragment); +static int in_mc_comparison_ignore(int block, int fragment); static size_t heap_comparison_ignore(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); @@ -232,8 +232,8 @@ 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(mmalloc_ignore)){ - if(in_mmalloc_ignore((int)current_block, -1)) + if(ignore_done < xbt_dynar_length(mc_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 res_compare = compare_area(addr_block1, addr_block2, heapinfo1[current_block].busy_block.busy_size, previous, 0); @@ -300,8 +300,8 @@ 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(mmalloc_ignore)){ - if(in_mmalloc_ignore((int)i1, -1)) + if(ignore_done < xbt_dynar_length(mc_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 res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 0); @@ -357,8 +357,8 @@ 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(mmalloc_ignore)){ - if(in_mmalloc_ignore((int)current_block, (int)current_fragment)) + if(ignore_done < xbt_dynar_length(mc_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 res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[current_block].busy_frag.frag_size[current_fragment], previous, 0); @@ -404,8 +404,8 @@ 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(mmalloc_ignore)){ - if(in_mmalloc_ignore((int)i1, (int)j1)) + if(ignore_done < xbt_dynar_length(mc_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 res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[i1].busy_frag.frag_size[j1], previous, 0); @@ -522,16 +522,16 @@ static heap_area_t new_heap_area(int block, int fragment){ return area; } -static int in_mmalloc_ignore(int block, int fragment){ +static int in_mc_comparison_ignore(int block, int fragment){ unsigned int cursor = 0; int start = 0; - int end = xbt_dynar_length(mmalloc_ignore) - 1; + int end = xbt_dynar_length(mc_comparison_ignore) - 1; mc_ignore_region_t region; while(start <= end){ cursor = (start + end) / 2; - region = (mc_ignore_region_t)xbt_dynar_get_as(mmalloc_ignore, cursor, mc_ignore_region_t); + region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t); if(region->block == block){ if(region->fragment == fragment) return 1; @@ -552,12 +552,12 @@ static int in_mmalloc_ignore(int block, int fragment){ static size_t heap_comparison_ignore(void *address){ unsigned int cursor = 0; int start = 0; - int end = xbt_dynar_length(mmalloc_ignore) - 1; + int end = xbt_dynar_length(mc_comparison_ignore) - 1; mc_ignore_region_t region; while(start <= end){ cursor = (start + end) / 2; - region = (mc_ignore_region_t)xbt_dynar_get_as(mmalloc_ignore, cursor, mc_ignore_region_t); + region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t); if(region->address == address) return region->size; if(region->address < address) @@ -626,8 +626,8 @@ 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(mmalloc_ignore)){ - if(in_mmalloc_ignore(block_pointed1, -1)) + if(ignore_done < xbt_dynar_length(mc_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 res_compare = compare_area(addr_block_pointed1, addr_block_pointed2, heapinfo1[block_pointed1].busy_block.busy_size, previous, 0); @@ -654,8 +654,8 @@ 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(mmalloc_ignore)){ - if(in_mmalloc_ignore(block_pointed1, frag_pointed1)) + if(ignore_done < xbt_dynar_length(mc_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 res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 0); @@ -688,8 +688,8 @@ 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(mmalloc_ignore)){ - if(in_mmalloc_ignore(block_pointed1, frag_pointed1)) + if(ignore_done < xbt_dynar_length(mc_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 res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 0);