model-checker : move functions about snapshot comparison in a separate file mc_compare.c

[simgrid.git] / src / mc / mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 9f46c20..f6bed22 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -76,6 +76,7 @@ int compare;
 xbt_dynar_t mc_binary_local_variables = NULL;
 
 extern xbt_dynar_t mmalloc_ignore;
+extern xbt_dynar_t stacks_areas;
 
 xbt_automaton_t _mc_property_automaton = NULL;
 
@@ -651,6 +652,7 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
 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;
 }
 
@@ -682,6 +684,16 @@ void MC_ignore(void *address, size_t size){
   MC_UNSET_RAW_MEM;
 }
 
+void MC_new_stack_area(void *stack, char *name){
+  MC_SET_RAW_MEM;
+  stack_region_t region = NULL;
+  region = xbt_new0(s_stack_region_t, 1);
+  region->address = stack;
+  region->process_name = strdup(name);
+  xbt_dynar_push(stacks_areas, &region);
+  MC_UNSET_RAW_MEM;
+}
+
 /************ DWARF ***********/
 
 static e_dw_location_type get_location(char *expr, dw_location_t entry);
@@ -702,6 +714,10 @@ void MC_get_binary_local_variables(){
   char *node_type = NULL, *location_type = NULL, *variable_name = NULL, *lowpc = NULL, *highpc = NULL;
   xbt_dynar_t split = NULL;
 
+  void *low_pc = NULL, *old_low_pc = NULL;
+
+  int compile_unit_found = 0; /* Detect if the program has been compiled with -g */
+
   read = getline(&line, &n, fp);
 
   while (read != -1) {
@@ -714,6 +730,9 @@ void MC_get_binary_local_variables(){
     
     if(line[0] == '<'){
 
+      /* If the program hasn't been compiled with -g, no symbol (line starting with '<' ) found */
+      compile_unit_found = 1;
+
       /* Get node type */
       strtok(line, " ");
       strtok(NULL, " ");
@@ -733,6 +752,8 @@ void MC_get_binary_local_variables(){
           if(node_type != NULL && strcmp(node_type, "DW_AT_name") == 0){
 
             frame_name = strdup(strtok(NULL, " "));
+            xbt_str_trim(frame_name, NULL);
+            xbt_str_trim(frame_name, "\"");
             read = getline(&line, &n, fp);
 
           }else if(node_type != NULL && strcmp(node_type, "DW_AT_frame_base") == 0){
@@ -764,10 +785,18 @@ void MC_get_binary_local_variables(){
              
                   dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
                 
-                  strtok(lowpc, "=");
-                  new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
-                  strtok(highpc, "=");
-                  new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
+                  if(low_pc == NULL){
+                    strtok(lowpc, "=");
+                    new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
+                    strtok(highpc, "=");
+                    new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);             
+                  }else{
+                    strtok(lowpc, "=");
+                    old_low_pc = (void *)strtoul(strtok(NULL, "="), NULL, 16);
+                    new_entry->lowpc = (char *)low_pc + (long)old_low_pc;
+                    strtok(highpc, "=");
+                    new_entry->highpc = (char*)low_pc + ((char *)((void *)strtoul(strtok(NULL, "="), NULL, 16)) - (char*)old_low_pc);
+                  }
 
                   new_entry->location = xbt_new0(s_dw_location_t, 1);
                 
@@ -827,6 +856,8 @@ void MC_get_binary_local_variables(){
           if(node_type != NULL && strcmp(node_type, "DW_AT_name") == 0){
 
             variable_name = strdup(strtok(NULL, " "));
+            xbt_str_trim(variable_name, NULL);
+            xbt_str_trim(variable_name, "\"");
             read = getline(&line, &n, fp);
             
           }else if(node_type != NULL && strcmp(node_type, "DW_AT_location") == 0){
@@ -857,10 +888,18 @@ void MC_get_binary_local_variables(){
 
                   dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
 
-                  strtok(lowpc, "=");
-                  new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
-                  strtok(highpc, "=");
-                  new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
+                  if(low_pc == NULL){
+                    strtok(lowpc, "=");
+                    new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
+                    strtok(highpc, "=");
+                    new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);             
+                  }else{
+                    strtok(lowpc, "=");
+                    old_low_pc = (void *)strtoul(strtok(NULL, "="), NULL, 16);
+                    new_entry->lowpc = (char *)low_pc + (long)old_low_pc;
+                    strtok(highpc, "=");
+                    new_entry->highpc = (char*)low_pc + ((char *)((void *)strtoul(strtok(NULL, "="), NULL, 16)) - (char*)old_low_pc);
+                  }
 
                   new_entry->location = xbt_new0(s_dw_location_t, 1);
                 
@@ -907,6 +946,25 @@ void MC_get_binary_local_variables(){
 
         valid_variable = 1;
 
+      }else if(strcmp(node_type, "DW_TAG_compile_unit") == 0){
+
+        read = getline(&line, &n, fp);
+        
+        while(read != -1 && line[0] != '<'){
+          
+          if(n == 0)
+            continue;
+          
+          node_type = strtok(line, " ");
+          
+          if(node_type != NULL && strcmp(node_type, "DW_AT_low_pc") == 0){
+            low_pc = (void *) strtoul(strtok(NULL, " "), NULL, 16);
+          }
+
+          read = getline(&line, &n, fp);
+
+        }
+
       }else{
 
         read = getline(&line, &n, fp);
@@ -921,6 +979,11 @@ void MC_get_binary_local_variables(){
 
   }
 
+  if(compile_unit_found == 0){
+    XBT_INFO("Your program must be compiled with -g");
+    xbt_abort();
+  }
+
   if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug))
     print_local_variables(mc_binary_local_variables);