Logo AND Algorithmique Numérique Distribuée

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