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 #include <libgen.h>
  12
  13 #include "simgrid/sg_config.h"
  14 #include "../surf/surf_private.h"
  15 #include "../simix/smx_private.h"
  16 #include "../xbt/mmalloc/mmprivate.h"
  17 #include "xbt/fifo.h"
  18 #include "mc_private.h"
  19 #include "xbt/automaton.h"
  20 #include "xbt/dict.h"
  21
  22 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
  23 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
  24                                 "Logging specific to MC (global)");
  25
  26 /* Configuration support */
  27 e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
  28
  29 int _sg_do_model_check = 0;
  30 int _sg_mc_checkpoint=0;
  31 char* _sg_mc_property_file=NULL;
  32 int _sg_mc_timeout=0;
  33 int _sg_mc_hash=0;
  34 int _sg_mc_max_depth=1000;
  35 int _sg_mc_visited=0;
  36 char *_sg_mc_dot_output_file = NULL;
  37
  38 int user_max_depth_reached = 0;
  39
  40 void _mc_cfg_cb_reduce(const char *name, int pos) {
  41   if (_sg_cfg_init_status && !_sg_do_model_check) {
  42     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.");
  43   }
  44   char *val= xbt_cfg_get_string(_sg_cfg_set, name);
  45   if (!strcasecmp(val,"none")) {
  46     mc_reduce_kind = e_mc_reduce_none;
  47   } else if (!strcasecmp(val,"dpor")) {
  48     mc_reduce_kind = e_mc_reduce_dpor;
  49   } else {
  50     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
  51   }
  52 }
  53
  54 void _mc_cfg_cb_checkpoint(const char *name, int pos) {
  55   if (_sg_cfg_init_status && !_sg_do_model_check) {
  56     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.");
  57   }
  58   _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
  59 }
  60 void _mc_cfg_cb_property(const char *name, int pos) {
  61   if (_sg_cfg_init_status && !_sg_do_model_check) {
  62     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.");
  63   }
  64   _sg_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
  65 }
  66
  67 void _mc_cfg_cb_timeout(const char *name, int pos) {
  68   if (_sg_cfg_init_status && !_sg_do_model_check) {
  69     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.");
  70   }
  71   _sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
  72 }
  73
  74 void _mc_cfg_cb_hash(const char *name, int pos) {
  75   if (_sg_cfg_init_status && !_sg_do_model_check) {
  76     xbt_die("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  77   }
  78   _sg_mc_hash= xbt_cfg_get_boolean(_sg_cfg_set, name);
  79 }
  80
  81 void _mc_cfg_cb_max_depth(const char *name, int pos) {
  82   if (_sg_cfg_init_status && !_sg_do_model_check) {
  83     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.");
  84   }
  85   _sg_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
  86 }
  87
  88 void _mc_cfg_cb_visited(const char *name, int pos) {
  89   if (_sg_cfg_init_status && !_sg_do_model_check) {
  90     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.");
  91   }
  92   _sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
  93 }
  94
  95 void _mc_cfg_cb_dot_output(const char *name, int pos) {
  96   if (_sg_cfg_init_status && !_sg_do_model_check) {
  97     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.");
  98   }
  99   _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
 100 }
 101
 102 /* MC global data structures */
 103 mc_state_t mc_current_state = NULL;
 104 char mc_replay_mode = FALSE;
 105 double *mc_time = NULL;
 106 __thread mc_comparison_times_t mc_comp_times = NULL;
 107 __thread double mc_snapshot_comparison_time;
 108 mc_stats_t mc_stats = NULL;
 109
 110 /* Safety */
 111 xbt_fifo_t mc_stack_safety = NULL;
 112 mc_global_t initial_state_safety = NULL;
 113
 114 /* Liveness */
 115 xbt_fifo_t mc_stack_liveness = NULL;
 116 mc_global_t initial_state_liveness = NULL;
 117 int compare;
 118
 119 xbt_automaton_t _mc_property_automaton = NULL;
 120
 121 /* Variables */
 122 mc_object_info_t mc_libsimgrid_info = NULL;
 123 mc_object_info_t mc_binary_info = NULL;
 124
 125 /* Ignore mechanism */
 126 extern xbt_dynar_t mc_heap_comparison_ignore;
 127 extern xbt_dynar_t stacks_areas;
 128
 129 /* Dot output */
 130 FILE *dot_output = NULL;
 131 const char* colors[13];
 132
 133
 134 /*******************************  DWARF Information *******************************/
 135 /**********************************************************************************/
 136
 137 /************************** Free functions *************************/
 138
 139 static void dw_location_free(dw_location_t l){
 140   if(l){
 141     if(l->type == e_dw_loclist)
 142       xbt_dynar_free(&(l->location.loclist));
 143     else if(l->type == e_dw_compose)
 144       xbt_dynar_free(&(l->location.compose));
 145     else if(l->type == e_dw_arithmetic)
 146       xbt_free(l->location.arithmetic);
 147
 148     xbt_free(l);
 149   }
 150 }
 151
 152 static void dw_location_entry_free(dw_location_entry_t e){
 153   dw_location_free(e->location);
 154   xbt_free(e);
 155 }
 156
 157 void dw_type_free(dw_type_t t){
 158   xbt_free(t->name);
 159   xbt_free(t->dw_type_id);
 160   xbt_dynar_free(&(t->members));
 161   xbt_free(t);
 162 }
 163
 164 static void dw_type_free_voidp(void *t){
 165   dw_type_free((dw_type_t) * (void **) t);
 166 }
 167
 168 void dw_variable_free(dw_variable_t v){
 169   if(v){
 170     xbt_free(v->name);
 171     xbt_free(v->type_origin);
 172     if(!v->global)
 173       dw_location_free(v->location);
 174     xbt_free(v);
 175   }
 176 }
 177
 178 void dw_variable_free_voidp(void *t){
 179   dw_variable_free((dw_variable_t) * (void **) t);
 180 }
 181
 182 // ***** object_info
 183
 184 mc_object_info_t MC_new_object_info(void) {
 185   mc_object_info_t res = xbt_new0(s_mc_object_info_t, 1);
 186   res->subprograms = xbt_dynar_new(sizeof(dw_frame_t), NULL);
 187   res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
 188   res->types = xbt_dict_new_homogeneous(NULL);
 189   res->types_by_name = xbt_dict_new_homogeneous(NULL);
 190   return res;
 191 }
 192
 193 void MC_free_object_info(mc_object_info_t* info) {
 194   xbt_free(&(*info)->file_name);
 195   xbt_dynar_free(&(*info)->subprograms);
 196   xbt_dynar_free(&(*info)->global_variables);
 197   xbt_dict_free(&(*info)->types);
 198   xbt_dict_free(&(*info)->types_by_name);
 199   xbt_free(info);
 200   xbt_dynar_free(&(*info)->functions_index);
 201   *info = NULL;
 202 }
 203
 204 // ***** Helpers
 205
 206 void* MC_object_base_address(mc_object_info_t info) {
 207   void* result = info->start_exec;
 208   if(info->start_rw!=NULL && result > (void*) info->start_rw) result = info->start_rw;
 209   if(info->start_ro!=NULL && result > (void*) info->start_ro) result = info->start_ro;
 210   return result;
 211 }
 212
 213 // ***** Functions index
 214
 215 static int MC_compare_frame_index_items(mc_function_index_item_t a, mc_function_index_item_t b) {
 216   if(a->low_pc < b->low_pc)
 217     return -1;
 218   else if(a->low_pc == b->low_pc)
 219     return 0;
 220   else
 221     return 1;
 222 }
 223
 224 static void MC_make_functions_index(mc_object_info_t info) {
 225   xbt_dynar_t index = xbt_dynar_new(sizeof(s_mc_function_index_item_t), NULL);
 226
 227   // Populate the array:
 228   dw_frame_t frame = NULL;
 229   unsigned cursor = 0;
 230   xbt_dynar_foreach(info->subprograms, cursor, frame) {
 231     if(frame->low_pc==NULL)
 232       continue;
 233     s_mc_function_index_item_t entry;
 234     entry.low_pc = frame->low_pc;
 235     entry.high_pc = frame->high_pc;
 236     entry.function = frame;
 237     xbt_dynar_push(index, &entry);
 238   }
 239
 240   mc_function_index_item_t base = (mc_function_index_item_t) xbt_dynar_get_ptr(index, 0);
 241
 242   // Sort the array by low_pc:
 243   qsort(base,
 244     xbt_dynar_length(index),
 245     sizeof(s_mc_function_index_item_t),
 246     (int (*)(const void *, const void *))MC_compare_frame_index_items);
 247
 248   info->functions_index = index;
 249 }
 250
 251 mc_object_info_t MC_ip_find_object_info(void* ip) {
 252   mc_object_info_t infos[2] = { mc_binary_info, mc_libsimgrid_info };
 253   size_t n = 2;
 254   size_t i;
 255   for(i=0; i!=n; ++i) {
 256     if(ip >= (void*)infos[i]->start_exec && ip <= (void*)infos[i]->end_exec) {
 257       return infos[i];
 258     }
 259   }
 260   return NULL;
 261 }
 262
 263 static dw_frame_t MC_find_function_by_ip_and_object(void* ip, mc_object_info_t info) {
 264   xbt_dynar_t dynar = info->functions_index;
 265   mc_function_index_item_t base = (mc_function_index_item_t) xbt_dynar_get_ptr(dynar, 0);
 266   int i = 0;
 267   int j = xbt_dynar_length(dynar) - 1;
 268   while(j>=i) {
 269     int k = i + ((j-i)/2);
 270     if(ip < base[k].low_pc) {
 271       j = k-1;
 272     } else if(ip > base[k].high_pc) {
 273       i = k+1;
 274     } else {
 275       return base[k].function;
 276     }
 277   }
 278   return NULL;
 279 }
 280
 281 dw_frame_t MC_find_function_by_ip(void* ip) {
 282   mc_object_info_t info = MC_ip_find_object_info(ip);
 283   if(info==NULL)
 284     return NULL;
 285   else
 286     return MC_find_function_by_ip_and_object(ip, info);
 287 }
 288
 289 static void MC_post_process_variables(mc_object_info_t info) {
 290   unsigned cursor = 0;
 291   dw_variable_t variable = NULL;
 292   xbt_dynar_foreach(info->global_variables, cursor, variable) {
 293     if(variable->type_origin) {
 294       variable->type = xbt_dict_get_or_null(info->types, variable->type_origin);
 295     }
 296   }
 297 }
 298
 299 static void MC_post_process_functions(mc_object_info_t info) {
 300   unsigned cursor = 0;
 301   dw_frame_t function = NULL;
 302   xbt_dynar_foreach(info->subprograms, cursor, function) {
 303     unsigned cursor2 = 0;
 304     dw_variable_t variable = NULL;
 305     xbt_dynar_foreach(function->variables, cursor2, variable) {
 306       if(variable->type_origin) {
 307         variable->type = xbt_dict_get_or_null(info->types, variable->type_origin);
 308       }
 309     }
 310   }
 311 }
 312
 313 /** \brief Finds informations about a given shared object/executable */
 314 mc_object_info_t MC_find_object_info(memory_map_t maps, char* name, int executable) {
 315   mc_object_info_t result = MC_new_object_info();
 316   if(executable)
 317     result->flags |= MC_OBJECT_INFO_EXECUTABLE;
 318   result->file_name = xbt_strdup(name);
 319   MC_find_object_address(maps, result);
 320   MC_dwarf_get_variables(result);
 321   MC_post_process_types(result);
 322   MC_post_process_variables(result);
 323   MC_post_process_functions(result);
 324   MC_make_functions_index(result);
 325   return result;
 326 }
 327
 328 /*************************************************************************/
 329
 330 static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr){
 331
 332   dw_location_t loc = xbt_new0(s_dw_location_t, 1);
 333
 334   if(location_list != NULL){
 335
 336     char *key = bprintf("%d", (int)strtoul(expr, NULL, 16));
 337     loc->type = e_dw_loclist;
 338     loc->location.loclist =  (xbt_dynar_t)xbt_dict_get_or_null(location_list, key);
 339     if(loc->location.loclist == NULL)
 340       XBT_INFO("Key not found in loclist");
 341     xbt_free(key);
 342     return loc;
 343
 344   }else{
 345
 346     int cursor = 0;
 347     char *tok = NULL, *tok2 = NULL;
 348
 349     xbt_dynar_t tokens1 = xbt_str_split(expr, ";");
 350     xbt_dynar_t tokens2;
 351
 352     loc->type = e_dw_compose;
 353     loc->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL);
 354
 355     while(cursor < xbt_dynar_length(tokens1)){
 356
 357       tok = xbt_dynar_get_as(tokens1, cursor, char*);
 358       tokens2 = xbt_str_split(tok, " ");
 359       tok2 = xbt_dynar_get_as(tokens2, 0, char*);
 360
 361       if(strncmp(tok2, "DW_OP_reg", 9) == 0){
 362         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 363         new_element->type = e_dw_register;
 364         new_element->location.reg = atoi(strtok(tok2, "DW_OP_reg"));
 365         xbt_dynar_push(loc->location.compose, &new_element);
 366       }else if(strcmp(tok2, "DW_OP_fbreg:") == 0){
 367         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 368         new_element->type = e_dw_fbregister_op;
 369         new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 370         xbt_dynar_push(loc->location.compose, &new_element);
 371       }else if(strncmp(tok2, "DW_OP_breg", 10) == 0){
 372         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 373         new_element->type = e_dw_bregister_op;
 374         new_element->location.breg_op.reg = atoi(strtok(tok2, "DW_OP_breg"));
 375         new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 376         xbt_dynar_push(loc->location.compose, &new_element);
 377       }else if(strncmp(tok2, "DW_OP_lit", 9) == 0){
 378         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 379         new_element->type = e_dw_lit;
 380         new_element->location.lit = atoi(strtok(tok2, "DW_OP_lit"));
 381         xbt_dynar_push(loc->location.compose, &new_element);
 382       }else if(strcmp(tok2, "DW_OP_piece:") == 0){
 383         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 384         new_element->type = e_dw_piece;
 385         new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 386         xbt_dynar_push(loc->location.compose, &new_element);
 387       }else if(strcmp(tok2, "DW_OP_plus_uconst:") == 0){
 388         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 389         new_element->type = e_dw_plus_uconst;
 390         new_element->location.plus_uconst = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char *));
 391         xbt_dynar_push(loc->location.compose, &new_element);
 392       }else if(strcmp(tok, "DW_OP_abs") == 0 ||
 393                strcmp(tok, "DW_OP_and") == 0 ||
 394                strcmp(tok, "DW_OP_div") == 0 ||
 395                strcmp(tok, "DW_OP_minus") == 0 ||
 396                strcmp(tok, "DW_OP_mod") == 0 ||
 397                strcmp(tok, "DW_OP_mul") == 0 ||
 398                strcmp(tok, "DW_OP_neg") == 0 ||
 399                strcmp(tok, "DW_OP_not") == 0 ||
 400                strcmp(tok, "DW_OP_or") == 0 ||
 401                strcmp(tok, "DW_OP_plus") == 0){
 402         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 403         new_element->type = e_dw_arithmetic;
 404         new_element->location.arithmetic = strdup(strtok(tok2, "DW_OP_"));
 405         xbt_dynar_push(loc->location.compose, &new_element);
 406       }else if(strcmp(tok, "DW_OP_stack_value") == 0){
 407       }else if(strcmp(tok2, "DW_OP_deref_size:") == 0){
 408         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 409         new_element->type = e_dw_deref;
 410         new_element->location.deref_size = (unsigned int short) atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 411         xbt_dynar_push(loc->location.compose, &new_element);
 412       }else if(strcmp(tok, "DW_OP_deref") == 0){
 413         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 414         new_element->type = e_dw_deref;
 415         new_element->location.deref_size = sizeof(void *);
 416         xbt_dynar_push(loc->location.compose, &new_element);
 417       }else if(strcmp(tok2, "DW_OP_constu:") == 0){
 418         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 419         new_element->type = e_dw_uconstant;
 420         new_element->location.uconstant.bytes = 1;
 421         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 422         xbt_dynar_push(loc->location.compose, &new_element);
 423       }else if(strcmp(tok2, "DW_OP_consts:") == 0){
 424         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 425         new_element->type = e_dw_sconstant;
 426         new_element->location.sconstant.bytes = 1;
 427         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 428         xbt_dynar_push(loc->location.compose, &new_element);
 429       }else if(strcmp(tok2, "DW_OP_const1u:") == 0 ||
 430                strcmp(tok2, "DW_OP_const2u:") == 0 ||
 431                strcmp(tok2, "DW_OP_const4u:") == 0 ||
 432                strcmp(tok2, "DW_OP_const8u:") == 0){
 433         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 434         new_element->type = e_dw_uconstant;
 435         new_element->location.uconstant.bytes = tok2[11] - '0';
 436         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 437         xbt_dynar_push(loc->location.compose, &new_element);
 438       }else if(strcmp(tok, "DW_OP_const1s") == 0 ||
 439                strcmp(tok, "DW_OP_const2s") == 0 ||
 440                strcmp(tok, "DW_OP_const4s") == 0 ||
 441                strcmp(tok, "DW_OP_const8s") == 0){
 442         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 443         new_element->type = e_dw_sconstant;
 444         new_element->location.sconstant.bytes = tok2[11] - '0';
 445         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 446         xbt_dynar_push(loc->location.compose, &new_element);
 447       }else{
 448         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 449         new_element->type = e_dw_unsupported;
 450         xbt_dynar_push(loc->location.compose, &new_element);
 451       }
 452
 453       cursor++;
 454       xbt_dynar_free(&tokens2);
 455
 456     }
 457
 458     xbt_dynar_free(&tokens1);
 459
 460     return loc;
 461
 462   }
 463
 464 }
 465
 466
 467 /** \brief Finds a frame (DW_TAG_subprogram) from an DWARF offset in the rangd of this subprogram
 468  *
 469  * The offset can be an offset of a child DW_TAG_variable.
 470  */
 471 static dw_frame_t MC_dwarf_get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset){
 472
 473   xbt_dict_cursor_t cursor = NULL;
 474   char *name;
 475   dw_frame_t res;
 476
 477   xbt_dict_foreach(all_variables, cursor, name, res) {
 478     if(offset >= res->start && offset < res->end){
 479       xbt_dict_cursor_free(&cursor);
 480       return res;
 481     }
 482   }
 483
 484   xbt_dict_cursor_free(&cursor);
 485   return NULL;
 486
 487 }
 488
 489 static dw_variable_t MC_dwarf_get_variable_by_name(dw_frame_t frame, char *var){
 490
 491   unsigned int cursor = 0;
 492   dw_variable_t current_var;
 493
 494   xbt_dynar_foreach(frame->variables, cursor, current_var){
 495     if(strcmp(var, current_var->name) == 0)
 496       return current_var;
 497   }
 498
 499   return NULL;
 500 }
 501
 502 static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *address){
 503
 504   if(xbt_dynar_is_empty(variables))
 505     return 0;
 506
 507   unsigned int cursor = 0;
 508   int start = 0;
 509   int end = xbt_dynar_length(variables) - 1;
 510   dw_variable_t var_test = NULL;
 511
 512   while(start <= end){
 513     cursor = (start + end) / 2;
 514     var_test = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t);
 515     if(strcmp(var_test->name, var) < 0){
 516       start = cursor + 1;
 517     }else if(strcmp(var_test->name, var) > 0){
 518       end = cursor - 1;
 519     }else{
 520       if(address){ /* global variable */
 521         if(var_test->address == address)
 522           return -1;
 523         if(var_test->address > address)
 524           end = cursor - 1;
 525         else
 526           start = cursor + 1;
 527       }else{ /* local variable */
 528         return -1;
 529       }
 530     }
 531   }
 532
 533   if(strcmp(var_test->name, var) == 0){
 534     if(address && var_test->address < address)
 535       return cursor+1;
 536     else
 537       return cursor;
 538   }else if(strcmp(var_test->name, var) < 0)
 539     return cursor+1;
 540   else
 541     return cursor;
 542
 543 }
 544
 545 void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t variable) {
 546   int index = MC_dwarf_get_variable_index(info->global_variables, variable->name, variable->address);
 547   if (index != -1)
 548     xbt_dynar_insert_at(info->global_variables, index, &variable);
 549   // TODO, else ?
 550 }
 551
 552 void MC_dwarf_register_non_global_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable) {
 553   xbt_assert(frame, "Frame is NULL");
 554   int index = MC_dwarf_get_variable_index(frame->variables, variable->name, NULL);
 555   if (index != -1)
 556     xbt_dynar_insert_at(frame->variables, index, &variable);
 557   // TODO, else ?
 558 }
 559
 560 void MC_dwarf_register_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable) {
 561   if(variable->global)
 562     MC_dwarf_register_global_variable(info, variable);
 563   else if(frame==NULL)
 564     xbt_die("No frame for this local variable");
 565   else
 566     MC_dwarf_register_non_global_variable(info, frame, variable);
 567 }
 568
 569
 570 /*******************************  Ignore mechanism *******************************/
 571 /*********************************************************************************/
 572
 573 xbt_dynar_t mc_checkpoint_ignore;
 574
 575 typedef struct s_mc_stack_ignore_variable{
 576   char *var_name;
 577   char *frame;
 578 }s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
 579
 580 /**************************** Free functions ******************************/
 581
 582 static void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
 583   xbt_free(v->var_name);
 584   xbt_free(v->frame);
 585   xbt_free(v);
 586 }
 587
 588 static void stack_ignore_variable_free_voidp(void *v){
 589   stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
 590 }
 591
 592 void heap_ignore_region_free(mc_heap_ignore_region_t r){
 593   xbt_free(r);
 594 }
 595
 596 void heap_ignore_region_free_voidp(void *r){
 597   heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
 598 }
 599
 600 static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r){
 601   xbt_free(r);
 602 }
 603
 604 static void checkpoint_ignore_region_free_voidp(void *r){
 605   checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
 606 }
 607
 608 /***********************************************************************/
 609
 610 void MC_ignore_heap(void *address, size_t size){
 611
 612   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 613
 614   MC_SET_RAW_MEM;
 615
 616   mc_heap_ignore_region_t region = NULL;
 617   region = xbt_new0(s_mc_heap_ignore_region_t, 1);
 618   region->address = address;
 619   region->size = size;
 620
 621   region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
 622
 623   if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
 624     region->fragment = -1;
 625     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
 626   }else{
 627     region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
 628     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
 629   }
 630
 631   if(mc_heap_comparison_ignore == NULL){
 632     mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
 633     xbt_dynar_push(mc_heap_comparison_ignore, &region);
 634     if(!raw_mem_set)
 635       MC_UNSET_RAW_MEM;
 636     return;
 637   }
 638
 639   unsigned int cursor = 0;
 640   mc_heap_ignore_region_t current_region = NULL;
 641   int start = 0;
 642   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
 643
 644   while(start <= end){
 645     cursor = (start + end) / 2;
 646     current_region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
 647     if(current_region->address == address){
 648       heap_ignore_region_free(region);
 649       if(!raw_mem_set)
 650         MC_UNSET_RAW_MEM;
 651       return;
 652     }else if(current_region->address < address){
 653       start = cursor + 1;
 654     }else{
 655       end = cursor - 1;
 656     }
 657   }
 658
 659   if(current_region->address < address)
 660     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
 661   else
 662     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
 663
 664   if(!raw_mem_set)
 665     MC_UNSET_RAW_MEM;
 666 }
 667
 668 void MC_remove_ignore_heap(void *address, size_t size){
 669
 670   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 671
 672   MC_SET_RAW_MEM;
 673
 674   unsigned int cursor = 0;
 675   int start = 0;
 676   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
 677   mc_heap_ignore_region_t region;
 678   int ignore_found = 0;
 679
 680   while(start <= end){
 681     cursor = (start + end) / 2;
 682     region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
 683     if(region->address == address){
 684       ignore_found = 1;
 685       break;
 686     }else if(region->address < address){
 687       start = cursor + 1;
 688     }else{
 689       if((char * )region->address <= ((char *)address + size)){
 690         ignore_found = 1;
 691         break;
 692       }else{
 693         end = cursor - 1;
 694       }
 695     }
 696   }
 697
 698   if(ignore_found == 1){
 699     xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
 700     MC_remove_ignore_heap(address, size);
 701   }
 702
 703   if(!raw_mem_set)
 704     MC_UNSET_RAW_MEM;
 705
 706 }
 707
 708 void MC_ignore_global_variable(const char *name){
 709
 710   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 711
 712   MC_SET_RAW_MEM;
 713
 714   xbt_assert(mc_libsimgrid_info, "MC subsystem not initialized");
 715
 716     unsigned int cursor = 0;
 717     dw_variable_t current_var;
 718     int start = 0;
 719     int end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
 720
 721     while(start <= end){
 722       cursor = (start + end) /2;
 723       current_var = (dw_variable_t)xbt_dynar_get_as(mc_libsimgrid_info->global_variables, cursor, dw_variable_t);
 724       if(strcmp(current_var->name, name) == 0){
 725         xbt_dynar_remove_at(mc_libsimgrid_info->global_variables, cursor, NULL);
 726         start = 0;
 727         end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
 728       }else if(strcmp(current_var->name, name) < 0){
 729         start = cursor + 1;
 730       }else{
 731         end = cursor - 1;
 732       }
 733     }
 734
 735   if(!raw_mem_set)
 736     MC_UNSET_RAW_MEM;
 737 }
 738
 739 static void MC_ignore_local_variable_in_object(const char *var_name, const char *frame_name, mc_object_info_t info) {
 740   unsigned cursor2;
 741   dw_frame_t frame;
 742   int start, end;
 743   int cursor = 0;
 744   dw_variable_t current_var;
 745
 746   xbt_dynar_foreach(info->subprograms, cursor2, frame) {
 747
 748     if(frame_name && strcmp(frame_name, frame->name))
 749       continue;
 750
 751     start = 0;
 752     end = xbt_dynar_length(frame->variables) - 1;
 753     while(start <= end){
 754       cursor = (start + end) / 2;
 755       current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
 756
 757       int compare = strcmp(current_var->name, var_name);
 758       if(compare == 0){
 759         xbt_dynar_remove_at(frame->variables, cursor, NULL);
 760         start = 0;
 761         end = xbt_dynar_length(frame->variables) - 1;
 762       }else if(compare < 0){
 763         start = cursor + 1;
 764       }else{
 765         end = cursor - 1;
 766       }
 767     }
 768   }
 769 }
 770
 771 void MC_ignore_local_variable(const char *var_name, const char *frame_name){
 772
 773   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 774
 775   if(strcmp(frame_name, "*") == 0)
 776     frame_name = NULL;
 777
 778   MC_SET_RAW_MEM;
 779
 780   MC_ignore_local_variable_in_object(var_name, frame_name, mc_libsimgrid_info);
 781   if(frame_name!=NULL)
 782     MC_ignore_local_variable_in_object(var_name, frame_name, mc_binary_info);
 783
 784   if(!raw_mem_set)
 785     MC_UNSET_RAW_MEM;
 786
 787 }
 788
 789 void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
 790
 791   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 792
 793   MC_SET_RAW_MEM;
 794
 795   if(stacks_areas == NULL)
 796     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
 797
 798   stack_region_t region = NULL;
 799   region = xbt_new0(s_stack_region_t, 1);
 800   region->address = stack;
 801   region->process_name = strdup(name);
 802   region->context = context;
 803   region->size = size;
 804   region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
 805   xbt_dynar_push(stacks_areas, &region);
 806
 807   if(!raw_mem_set)
 808     MC_UNSET_RAW_MEM;
 809 }
 810
 811 void MC_ignore(void *addr, size_t size){
 812
 813   int raw_mem_set= (mmalloc_get_current_heap() == raw_heap);
 814
 815   MC_SET_RAW_MEM;
 816
 817   if(mc_checkpoint_ignore == NULL)
 818     mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp);
 819
 820   mc_checkpoint_ignore_region_t region = xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
 821   region->addr = addr;
 822   region->size = size;
 823
 824   if(xbt_dynar_is_empty(mc_checkpoint_ignore)){
 825     xbt_dynar_push(mc_checkpoint_ignore, &region);
 826   }else{
 827
 828     unsigned int cursor = 0;
 829     int start = 0;
 830     int end = xbt_dynar_length(mc_checkpoint_ignore) -1;
 831     mc_checkpoint_ignore_region_t current_region = NULL;
 832
 833     while(start <= end){
 834       cursor = (start + end) / 2;
 835       current_region = (mc_checkpoint_ignore_region_t)xbt_dynar_get_as(mc_checkpoint_ignore, cursor, mc_checkpoint_ignore_region_t);
 836       if(current_region->addr == addr){
 837         if(current_region->size == size){
 838           checkpoint_ignore_region_free(region);
 839           if(!raw_mem_set)
 840             MC_UNSET_RAW_MEM;
 841           return;
 842         }else if(current_region->size < size){
 843           start = cursor + 1;
 844         }else{
 845           end = cursor - 1;
 846         }
 847       }else if(current_region->addr < addr){
 848           start = cursor + 1;
 849       }else{
 850         end = cursor - 1;
 851       }
 852     }
 853
 854      if(current_region->addr == addr){
 855        if(current_region->size < size){
 856         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
 857       }else{
 858         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
 859       }
 860     }else if(current_region->addr < addr){
 861        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
 862     }else{
 863        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
 864     }
 865   }
 866
 867   if(!raw_mem_set)
 868     MC_UNSET_RAW_MEM;
 869 }
 870
 871 /*******************************  Initialisation of MC *******************************/
 872 /*********************************************************************************/
 873
 874 static void MC_post_process_object_info(mc_object_info_t info) {
 875   mc_object_info_t other_info = info == mc_binary_info ? mc_libsimgrid_info : mc_binary_info;
 876   xbt_dict_cursor_t cursor = NULL;
 877   char* key = NULL;
 878   dw_type_t type = NULL;
 879   xbt_dict_foreach(info->types, cursor, key, type){
 880     if(type->name && type->byte_size == 0) {
 881       type->other_object_same_type = xbt_dict_get_or_null(other_info->types_by_name, type->name);
 882     }
 883   }
 884 }
 885
 886 static void MC_init_debug_info(void) {
 887   XBT_INFO("Get debug information ...");
 888
 889   memory_map_t maps = MC_get_memory_map();
 890
 891   /* Get local variables for state equality detection */
 892   mc_binary_info = MC_find_object_info(maps, xbt_binary_name, 1);
 893   mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path, 0);
 894
 895   // Use information of the other objects:
 896   MC_post_process_object_info(mc_binary_info);
 897   MC_post_process_object_info(mc_libsimgrid_info);
 898
 899   MC_free_memory_map(maps);
 900   XBT_INFO("Get debug information done !");
 901 }
 902
 903 void MC_init(){
 904
 905   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 906
 907   compare = 0;
 908
 909   /* Initialize the data structures that must be persistent across every
 910      iteration of the model-checker (in RAW memory) */
 911
 912   MC_SET_RAW_MEM;
 913
 914   MC_init_memory_map_info();
 915   MC_init_debug_info();
 916
 917    /* Init parmap */
 918   parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
 919
 920   MC_UNSET_RAW_MEM;
 921
 922    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
 923   MC_ignore_local_variable("e", "*");
 924   MC_ignore_local_variable("__ex_cleanup", "*");
 925   MC_ignore_local_variable("__ex_mctx_en", "*");
 926   MC_ignore_local_variable("__ex_mctx_me", "*");
 927   MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
 928   MC_ignore_local_variable("_log_ev", "*");
 929   MC_ignore_local_variable("_throw_ctx", "*");
 930   MC_ignore_local_variable("ctx", "*");
 931
 932   MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
 933   MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
 934   MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
 935
 936   /* Ignore local variable about time used for tracing */
 937   MC_ignore_local_variable("start_time", "*");
 938
 939   MC_ignore_global_variable("compared_pointers");
 940   MC_ignore_global_variable("mc_comp_times");
 941   MC_ignore_global_variable("mc_snapshot_comparison_time");
 942   MC_ignore_global_variable("mc_time");
 943   MC_ignore_global_variable("smpi_current_rank");
 944   MC_ignore_global_variable("counter"); /* Static variable used for tracing */
 945   MC_ignore_global_variable("maestro_stack_start");
 946   MC_ignore_global_variable("maestro_stack_end");
 947   MC_ignore_global_variable("smx_total_comms");
 948
 949   MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run));
 950   MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran));
 951   MC_ignore_heap(simix_global->process_to_run, sizeof(*(simix_global->process_to_run)));
 952   MC_ignore_heap(simix_global->process_that_ran, sizeof(*(simix_global->process_that_ran)));
 953
 954   smx_process_t process;
 955   xbt_swag_foreach(process, simix_global->process_list){
 956     MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
 957   }
 958
 959   if(raw_mem_set)
 960     MC_SET_RAW_MEM;
 961
 962 }
 963
 964 static void MC_init_dot_output(){ /* FIXME : more colors */
 965
 966   colors[0] = "blue";
 967   colors[1] = "red";
 968   colors[2] = "green3";
 969   colors[3] = "goldenrod";
 970   colors[4] = "brown";
 971   colors[5] = "purple";
 972   colors[6] = "magenta";
 973   colors[7] = "turquoise4";
 974   colors[8] = "gray25";
 975   colors[9] = "forestgreen";
 976   colors[10] = "hotpink";
 977   colors[11] = "lightblue";
 978   colors[12] = "tan";
 979
 980   dot_output = fopen(_sg_mc_dot_output_file, "w");
 981
 982   if(dot_output == NULL){
 983     perror("Error open dot output file");
 984     xbt_abort();
 985   }
 986
 987   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");
 988
 989 }
 990
 991 /*******************************  Core of MC *******************************/
 992 /**************************************************************************/
 993
 994 void MC_do_the_modelcheck_for_real() {
 995
 996   MC_SET_RAW_MEM;
 997   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
 998   MC_UNSET_RAW_MEM;
 999
1000   if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
1001     if (mc_reduce_kind==e_mc_reduce_unset)
1002       mc_reduce_kind=e_mc_reduce_dpor;
1003
1004     XBT_INFO("Check a safety property");
1005     MC_modelcheck_safety();
1006
1007   } else  {
1008
1009     if (mc_reduce_kind==e_mc_reduce_unset)
1010       mc_reduce_kind=e_mc_reduce_none;
1011
1012     XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
1013     MC_automaton_load(_sg_mc_property_file);
1014     MC_modelcheck_liveness();
1015   }
1016 }
1017
1018 void MC_modelcheck_safety(void)
1019 {
1020   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1021
1022   /* Check if MC is already initialized */
1023   if (initial_state_safety)
1024     return;
1025
1026   mc_time = xbt_new0(double, simix_process_maxpid);
1027
1028   /* mc_time refers to clock for each process -> ignore it for heap comparison */
1029   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1030
1031   /* Initialize the data structures that must be persistent across every
1032      iteration of the model-checker (in RAW memory) */
1033
1034   MC_SET_RAW_MEM;
1035
1036   /* Initialize statistics */
1037   mc_stats = xbt_new0(s_mc_stats_t, 1);
1038   mc_stats->state_size = 1;
1039
1040   /* Create exploration stack */
1041   mc_stack_safety = xbt_fifo_new();
1042
1043   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1044     MC_init_dot_output();
1045
1046   MC_UNSET_RAW_MEM;
1047
1048   if(_sg_mc_visited > 0){
1049     MC_init();
1050   }else{
1051     MC_SET_RAW_MEM;
1052     MC_init_memory_map_info();
1053     MC_init_debug_info();
1054     MC_UNSET_RAW_MEM;
1055   }
1056
1057   MC_dpor_init();
1058
1059   MC_SET_RAW_MEM;
1060   /* Save the initial state */
1061   initial_state_safety = xbt_new0(s_mc_global_t, 1);
1062   initial_state_safety->snapshot = MC_take_snapshot(0);
1063   initial_state_safety->initial_communications_pattern_done = 0;
1064   initial_state_safety->comm_deterministic = 1;
1065   initial_state_safety->send_deterministic = 1;
1066   MC_UNSET_RAW_MEM;
1067
1068   MC_dpor();
1069
1070   if(raw_mem_set)
1071     MC_SET_RAW_MEM;
1072
1073   xbt_abort();
1074   //MC_exit();
1075 }
1076
1077 void MC_modelcheck_liveness(){
1078
1079   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1080
1081   MC_init();
1082
1083   mc_time = xbt_new0(double, simix_process_maxpid);
1084
1085   /* mc_time refers to clock for each process -> ignore it for heap comparison */
1086   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1087
1088   MC_SET_RAW_MEM;
1089
1090   /* Initialize statistics */
1091   mc_stats = xbt_new0(s_mc_stats_t, 1);
1092   mc_stats->state_size = 1;
1093
1094   /* Create exploration stack */
1095   mc_stack_liveness = xbt_fifo_new();
1096
1097   /* Create the initial state */
1098   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
1099
1100   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1101     MC_init_dot_output();
1102
1103   MC_UNSET_RAW_MEM;
1104
1105   MC_ddfs_init();
1106
1107   /* We're done */
1108   MC_print_statistics(mc_stats);
1109   xbt_free(mc_time);
1110
1111   if(raw_mem_set)
1112     MC_SET_RAW_MEM;
1113
1114 }
1115
1116
1117 void MC_exit(void)
1118 {
1119   xbt_free(mc_time);
1120
1121   MC_memory_exit();
1122   //xbt_abort();
1123 }
1124
1125 int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
1126
1127   return simcall->mc_value;
1128 }
1129
1130
1131 int MC_random(int min, int max)
1132 {
1133   /*FIXME: return mc_current_state->executed_transition->random.value;*/
1134   return simcall_mc_random(min, max);
1135 }
1136
1137 /**
1138  * \brief Schedules all the process that are ready to run
1139  */
1140 void MC_wait_for_requests(void)
1141 {
1142   smx_process_t process;
1143   smx_simcall_t req;
1144   unsigned int iter;
1145
1146   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
1147     SIMIX_process_runall();
1148     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
1149       req = &process->simcall;
1150       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
1151         SIMIX_simcall_pre(req, 0);
1152     }
1153   }
1154 }
1155
1156 int MC_deadlock_check()
1157 {
1158   int deadlock = FALSE;
1159   smx_process_t process;
1160   if(xbt_swag_size(simix_global->process_list)){
1161     deadlock = TRUE;
1162     xbt_swag_foreach(process, simix_global->process_list){
1163       if(process->simcall.call != SIMCALL_NONE
1164          && MC_request_is_enabled(&process->simcall)){
1165         deadlock = FALSE;
1166         break;
1167       }
1168     }
1169   }
1170   return deadlock;
1171 }
1172
1173 /**
1174  * \brief Re-executes from the state at position start all the transitions indicated by
1175  *        a given model-checker stack.
1176  * \param stack The stack with the transitions to execute.
1177  * \param start Start index to begin the re-execution.
1178  */
1179 void MC_replay(xbt_fifo_t stack, int start)
1180 {
1181   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
1182
1183   int value, i = 1, count = 1;
1184   char *req_str;
1185   smx_simcall_t req = NULL, saved_req = NULL;
1186   xbt_fifo_item_t item, start_item;
1187   mc_state_t state;
1188   smx_process_t process = NULL;
1189   int comm_pattern = 0;
1190
1191   XBT_DEBUG("**** Begin Replay ****");
1192
1193   if(start == -1){
1194     /* Restore the initial state */
1195     MC_restore_snapshot(initial_state_safety->snapshot);
1196     /* At the moment of taking the snapshot the raw heap was set, so restoring
1197      * it will set it back again, we have to unset it to continue  */
1198     MC_UNSET_RAW_MEM;
1199   }
1200
1201   start_item = xbt_fifo_get_last_item(stack);
1202   if(start != -1){
1203     while (i != start){
1204       start_item = xbt_fifo_get_prev_item(start_item);
1205       i++;
1206     }
1207   }
1208
1209   MC_SET_RAW_MEM;
1210   xbt_dict_reset(first_enabled_state);
1211   xbt_swag_foreach(process, simix_global->process_list){
1212     if(MC_process_is_enabled(process)){
1213       char *key = bprintf("%lu", process->pid);
1214       char *data = bprintf("%d", count);
1215       xbt_dict_set(first_enabled_state, key, data, NULL);
1216       xbt_free(key);
1217     }
1218   }
1219   xbt_dynar_reset(communications_pattern);
1220   MC_UNSET_RAW_MEM;
1221
1222
1223   /* Traverse the stack from the state at position start and re-execute the transitions */
1224   for (item = start_item;
1225        item != xbt_fifo_get_first_item(stack);
1226        item = xbt_fifo_get_prev_item(item)) {
1227
1228     state = (mc_state_t) xbt_fifo_get_item_content(item);
1229     saved_req = MC_state_get_executed_request(state, &value);
1230
1231     MC_SET_RAW_MEM;
1232     char *key = bprintf("%lu", saved_req->issuer->pid);
1233     xbt_dict_remove(first_enabled_state, key);
1234     xbt_free(key);
1235     MC_UNSET_RAW_MEM;
1236
1237     if(saved_req){
1238       /* because we got a copy of the executed request, we have to fetch the
1239          real one, pointed by the request field of the issuer process */
1240       req = &saved_req->issuer->simcall;
1241
1242       /* Debug information */
1243       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1244         req_str = MC_request_to_string(req, value);
1245         XBT_DEBUG("Replay: %s (%p)", req_str, state);
1246         xbt_free(req_str);
1247       }
1248     }
1249
1250     if(req->call == SIMCALL_COMM_ISEND)
1251       comm_pattern = 1;
1252     else if(req->call == SIMCALL_COMM_IRECV)
1253       comm_pattern = 2;
1254
1255     SIMIX_simcall_pre(req, value);
1256
1257     MC_SET_RAW_MEM;
1258     if(comm_pattern != 0){
1259       get_comm_pattern(communications_pattern, req, comm_pattern);
1260     }
1261     MC_UNSET_RAW_MEM;
1262
1263     comm_pattern = 0;
1264
1265     MC_wait_for_requests();
1266
1267     count++;
1268
1269     MC_SET_RAW_MEM;
1270     /* Insert in dict all enabled processes */
1271     xbt_swag_foreach(process, simix_global->process_list){
1272       if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
1273         char *key = bprintf("%lu", process->pid);
1274         if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
1275           char *data = bprintf("%d", count);
1276           xbt_dict_set(first_enabled_state, key, data, NULL);
1277         }
1278         xbt_free(key);
1279       }
1280     }
1281     MC_UNSET_RAW_MEM;
1282
1283     /* Update statistics */
1284     mc_stats->visited_states++;
1285     mc_stats->executed_transitions++;
1286
1287   }
1288
1289   XBT_DEBUG("**** End Replay ****");
1290
1291   if(raw_mem)
1292     MC_SET_RAW_MEM;
1293   else
1294     MC_UNSET_RAW_MEM;
1295
1296
1297 }
1298
1299 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
1300 {
1301
1302   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1303
1304   int value;
1305   char *req_str;
1306   smx_simcall_t req = NULL, saved_req = NULL;
1307   xbt_fifo_item_t item;
1308   mc_state_t state;
1309   mc_pair_t pair;
1310   int depth = 1;
1311
1312   XBT_DEBUG("**** Begin Replay ****");
1313
1314   /* Restore the initial state */
1315   MC_restore_snapshot(initial_state_liveness->snapshot);
1316
1317   /* At the moment of taking the snapshot the raw heap was set, so restoring
1318    * it will set it back again, we have to unset it to continue  */
1319   if(!initial_state_liveness->raw_mem_set)
1320     MC_UNSET_RAW_MEM;
1321
1322   if(all_stack){
1323
1324     item = xbt_fifo_get_last_item(stack);
1325
1326     while(depth <= xbt_fifo_size(stack)){
1327
1328       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
1329       state = (mc_state_t) pair->graph_state;
1330
1331       if(pair->requests > 0){
1332
1333         saved_req = MC_state_get_executed_request(state, &value);
1334         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
1335
1336         if(saved_req != NULL){
1337           /* because we got a copy of the executed request, we have to fetch the
1338              real one, pointed by the request field of the issuer process */
1339           req = &saved_req->issuer->simcall;
1340           //XBT_DEBUG("Req->call %u", req->call);
1341
1342           /* Debug information */
1343           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1344             req_str = MC_request_to_string(req, value);
1345             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
1346             xbt_free(req_str);
1347           }
1348
1349         }
1350
1351         SIMIX_simcall_pre(req, value);
1352         MC_wait_for_requests();
1353       }
1354
1355       depth++;
1356
1357       /* Update statistics */
1358       mc_stats->visited_pairs++;
1359       mc_stats->executed_transitions++;
1360
1361       item = xbt_fifo_get_prev_item(item);
1362     }
1363
1364   }else{
1365
1366     /* Traverse the stack from the initial state and re-execute the transitions */
1367     for (item = xbt_fifo_get_last_item(stack);
1368          item != xbt_fifo_get_first_item(stack);
1369          item = xbt_fifo_get_prev_item(item)) {
1370
1371       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
1372       state = (mc_state_t) pair->graph_state;
1373
1374       if(pair->requests > 0){
1375
1376         saved_req = MC_state_get_executed_request(state, &value);
1377         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
1378
1379         if(saved_req != NULL){
1380           /* because we got a copy of the executed request, we have to fetch the
1381              real one, pointed by the request field of the issuer process */
1382           req = &saved_req->issuer->simcall;
1383           //XBT_DEBUG("Req->call %u", req->call);
1384
1385           /* Debug information */
1386           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1387             req_str = MC_request_to_string(req, value);
1388             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
1389             xbt_free(req_str);
1390           }
1391
1392         }
1393
1394         SIMIX_simcall_pre(req, value);
1395         MC_wait_for_requests();
1396       }
1397
1398       depth++;
1399
1400       /* Update statistics */
1401       mc_stats->visited_pairs++;
1402       mc_stats->executed_transitions++;
1403     }
1404   }
1405
1406   XBT_DEBUG("**** End Replay ****");
1407
1408   if(initial_state_liveness->raw_mem_set)
1409     MC_SET_RAW_MEM;
1410   else
1411     MC_UNSET_RAW_MEM;
1412
1413 }
1414
1415 /**
1416  * \brief Dumps the contents of a model-checker's stack and shows the actual
1417  *        execution trace
1418  * \param stack The stack to dump
1419  */
1420 void MC_dump_stack_safety(xbt_fifo_t stack)
1421 {
1422
1423   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1424
1425   MC_show_stack_safety(stack);
1426
1427   if(!_sg_mc_checkpoint){
1428
1429     mc_state_t state;
1430
1431     MC_SET_RAW_MEM;
1432     while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
1433       MC_state_delete(state);
1434     MC_UNSET_RAW_MEM;
1435
1436   }
1437
1438   if(raw_mem_set)
1439     MC_SET_RAW_MEM;
1440   else
1441     MC_UNSET_RAW_MEM;
1442
1443 }
1444
1445
1446 void MC_show_stack_safety(xbt_fifo_t stack)
1447 {
1448
1449   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1450
1451   MC_SET_RAW_MEM;
1452
1453   int value;
1454   mc_state_t state;
1455   xbt_fifo_item_t item;
1456   smx_simcall_t req;
1457   char *req_str = NULL;
1458
1459   for (item = xbt_fifo_get_last_item(stack);
1460        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
1461         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
1462     req = MC_state_get_executed_request(state, &value);
1463     if(req){
1464       req_str = MC_request_to_string(req, value);
1465       XBT_INFO("%s", req_str);
1466       xbt_free(req_str);
1467     }
1468   }
1469
1470   if(!raw_mem_set)
1471     MC_UNSET_RAW_MEM;
1472 }
1473
1474 void MC_show_deadlock(smx_simcall_t req)
1475 {
1476   /*char *req_str = NULL;*/
1477   XBT_INFO("**************************");
1478   XBT_INFO("*** DEAD-LOCK DETECTED ***");
1479   XBT_INFO("**************************");
1480   XBT_INFO("Locked request:");
1481   /*req_str = MC_request_to_string(req);
1482     XBT_INFO("%s", req_str);
1483     xbt_free(req_str);*/
1484   XBT_INFO("Counter-example execution trace:");
1485   MC_dump_stack_safety(mc_stack_safety);
1486   MC_print_statistics(mc_stats);
1487 }
1488
1489
1490 void MC_show_stack_liveness(xbt_fifo_t stack){
1491   int value;
1492   mc_pair_t pair;
1493   xbt_fifo_item_t item;
1494   smx_simcall_t req;
1495   char *req_str = NULL;
1496
1497   for (item = xbt_fifo_get_last_item(stack);
1498        (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
1499         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
1500     req = MC_state_get_executed_request(pair->graph_state, &value);
1501     if(req){
1502       if(pair->requests>0){
1503         req_str = MC_request_to_string(req, value);
1504         XBT_INFO("%s", req_str);
1505         xbt_free(req_str);
1506       }else{
1507         XBT_INFO("End of system requests but evolution in Büchi automaton");
1508       }
1509     }
1510   }
1511 }
1512
1513 void MC_dump_stack_liveness(xbt_fifo_t stack){
1514
1515   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1516
1517   mc_pair_t pair;
1518
1519   MC_SET_RAW_MEM;
1520   while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
1521     MC_pair_delete(pair);
1522   MC_UNSET_RAW_MEM;
1523
1524   if(raw_mem_set)
1525     MC_SET_RAW_MEM;
1526
1527 }
1528
1529
1530 void MC_print_statistics(mc_stats_t stats)
1531 {
1532   if(stats->expanded_pairs == 0){
1533     XBT_INFO("Expanded states = %lu", stats->expanded_states);
1534     XBT_INFO("Visited states = %lu", stats->visited_states);
1535   }else{
1536     XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
1537     XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
1538   }
1539   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
1540   MC_SET_RAW_MEM;
1541   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
1542     fprintf(dot_output, "}\n");
1543     fclose(dot_output);
1544   }
1545   if(initial_state_safety != NULL){
1546     // XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
1547     // XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
1548   }
1549   MC_UNSET_RAW_MEM;
1550 }
1551
1552 void MC_assert(int prop)
1553 {
1554   if (MC_is_active() && !prop){
1555     XBT_INFO("**************************");
1556     XBT_INFO("*** PROPERTY NOT VALID ***");
1557     XBT_INFO("**************************");
1558     XBT_INFO("Counter-example execution trace:");
1559     MC_dump_stack_safety(mc_stack_safety);
1560     MC_print_statistics(mc_stats);
1561     xbt_abort();
1562   }
1563 }
1564
1565 void MC_cut(void){
1566   user_max_depth_reached = 1;
1567 }
1568
1569 void MC_process_clock_add(smx_process_t process, double amount)
1570 {
1571   mc_time[process->pid] += amount;
1572 }
1573
1574 double MC_process_clock_get(smx_process_t process)
1575 {
1576   if(mc_time){
1577     if(process != NULL)
1578       return mc_time[process->pid];
1579     else
1580       return -1;
1581   }else{
1582     return 0;
1583   }
1584 }
1585
1586 void MC_automaton_load(const char *file){
1587
1588   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1589
1590   MC_SET_RAW_MEM;
1591
1592   if (_mc_property_automaton == NULL)
1593     _mc_property_automaton = xbt_automaton_new();
1594
1595   xbt_automaton_load(_mc_property_automaton,file);
1596
1597   MC_UNSET_RAW_MEM;
1598
1599   if(raw_mem_set)
1600     MC_SET_RAW_MEM;
1601
1602 }
1603
1604 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
1605
1606   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1607
1608   MC_SET_RAW_MEM;
1609
1610   if (_mc_property_automaton == NULL)
1611     _mc_property_automaton = xbt_automaton_new();
1612
1613   xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
1614
1615   MC_UNSET_RAW_MEM;
1616
1617   if(raw_mem_set)
1618     MC_SET_RAW_MEM;
1619
1620 }
1621
1622
1623