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