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