src/mc/mc_global.c

   1 /* Copyright (c) 2008-2013. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include <unistd.h>
   8 #include <sys/types.h>
   9 #include <sys/wait.h>
  10 #include <sys/time.h>
  11
  12 #include "simgrid/sg_config.h"
  13 #include "../surf/surf_private.h"
  14 #include "../simix/smx_private.h"
  15 #include "../xbt/mmalloc/mmprivate.h"
  16 #include "xbt/fifo.h"
  17 #include "mc_private.h"
  18 #include "xbt/automaton.h"
  19 #include "xbt/dict.h"
  20
  21 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
  22 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
  23                                 "Logging specific to MC (global)");
  24
  25 /* Configuration support */
  26 e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
  27
  28 int _sg_do_model_check = 0;
  29 int _sg_mc_checkpoint=0;
  30 char* _sg_mc_property_file=NULL;
  31 int _sg_mc_timeout=0;
  32 int _sg_mc_max_depth=1000;
  33 int _sg_mc_visited=0;
  34 char *_sg_mc_dot_output_file = NULL;
  35
  36 int user_max_depth_reached = 0;
  37
  38 void _mc_cfg_cb_reduce(const char *name, int pos) {
  39   if (_sg_cfg_init_status && !_sg_do_model_check) {
  40     xbt_die("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  41   }
  42   char *val= xbt_cfg_get_string(_sg_cfg_set, name);
  43   if (!strcasecmp(val,"none")) {
  44     mc_reduce_kind = e_mc_reduce_none;
  45   } else if (!strcasecmp(val,"dpor")) {
  46     mc_reduce_kind = e_mc_reduce_dpor;
  47   } else {
  48     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
  49   }
  50 }
  51
  52 void _mc_cfg_cb_checkpoint(const char *name, int pos) {
  53   if (_sg_cfg_init_status && !_sg_do_model_check) {
  54     xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  55   }
  56   _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
  57 }
  58 void _mc_cfg_cb_property(const char *name, int pos) {
  59   if (_sg_cfg_init_status && !_sg_do_model_check) {
  60     xbt_die("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  61   }
  62   _sg_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
  63 }
  64
  65 void _mc_cfg_cb_timeout(const char *name, int pos) {
  66   if (_sg_cfg_init_status && !_sg_do_model_check) {
  67     xbt_die("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  68   }
  69   _sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
  70 }
  71
  72 void _mc_cfg_cb_max_depth(const char *name, int pos) {
  73   if (_sg_cfg_init_status && !_sg_do_model_check) {
  74     xbt_die("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  75   }
  76   _sg_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
  77 }
  78
  79 void _mc_cfg_cb_visited(const char *name, int pos) {
  80   if (_sg_cfg_init_status && !_sg_do_model_check) {
  81     xbt_die("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  82   }
  83   _sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
  84 }
  85
  86 void _mc_cfg_cb_dot_output(const char *name, int pos) {
  87   if (_sg_cfg_init_status && !_sg_do_model_check) {
  88     xbt_die("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  89   }
  90   _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
  91 }
  92
  93 /* MC global data structures */
  94 mc_state_t mc_current_state = NULL;
  95 char mc_replay_mode = FALSE;
  96 double *mc_time = NULL;
  97 __thread mc_comparison_times_t mc_comp_times = NULL;
  98 __thread double mc_snapshot_comparison_time;
  99 mc_stats_t mc_stats = NULL;
 100
 101 /* Safety */
 102 xbt_fifo_t mc_stack_safety = NULL;
 103 mc_global_t initial_state_safety = NULL;
 104
 105 /* Liveness */
 106 xbt_fifo_t mc_stack_liveness = NULL;
 107 mc_global_t initial_state_liveness = NULL;
 108 int compare;
 109
 110 xbt_automaton_t _mc_property_automaton = NULL;
 111
 112 /* Variables */
 113 xbt_dict_t mc_local_variables_libsimgrid = NULL;
 114 xbt_dict_t mc_local_variables_binary = NULL;
 115 xbt_dynar_t mc_global_variables_libsimgrid = NULL;
 116 xbt_dynar_t mc_global_variables_binary = NULL;
 117 xbt_dict_t mc_variables_type_libsimgrid = NULL;
 118 xbt_dict_t mc_variables_type_binary = NULL;
 119 mc_object_info_t mc_libsimgrid_info = NULL;
 120 mc_object_info_t mc_binary_info = NULL;
 121
 122 /* Ignore mechanism */
 123 xbt_dynar_t mc_stack_comparison_ignore;
 124 xbt_dynar_t mc_data_bss_comparison_ignore;
 125 extern xbt_dynar_t mc_heap_comparison_ignore;
 126 extern xbt_dynar_t stacks_areas;
 127
 128 /* Dot output */
 129 FILE *dot_output = NULL;
 130 const char* colors[13];
 131
 132
 133 /*******************************  DWARF Information *******************************/
 134 /**********************************************************************************/
 135
 136 /************************** Free functions *************************/
 137
 138 static void dw_location_free(dw_location_t l){
 139   if(l){
 140     if(l->type == e_dw_loclist)
 141       xbt_dynar_free(&(l->location.loclist));
 142     else if(l->type == e_dw_compose)
 143       xbt_dynar_free(&(l->location.compose));
 144     else if(l->type == e_dw_arithmetic)
 145       xbt_free(l->location.arithmetic);
 146
 147     xbt_free(l);
 148   }
 149 }
 150
 151 static void dw_location_entry_free(dw_location_entry_t e){
 152   dw_location_free(e->location);
 153   xbt_free(e);
 154 }
 155
 156 static void dw_type_free(dw_type_t t){
 157   xbt_free(t->name);
 158   xbt_free(t->dw_type_id);
 159   xbt_dynar_free(&(t->members));
 160   xbt_free(t);
 161 }
 162
 163 static void dw_type_free_voidp(void *t){
 164   dw_type_free((dw_type_t) * (void **) t);
 165 }
 166
 167 static void dw_variable_free(dw_variable_t v){
 168   if(v){
 169     xbt_free(v->name);
 170     xbt_free(v->type_origin);
 171     if(!v->global)
 172       dw_location_free(v->address.location);
 173     xbt_free(v);
 174   }
 175 }
 176
 177 static void dw_variable_free_voidp(void *t){
 178   dw_variable_free((dw_variable_t) * (void **) t);
 179 }
 180
 181 // object_info
 182
 183 mc_object_info_t MC_new_object_info() {
 184   mc_object_info_t res = xbt_new(s_mc_object_info_t, 1);
 185   res->local_variables = xbt_dict_new_homogeneous(NULL);
 186   res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
 187   res->types = xbt_dict_new_homogeneous(NULL);
 188   return res;
 189 }
 190
 191 void MC_free_object_info(mc_object_info_t* info) {
 192   xbt_dict_free(&(*info)->local_variables);
 193   xbt_dynar_free(&(*info)->global_variables);
 194   xbt_dict_free(&(*info)->types);
 195   xbt_free(info);
 196   info = NULL;
 197 }
 198
 199 /*************************************************************************/
 200
 201 static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr){
 202
 203   dw_location_t loc = xbt_new0(s_dw_location_t, 1);
 204
 205   if(location_list != NULL){
 206
 207     char *key = bprintf("%d", (int)strtoul(expr, NULL, 16));
 208     loc->type = e_dw_loclist;
 209     loc->location.loclist =  (xbt_dynar_t)xbt_dict_get_or_null(location_list, key);
 210     if(loc->location.loclist == NULL)
 211       XBT_INFO("Key not found in loclist");
 212     xbt_free(key);
 213     return loc;
 214
 215   }else{
 216
 217     int cursor = 0;
 218     char *tok = NULL, *tok2 = NULL;
 219
 220     xbt_dynar_t tokens1 = xbt_str_split(expr, ";");
 221     xbt_dynar_t tokens2;
 222
 223     loc->type = e_dw_compose;
 224     loc->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL);
 225
 226     while(cursor < xbt_dynar_length(tokens1)){
 227
 228       tok = xbt_dynar_get_as(tokens1, cursor, char*);
 229       tokens2 = xbt_str_split(tok, " ");
 230       tok2 = xbt_dynar_get_as(tokens2, 0, char*);
 231
 232       if(strncmp(tok2, "DW_OP_reg", 9) == 0){
 233         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 234         new_element->type = e_dw_register;
 235         new_element->location.reg = atoi(strtok(tok2, "DW_OP_reg"));
 236         xbt_dynar_push(loc->location.compose, &new_element);
 237       }else if(strcmp(tok2, "DW_OP_fbreg:") == 0){
 238         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 239         new_element->type = e_dw_fbregister_op;
 240         new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 241         xbt_dynar_push(loc->location.compose, &new_element);
 242       }else if(strncmp(tok2, "DW_OP_breg", 10) == 0){
 243         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 244         new_element->type = e_dw_bregister_op;
 245         new_element->location.breg_op.reg = atoi(strtok(tok2, "DW_OP_breg"));
 246         new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 247         xbt_dynar_push(loc->location.compose, &new_element);
 248       }else if(strncmp(tok2, "DW_OP_lit", 9) == 0){
 249         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 250         new_element->type = e_dw_lit;
 251         new_element->location.lit = atoi(strtok(tok2, "DW_OP_lit"));
 252         xbt_dynar_push(loc->location.compose, &new_element);
 253       }else if(strcmp(tok2, "DW_OP_piece:") == 0){
 254         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 255         new_element->type = e_dw_piece;
 256         new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 257         xbt_dynar_push(loc->location.compose, &new_element);
 258       }else if(strcmp(tok2, "DW_OP_plus_uconst:") == 0){
 259         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 260         new_element->type = e_dw_plus_uconst;
 261         new_element->location.plus_uconst = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char *));
 262         xbt_dynar_push(loc->location.compose, &new_element);
 263       }else if(strcmp(tok, "DW_OP_abs") == 0 ||
 264                strcmp(tok, "DW_OP_and") == 0 ||
 265                strcmp(tok, "DW_OP_div") == 0 ||
 266                strcmp(tok, "DW_OP_minus") == 0 ||
 267                strcmp(tok, "DW_OP_mod") == 0 ||
 268                strcmp(tok, "DW_OP_mul") == 0 ||
 269                strcmp(tok, "DW_OP_neg") == 0 ||
 270                strcmp(tok, "DW_OP_not") == 0 ||
 271                strcmp(tok, "DW_OP_or") == 0 ||
 272                strcmp(tok, "DW_OP_plus") == 0){
 273         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 274         new_element->type = e_dw_arithmetic;
 275         new_element->location.arithmetic = strdup(strtok(tok2, "DW_OP_"));
 276         xbt_dynar_push(loc->location.compose, &new_element);
 277       }else if(strcmp(tok, "DW_OP_stack_value") == 0){
 278       }else if(strcmp(tok2, "DW_OP_deref_size:") == 0){
 279         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 280         new_element->type = e_dw_deref;
 281         new_element->location.deref_size = (unsigned int short) atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 282         xbt_dynar_push(loc->location.compose, &new_element);
 283       }else if(strcmp(tok, "DW_OP_deref") == 0){
 284         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 285         new_element->type = e_dw_deref;
 286         new_element->location.deref_size = sizeof(void *);
 287         xbt_dynar_push(loc->location.compose, &new_element);
 288       }else if(strcmp(tok2, "DW_OP_constu:") == 0){
 289         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 290         new_element->type = e_dw_uconstant;
 291         new_element->location.uconstant.bytes = 1;
 292         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 293         xbt_dynar_push(loc->location.compose, &new_element);
 294       }else if(strcmp(tok2, "DW_OP_consts:") == 0){
 295         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 296         new_element->type = e_dw_sconstant;
 297         new_element->location.sconstant.bytes = 1;
 298         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 299         xbt_dynar_push(loc->location.compose, &new_element);
 300       }else if(strcmp(tok2, "DW_OP_const1u:") == 0 ||
 301                strcmp(tok2, "DW_OP_const2u:") == 0 ||
 302                strcmp(tok2, "DW_OP_const4u:") == 0 ||
 303                strcmp(tok2, "DW_OP_const8u:") == 0){
 304         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 305         new_element->type = e_dw_uconstant;
 306         new_element->location.uconstant.bytes = tok2[11] - '0';
 307         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 308         xbt_dynar_push(loc->location.compose, &new_element);
 309       }else if(strcmp(tok, "DW_OP_const1s") == 0 ||
 310                strcmp(tok, "DW_OP_const2s") == 0 ||
 311                strcmp(tok, "DW_OP_const4s") == 0 ||
 312                strcmp(tok, "DW_OP_const8s") == 0){
 313         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 314         new_element->type = e_dw_sconstant;
 315         new_element->location.sconstant.bytes = tok2[11] - '0';
 316         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 317         xbt_dynar_push(loc->location.compose, &new_element);
 318       }else{
 319         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 320         new_element->type = e_dw_unsupported;
 321         xbt_dynar_push(loc->location.compose, &new_element);
 322       }
 323
 324       cursor++;
 325       xbt_dynar_free(&tokens2);
 326
 327     }
 328
 329     xbt_dynar_free(&tokens1);
 330
 331     return loc;
 332
 333   }
 334
 335 }
 336
 337 /** @brief Extract the location lists from an ELF file (.debug_loc)
 338  *
 339  *  @return A map from the offset in the list (in hexadecimal string)
 340  *          into a location list (dynar of dw_location_entry_t).
 341  */
 342 static xbt_dict_t MC_dwarf_get_location_list(const char *elf_file){
 343
 344   char *command = bprintf("LANG=C objdump -Wo %s", elf_file);
 345
 346   FILE *fp = popen(command, "r");
 347
 348   if(fp == NULL){
 349     perror("popen for objdump failed");
 350     xbt_abort();
 351   }
 352
 353   int debug = 0; /*Detect if the program has been compiled with -g */
 354
 355   xbt_dict_t location_list = xbt_dict_new_homogeneous(NULL);
 356   char *line = NULL, *loc_expr = NULL;
 357   ssize_t read;
 358   size_t n = 0;
 359   int cursor_remove;
 360   xbt_dynar_t split = NULL;
 361
 362   while ((read = xbt_getline(&line, &n, fp)) != -1) {
 363
 364     /* Wipeout the new line character */
 365     line[read - 1] = '\0';
 366
 367     xbt_str_trim(line, NULL);
 368
 369     if(n == 0)
 370       continue;
 371
 372     if(strlen(line) == 0)
 373       continue;
 374
 375     if(debug == 0){
 376
 377       if(strncmp(line, elf_file, strlen(elf_file)) == 0)
 378         continue;
 379
 380       if(strncmp(line, "Contents", 8) == 0)
 381         continue;
 382
 383       if(strncmp(line, "Offset", 6) == 0){
 384         debug = 1;
 385         continue;
 386       }
 387     }
 388
 389     if(debug == 0){
 390       XBT_INFO("Your program must be compiled with -g");
 391       xbt_abort();
 392     }
 393
 394     xbt_dynar_t loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL);
 395
 396     xbt_str_strip_spaces(line);
 397     split = xbt_str_split(line, " ");
 398
 399     char *key = NULL;
 400     while(read != -1 && strcmp("<End", (char *)xbt_dynar_get_as(split, 1, char *)) != 0){
 401
 402       // Take the key from the first line of the list:
 403       if(key==NULL){
 404         key = bprintf("%d", (int)strtoul((char *)xbt_dynar_get_as(split, 0, char *), NULL, 16));
 405       }
 406
 407       dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
 408       new_entry->lowpc = strtoul((char *)xbt_dynar_get_as(split, 1, char *), NULL, 16);
 409       new_entry->highpc = strtoul((char *)xbt_dynar_get_as(split, 2, char *), NULL, 16);
 410
 411       cursor_remove =0;
 412       while(cursor_remove < 3){
 413         xbt_dynar_remove_at(split, 0, NULL);
 414         cursor_remove++;
 415       }
 416
 417       loc_expr = xbt_str_join(split, " ");
 418       xbt_str_ltrim(loc_expr, "(");
 419       xbt_str_rtrim(loc_expr, ")");
 420       new_entry->location = MC_dwarf_get_location(NULL, loc_expr);
 421
 422       xbt_dynar_push(loclist, &new_entry);
 423
 424       xbt_dynar_free(&split);
 425       free(loc_expr);
 426
 427       read = xbt_getline(&line, &n, fp);
 428       if(read != -1){
 429         line[read - 1] = '\0';
 430         xbt_str_strip_spaces(line);
 431         split = xbt_str_split(line, " ");
 432       }
 433
 434     }
 435
 436
 437     xbt_dict_set(location_list, key, loclist, NULL);
 438     xbt_free(key);
 439
 440     xbt_dynar_free(&split);
 441
 442   }
 443
 444   xbt_free(line);
 445   xbt_free(command);
 446   pclose(fp);
 447
 448   return location_list;
 449 }
 450
 451 static dw_frame_t MC_dwarf_get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset){
 452
 453   xbt_dict_cursor_t cursor = NULL;
 454   char *name;
 455   dw_frame_t res;
 456
 457   xbt_dict_foreach(all_variables, cursor, name, res) {
 458     if(offset >= res->start && offset < res->end){
 459       xbt_dict_cursor_free(&cursor);
 460       return res;
 461     }
 462   }
 463
 464   xbt_dict_cursor_free(&cursor);
 465   return NULL;
 466
 467 }
 468
 469 static dw_variable_t MC_dwarf_get_variable_by_name(dw_frame_t frame, char *var){
 470
 471   unsigned int cursor = 0;
 472   dw_variable_t current_var;
 473
 474   xbt_dynar_foreach(frame->variables, cursor, current_var){
 475     if(strcmp(var, current_var->name) == 0)
 476       return current_var;
 477   }
 478
 479   return NULL;
 480 }
 481
 482 static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *address){
 483
 484   if(xbt_dynar_is_empty(variables))
 485     return 0;
 486
 487   unsigned int cursor = 0;
 488   int start = 0;
 489   int end = xbt_dynar_length(variables) - 1;
 490   dw_variable_t var_test = NULL;
 491
 492   while(start <= end){
 493     cursor = (start + end) / 2;
 494     var_test = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t);
 495     if(strcmp(var_test->name, var) < 0){
 496       start = cursor + 1;
 497     }else if(strcmp(var_test->name, var) > 0){
 498       end = cursor - 1;
 499     }else{
 500       if(address){ /* global variable */
 501         if(var_test->address.address == address)
 502           return -1;
 503         if(var_test->address.address > address)
 504           end = cursor - 1;
 505         else
 506           start = cursor + 1;
 507       }else{ /* local variable */
 508         return -1;
 509       }
 510     }
 511   }
 512
 513   if(strcmp(var_test->name, var) == 0){
 514     if(address && var_test->address.address < address)
 515       return cursor+1;
 516     else
 517       return cursor;
 518   }else if(strcmp(var_test->name, var) < 0)
 519     return cursor+1;
 520   else
 521     return cursor;
 522
 523 }
 524
 525 static mc_object_info_t MC_dwarf_get_variables(const char *elf_file){
 526
 527   xbt_dict_t location_list = MC_dwarf_get_location_list(elf_file);
 528
 529   char *command = bprintf("LANG=C objdump -Wi %s", elf_file);
 530
 531   FILE *fp = popen(command, "r");
 532
 533   if(fp == NULL)
 534     perror("popen for objdump failed");
 535
 536   mc_object_info_t result = MC_new_object_info();
 537   xbt_dict_t *local_variables = &result->local_variables;
 538   xbt_dynar_t *global_variables = &result->global_variables;
 539   xbt_dict_t *types = &result->types;
 540
 541   char *line = NULL, *origin, *abstract_origin, *current_frame = NULL,
 542     *subprogram_name = NULL, *subprogram_start = NULL, *subprogram_end = NULL,
 543     *node_type = NULL, *location_type = NULL, *variable_name = NULL,
 544     *loc_expr = NULL, *name = NULL, *end =NULL, *type_origin = NULL, *global_address = NULL,
 545     *parent_value = NULL;
 546
 547   ssize_t read =0;
 548   size_t n = 0;
 549   int global_variable = 0, parent = 0, new_frame = 0, new_variable = 1, size = 0,
 550     is_pointer = 0, struct_decl = 0, member_end = 0,
 551     enumeration_size = 0, subrange = 0, union_decl = 0, offset = 0, index = 0;
 552
 553   xbt_dynar_t split = NULL, split2 = NULL;
 554
 555   xbt_dict_t variables_origin = xbt_dict_new_homogeneous(xbt_free);
 556   xbt_dict_t subprograms_origin = xbt_dict_new_homogeneous(xbt_free);
 557
 558   dw_frame_t variable_frame, subroutine_frame = NULL;
 559
 560   e_dw_type_type type_type = -1;
 561
 562   read = xbt_getline(&line, &n, fp);
 563
 564   while (read != -1) {
 565
 566     /* Wipeout the new line character */
 567     line[read - 1] = '\0';
 568
 569     if(n == 0 || strlen(line) == 0){
 570       read = xbt_getline(&line, &n, fp);
 571       continue;
 572     }
 573
 574     xbt_str_ltrim(line, NULL);
 575     xbt_str_strip_spaces(line);
 576
 577     if(line[0] != '<'){
 578       read = xbt_getline(&line, &n, fp);
 579       continue;
 580     }
 581
 582     xbt_dynar_free(&split);
 583     split = xbt_str_split(line, " ");
 584
 585     /* Get node type */
 586     node_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
 587
 588     if(strcmp(node_type, "(DW_TAG_subprogram)") == 0){ /* New frame */
 589       /* We build/complete a dw_frame_t object
 590        * and append it if necessary to the local_variables dictionnary */
 591
 592       dw_frame_t frame = NULL;
 593
 594       strtok(xbt_dynar_get_as(split, 0, char *), "<");
 595       subprogram_start = xbt_strdup(strtok(NULL, "<"));
 596       xbt_str_rtrim(subprogram_start, ">:");
 597
 598       read = xbt_getline(&line, &n, fp);
 599
 600       while(read != -1){
 601
 602         /* Wipeout the new line character */
 603         line[read - 1] = '\0';
 604
 605         if(n == 0 || strlen(line) == 0){
 606           read = xbt_getline(&line, &n, fp);
 607           continue;
 608         }
 609
 610         xbt_dynar_free(&split);
 611         xbt_str_rtrim(line, NULL);
 612         xbt_str_strip_spaces(line);
 613         split = xbt_str_split(line, " ");
 614
 615         node_type = xbt_dynar_get_as(split, 1, char *);
 616
 617         if(strncmp(node_type, "DW_AT_", 6) != 0)
 618           break;
 619
 620         if(strcmp(node_type, "DW_AT_sibling") == 0){
 621
 622           subprogram_end = xbt_strdup(xbt_dynar_get_as(split, 3, char*));
 623           xbt_str_ltrim(subprogram_end, "<0x");
 624           xbt_str_rtrim(subprogram_end, ">");
 625
 626         }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){ /* Frame already in dict */
 627
 628           new_frame = 0;
 629           abstract_origin = xbt_strdup(xbt_dynar_get_as(split, 2, char*));
 630           xbt_str_ltrim(abstract_origin, "<0x");
 631           xbt_str_rtrim(abstract_origin, ">");
 632           subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, abstract_origin);
 633           frame = xbt_dict_get_or_null(*local_variables, subprogram_name);
 634           xbt_free(abstract_origin);
 635
 636         }else if(strcmp(node_type, "DW_AT_name") == 0){
 637
 638           new_frame = 1;
 639           xbt_free(current_frame);
 640           frame = xbt_new0(s_dw_frame_t, 1);
 641           frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 642           frame->variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
 643           frame->frame_base = xbt_new0(s_dw_location_t, 1);
 644           current_frame = strdup(frame->name);
 645
 646           xbt_dict_set(subprograms_origin, subprogram_start, xbt_strdup(frame->name), NULL);
 647
 648         }else if(strcmp(node_type, "DW_AT_frame_base") == 0){
 649
 650           location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
 651
 652           if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
 653
 654             frame->frame_base = MC_dwarf_get_location(location_list, xbt_dynar_get_as(split, 3, char *));
 655
 656           }else{
 657
 658             xbt_str_strip_spaces(line);
 659             split2 = xbt_str_split(line, "(");
 660             xbt_dynar_remove_at(split2, 0, NULL);
 661             loc_expr = xbt_str_join(split2, " ");
 662             xbt_str_rtrim(loc_expr, ")");
 663             frame->frame_base = MC_dwarf_get_location(NULL, loc_expr);
 664             xbt_dynar_free(&split2);
 665             xbt_free(loc_expr);
 666
 667           }
 668
 669         }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
 670
 671           if(frame != NULL)
 672             frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 673
 674         }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
 675
 676           if(frame != NULL)
 677             frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 678
 679         }else if(strcmp(node_type, "DW_AT_MIPS_linkage_name:") == 0){
 680
 681           xbt_free(frame->name);
 682           xbt_free(current_frame);
 683           frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 684           current_frame = strdup(frame->name);
 685           xbt_dict_set(subprograms_origin, subprogram_start, xbt_strdup(frame->name), NULL);
 686
 687         }
 688
 689         read = xbt_getline(&line, &n, fp);
 690
 691       }
 692
 693       if(new_frame == 1){
 694         frame->start = strtoul(subprogram_start, NULL, 16);
 695         if(subprogram_end != NULL)
 696           frame->end = strtoul(subprogram_end, NULL, 16);
 697         xbt_dict_set(*local_variables, frame->name, frame, NULL);
 698       }
 699
 700       xbt_free(subprogram_start);
 701       xbt_free(subprogram_end);
 702       subprogram_end = NULL;
 703
 704
 705     }else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
 706       /* We build a dw_variable_t object and append it either to
 707          the list of variables of the frame (local variable)
 708          or to the list of global variables (global variables). */
 709
 710       dw_variable_t var = NULL;
 711
 712       parent_value = strdup(xbt_dynar_get_as(split, 0, char *));
 713       parent_value = strtok(parent_value,"<");
 714       xbt_str_rtrim(parent_value, ">");
 715       parent = atoi(parent_value);
 716       xbt_free(parent_value);
 717
 718       if(parent == 1)
 719         global_variable = 1;
 720
 721       strtok(xbt_dynar_get_as(split, 0, char *), "<");
 722       origin = xbt_strdup(strtok(NULL, "<"));
 723       xbt_str_rtrim(origin, ">:");
 724
 725       read = xbt_getline(&line, &n, fp);
 726
 727       while(read != -1){
 728
 729         /* Wipeout the new line character */
 730         line[read - 1] = '\0';
 731
 732         if(n == 0 || strlen(line) == 0){
 733           read = xbt_getline(&line, &n, fp);
 734           continue;
 735         }
 736
 737         xbt_dynar_free(&split);
 738         xbt_str_rtrim(line, NULL);
 739         xbt_str_strip_spaces(line);
 740         split = xbt_str_split(line, " ");
 741
 742         node_type = xbt_dynar_get_as(split, 1, char *);
 743
 744         if(strncmp(node_type, "DW_AT_", 6) != 0)
 745           break;
 746
 747         if(strcmp(node_type, "DW_AT_name") == 0){
 748
 749           var = xbt_new0(s_dw_variable_t, 1);
 750           var->name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 751           xbt_dict_set(variables_origin, origin, xbt_strdup(var->name), NULL);
 752
 753         }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
 754
 755           new_variable = 0;
 756
 757           abstract_origin = xbt_dynar_get_as(split, 2, char *);
 758           xbt_str_ltrim(abstract_origin, "<0x");
 759           xbt_str_rtrim(abstract_origin, ">");
 760
 761           variable_name = (char *)xbt_dict_get_or_null(variables_origin, abstract_origin);
 762           variable_frame = MC_dwarf_get_frame_by_offset(*local_variables, strtoul(abstract_origin, NULL, 16));
 763           var = MC_dwarf_get_variable_by_name(variable_frame, variable_name);
 764
 765         }else if(strcmp(node_type, "DW_AT_location") == 0){
 766
 767           if(var != NULL){
 768
 769             if(!global_variable){
 770
 771               location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
 772
 773               if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
 774                 var->address.location = MC_dwarf_get_location(location_list, xbt_dynar_get_as(split, 3, char *));
 775               }else{
 776                 xbt_str_strip_spaces(line);
 777                 split2 = xbt_str_split(line, "(");
 778                 xbt_dynar_remove_at(split2, 0, NULL);
 779                 loc_expr = xbt_str_join(split2, " ");
 780                 xbt_str_rtrim(loc_expr, ")");
 781                 if(strncmp("DW_OP_addr", loc_expr, 10) == 0){
 782                   global_variable = 1;
 783                   xbt_dynar_free(&split2);
 784                   split2 = xbt_str_split(loc_expr, " ");
 785                   if(strcmp(elf_file, xbt_binary_name) != 0)
 786                     var->address.address = (char *)start_text_libsimgrid + (long)((void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16));
 787                   else
 788                     var->address.address = (void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16);
 789                 }else{
 790                   var->address.location = MC_dwarf_get_location(NULL, loc_expr);
 791                 }
 792                 xbt_dynar_free(&split2);
 793                 xbt_free(loc_expr);
 794               }
 795             }else{
 796               global_address = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 797               xbt_str_rtrim(global_address, ")");
 798               if(strcmp(elf_file, xbt_binary_name) != 0)
 799                 var->address.address = (char *)start_text_libsimgrid + (long)((void *)strtoul(global_address, NULL, 16));
 800               else
 801                 var->address.address = (void *)strtoul(global_address, NULL, 16);
 802               xbt_free(global_address);
 803               global_address = NULL;
 804             }
 805
 806           }
 807
 808         }else if(strcmp(node_type, "DW_AT_type") == 0){
 809
 810           type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
 811           xbt_str_ltrim(type_origin, "<0x");
 812           xbt_str_rtrim(type_origin, ">");
 813
 814         }else if(strcmp(node_type, "DW_AT_declaration") == 0){
 815
 816           new_variable = 0;
 817           if(new_variable){
 818             dw_variable_free(var);
 819             var = NULL;
 820           }
 821
 822         }else if(strcmp(node_type, "DW_AT_artificial") == 0){
 823
 824           new_variable = 0;
 825           if(new_variable){
 826             dw_variable_free(var);
 827             var = NULL;
 828           }
 829
 830         }
 831
 832         read = xbt_getline(&line, &n, fp);
 833
 834       }
 835
 836       if(new_variable == 1){
 837
 838         if(!global_variable){
 839           variable_frame = xbt_dict_get_or_null(*local_variables, current_frame);
 840           var->type_origin = strdup(type_origin);
 841           var->global = 0;
 842           index = MC_dwarf_get_variable_index(variable_frame->variables, var->name, NULL);
 843           if(index != -1)
 844             xbt_dynar_insert_at(variable_frame->variables, index, &var);
 845         }else{
 846           var->type_origin = strdup(type_origin);
 847           var->global = 1;
 848           index = MC_dwarf_get_variable_index(*global_variables, var->name, var->address.address);
 849           if(index != -1)
 850             xbt_dynar_insert_at(*global_variables, index, &var);
 851         }
 852
 853          xbt_free(type_origin);
 854          type_origin = NULL;
 855       }
 856
 857       global_variable = 0;
 858       new_variable = 1;
 859
 860     }else if(strcmp(node_type, "(DW_TAG_inlined_subroutine)") == 0){
 861       /* Update the information on the frame (we should duplicate it instead). */
 862
 863       read = xbt_getline(&line, &n, fp);
 864
 865       while(read != -1){
 866
 867         /* Wipeout the new line character */
 868         line[read - 1] = '\0';
 869
 870         if(n == 0 || strlen(line) == 0){
 871           read = xbt_getline(&line, &n, fp);
 872           continue;
 873         }
 874
 875         xbt_dynar_free(&split);
 876         xbt_str_rtrim(line, NULL);
 877         xbt_str_strip_spaces(line);
 878         split = xbt_str_split(line, " ");
 879
 880         if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
 881           break;
 882
 883         node_type = xbt_dynar_get_as(split, 1, char *);
 884
 885         if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
 886
 887           origin = xbt_dynar_get_as(split, 2, char *);
 888           xbt_str_ltrim(origin, "<0x");
 889           xbt_str_rtrim(origin, ">");
 890
 891           subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, origin);
 892           subroutine_frame = xbt_dict_get_or_null(*local_variables, subprogram_name);
 893
 894         }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
 895
 896           subroutine_frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 897
 898         }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
 899
 900           subroutine_frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 901         }
 902
 903         read = xbt_getline(&line, &n, fp);
 904
 905       }
 906
 907     }else if(strcmp(node_type, "(DW_TAG_base_type)") == 0
 908              || strcmp(node_type, "(DW_TAG_enumeration_type)") == 0
 909              || strcmp(node_type, "(DW_TAG_enumerator)") == 0
 910              || strcmp(node_type, "(DW_TAG_typedef)") == 0
 911              || strcmp(node_type, "(DW_TAG_const_type)") == 0
 912              || strcmp(node_type, "(DW_TAG_subroutine_type)") == 0
 913              || strcmp(node_type, "(DW_TAG_volatile_type)") == 0
 914              || (is_pointer = !strcmp(node_type, "(DW_TAG_pointer_type)"))){
 915
 916       /* Create the and add it to the types dictionnary */
 917
 918       if(strcmp(node_type, "(DW_TAG_base_type)") == 0)
 919         type_type = e_dw_base_type;
 920       else if(strcmp(node_type, "(DW_TAG_enumeration_type)") == 0)
 921         type_type = e_dw_enumeration_type;
 922       else if(strcmp(node_type, "(DW_TAG_enumerator)") == 0)
 923         type_type = e_dw_enumerator;
 924       else if(strcmp(node_type, "(DW_TAG_typedef)") == 0)
 925         type_type = e_dw_typedef;
 926       else if(strcmp(node_type, "(DW_TAG_const_type)") == 0)
 927         type_type = e_dw_const_type;
 928       else if(strcmp(node_type, "(DW_TAG_pointer_type)") == 0)
 929         type_type = e_dw_pointer_type;
 930       else if(strcmp(node_type, "(DW_TAG_subroutine_type)") == 0)
 931         type_type = e_dw_subroutine_type;
 932       else if(strcmp(node_type, "(DW_TAG_volatile_type)") == 0)
 933         type_type = e_dw_volatile_type;
 934
 935       strtok(xbt_dynar_get_as(split, 0, char *), "<");
 936       origin = strdup(strtok(NULL, "<"));
 937       xbt_str_rtrim(origin, ">:");
 938
 939       read = xbt_getline(&line, &n, fp);
 940
 941       while(read != -1){
 942
 943          /* Wipeout the new line character */
 944         line[read - 1] = '\0';
 945
 946         if(n == 0 || strlen(line) == 0){
 947           read = xbt_getline(&line, &n, fp);
 948           continue;
 949         }
 950
 951         xbt_dynar_free(&split);
 952         xbt_str_rtrim(line, NULL);
 953         xbt_str_strip_spaces(line);
 954         split = xbt_str_split(line, " ");
 955
 956         if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
 957           break;
 958
 959         node_type = xbt_dynar_get_as(split, 1, char *);
 960
 961         if(strcmp(node_type, "DW_AT_byte_size") == 0){
 962           size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
 963           if(type_type == e_dw_enumeration_type)
 964             enumeration_size = size;
 965         }else if(strcmp(node_type, "DW_AT_name") == 0){
 966           end = xbt_str_join(split, " ");
 967           xbt_dynar_free(&split);
 968           split = xbt_str_split(end, "):");
 969           xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
 970           name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
 971         }else if(strcmp(node_type, "DW_AT_type") == 0){
 972           type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
 973           xbt_str_ltrim(type_origin, "<0x");
 974           xbt_str_rtrim(type_origin, ">");
 975         }
 976
 977         read = xbt_getline(&line, &n, fp);
 978       }
 979
 980       dw_type_t type = xbt_new0(s_dw_type_t, 1);
 981       type->type = type_type;
 982       if(name)
 983         type->name = xbt_strdup(name);
 984       else
 985         type->name = xbt_strdup("undefined");
 986       type->is_pointer_type = is_pointer;
 987       type->id = (void *)strtoul(origin, NULL, 16);
 988       if(type_origin)
 989         type->dw_type_id = xbt_strdup(type_origin);
 990       if(type_type == e_dw_enumerator)
 991         type->size = enumeration_size;
 992       else
 993         type->size = size;
 994       type->members = NULL;
 995
 996       xbt_dict_set(*types, origin, type, NULL);
 997
 998       xbt_free(name);
 999       name = NULL;
1000       xbt_free(type_origin);
1001       type_origin = NULL;
1002       xbt_free(end);
1003       end = NULL;
1004
1005       is_pointer = 0;
1006       size = 0;
1007       xbt_free(origin);
1008
1009     }else if(strcmp(node_type, "(DW_TAG_structure_type)") == 0 || strcmp(node_type, "(DW_TAG_union_type)") == 0){
1010
1011       if(strcmp(node_type, "(DW_TAG_structure_type)") == 0)
1012         struct_decl = 1;
1013       else
1014         union_decl = 1;
1015
1016       strtok(xbt_dynar_get_as(split, 0, char *), "<");
1017       origin = strdup(strtok(NULL, "<"));
1018       xbt_str_rtrim(origin, ">:");
1019
1020       read = xbt_getline(&line, &n, fp);
1021
1022       dw_type_t type = NULL;
1023
1024       while(read != -1){
1025
1026         while(read != -1){
1027
1028           /* Wipeout the new line character */
1029           line[read - 1] = '\0';
1030
1031           if(n == 0 || strlen(line) == 0){
1032             read = xbt_getline(&line, &n, fp);
1033             continue;
1034           }
1035
1036           xbt_dynar_free(&split);
1037           xbt_str_rtrim(line, NULL);
1038           xbt_str_strip_spaces(line);
1039           split = xbt_str_split(line, " ");
1040
1041           node_type = xbt_dynar_get_as(split, 1, char *);
1042
1043           if(strncmp(node_type, "DW_AT_", 6) != 0){
1044             member_end = 1;
1045             break;
1046           }
1047
1048           if(strcmp(node_type, "DW_AT_byte_size") == 0){
1049             size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1050           }else if(strcmp(node_type, "DW_AT_name") == 0){
1051             xbt_free(end);
1052             end = xbt_str_join(split, " ");
1053             xbt_dynar_free(&split);
1054             split = xbt_str_split(end, "):");
1055             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
1056             name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
1057           }else if(strcmp(node_type, "DW_AT_type") == 0){
1058             type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
1059             xbt_str_ltrim(type_origin, "<0x");
1060             xbt_str_rtrim(type_origin, ">");
1061           }else if(strcmp(node_type, "DW_AT_data_member_location:") == 0){
1062             xbt_free(end);
1063             end = xbt_str_join(split, " ");
1064             xbt_dynar_free(&split);
1065             split = xbt_str_split(end, "DW_OP_plus_uconst:");
1066             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), NULL);
1067             xbt_str_rtrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), ")");
1068             offset = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1069           }
1070
1071           read = xbt_getline(&line, &n, fp);
1072
1073         }
1074
1075         if(member_end && type){
1076           member_end = 0;
1077
1078           dw_type_t member_type = xbt_new0(s_dw_type_t, 1);
1079           member_type->name = xbt_strdup(name);
1080           member_type->size = size;
1081           member_type->is_pointer_type = is_pointer;
1082           member_type->id = (void *)strtoul(origin, NULL, 16);
1083           member_type->offset = offset;
1084           if(type_origin)
1085             member_type->dw_type_id = xbt_strdup(type_origin);
1086
1087           xbt_dynar_push(type->members, &member_type);
1088
1089           xbt_free(name);
1090           name = NULL;
1091           xbt_free(end);
1092           end = NULL;
1093           xbt_free(type_origin);
1094           type_origin = NULL;
1095           size = 0;
1096           offset = 0;
1097
1098           xbt_free(origin);
1099           origin = NULL;
1100           strtok(xbt_dynar_get_as(split, 0, char *), "<");
1101           origin = strdup(strtok(NULL, "<"));
1102           xbt_str_rtrim(origin, ">:");
1103
1104         }
1105
1106         if(struct_decl || union_decl){
1107           type = xbt_new0(s_dw_type_t, 1);
1108           if(struct_decl)
1109             type->type = e_dw_structure_type;
1110           else
1111             type->type = e_dw_union_type;
1112           type->name = xbt_strdup(name);
1113           type->size = size;
1114           type->is_pointer_type = is_pointer;
1115           type->id = (void *)strtoul(origin, NULL, 16);
1116           if(type_origin)
1117             type->dw_type_id = xbt_strdup(type_origin);
1118           type->members = xbt_dynar_new(sizeof(dw_type_t), dw_type_free_voidp);
1119
1120           xbt_dict_set(*types, origin, type, NULL);
1121
1122           xbt_free(name);
1123           name = NULL;
1124           xbt_free(end);
1125           end = NULL;
1126           xbt_free(type_origin);
1127           type_origin = NULL;
1128           size = 0;
1129           struct_decl = 0;
1130           union_decl = 0;
1131
1132         }
1133
1134         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_member)") != 0)
1135           break;
1136
1137         read = xbt_getline(&line, &n, fp);
1138
1139       }
1140
1141       xbt_free(origin);
1142       origin = NULL;
1143
1144     }else if(strcmp(node_type, "(DW_TAG_array_type)") == 0){
1145
1146       strtok(xbt_dynar_get_as(split, 0, char *), "<");
1147       origin = strdup(strtok(NULL, "<"));
1148       xbt_str_rtrim(origin, ">:");
1149
1150       read = xbt_getline(&line, &n, fp);
1151
1152       dw_type_t type = NULL;
1153
1154       while(read != -1){
1155
1156         while(read != -1){
1157
1158           /* Wipeout the new line character */
1159           line[read - 1] = '\0';
1160
1161           if(n == 0 || strlen(line) == 0){
1162             read = xbt_getline(&line, &n, fp);
1163             continue;
1164           }
1165
1166           xbt_dynar_free(&split);
1167           xbt_str_rtrim(line, NULL);
1168           xbt_str_strip_spaces(line);
1169           split = xbt_str_split(line, " ");
1170
1171           node_type = xbt_dynar_get_as(split, 1, char *);
1172
1173           if(strncmp(node_type, "DW_AT_", 6) != 0)
1174             break;
1175
1176           if(strcmp(node_type, "DW_AT_upper_bound") == 0){
1177             size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1178           }else if(strcmp(node_type, "DW_AT_name") == 0){
1179             end = xbt_str_join(split, " ");
1180             xbt_dynar_free(&split);
1181             split = xbt_str_split(end, "):");
1182             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
1183             name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
1184           }else if(strcmp(node_type, "DW_AT_type") == 0){
1185             type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
1186             xbt_str_ltrim(type_origin, "<0x");
1187             xbt_str_rtrim(type_origin, ">");
1188           }
1189
1190           read = xbt_getline(&line, &n, fp);
1191
1192         }
1193
1194         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_subrange_type)") == 0){
1195           subrange = 1;
1196         }
1197
1198         if(subrange && type){
1199           type->size = size;
1200
1201           xbt_free(name);
1202           name = NULL;
1203           xbt_free(end);
1204           end = NULL;
1205           xbt_free(type_origin);
1206           type_origin = NULL;
1207           size = 0;
1208
1209           xbt_free(origin);
1210           origin = NULL;
1211           strtok(xbt_dynar_get_as(split, 0, char *), "<");
1212           origin = strdup(strtok(NULL, "<"));
1213           xbt_str_rtrim(origin, ">:");
1214
1215         }else {
1216
1217           type = xbt_new0(s_dw_type_t, 1);
1218           type->type = e_dw_array_type;
1219           type->name = xbt_strdup(name);
1220           type->is_pointer_type = is_pointer;
1221           type->id = (void *)strtoul(origin, NULL, 16);
1222           if(type_origin)
1223             type->dw_type_id = xbt_strdup(type_origin);
1224           type->members = NULL;
1225
1226           xbt_dict_set(*types, origin, type, NULL);
1227
1228           xbt_free(name);
1229           name = NULL;
1230           xbt_free(end);
1231           end = NULL;
1232           xbt_free(type_origin);
1233           type_origin = NULL;
1234           size = 0;
1235         }
1236
1237         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_subrange_type)") != 0)
1238           break;
1239
1240         read = xbt_getline(&line, &n, fp);
1241
1242       }
1243
1244       xbt_free(origin);
1245       origin = NULL;
1246
1247     }else{
1248
1249       read = xbt_getline(&line, &n, fp);
1250
1251     }
1252
1253   }
1254
1255   xbt_dynar_free(&split);
1256   xbt_dict_free(&variables_origin);
1257   xbt_dict_free(&subprograms_origin);
1258   xbt_free(line);
1259   xbt_free(command);
1260   xbt_dict_free(&location_list);
1261
1262   pclose(fp);
1263   return result;
1264 }
1265
1266
1267 /*******************************  Ignore mechanism *******************************/
1268 /*********************************************************************************/
1269
1270 xbt_dynar_t mc_checkpoint_ignore;
1271
1272 typedef struct s_mc_stack_ignore_variable{
1273   char *var_name;
1274   char *frame;
1275 }s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
1276
1277 typedef struct s_mc_data_bss_ignore_variable{
1278   char *name;
1279 }s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t;
1280
1281 /**************************** Free functions ******************************/
1282
1283 static void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
1284   xbt_free(v->var_name);
1285   xbt_free(v->frame);
1286   xbt_free(v);
1287 }
1288
1289 static void stack_ignore_variable_free_voidp(void *v){
1290   stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
1291 }
1292
1293 void heap_ignore_region_free(mc_heap_ignore_region_t r){
1294   xbt_free(r);
1295 }
1296
1297 void heap_ignore_region_free_voidp(void *r){
1298   heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
1299 }
1300
1301 static void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v){
1302   xbt_free(v->name);
1303   xbt_free(v);
1304 }
1305
1306 static void data_bss_ignore_variable_free_voidp(void *v){
1307   data_bss_ignore_variable_free((mc_data_bss_ignore_variable_t) * (void **) v);
1308 }
1309
1310 static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r){
1311   xbt_free(r);
1312 }
1313
1314 static void checkpoint_ignore_region_free_voidp(void *r){
1315   checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
1316 }
1317
1318 /***********************************************************************/
1319
1320 void MC_ignore_heap(void *address, size_t size){
1321
1322   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1323
1324   MC_SET_RAW_MEM;
1325
1326   mc_heap_ignore_region_t region = NULL;
1327   region = xbt_new0(s_mc_heap_ignore_region_t, 1);
1328   region->address = address;
1329   region->size = size;
1330
1331   region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
1332
1333   if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
1334     region->fragment = -1;
1335     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
1336   }else{
1337     region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
1338     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
1339   }
1340
1341   if(mc_heap_comparison_ignore == NULL){
1342     mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
1343     xbt_dynar_push(mc_heap_comparison_ignore, &region);
1344     if(!raw_mem_set)
1345       MC_UNSET_RAW_MEM;
1346     return;
1347   }
1348
1349   unsigned int cursor = 0;
1350   mc_heap_ignore_region_t current_region = NULL;
1351   int start = 0;
1352   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
1353
1354   while(start <= end){
1355     cursor = (start + end) / 2;
1356     current_region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
1357     if(current_region->address == address){
1358       heap_ignore_region_free(region);
1359       if(!raw_mem_set)
1360         MC_UNSET_RAW_MEM;
1361       return;
1362     }else if(current_region->address < address){
1363       start = cursor + 1;
1364     }else{
1365       end = cursor - 1;
1366     }
1367   }
1368
1369   if(current_region->address < address)
1370     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
1371   else
1372     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
1373
1374   if(!raw_mem_set)
1375     MC_UNSET_RAW_MEM;
1376 }
1377
1378 void MC_remove_ignore_heap(void *address, size_t size){
1379
1380   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1381
1382   MC_SET_RAW_MEM;
1383
1384   unsigned int cursor = 0;
1385   int start = 0;
1386   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
1387   mc_heap_ignore_region_t region;
1388   int ignore_found = 0;
1389
1390   while(start <= end){
1391     cursor = (start + end) / 2;
1392     region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
1393     if(region->address == address){
1394       ignore_found = 1;
1395       break;
1396     }else if(region->address < address){
1397       start = cursor + 1;
1398     }else{
1399       if((char * )region->address <= ((char *)address + size)){
1400         ignore_found = 1;
1401         break;
1402       }else{
1403         end = cursor - 1;
1404       }
1405     }
1406   }
1407
1408   if(ignore_found == 1){
1409     xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
1410     MC_remove_ignore_heap(address, size);
1411   }
1412
1413   if(!raw_mem_set)
1414     MC_UNSET_RAW_MEM;
1415
1416 }
1417
1418 void MC_ignore_global_variable(const char *name){
1419
1420   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1421
1422   MC_SET_RAW_MEM;
1423
1424   if(mc_libsimgrid_info){
1425
1426     unsigned int cursor = 0;
1427     dw_variable_t current_var;
1428     int start = 0;
1429     int end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
1430
1431     while(start <= end){
1432       cursor = (start + end) /2;
1433       current_var = (dw_variable_t)xbt_dynar_get_as(mc_libsimgrid_info->global_variables, cursor, dw_variable_t);
1434       if(strcmp(current_var->name, name) == 0){
1435         xbt_dynar_remove_at(mc_libsimgrid_info->global_variables, cursor, NULL);
1436         start = 0;
1437         end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
1438       }else if(strcmp(current_var->name, name) < 0){
1439         start = cursor + 1;
1440       }else{
1441         end = cursor - 1;
1442       }
1443     }
1444
1445   }else{
1446
1447     if(mc_data_bss_comparison_ignore == NULL)
1448       mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), data_bss_ignore_variable_free_voidp);
1449
1450     mc_data_bss_ignore_variable_t var = NULL;
1451     var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
1452     var->name = strdup(name);
1453
1454     if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
1455
1456       xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
1457
1458     }else{
1459
1460       unsigned int cursor = 0;
1461       int start = 0;
1462       int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
1463       mc_data_bss_ignore_variable_t current_var = NULL;
1464
1465       while(start <= end){
1466         cursor = (start + end) / 2;
1467         current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
1468         if(strcmp(current_var->name, name) == 0){
1469           data_bss_ignore_variable_free(var);
1470           if(!raw_mem_set)
1471             MC_UNSET_RAW_MEM;
1472           return;
1473         }else if(strcmp(current_var->name, name) < 0){
1474           start = cursor + 1;
1475         }else{
1476           end = cursor - 1;
1477         }
1478       }
1479
1480       if(strcmp(current_var->name, name) < 0)
1481         xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
1482       else
1483         xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);
1484
1485     }
1486   }
1487
1488   if(!raw_mem_set)
1489     MC_UNSET_RAW_MEM;
1490 }
1491
1492 void MC_ignore_local_variable(const char *var_name, const char *frame_name){
1493
1494   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1495
1496   MC_SET_RAW_MEM;
1497
1498   if(mc_libsimgrid_info){
1499     unsigned int cursor = 0;
1500     dw_variable_t current_var;
1501     int start, end;
1502     if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames */
1503       xbt_dict_cursor_t dict_cursor;
1504       char *current_frame_name;
1505       dw_frame_t frame;
1506       xbt_dict_foreach(mc_libsimgrid_info->local_variables, dict_cursor, current_frame_name, frame){
1507         start = 0;
1508         end = xbt_dynar_length(frame->variables) - 1;
1509         while(start <= end){
1510           cursor = (start + end) / 2;
1511           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
1512           if(strcmp(current_var->name, var_name) == 0){
1513             xbt_dynar_remove_at(frame->variables, cursor, NULL);
1514             start = 0;
1515             end = xbt_dynar_length(frame->variables) - 1;
1516           }else if(strcmp(current_var->name, var_name) < 0){
1517             start = cursor + 1;
1518           }else{
1519             end = cursor - 1;
1520           }
1521         }
1522       }
1523        xbt_dict_foreach(mc_binary_info->local_variables, dict_cursor, current_frame_name, frame){
1524         start = 0;
1525         end = xbt_dynar_length(frame->variables) - 1;
1526         while(start <= end){
1527           cursor = (start + end) / 2;
1528           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
1529           if(strcmp(current_var->name, var_name) == 0){
1530             xbt_dynar_remove_at(frame->variables, cursor, NULL);
1531             start = 0;
1532             end = xbt_dynar_length(frame->variables) - 1;
1533           }else if(strcmp(current_var->name, var_name) < 0){
1534             start = cursor + 1;
1535           }else{
1536             end = cursor - 1;
1537           }
1538         }
1539       }
1540     }else{
1541       xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(
1542                                       mc_libsimgrid_info->local_variables, frame_name))->variables;
1543       start = 0;
1544       end = xbt_dynar_length(variables_list) - 1;
1545       while(start <= end){
1546         cursor = (start + end) / 2;
1547         current_var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor, dw_variable_t);
1548         if(strcmp(current_var->name, var_name) == 0){
1549           xbt_dynar_remove_at(variables_list, cursor, NULL);
1550           start = 0;
1551           end = xbt_dynar_length(variables_list) - 1;
1552         }else if(strcmp(current_var->name, var_name) < 0){
1553           start = cursor + 1;
1554         }else{
1555           end = cursor - 1;
1556         }
1557       }
1558     }
1559   }else{
1560
1561     if(mc_stack_comparison_ignore == NULL)
1562       mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), stack_ignore_variable_free_voidp);
1563
1564     mc_stack_ignore_variable_t var = NULL;
1565     var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
1566     var->var_name = strdup(var_name);
1567     var->frame = strdup(frame_name);
1568
1569     if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){
1570
1571       xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
1572
1573     }else{
1574
1575       unsigned int cursor = 0;
1576       int start = 0;
1577       int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
1578       mc_stack_ignore_variable_t current_var = NULL;
1579
1580       while(start <= end){
1581         cursor = (start + end) / 2;
1582         current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
1583         if(strcmp(current_var->frame, frame_name) == 0){
1584           if(strcmp(current_var->var_name, var_name) == 0){
1585             stack_ignore_variable_free(var);
1586             if(!raw_mem_set)
1587               MC_UNSET_RAW_MEM;
1588             return;
1589           }else if(strcmp(current_var->var_name, var_name) < 0){
1590             start = cursor + 1;
1591           }else{
1592             end = cursor - 1;
1593           }
1594         }else if(strcmp(current_var->frame, frame_name) < 0){
1595           start = cursor + 1;
1596         }else{
1597           end = cursor - 1;
1598         }
1599       }
1600
1601       if(strcmp(current_var->frame, frame_name) == 0){
1602         if(strcmp(current_var->var_name, var_name) < 0){
1603           xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
1604         }else{
1605           xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
1606         }
1607       }else if(strcmp(current_var->frame, frame_name) < 0){
1608         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
1609       }else{
1610         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
1611       }
1612     }
1613   }
1614
1615   if(!raw_mem_set)
1616     MC_UNSET_RAW_MEM;
1617
1618 }
1619
1620 void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
1621
1622   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1623
1624   MC_SET_RAW_MEM;
1625
1626   if(stacks_areas == NULL)
1627     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
1628
1629   stack_region_t region = NULL;
1630   region = xbt_new0(s_stack_region_t, 1);
1631   region->address = stack;
1632   region->process_name = strdup(name);
1633   region->context = context;
1634   region->size = size;
1635   region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
1636   xbt_dynar_push(stacks_areas, &region);
1637
1638   if(!raw_mem_set)
1639     MC_UNSET_RAW_MEM;
1640 }
1641
1642 void MC_ignore(void *addr, size_t size){
1643
1644   int raw_mem_set= (mmalloc_get_current_heap() == raw_heap);
1645
1646   MC_SET_RAW_MEM;
1647
1648   if(mc_checkpoint_ignore == NULL)
1649     mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp);
1650
1651   mc_checkpoint_ignore_region_t region = xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
1652   region->addr = addr;
1653   region->size = size;
1654
1655   if(xbt_dynar_is_empty(mc_checkpoint_ignore)){
1656     xbt_dynar_push(mc_checkpoint_ignore, &region);
1657   }else{
1658
1659     unsigned int cursor = 0;
1660     int start = 0;
1661     int end = xbt_dynar_length(mc_checkpoint_ignore) -1;
1662     mc_checkpoint_ignore_region_t current_region = NULL;
1663
1664     while(start <= end){
1665       cursor = (start + end) / 2;
1666       current_region = (mc_checkpoint_ignore_region_t)xbt_dynar_get_as(mc_checkpoint_ignore, cursor, mc_checkpoint_ignore_region_t);
1667       if(current_region->addr == addr){
1668         if(current_region->size == size){
1669           checkpoint_ignore_region_free(region);
1670           if(!raw_mem_set)
1671             MC_UNSET_RAW_MEM;
1672           return;
1673         }else if(current_region->size < size){
1674           start = cursor + 1;
1675         }else{
1676           end = cursor - 1;
1677         }
1678       }else if(current_region->addr < addr){
1679           start = cursor + 1;
1680       }else{
1681         end = cursor - 1;
1682       }
1683     }
1684
1685      if(current_region->addr == addr){
1686        if(current_region->size < size){
1687         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
1688       }else{
1689         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
1690       }
1691     }else if(current_region->addr < addr){
1692        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
1693     }else{
1694        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
1695     }
1696   }
1697
1698   if(!raw_mem_set)
1699     MC_UNSET_RAW_MEM;
1700 }
1701
1702 /*******************************  Initialisation of MC *******************************/
1703 /*********************************************************************************/
1704
1705 static void MC_dump_ignored_local_variables(void){
1706
1707   if(mc_stack_comparison_ignore == NULL || xbt_dynar_is_empty(mc_stack_comparison_ignore))
1708     return;
1709
1710   unsigned int cursor = 0;
1711   mc_stack_ignore_variable_t current_var;
1712
1713   xbt_dynar_foreach(mc_stack_comparison_ignore, cursor, current_var){
1714     MC_ignore_local_variable(current_var->var_name, current_var->frame);
1715   }
1716
1717   xbt_dynar_free(&mc_stack_comparison_ignore);
1718   mc_stack_comparison_ignore = NULL;
1719
1720 }
1721
1722 static void MC_dump_ignored_global_variables(void){
1723
1724   if(mc_data_bss_comparison_ignore == NULL || xbt_dynar_is_empty(mc_data_bss_comparison_ignore))
1725     return;
1726
1727   unsigned int cursor = 0;
1728   mc_data_bss_ignore_variable_t current_var;
1729
1730   xbt_dynar_foreach(mc_data_bss_comparison_ignore, cursor, current_var){
1731     MC_ignore_global_variable(current_var->name);
1732   }
1733
1734   xbt_dynar_free(&mc_data_bss_comparison_ignore);
1735   mc_data_bss_comparison_ignore = NULL;
1736
1737 }
1738
1739 void MC_init(){
1740
1741   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1742
1743   compare = 0;
1744
1745   /* Initialize the data structures that must be persistent across every
1746      iteration of the model-checker (in RAW memory) */
1747
1748   MC_SET_RAW_MEM;
1749
1750   MC_init_memory_map_info();
1751
1752   XBT_INFO("Get debug information ...");
1753
1754   /* Get local variables for state equality detection */
1755   mc_binary_info = MC_dwarf_get_variables(xbt_binary_name);
1756   mc_libsimgrid_info = MC_dwarf_get_variables(libsimgrid_path);
1757
1758   mc_local_variables_libsimgrid = mc_libsimgrid_info->local_variables;
1759   mc_local_variables_binary = mc_binary_info->local_variables;
1760   mc_global_variables_libsimgrid = mc_libsimgrid_info->global_variables;
1761   mc_global_variables_binary = mc_binary_info->global_variables;
1762   mc_variables_type_libsimgrid = mc_libsimgrid_info->types;
1763   mc_variables_type_binary = mc_binary_info->types;
1764
1765   XBT_INFO("Get debug information done !");
1766
1767   /* Remove variables ignored before getting list of variables */
1768   MC_dump_ignored_local_variables();
1769   MC_dump_ignored_global_variables();
1770
1771   /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
1772   MC_get_libsimgrid_plt_section();
1773   MC_get_binary_plt_section();
1774
1775    /* Init parmap */
1776   parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
1777
1778   MC_UNSET_RAW_MEM;
1779
1780    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
1781   MC_ignore_local_variable("e", "*");
1782   MC_ignore_local_variable("__ex_cleanup", "*");
1783   MC_ignore_local_variable("__ex_mctx_en", "*");
1784   MC_ignore_local_variable("__ex_mctx_me", "*");
1785   MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
1786   MC_ignore_local_variable("_log_ev", "*");
1787   MC_ignore_local_variable("_throw_ctx", "*");
1788   MC_ignore_local_variable("ctx", "*");
1789
1790   MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
1791   MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
1792
1793   /* Ignore local variable about time used for tracing */
1794   MC_ignore_local_variable("start_time", "*");
1795
1796   MC_ignore_global_variable("mc_comp_times");
1797   MC_ignore_global_variable("mc_snapshot_comparison_time");
1798   MC_ignore_global_variable("mc_time");
1799   MC_ignore_global_variable("smpi_current_rank");
1800   MC_ignore_global_variable("counter"); /* Static variable used for tracing */
1801   MC_ignore_global_variable("maestro_stack_start");
1802   MC_ignore_global_variable("maestro_stack_end");
1803
1804   MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run));
1805   MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran));
1806   MC_ignore_heap(simix_global->process_to_run, sizeof(*(simix_global->process_to_run)));
1807   MC_ignore_heap(simix_global->process_that_ran, sizeof(*(simix_global->process_that_ran)));
1808
1809   smx_process_t process;
1810   xbt_swag_foreach(process, simix_global->process_list){
1811     MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
1812   }
1813
1814   if(raw_mem_set)
1815     MC_SET_RAW_MEM;
1816
1817 }
1818
1819 static void MC_init_dot_output(){ /* FIXME : more colors */
1820
1821   colors[0] = "blue";
1822   colors[1] = "red";
1823   colors[2] = "green3";
1824   colors[3] = "goldenrod";
1825   colors[4] = "brown";
1826   colors[5] = "purple";
1827   colors[6] = "magenta";
1828   colors[7] = "turquoise4";
1829   colors[8] = "gray25";
1830   colors[9] = "forestgreen";
1831   colors[10] = "hotpink";
1832   colors[11] = "lightblue";
1833   colors[12] = "tan";
1834
1835   dot_output = fopen(_sg_mc_dot_output_file, "w");
1836
1837   if(dot_output == NULL){
1838     perror("Error open dot output file");
1839     xbt_abort();
1840   }
1841
1842   fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
1843
1844 }
1845
1846 /*******************************  Core of MC *******************************/
1847 /**************************************************************************/
1848
1849 void MC_do_the_modelcheck_for_real() {
1850
1851   MC_SET_RAW_MEM;
1852   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
1853   MC_UNSET_RAW_MEM;
1854
1855   if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
1856     if (mc_reduce_kind==e_mc_reduce_unset)
1857       mc_reduce_kind=e_mc_reduce_dpor;
1858
1859     XBT_INFO("Check a safety property");
1860     MC_modelcheck_safety();
1861
1862   } else  {
1863
1864     if (mc_reduce_kind==e_mc_reduce_unset)
1865       mc_reduce_kind=e_mc_reduce_none;
1866
1867     XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
1868     MC_automaton_load(_sg_mc_property_file);
1869     MC_modelcheck_liveness();
1870   }
1871 }
1872
1873 void MC_modelcheck_safety(void)
1874 {
1875   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1876
1877   /* Check if MC is already initialized */
1878   if (initial_state_safety)
1879     return;
1880
1881   mc_time = xbt_new0(double, simix_process_maxpid);
1882
1883   /* mc_time refers to clock for each process -> ignore it for heap comparison */
1884   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1885
1886   /* Initialize the data structures that must be persistent across every
1887      iteration of the model-checker (in RAW memory) */
1888
1889   MC_SET_RAW_MEM;
1890
1891   /* Initialize statistics */
1892   mc_stats = xbt_new0(s_mc_stats_t, 1);
1893   mc_stats->state_size = 1;
1894
1895   /* Create exploration stack */
1896   mc_stack_safety = xbt_fifo_new();
1897
1898   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1899     MC_init_dot_output();
1900
1901   MC_UNSET_RAW_MEM;
1902
1903   if(_sg_mc_visited > 0){
1904     MC_init();
1905   }else{
1906     MC_SET_RAW_MEM;
1907     MC_init_memory_map_info();
1908     MC_get_libsimgrid_plt_section();
1909     MC_get_binary_plt_section();
1910     MC_UNSET_RAW_MEM;
1911   }
1912
1913   MC_dpor_init();
1914
1915   MC_SET_RAW_MEM;
1916   /* Save the initial state */
1917   initial_state_safety = xbt_new0(s_mc_global_t, 1);
1918   initial_state_safety->snapshot = MC_take_snapshot(0);
1919   MC_UNSET_RAW_MEM;
1920
1921   MC_dpor();
1922
1923   if(raw_mem_set)
1924     MC_SET_RAW_MEM;
1925
1926   xbt_abort();
1927   //MC_exit();
1928 }
1929
1930 void MC_modelcheck_liveness(){
1931
1932   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1933
1934   MC_init();
1935
1936   mc_time = xbt_new0(double, simix_process_maxpid);
1937
1938   /* mc_time refers to clock for each process -> ignore it for heap comparison */
1939   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1940
1941   MC_SET_RAW_MEM;
1942
1943   /* Initialize statistics */
1944   mc_stats = xbt_new0(s_mc_stats_t, 1);
1945   mc_stats->state_size = 1;
1946
1947   /* Create exploration stack */
1948   mc_stack_liveness = xbt_fifo_new();
1949
1950   /* Create the initial state */
1951   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
1952
1953   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1954     MC_init_dot_output();
1955
1956   MC_UNSET_RAW_MEM;
1957
1958   MC_ddfs_init();
1959
1960   /* We're done */
1961   MC_print_statistics(mc_stats);
1962   xbt_free(mc_time);
1963
1964   if(raw_mem_set)
1965     MC_SET_RAW_MEM;
1966
1967 }
1968
1969
1970 void MC_exit(void)
1971 {
1972   xbt_free(mc_time);
1973   MC_memory_exit();
1974   //xbt_abort();
1975 }
1976
1977 int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
1978
1979   return simcall->mc_value;
1980 }
1981
1982
1983 int MC_random(int min, int max)
1984 {
1985   /*FIXME: return mc_current_state->executed_transition->random.value;*/
1986   return simcall_mc_random(min, max);
1987 }
1988
1989 /**
1990  * \brief Schedules all the process that are ready to run
1991  */
1992 void MC_wait_for_requests(void)
1993 {
1994   smx_process_t process;
1995   smx_simcall_t req;
1996   unsigned int iter;
1997
1998   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
1999     SIMIX_process_runall();
2000     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
2001       req = &process->simcall;
2002       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
2003         SIMIX_simcall_pre(req, 0);
2004     }
2005   }
2006 }
2007
2008 int MC_deadlock_check()
2009 {
2010   int deadlock = FALSE;
2011   smx_process_t process;
2012   if(xbt_swag_size(simix_global->process_list)){
2013     deadlock = TRUE;
2014     xbt_swag_foreach(process, simix_global->process_list){
2015       if(process->simcall.call != SIMCALL_NONE
2016          && MC_request_is_enabled(&process->simcall)){
2017         deadlock = FALSE;
2018         break;
2019       }
2020     }
2021   }
2022   return deadlock;
2023 }
2024
2025 /**
2026  * \brief Re-executes from the state at position start all the transitions indicated by
2027  *        a given model-checker stack.
2028  * \param stack The stack with the transitions to execute.
2029  * \param start Start index to begin the re-execution.
2030  */
2031 void MC_replay(xbt_fifo_t stack, int start)
2032 {
2033   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
2034
2035   int value, i = 1, count = 1;
2036   char *req_str;
2037   smx_simcall_t req = NULL, saved_req = NULL;
2038   xbt_fifo_item_t item, start_item;
2039   mc_state_t state;
2040   smx_process_t process = NULL;
2041
2042   XBT_DEBUG("**** Begin Replay ****");
2043
2044   if(start == -1){
2045     /* Restore the initial state */
2046     MC_restore_snapshot(initial_state_safety->snapshot);
2047     /* At the moment of taking the snapshot the raw heap was set, so restoring
2048      * it will set it back again, we have to unset it to continue  */
2049     MC_UNSET_RAW_MEM;
2050   }
2051
2052   start_item = xbt_fifo_get_last_item(stack);
2053   if(start != -1){
2054     while (i != start){
2055       start_item = xbt_fifo_get_prev_item(start_item);
2056       i++;
2057     }
2058   }
2059
2060   MC_SET_RAW_MEM;
2061   xbt_dict_reset(first_enabled_state);
2062   xbt_swag_foreach(process, simix_global->process_list){
2063     if(MC_process_is_enabled(process)){
2064       char *key = bprintf("%lu", process->pid);
2065       char *data = bprintf("%d", count);
2066       xbt_dict_set(first_enabled_state, key, data, NULL);
2067       xbt_free(key);
2068     }
2069   }
2070   MC_UNSET_RAW_MEM;
2071
2072
2073   /* Traverse the stack from the state at position start and re-execute the transitions */
2074   for (item = start_item;
2075        item != xbt_fifo_get_first_item(stack);
2076        item = xbt_fifo_get_prev_item(item)) {
2077
2078     state = (mc_state_t) xbt_fifo_get_item_content(item);
2079     saved_req = MC_state_get_executed_request(state, &value);
2080
2081     MC_SET_RAW_MEM;
2082     char *key = bprintf("%lu", saved_req->issuer->pid);
2083     xbt_dict_remove(first_enabled_state, key);
2084     xbt_free(key);
2085     MC_UNSET_RAW_MEM;
2086
2087     if(saved_req){
2088       /* because we got a copy of the executed request, we have to fetch the
2089          real one, pointed by the request field of the issuer process */
2090       req = &saved_req->issuer->simcall;
2091
2092       /* Debug information */
2093       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2094         req_str = MC_request_to_string(req, value);
2095         XBT_DEBUG("Replay: %s (%p)", req_str, state);
2096         xbt_free(req_str);
2097       }
2098     }
2099
2100     SIMIX_simcall_pre(req, value);
2101     MC_wait_for_requests();
2102
2103     count++;
2104
2105     MC_SET_RAW_MEM;
2106     /* Insert in dict all enabled processes */
2107     xbt_swag_foreach(process, simix_global->process_list){
2108       if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
2109         char *key = bprintf("%lu", process->pid);
2110         if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
2111           char *data = bprintf("%d", count);
2112           xbt_dict_set(first_enabled_state, key, data, NULL);
2113         }
2114         xbt_free(key);
2115       }
2116     }
2117     MC_UNSET_RAW_MEM;
2118
2119     /* Update statistics */
2120     mc_stats->visited_states++;
2121     mc_stats->executed_transitions++;
2122
2123   }
2124
2125   XBT_DEBUG("**** End Replay ****");
2126
2127   if(raw_mem)
2128     MC_SET_RAW_MEM;
2129   else
2130     MC_UNSET_RAW_MEM;
2131
2132
2133 }
2134
2135 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
2136 {
2137
2138   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2139
2140   int value;
2141   char *req_str;
2142   smx_simcall_t req = NULL, saved_req = NULL;
2143   xbt_fifo_item_t item;
2144   mc_state_t state;
2145   mc_pair_t pair;
2146   int depth = 1;
2147
2148   XBT_DEBUG("**** Begin Replay ****");
2149
2150   /* Restore the initial state */
2151   MC_restore_snapshot(initial_state_liveness->snapshot);
2152
2153   /* At the moment of taking the snapshot the raw heap was set, so restoring
2154    * it will set it back again, we have to unset it to continue  */
2155   if(!initial_state_liveness->raw_mem_set)
2156     MC_UNSET_RAW_MEM;
2157
2158   if(all_stack){
2159
2160     item = xbt_fifo_get_last_item(stack);
2161
2162     while(depth <= xbt_fifo_size(stack)){
2163
2164       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
2165       state = (mc_state_t) pair->graph_state;
2166
2167       if(pair->requests > 0){
2168
2169         saved_req = MC_state_get_executed_request(state, &value);
2170         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
2171
2172         if(saved_req != NULL){
2173           /* because we got a copy of the executed request, we have to fetch the
2174              real one, pointed by the request field of the issuer process */
2175           req = &saved_req->issuer->simcall;
2176           //XBT_DEBUG("Req->call %u", req->call);
2177
2178           /* Debug information */
2179           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2180             req_str = MC_request_to_string(req, value);
2181             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
2182             xbt_free(req_str);
2183           }
2184
2185         }
2186
2187         SIMIX_simcall_pre(req, value);
2188         MC_wait_for_requests();
2189       }
2190
2191       depth++;
2192
2193       /* Update statistics */
2194       mc_stats->visited_pairs++;
2195       mc_stats->executed_transitions++;
2196
2197       item = xbt_fifo_get_prev_item(item);
2198     }
2199
2200   }else{
2201
2202     /* Traverse the stack from the initial state and re-execute the transitions */
2203     for (item = xbt_fifo_get_last_item(stack);
2204          item != xbt_fifo_get_first_item(stack);
2205          item = xbt_fifo_get_prev_item(item)) {
2206
2207       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
2208       state = (mc_state_t) pair->graph_state;
2209
2210       if(pair->requests > 0){
2211
2212         saved_req = MC_state_get_executed_request(state, &value);
2213         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
2214
2215         if(saved_req != NULL){
2216           /* because we got a copy of the executed request, we have to fetch the
2217              real one, pointed by the request field of the issuer process */
2218           req = &saved_req->issuer->simcall;
2219           //XBT_DEBUG("Req->call %u", req->call);
2220
2221           /* Debug information */
2222           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2223             req_str = MC_request_to_string(req, value);
2224             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
2225             xbt_free(req_str);
2226           }
2227
2228         }
2229
2230         SIMIX_simcall_pre(req, value);
2231         MC_wait_for_requests();
2232       }
2233
2234       depth++;
2235
2236       /* Update statistics */
2237       mc_stats->visited_pairs++;
2238       mc_stats->executed_transitions++;
2239     }
2240   }
2241
2242   XBT_DEBUG("**** End Replay ****");
2243
2244   if(initial_state_liveness->raw_mem_set)
2245     MC_SET_RAW_MEM;
2246   else
2247     MC_UNSET_RAW_MEM;
2248
2249 }
2250
2251 /**
2252  * \brief Dumps the contents of a model-checker's stack and shows the actual
2253  *        execution trace
2254  * \param stack The stack to dump
2255  */
2256 void MC_dump_stack_safety(xbt_fifo_t stack)
2257 {
2258
2259   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2260
2261   MC_show_stack_safety(stack);
2262
2263   if(!_sg_mc_checkpoint){
2264
2265     mc_state_t state;
2266
2267     MC_SET_RAW_MEM;
2268     while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
2269       MC_state_delete(state);
2270     MC_UNSET_RAW_MEM;
2271
2272   }
2273
2274   if(raw_mem_set)
2275     MC_SET_RAW_MEM;
2276   else
2277     MC_UNSET_RAW_MEM;
2278
2279 }
2280
2281
2282 void MC_show_stack_safety(xbt_fifo_t stack)
2283 {
2284
2285   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2286
2287   MC_SET_RAW_MEM;
2288
2289   int value;
2290   mc_state_t state;
2291   xbt_fifo_item_t item;
2292   smx_simcall_t req;
2293   char *req_str = NULL;
2294
2295   for (item = xbt_fifo_get_last_item(stack);
2296        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
2297         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
2298     req = MC_state_get_executed_request(state, &value);
2299     if(req){
2300       req_str = MC_request_to_string(req, value);
2301       XBT_INFO("%s", req_str);
2302       xbt_free(req_str);
2303     }
2304   }
2305
2306   if(!raw_mem_set)
2307     MC_UNSET_RAW_MEM;
2308 }
2309
2310 void MC_show_deadlock(smx_simcall_t req)
2311 {
2312   /*char *req_str = NULL;*/
2313   XBT_INFO("**************************");
2314   XBT_INFO("*** DEAD-LOCK DETECTED ***");
2315   XBT_INFO("**************************");
2316   XBT_INFO("Locked request:");
2317   /*req_str = MC_request_to_string(req);
2318     XBT_INFO("%s", req_str);
2319     xbt_free(req_str);*/
2320   XBT_INFO("Counter-example execution trace:");
2321   MC_dump_stack_safety(mc_stack_safety);
2322   MC_print_statistics(mc_stats);
2323 }
2324
2325
2326 void MC_show_stack_liveness(xbt_fifo_t stack){
2327   int value;
2328   mc_pair_t pair;
2329   xbt_fifo_item_t item;
2330   smx_simcall_t req;
2331   char *req_str = NULL;
2332
2333   for (item = xbt_fifo_get_last_item(stack);
2334        (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
2335         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
2336     req = MC_state_get_executed_request(pair->graph_state, &value);
2337     if(req){
2338       if(pair->requests>0){
2339         req_str = MC_request_to_string(req, value);
2340         XBT_INFO("%s", req_str);
2341         xbt_free(req_str);
2342       }else{
2343         XBT_INFO("End of system requests but evolution in Büchi automaton");
2344       }
2345     }
2346   }
2347 }
2348
2349 void MC_dump_stack_liveness(xbt_fifo_t stack){
2350
2351   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2352
2353   mc_pair_t pair;
2354
2355   MC_SET_RAW_MEM;
2356   while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
2357     MC_pair_delete(pair);
2358   MC_UNSET_RAW_MEM;
2359
2360   if(raw_mem_set)
2361     MC_SET_RAW_MEM;
2362
2363 }
2364
2365
2366 void MC_print_statistics(mc_stats_t stats)
2367 {
2368   if(stats->expanded_pairs == 0){
2369     XBT_INFO("Expanded states = %lu", stats->expanded_states);
2370     XBT_INFO("Visited states = %lu", stats->visited_states);
2371   }else{
2372     XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
2373     XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
2374   }
2375   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
2376   MC_SET_RAW_MEM;
2377   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
2378     fprintf(dot_output, "}\n");
2379     fclose(dot_output);
2380   }
2381   MC_UNSET_RAW_MEM;
2382 }
2383
2384 void MC_assert(int prop)
2385 {
2386   if (MC_is_active() && !prop){
2387     XBT_INFO("**************************");
2388     XBT_INFO("*** PROPERTY NOT VALID ***");
2389     XBT_INFO("**************************");
2390     XBT_INFO("Counter-example execution trace:");
2391     MC_dump_stack_safety(mc_stack_safety);
2392     MC_print_statistics(mc_stats);
2393     xbt_abort();
2394   }
2395 }
2396
2397 void MC_cut(void){
2398   user_max_depth_reached = 1;
2399 }
2400
2401 void MC_process_clock_add(smx_process_t process, double amount)
2402 {
2403   mc_time[process->pid] += amount;
2404 }
2405
2406 double MC_process_clock_get(smx_process_t process)
2407 {
2408   if(mc_time){
2409     if(process != NULL)
2410       return mc_time[process->pid];
2411     else
2412       return -1;
2413   }else{
2414     return 0;
2415   }
2416 }
2417
2418 void MC_automaton_load(const char *file){
2419
2420   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2421
2422   MC_SET_RAW_MEM;
2423
2424   if (_mc_property_automaton == NULL)
2425     _mc_property_automaton = xbt_automaton_new();
2426
2427   xbt_automaton_load(_mc_property_automaton,file);
2428
2429   MC_UNSET_RAW_MEM;
2430
2431   if(raw_mem_set)
2432     MC_SET_RAW_MEM;
2433
2434 }
2435
2436 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
2437
2438   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2439
2440   MC_SET_RAW_MEM;
2441
2442   if (_mc_property_automaton == NULL)
2443     _mc_property_automaton = xbt_automaton_new();
2444
2445   xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
2446
2447   MC_UNSET_RAW_MEM;
2448
2449   if(raw_mem_set)
2450     MC_SET_RAW_MEM;
2451
2452 }
2453
2454
2455