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