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