From: Marion Guthmuller Date: Mon, 21 May 2012 13:59:24 +0000 (+0200) Subject: model-checker : get location of pointed address in comparison of process memory area X-Git-Tag: v3_8~704 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/dda93e7e3c8844b68b25ce1172d9fe1b6fcb8d37 model-checker : get location of pointed address in comparison of process memory area --- diff --git a/include/xbt/mmalloc.h b/include/xbt/mmalloc.h index 93ba1f582a..b53046853f 100644 --- a/include/xbt/mmalloc.h +++ b/include/xbt/mmalloc.h @@ -58,7 +58,7 @@ extern void mmalloc_display_info_heap(xbt_mheap_t h); void mmalloc_set_current_heap(xbt_mheap_t new_heap); xbt_mheap_t mmalloc_get_current_heap(void); -int mmalloc_compare_heap(xbt_mheap_t mdp1, xbt_mheap_t mdp2); +int mmalloc_compare_heap(xbt_mheap_t mdp1, xbt_mheap_t mdp2, void* s_heap, void* r_heap); void mmalloc_backtrace_display(xbt_mheap_t mdp, void *addr); diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 221b87992c..ae15bbfcef 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -33,6 +33,62 @@ unsigned int hash_region(char *str, int str_len){ } +const char* get_memory_map_addr(void *addr){ + + FILE *fp; /* File pointer to process's proc maps file */ + char *line = NULL; /* Temporal storage for each line that is readed */ + ssize_t read; /* Number of bytes readed */ + size_t n = 0; /* Amount of bytes to read by getline */ + + fp = fopen("/proc/self/maps", "r"); + + if(fp == NULL) + perror("fopen failed"); + + if(addr == NULL) + return "nil"; + + char *lfields[6], *start, *end, *endptr; + int i; + void *start_addr; + void *end_addr; + + while ((read = getline(&line, &n, fp)) != -1) { + + line[read - 1] = '\0'; + + lfields[0] = strtok(line, " "); + + for (i = 1; i < 6 && lfields[i - 1] != NULL; i++) { + lfields[i] = strtok(NULL, " "); + } + + start = strtok(lfields[0], "-"); + start_addr = (void *) strtoul(start, &endptr, 16); + + if(start_addr == std_heap) + lfields[5] = strdup("std_heap"); + if(start_addr == raw_heap) + lfields[5] = strdup("raw_heap"); + end = strtok(NULL, "-"); + end_addr = (void *) strtoul(end, &endptr, 16); + + if((addr > start_addr) && ( addr < end_addr)){ + free(line); + fclose(fp); + if(lfields[5] != NULL){ + return lfields[5]; + }else{ + return "Anonymous"; + } + } + + } + + return "Unknown area"; + +} + int data_program_region_compare(void *d1, void *d2, size_t size){ int distance = 0; int pointer_align; @@ -43,12 +99,11 @@ int data_program_region_compare(void *d1, void *d2, size_t size){ fprintf(stderr,"Different byte (offset=%d) (%p - %p) in data program region\n", i, (char *)d1 + i, (char *)d2 + i); distance++; pointer_align = (i /sizeof(void *)) * sizeof(void *); - fprintf(stderr, "Pointer address : %p - %p\n", (char *)d1 + pointer_align, (char *)d2 + pointer_align); - fprintf(stderr, "Pointed address : %p - %p\n", *((void **)((char *)d1 + pointer_align)), *((void **)((char *)d2 + pointer_align))); + fprintf(stderr, "Pointed address : %p (in %s) - %p (in %s)\n", *((void **)((char *)d1 + pointer_align)), get_memory_map_addr(*((void **)((char *)d1 + pointer_align))), *((void **)((char *)d2 + pointer_align)), get_memory_map_addr(*((void **)((char *)d2 + pointer_align)))); } } - fprintf(stderr, "Hamming distance between data program regions : %d", distance); + fprintf(stderr, "Hamming distance between data program regions : %d\n", distance); return distance; } @@ -60,20 +115,19 @@ int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){ for(i=0; inum_reg != s2->num_reg){ @@ -113,7 +167,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ return 1; } } - if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){ + if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data, s_heap, r_heap)){ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ XBT_DEBUG("Different heap (mmalloc_compare)"); errors++; @@ -222,7 +276,7 @@ int reached(xbt_state_t st){ //XBT_DEBUG("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points)); //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){ //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){ - if(snapshot_compare(pair_test->system_state, sn) == 0){ + if(snapshot_compare(pair_test->system_state, sn, std_heap, raw_heap) == 0){ MC_free_snapshot(sn); xbt_dynar_reset(prop_ato); xbt_free(prop_ato); @@ -619,7 +673,7 @@ int visited(xbt_state_t st, int sc){ if(pair_test->search_cycle == sc) { if(automaton_state_compare(pair_test->automaton_state, st) == 0){ if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ - if(snapshot_compare(pair_test->system_state, sn) == 0){ + if(snapshot_compare(pair_test->system_state, sn, std_heap, raw_heap) == 0){ MC_free_snapshot(sn); xbt_dynar_reset(prop_ato); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 09e8932ec1..a34855fae3 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -252,7 +252,7 @@ int reached(xbt_state_t st); void set_pair_reached(xbt_state_t st); int reached_hash(xbt_state_t st); void set_pair_reached_hash(xbt_state_t st); -int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2); +int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, void* s_heap, void* r_heap); int data_program_region_compare(void *d1, void *d2, size_t size); int data_libsimgrid_region_compare(void *d1, void *d2, size_t size); void MC_pair_delete(mc_pair_t pair); @@ -265,6 +265,7 @@ void set_pair_visited_hash(xbt_state_t st, int search_cycle); unsigned int hash_region(char *str, int str_len); int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2); +const char* get_memory_map_addr(void *addr); /* **** Double-DFS stateless **** */ diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c index 96df86007f..c8bc05adfa 100644 --- a/src/xbt/mmalloc/mm_diff.c +++ b/src/xbt/mmalloc/mm_diff.c @@ -111,20 +111,20 @@ void mmalloc_backtrace_fragment_display(xbt_mheap_t mdp, size_t block, size_t fr } } -int mmalloc_compare_heap(xbt_mheap_t mdp1, xbt_mheap_t mdp2){ +int mmalloc_compare_heap(xbt_mheap_t mdp1, xbt_mheap_t mdp2, void* s_heap, void* r_heap){ if(mdp1 == NULL && mdp2 == NULL){ fprintf(stderr, "Malloc descriptors null\n"); return 0; } - int errors = mmalloc_compare_mdesc(mdp1, mdp2); + int errors = mmalloc_compare_mdesc(mdp1, mdp2, s_heap, r_heap); return (errors > 0); } -int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ +int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2, void* s_heap, void* r_heap){ int errors = 0; @@ -238,7 +238,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ fprintf(stderr, "Different byte (offset=%d) (%p - %p) in block %zu\n", k, (char *)addr_block1 + k, (char *)addr_block2 + k, i); distance++; pointer_align = (k / sizeof(void*)) * sizeof(void*); - fprintf(stderr, "Pointer address : %p - %p\n", *((void **)((char *)addr_block1 + pointer_align)), *((void **)((char *)addr_block2 + pointer_align))); + fprintf(stderr, "Pointed address : %p (in %s) - %p (in %s)\n", *((void **)((char *)addr_block1 + pointer_align)), get_addr_memory_map(*((void **)((char *)addr_block1 + pointer_align)), s_heap, r_heap), *((void **)((char *)addr_block2 + pointer_align)),get_addr_memory_map(*((void **)((char *)addr_block2 + pointer_align)), s_heap, r_heap) ); } } @@ -296,7 +296,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ fprintf(stderr, "Different byte (offset=%d) (%p - %p) in fragment %zu in block %zu\n", k, (char *)addr_frag1 + k, (char *)addr_frag2 + k, j, i); distance++; pointer_align = (k / sizeof(void*)) * sizeof(void*); - fprintf(stderr, "Pointer address : %p - %p\n", *((void **)((char *)addr_frag1 + pointer_align)), *((void **)((char *)addr_frag2 + pointer_align))); + fprintf(stderr, "Pointed address : %p (in %s) - %p (in %s)\n", *((void **)((char *)addr_frag1 + pointer_align)), get_addr_memory_map(*((void **)((char *)addr_frag1 + pointer_align)), s_heap, r_heap), *((void **)((char *)addr_frag2 + pointer_align)), get_addr_memory_map(*((void **)((char *)addr_frag2 + pointer_align)), s_heap, r_heap)); } } @@ -327,6 +327,62 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ } +const char* get_addr_memory_map(void *addr, void* s_heap, void* r_heap){ + + FILE *fp; /* File pointer to process's proc maps file */ + char *line = NULL; /* Temporal storage for each line that is readed */ + ssize_t read; /* Number of bytes readed */ + size_t n = 0; /* Amount of bytes to read by getline */ + + fp = fopen("/proc/self/maps", "r"); + + if(fp == NULL) + perror("fopen failed"); + + if(addr == NULL) + return "nil"; + + char *lfields[6], *start, *end, *endptr; + int i; + void *start_addr; + void *end_addr; + + while ((read = getline(&line, &n, fp)) != -1) { + + line[read - 1] = '\0'; + + lfields[0] = strtok(line, " "); + + for (i = 1; i < 6 && lfields[i - 1] != NULL; i++) { + lfields[i] = strtok(NULL, " "); + } + + start = strtok(lfields[0], "-"); + start_addr = (void *) strtoul(start, &endptr, 16); + + if(start_addr == s_heap) + lfields[5] = strdup("std_heap"); + if(start_addr == r_heap) + lfields[5] = strdup("raw_heap"); + end = strtok(NULL, "-"); + end_addr = (void *) strtoul(end, &endptr, 16); + + if((addr > start_addr) && ( addr < end_addr)){ + free(line); + fclose(fp); + if(lfields[5] != NULL){ + return lfields[5]; + }else{ + return "Anonymous"; + } + } + + } + + return "Unknown area"; + +} + void mmalloc_display_info_heap(xbt_mheap_t h){ } diff --git a/src/xbt/mmalloc/mmprivate.h b/src/xbt/mmalloc/mmprivate.h index d2e638bde9..f322b11c32 100644 --- a/src/xbt/mmalloc/mmprivate.h +++ b/src/xbt/mmalloc/mmprivate.h @@ -224,10 +224,12 @@ struct mdesc { }; -int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2); +int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2, void* s_heap, void* r_heap); void mmalloc_display_info(void *h); +const char* get_addr_memory_map(void *addr, void* s_heap, void* r_heap); + /* Bits to look at in the malloc descriptor flags word */ #define MMALLOC_DEVZERO (1 << 0) /* Have mapped to /dev/zero */