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