src/mc/mc_global.c

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