Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : store heap_bytes_used and number of processes directly in mc_visited_...
[simgrid.git] / src / mc / mc_compare.c
index 6e1ea06..7388684 100644 (file)
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2012-2013 Da SimGrid Team. All rights reserved.            */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
@@ -41,7 +41,7 @@ static size_t heap_ignore_size(void *address){
   return 0;
 }
 
-static int compare_global_variables(int region_type, void *d1, void *d2){
+static int compare_global_variables(int region_type, void *d1, void *d2){ /* region_type = 1 -> libsimgrid, region_type = 2 -> binary */
 
   unsigned int cursor = 0;
   size_t offset; 
@@ -50,78 +50,74 @@ static int compare_global_variables(int region_type, void *d1, void *d2){
   int pointer_align; 
   void *addr_pointed1 = NULL, *addr_pointed2 = NULL;
   int res_compare = 0;
+  void *plt_start, *plt_end;
 
-  if(region_type == 1){ /* libsimgrid */
-    xbt_dynar_foreach(mc_global_variables, cursor, current_var){
-      if(current_var->address < start_data_libsimgrid)
+  if(region_type == 2){
+    plt_start = start_plt_binary;
+    plt_end = end_plt_binary;
+  }else{
+    plt_start = start_plt_libsimgrid;
+    plt_end = end_plt_libsimgrid;
+  }
+
+  xbt_dynar_foreach(mc_global_variables, cursor, current_var){
+    if(current_var->address < start_data_libsimgrid){ /* binary global variable */
+      if(region_type == 1)
         continue;
+      offset = (char *)current_var->address - (char *)start_data_binary;
+    }else{ /* libsimgrid global variable */
+      if(region_type == 2)
+        break;
       offset = (char *)current_var->address - (char *)start_data_libsimgrid;
-      i = 0;
-      while(i < current_var->size){
-        if(memcmp((char*)d1 + offset + i, (char*)d2 + offset + i, 1) != 0){
-          pointer_align = (i / sizeof(void*)) * sizeof(void*); 
-          addr_pointed1 = *((void **)((char *)d1 + offset + pointer_align));
-          addr_pointed2 = *((void **)((char *)d2 + offset + pointer_align));
-          if((addr_pointed1 > start_plt_libsimgrid && addr_pointed1 < end_plt_libsimgrid) 
-             || (addr_pointed2 > start_plt_libsimgrid && addr_pointed2 < end_plt_libsimgrid)){
-            i = current_var->size;
-            continue;
-          }else{
-            if((addr_pointed1 > std_heap) && ((char *)addr_pointed1 < (char *)std_heap + STD_HEAP_SIZE) 
-               && (addr_pointed2 > std_heap) && ((char *)addr_pointed2 < (char *)std_heap + STD_HEAP_SIZE)){
-              res_compare = compare_area(addr_pointed1, addr_pointed2, NULL);
-              if(res_compare == 1){
-                #ifdef MC_VERBOSE
-                  XBT_VERB("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
-                #endif
-                return 1;
-              }
-            }else{
+    }
+    i = 0;
+    while(i < current_var->size){
+      if(memcmp((char*)d1 + offset + i, (char*)d2 + offset + i, 1) != 0){
+        pointer_align = (i / sizeof(void*)) * sizeof(void*); 
+        addr_pointed1 = *((void **)((char *)d1 + offset + pointer_align));
+        addr_pointed2 = *((void **)((char *)d2 + offset + pointer_align));
+        if((addr_pointed1 > plt_start && addr_pointed1 < plt_end) || (addr_pointed2 > plt_start && addr_pointed2 < plt_end)){
+          break;
+        }else{
+          if((addr_pointed1 > std_heap) && ((char *)addr_pointed1 < (char *)std_heap + STD_HEAP_SIZE) 
+             && (addr_pointed2 > std_heap) && ((char *)addr_pointed2 < (char *)std_heap + STD_HEAP_SIZE)){
+            res_compare = compare_area(addr_pointed1, addr_pointed2, NULL);
+            if(res_compare == 1){
               #ifdef MC_VERBOSE
+              if(region_type == 2)
+                XBT_VERB("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
+              else
                 XBT_VERB("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
               #endif
+              #ifdef MC_DEBUG
+                if(region_type == 2)
+                  XBT_DEBUG("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
+                else
+                  XBT_DEBUG("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
+              #endif
+                XBT_INFO("Different global variable (%p, %p) : %s at addresses %p - %p (size = %zu)", current_var->address, addr_pointed1, current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
               return 1;
             }
-           
-          }
-        } 
-        i++;
-      }
-    }
-  }else{ /* binary */
-    xbt_dynar_foreach(mc_global_variables, cursor, current_var){
-      if(current_var->address > start_data_libsimgrid)
-        break;
-      offset = (char *)current_var->address - (char *)start_data_binary;
-      i = 0;
-      while(i < current_var->size){
-        if(memcmp((char*)d1 + offset + i, (char*)d2 + offset + i, 1) != 0){
-          pointer_align = (i / sizeof(void*)) * sizeof(void*); 
-          addr_pointed1 = *((void **)((char *)d1 + offset + pointer_align));
-          addr_pointed2 = *((void **)((char *)d2 + offset + pointer_align));
-          if((addr_pointed1 > start_plt_binary && addr_pointed1 < end_plt_binary) || (addr_pointed2 > start_plt_binary && addr_pointed2 < end_plt_binary)){
-            i = current_var->size;
-            continue;
           }else{
-            if((addr_pointed1 > std_heap) && ((char *)addr_pointed1 < (char *)std_heap + STD_HEAP_SIZE) && (addr_pointed2 > std_heap) && ((char *)addr_pointed2 < (char *)std_heap + STD_HEAP_SIZE)){
-              res_compare = compare_area(addr_pointed1, addr_pointed2, NULL);
-              if(res_compare == 1){
-                #ifdef MC_VERBOSE
-                  XBT_VERB("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
-                #endif
-                return 1;
-              }
-            }else{
-              #ifdef MC_VERBOSE
+            #ifdef MC_VERBOSE
+              if(region_type == 2)
                 XBT_VERB("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
-              #endif
-              return 1;
-            }
+              else
+                XBT_VERB("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
+            #endif
+            #ifdef MC_DEBUG
+              if(region_type == 2)
+                XBT_DEBUG("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
+              else
+                XBT_DEBUG("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
+            #endif
+              XBT_INFO("Different global variable (%p, %p) : %s at addresses %p - %p (size = %zu)", current_var->address, addr_pointed1, current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
+            return 1;
           }
-        } 
-        i++;
-      }
-      
+              
+        }
+      } 
+      i++;
     }
   }
 
@@ -196,7 +192,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       #ifdef MC_VERBOSE
         XBT_VERB("Different number of processes : %d - %d", s1->nb_processes, s2->nb_processes);
       #endif
-     
+
       xbt_os_timer_free(timer);
       xbt_os_timer_stop(global_timer);
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
@@ -265,7 +261,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       #ifdef MC_VERBOSE
         XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2);
       #endif
+
       xbt_os_timer_free(timer);
       xbt_os_timer_stop(global_timer);
       mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
@@ -298,7 +294,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         #ifdef MC_VERBOSE
           XBT_VERB("Different hash of global variables : %s - %s", s1->hash_global, s2->hash_global); 
         #endif
-    
+
         xbt_os_timer_free(timer);
         xbt_os_timer_stop(global_timer);
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
@@ -328,7 +324,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
         #ifdef MC_VERBOSE
           XBT_VERB("Different hash of local variables : %s - %s", s1->hash_local, s2->hash_local); 
         #endif
-    
+
         xbt_os_timer_free(timer);
         xbt_os_timer_stop(global_timer);
         mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
@@ -361,7 +357,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       #ifdef MC_VERBOSE
         XBT_VERB("Different global variables in binary"); 
       #endif
-    
+
       reset_heap_information();
       xbt_os_timer_free(timer);
       xbt_os_timer_stop(global_timer);
@@ -604,6 +600,7 @@ static int compare_local_variables(char *s1, char *s2){
             #ifdef MC_DEBUG
               XBT_DEBUG("Different local variable : %s (%s - %s)", var_name, xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *));
             #endif
+
             xbt_dynar_free(&s_tokens1);
             xbt_dynar_free(&s_tokens2);
             xbt_dynar_free(&tokens1);