model-checker : add block and fragment number in mc_ignore_region

diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h
index 4c6cda3..da5a3ca 100644 (file)
--- a/src/include/mc/datatypes.h
+++ b/src/include/mc/datatypes.h
@@ -15,6 +15,8 @@ SG_BEGIN_DECL()
 typedef struct s_mc_transition *mc_transition_t;
 
 typedef struct s_mc_ignore_region{
 typedef struct s_mc_transition *mc_transition_t;
 
 typedef struct s_mc_ignore_region{

+  int block;
+  int fragment;

   void *address;
   size_t size;
 }s_mc_ignore_region_t, *mc_ignore_region_t;
   void *address;
   size_t size;
 }s_mc_ignore_region_t, *mc_ignore_region_t;

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index d91af14..fa47253 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -10,6 +10,7 @@
 
 #include "../surf/surf_private.h"
 #include "../simix/smx_private.h"
 
 #include "../surf/surf_private.h"
 #include "../simix/smx_private.h"

+#include "../xbt/mmalloc/mmprivate.h"

 #include "xbt/fifo.h"
 #include "mc_private.h"
 #include "xbt/automaton.h"
 #include "xbt/fifo.h"
 #include "mc_private.h"
 #include "xbt/automaton.h"


@@ -653,6 +654,13 @@ void MC_ignore(void *address, size_t size){
   region = xbt_new0(s_mc_ignore_region_t, 1);
   region->address = address;
   region->size = size;
   region = xbt_new0(s_mc_ignore_region_t, 1);
   region->address = address;
   region->size = size;

+  region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
+
+  if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
+    region->fragment = -1;
+  }else{
+    region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
+  }

 
   unsigned int cursor = 0;
   mc_ignore_region_t current_region;
 
   unsigned int cursor = 0;
   mc_ignore_region_t current_region;

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 86431c7..6e36d0a 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -143,13 +143,13 @@ extern void *raw_heap;
 /* an API to query about the status of a heap, we simply call mmstats and */
 /* because I now how does structure looks like, then I redefine it here */
 
 /* an API to query about the status of a heap, we simply call mmstats and */
 /* because I now how does structure looks like, then I redefine it here */
 

-struct mstats {
-  size_t bytes_total;           /* Total size of the heap. */
-  size_t chunks_used;           /* Chunks allocated by the user. */
-  size_t bytes_used;            /* Byte total of user-allocated chunks. */
-  size_t chunks_free;           /* Chunks in the free list. */
-  size_t bytes_free;            /* Byte total of chunks in the free list. */
-};
+/* struct mstats { */
+/*   size_t bytes_total;           /\* Total size of the heap. *\/ */
+/*   size_t chunks_used;           /\* Chunks allocated by the user. *\/ */
+/*   size_t bytes_used;            /\* Byte total of user-allocated chunks. *\/ */
+/*   size_t chunks_free;           /\* Chunks in the free list. *\/ */
+/*   size_t bytes_free;            /\* Byte total of chunks in the free list. *\/ */
+/* }; */

 
 #define MC_SET_RAW_MEM    mmalloc_set_current_heap(raw_heap)
 #define MC_UNSET_RAW_MEM  mmalloc_set_current_heap(std_heap)
 
 #define MC_SET_RAW_MEM    mmalloc_set_current_heap(raw_heap)
 #define MC_UNSET_RAW_MEM  mmalloc_set_current_heap(std_heap)

diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c
index 395ec57..a33b54a 100644 (file)
--- a/src/xbt/mmalloc/mm_diff.c
+++ b/src/xbt/mmalloc/mm_diff.c
@@ -28,9 +28,10 @@ static void heap_area_pair_free_voidp(void *d);
 static int add_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2);
 static int is_new_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2);
 
 static int add_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2);
 static int is_new_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2);
 

-static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previous);
+static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previous, int check_ignore);

 static void match_equals(xbt_dynar_t list);
 
 static void match_equals(xbt_dynar_t list);
 

