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