src/mc/mc_global.c

   1 /* Copyright (c) 2008-2014. 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("%lu", 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 /** \brief Finds a frame (DW_TAG_subprogram) from an DWARF offset in the rangd of this subprogram
 478  *
 479  * The offset can be an offset of a child DW_TAG_variable.
 480  */
 481 static dw_frame_t MC_dwarf_get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset){
 482
 483   xbt_dict_cursor_t cursor = NULL;
 484   char *name;
 485   dw_frame_t res;
 486
 487   xbt_dict_foreach(all_variables, cursor, name, res) {
 488     if(offset >= res->start && offset < res->end){
 489       xbt_dict_cursor_free(&cursor);
 490       return res;
 491     }
 492   }
 493
 494   xbt_dict_cursor_free(&cursor);
 495   return NULL;
 496
 497 }
 498
 499 static dw_variable_t MC_dwarf_get_variable_by_name(dw_frame_t frame, char *var){
 500
 501   unsigned int cursor = 0;
 502   dw_variable_t current_var;
 503
 504   xbt_dynar_foreach(frame->variables, cursor, current_var){
 505     if(strcmp(var, current_var->name) == 0)
 506       return current_var;
 507   }
 508
 509   return NULL;
 510 }
 511
 512 static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *address){
 513
 514   if(xbt_dynar_is_empty(variables))
 515     return 0;
 516
 517   unsigned int cursor = 0;
 518   int start = 0;
 519   int end = xbt_dynar_length(variables) - 1;
 520   dw_variable_t var_test = NULL;
 521
 522   while(start <= end){
 523     cursor = (start + end) / 2;
 524     var_test = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t);
 525     if(strcmp(var_test->name, var) < 0){
 526       start = cursor + 1;
 527     }else if(strcmp(var_test->name, var) > 0){
 528       end = cursor - 1;
 529     }else{
 530       if(address){ /* global variable */
 531         if(var_test->address == address)
 532           return -1;
 533         if(var_test->address > address)
 534           end = cursor - 1;
 535         else
 536           start = cursor + 1;
 537       }else{ /* local variable */
 538         return -1;
 539       }
 540     }
 541   }
 542
 543   if(strcmp(var_test->name, var) == 0){
 544     if(address && var_test->address < address)
 545       return cursor+1;
 546     else
 547       return cursor;
 548   }else if(strcmp(var_test->name, var) < 0)
 549     return cursor+1;
 550   else
 551     return cursor;
 552
 553 }
 554
 555 void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t variable) {
 556   int index = MC_dwarf_get_variable_index(info->global_variables, variable->name, variable->address);
 557   if (index != -1)
 558     xbt_dynar_insert_at(info->global_variables, index, &variable);
 559   // TODO, else ?
 560 }
 561
 562 void MC_dwarf_register_non_global_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable) {
 563   xbt_assert(frame, "Frame is NULL");
 564   int index = MC_dwarf_get_variable_index(frame->variables, variable->name, NULL);
 565   if (index != -1)
 566     xbt_dynar_insert_at(frame->variables, index, &variable);
 567   // TODO, else ?
 568 }
 569
 570 void MC_dwarf_register_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable) {
 571   if(variable->global)
 572     MC_dwarf_register_global_variable(info, variable);
 573   else if(frame==NULL)
 574     xbt_die("No frame for this local variable");
 575   else
 576     MC_dwarf_register_non_global_variable(info, frame, variable);
 577 }
 578
 579
 580 /*******************************  Ignore mechanism *******************************/
 581 /*********************************************************************************/
 582
 583 xbt_dynar_t mc_checkpoint_ignore;
 584
 585 typedef struct s_mc_stack_ignore_variable{
 586   char *var_name;
 587   char *frame;
 588 }s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
 589
 590 /**************************** Free functions ******************************/
 591
 592 static void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
 593   xbt_free(v->var_name);
 594   xbt_free(v->frame);
 595   xbt_free(v);
 596 }
 597
 598 static void stack_ignore_variable_free_voidp(void *v){
 599   stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
 600 }
 601
 602 void heap_ignore_region_free(mc_heap_ignore_region_t r){
 603   xbt_free(r);
 604 }
 605
 606 void heap_ignore_region_free_voidp(void *r){
 607   heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
 608 }
 609
 610 static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r){
 611   xbt_free(r);
 612 }
 613
 614 static void checkpoint_ignore_region_free_voidp(void *r){
 615   checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
 616 }
 617
 618 /***********************************************************************/
 619
 620 void MC_ignore_heap(void *address, size_t size){
 621
 622   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 623
 624   MC_SET_RAW_MEM;
 625
 626   mc_heap_ignore_region_t region = NULL;
 627   region = xbt_new0(s_mc_heap_ignore_region_t, 1);
 628   region->address = address;
 629   region->size = size;
 630
 631   region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
 632
 633   if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
 634     region->fragment = -1;
 635     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
 636   }else{
 637     region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
 638     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
 639   }
 640
 641   if(mc_heap_comparison_ignore == NULL){
 642     mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
 643     xbt_dynar_push(mc_heap_comparison_ignore, &region);
 644     if(!raw_mem_set)
 645       MC_UNSET_RAW_MEM;
 646     return;
 647   }
 648
 649   unsigned int cursor = 0;
 650   mc_heap_ignore_region_t current_region = NULL;
 651   int start = 0;
 652   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
 653
 654   while(start <= end){
 655     cursor = (start + end) / 2;
 656     current_region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
 657     if(current_region->address == address){
 658       heap_ignore_region_free(region);
 659       if(!raw_mem_set)
 660         MC_UNSET_RAW_MEM;
 661       return;
 662     }else if(current_region->address < address){
 663       start = cursor + 1;
 664     }else{
 665       end = cursor - 1;
 666     }
 667   }
 668
 669   if(current_region->address < address)
 670     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
 671   else
 672     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
 673
 674   if(!raw_mem_set)
 675     MC_UNSET_RAW_MEM;
 676 }
 677
 678 void MC_remove_ignore_heap(void *address, size_t size){
 679
 680   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 681
 682   MC_SET_RAW_MEM;
 683
 684   unsigned int cursor = 0;
 685   int start = 0;
 686   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
 687   mc_heap_ignore_region_t region;
 688   int ignore_found = 0;
 689
 690   while(start <= end){
 691     cursor = (start + end) / 2;
 692     region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
 693     if(region->address == address){
 694       ignore_found = 1;
 695       break;
 696     }else if(region->address < address){
 697       start = cursor + 1;
 698     }else{
 699       if((char * )region->address <= ((char *)address + size)){
 700         ignore_found = 1;
 701         break;
 702       }else{
 703         end = cursor - 1;
 704       }
 705     }
 706   }
 707
 708   if(ignore_found == 1){
 709     xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
 710     MC_remove_ignore_heap(address, size);
 711   }
 712
 713   if(!raw_mem_set)
 714     MC_UNSET_RAW_MEM;
 715
 716 }
 717
 718 void MC_ignore_global_variable(const char *name){
 719
 720   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 721
 722   MC_SET_RAW_MEM;
 723
 724   xbt_assert(mc_libsimgrid_info, "MC subsystem not initialized");
 725
 726     unsigned int cursor = 0;
 727     dw_variable_t current_var;
 728     int start = 0;
 729     int end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
 730
 731     while(start <= end){
 732       cursor = (start + end) /2;
 733       current_var = (dw_variable_t)xbt_dynar_get_as(mc_libsimgrid_info->global_variables, cursor, dw_variable_t);
 734       if(strcmp(current_var->name, name) == 0){
 735         xbt_dynar_remove_at(mc_libsimgrid_info->global_variables, cursor, NULL);
 736         start = 0;
 737         end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
 738       }else if(strcmp(current_var->name, name) < 0){
 739         start = cursor + 1;
 740       }else{
 741         end = cursor - 1;
 742       }
 743     }
 744
 745   if(!raw_mem_set)
 746     MC_UNSET_RAW_MEM;
 747 }
 748
 749 void MC_ignore_local_variable(const char *var_name, const char *frame_name){
 750
 751   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 752
 753   MC_SET_RAW_MEM;
 754
 755     unsigned int cursor = 0;
 756     dw_variable_t current_var;
 757     int start, end;
 758     if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames */
 759       xbt_dict_cursor_t dict_cursor;
 760       char *current_frame_name;
 761       dw_frame_t frame;
 762       xbt_dict_foreach(mc_libsimgrid_info->local_variables, dict_cursor, current_frame_name, frame){
 763         start = 0;
 764         end = xbt_dynar_length(frame->variables) - 1;
 765         while(start <= end){
 766           cursor = (start + end) / 2;
 767           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
 768           if(strcmp(current_var->name, var_name) == 0){
 769             xbt_dynar_remove_at(frame->variables, cursor, NULL);
 770             start = 0;
 771             end = xbt_dynar_length(frame->variables) - 1;
 772           }else if(strcmp(current_var->name, var_name) < 0){
 773             start = cursor + 1;
 774           }else{
 775             end = cursor - 1;
 776           }
 777         }
 778       }
 779        xbt_dict_foreach(mc_binary_info->local_variables, dict_cursor, current_frame_name, frame){
 780         start = 0;
 781         end = xbt_dynar_length(frame->variables) - 1;
 782         while(start <= end){
 783           cursor = (start + end) / 2;
 784           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
 785           if(strcmp(current_var->name, var_name) == 0){
 786             xbt_dynar_remove_at(frame->variables, cursor, NULL);
 787             start = 0;
 788             end = xbt_dynar_length(frame->variables) - 1;
 789           }else if(strcmp(current_var->name, var_name) < 0){
 790             start = cursor + 1;
 791           }else{
 792             end = cursor - 1;
 793           }
 794         }
 795       }
 796     }else{
 797       xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(
 798                                       mc_libsimgrid_info->local_variables, frame_name))->variables;
 799       start = 0;
 800       end = xbt_dynar_length(variables_list) - 1;
 801       while(start <= end){
 802         cursor = (start + end) / 2;
 803         current_var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor, dw_variable_t);
 804         if(strcmp(current_var->name, var_name) == 0){
 805           xbt_dynar_remove_at(variables_list, cursor, NULL);
 806           start = 0;
 807           end = xbt_dynar_length(variables_list) - 1;
 808         }else if(strcmp(current_var->name, var_name) < 0){
 809           start = cursor + 1;
 810         }else{
 811           end = cursor - 1;
 812         }
 813       }
 814     }
 815
 816   if(!raw_mem_set)
 817     MC_UNSET_RAW_MEM;
 818
 819 }
 820
 821 void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
 822
 823   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 824
 825   MC_SET_RAW_MEM;
 826
 827   if(stacks_areas == NULL)
 828     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
 829
 830   stack_region_t region = NULL;
 831   region = xbt_new0(s_stack_region_t, 1);
 832   region->address = stack;
 833   region->process_name = strdup(name);
 834   region->context = context;
 835   region->size = size;
 836   region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
 837   xbt_dynar_push(stacks_areas, &region);
 838
 839   if(!raw_mem_set)
 840     MC_UNSET_RAW_MEM;
 841 }
 842
 843 void MC_ignore(void *addr, size_t size){
 844
 845   int raw_mem_set= (mmalloc_get_current_heap() == raw_heap);
 846
 847   MC_SET_RAW_MEM;
 848
 849   if(mc_checkpoint_ignore == NULL)
 850     mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp);
 851
 852   mc_checkpoint_ignore_region_t region = xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
 853   region->addr = addr;
 854   region->size = size;
 855
 856   if(xbt_dynar_is_empty(mc_checkpoint_ignore)){
 857     xbt_dynar_push(mc_checkpoint_ignore, &region);
 858   }else{
 859
 860     unsigned int cursor = 0;
 861     int start = 0;
 862     int end = xbt_dynar_length(mc_checkpoint_ignore) -1;
 863     mc_checkpoint_ignore_region_t current_region = NULL;
 864
 865     while(start <= end){
 866       cursor = (start + end) / 2;
 867       current_region = (mc_checkpoint_ignore_region_t)xbt_dynar_get_as(mc_checkpoint_ignore, cursor, mc_checkpoint_ignore_region_t);
 868       if(current_region->addr == addr){
 869         if(current_region->size == size){
 870           checkpoint_ignore_region_free(region);
 871           if(!raw_mem_set)
 872             MC_UNSET_RAW_MEM;
 873           return;
 874         }else if(current_region->size < size){
 875           start = cursor + 1;
 876         }else{
 877           end = cursor - 1;
 878         }
 879       }else if(current_region->addr < addr){
 880           start = cursor + 1;
 881       }else{
 882         end = cursor - 1;
 883       }
 884     }
 885
 886      if(current_region->addr == addr){
 887        if(current_region->size < size){
 888         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
 889       }else{
 890         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
 891       }
 892     }else if(current_region->addr < addr){
 893        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
 894     }else{
 895        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
 896     }
 897   }
 898
 899   if(!raw_mem_set)
 900     MC_UNSET_RAW_MEM;
 901 }
 902
 903 /*******************************  Initialisation of MC *******************************/
 904 /*********************************************************************************/
 905
 906 static void MC_post_process_object_info(mc_object_info_t info) {
 907   mc_object_info_t other_info = info == mc_binary_info ? mc_libsimgrid_info : mc_binary_info;
 908   xbt_dict_cursor_t cursor = NULL;
 909   char* key = NULL;
 910   dw_type_t type = NULL;
 911   xbt_dict_foreach(info->types, cursor, key, type){
 912     if(type->name && type->byte_size == 0) {
 913       type->other_object_same_type = xbt_dict_get_or_null(other_info->types_by_name, type->name);
 914     }
 915   }
 916 }
 917
 918 static void MC_init_debug_info(void) {
 919   XBT_INFO("Get debug information ...");
 920
 921   memory_map_t maps = MC_get_memory_map();
 922
 923   /* Get local variables for state equality detection */
 924   mc_binary_info = MC_find_object_info(maps, xbt_binary_name, 1);
 925   mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path, 0);
 926
 927   // Use information of the other objects:
 928   MC_post_process_object_info(mc_binary_info);
 929   MC_post_process_object_info(mc_libsimgrid_info);
 930
 931   MC_free_memory_map(maps);
 932   XBT_INFO("Get debug information done !");
 933 }
 934
 935 void MC_init(){
 936
 937   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 938
 939   compare = 0;
 940
 941   /* Initialize the data structures that must be persistent across every
 942      iteration of the model-checker (in RAW memory) */
 943
 944   MC_SET_RAW_MEM;
 945
 946   MC_init_memory_map_info();
 947   MC_init_debug_info();
 948
 949    /* Init parmap */
 950   parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
 951
 952   MC_UNSET_RAW_MEM;
 953
 954    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
 955   MC_ignore_local_variable("e", "*");
 956   MC_ignore_local_variable("__ex_cleanup", "*");
 957   MC_ignore_local_variable("__ex_mctx_en", "*");
 958   MC_ignore_local_variable("__ex_mctx_me", "*");
 959   MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
 960   MC_ignore_local_variable("_log_ev", "*");
 961   MC_ignore_local_variable("_throw_ctx", "*");
 962   MC_ignore_local_variable("ctx", "*");
 963
 964   MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
 965   MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
 966
 967   /* Ignore local variable about time used for tracing */
 968   MC_ignore_local_variable("start_time", "*");
 969
 970   MC_ignore_global_variable("mc_comp_times");
 971   MC_ignore_global_variable("mc_snapshot_comparison_time");
 972   MC_ignore_global_variable("mc_time");
 973   MC_ignore_global_variable("smpi_current_rank");
 974   MC_ignore_global_variable("counter"); /* Static variable used for tracing */
 975   MC_ignore_global_variable("maestro_stack_start");
 976   MC_ignore_global_variable("maestro_stack_end");
 977   MC_ignore_global_variable("smx_total_comms");
 978
 979   MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run));
 980   MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran));
 981   MC_ignore_heap(simix_global->process_to_run, sizeof(*(simix_global->process_to_run)));
 982   MC_ignore_heap(simix_global->process_that_ran, sizeof(*(simix_global->process_that_ran)));
 983
 984   smx_process_t process;
 985   xbt_swag_foreach(process, simix_global->process_list){
 986     MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
 987   }
 988
 989   if(raw_mem_set)
 990     MC_SET_RAW_MEM;
 991
 992 }
 993
 994 static void MC_init_dot_output(){ /* FIXME : more colors */
 995
 996   colors[0] = "blue";
 997   colors[1] = "red";
 998   colors[2] = "green3";
 999   colors[3] = "goldenrod";
1000   colors[4] = "brown";
1001   colors[5] = "purple";
1002   colors[6] = "magenta";
1003   colors[7] = "turquoise4";
1004   colors[8] = "gray25";
1005   colors[9] = "forestgreen";
1006   colors[10] = "hotpink";
1007   colors[11] = "lightblue";
1008   colors[12] = "tan";
1009
1010   dot_output = fopen(_sg_mc_dot_output_file, "w");
1011
1012   if(dot_output == NULL){
1013     perror("Error open dot output file");
1014     xbt_abort();
1015   }
1016
1017   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");
1018
1019 }
1020
1021 /*******************************  Core of MC *******************************/
1022 /**************************************************************************/
1023
1024 void MC_do_the_modelcheck_for_real() {
1025
1026   MC_SET_RAW_MEM;
1027   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
1028   MC_UNSET_RAW_MEM;
1029
1030   if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
1031     if (mc_reduce_kind==e_mc_reduce_unset)
1032       mc_reduce_kind=e_mc_reduce_dpor;
1033
1034     XBT_INFO("Check a safety property");
1035     MC_modelcheck_safety();
1036
1037   } else  {
1038
1039     if (mc_reduce_kind==e_mc_reduce_unset)
1040       mc_reduce_kind=e_mc_reduce_none;
1041
1042     XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
1043     MC_automaton_load(_sg_mc_property_file);
1044     MC_modelcheck_liveness();
1045   }
1046 }
1047
1048 void MC_modelcheck_safety(void)
1049 {
1050   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1051
1052   /* Check if MC is already initialized */
1053   if (initial_state_safety)
1054     return;
1055
1056   mc_time = xbt_new0(double, simix_process_maxpid);
1057
1058   /* mc_time refers to clock for each process -> ignore it for heap comparison */
1059   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1060
1061   /* Initialize the data structures that must be persistent across every
1062      iteration of the model-checker (in RAW memory) */
1063
1064   MC_SET_RAW_MEM;
1065
1066   /* Initialize statistics */
1067   mc_stats = xbt_new0(s_mc_stats_t, 1);
1068   mc_stats->state_size = 1;
1069
1070   /* Create exploration stack */
1071   mc_stack_safety = xbt_fifo_new();
1072
1073   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1074     MC_init_dot_output();
1075
1076   MC_UNSET_RAW_MEM;
1077
1078   if(_sg_mc_visited > 0){
1079     MC_init();
1080   }else{
1081     MC_SET_RAW_MEM;
1082     MC_init_memory_map_info();
1083     MC_init_debug_info();
1084     MC_UNSET_RAW_MEM;
1085   }
1086
1087   MC_dpor_init();
1088
1089   MC_SET_RAW_MEM;
1090   /* Save the initial state */
1091   initial_state_safety = xbt_new0(s_mc_global_t, 1);
1092   initial_state_safety->snapshot = MC_take_snapshot(0);
1093   initial_state_safety->initial_communications_pattern_done = 0;
1094   initial_state_safety->comm_deterministic = 1;
1095   initial_state_safety->send_deterministic = 1;
1096   MC_UNSET_RAW_MEM;
1097
1098   MC_dpor();
1099
1100   if(raw_mem_set)
1101     MC_SET_RAW_MEM;
1102
1103   xbt_abort();
1104   //MC_exit();
1105 }
1106
1107 void MC_modelcheck_liveness(){
1108
1109   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1110
1111   MC_init();
1112
1113   mc_time = xbt_new0(double, simix_process_maxpid);
1114
1115   /* mc_time refers to clock for each process -> ignore it for heap comparison */
1116   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1117
1118   MC_SET_RAW_MEM;
1119
1120   /* Initialize statistics */
1121   mc_stats = xbt_new0(s_mc_stats_t, 1);
1122   mc_stats->state_size = 1;
1123
1124   /* Create exploration stack */
1125   mc_stack_liveness = xbt_fifo_new();
1126
1127   /* Create the initial state */
1128   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
1129
1130   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1131     MC_init_dot_output();
1132
1133   MC_UNSET_RAW_MEM;
1134
1135   MC_ddfs_init();
1136
1137   /* We're done */
1138   MC_print_statistics(mc_stats);
1139   xbt_free(mc_time);
1140
1141   if(raw_mem_set)
1142     MC_SET_RAW_MEM;
1143
1144 }
1145
1146
1147 void MC_exit(void)
1148 {
1149   xbt_free(mc_time);
1150
1151   MC_memory_exit();
1152   //xbt_abort();
1153 }
1154
1155 int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
1156
1157   return simcall->mc_value;
1158 }
1159
1160
1161 int MC_random(int min, int max)
1162 {
1163   /*FIXME: return mc_current_state->executed_transition->random.value;*/
1164   return simcall_mc_random(min, max);
1165 }
1166
1167 /**
1168  * \brief Schedules all the process that are ready to run
1169  */
1170 void MC_wait_for_requests(void)
1171 {
1172   smx_process_t process;
1173   smx_simcall_t req;
1174   unsigned int iter;
1175
1176   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
1177     SIMIX_process_runall();
1178     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
1179       req = &process->simcall;
1180       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
1181         SIMIX_simcall_pre(req, 0);
1182     }
1183   }
1184 }
1185
1186 int MC_deadlock_check()
1187 {
1188   int deadlock = FALSE;
1189   smx_process_t process;
1190   if(xbt_swag_size(simix_global->process_list)){
1191     deadlock = TRUE;
1192     xbt_swag_foreach(process, simix_global->process_list){
1193       if(process->simcall.call != SIMCALL_NONE
1194          && MC_request_is_enabled(&process->simcall)){
1195         deadlock = FALSE;
1196         break;
1197       }
1198     }
1199   }
1200   return deadlock;
1201 }
1202
1203 /**
1204  * \brief Re-executes from the state at position start all the transitions indicated by
1205  *        a given model-checker stack.
1206  * \param stack The stack with the transitions to execute.
1207  * \param start Start index to begin the re-execution.
1208  */
1209 void MC_replay(xbt_fifo_t stack, int start)
1210 {
1211   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
1212
1213   int value, i = 1, count = 1;
1214   char *req_str;
1215   smx_simcall_t req = NULL, saved_req = NULL;
1216   xbt_fifo_item_t item, start_item;
1217   mc_state_t state;
1218   smx_process_t process = NULL;
1219   int comm_pattern = 0;
1220
1221   XBT_DEBUG("**** Begin Replay ****");
1222
1223   if(start == -1){
1224     /* Restore the initial state */
1225     MC_restore_snapshot(initial_state_safety->snapshot);
1226     /* At the moment of taking the snapshot the raw heap was set, so restoring
1227      * it will set it back again, we have to unset it to continue  */
1228     MC_UNSET_RAW_MEM;
1229   }
1230
1231   start_item = xbt_fifo_get_last_item(stack);
1232   if(start != -1){
1233     while (i != start){
1234       start_item = xbt_fifo_get_prev_item(start_item);
1235       i++;
1236     }
1237   }
1238
1239   MC_SET_RAW_MEM;
1240   xbt_dict_reset(first_enabled_state);
1241   xbt_swag_foreach(process, simix_global->process_list){
1242     if(MC_process_is_enabled(process)){
1243       char *key = bprintf("%lu", process->pid);
1244       char *data = bprintf("%d", count);
1245       xbt_dict_set(first_enabled_state, key, data, NULL);
1246       xbt_free(key);
1247     }
1248   }
1249   if(_sg_mc_comms_determinism)
1250     xbt_dynar_reset(communications_pattern);
1251   MC_UNSET_RAW_MEM;
1252
1253
1254   /* Traverse the stack from the state at position start and re-execute the transitions */
1255   for (item = start_item;
1256        item != xbt_fifo_get_first_item(stack);
1257        item = xbt_fifo_get_prev_item(item)) {
1258
1259     state = (mc_state_t) xbt_fifo_get_item_content(item);
1260     saved_req = MC_state_get_executed_request(state, &value);
1261
1262     MC_SET_RAW_MEM;
1263     char *key = bprintf("%lu", saved_req->issuer->pid);
1264     xbt_dict_remove(first_enabled_state, key);
1265     xbt_free(key);
1266     MC_UNSET_RAW_MEM;
1267
1268     if(saved_req){
1269       /* because we got a copy of the executed request, we have to fetch the
1270          real one, pointed by the request field of the issuer process */
1271       req = &saved_req->issuer->simcall;
1272
1273       /* Debug information */
1274       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1275         req_str = MC_request_to_string(req, value);
1276         XBT_DEBUG("Replay: %s (%p)", req_str, state);
1277         xbt_free(req_str);
1278       }
1279     }
1280
1281     if(_sg_mc_comms_determinism){
1282       if(req->call == SIMCALL_COMM_ISEND)
1283         comm_pattern = 1;
1284       else if(req->call == SIMCALL_COMM_IRECV)
1285       comm_pattern = 2;
1286     }
1287
1288     SIMIX_simcall_pre(req, value);
1289
1290     if(_sg_mc_comms_determinism){
1291       MC_SET_RAW_MEM;
1292       if(comm_pattern != 0){
1293         get_comm_pattern(communications_pattern, req, comm_pattern);
1294       }
1295       MC_UNSET_RAW_MEM;
1296       comm_pattern = 0;
1297     }
1298
1299     MC_wait_for_requests();
1300
1301     count++;
1302
1303     MC_SET_RAW_MEM;
1304     /* Insert in dict all enabled processes */
1305     xbt_swag_foreach(process, simix_global->process_list){
1306       if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
1307         char *key = bprintf("%lu", process->pid);
1308         if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
1309           char *data = bprintf("%d", count);
1310           xbt_dict_set(first_enabled_state, key, data, NULL);
1311         }
1312         xbt_free(key);
1313       }
1314     }
1315     MC_UNSET_RAW_MEM;
1316
1317     /* Update statistics */
1318     mc_stats->visited_states++;
1319     mc_stats->executed_transitions++;
1320
1321   }
1322
1323   XBT_DEBUG("**** End Replay ****");
1324
1325   if(raw_mem)
1326     MC_SET_RAW_MEM;
1327   else
1328     MC_UNSET_RAW_MEM;
1329
1330
1331 }
1332
1333 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
1334 {
1335
1336   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1337
1338   int value;
1339   char *req_str;
1340   smx_simcall_t req = NULL, saved_req = NULL;
1341   xbt_fifo_item_t item;
1342   mc_state_t state;
1343   mc_pair_t pair;
1344   int depth = 1;
1345
1346   XBT_DEBUG("**** Begin Replay ****");
1347
1348   /* Restore the initial state */
1349   MC_restore_snapshot(initial_state_liveness->snapshot);
1350
1351   /* At the moment of taking the snapshot the raw heap was set, so restoring
1352    * it will set it back again, we have to unset it to continue  */
1353   if(!initial_state_liveness->raw_mem_set)
1354     MC_UNSET_RAW_MEM;
1355
1356   if(all_stack){
1357
1358     item = xbt_fifo_get_last_item(stack);
1359
1360     while(depth <= xbt_fifo_size(stack)){
1361
1362       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
1363       state = (mc_state_t) pair->graph_state;
1364
1365       if(pair->requests > 0){
1366
1367         saved_req = MC_state_get_executed_request(state, &value);
1368         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
1369
1370         if(saved_req != NULL){
1371           /* because we got a copy of the executed request, we have to fetch the
1372              real one, pointed by the request field of the issuer process */
1373           req = &saved_req->issuer->simcall;
1374           //XBT_DEBUG("Req->call %u", req->call);
1375
1376           /* Debug information */
1377           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1378             req_str = MC_request_to_string(req, value);
1379             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
1380             xbt_free(req_str);
1381           }
1382
1383         }
1384
1385         SIMIX_simcall_pre(req, value);
1386         MC_wait_for_requests();
1387       }
1388
1389       depth++;
1390
1391       /* Update statistics */
1392       mc_stats->visited_pairs++;
1393       mc_stats->executed_transitions++;
1394
1395       item = xbt_fifo_get_prev_item(item);
1396     }
1397
1398   }else{
1399
1400     /* Traverse the stack from the initial state and re-execute the transitions */
1401     for (item = xbt_fifo_get_last_item(stack);
1402          item != xbt_fifo_get_first_item(stack);
1403          item = xbt_fifo_get_prev_item(item)) {
1404
1405       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
1406       state = (mc_state_t) pair->graph_state;
1407
1408       if(pair->requests > 0){
1409
1410         saved_req = MC_state_get_executed_request(state, &value);
1411         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
1412
1413         if(saved_req != NULL){
1414           /* because we got a copy of the executed request, we have to fetch the
1415              real one, pointed by the request field of the issuer process */
1416           req = &saved_req->issuer->simcall;
1417           //XBT_DEBUG("Req->call %u", req->call);
1418
1419           /* Debug information */
1420           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1421             req_str = MC_request_to_string(req, value);
1422             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
1423             xbt_free(req_str);
1424           }
1425
1426         }
1427
1428         SIMIX_simcall_pre(req, value);
1429         MC_wait_for_requests();
1430       }
1431
1432       depth++;
1433
1434       /* Update statistics */
1435       mc_stats->visited_pairs++;
1436       mc_stats->executed_transitions++;
1437     }
1438   }
1439
1440   XBT_DEBUG("**** End Replay ****");
1441
1442   if(initial_state_liveness->raw_mem_set)
1443     MC_SET_RAW_MEM;
1444   else
1445     MC_UNSET_RAW_MEM;
1446
1447 }
1448
1449 /**
1450  * \brief Dumps the contents of a model-checker's stack and shows the actual
1451  *        execution trace
1452  * \param stack The stack to dump
1453  */
1454 void MC_dump_stack_safety(xbt_fifo_t stack)
1455 {
1456
1457   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1458
1459   MC_show_stack_safety(stack);
1460
1461   if(!_sg_mc_checkpoint){
1462
1463     mc_state_t state;
1464
1465     MC_SET_RAW_MEM;
1466     while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
1467       MC_state_delete(state);
1468     MC_UNSET_RAW_MEM;
1469
1470   }
1471
1472   if(raw_mem_set)
1473     MC_SET_RAW_MEM;
1474   else
1475     MC_UNSET_RAW_MEM;
1476
1477 }
1478
1479
1480 void MC_show_stack_safety(xbt_fifo_t stack)
1481 {
1482
1483   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1484
1485   MC_SET_RAW_MEM;
1486
1487   int value;
1488   mc_state_t state;
1489   xbt_fifo_item_t item;
1490   smx_simcall_t req;
1491   char *req_str = NULL;
1492
1493   for (item = xbt_fifo_get_last_item(stack);
1494        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
1495         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
1496     req = MC_state_get_executed_request(state, &value);
1497     if(req){
1498       req_str = MC_request_to_string(req, value);
1499       XBT_INFO("%s", req_str);
1500       xbt_free(req_str);
1501     }
1502   }
1503
1504   if(!raw_mem_set)
1505     MC_UNSET_RAW_MEM;
1506 }
1507
1508 void MC_show_deadlock(smx_simcall_t req)
1509 {
1510   /*char *req_str = NULL;*/
1511   XBT_INFO("**************************");
1512   XBT_INFO("*** DEAD-LOCK DETECTED ***");
1513   XBT_INFO("**************************");
1514   XBT_INFO("Locked request:");
1515   /*req_str = MC_request_to_string(req);
1516     XBT_INFO("%s", req_str);
1517     xbt_free(req_str);*/
1518   XBT_INFO("Counter-example execution trace:");
1519   MC_dump_stack_safety(mc_stack_safety);
1520   MC_print_statistics(mc_stats);
1521 }
1522
1523
1524 void MC_show_stack_liveness(xbt_fifo_t stack){
1525   int value;
1526   mc_pair_t pair;
1527   xbt_fifo_item_t item;
1528   smx_simcall_t req;
1529   char *req_str = NULL;
1530
1531   for (item = xbt_fifo_get_last_item(stack);
1532        (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
1533         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
1534     req = MC_state_get_executed_request(pair->graph_state, &value);
1535     if(req){
1536       if(pair->requests>0){
1537         req_str = MC_request_to_string(req, value);
1538         XBT_INFO("%s", req_str);
1539         xbt_free(req_str);
1540       }else{
1541         XBT_INFO("End of system requests but evolution in Büchi automaton");
1542       }
1543     }
1544   }
1545 }
1546
1547 void MC_dump_stack_liveness(xbt_fifo_t stack){
1548
1549   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1550
1551   mc_pair_t pair;
1552
1553   MC_SET_RAW_MEM;
1554   while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
1555     MC_pair_delete(pair);
1556   MC_UNSET_RAW_MEM;
1557
1558   if(raw_mem_set)
1559     MC_SET_RAW_MEM;
1560
1561 }
1562
1563
1564 void MC_print_statistics(mc_stats_t stats)
1565 {
1566   if(stats->expanded_pairs == 0){
1567     XBT_INFO("Expanded states = %lu", stats->expanded_states);
1568     XBT_INFO("Visited states = %lu", stats->visited_states);
1569   }else{
1570     XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
1571     XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
1572   }
1573   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
1574   MC_SET_RAW_MEM;
1575   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
1576     fprintf(dot_output, "}\n");
1577     fclose(dot_output);
1578   }
1579   if(initial_state_safety != NULL && _sg_mc_comms_determinism){
1580     XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
1581     XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
1582   }
1583   MC_UNSET_RAW_MEM;
1584 }
1585
1586 void MC_assert(int prop)
1587 {
1588   if (MC_is_active() && !prop){
1589     XBT_INFO("**************************");
1590     XBT_INFO("*** PROPERTY NOT VALID ***");
1591     XBT_INFO("**************************");
1592     XBT_INFO("Counter-example execution trace:");
1593     MC_dump_stack_safety(mc_stack_safety);
1594     MC_print_statistics(mc_stats);
1595     xbt_abort();
1596   }
1597 }
1598
1599 void MC_cut(void){
1600   user_max_depth_reached = 1;
1601 }
1602
1603 void MC_process_clock_add(smx_process_t process, double amount)
1604 {
1605   mc_time[process->pid] += amount;
1606 }
1607
1608 double MC_process_clock_get(smx_process_t process)
1609 {
1610   if(mc_time){
1611     if(process != NULL)
1612       return mc_time[process->pid];
1613     else
1614       return -1;
1615   }else{
1616     return 0;
1617   }
1618 }
1619
1620 void MC_automaton_load(const char *file){
1621
1622   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1623
1624   MC_SET_RAW_MEM;
1625
1626   if (_mc_property_automaton == NULL)
1627     _mc_property_automaton = xbt_automaton_new();
1628
1629   xbt_automaton_load(_mc_property_automaton,file);
1630
1631   MC_UNSET_RAW_MEM;
1632
1633   if(raw_mem_set)
1634     MC_SET_RAW_MEM;
1635
1636 }
1637
1638 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
1639
1640   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1641
1642   MC_SET_RAW_MEM;
1643
1644   if (_mc_property_automaton == NULL)
1645     _mc_property_automaton = xbt_automaton_new();
1646
1647   xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
1648
1649   MC_UNSET_RAW_MEM;
1650
1651   if(raw_mem_set)
1652     MC_SET_RAW_MEM;
1653
1654 }
1655
1656
1657