src/mc/mc_global.c

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