src/mc/mc_global.c

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