+static int in_mmalloc_ignore(int block, int fragment);

 static size_t heap_comparison_ignore(void *address);
 
 void mmalloc_backtrace_block_display(void* heapinfo, int block){
 static size_t heap_comparison_ignore(void *address);
 
 void mmalloc_backtrace_block_display(void* heapinfo, int block){


@@ -123,7 +124,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
   xbt_dynar_t previous = xbt_dynar_new(sizeof(heap_area_pair_t), heap_area_pair_free_voidp);
 
 
   xbt_dynar_t previous = xbt_dynar_new(sizeof(heap_area_pair_t), heap_area_pair_free_voidp);
 

-  int equal;
+  int equal, res_compare;

 
   ignore_done = 0;
 
 
   ignore_done = 0;
 


@@ -168,10 +169,20 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
         }
 
         addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)heapbase2));
         }
 
         addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)heapbase2));

-        
+

         /* Comparison */
         add_heap_area_pair(previous, i1, -1, i2, -1);
         /* Comparison */
         add_heap_area_pair(previous, i1, -1, i2, -1);

-        if(!compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous)){
+        
+        if(ignore_done < xbt_dynar_length(mmalloc_ignore)){
+          if(in_mmalloc_ignore((int)i1, -1))
+            res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 1);
+          else
+            res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 0);
+        }else{
+          res_compare = compare_area(addr_block1, addr_block2, heapinfo1[i1].busy_block.busy_size, previous, 0);
+        }
+        
+        if(!res_compare){

           for(k=0; k < heapinfo2[i2].busy_block.size; k++)
             heapinfo2[i2+k].busy_block.equal_to = 1;
           for(k=0; k < heapinfo1[i1].busy_block.size; k++)
           for(k=0; k < heapinfo2[i2].busy_block.size; k++)
             heapinfo2[i2+k].busy_block.equal_to = 1;
           for(k=0; k < heapinfo1[i1].busy_block.size; k++)


@@ -223,7 +234,17 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
              
             /* Comparison */
             add_heap_area_pair(previous, i1, j1, i2, j2);
              
             /* Comparison */
             add_heap_area_pair(previous, i1, j1, i2, j2);

-            if(!compare_area(addr_frag1, addr_frag2, heapinfo1[i1].busy_frag.frag_size[j1], previous)){
+            
+            if(ignore_done < xbt_dynar_length(mmalloc_ignore)){
+              if(in_mmalloc_ignore((int)i1, (int)j1))
+                res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[i1].busy_frag.frag_size[j1], previous, 1);
+              else
+                res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[i1].busy_frag.frag_size[j1], previous, 0);
+            }else{
+              res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[i1].busy_frag.frag_size[j1], previous, 0);
+            }
+
+            if(!res_compare){

               heapinfo2[i2].busy_frag.equal_to[j2] = 1;
               heapinfo1[i1].busy_frag.equal_to[j1] = 1;
               equal = 1;
               heapinfo2[i2].busy_frag.equal_to[j2] = 1;
               heapinfo1[i1].busy_frag.equal_to[j1] = 1;
               equal = 1;


@@ -358,6 +379,33 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
 }
 
 
 }
 

