Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : free memory
[simgrid.git] / src / mc / mc_compare.c
index 07550eb..0e038ca 100644 (file)
@@ -148,7 +148,7 @@ int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall,
 }
 
 int get_heap_region_index(mc_snapshot_t s){
-  int i =0;
+  int i = 0;
   while(i < s->num_reg){
     switch(s->regions[i]->type){
     case 0:
@@ -217,20 +217,20 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     xbt_os_timer_start(timer);
 
   /* Compare number of blocks/fragments used in each heap */
-  size_t chunks_used1 = mmalloc_get_chunks_used((xbt_mheap_t)s1->regions[heap_index]->data);
-  size_t chunks_used2 = mmalloc_get_chunks_used((xbt_mheap_t)s2->regions[heap_index]->data);
-  if(chunks_used1 != chunks_used2){
+
+  if(s1->heap_chunks_used != s2->heap_chunks_used){
+
     if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
       xbt_os_timer_stop(timer);
       if(ct1 != NULL)
         xbt_dynar_push_as(ct1->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
       if(ct2 != NULL)
         xbt_dynar_push_as(ct2->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
-      XBT_DEBUG("Different number of chunks used in each heap : %zu - %zu", chunks_used1, chunks_used2);
+      XBT_DEBUG("Different number of chunks used in each heap : %zu - %zu", s1->heap_chunks_used, s2->heap_chunks_used);
       errors++;
     }else{
       if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
-        XBT_VERB("Different number of chunks used in each heap : %zu - %zu", chunks_used1, chunks_used2);
+        XBT_VERB("Different number of chunks used in each heap : %zu - %zu", s1->heap_chunks_used, s2->heap_chunks_used);
      
       xbt_os_timer_free(timer);
       xbt_os_timer_stop(global_timer);
@@ -246,26 +246,22 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
       return 1;
     }
   }else{
+
     if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
       xbt_os_timer_stop(timer);
   }
   
   if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
     xbt_os_timer_start(timer);
-
+  
   /* Compare size of stacks */
+
   unsigned int cursor = 0;
-  void *addr_stack1, *addr_stack2;
-  void *sp1, *sp2;
   size_t size_used1, size_used2;
   int is_diff = 0;
   while(cursor < xbt_dynar_length(stacks_areas)){
-    addr_stack1 = (char *)s1->regions[heap_index]->data + ((char *)((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->address - (char *)std_heap);
-    addr_stack2 = (char *)s2->regions[heap_index]->data + ((char *)((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->address - (char *)std_heap);
-    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;
-    size_used1 = ((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->size - ((char*)sp1 - (char*)addr_stack1);
-    size_used2 = ((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->size - ((char*)sp2 - (char*)addr_stack2);
+    size_used1 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->size_used;
+    size_used2 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->size_used;
     if(size_used1 != size_used2){
       if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
         if(is_diff == 0){
@@ -306,6 +302,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
   }
 
   /* Compare binary global variables */
+
   is_diff = compare_global_variables(s1->regions[data_program_index]->type, s1->regions[data_program_index]->data, s2->regions[data_program_index]->data);
   if(is_diff != 0){
     if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
@@ -330,6 +327,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     
       if(!raw_mem)
         MC_UNSET_RAW_MEM;
+
       return 1;
     }
   }
@@ -338,9 +336,10 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     if(is_diff == 0)
       xbt_os_timer_stop(timer);
     xbt_os_timer_start(timer);
-  }
+  } 
 
   /* Compare libsimgrid global variables */
+
   is_diff = compare_global_variables(s1->regions[data_libsimgrid_index]->type, s1->regions[data_libsimgrid_index]->data, s2->regions[data_libsimgrid_index]->data);
   if(is_diff != 0){
     if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
@@ -365,6 +364,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     
       if(!raw_mem)
         MC_UNSET_RAW_MEM;
+
       return 1;
     }
   }  
@@ -376,6 +376,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
   }
 
   /* Compare heap */
+
   xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
   xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
   xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), heap_equality_free_voidp);
@@ -411,6 +412,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
 
       if(!raw_mem)
         MC_UNSET_RAW_MEM;
+
       return 1;
     } 
   }else{
@@ -422,9 +424,11 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     xbt_os_timer_start(timer);
 
   /* Stacks comparison */
+
   cursor = 0;
   stack_region_t stack_region1, stack_region2;
   int diff = 0, diff_local = 0;
+  void *sp1, *sp2;
   is_diff = 0;
 
   while(cursor < xbt_dynar_length(stacks1)){
@@ -477,9 +481,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
   xbt_dynar_free(&stacks1);
   xbt_dynar_free(&stacks2);
   xbt_dynar_free(&equals);
-
-  if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))    
-    xbt_os_timer_free(timer);
+   
+  xbt_os_timer_free(timer);
 
   if(!XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
     xbt_os_timer_stop(global_timer);
@@ -539,8 +542,10 @@ static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals){
     s_tokens2 = xbt_str_split(xbt_dynar_get_as(tokens2, cursor, char *), "=");
     if(xbt_dynar_length(s_tokens1) > 1 && xbt_dynar_length(s_tokens2) > 1){
       if((strcmp(xbt_dynar_get_as(s_tokens1, 0, char *), "ip") == 0) && (strcmp(xbt_dynar_get_as(s_tokens2, 0, char *), "ip") == 0)){
-        ip1 = xbt_dynar_get_as(s_tokens1, 1, char *);
-        ip2 = xbt_dynar_get_as(s_tokens2, 1, char *);
+        xbt_free(ip1);
+        xbt_free(ip2);
+        ip1 = strdup(xbt_dynar_get_as(s_tokens1, 1, char *));
+        ip2 = strdup(xbt_dynar_get_as(s_tokens2, 1, char *));
       }
       if(strcmp(xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *)) != 0){   
         /* Ignore this variable ?  */
@@ -559,15 +564,20 @@ static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals){
           xbt_dynar_free(&s_tokens2);
           xbt_dynar_free(&tokens1);
           xbt_dynar_free(&tokens2);
+          xbt_free(ip1);
+          xbt_free(ip2);
           return 1;
         }
       }
     }
     xbt_dynar_free(&s_tokens1);
     xbt_dynar_free(&s_tokens2);
+         
     cursor++;
   }
 
+  xbt_free(ip1);
+  xbt_free(ip2);
   xbt_dynar_free(&tokens1);
   xbt_dynar_free(&tokens2);
   return 0;