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