+static int in_mmalloc_ignore(int block, int fragment){
+
+  unsigned int cursor = 0;
+  int start = 0;
+  int end = xbt_dynar_length(mmalloc_ignore) - 1;
+  mc_ignore_region_t region;
+
+  while(start <= end){
+    cursor = (start + end) / 2;
+    region = (mc_ignore_region_t)xbt_dynar_get_as(mmalloc_ignore, cursor, mc_ignore_region_t);
+    if(region->block == block){
+      if(region->fragment == fragment)
+        return 1;
+      if(region->fragment < fragment)
+        start = cursor + 1;
+      if(region->fragment > fragment)
+        end = cursor - 1;
+    }
+    if(region->block < block)
+      start = cursor + 1;
+    if(region->block > block)
+      end = cursor - 1; 
+  }
+
+  return 0;
+}
+

 static size_t heap_comparison_ignore(void *address){
   unsigned int cursor = 0;
   int start = 0;
 static size_t heap_comparison_ignore(void *address){
   unsigned int cursor = 0;
   int start = 0;


@@ -379,7 +427,7 @@ static size_t heap_comparison_ignore(void *address){
 }
 
 
 }
 
 

-static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previous){
+static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previous, int check_ignore){

 
   size_t i = 0, pointer_align = 0, ignore1 = 0, ignore2 = 0;
   void *address_pointed1, *address_pointed2, *addr_block_pointed1, *addr_block_pointed2, *addr_frag_pointed1, *addr_frag_pointed2;
 
   size_t i = 0, pointer_align = 0, ignore1 = 0, ignore2 = 0;
   void *address_pointed1, *address_pointed2, *addr_block_pointed1, *addr_block_pointed2, *addr_frag_pointed1, *addr_frag_pointed2;


@@ -390,7 +438,7 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ
  
   while(i<size){
 
  
   while(i<size){
 

-    if(ignore_done < xbt_dynar_length(mmalloc_ignore)){
+    if(check_ignore){

 
       current_area1 = (char*)((xbt_mheap_t)s_heap)->heapbase + ((((char *)area1) + i) - (char *)heapbase1);
       if((ignore1 = heap_comparison_ignore(current_area1)) > 0){
 
       current_area1 = (char*)((xbt_mheap_t)s_heap)->heapbase + ((((char *)area1) + i) - (char *)heapbase1);
       if((ignore1 = heap_comparison_ignore(current_area1)) > 0){


@@ -435,8 +483,15 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ
           }
 
           if(add_heap_area_pair(previous, block_pointed1, -1, block_pointed2, -1)){
           }
 
           if(add_heap_area_pair(previous, block_pointed1, -1, block_pointed2, -1)){

-            
-            res_compare = compare_area(addr_block_pointed1, addr_block_pointed2, heapinfo1[block_pointed1].busy_block.busy_size, previous);
+
+            if(ignore_done < xbt_dynar_length(mmalloc_ignore)){
+              if(in_mmalloc_ignore(block_pointed1, -1))
+                res_compare = compare_area(addr_block_pointed1, addr_block_pointed2, heapinfo1[block_pointed1].busy_block.busy_size, previous, 1);
+              else
+                res_compare = compare_area(addr_block_pointed1, addr_block_pointed2, heapinfo1[block_pointed1].busy_block.busy_size, previous, 0);
+            }else{
+              res_compare = compare_area(addr_block_pointed1, addr_block_pointed2, heapinfo1[block_pointed1].busy_block.busy_size, previous, 0);
+            }

             
             if(res_compare)    
               return 1;
             
             if(res_compare)    
               return 1;


@@ -459,8 +514,15 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ
 
           if(add_heap_area_pair(previous, block_pointed1, frag_pointed1, block_pointed2, frag_pointed2)){
 
 
           if(add_heap_area_pair(previous, block_pointed1, frag_pointed1, block_pointed2, frag_pointed2)){
 

-            res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous);
-            
+            if(ignore_done < xbt_dynar_length(mmalloc_ignore)){
+              if(in_mmalloc_ignore(block_pointed1, frag_pointed1))
+                res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 1);
+              else
+                res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 0);
+            }else{
+              res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 0);
+            }
+

             if(res_compare)
               return 1;
            
             if(res_compare)
               return 1;
            


@@ -489,7 +551,14 @@ static int compare_area(void *area1, void* area2, size_t size, xbt_dynar_t previ
 
           if(add_heap_area_pair(previous, block_pointed1, frag_pointed1, block_pointed2, frag_pointed2)){
 
 
           if(add_heap_area_pair(previous, block_pointed1, frag_pointed1, block_pointed2, frag_pointed2)){
 

-            res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous);
+            if(ignore_done < xbt_dynar_length(mmalloc_ignore)){
+              if(in_mmalloc_ignore(block_pointed1, frag_pointed1))
+                res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 1);
+              else
+                res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 0);
+            }else{
+              res_compare = compare_area(addr_frag_pointed1, addr_frag_pointed2, heapinfo1[block_pointed1].busy_frag.frag_size[frag_pointed1], previous, 0);
+            }

             
             if(res_compare)
               return 1;
             
             if(res_compare)
               return 1;