From abe361354c941e1725e122f12a1bcce332a5a716 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Mon, 1 Oct 2012 17:08:01 +0200 Subject: [PATCH] model-checker : check if a difference detected in stack comparison is a pointer on block or fragment previously free --- include/xbt/mmalloc.h | 2 ++ src/mc/mc_compare.c | 38 +++++++++++++++++++++++++++----------- src/xbt/mmalloc/mm_diff.c | 32 ++++++++++++++++++++++++++++++++ 3 files changed, 61 insertions(+), 11 deletions(-) diff --git a/include/xbt/mmalloc.h b/include/xbt/mmalloc.h index e47604ffb5..0c706ee990 100644 --- a/include/xbt/mmalloc.h +++ b/include/xbt/mmalloc.h @@ -64,6 +64,8 @@ int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2); void mmalloc_backtrace_block_display(void* heapinfo, int block); void mmalloc_backtrace_fragment_display(void* heapinfo, int block, int frag); +int is_free_area(void *area, xbt_mheap_t heap); + #endif /* MMALLOC_H */ diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 5e7db16994..6ae4bb8332 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -15,7 +15,7 @@ static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size); 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, xbt_dynar_t equals); +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 int data_program_region_compare(void *d1, void *d2, size_t size){ @@ -83,6 +83,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), NULL); xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), NULL); xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), NULL); + + void *heap1 = NULL, *heap2 = NULL; if(s1->num_reg != s2->num_reg){ XBT_DEBUG("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg); @@ -111,6 +113,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ XBT_DEBUG("Different heap (mmalloc_compare)"); return 1; } + heap1 = s1->regions[i]->data; + heap2 = s2->regions[i]->data; break; case 1 : /* Compare data libsimgrid region */ @@ -151,18 +155,23 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ /* Stacks comparison */ unsigned int cursor = 1; stack_region_t stack_region1, stack_region2; - void *stack_pointer1, *stack_pointer2; + void *sp1, *sp2; + int diff = 0; while(cursor < xbt_dynar_length(stacks1)){ + XBT_DEBUG("Stack %d", cursor + 1); stack_region1 = (stack_region_t)(xbt_dynar_get_as(stacks1, cursor, stack_region_t)); stack_region2 = (stack_region_t)(xbt_dynar_get_as(stacks2, cursor, stack_region_t)); - stack_pointer1 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->stack_pointer; - stack_pointer2 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->stack_pointer; - if(compare_stack(stack_region1, stack_region2, stack_pointer1, stack_pointer2, equals) > 0) - return 1; + sp1 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->stack_pointer; + sp2 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->stack_pointer; + diff += compare_stack(stack_region1, stack_region2, sp1, sp2, heap1, heap2, equals); cursor++; } + XBT_DEBUG("Hamming distance between stacks : %d", diff); + if(diff>0) + return 1; + return 0; } @@ -196,25 +205,32 @@ static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2){ } -static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void *sp2, xbt_dynar_t equals){ +static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void *sp2, void *heap1, void *heap2, xbt_dynar_t equals){ int k = 0, nb_diff = 0; long size_used1 = (long)s1->size - (long)((char*)sp1 - (char*)s1->address); long size_used2 = (long)s2->size - (long)((char*)sp2 - (char*)s2->address); int pointer_align; - void *addr_pointed1 = NULL, *addr_pointed2 = NULL; + void *addr_pointed1 = NULL, *addr_pointed2 = NULL; if(size_used1 == size_used2){ - + while(k < size_used1){ if(memcmp((char *)s1->address + s1->size - k, (char *)s2->address + s2->size - k, 1) != 0){ pointer_align = ((size_used1 - k) / sizeof(void*)) * sizeof(void*); addr_pointed1 = *((void **)(((char*)s1->address + (s1->size - size_used1)) + pointer_align)); addr_pointed2 = *((void **)(((char*)s2->address + (s2->size - size_used2)) + pointer_align)); if(is_heap_equality(equals, addr_pointed1, addr_pointed2) == 0){ - XBT_DEBUG("Difference at offset %d (%p - %p)", k, (char *)s1->address + s1->size - k, (char *)s2->address + s2->size - k); - nb_diff++; + if((addr_pointed1 > std_heap) && (addr_pointed1 < (void *)((char *)std_heap + STD_HEAP_SIZE)) && (addr_pointed2 > std_heap) && (addr_pointed2 < (void *)((char *)std_heap + STD_HEAP_SIZE))){ + if(is_free_area(addr_pointed1, (xbt_mheap_t)heap1) == 0 || is_free_area(addr_pointed2, (xbt_mheap_t)heap2) == 0){ + XBT_DEBUG("Difference at offset %d (%p - %p)", k, (char *)s1->address + s1->size - k, (char *)s2->address + s2->size - k); + nb_diff++; + } + }else{ + XBT_DEBUG("Difference at offset %d (%p - %p)", k, (char *)s1->address + s1->size - k, (char *)s2->address + s2->size - k); + nb_diff++; + } } } k++; diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c index a6da0077ea..ac7fe3584d 100644 --- a/src/xbt/mmalloc/mm_diff.c +++ b/src/xbt/mmalloc/mm_diff.c @@ -1061,4 +1061,36 @@ static void remove_heap_equality(xbt_dynar_t *equals, int address, void *a){ } +} + +int is_free_area(void *area, xbt_mheap_t heap){ + + void *sheap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - getpagesize(); + malloc_info *heapinfo = (malloc_info *)((char *)heap + ((uintptr_t)((char *)heap->heapinfo - (char *)sheap))); + size_t heapsize = heap->heapsize; + + /* Get block number */ + size_t block = ((char*)area - (char*)((xbt_mheap_t)sheap)->heapbase) / BLOCKSIZE + 1; + size_t fragment; + + /* Check if valid block number */ + if((char *)area < (char*)((xbt_mheap_t)sheap)->heapbase || block > heapsize || block < 1) + return 0; + + if(heapinfo[block].type < 0) + return 1; + + if(heapinfo[block].type == 0) + return 0; + + if(heapinfo[block].type > 0){ + fragment = ((uintptr_t) (ADDR2UINT(area) % (BLOCKSIZE))) >> heapinfo[block].type; + if(heapinfo[block].busy_frag.frag_size[fragment] == 0) + return 1; + } + + return 0; + + + } -- 2.20.1