src/mc/mc_global.c

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