From: Marion Guthmuller Date: Mon, 1 Apr 2013 12:33:01 +0000 (+0200) Subject: model-checker : update state equality detection X-Git-Tag: v3_9_90~412^2~68 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d1881aa45492b97948d3eff7b8c5357571e2142d model-checker : update state equality detection - ignore field in mmalloc meta-data equal to the amount of elements to ignore in this area - match_equals was applied twice in heap comparison algorithm, remove one unnecessary call - apply these changes in system-state equality comparison --- diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 73886842c9..da1efaaba8 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -72,33 +72,17 @@ static int compare_global_variables(int region_type, void *d1, void *d2){ /* reg } i = 0; while(i < current_var->size){ - if(memcmp((char*)d1 + offset + i, (char*)d2 + offset + i, 1) != 0){ + if(memcmp((char *)d1 + offset + i, (char *)d2 + offset + i, 1) != 0){ pointer_align = (i / sizeof(void*)) * sizeof(void*); addr_pointed1 = *((void **)((char *)d1 + offset + pointer_align)); addr_pointed2 = *((void **)((char *)d2 + offset + pointer_align)); if((addr_pointed1 > plt_start && addr_pointed1 < plt_end) || (addr_pointed2 > plt_start && addr_pointed2 < plt_end)){ - break; - }else{ - if((addr_pointed1 > std_heap) && ((char *)addr_pointed1 < (char *)std_heap + STD_HEAP_SIZE) - && (addr_pointed2 > std_heap) && ((char *)addr_pointed2 < (char *)std_heap + STD_HEAP_SIZE)){ - res_compare = compare_area(addr_pointed1, addr_pointed2, NULL); - if(res_compare == 1){ - #ifdef MC_VERBOSE - if(region_type == 2) - XBT_VERB("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); - else - XBT_VERB("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); - #endif - #ifdef MC_DEBUG - if(region_type == 2) - XBT_DEBUG("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); - else - XBT_DEBUG("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); - #endif - XBT_INFO("Different global variable (%p, %p) : %s at addresses %p - %p (size = %zu)", current_var->address, addr_pointed1, current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); - return 1; - } - }else{ + i = pointer_align + sizeof(void*); + continue; + }else if((addr_pointed1 > std_heap) && ((char *)addr_pointed1 < (char *)std_heap + STD_HEAP_SIZE) + && (addr_pointed2 > std_heap) && ((char *)addr_pointed2 < (char *)std_heap + STD_HEAP_SIZE)){ + res_compare = compare_area(addr_pointed1, addr_pointed2, NULL); + if(res_compare == 1){ #ifdef MC_VERBOSE if(region_type == 2) XBT_VERB("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); @@ -111,12 +95,26 @@ static int compare_global_variables(int region_type, void *d1, void *d2){ /* reg else XBT_DEBUG("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); #endif - XBT_INFO("Different global variable (%p, %p) : %s at addresses %p - %p (size = %zu)", current_var->address, addr_pointed1, current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); return 1; } - - } - } + i = pointer_align + sizeof(void*); + continue; + }else{ + #ifdef MC_VERBOSE + if(region_type == 2) + XBT_VERB("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); + else + XBT_VERB("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); + #endif + #ifdef MC_DEBUG + if(region_type == 2) + XBT_DEBUG("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); + else + XBT_DEBUG("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size); + #endif + return 1; + } + } i++; } } @@ -409,49 +407,48 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ xbt_os_timer_start(timer); #endif - /* Stacks comparison */ - unsigned int cursor = 0; - int diff_local = 0; - is_diff = 0; + /* Stacks comparison */ + unsigned int cursor = 0; + int diff_local = 0; + is_diff = 0; - while(cursor < xbt_dynar_length(s1->stacks)){ - diff_local = compare_local_variables(((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->local_variables->data); - if(diff_local > 0){ - #ifdef MC_DEBUG - if(is_diff == 0){ - xbt_os_timer_stop(timer); - mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer); - } - XBT_DEBUG("Different local variables between stacks %d", cursor + 1); - errors++; - is_diff = 1; - #else + while(cursor < xbt_dynar_length(s1->stacks)){ + diff_local = compare_local_variables(((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->local_variables->data); + if(diff_local > 0){ + #ifdef MC_DEBUG + if(is_diff == 0){ + xbt_os_timer_stop(timer); + mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer); + } + XBT_DEBUG("Different local variables between stacks %d", cursor + 1); + errors++; + is_diff = 1; + #else - #ifdef MC_VERBOSE - XBT_VERB("Different local variables between stacks %d", cursor + 1); - #endif - - reset_heap_information(); - 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; + #ifdef MC_VERBOSE + XBT_VERB("Different local variables between stacks %d", cursor + 1); #endif - } - cursor++; + + reset_heap_information(); + 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 } + cursor++; + } - #ifdef MC_DEBUG - xbt_os_timer_start(timer); - #endif + #ifdef MC_DEBUG + xbt_os_timer_start(timer); + #endif /* Compare heap */ - if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data)){ #ifdef MC_DEBUG @@ -572,7 +569,7 @@ static int compare_local_variables(char *s1, char *s2){ continue; }else { #ifdef MC_VERBOSE - XBT_VERB("Different local variable : %s at addresses %p - %p", var_name, addr1, addr2); + XBT_VERB("Different local variable : %s at addresses %p - %p in frame %s", var_name, addr1, addr2, frame_name1); #endif #ifdef MC_DEBUG XBT_DEBUG("Different local variable : %s at addresses %p - %p", var_name, addr1, addr2); @@ -595,7 +592,7 @@ static int compare_local_variables(char *s1, char *s2){ continue; }else { #ifdef MC_VERBOSE - XBT_VERB("Different local variable : %s (%s - %s)", var_name, xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *)); + XBT_VERB("Different local variable : %s (%s - %s) in frame %s", var_name, xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *), frame_name1); #endif #ifdef MC_DEBUG XBT_DEBUG("Different local variable : %s (%s - %s)", var_name, xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *)); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 025dfe02de..43d50974e9 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -856,10 +856,10 @@ void MC_ignore_heap(void *address, size_t size){ if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){ region->fragment = -1; - ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore = 1; + ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++; }else{ region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type; - ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment] = 1; + ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++; } if(mc_heap_comparison_ignore == NULL){ diff --git a/src/xbt/mmalloc/mfree.c b/src/xbt/mmalloc/mfree.c index a6735e019f..ad5e05e45e 100644 --- a/src/xbt/mmalloc/mfree.c +++ b/src/xbt/mmalloc/mfree.c @@ -55,7 +55,7 @@ void mfree(struct mdesc *mdp, void *ptr) mdp -> heapinfo[block].busy_block.size * BLOCKSIZE; if(MC_is_active()){ - if(mdp->heapinfo[block].busy_block.ignore == 1) + if(mdp->heapinfo[block].busy_block.ignore > 0) MC_remove_ignore_heap(ptr, mdp -> heapinfo[block].busy_block.busy_size); } @@ -162,7 +162,7 @@ void mfree(struct mdesc *mdp, void *ptr) } if(MC_is_active()){ - if(mdp->heapinfo[block].busy_frag.ignore[frag_nb] == 1) + if(mdp->heapinfo[block].busy_frag.ignore[frag_nb] > 0) MC_remove_ignore_heap(ptr, mdp->heapinfo[block].busy_frag.frag_size[frag_nb]); } diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c index bede1626fa..b80543e668 100644 --- a/src/xbt/mmalloc/mm_diff.c +++ b/src/xbt/mmalloc/mm_diff.c @@ -215,7 +215,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ addr_block2 = ((void*) (((ADDR2UINT(current_block)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase)); - res_compare = compare_area(addr_block1, addr_block2, previous); + res_compare = compare_area(addr_block1, addr_block2, NULL); if(res_compare == 0){ for(k=1; k < heapinfo2[current_block].busy_block.size; k++) @@ -223,7 +223,6 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ for(k=1; k < heapinfo1[current_block].busy_block.size; k++) heapinfo1[current_block+k].busy_block.equal_to = new_heap_area(i1, -1); equal = 1; - match_equals(previous); i1 = i1 + heapinfo1[current_block].busy_block.size; } @@ -251,8 +250,8 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ i2++; continue; } - - res_compare = compare_area(addr_block1, addr_block2, previous); + + res_compare = compare_area(addr_block1, addr_block2, NULL); if(res_compare == 0){ for(k=1; k < heapinfo2[i2].busy_block.size; k++) @@ -260,7 +259,6 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ for(k=1; k < heapinfo1[i1].busy_block.size; k++) heapinfo1[i1+k].busy_block.equal_to = new_heap_area(i2, -1); equal = 1; - match_equals(previous); i1 = i1 + heapinfo1[i1].busy_block.size; } @@ -301,16 +299,15 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ addr_block2 = ((void*) (((ADDR2UINT(current_block)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase)); addr_frag2 = (void*) ((char *)addr_block2 + (current_fragment << ((xbt_mheap_t)s_heap)->heapinfo[current_block].type)); - res_compare = compare_area(addr_frag1, addr_frag2, previous); + res_compare = compare_area(addr_frag1, addr_frag2, NULL); - if(res_compare == 0){ + if(res_compare == 0) equal = 1; - match_equals(previous); - } xbt_dynar_reset(previous); - } + } + } while(i2 <= heaplimit && !equal){ @@ -323,7 +320,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ for(j2=0; j2 < (size_t) (BLOCKSIZE >> heapinfo2[i2].type); j2++){ - if(heapinfo2[i2].type == heapinfo1[i1].type && i2 == current_block && j2 == current_fragment) + if(i2 == current_block && j2 == current_fragment) continue; if(heapinfo2[i2].busy_frag.equal_to[j2] != NULL) @@ -332,11 +329,10 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){ addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase)); addr_frag2 = (void*) ((char *)addr_block2 + (j2 << ((xbt_mheap_t)s_heap)->heapinfo[i2].type)); - res_compare = compare_area(addr_frag1, addr_frag2, previous); + res_compare = compare_area(addr_frag1, addr_frag2, NULL); if(res_compare == 0){ equal = 1; - match_equals(previous); xbt_dynar_reset(previous); break; } @@ -529,7 +525,7 @@ static size_t heap_comparison_ignore_size(xbt_dynar_t ignore_list, void *address } -int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code : 0 = equal, 1 = same size but different bytes, 2 = different size used */ +int compare_area(void *area1, void* area2, xbt_dynar_t previous){ size_t i = 0, pointer_align = 0, ignore1 = 0, ignore2 = 0; void *addr_pointed1, *addr_pointed2; @@ -537,7 +533,6 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code ssize_t block1, frag1, block2, frag2; ssize_t size; int check_ignore = 0; - int j; void *addr_block1, *addr_block2, *addr_frag1, *addr_frag2; void *area1_to_compare, *area2_to_compare; @@ -573,26 +568,22 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code if(heapinfo1[block1].type == heapinfo2[block2].type){ - if(heapinfo1[block1].type == -1){ + if(heapinfo1[block1].type == -1){ /* Free block */ if(match_pairs){ match_equals(previous); xbt_dynar_free(&previous); } return 0; - }else if(heapinfo1[block1].type == 0){ - if(heapinfo1[block1].busy_block.equal_to != NULL || heapinfo2[block2].busy_block.equal_to != NULL){ + }else if(heapinfo1[block1].type == 0){ /* Complete block */ + + if(heapinfo1[block1].busy_block.equal_to != NULL && heapinfo2[block2].busy_block.equal_to != NULL){ if(equal_blocks(block1, block2)){ if(match_pairs){ match_equals(previous); xbt_dynar_free(&previous); } return 0; - }else{ - if(match_pairs){ - xbt_dynar_free(&previous); - } - return 1; } } @@ -607,7 +598,7 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code if(match_pairs){ xbt_dynar_free(&previous); } - return 2; + return 1; } if(!add_heap_area_pair(previous, block1, -1, block2, -1)){ @@ -634,8 +625,8 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code area1_to_compare = addr_block1; area2_to_compare = addr_block2; - if(heapinfo1[block1].busy_block.ignore == 1 && heapinfo2[block2].busy_block.ignore == 1) - check_ignore = 1; + if((heapinfo1[block1].busy_block.ignore > 0) && (heapinfo2[block2].busy_block.ignore == heapinfo1[block1].busy_block.ignore)) + check_ignore = heapinfo1[block1].busy_block.ignore; }else{ frag1 = ((uintptr_t) (ADDR2UINT (area1) % (BLOCKSIZE))) >> heapinfo1[block1].type; @@ -647,18 +638,13 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code area1_to_compare = addr_frag1; area2_to_compare = addr_frag2; - if(heapinfo1[block1].busy_frag.equal_to[frag1] != NULL || heapinfo2[block2].busy_frag.equal_to[frag2] != NULL){ + if(heapinfo1[block1].busy_frag.equal_to[frag1] != NULL && heapinfo2[block2].busy_frag.equal_to[frag2] != NULL){ if(equal_fragments(block1, frag1, block2, frag2)){ if(match_pairs){ match_equals(previous); xbt_dynar_free(&previous); } return 0; - }else{ - if(match_pairs){ - xbt_dynar_free(&previous); - } - return 1; } } @@ -666,7 +652,7 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code if(match_pairs){ xbt_dynar_free(&previous); } - return 2; + return 1; } if(!add_heap_area_pair(previous, block1, frag1, block2, frag2)){ @@ -687,8 +673,8 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code return 0; } - if(heapinfo1[block1].busy_frag.ignore[frag1] == 1 && heapinfo2[block2].busy_frag.ignore[frag2] == 1) - check_ignore = 1; + if((heapinfo1[block1].busy_frag.ignore[frag1] > 0) && ( heapinfo2[block2].busy_frag.ignore[frag2] == heapinfo1[block1].busy_frag.ignore[frag1])) + check_ignore = heapinfo1[block1].busy_frag.ignore[frag1]; } @@ -704,11 +690,6 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code xbt_dynar_free(&previous); } return 0; - }else{ - if(match_pairs){ - xbt_dynar_free(&previous); - } - return 1; } } @@ -716,7 +697,7 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code if(match_pairs){ xbt_dynar_free(&previous); } - return 2; + return 1; } if(!add_heap_area_pair(previous, block1, frag1, block2, frag2)){ @@ -743,8 +724,8 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code return 0; } - if(heapinfo1[block1].busy_frag.ignore[frag1] == 1 && heapinfo2[block2].busy_frag.ignore[frag2] == 1) - check_ignore = 1; + if((heapinfo1[block1].busy_frag.ignore[frag1] > 0) && (heapinfo2[block2].busy_frag.ignore[frag2] == heapinfo1[block1].busy_frag.ignore[frag1])) + check_ignore = heapinfo1[block1].busy_frag.ignore[frag1]; }else{ if(match_pairs){ @@ -755,43 +736,45 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){ /* Return code while(i 0){ if((ignore1 = heap_comparison_ignore_size(to_ignore1, (char *)area1 + i)) > 0){ if((ignore2 = heap_comparison_ignore_size(to_ignore2, (char *)area2 + i)) == ignore1){ i = i + ignore2; + check_ignore--; continue; } } } - pointer_align = (i / sizeof(void*)) * sizeof(void*); - addr_pointed1 = *((void **)((char *)area1_to_compare + pointer_align)); - addr_pointed2 = *((void **)((char *)area2_to_compare + pointer_align)); + if(memcmp(((char *)area1_to_compare) + i, ((char *)area2_to_compare) + i, 1) != 0){ - if(addr_pointed1 > maestro_stack_start && addr_pointed1 < maestro_stack_end && addr_pointed2 > maestro_stack_start && addr_pointed2 < maestro_stack_end){ - i = pointer_align + sizeof(void *); - continue; - }else if((addr_pointed1 > s_heap) && ((char *)addr_pointed1 < (char *)s_heap + STD_HEAP_SIZE) + pointer_align = (i / sizeof(void*)) * sizeof(void*); + addr_pointed1 = *((void **)((char *)area1_to_compare + pointer_align)); + addr_pointed2 = *((void **)((char *)area2_to_compare + pointer_align)); + + if(addr_pointed1 > maestro_stack_start && addr_pointed1 < maestro_stack_end && addr_pointed2 > maestro_stack_start && addr_pointed2 < maestro_stack_end){ + i = pointer_align + sizeof(void *); + continue; + }else if((addr_pointed1 > s_heap) && ((char *)addr_pointed1 < (char *)s_heap + STD_HEAP_SIZE) && (addr_pointed2 > s_heap) && ((char *)addr_pointed2 < (char *)s_heap + STD_HEAP_SIZE)){ - res_compare = compare_area(addr_pointed1, addr_pointed2, previous); - if(res_compare != 0){ - if(match_pairs) - xbt_dynar_free(&previous); - return res_compare; - } - }else{ - j=0; - while(j