src/mc/mc_global.c

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