src/mc/mc_global.c

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