model-checker : extend MC_ignore mechanism for global variables in libsimgrid

diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h
index 7a7956f..3d4647f 100644 (file)
--- a/src/include/mc/mc.h
+++ b/src/include/mc/mc.h
@@ -22,7 +22,7 @@ SG_BEGIN_DECL()
 
 extern char*_surf_mc_property_file; /* fixme: better location? */
 
-extern xbt_dynar_t mmalloc_ignore;
+extern xbt_dynar_t mc_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
 
 /********************************* Global *************************************/
@@ -41,7 +41,6 @@ XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
 XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
 void MC_automaton_load(const char *file);
 
-void MC_ignore_init(void);
 XBT_PUBLIC(void) MC_ignore(void *address, size_t size);
 void MC_new_stack_area(void *stack, char *name);
 

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 26b56fb..6f815cc 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -17,6 +17,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkpoint, mc,
 void *start_text_libsimgrid;
 void *start_plt, *end_plt;
 char *libsimgrid_path;
+void *start_data_libsimgrid;
 
 static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size);
 static void MC_region_restore(mc_mem_region_t reg);
@@ -116,6 +117,7 @@ void MC_take_snapshot_liveness(mc_snapshot_t snapshot)
         if (!memcmp(basename(maps->regions[i].pathname), "libsimgrid", 10)){
           MC_snapshot_add_region(snapshot, 1, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
           nb_reg++;
+          start_data_libsimgrid = reg.start_addr;
         } else {
           if (!memcmp(basename(maps->regions[i].pathname), basename(xbt_binary_name), strlen(basename(xbt_binary_name)))){
             MC_snapshot_add_region(snapshot, 2, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 6ae4bb8..36ce557 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -17,6 +17,27 @@ 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, void *heap1, void *heap2, xbt_dynar_t equals);
 static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2);
+static size_t ignore(void *address);
+
+static size_t ignore(void *address){
+  unsigned int cursor = 0;
+  int start = 0;
+  int end = xbt_dynar_length(mc_comparison_ignore) - 1;
+  mc_ignore_region_t region;
+
+  while(start <= end){
+    cursor = (start + end) / 2;
+    region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t);
+    if(region->address == address)
+      return region->size;
+    if(region->address < address)
+      start = cursor + 1;
+    if(region->address > address)
+      end = cursor - 1;   
+  }
+
+  return 0;
+}
 
 static int data_program_region_compare(void *d1, void *d2, size_t size){
   int distance = 0;
@@ -36,12 +57,16 @@ static int data_program_region_compare(void *d1, void *d2, size_t size){
 
 static int data_libsimgrid_region_compare(void *d1, void *d2, size_t size){
   int distance = 0;
-  size_t i = 0;
+  size_t i = 0, ignore_size = 0;
   int pointer_align;
   void *addr_pointed1 = NULL, *addr_pointed2 = NULL;
 
   for(i=0; i<size; i++){
     if(memcmp(((char *)d1) + i, ((char *)d2) + i, 1) != 0){
+      if((ignore_size = ignore((char *)start_data_libsimgrid+i)) > 0){
+        i = i + ignore_size;
+        continue;
+      }
       pointer_align = (i / sizeof(void*)) * sizeof(void*);
       addr_pointed1 = *((void **)((char *)d1 + pointer_align));
       addr_pointed2 = *((void **)((char *)d2 + pointer_align));

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 03d05a0..a090664 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -73,18 +73,21 @@ mc_stats_pair_t mc_stats_pair = NULL;
 xbt_fifo_t mc_stack_liveness = NULL;
 mc_snapshot_t initial_snapshot_liveness = NULL;
 int compare;
-xbt_dynar_t mc_binary_local_variables = NULL;
 
-extern xbt_dynar_t mmalloc_ignore;
+/* Local */
+xbt_dict_t mc_local_variables = NULL;
+
+/* Ignore mechanism */
+extern xbt_dynar_t mc_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
 
 xbt_automaton_t _mc_property_automaton = NULL;
 
-static void MC_assert_pair(int prop);
-static e_dw_location_type get_location(char *expr, dw_location_t entry);
+/* Static functions */
 
-static void MC_get_binary_local_variables(void);
-static void print_local_variables(xbt_dynar_t list);
+static void MC_assert_pair(int prop);
+static dw_location_t get_location(xbt_dict_t location_list, char *expr);
+static dw_frame_t get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset);
 
 void MC_do_the_modelcheck_for_real() {
   if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') {
@@ -651,42 +654,47 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
 
 /************ MC_ignore ***********/ 
 
-void MC_ignore_init(){
-  MC_SET_RAW_MEM;
-  mmalloc_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL);
-  stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
-  MC_UNSET_RAW_MEM;
-}
-
 void MC_ignore(void *address, size_t size){
 
   MC_SET_RAW_MEM;
+  
+  if(mc_comparison_ignore == NULL)
+    mc_comparison_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL);
 
   mc_ignore_region_t region = NULL;
   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;
+  if((address >= std_heap) && (address <= (void*)((char *)std_heap + STD_HEAP_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;
-  xbt_dynar_foreach(mmalloc_ignore, cursor, current_region){
+  xbt_dynar_foreach(mc_comparison_ignore, cursor, current_region){
     if(current_region->address > address)
       break;
   }
 
-  xbt_dynar_insert_at(mmalloc_ignore, cursor, &region);
+  xbt_dynar_insert_at(mc_comparison_ignore, cursor, &region);
 
   MC_UNSET_RAW_MEM;
 }
 
 void MC_new_stack_area(void *stack, char *name){
+
+  if(stacks_areas == NULL)
+    stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
+
   MC_SET_RAW_MEM;
   stack_region_t region = NULL;
   region = xbt_new0(s_stack_region_t, 1);

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index fbca8a5..3172c25 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -191,6 +191,7 @@ memory_map_t get_memory_map(void);
 void free_memory_map(memory_map_t map);
 void get_plt_section(void);
 
+extern void *start_data_libsimgrid;
 
 /********************************** DPOR for safety  **************************************/
 typedef enum {

diff --git a/src/msg/msg_global.c b/src/msg/msg_global.c
index 9daa413..4bd4eb5 100644 (file)
--- a/src/msg/msg_global.c
+++ b/src/msg/msg_global.c
@@ -38,9 +38,6 @@ void MSG_init_nocheck(int *argc, char **argv) {
     s_msg_vm_t vm; // to compute the offset
 
     SIMIX_global_init(argc, argv);
-
-    if(MC_IS_ENABLED && mmalloc_ignore == NULL)
-      MC_ignore_init();
     
     msg_global = xbt_new0(s_MSG_Global_t, 1);
 

diff --git a/src/simix/smx_context_base.c b/src/simix/smx_context_base.c
index c934a08..d7f1a79 100644 (file)
--- a/src/simix/smx_context_base.c
+++ b/src/simix/smx_context_base.c
@@ -48,15 +48,9 @@ smx_ctx_base_factory_create_context_sized(size_t size,
   smx_context_t context = xbt_malloc0(size);
 
   /* Store the address of the stack in heap to compare it apart of heap comparison */
-  if(MC_IS_ENABLED){
-
-    if(mmalloc_ignore == NULL)
-      MC_ignore_init(); 
-    
+  if(MC_IS_ENABLED)   
     MC_ignore(context, size);
 
-  }
-
   /* If the user provided a function for the process then use it.
      Otherwise, it is the context for maestro and we should set it as the
      current context */

diff --git a/src/simix/smx_context_raw.c b/src/simix/smx_context_raw.c
index 2b94104..c78a6f8 100644 (file)
--- a/src/simix/smx_context_raw.c
+++ b/src/simix/smx_context_raw.c
@@ -228,11 +228,6 @@ static void smx_ctx_raw_runall(void);
 void SIMIX_ctx_raw_factory_init(smx_context_factory_t *factory)
 {
 
-  if(MC_IS_ENABLED && mmalloc_ignore == NULL){
-    /* Create list of elements to ignore for heap comparison algorithm */
-    MC_ignore_init();
-  }
-
   XBT_VERB("Using raw contexts. Because the glibc is just not good enough for us.");
   smx_ctx_base_factory_init(factory);
 

diff --git a/src/simix/smx_network.c b/src/simix/smx_network.c
index 8059ee7..9886e65 100644 (file)
--- a/src/simix/smx_network.c
+++ b/src/simix/smx_network.c
@@ -30,6 +30,8 @@ static void SIMIX_rdv_free(void *data);
 void SIMIX_network_init(void)
 {
   rdv_points = xbt_dict_new_homogeneous(SIMIX_rdv_free);
+  if(MC_IS_ENABLED)
+    MC_ignore(&smx_total_comms, sizeof(smx_total_comms));
 }
 
 void SIMIX_network_exit(void)

diff --git a/src/xbt/mmalloc/mm_diff.c b/src/xbt/mmalloc/mm_diff.c
index f32cb5d..bf9fb0d 100644 (file)
--- a/src/xbt/mmalloc/mm_diff.c
+++ b/src/xbt/mmalloc/mm_diff.c
@@ -15,7 +15,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mm_diff, xbt,
 
 extern char *xbt_binary_name;
 
-xbt_dynar_t mmalloc_ignore;
+xbt_dynar_t mc_comparison_ignore;
 xbt_dynar_t stacks_areas;
 
 static void heap_area_pair_free(heap_area_pair_t pair);
@@ -27,7 +27,7 @@ static heap_area_t new_heap_area(int block, int fragment);
 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, xbt_dynar_t *equals);
 
-static int in_mmalloc_ignore(int block, int fragment);
+static int in_mc_comparison_ignore(int block, int fragment);
 static size_t heap_comparison_ignore(void *address);
 static void add_heap_equality(xbt_dynar_t *equals, void *a1, void *a2);
 static void remove_heap_equality(xbt_dynar_t *equals, int address, void *a);
@@ -232,8 +232,8 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac
         
             add_heap_area_pair(previous, current_block, -1, current_block, -1);
         
-            if(ignore_done < xbt_dynar_length(mmalloc_ignore)){
-              if(in_mmalloc_ignore((int)current_block, -1))
+            if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+              if(in_mc_comparison_ignore((int)current_block, -1))
                 res_compare = compare_area(addr_block1, addr_block2, heapinfo1[current_block].busy_block.busy_size, previous, 1);
               else
                 res_compare = compare_area(addr_block1, addr_block2, heapinfo1[current_block].busy_block.busy_size, previous, 0);
@@ -300,8 +300,8 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac
         /* Comparison */
         add_heap_area_pair(previous, i1, -1, i2, -1);
         
-        if(ignore_done < xbt_dynar_length(mmalloc_ignore)){
-          if(in_mmalloc_ignore((int)i1, -1))
+        if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+          if(in_mc_comparison_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);
@@ -357,8 +357,8 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac
                
                 add_heap_area_pair(previous, current_block, current_fragment, current_block, current_fragment);
             
-                if(ignore_done < xbt_dynar_length(mmalloc_ignore)){
-                  if(in_mmalloc_ignore((int)current_block, (int)current_fragment))
+                if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+                  if(in_mc_comparison_ignore((int)current_block, (int)current_fragment))
                     res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[current_block].busy_frag.frag_size[current_fragment], previous, 1);
                   else
                     res_compare = compare_area(addr_frag1, addr_frag2, heapinfo1[current_block].busy_frag.frag_size[current_fragment], previous, 0);
@@ -404,8 +404,8 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t *stac
             /* Comparison */
             add_heap_area_pair(previous, i1, j1, i2, j2);
             
-            if(ignore_done < xbt_dynar_length(mmalloc_ignore)){
-              if(in_mmalloc_ignore((int)i1, (int)j1))
+            if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+              if(in_mc_comparison_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);
@@ -522,16 +522,16 @@ static heap_area_t new_heap_area(int block, int fragment){
   return area;
 }
 
-static int in_mmalloc_ignore(int block, int fragment){
+static int in_mc_comparison_ignore(int block, int fragment){
 
   unsigned int cursor = 0;
   int start = 0;
-  int end = xbt_dynar_length(mmalloc_ignore) - 1;
+  int end = xbt_dynar_length(mc_comparison_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);
+    region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t);
     if(region->block == block){
       if(region->fragment == fragment)
         return 1;
@@ -552,12 +552,12 @@ static int in_mmalloc_ignore(int block, int fragment){
 static size_t heap_comparison_ignore(void *address){
   unsigned int cursor = 0;
   int start = 0;
-  int end = xbt_dynar_length(mmalloc_ignore) - 1;
+  int end = xbt_dynar_length(mc_comparison_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);
+    region = (mc_ignore_region_t)xbt_dynar_get_as(mc_comparison_ignore, cursor, mc_ignore_region_t);
     if(region->address == address)
       return region->size;
     if(region->address < address)
@@ -626,8 +626,8 @@ 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(ignore_done < xbt_dynar_length(mmalloc_ignore)){
-              if(in_mmalloc_ignore(block_pointed1, -1))
+            if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+              if(in_mc_comparison_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);
@@ -654,8 +654,8 @@ 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(ignore_done < xbt_dynar_length(mmalloc_ignore)){
-              if(in_mmalloc_ignore(block_pointed1, frag_pointed1))
+            if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+              if(in_mc_comparison_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);
@@ -688,8 +688,8 @@ 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(ignore_done < xbt_dynar_length(mmalloc_ignore)){
-              if(in_mmalloc_ignore(block_pointed1, frag_pointed1))
+            if(ignore_done < xbt_dynar_length(mc_comparison_ignore)){
+              if(in_mc_comparison_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);