From: Marion Guthmuller Date: Fri, 22 Jun 2012 15:44:40 +0000 (+0200) Subject: model-checker : detect pointers on valid fragment in heap comparison algorithm X-Git-Tag: v3_8~479 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/82588cd669285c1f7aa78a1d97745406e9080d54 model-checker : detect pointers on valid fragment in heap comparison algorithm --- diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index 6e86e52f1a..4e2f36cd62 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -950,9 +950,11 @@ void MC_ddfs(int search_cycle){ /* Debug information */ + MC_SET_RAW_MEM; req_str = MC_request_to_string(req, value); XBT_INFO("Execute: %s", req_str); xbt_free(req_str); + MC_UNSET_RAW_MEM; MC_state_set_executed_request(current_pair->graph_state, req, value); diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c index 60fb787b6e..c0701553a2 100644 --- a/src/xbt/mmalloc/mm_diff.c +++ b/src/xbt/mmalloc/mm_diff.c @@ -145,7 +145,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ size_t i, j; void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2; - size_t frag_size; + size_t frag_size, frag_size_pointed; i = 1; @@ -157,7 +157,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ void *address_pointed1, *address_pointed2; int block_pointed1, block_pointed2; - void *addr_block_pointed1, *addr_block_pointed2; + void *addr_block_pointed1, *addr_block_pointed2, *addr_frag_pointed1, *addr_frag_pointed2; /* Check busy blocks*/ @@ -193,7 +193,6 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ //for(k=0;kheapinfo[i].busy_block.size * BLOCKSIZE;k++){ for(k=0;kheapinfo[i].busy_block.busy_size;k++){ - //if((((char *)addr_block1) + k != 0) && (((char *)addr_block2) + k != 0)){ if(memcmp(((char *)addr_block1) + k, ((char *)addr_block2) + k, 1) != 0){ fprintf(stderr, "Different byte (offset=%d) (%p - %p) in block %zu\n", k, (char *)addr_block1 + k, (char *)addr_block2 + k, i); fflush(NULL); pointer_align = (k / sizeof(void*)) * sizeof(void*); @@ -202,7 +201,6 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ if(((address_pointed1 > (void *)s_heap) && (address_pointed1 < mdp1->breakval)) && ((address_pointed2 > (void *)s_heap) && (address_pointed2 < mdp2->breakval))){ block_pointed1 = ((char*)address_pointed1 - (char*)((struct mdesc*)s_heap)->heapbase) % BLOCKSIZE; block_pointed2 = ((char*)address_pointed2 - (char*)((struct mdesc*)s_heap)->heapbase) % BLOCKSIZE; - //fprintf(stderr, "Blocks pointed : %d - %d\n", block_pointed1, block_pointed2); if((block_pointed1 == 0) && (block_pointed2 == 0)){ block_pointed1 = ((char*)address_pointed1 - (char*)((struct mdesc*)s_heap)->heapbase) / BLOCKSIZE + 1; block_pointed2 = ((char*)address_pointed2 - (char*)((struct mdesc*)s_heap)->heapbase) / BLOCKSIZE + 1; @@ -239,16 +237,38 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ distance++; } }else{ - /* FIXME : peut pointer vers le début d'un fragment mais dans un bloc */ - fprintf(stderr, "Pointed addresses (%p - %p) not valid\n", address_pointed1, address_pointed2); - distance++; + block_pointed1 = ((char*)address_pointed1 - (char*)((struct mdesc*)s_heap)->heapbase) / BLOCKSIZE + 1; + block_pointed2 = ((char*)address_pointed2 - (char*)((struct mdesc*)s_heap)->heapbase) / BLOCKSIZE + 1; + if((mdp1->heapinfo[block_pointed1].type == mdp2->heapinfo[block_pointed2].type) && (mdp1->heapinfo[block_pointed1].type > 0)){ + addr_block_pointed1 = (char*)((struct mdesc*)s_heap)->heapbase + ((block_pointed1 - 1)*BLOCKSIZE); + addr_block_pointed2 = (char*)((struct mdesc*)s_heap)->heapbase + ((block_pointed2 - 1)*BLOCKSIZE); + frag_size_pointed = pow (2,mdp1->heapinfo[block_pointed1].type); + if((((char*)address_pointed1 - (char*)addr_block_pointed1) % frag_size_pointed == 0) && (((char*)address_pointed2 - (char*)addr_block_pointed2) % frag_size_pointed == 0)){ + addr_frag_pointed1 = (char *)heapbase1 + ((char*)address_pointed1 - (char*)((struct mdesc*)s_heap)->heapbase); + addr_frag_pointed2 = (char *)heapbase2 + ((char*)address_pointed2 - (char*)((struct mdesc*)s_heap)->heapbase); + if(memcmp(addr_frag_pointed1, addr_frag_pointed2, frag_size_pointed) != 0){ + distance++; + }else{ + fprintf(stderr, "False difference detected\n"); + fflush(NULL); + } + }else{ + fprintf(stderr, "Pointed addresses (%p - %p) not valid \n", address_pointed1, address_pointed2); + fflush(NULL); + distance++; + } + }else{ + fprintf(stderr, "Pointed addresses (%p - %p) not valid \n", address_pointed1, address_pointed2); + fflush(NULL); + distance++; + } } }else{ fprintf(stderr, "Pointed addresses (%p - %p) not in std_heap\n", address_pointed1, address_pointed2); + fflush(NULL); distance++; } } - //} } @@ -305,7 +325,6 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ distance = 0; //for(k=0;kheapinfo[i].busy_frag.frag_size[j];k++){ - //if((((char *)addr_frag1) + k != 0) && (((char *)addr_frag2) + k != 0)){ if(memcmp(((char *)addr_frag1) + k, ((char *)addr_frag2) + k, 1) != 0){ 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); fflush(NULL); pointer_align = (k / sizeof(void*)) * sizeof(void*); @@ -349,16 +368,38 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ distance++; } }else{ - /* FIXME : peut pointer vers le début d'un fragment mais dans un bloc */ - fprintf(stderr, "Pointed addresses (%p - %p) not valid \n", address_pointed1, address_pointed2); - distance++; + block_pointed1 = ((char*)address_pointed1 - (char*)((struct mdesc*)s_heap)->heapbase) / BLOCKSIZE + 1; + block_pointed2 = ((char*)address_pointed2 - (char*)((struct mdesc*)s_heap)->heapbase) / BLOCKSIZE + 1; + if((mdp1->heapinfo[block_pointed1].type == mdp2->heapinfo[block_pointed2].type) && (mdp1->heapinfo[block_pointed1].type > 0)){ + addr_block_pointed1 = (char*)((struct mdesc*)s_heap)->heapbase + ((block_pointed1 - 1)*BLOCKSIZE); + addr_block_pointed2 = (char*)((struct mdesc*)s_heap)->heapbase + ((block_pointed2 - 1)*BLOCKSIZE); + frag_size_pointed = pow (2,mdp1->heapinfo[block_pointed1].type); + if((((char*)address_pointed1 - (char*)addr_block_pointed1) % frag_size_pointed == 0) && (((char*)address_pointed2 - (char*)addr_block_pointed2) % frag_size_pointed == 0)){ + addr_frag_pointed1 = (char *)heapbase1 + ((char*)address_pointed1 - (char*)((struct mdesc*)s_heap)->heapbase); + addr_frag_pointed2 = (char *)heapbase2 + ((char*)address_pointed2 - (char*)((struct mdesc*)s_heap)->heapbase); + if(memcmp(addr_frag_pointed1, addr_frag_pointed2, frag_size_pointed) != 0){ + distance++; + }else{ + fprintf(stderr, "False difference detected\n"); + fflush(NULL); + } + }else{ + fprintf(stderr, "Pointed addresses (%p - %p) not valid \n", address_pointed1, address_pointed2); + fflush(NULL); + distance++; + } + }else{ + fprintf(stderr, "Pointed addresses (%p - %p) not valid \n", address_pointed1, address_pointed2); + fflush(NULL); + distance++; + } } }else{ fprintf(stderr, "Pointed addresses (%p - %p) not in std_heap\n", address_pointed1, address_pointed2); + fflush(NULL); distance++; } } - //} }