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