model-checker : check if a difference detected in stack comparison is a pointer on...

diff --git a/include/xbt/mmalloc.h b/include/xbt/mmalloc.h
index e47604f..0c706ee 100644 (file)
--- 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 5e7db16..6ae4bb8 100644 (file)
--- 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 a6da007..ac7fe35 100644 (file)
--- 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;
+  
+
+
 }