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