From fff99c2e390f3924dfc68006fbc5c214370df751 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Fri, 28 Oct 2011 16:14:22 +0200 Subject: [PATCH] model-checker : function mmalloc_compare_mdesc fixed (blocks unchecked) --- src/xbt/mmalloc/mm_legacy.c | 227 ++++++++++++++---------------------- 1 file changed, 85 insertions(+), 142 deletions(-) diff --git a/src/xbt/mmalloc/mm_legacy.c b/src/xbt/mmalloc/mm_legacy.c index ba34bff94f..216babd93c 100644 --- a/src/xbt/mmalloc/mm_legacy.c +++ b/src/xbt/mmalloc/mm_legacy.c @@ -219,7 +219,10 @@ int mmalloc_compare_heap(void *h1, void *h2){ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ - if(mdp1->headersize != mdp2->headersize){ + struct mdesc* mdp; + + + if(mdp1->headersize != mdp2->headersize){ XBT_DEBUG("Different size of the file header for the mapped files"); return 1; } @@ -244,19 +247,20 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ return 1; } - //XBT_DEBUG("Heap size : %d", mdp1->heapsize); + // XBT_DEBUG("Heap size : %Zu", mdp1->heapsize); if(mdp1->heapbase != mdp2->heapbase){ XBT_DEBUG("Different first block of the heap"); return 1; } + if(mdp1->heapindex != mdp2->heapindex){ XBT_DEBUG("Different index for the heap table"); return 1; } - //XBT_DEBUG("Heap index : %d", mdp1->heapindex); + //XBT_DEBUG("Heap index : %Zu", mdp1->heapindex); if(mdp1->base != mdp2->base){ XBT_DEBUG("Different base address of the memory region"); @@ -278,7 +282,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ return 1; } - //XBT_DEBUG("Heap limit : %d", mdp1->heaplimit); + //XBT_DEBUG("Heap limit : %Zu", mdp1->heaplimit); if(mdp1->fd != mdp2->fd){ @@ -297,172 +301,111 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){ } - size_t block_free1, start1, block_free2 , start2, block_busy1, block_busy2 ; - size_t i; + size_t block_free1, block_free2 , next_block_free, first_block_free ; + size_t i, j; void *addr_block1, *addr_block2; - struct mdesc* mdp; - - start1 = block_free1 = mdp1->heapindex; - start2 = block_free2 = mdp2->heapindex; - block_busy1 = start1 + mdp1->heapinfo[start1].free.size; - block_busy2 = start2 + mdp2->heapinfo[start2].free.size; - - //XBT_DEBUG("Block busy : %Zu - %Zu", block_busy1, block_busy2); - - - if(mdp1->heapinfo[start1].free.size != mdp2->heapinfo[start2].free.size){ // <=> check block_busy - - XBT_DEBUG("Different size (in blocks) of a free cluster"); - return 1; - - }else{ - if(mdp1->heapinfo[start1].free.next != mdp2->heapinfo[start1].free.next){ - - XBT_DEBUG("Different index of next free cluster"); - return 1; - - }else{ - - i=block_busy1 ; - - //XBT_DEBUG("Next free : %Zu", mdp1->heapinfo[start1].free.next); + + /* Search index of the first free block */ - while(iheapinfo[start1].free.next){ + block_free1 = mdp1->heapindex; + block_free2 = mdp2->heapindex; - //XBT_DEBUG("i (block busy) : %Zu", i); + while(mdp1->heapinfo[block_free1].free.prev != 0){ + block_free1 = mdp1->heapinfo[block_free1].free.prev; + } - if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){ - XBT_DEBUG("Different type of busy block"); - return 1; - }else{ - mdp = mdp1; - addr_block1 = ADDRESS(i); - mdp = mdp2; - addr_block2 = ADDRESS(i); - switch(mdp1->heapinfo[i].busy.type){ - case 0 : - if(mdp1->heapinfo[i].busy.info.size != mdp2->heapinfo[i].busy.info.size){ - XBT_DEBUG("Different size of a large cluster"); - return 1; - }else{ - //XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu (%Zu blocks)", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE),mdp->heapinfo[i].busy.info.size ); - if(memcmp(addr_block1, addr_block2, mdp1->heapinfo[i].busy.info.size * BLOCKSIZE) != 0){ - XBT_DEBUG("Different data in block %Zu", i); - return 1; - } - } - i = i + mdp1->heapinfo[i].busy.info.size; - break; - default : - if(mdp1->heapinfo[i].busy.info.frag.nfree != mdp2->heapinfo[i].busy.info.frag.nfree){ - XBT_DEBUG("Different free fragments in a fragmented block"); - return 1; - }else{ - if(mdp1->heapinfo[i].busy.info.frag.first != mdp2->heapinfo[i].busy.info.frag.first){ - XBT_DEBUG("Different first free fragments of the block"); - return 1; - }else{ - if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){ - XBT_DEBUG("Different data in block %Zu", i); - return 1; - } - } - } - i++; - break; - } - } - } + while(mdp2->heapinfo[block_free2].free.prev != 0){ + block_free2 = mdp1->heapinfo[block_free2].free.prev; + } + if(block_free1 != block_free2){ + XBT_DEBUG("Different first free block"); + return 1; + } - block_free1 = mdp1->heapinfo[start1].free.next; - block_free2 = mdp2->heapinfo[start2].free.next; + first_block_free = block_free1; - //XBT_DEBUG("Index of next free cluster : %d", block_free1); + if(mdp1->heapinfo[block_free1].free.size != mdp2->heapinfo[block_free2].free.size){ + XBT_DEBUG("Different size (in blocks) of the first free cluster"); + return 1; + } - while((block_free1 != start1) && (block_free2 != start2)){ + /* Check busy blocks (circular checking)*/ - block_busy1 = block_free1 + mdp1->heapinfo[block_free1].free.size; - block_busy2 = block_free2 + mdp2->heapinfo[block_free2].free.size; + i = block_free1 + mdp1->heapinfo[block_free1].free.size; + next_block_free = mdp1->heapinfo[block_free1].free.next; - if(block_busy1 != block_busy2){ - XBT_DEBUG("Different index of busy block"); - return 1; - }else{ + if(next_block_free == 0) + next_block_free = mdp1->heaplimit; - //XBT_DEBUG("Index of next busy block : %Zu - %Zu", block_busy1, block_busy2); - //XBT_DEBUG("Index of next free cluster : %Zu", mdp1->heapinfo[block_free1].free.next); - - i = block_busy1; - while(iheapinfo[block_free1].free.next){ + while(i != first_block_free){ - //XBT_DEBUG("i (block busy) : %Zu", i); + while(iheapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){ - XBT_DEBUG("Different type of busy block"); + if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){ + XBT_DEBUG("Different type of busy block"); + return 1; + }else{ + if(i == 0) + j++; + mdp = mdp1; + addr_block1 = ADDRESS(j); + mdp = mdp2; + addr_block2 = ADDRESS(j); + switch(mdp1->heapinfo[i].busy.type){ + case 0 : + if(mdp1->heapinfo[i].busy.info.size != mdp2->heapinfo[i].busy.info.size){ + XBT_DEBUG("Different size of a large cluster"); + return 1; + }else{ + if(memcmp(addr_block1, addr_block2, (mdp1->heapinfo[i].busy.info.size * BLOCKSIZE)) != 0){ + XBT_DEBUG("Different data in block %Zu", i); return 1; + } + } + i = i+mdp1->heapinfo[i].busy.info.size; + break; + default : + if(mdp1->heapinfo[i].busy.info.frag.nfree != mdp2->heapinfo[i].busy.info.frag.nfree){ + XBT_DEBUG("Different free fragments in a fragmented block"); + return 1; + }else{ + if(mdp1->heapinfo[i].busy.info.frag.first != mdp2->heapinfo[i].busy.info.frag.first){ + XBT_DEBUG("Different first free fragments of the block"); + return 1; }else{ - mdp = mdp1; - addr_block1 = ADDRESS(i); - mdp = mdp2; - addr_block2 = ADDRESS(i); - switch(mdp1->heapinfo[i].busy.type){ - case 0 : - if(mdp1->heapinfo[i].busy.info.size != mdp2->heapinfo[i].busy.info.size){ - XBT_DEBUG("Different size of a large cluster"); - return 1; - }else{ - //XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE)); - //XBT_DEBUG("Size of large cluster %d", mdp->heapinfo[i].busy.info.size); - if(memcmp(addr_block1, addr_block2, (mdp1->heapinfo[i].busy.info.size * BLOCKSIZE)) != 0){ - XBT_DEBUG("Different data in block %Zu", i); - return 1; - } - } - i = i+mdp1->heapinfo[i].busy.info.size; - break; - default : - if(mdp1->heapinfo[i].busy.info.frag.nfree != mdp2->heapinfo[i].busy.info.frag.nfree){ - XBT_DEBUG("Different free fragments in a fragmented block"); - return 1; - }else{ - if(mdp1->heapinfo[i].busy.info.frag.first != mdp2->heapinfo[i].busy.info.frag.first){ - XBT_DEBUG("Different first free fragments of the block"); - return 1; - }else{ - if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){ - XBT_DEBUG("Different data in fragmented block %Zu", i); - return 1; - } - } - } - i++; - break; - } + if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){ + XBT_DEBUG("Different data in fragmented block %Zu", i); + return 1; + } } - - } + i++; + break; } + } + } - block_free1 = mdp1->heapinfo[block_free1].free.next; - block_free2 = mdp2->heapinfo[block_free2].free.next; - - } - + + block_free1 = mdp1->heapinfo[block_free1].free.next; + next_block_free = mdp1->heapinfo[block_free1].free.next; + if(i != first_block_free){ + if(block_free1 != 0) + i = block_free1 + mdp1->heapinfo[block_free1].free.size; + else + i = 0; } + + } - } return 0; - } -- 2.20.1