Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : update tesh files
[simgrid.git] / src / mc / mc_global.c
1 /* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved.            */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #include <unistd.h>
7 #include <sys/types.h>
8 #include <sys/wait.h>
9 #include <sys/time.h>
10
11 #include "simgrid/sg_config.h"
12 #include "../surf/surf_private.h"
13 #include "../simix/smx_private.h"
14 #include "../xbt/mmalloc/mmprivate.h"
15 #include "xbt/fifo.h"
16 #include "mc_private.h"
17 #include "xbt/automaton.h"
18 #include "xbt/dict.h"
19
20 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
21 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
22                                 "Logging specific to MC (global)");
23
24 /* Configuration support */
25 e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
26
27 int _sg_do_model_check = 0;
28 int _sg_mc_checkpoint=0;
29 char* _sg_mc_property_file=NULL;
30 int _sg_mc_timeout=0;
31 int _sg_mc_max_depth=1000;
32 int _sg_mc_visited=0;
33 char *_sg_mc_dot_output_file = NULL;
34
35 extern int _sg_init_status;
36 void _mc_cfg_cb_reduce(const char *name, int pos) {
37   if (_sg_init_status && !_sg_do_model_check) {
38     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.");
39   }
40   char *val= xbt_cfg_get_string(_sg_cfg_set, name);
41   if (!strcasecmp(val,"none")) {
42     mc_reduce_kind = e_mc_reduce_none;
43   } else if (!strcasecmp(val,"dpor")) {
44     mc_reduce_kind = e_mc_reduce_dpor;
45   } else {
46     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
47   }
48 }
49
50 void _mc_cfg_cb_checkpoint(const char *name, int pos) {
51   if (_sg_init_status && !_sg_do_model_check) {
52     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.");
53   }
54   _sg_mc_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
55 }
56 void _mc_cfg_cb_property(const char *name, int pos) {
57   if (_sg_init_status && !_sg_do_model_check) {
58     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.");
59   }
60   _sg_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
61 }
62
63 void _mc_cfg_cb_timeout(const char *name, int pos) {
64   if (_sg_init_status && !_sg_do_model_check) {
65     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.");
66   }
67   _sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
68 }
69
70 void _mc_cfg_cb_max_depth(const char *name, int pos) {
71   if (_sg_init_status && !_sg_do_model_check) {
72     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.");
73   }
74   _sg_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
75 }
76
77 void _mc_cfg_cb_visited(const char *name, int pos) {
78   if (_sg_init_status && !_sg_do_model_check) {
79     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.");
80   }
81   _sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
82 }
83
84 void _mc_cfg_cb_dot_output(const char *name, int pos) {
85   if (_sg_init_status && !_sg_do_model_check) {
86     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.");
87   }
88   _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
89 }
90
91 /* MC global data structures */
92 mc_state_t mc_current_state = NULL;
93 char mc_replay_mode = FALSE;
94 double *mc_time = NULL;
95 mc_comparison_times_t mc_comp_times = NULL;
96 double mc_snapshot_comparison_time;
97 mc_stats_t mc_stats = NULL;
98
99 /* Safety */
100 xbt_fifo_t mc_stack_safety = NULL;
101 mc_global_t initial_state_safety = NULL;
102
103 /* Liveness */
104 xbt_fifo_t mc_stack_liveness = NULL;
105 mc_global_t initial_state_liveness = NULL;
106 int compare;
107
108 xbt_automaton_t _mc_property_automaton = NULL;
109
110 /* Variables */
111 xbt_dict_t mc_local_variables_libsimgrid = NULL;
112 xbt_dict_t mc_local_variables_binary = NULL;
113 xbt_dynar_t mc_global_variables_libsimgrid = NULL;
114 xbt_dynar_t mc_global_variables_binary = NULL;
115 xbt_dict_t mc_variables_type_libsimgrid = NULL;
116 xbt_dict_t mc_variables_type_binary = NULL;
117
118 /* Ignore mechanism */
119 xbt_dynar_t mc_stack_comparison_ignore;
120 xbt_dynar_t mc_data_bss_comparison_ignore;
121 extern xbt_dynar_t mc_heap_comparison_ignore;
122 extern xbt_dynar_t stacks_areas;
123
124 /* Dot output */
125 FILE *dot_output = NULL;
126 const char* colors[13];
127
128
129 /*******************************  DWARF Information *******************************/
130 /**********************************************************************************/
131
132 /************************** Free functions *************************/
133
134 static void dw_location_free(dw_location_t l){
135   if(l){
136     if(l->type == e_dw_loclist)
137       xbt_dynar_free(&(l->location.loclist));
138     else if(l->type == e_dw_compose)
139       xbt_dynar_free(&(l->location.compose));
140     else if(l->type == e_dw_arithmetic)
141       xbt_free(l->location.arithmetic);
142   
143     xbt_free(l);
144   }
145 }
146
147 static void dw_location_entry_free(dw_location_entry_t e){
148   dw_location_free(e->location);
149   xbt_free(e);
150 }
151
152 static void dw_type_free(dw_type_t t){
153   xbt_free(t->name);
154   xbt_free(t->dw_type_id);
155   xbt_dynar_free(&(t->members));
156   xbt_free(t);
157 }
158
159 static void dw_type_free_voidp(void *t){
160   dw_type_free((dw_type_t) * (void **) t);
161 }
162
163 static void dw_variable_free(dw_variable_t v){
164   if(v){
165     xbt_free(v->name);
166     xbt_free(v->type_origin);
167     if(!v->global)
168       dw_location_free(v->address.location);
169     xbt_free(v);
170   }
171 }
172
173 static void dw_variable_free_voidp(void *t){
174   dw_variable_free((dw_variable_t) * (void **) t);
175 }
176
177 /*************************************************************************/
178
179 static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr){
180
181   dw_location_t loc = xbt_new0(s_dw_location_t, 1);
182
183   if(location_list != NULL){
184     
185     char *key = bprintf("%d", (int)strtoul(expr, NULL, 16));
186     loc->type = e_dw_loclist;
187     loc->location.loclist =  (xbt_dynar_t)xbt_dict_get_or_null(location_list, key);
188     if(loc->location.loclist == NULL)
189       XBT_INFO("Key not found in loclist");
190     xbt_free(key);
191     return loc;
192
193   }else{
194
195     int cursor = 0;
196     char *tok = NULL, *tok2 = NULL; 
197     
198     xbt_dynar_t tokens1 = xbt_str_split(expr, ";");
199     xbt_dynar_t tokens2;
200
201     loc->type = e_dw_compose;
202     loc->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL);
203
204     while(cursor < xbt_dynar_length(tokens1)){
205
206       tok = xbt_dynar_get_as(tokens1, cursor, char*);
207       tokens2 = xbt_str_split(tok, " ");
208       tok2 = xbt_dynar_get_as(tokens2, 0, char*);
209       
210       if(strncmp(tok2, "DW_OP_reg", 9) == 0){
211         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
212         new_element->type = e_dw_register;
213         new_element->location.reg = atoi(strtok(tok2, "DW_OP_reg"));
214         xbt_dynar_push(loc->location.compose, &new_element);     
215       }else if(strcmp(tok2, "DW_OP_fbreg:") == 0){
216         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
217         new_element->type = e_dw_fbregister_op;
218         new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
219         xbt_dynar_push(loc->location.compose, &new_element);
220       }else if(strncmp(tok2, "DW_OP_breg", 10) == 0){
221         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
222         new_element->type = e_dw_bregister_op;
223         new_element->location.breg_op.reg = atoi(strtok(tok2, "DW_OP_breg"));
224         new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
225         xbt_dynar_push(loc->location.compose, &new_element);
226       }else if(strncmp(tok2, "DW_OP_lit", 9) == 0){
227         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
228         new_element->type = e_dw_lit;
229         new_element->location.lit = atoi(strtok(tok2, "DW_OP_lit"));
230         xbt_dynar_push(loc->location.compose, &new_element);
231       }else if(strcmp(tok2, "DW_OP_piece:") == 0){
232         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
233         new_element->type = e_dw_piece;
234         new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
235         xbt_dynar_push(loc->location.compose, &new_element);
236       }else if(strcmp(tok2, "DW_OP_plus_uconst:") == 0){
237         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
238         new_element->type = e_dw_plus_uconst;
239         new_element->location.plus_uconst = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char *));
240         xbt_dynar_push(loc->location.compose, &new_element);
241       }else if(strcmp(tok, "DW_OP_abs") == 0 || 
242                strcmp(tok, "DW_OP_and") == 0 ||
243                strcmp(tok, "DW_OP_div") == 0 ||
244                strcmp(tok, "DW_OP_minus") == 0 ||
245                strcmp(tok, "DW_OP_mod") == 0 ||
246                strcmp(tok, "DW_OP_mul") == 0 ||
247                strcmp(tok, "DW_OP_neg") == 0 ||
248                strcmp(tok, "DW_OP_not") == 0 ||
249                strcmp(tok, "DW_OP_or") == 0 ||
250                strcmp(tok, "DW_OP_plus") == 0){               
251         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
252         new_element->type = e_dw_arithmetic;
253         new_element->location.arithmetic = strdup(strtok(tok2, "DW_OP_"));
254         xbt_dynar_push(loc->location.compose, &new_element);
255       }else if(strcmp(tok, "DW_OP_stack_value") == 0){
256       }else if(strcmp(tok2, "DW_OP_deref_size:") == 0){
257         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
258         new_element->type = e_dw_deref;
259         new_element->location.deref_size = (unsigned int short) atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
260         xbt_dynar_push(loc->location.compose, &new_element);
261       }else if(strcmp(tok, "DW_OP_deref") == 0){
262         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
263         new_element->type = e_dw_deref;
264         new_element->location.deref_size = sizeof(void *);
265         xbt_dynar_push(loc->location.compose, &new_element);
266       }else if(strcmp(tok2, "DW_OP_constu:") == 0){
267         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
268         new_element->type = e_dw_uconstant;
269         new_element->location.uconstant.bytes = 1;
270         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
271         xbt_dynar_push(loc->location.compose, &new_element);
272       }else if(strcmp(tok2, "DW_OP_consts:") == 0){
273         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
274         new_element->type = e_dw_sconstant;
275         new_element->location.sconstant.bytes = 1;
276         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
277         xbt_dynar_push(loc->location.compose, &new_element);
278       }else if(strcmp(tok2, "DW_OP_const1u:") == 0 ||
279                strcmp(tok2, "DW_OP_const2u:") == 0 ||
280                strcmp(tok2, "DW_OP_const4u:") == 0 ||
281                strcmp(tok2, "DW_OP_const8u:") == 0){
282         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
283         new_element->type = e_dw_uconstant;
284         new_element->location.uconstant.bytes = tok2[11] - '0';
285         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
286         xbt_dynar_push(loc->location.compose, &new_element);
287       }else if(strcmp(tok, "DW_OP_const1s") == 0 ||
288                strcmp(tok, "DW_OP_const2s") == 0 ||
289                strcmp(tok, "DW_OP_const4s") == 0 ||
290                strcmp(tok, "DW_OP_const8s") == 0){
291         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
292         new_element->type = e_dw_sconstant;
293         new_element->location.sconstant.bytes = tok2[11] - '0';
294         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
295         xbt_dynar_push(loc->location.compose, &new_element);
296       }else{
297         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
298         new_element->type = e_dw_unsupported;
299         xbt_dynar_push(loc->location.compose, &new_element);
300       }
301
302       cursor++;
303       xbt_dynar_free(&tokens2);
304
305     }
306     
307     xbt_dynar_free(&tokens1);
308
309     return loc;
310     
311   }
312
313 }
314
315 static xbt_dict_t MC_dwarf_get_location_list(const char *elf_file){
316
317   char *command = bprintf("objdump -Wo %s", elf_file);
318
319   FILE *fp = popen(command, "r");
320
321   if(fp == NULL){
322     perror("popen for objdump failed");
323     xbt_abort();
324   }
325
326   int debug = 0; /*Detect if the program has been compiled with -g */
327
328   xbt_dict_t location_list = xbt_dict_new_homogeneous(NULL);
329   char *line = NULL, *loc_expr = NULL;
330   ssize_t read;
331   size_t n = 0;
332   int cursor_remove;
333   xbt_dynar_t split = NULL;
334
335   while ((read = xbt_getline(&line, &n, fp)) != -1) {
336
337     /* Wipeout the new line character */
338     line[read - 1] = '\0';
339
340     xbt_str_trim(line, NULL);
341     
342     if(n == 0)
343       continue;
344
345     if(strlen(line) == 0)
346       continue;
347
348     if(debug == 0){
349
350       if(strncmp(line, elf_file, strlen(elf_file)) == 0)
351         continue;
352       
353       if(strncmp(line, "Contents", 8) == 0)
354         continue;
355
356       if(strncmp(line, "Offset", 6) == 0){
357         debug = 1;
358         continue;
359       }
360     }
361
362     if(debug == 0){
363       XBT_INFO("Your program must be compiled with -g");
364       xbt_abort();
365     }
366
367     xbt_dynar_t loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL);
368
369     xbt_str_strip_spaces(line);
370     split = xbt_str_split(line, " ");
371
372     while(read != -1 && strcmp("<End", (char *)xbt_dynar_get_as(split, 1, char *)) != 0){
373       
374       dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
375       new_entry->lowpc = strtoul((char *)xbt_dynar_get_as(split, 1, char *), NULL, 16);
376       new_entry->highpc = strtoul((char *)xbt_dynar_get_as(split, 2, char *), NULL, 16);
377       
378       cursor_remove =0;
379       while(cursor_remove < 3){
380         xbt_dynar_remove_at(split, 0, NULL);
381         cursor_remove++;
382       }
383
384       loc_expr = xbt_str_join(split, " ");
385       xbt_str_ltrim(loc_expr, "(");
386       xbt_str_rtrim(loc_expr, ")");
387       new_entry->location = MC_dwarf_get_location(NULL, loc_expr);
388
389       xbt_dynar_push(loclist, &new_entry);
390
391       xbt_dynar_free(&split);
392       free(loc_expr);
393
394       read = xbt_getline(&line, &n, fp);
395       if(read != -1){
396         line[read - 1] = '\0';
397         xbt_str_strip_spaces(line);
398         split = xbt_str_split(line, " ");
399       }
400
401     }
402
403
404     char *key = bprintf("%d", (int)strtoul((char *)xbt_dynar_get_as(split, 0, char *), NULL, 16));
405     xbt_dict_set(location_list, key, loclist, NULL);
406     xbt_free(key);
407     
408     xbt_dynar_free(&split);
409
410   }
411
412   xbt_free(line);
413   xbt_free(command);
414   pclose(fp);
415
416   return location_list;
417 }
418
419 static dw_frame_t MC_dwarf_get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset){
420
421   xbt_dict_cursor_t cursor = NULL;
422   char *name;
423   dw_frame_t res;
424
425   xbt_dict_foreach(all_variables, cursor, name, res) {
426     if(offset >= res->start && offset < res->end){
427       xbt_dict_cursor_free(&cursor);
428       return res;
429     }
430   }
431
432   xbt_dict_cursor_free(&cursor);
433   return NULL;
434   
435 }
436
437 static dw_variable_t MC_dwarf_get_variable_by_name(dw_frame_t frame, char *var){
438
439   unsigned int cursor = 0;
440   dw_variable_t current_var;
441
442   xbt_dynar_foreach(frame->variables, cursor, current_var){
443     if(strcmp(var, current_var->name) == 0)
444       return current_var;
445   }
446
447   return NULL;
448 }
449
450 static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *address){
451
452   if(xbt_dynar_is_empty(variables))
453     return 0;
454
455   unsigned int cursor = 0;
456   int start = 0;
457   int end = xbt_dynar_length(variables) - 1;
458   dw_variable_t var_test = NULL;
459
460   while(start <= end){
461     cursor = (start + end) / 2;
462     var_test = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t);
463     if(strcmp(var_test->name, var) < 0){
464       start = cursor + 1;
465     }else if(strcmp(var_test->name, var) > 0){
466       end = cursor - 1;
467     }else{
468       if(address){ /* global variable */
469         if(var_test->address.address == address)
470           return -1;
471         if(var_test->address.address > address)
472           end = cursor - 1;
473         else
474           start = cursor + 1;
475       }else{ /* local variable */
476         return -1;
477       }
478     }
479   }
480
481   if(strcmp(var_test->name, var) == 0){
482     if(address && var_test->address.address < address)
483       return cursor+1;
484     else
485       return cursor;
486   }else if(strcmp(var_test->name, var) < 0)
487     return cursor+1;
488   else
489     return cursor;
490
491 }
492
493
494 static void MC_dwarf_get_variables(const char *elf_file, xbt_dict_t location_list, xbt_dict_t *local_variables, xbt_dynar_t *global_variables, xbt_dict_t *types){
495
496   char *command = bprintf("objdump -Wi %s", elf_file);
497   
498   FILE *fp = popen(command, "r");
499
500   if(fp == NULL)
501     perror("popen for objdump failed");
502
503   char *line = NULL, *origin, *abstract_origin, *current_frame = NULL, 
504     *subprogram_name = NULL, *subprogram_start = NULL, *subprogram_end = NULL,
505     *node_type = NULL, *location_type = NULL, *variable_name = NULL, 
506     *loc_expr = NULL, *name = NULL, *end =NULL, *type_origin = NULL, *global_address = NULL, 
507     *parent_value = NULL;
508
509   ssize_t read =0;
510   size_t n = 0;
511   int global_variable = 0, parent = 0, new_frame = 0, new_variable = 1, size = 0, 
512     is_pointer = 0, struct_decl = 0, member_end = 0,
513     enumeration_size = 0, subrange = 0, union_decl = 0, offset = 0, index = 0;
514   
515   xbt_dynar_t split = NULL, split2 = NULL;
516
517   xbt_dict_t variables_origin = xbt_dict_new_homogeneous(xbt_free);
518   xbt_dict_t subprograms_origin = xbt_dict_new_homogeneous(xbt_free);
519
520   dw_frame_t variable_frame, subroutine_frame = NULL;
521
522   e_dw_type_type type_type = -1;
523
524   read = xbt_getline(&line, &n, fp);
525
526   while (read != -1) {
527
528     /* Wipeout the new line character */
529     line[read - 1] = '\0';
530   
531     if(n == 0 || strlen(line) == 0){
532       read = xbt_getline(&line, &n, fp);
533       continue;
534     }
535
536     xbt_str_ltrim(line, NULL);
537     xbt_str_strip_spaces(line);
538     
539     if(line[0] != '<'){
540       read = xbt_getline(&line, &n, fp);
541       continue;
542     }
543     
544     xbt_dynar_free(&split);
545     split = xbt_str_split(line, " ");
546
547     /* Get node type */
548     node_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
549
550     if(strcmp(node_type, "(DW_TAG_subprogram)") == 0){ /* New frame */
551
552       dw_frame_t frame = NULL;
553
554       strtok(xbt_dynar_get_as(split, 0, char *), "<");
555       subprogram_start = xbt_strdup(strtok(NULL, "<"));
556       xbt_str_rtrim(subprogram_start, ">:");
557
558       read = xbt_getline(&line, &n, fp);
559    
560       while(read != -1){
561
562         /* Wipeout the new line character */
563         line[read - 1] = '\0';
564
565         if(n == 0 || strlen(line) == 0){
566           read = xbt_getline(&line, &n, fp);
567           continue;
568         }
569         
570         xbt_dynar_free(&split);
571         xbt_str_rtrim(line, NULL);
572         xbt_str_strip_spaces(line);
573         split = xbt_str_split(line, " ");
574           
575         node_type = xbt_dynar_get_as(split, 1, char *);
576
577         if(strncmp(node_type, "DW_AT_", 6) != 0)
578           break;
579
580         if(strcmp(node_type, "DW_AT_sibling") == 0){
581
582           subprogram_end = xbt_strdup(xbt_dynar_get_as(split, 3, char*));
583           xbt_str_ltrim(subprogram_end, "<0x");
584           xbt_str_rtrim(subprogram_end, ">");
585           
586         }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){ /* Frame already in dict */
587           
588           new_frame = 0;
589           abstract_origin = xbt_strdup(xbt_dynar_get_as(split, 2, char*));
590           xbt_str_ltrim(abstract_origin, "<0x");
591           xbt_str_rtrim(abstract_origin, ">");
592           subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, abstract_origin);
593           frame = xbt_dict_get_or_null(*local_variables, subprogram_name); 
594           xbt_free(abstract_origin);
595
596         }else if(strcmp(node_type, "DW_AT_name") == 0){
597
598           new_frame = 1;
599           xbt_free(current_frame);
600           frame = xbt_new0(s_dw_frame_t, 1);
601           frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *)); 
602           frame->variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
603           frame->frame_base = xbt_new0(s_dw_location_t, 1); 
604           current_frame = strdup(frame->name);
605
606           xbt_dict_set(subprograms_origin, subprogram_start, xbt_strdup(frame->name), NULL);
607         
608         }else if(strcmp(node_type, "DW_AT_frame_base") == 0){
609
610           location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
611
612           if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
613
614             frame->frame_base = MC_dwarf_get_location(location_list, xbt_dynar_get_as(split, 3, char *));
615              
616           }else{
617                 
618             xbt_str_strip_spaces(line);
619             split2 = xbt_str_split(line, "(");
620             xbt_dynar_remove_at(split2, 0, NULL);
621             loc_expr = xbt_str_join(split2, " ");
622             xbt_str_rtrim(loc_expr, ")");
623             frame->frame_base = MC_dwarf_get_location(NULL, loc_expr);
624             xbt_dynar_free(&split2);
625             xbt_free(loc_expr);
626
627           }
628  
629         }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
630           
631           if(frame != NULL)
632             frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
633
634         }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
635
636           if(frame != NULL)
637             frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
638
639         }else if(strcmp(node_type, "DW_AT_MIPS_linkage_name:") == 0){
640
641           xbt_free(frame->name);
642           xbt_free(current_frame);
643           frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));   
644           current_frame = strdup(frame->name);
645           xbt_dict_set(subprograms_origin, subprogram_start, xbt_strdup(frame->name), NULL);
646
647         }
648
649         read = xbt_getline(&line, &n, fp);
650
651       }
652  
653       if(new_frame == 1){
654         frame->start = strtoul(subprogram_start, NULL, 16);
655         if(subprogram_end != NULL)
656           frame->end = strtoul(subprogram_end, NULL, 16);
657         xbt_dict_set(*local_variables, frame->name, frame, NULL);
658       }
659
660       xbt_free(subprogram_start);
661       xbt_free(subprogram_end);
662       subprogram_end = NULL;
663         
664
665     }else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
666
667       dw_variable_t var = NULL;
668       
669       parent_value = strdup(xbt_dynar_get_as(split, 0, char *));
670       parent_value = strtok(parent_value,"<");
671       xbt_str_rtrim(parent_value, ">");
672       parent = atoi(parent_value);
673       xbt_free(parent_value);
674
675       if(parent == 1)
676         global_variable = 1;
677     
678       strtok(xbt_dynar_get_as(split, 0, char *), "<");
679       origin = xbt_strdup(strtok(NULL, "<"));
680       xbt_str_rtrim(origin, ">:");
681       
682       read = xbt_getline(&line, &n, fp);
683       
684       while(read != -1){
685
686         /* Wipeout the new line character */
687         line[read - 1] = '\0'; 
688
689         if(n == 0 || strlen(line) == 0){
690           read = xbt_getline(&line, &n, fp);
691           continue;
692         }
693     
694         xbt_dynar_free(&split);
695         xbt_str_rtrim(line, NULL);
696         xbt_str_strip_spaces(line);
697         split = xbt_str_split(line, " ");
698   
699         node_type = xbt_dynar_get_as(split, 1, char *);
700
701         if(strncmp(node_type, "DW_AT_", 6) != 0)
702           break;
703
704         if(strcmp(node_type, "DW_AT_name") == 0){
705
706           var = xbt_new0(s_dw_variable_t, 1);
707           var->name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
708           xbt_dict_set(variables_origin, origin, xbt_strdup(var->name), NULL);
709          
710         }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
711
712           new_variable = 0;
713
714           abstract_origin = xbt_dynar_get_as(split, 2, char *);
715           xbt_str_ltrim(abstract_origin, "<0x");
716           xbt_str_rtrim(abstract_origin, ">");
717           
718           variable_name = (char *)xbt_dict_get_or_null(variables_origin, abstract_origin);
719           variable_frame = MC_dwarf_get_frame_by_offset(*local_variables, strtoul(abstract_origin, NULL, 16));
720           var = MC_dwarf_get_variable_by_name(variable_frame, variable_name); 
721
722         }else if(strcmp(node_type, "DW_AT_location") == 0){
723
724           if(var != NULL){
725
726             if(!global_variable){
727
728               location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
729
730               if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
731                 var->address.location = MC_dwarf_get_location(location_list, xbt_dynar_get_as(split, 3, char *));
732               }else{
733                 xbt_str_strip_spaces(line);
734                 split2 = xbt_str_split(line, "(");
735                 xbt_dynar_remove_at(split2, 0, NULL);
736                 loc_expr = xbt_str_join(split2, " ");
737                 xbt_str_rtrim(loc_expr, ")");
738                 if(strncmp("DW_OP_addr", loc_expr, 10) == 0){
739                   global_variable = 1;
740                   xbt_dynar_free(&split2);
741                   split2 = xbt_str_split(loc_expr, " ");
742                   if(strcmp(elf_file, xbt_binary_name) != 0)
743                     var->address.address = (char *)start_text_libsimgrid + (long)((void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16));
744                   else
745                     var->address.address = (void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16);
746                 }else{
747                   var->address.location = MC_dwarf_get_location(NULL, loc_expr);
748                 }
749                 xbt_dynar_free(&split2);
750                 xbt_free(loc_expr);
751               }
752             }else{
753               global_address = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
754               xbt_str_rtrim(global_address, ")");
755               if(strcmp(elf_file, xbt_binary_name) != 0)
756                 var->address.address = (char *)start_text_libsimgrid + (long)((void *)strtoul(global_address, NULL, 16));
757               else
758                 var->address.address = (void *)strtoul(global_address, NULL, 16);
759               xbt_free(global_address);
760               global_address = NULL;
761             }
762
763           }
764                    
765         }else if(strcmp(node_type, "DW_AT_type") == 0){
766           
767           type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
768           xbt_str_ltrim(type_origin, "<0x");
769           xbt_str_rtrim(type_origin, ">");
770         
771         }else if(strcmp(node_type, "DW_AT_declaration") == 0){
772
773           new_variable = 0;
774           if(new_variable){
775             dw_variable_free(var);
776             var = NULL;
777           }
778         
779         }else if(strcmp(node_type, "DW_AT_artificial") == 0){
780           
781           new_variable = 0;
782           if(new_variable){
783             dw_variable_free(var);
784             var = NULL;
785           }
786         
787         }
788
789         read = xbt_getline(&line, &n, fp);
790  
791       }
792
793       if(new_variable == 1){
794         
795         if(!global_variable){
796           variable_frame = xbt_dict_get_or_null(*local_variables, current_frame);
797           var->type_origin = strdup(type_origin);
798           var->global = 0;
799           index = MC_dwarf_get_variable_index(variable_frame->variables, var->name, NULL);
800           if(index != -1)
801             xbt_dynar_insert_at(variable_frame->variables, index, &var);
802         }else{
803           var->type_origin = strdup(type_origin);
804           var->global = 1;
805           index = MC_dwarf_get_variable_index(*global_variables, var->name, var->address.address);
806           if(index != -1)
807             xbt_dynar_insert_at(*global_variables, index, &var); 
808         }
809
810          xbt_free(type_origin);
811          type_origin = NULL;
812       }
813
814       global_variable = 0;
815       new_variable = 1;
816
817     }else if(strcmp(node_type, "(DW_TAG_inlined_subroutine)") == 0){
818
819       read = xbt_getline(&line, &n, fp);
820
821       while(read != -1){
822
823         /* Wipeout the new line character */
824         line[read - 1] = '\0'; 
825
826         if(n == 0 || strlen(line) == 0){
827           read = xbt_getline(&line, &n, fp);
828           continue;
829         }
830
831         xbt_dynar_free(&split);
832         xbt_str_rtrim(line, NULL);
833         xbt_str_strip_spaces(line);
834         split = xbt_str_split(line, " ");
835         
836         if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
837           break;
838           
839         node_type = xbt_dynar_get_as(split, 1, char *);
840
841         if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
842
843           origin = xbt_dynar_get_as(split, 2, char *);
844           xbt_str_ltrim(origin, "<0x");
845           xbt_str_rtrim(origin, ">");
846           
847           subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, origin);
848           subroutine_frame = xbt_dict_get_or_null(*local_variables, subprogram_name);
849         
850         }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
851
852           subroutine_frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
853
854         }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
855
856           subroutine_frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
857         }
858
859         read = xbt_getline(&line, &n, fp);
860       
861       }
862
863     }else if(strcmp(node_type, "(DW_TAG_base_type)") == 0 
864              || strcmp(node_type, "(DW_TAG_enumeration_type)") == 0
865              || strcmp(node_type, "(DW_TAG_enumerator)") == 0
866              || strcmp(node_type, "(DW_TAG_typedef)") == 0
867              || strcmp(node_type, "(DW_TAG_const_type)") == 0
868              || strcmp(node_type, "(DW_TAG_subroutine_type)") == 0
869              || strcmp(node_type, "(DW_TAG_volatile_type)") == 0
870              || (is_pointer = !strcmp(node_type, "(DW_TAG_pointer_type)"))){
871
872       if(strcmp(node_type, "(DW_TAG_base_type)") == 0)
873         type_type = e_dw_base_type;
874       else if(strcmp(node_type, "(DW_TAG_enumeration_type)") == 0)
875         type_type = e_dw_enumeration_type;
876       else if(strcmp(node_type, "(DW_TAG_enumerator)") == 0)
877         type_type = e_dw_enumerator;
878       else if(strcmp(node_type, "(DW_TAG_typedef)") == 0)
879         type_type = e_dw_typedef;
880       else if(strcmp(node_type, "(DW_TAG_const_type)") == 0)
881         type_type = e_dw_const_type;
882       else if(strcmp(node_type, "(DW_TAG_pointer_type)") == 0)
883         type_type = e_dw_pointer_type;
884       else if(strcmp(node_type, "(DW_TAG_subroutine_type)") == 0)
885         type_type = e_dw_subroutine_type;
886       else if(strcmp(node_type, "(DW_TAG_volatile_type)") == 0)
887         type_type = e_dw_volatile_type;
888
889       strtok(xbt_dynar_get_as(split, 0, char *), "<");
890       origin = strdup(strtok(NULL, "<"));
891       xbt_str_rtrim(origin, ">:");
892       
893       read = xbt_getline(&line, &n, fp);
894       
895       while(read != -1){
896         
897          /* Wipeout the new line character */
898         line[read - 1] = '\0'; 
899
900         if(n == 0 || strlen(line) == 0){
901           read = xbt_getline(&line, &n, fp);
902           continue;
903         }
904
905         xbt_dynar_free(&split);
906         xbt_str_rtrim(line, NULL);
907         xbt_str_strip_spaces(line);
908         split = xbt_str_split(line, " ");
909         
910         if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
911           break;
912
913         node_type = xbt_dynar_get_as(split, 1, char *);
914
915         if(strcmp(node_type, "DW_AT_byte_size") == 0){
916           size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
917           if(type_type == e_dw_enumeration_type)
918             enumeration_size = size;
919         }else if(strcmp(node_type, "DW_AT_name") == 0){
920           end = xbt_str_join(split, " ");
921           xbt_dynar_free(&split);
922           split = xbt_str_split(end, "):");
923           xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
924           name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
925         }else if(strcmp(node_type, "DW_AT_type") == 0){
926           type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
927           xbt_str_ltrim(type_origin, "<0x");
928           xbt_str_rtrim(type_origin, ">");
929         }
930         
931         read = xbt_getline(&line, &n, fp);
932       }
933
934       dw_type_t type = xbt_new0(s_dw_type_t, 1);
935       type->type = type_type;
936       if(name)
937         type->name = xbt_strdup(name);
938       else
939         type->name = xbt_strdup("undefined");
940       type->is_pointer_type = is_pointer;
941       type->id = (void *)strtoul(origin, NULL, 16);
942       if(type_origin)
943         type->dw_type_id = xbt_strdup(type_origin);
944       if(type_type == e_dw_enumerator)
945         type->size = enumeration_size;
946       else
947         type->size = size;
948       type->members = NULL;
949
950       xbt_dict_set(*types, origin, type, NULL); 
951
952       xbt_free(name);
953       name = NULL;
954       xbt_free(type_origin);
955       type_origin = NULL;
956       xbt_free(end);
957       end = NULL;
958
959       is_pointer = 0;
960       size = 0;
961       xbt_free(origin);
962
963     }else if(strcmp(node_type, "(DW_TAG_structure_type)") == 0 || strcmp(node_type, "(DW_TAG_union_type)") == 0){
964       
965       if(strcmp(node_type, "(DW_TAG_structure_type)") == 0)
966         struct_decl = 1;
967       else
968         union_decl = 1;
969
970       strtok(xbt_dynar_get_as(split, 0, char *), "<");
971       origin = strdup(strtok(NULL, "<"));
972       xbt_str_rtrim(origin, ">:");
973       
974       read = xbt_getline(&line, &n, fp);
975
976       dw_type_t type = NULL;
977
978       while(read != -1){
979       
980         while(read != -1){
981         
982           /* Wipeout the new line character */
983           line[read - 1] = '\0'; 
984
985           if(n == 0 || strlen(line) == 0){
986             read = xbt_getline(&line, &n, fp);
987             continue;
988           }
989
990           xbt_dynar_free(&split);
991           xbt_str_rtrim(line, NULL);
992           xbt_str_strip_spaces(line);
993           split = xbt_str_split(line, " ");
994         
995           node_type = xbt_dynar_get_as(split, 1, char *);
996
997           if(strncmp(node_type, "DW_AT_", 6) != 0){
998             member_end = 1;
999             break;
1000           }
1001
1002           if(strcmp(node_type, "DW_AT_byte_size") == 0){
1003             size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1004           }else if(strcmp(node_type, "DW_AT_name") == 0){
1005             xbt_free(end);
1006             end = xbt_str_join(split, " ");
1007             xbt_dynar_free(&split);
1008             split = xbt_str_split(end, "):");
1009             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
1010             name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
1011           }else if(strcmp(node_type, "DW_AT_type") == 0){
1012             type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
1013             xbt_str_ltrim(type_origin, "<0x");
1014             xbt_str_rtrim(type_origin, ">");
1015           }else if(strcmp(node_type, "DW_AT_data_member_location:") == 0){
1016             xbt_free(end);
1017             end = xbt_str_join(split, " ");
1018             xbt_dynar_free(&split);
1019             split = xbt_str_split(end, "DW_OP_plus_uconst:");
1020             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), NULL);
1021             xbt_str_rtrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), ")");
1022             offset = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1023           }
1024
1025           read = xbt_getline(&line, &n, fp);
1026           
1027         }
1028
1029         if(member_end && type){         
1030           member_end = 0;
1031           
1032           dw_type_t member_type = xbt_new0(s_dw_type_t, 1);
1033           member_type->name = xbt_strdup(name);
1034           member_type->size = size;
1035           member_type->is_pointer_type = is_pointer;
1036           member_type->id = (void *)strtoul(origin, NULL, 16);
1037           member_type->offset = offset;
1038           if(type_origin)
1039             member_type->dw_type_id = xbt_strdup(type_origin);
1040
1041           xbt_dynar_push(type->members, &member_type);
1042
1043           xbt_free(name);
1044           name = NULL;
1045           xbt_free(end);
1046           end = NULL;
1047           xbt_free(type_origin);
1048           type_origin = NULL;
1049           size = 0;
1050           offset = 0;
1051
1052           xbt_free(origin);
1053           origin = NULL;
1054           strtok(xbt_dynar_get_as(split, 0, char *), "<");
1055           origin = strdup(strtok(NULL, "<"));
1056           xbt_str_rtrim(origin, ">:");
1057
1058         }
1059
1060         if(struct_decl || union_decl){
1061           type = xbt_new0(s_dw_type_t, 1);
1062           if(struct_decl)
1063             type->type = e_dw_structure_type;
1064           else
1065             type->type = e_dw_union_type;
1066           type->name = xbt_strdup(name);
1067           type->size = size;
1068           type->is_pointer_type = is_pointer;
1069           type->id = (void *)strtoul(origin, NULL, 16);
1070           if(type_origin)
1071             type->dw_type_id = xbt_strdup(type_origin);
1072           type->members = xbt_dynar_new(sizeof(dw_type_t), dw_type_free_voidp);
1073           
1074           xbt_dict_set(*types, origin, type, NULL); 
1075           
1076           xbt_free(name);
1077           name = NULL;
1078           xbt_free(end);
1079           end = NULL;
1080           xbt_free(type_origin);
1081           type_origin = NULL;
1082           size = 0;
1083           struct_decl = 0;
1084           union_decl = 0;
1085
1086         }
1087
1088         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_member)") != 0)
1089           break;  
1090
1091         read = xbt_getline(&line, &n, fp);
1092     
1093       }
1094
1095       xbt_free(origin);
1096       origin = NULL;
1097
1098     }else if(strcmp(node_type, "(DW_TAG_array_type)") == 0){
1099       
1100       strtok(xbt_dynar_get_as(split, 0, char *), "<");
1101       origin = strdup(strtok(NULL, "<"));
1102       xbt_str_rtrim(origin, ">:");
1103       
1104       read = xbt_getline(&line, &n, fp);
1105
1106       dw_type_t type = NULL;
1107
1108       while(read != -1){
1109       
1110         while(read != -1){
1111         
1112           /* Wipeout the new line character */
1113           line[read - 1] = '\0'; 
1114
1115           if(n == 0 || strlen(line) == 0){
1116             read = xbt_getline(&line, &n, fp);
1117             continue;
1118           }
1119
1120           xbt_dynar_free(&split);
1121           xbt_str_rtrim(line, NULL);
1122           xbt_str_strip_spaces(line);
1123           split = xbt_str_split(line, " ");
1124         
1125           node_type = xbt_dynar_get_as(split, 1, char *);
1126
1127           if(strncmp(node_type, "DW_AT_", 6) != 0)
1128             break;
1129
1130           if(strcmp(node_type, "DW_AT_upper_bound") == 0){
1131             size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1132           }else if(strcmp(node_type, "DW_AT_name") == 0){
1133             end = xbt_str_join(split, " ");
1134             xbt_dynar_free(&split);
1135             split = xbt_str_split(end, "):");
1136             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
1137             name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
1138           }else if(strcmp(node_type, "DW_AT_type") == 0){
1139             type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
1140             xbt_str_ltrim(type_origin, "<0x");
1141             xbt_str_rtrim(type_origin, ">");
1142           }
1143
1144           read = xbt_getline(&line, &n, fp);
1145           
1146         }
1147
1148         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_subrange_type)") == 0){
1149           subrange = 1;         
1150         }
1151
1152         if(subrange && type){         
1153           type->size = size;
1154       
1155           xbt_free(name);
1156           name = NULL;
1157           xbt_free(end);
1158           end = NULL;
1159           xbt_free(type_origin);
1160           type_origin = NULL;
1161           size = 0;
1162
1163           xbt_free(origin);
1164           origin = NULL;
1165           strtok(xbt_dynar_get_as(split, 0, char *), "<");
1166           origin = strdup(strtok(NULL, "<"));
1167           xbt_str_rtrim(origin, ">:");
1168
1169         }else {
1170           
1171           type = xbt_new0(s_dw_type_t, 1);
1172           type->type = e_dw_array_type;
1173           type->name = xbt_strdup(name);
1174           type->is_pointer_type = is_pointer;
1175           type->id = (void *)strtoul(origin, NULL, 16);
1176           if(type_origin)
1177             type->dw_type_id = xbt_strdup(type_origin);
1178           type->members = NULL;
1179           
1180           xbt_dict_set(*types, origin, type, NULL); 
1181           
1182           xbt_free(name);
1183           name = NULL;
1184           xbt_free(end);
1185           end = NULL;
1186           xbt_free(type_origin);
1187           type_origin = NULL;
1188           size = 0;
1189         }
1190
1191         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_subrange_type)") != 0)
1192           break;  
1193
1194         read = xbt_getline(&line, &n, fp);
1195     
1196       }
1197
1198       xbt_free(origin);
1199       origin = NULL;
1200
1201     }else{
1202
1203       read = xbt_getline(&line, &n, fp);
1204
1205     }
1206
1207   }
1208   
1209   xbt_dynar_free(&split);
1210   xbt_dict_free(&variables_origin);
1211   xbt_dict_free(&subprograms_origin);
1212   xbt_free(line);
1213   xbt_free(command);
1214   pclose(fp);
1215   
1216 }
1217
1218
1219 /*******************************  Ignore mechanism *******************************/
1220 /*********************************************************************************/
1221
1222 typedef struct s_mc_stack_ignore_variable{
1223   int in_libsimgrid;
1224   char *var_name;
1225   char *frame;
1226 }s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
1227
1228 typedef struct s_mc_data_bss_ignore_variable{
1229   int in_libsimgrid;
1230   char *name;
1231 }s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t;
1232
1233 /**************************** Free functions ******************************/
1234
1235 static void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
1236   xbt_free(v->var_name);
1237   xbt_free(v->frame);
1238   xbt_free(v);
1239 }
1240
1241 static void stack_ignore_variable_free_voidp(void *v){
1242   stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
1243 }
1244
1245 void heap_ignore_region_free(mc_heap_ignore_region_t r){
1246   xbt_free(r);
1247 }
1248
1249 void heap_ignore_region_free_voidp(void *r){
1250   heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
1251 }
1252
1253 static void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v){
1254   xbt_free(v->name);
1255   xbt_free(v);
1256 }
1257
1258 static void data_bss_ignore_variable_free_voidp(void *v){
1259   data_bss_ignore_variable_free((mc_data_bss_ignore_variable_t) * (void **) v);
1260 }
1261
1262 /***********************************************************************/
1263
1264 void MC_ignore_heap(void *address, size_t size){
1265
1266   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1267
1268   MC_SET_RAW_MEM;
1269
1270   mc_heap_ignore_region_t region = NULL;
1271   region = xbt_new0(s_mc_heap_ignore_region_t, 1);
1272   region->address = address;
1273   region->size = size;
1274   
1275   region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
1276   
1277   if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
1278     region->fragment = -1;
1279     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
1280   }else{
1281     region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
1282     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
1283   }
1284   
1285   if(mc_heap_comparison_ignore == NULL){
1286     mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
1287     xbt_dynar_push(mc_heap_comparison_ignore, &region);
1288     if(!raw_mem_set)
1289       MC_UNSET_RAW_MEM;
1290     return;
1291   }
1292
1293   unsigned int cursor = 0;
1294   mc_heap_ignore_region_t current_region = NULL;
1295   int start = 0;
1296   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
1297   
1298   while(start <= end){
1299     cursor = (start + end) / 2;
1300     current_region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
1301     if(current_region->address == address){
1302       heap_ignore_region_free(region);
1303       if(!raw_mem_set)
1304         MC_UNSET_RAW_MEM;
1305       return;
1306     }
1307     if(current_region->address < address)
1308       start = cursor + 1;
1309     if(current_region->address > address)
1310       end = cursor - 1;   
1311   }
1312
1313   if(current_region->address < address)
1314     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
1315   else
1316     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
1317
1318   MC_UNSET_RAW_MEM;
1319
1320   if(raw_mem_set)
1321     MC_SET_RAW_MEM;
1322 }
1323
1324 void MC_remove_ignore_heap(void *address, size_t size){
1325
1326   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1327
1328   MC_SET_RAW_MEM;
1329
1330   unsigned int cursor = 0;
1331   int start = 0;
1332   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
1333   mc_heap_ignore_region_t region;
1334   int ignore_found = 0;
1335
1336   while(start <= end){
1337     cursor = (start + end) / 2;
1338     region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
1339     if(region->address == address){
1340       ignore_found = 1;
1341       break;
1342     }
1343     if(region->address < address)
1344       start = cursor + 1;
1345     if(region->address > address){
1346       if((char * )region->address <= ((char *)address + size)){
1347         ignore_found = 1;
1348         break;
1349       }else
1350         end = cursor - 1;   
1351     }
1352   }
1353   
1354   if(ignore_found == 1){
1355     xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
1356     MC_remove_ignore_heap(address, size);
1357   }
1358
1359   MC_UNSET_RAW_MEM;
1360   
1361   if(raw_mem_set)
1362     MC_SET_RAW_MEM;
1363
1364 }
1365
1366 void MC_ignore_global_variable(const char *name,  ...){
1367
1368   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1369
1370   MC_SET_RAW_MEM;
1371
1372   va_list ap;
1373   va_start(ap, name);
1374   int in_libsimgrid = va_arg(ap, int);
1375   va_end(ap);
1376
1377   xbt_dynar_t variables = NULL;
1378
1379   if(in_libsimgrid == 1){
1380     variables = mc_global_variables_libsimgrid;
1381   }else{
1382     variables = mc_global_variables_binary;
1383   }
1384
1385   if(variables){
1386
1387     unsigned int cursor = 0;
1388     dw_variable_t current_var;
1389     int start = 0;
1390     int end = xbt_dynar_length(variables) - 1;
1391     int var_found;
1392
1393     while(start <= end){
1394       cursor = (start + end) /2;
1395       current_var = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t);
1396       if(strcmp(current_var->name, name) == 0){
1397         xbt_dynar_remove_at(variables, cursor, NULL);
1398         var_found = 1;
1399         break;
1400       }else if(strcmp(current_var->name, name) < 0){
1401         start = cursor + 1;
1402       }else{
1403         end = cursor - 1;
1404       } 
1405     }
1406
1407     if(var_found){
1408       if(in_libsimgrid == 1)
1409         MC_ignore_global_variable(name, 1);
1410       else 
1411         MC_ignore_global_variable(name);
1412     }
1413     
1414   }else{
1415
1416     if(mc_data_bss_comparison_ignore == NULL)
1417       mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), data_bss_ignore_variable_free_voidp);
1418
1419     mc_data_bss_ignore_variable_t var = NULL;
1420     var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
1421     var->name = strdup(name);
1422     var->in_libsimgrid = (in_libsimgrid == 1);
1423
1424     if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
1425
1426       xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
1427
1428     }else{
1429     
1430       unsigned int cursor = 0;
1431       int start = 0;
1432       int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
1433       mc_data_bss_ignore_variable_t current_var = NULL;
1434
1435       while(start <= end){
1436         cursor = (start + end) / 2;
1437         current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
1438         if(strcmp(current_var->name, name) == 0){
1439           data_bss_ignore_variable_free(var);
1440           if(!raw_mem_set)
1441             MC_UNSET_RAW_MEM;
1442           return;
1443         }else if(strcmp(current_var->name, name) < 0){
1444           start = cursor + 1;
1445         }else{
1446           end = cursor - 1;
1447         }
1448       }
1449
1450       if(strcmp(current_var->name, name) < 0)
1451         xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
1452       else
1453         xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);
1454
1455     }
1456   }
1457
1458   MC_UNSET_RAW_MEM;
1459
1460   if(raw_mem_set)
1461     MC_SET_RAW_MEM;
1462 }
1463
1464 void MC_ignore_local_variable(const char *var_name, const char *frame_name, ...){
1465   
1466   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1467
1468   MC_SET_RAW_MEM;
1469
1470   va_list ap;
1471   va_start(ap, frame_name);
1472   int in_libsimgrid = va_arg(ap, int);
1473   va_end(ap);
1474
1475   xbt_dict_t variables = NULL;
1476
1477   if(in_libsimgrid == 1){
1478     variables = mc_local_variables_libsimgrid;
1479   }else{
1480     variables = mc_local_variables_binary;
1481   }
1482
1483   if(variables){
1484     unsigned int cursor = 0;
1485     dw_variable_t current_var;
1486     int start, end;
1487     if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames (binary and libsimgrid) */
1488       xbt_dict_cursor_t dict_cursor, dict_cursor2;
1489       char *current_frame_name;
1490       dw_frame_t frame;
1491       xbt_dict_foreach(mc_local_variables_libsimgrid, dict_cursor, current_frame_name, frame){
1492         start = 0;
1493         end = xbt_dynar_length(frame->variables) - 1;
1494         while(start <= end){
1495           cursor = (start + end) / 2;
1496           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);          
1497           if(strcmp(current_var->name, var_name) == 0){
1498             xbt_dynar_remove_at(frame->variables, cursor, NULL);
1499             start = 0;
1500             end = xbt_dynar_length(frame->variables) - 1;
1501           }else if(strcmp(current_var->name, var_name) < 0){
1502             start = cursor + 1;
1503           }else{
1504             end = cursor - 1;
1505           } 
1506         }
1507       }
1508       xbt_dict_foreach(mc_local_variables_binary, dict_cursor2, current_frame_name, frame){
1509         start = 0;
1510         end = xbt_dynar_length(frame->variables) - 1;
1511         while(start <= end){
1512           cursor = (start + end) / 2;
1513           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
1514           if(strcmp(current_var->name, var_name) == 0){
1515             xbt_dynar_remove_at(frame->variables, cursor, NULL);
1516             start = 0;
1517             end = xbt_dynar_length(frame->variables) - 1;
1518           }else if(strcmp(current_var->name, var_name) < 0){
1519             start = cursor + 1;
1520           }else{
1521             end = cursor - 1;
1522           } 
1523         }
1524       }
1525     }else{
1526       xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(variables, frame_name))->variables;
1527       start = 0;
1528       end = xbt_dynar_length(variables_list) - 1;
1529       while(start <= end){
1530         cursor = (start + end) / 2;
1531         current_var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor, dw_variable_t);
1532         if(strcmp(current_var->name, var_name) == 0){
1533           xbt_dynar_remove_at(variables_list, cursor, NULL);
1534           start = 0;
1535           end = xbt_dynar_length(variables_list) - 1;
1536         }else if(strcmp(current_var->name, var_name) < 0){
1537           start = cursor + 1;
1538         }else{
1539           end = cursor - 1;
1540         } 
1541       }
1542     } 
1543   }else{
1544
1545     if(mc_stack_comparison_ignore == NULL)
1546       mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), stack_ignore_variable_free_voidp);
1547   
1548     mc_stack_ignore_variable_t var = NULL;
1549     var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
1550     var->in_libsimgrid = (in_libsimgrid == 1);
1551     var->var_name = strdup(var_name);
1552     var->frame = strdup(frame_name);
1553   
1554     if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){
1555
1556       xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
1557
1558     }else{
1559     
1560       unsigned int cursor = 0;
1561       int start = 0;
1562       int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
1563       mc_stack_ignore_variable_t current_var = NULL;
1564
1565       while(start <= end){
1566         cursor = (start + end) / 2;
1567         current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
1568         if(strcmp(current_var->frame, frame_name) == 0){
1569           if(strcmp(current_var->var_name, var_name) == 0){
1570             stack_ignore_variable_free(var);
1571             if(!raw_mem_set)
1572               MC_UNSET_RAW_MEM;
1573             return;
1574           }
1575           if(strcmp(current_var->var_name, var_name) < 0)
1576             start = cursor + 1;
1577           if(strcmp(current_var->var_name, var_name) > 0)
1578             end = cursor - 1;
1579         }
1580         if(strcmp(current_var->frame, frame_name) < 0)
1581           start = cursor + 1;
1582         if(strcmp(current_var->frame, frame_name) > 0)
1583           end = cursor - 1;
1584       }
1585
1586       if(strcmp(current_var->frame, frame_name) < 0)
1587         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
1588       else
1589         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
1590
1591     }
1592   }
1593
1594   MC_UNSET_RAW_MEM;
1595   
1596   if(raw_mem_set)
1597     MC_SET_RAW_MEM;
1598
1599 }
1600
1601 void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
1602
1603   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1604
1605   MC_SET_RAW_MEM;
1606   if(stacks_areas == NULL)
1607     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
1608   
1609   stack_region_t region = NULL;
1610   region = xbt_new0(s_stack_region_t, 1);
1611   region->address = stack;
1612   region->process_name = strdup(name);
1613   region->context = context;
1614   region->size = size;
1615   region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
1616   xbt_dynar_push(stacks_areas, &region);
1617   
1618   MC_UNSET_RAW_MEM;
1619
1620   if(raw_mem_set)
1621     MC_SET_RAW_MEM;
1622 }
1623
1624 /*******************************  Initialisation of MC *******************************/
1625 /*********************************************************************************/
1626
1627 static void MC_dump_ignored_local_variables(void){
1628
1629   if(mc_stack_comparison_ignore == NULL || xbt_dynar_is_empty(mc_stack_comparison_ignore))
1630     return;
1631
1632   unsigned int cursor = 0;
1633   mc_stack_ignore_variable_t current_var;
1634   xbt_dict_t variables;
1635
1636   xbt_dynar_foreach(mc_stack_comparison_ignore, cursor, current_var){
1637
1638     if(current_var->in_libsimgrid == 1){
1639       variables = mc_local_variables_libsimgrid;
1640     }else{
1641       variables = mc_local_variables_binary;
1642     }
1643
1644     unsigned int cursor2 = 0;
1645     dw_variable_t var;
1646     int start, end;
1647
1648     if(strcmp(current_var->frame, "*") == 0){
1649       xbt_dict_cursor_t dict_cursor;
1650       char *frame_name;
1651       dw_frame_t frame;
1652       xbt_dict_foreach(variables, dict_cursor, frame_name, frame){
1653         start = 0;
1654         end = xbt_dynar_length(frame->variables) - 1;
1655         while(start <= end){
1656           cursor2 = (start + end) / 2;
1657           var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor2, dw_variable_t);
1658           if(strcmp(var->name, current_var->var_name) == 0){
1659             xbt_dynar_remove_at(frame->variables, cursor2, NULL);
1660             start = 0;
1661             end = xbt_dynar_length(frame->variables) - 1;
1662           }else if(strcmp(var->name, current_var->var_name) < 0){
1663             start = cursor2 + 1;
1664           }else{
1665             end = cursor2 - 1;
1666           } 
1667         }
1668       }
1669     }else{
1670       xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(variables, current_var->frame))->variables;
1671       start = 0;
1672       end = xbt_dynar_length(variables_list) - 1;
1673       while(start <= end){
1674         cursor2 = (start + end) / 2;
1675         var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor2, dw_variable_t);
1676         if(strcmp(var->name, current_var->var_name) == 0){
1677           xbt_dynar_remove_at(variables_list, cursor2, NULL);
1678           start = 0;
1679           end = xbt_dynar_length(variables_list) - 1; 
1680         }else if(strcmp(var->name, current_var->var_name) < 0){
1681           start = cursor2 + 1;
1682         }else{
1683           end = cursor2 - 1;
1684         } 
1685       }
1686     } 
1687   }
1688
1689   xbt_dynar_free(&mc_stack_comparison_ignore);
1690   mc_stack_comparison_ignore = NULL;
1691  
1692 }
1693
1694 static void MC_dump_ignored_global_variables(void){
1695
1696   if(mc_data_bss_comparison_ignore == NULL || xbt_dynar_is_empty(mc_data_bss_comparison_ignore))
1697     return;
1698
1699   unsigned int cursor = 0;
1700   mc_data_bss_ignore_variable_t current_var;
1701   xbt_dynar_t variables;
1702   
1703   unsigned int cursor2 = 0;
1704   dw_variable_t var;
1705   int start, end;
1706
1707   xbt_dynar_foreach(mc_data_bss_comparison_ignore, cursor, current_var){
1708
1709     if(current_var->in_libsimgrid == 1){
1710       variables = mc_global_variables_libsimgrid;
1711     }else{
1712       variables = mc_global_variables_binary;
1713     }
1714
1715     cursor2 = 0;
1716     start = 0;
1717     end = xbt_dynar_length(variables) - 1;
1718
1719     while(start <= end){
1720       cursor2 = (start + end) / 2;
1721       var = (dw_variable_t)xbt_dynar_get_as(variables, cursor2, dw_variable_t);
1722       if(strcmp(var->name, current_var->name) == 0){
1723         xbt_dynar_remove_at(variables, cursor2, NULL);
1724         return;
1725       }else if(strcmp(var->name, current_var->name) < 0){
1726         start = cursor2 + 1;
1727       }else{
1728         end = cursor2 - 1;
1729       } 
1730     }
1731   } 
1732
1733   xbt_dynar_free(&mc_data_bss_comparison_ignore);
1734   mc_data_bss_comparison_ignore = NULL;
1735   
1736
1737 }
1738
1739 void MC_init(){
1740
1741   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1742   
1743   compare = 0;
1744
1745   /* Initialize the data structures that must be persistent across every
1746      iteration of the model-checker (in RAW memory) */
1747
1748   MC_SET_RAW_MEM;
1749
1750   MC_init_memory_map_info();
1751   
1752   mc_local_variables_libsimgrid = xbt_dict_new_homogeneous(NULL);
1753   mc_local_variables_binary = xbt_dict_new_homogeneous(NULL);
1754   mc_global_variables_libsimgrid = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
1755   mc_global_variables_binary = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
1756   mc_variables_type_libsimgrid = xbt_dict_new_homogeneous(NULL);
1757   mc_variables_type_binary = xbt_dict_new_homogeneous(NULL);
1758
1759   XBT_INFO("Get debug information ...");
1760
1761   /* Get local variables in binary for state equality detection */
1762   xbt_dict_t binary_location_list = MC_dwarf_get_location_list(xbt_binary_name);
1763   MC_dwarf_get_variables(xbt_binary_name, binary_location_list, &mc_local_variables_binary, &mc_global_variables_binary, &mc_variables_type_binary);
1764
1765   /* Get local variables in libsimgrid for state equality detection */
1766   xbt_dict_t libsimgrid_location_list = MC_dwarf_get_location_list(libsimgrid_path);
1767   MC_dwarf_get_variables(libsimgrid_path, libsimgrid_location_list, &mc_local_variables_libsimgrid, &mc_global_variables_libsimgrid, &mc_variables_type_libsimgrid);
1768
1769   xbt_dict_free(&libsimgrid_location_list);
1770   xbt_dict_free(&binary_location_list);
1771
1772   /* Remove variables ignored before getting list of variables */
1773   MC_dump_ignored_local_variables();
1774   MC_dump_ignored_global_variables();
1775   
1776   /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
1777   MC_get_libsimgrid_plt_section();
1778   MC_get_binary_plt_section();
1779
1780   MC_UNSET_RAW_MEM;
1781
1782    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
1783   MC_ignore_local_variable("e", "*");
1784   MC_ignore_local_variable("__ex_cleanup", "*", 1);
1785   MC_ignore_local_variable("__ex_mctx_en", "*", 1);
1786   MC_ignore_local_variable("__ex_mctx_me", "*", 1);
1787   MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*", 1);
1788   MC_ignore_local_variable("_log_ev", "*", 1);
1789   MC_ignore_local_variable("_throw_ctx", "*", 1);
1790   MC_ignore_local_variable("ctx", "*", 1);
1791
1792   MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial", 1);
1793   MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial", 1);
1794
1795   /* Ignore local variable about time used for tracing */
1796   MC_ignore_local_variable("start_time", "*", 1); 
1797
1798   MC_ignore_global_variable("mc_comp_times", 1);
1799   MC_ignore_global_variable("mc_snapshot_comparison_time", 1); 
1800   MC_ignore_global_variable("mc_time", 1);
1801   MC_ignore_global_variable("smpi_current_rank", 1);
1802   MC_ignore_global_variable("smx_current_context_serial", 1);
1803   MC_ignore_global_variable("smx_current_context_key", 1);
1804   MC_ignore_global_variable("sysv_maestro_context", 1);
1805   MC_ignore_global_variable("counter", 1); /* Static variable used for tracing */
1806
1807   if(raw_mem_set)
1808     MC_SET_RAW_MEM;
1809
1810   XBT_INFO("Get debug information done !");
1811
1812 }
1813
1814 static void MC_init_dot_output(){ /* FIXME : more colors */
1815
1816   colors[0] = "blue";
1817   colors[1] = "red";
1818   colors[2] = "green3";
1819   colors[3] = "goldenrod";
1820   colors[4] = "brown";
1821   colors[5] = "purple";
1822   colors[6] = "magenta";
1823   colors[7] = "turquoise4";
1824   colors[8] = "gray25";
1825   colors[9] = "forestgreen";
1826   colors[10] = "hotpink";
1827   colors[11] = "lightblue";
1828   colors[12] = "tan";
1829
1830   dot_output = fopen(_sg_mc_dot_output_file, "w");
1831   
1832   if(dot_output == NULL){
1833     perror("Error open dot output file");
1834     xbt_abort();
1835   }
1836
1837   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");
1838
1839 }
1840
1841 /*******************************  Core of MC *******************************/
1842 /**************************************************************************/
1843
1844 void MC_do_the_modelcheck_for_real() {
1845
1846   MC_SET_RAW_MEM;
1847   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
1848   MC_UNSET_RAW_MEM;
1849   
1850   if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
1851     if (mc_reduce_kind==e_mc_reduce_unset)
1852       mc_reduce_kind=e_mc_reduce_dpor;
1853
1854     XBT_INFO("Check a safety property");
1855     MC_modelcheck_safety();
1856
1857   } else  {
1858
1859     if (mc_reduce_kind==e_mc_reduce_unset)
1860       mc_reduce_kind=e_mc_reduce_none;
1861
1862     XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
1863     MC_automaton_load(_sg_mc_property_file);
1864     MC_modelcheck_liveness();
1865   }
1866 }
1867
1868 void MC_modelcheck_safety(void)
1869 {
1870   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1871
1872   /* Check if MC is already initialized */
1873   if (initial_state_safety)
1874     return;
1875
1876   mc_time = xbt_new0(double, simix_process_maxpid);
1877
1878   /* mc_time refers to clock for each process -> ignore it for heap comparison */  
1879   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1880
1881   /* Initialize the data structures that must be persistent across every
1882      iteration of the model-checker (in RAW memory) */
1883   
1884   MC_SET_RAW_MEM;
1885
1886   /* Initialize statistics */
1887   mc_stats = xbt_new0(s_mc_stats_t, 1);
1888   mc_stats->state_size = 1;
1889
1890   /* Create exploration stack */
1891   mc_stack_safety = xbt_fifo_new();
1892
1893   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1894     MC_init_dot_output();
1895
1896   MC_UNSET_RAW_MEM;
1897
1898   if(_sg_mc_visited > 0){
1899     MC_init();
1900   }else{
1901     MC_SET_RAW_MEM;
1902     MC_init_memory_map_info();
1903     MC_get_libsimgrid_plt_section();
1904     MC_get_binary_plt_section();
1905     MC_UNSET_RAW_MEM;
1906   }
1907
1908   MC_dpor_init();
1909
1910   MC_SET_RAW_MEM;
1911   /* Save the initial state */
1912   initial_state_safety = xbt_new0(s_mc_global_t, 1);
1913   initial_state_safety->snapshot = MC_take_snapshot();
1914   MC_UNSET_RAW_MEM;
1915
1916   MC_dpor();
1917
1918   if(raw_mem_set)
1919     MC_SET_RAW_MEM;
1920
1921   xbt_abort();
1922   //MC_exit();
1923 }
1924
1925 void MC_modelcheck_liveness(){
1926
1927   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1928
1929   MC_init();
1930
1931   mc_time = xbt_new0(double, simix_process_maxpid);
1932
1933   /* mc_time refers to clock for each process -> ignore it for heap comparison */  
1934   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1935  
1936   MC_SET_RAW_MEM;
1937  
1938   /* Initialize statistics */
1939   mc_stats = xbt_new0(s_mc_stats_t, 1);
1940   mc_stats->state_size = 1;
1941
1942   /* Create exploration stack */
1943   mc_stack_liveness = xbt_fifo_new();
1944
1945   /* Create the initial state */
1946   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
1947
1948   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1949     MC_init_dot_output();
1950   
1951   MC_UNSET_RAW_MEM;
1952
1953   MC_ddfs_init();
1954
1955   /* We're done */
1956   MC_print_statistics(mc_stats);
1957   xbt_free(mc_time);
1958
1959   if(raw_mem_set)
1960     MC_SET_RAW_MEM;
1961
1962 }
1963
1964
1965 void MC_exit(void)
1966 {
1967   xbt_free(mc_time);
1968   MC_memory_exit();
1969   //xbt_abort();
1970 }
1971
1972 int SIMIX_pre_mc_random(smx_simcall_t simcall){
1973
1974   return simcall->mc_value;
1975 }
1976
1977
1978 int MC_random(void)
1979 {
1980   /*FIXME: return mc_current_state->executed_transition->random.value;*/
1981   return simcall_mc_random();
1982 }
1983
1984 /**
1985  * \brief Schedules all the process that are ready to run
1986  */
1987 void MC_wait_for_requests(void)
1988 {
1989   smx_process_t process;
1990   smx_simcall_t req;
1991   unsigned int iter;
1992
1993   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
1994     SIMIX_process_runall();
1995     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
1996       req = &process->simcall;
1997       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
1998         SIMIX_simcall_pre(req, 0);
1999     }
2000   }
2001 }
2002
2003 int MC_deadlock_check()
2004 {
2005   int deadlock = FALSE;
2006   smx_process_t process;
2007   if(xbt_swag_size(simix_global->process_list)){
2008     deadlock = TRUE;
2009     xbt_swag_foreach(process, simix_global->process_list){
2010       if(process->simcall.call != SIMCALL_NONE
2011          && MC_request_is_enabled(&process->simcall)){
2012         deadlock = FALSE;
2013         break;
2014       }
2015     }
2016   }
2017   return deadlock;
2018 }
2019
2020 /**
2021  * \brief Re-executes from the state at position start all the transitions indicated by
2022  *        a given model-checker stack.
2023  * \param stack The stack with the transitions to execute.
2024  * \param start Start index to begin the re-execution.
2025  */
2026 void MC_replay(xbt_fifo_t stack, int start)
2027 {
2028   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
2029
2030   int value, i = 1, count = 1;
2031   char *req_str;
2032   smx_simcall_t req = NULL, saved_req = NULL;
2033   xbt_fifo_item_t item, start_item;
2034   mc_state_t state;
2035   smx_process_t process = NULL;
2036
2037   XBT_DEBUG("**** Begin Replay ****");
2038
2039   if(start == -1){
2040     /* Restore the initial state */
2041     MC_restore_snapshot(initial_state_safety->snapshot);
2042     /* At the moment of taking the snapshot the raw heap was set, so restoring
2043      * it will set it back again, we have to unset it to continue  */
2044     MC_UNSET_RAW_MEM;
2045   }
2046
2047   start_item = xbt_fifo_get_last_item(stack);
2048   if(start != -1){
2049     while (i != start){
2050       start_item = xbt_fifo_get_prev_item(start_item);
2051       i++;
2052     }
2053   }
2054
2055   MC_SET_RAW_MEM;
2056   xbt_dict_reset(first_enabled_state);
2057   xbt_swag_foreach(process, simix_global->process_list){
2058     if(MC_process_is_enabled(process)){
2059       char *key = bprintf("%lu", process->pid);
2060       char *data = bprintf("%d", count);
2061       xbt_dict_set(first_enabled_state, key, data, NULL);
2062       xbt_free(key);
2063     }
2064   }
2065   MC_UNSET_RAW_MEM;
2066   
2067
2068   /* Traverse the stack from the state at position start and re-execute the transitions */
2069   for (item = start_item;
2070        item != xbt_fifo_get_first_item(stack);
2071        item = xbt_fifo_get_prev_item(item)) {
2072
2073     state = (mc_state_t) xbt_fifo_get_item_content(item);
2074     saved_req = MC_state_get_executed_request(state, &value);
2075    
2076     MC_SET_RAW_MEM;
2077     char *key = bprintf("%lu", saved_req->issuer->pid);
2078     xbt_dict_remove(first_enabled_state, key); 
2079     xbt_free(key);
2080     MC_UNSET_RAW_MEM;
2081    
2082     if(saved_req){
2083       /* because we got a copy of the executed request, we have to fetch the  
2084          real one, pointed by the request field of the issuer process */
2085       req = &saved_req->issuer->simcall;
2086
2087       /* Debug information */
2088       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2089         req_str = MC_request_to_string(req, value);
2090         XBT_DEBUG("Replay: %s (%p)", req_str, state);
2091         xbt_free(req_str);
2092       }
2093     }
2094     
2095     SIMIX_simcall_pre(req, value);
2096     MC_wait_for_requests();
2097
2098     count++;
2099
2100     MC_SET_RAW_MEM;
2101     /* Insert in dict all enabled processes */
2102     xbt_swag_foreach(process, simix_global->process_list){
2103       if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
2104         char *key = bprintf("%lu", process->pid);
2105         if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
2106           char *data = bprintf("%d", count);
2107           xbt_dict_set(first_enabled_state, key, data, NULL);
2108         }
2109         xbt_free(key);
2110       }
2111     }
2112     MC_UNSET_RAW_MEM;
2113          
2114     /* Update statistics */
2115     mc_stats->visited_states++;
2116     mc_stats->executed_transitions++;
2117
2118   }
2119
2120   XBT_DEBUG("**** End Replay ****");
2121
2122   if(raw_mem)
2123     MC_SET_RAW_MEM;
2124   else
2125     MC_UNSET_RAW_MEM;
2126   
2127
2128 }
2129
2130 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
2131 {
2132
2133   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2134
2135   int value;
2136   char *req_str;
2137   smx_simcall_t req = NULL, saved_req = NULL;
2138   xbt_fifo_item_t item;
2139   mc_state_t state;
2140   mc_pair_t pair;
2141   int depth = 1;
2142
2143   XBT_DEBUG("**** Begin Replay ****");
2144
2145   /* Restore the initial state */
2146   MC_restore_snapshot(initial_state_liveness->snapshot);
2147
2148   /* At the moment of taking the snapshot the raw heap was set, so restoring
2149    * it will set it back again, we have to unset it to continue  */
2150   if(!initial_state_liveness->raw_mem_set)
2151     MC_UNSET_RAW_MEM;
2152
2153   if(all_stack){
2154
2155     item = xbt_fifo_get_last_item(stack);
2156
2157     while(depth <= xbt_fifo_size(stack)){
2158
2159       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
2160       state = (mc_state_t) pair->graph_state;
2161
2162       if(pair->requests > 0){
2163    
2164         saved_req = MC_state_get_executed_request(state, &value);
2165         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
2166       
2167         if(saved_req != NULL){
2168           /* because we got a copy of the executed request, we have to fetch the  
2169              real one, pointed by the request field of the issuer process */
2170           req = &saved_req->issuer->simcall;
2171           //XBT_DEBUG("Req->call %u", req->call);
2172   
2173           /* Debug information */
2174           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2175             req_str = MC_request_to_string(req, value);
2176             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
2177             xbt_free(req_str);
2178           }
2179   
2180         }
2181  
2182         SIMIX_simcall_pre(req, value);
2183         MC_wait_for_requests();
2184       }
2185
2186       depth++;
2187     
2188       /* Update statistics */
2189       mc_stats->visited_pairs++;
2190       mc_stats->executed_transitions++;
2191
2192       item = xbt_fifo_get_prev_item(item);
2193     }
2194
2195   }else{
2196
2197     /* Traverse the stack from the initial state and re-execute the transitions */
2198     for (item = xbt_fifo_get_last_item(stack);
2199          item != xbt_fifo_get_first_item(stack);
2200          item = xbt_fifo_get_prev_item(item)) {
2201
2202       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
2203       state = (mc_state_t) pair->graph_state;
2204
2205       if(pair->requests > 0){
2206    
2207         saved_req = MC_state_get_executed_request(state, &value);
2208         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
2209       
2210         if(saved_req != NULL){
2211           /* because we got a copy of the executed request, we have to fetch the  
2212              real one, pointed by the request field of the issuer process */
2213           req = &saved_req->issuer->simcall;
2214           //XBT_DEBUG("Req->call %u", req->call);
2215   
2216           /* Debug information */
2217           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2218             req_str = MC_request_to_string(req, value);
2219             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
2220             xbt_free(req_str);
2221           }
2222   
2223         }
2224  
2225         SIMIX_simcall_pre(req, value);
2226         MC_wait_for_requests();
2227       }
2228
2229       depth++;
2230     
2231       /* Update statistics */
2232       mc_stats->visited_pairs++;
2233       mc_stats->executed_transitions++;
2234     }
2235   }  
2236
2237   XBT_DEBUG("**** End Replay ****");
2238
2239   if(initial_state_liveness->raw_mem_set)
2240     MC_SET_RAW_MEM;
2241   else
2242     MC_UNSET_RAW_MEM;
2243   
2244 }
2245
2246 /**
2247  * \brief Dumps the contents of a model-checker's stack and shows the actual
2248  *        execution trace
2249  * \param stack The stack to dump
2250  */
2251 void MC_dump_stack_safety(xbt_fifo_t stack)
2252 {
2253   
2254   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2255
2256   MC_show_stack_safety(stack);
2257
2258   if(!_sg_mc_checkpoint){
2259
2260     mc_state_t state;
2261
2262     MC_SET_RAW_MEM;
2263     while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
2264       MC_state_delete(state);
2265     MC_UNSET_RAW_MEM;
2266
2267   }
2268
2269   if(raw_mem_set)
2270     MC_SET_RAW_MEM;
2271   else
2272     MC_UNSET_RAW_MEM;
2273   
2274 }
2275
2276
2277 void MC_show_stack_safety(xbt_fifo_t stack)
2278 {
2279
2280   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2281
2282   MC_SET_RAW_MEM;
2283
2284   int value;
2285   mc_state_t state;
2286   xbt_fifo_item_t item;
2287   smx_simcall_t req;
2288   char *req_str = NULL;
2289   
2290   for (item = xbt_fifo_get_last_item(stack);
2291        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
2292         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
2293     req = MC_state_get_executed_request(state, &value);
2294     if(req){
2295       req_str = MC_request_to_string(req, value);
2296       XBT_INFO("%s", req_str);
2297       xbt_free(req_str);
2298     }
2299   }
2300
2301   if(!raw_mem_set)
2302     MC_UNSET_RAW_MEM;
2303 }
2304
2305 void MC_show_deadlock(smx_simcall_t req)
2306 {
2307   /*char *req_str = NULL;*/
2308   XBT_INFO("**************************");
2309   XBT_INFO("*** DEAD-LOCK DETECTED ***");
2310   XBT_INFO("**************************");
2311   XBT_INFO("Locked request:");
2312   /*req_str = MC_request_to_string(req);
2313     XBT_INFO("%s", req_str);
2314     xbt_free(req_str);*/
2315   XBT_INFO("Counter-example execution trace:");
2316   MC_dump_stack_safety(mc_stack_safety);
2317   MC_print_statistics(mc_stats);
2318 }
2319
2320
2321 void MC_show_stack_liveness(xbt_fifo_t stack){
2322   int value;
2323   mc_pair_t pair;
2324   xbt_fifo_item_t item;
2325   smx_simcall_t req;
2326   char *req_str = NULL;
2327   
2328   for (item = xbt_fifo_get_last_item(stack);
2329        (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
2330         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
2331     req = MC_state_get_executed_request(pair->graph_state, &value);
2332     if(req){
2333       if(pair->requests>0){
2334         req_str = MC_request_to_string(req, value);
2335         XBT_INFO("%s", req_str);
2336         xbt_free(req_str);
2337       }else{
2338         XBT_INFO("End of system requests but evolution in B├╝chi automaton");
2339       }
2340     }
2341   }
2342 }
2343
2344 void MC_dump_stack_liveness(xbt_fifo_t stack){
2345
2346   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2347
2348   mc_pair_t pair;
2349
2350   MC_SET_RAW_MEM;
2351   while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
2352     MC_pair_delete(pair);
2353   MC_UNSET_RAW_MEM;
2354
2355   if(raw_mem_set)
2356     MC_SET_RAW_MEM;
2357
2358 }
2359
2360
2361 void MC_print_statistics(mc_stats_t stats)
2362 {
2363   if(stats->expanded_pairs == 0){
2364     XBT_INFO("Expanded states = %lu", stats->expanded_states);
2365     XBT_INFO("Visited states = %lu", stats->visited_states);
2366   }else{
2367     XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
2368     XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
2369   }
2370   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
2371   MC_SET_RAW_MEM;
2372   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
2373     fprintf(dot_output, "}\n");
2374     fclose(dot_output);
2375   }
2376   MC_UNSET_RAW_MEM;
2377 }
2378
2379 void MC_assert(int prop)
2380 {
2381   if (MC_is_active() && !prop){
2382     XBT_INFO("**************************");
2383     XBT_INFO("*** PROPERTY NOT VALID ***");
2384     XBT_INFO("**************************");
2385     XBT_INFO("Counter-example execution trace:");
2386     MC_dump_stack_safety(mc_stack_safety);
2387     MC_print_statistics(mc_stats);
2388     xbt_abort();
2389   }
2390 }
2391
2392 void MC_max_depth(int max_depth){
2393   user_max_depth_reached = max_depth;
2394 }
2395
2396 void MC_process_clock_add(smx_process_t process, double amount)
2397 {
2398   mc_time[process->pid] += amount;
2399 }
2400
2401 double MC_process_clock_get(smx_process_t process)
2402 {
2403   if(mc_time){
2404     if(process != NULL)
2405       return mc_time[process->pid];
2406     else 
2407       return -1;
2408   }else{
2409     return 0;
2410   }
2411 }
2412
2413 void MC_automaton_load(const char *file){
2414
2415   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2416
2417   MC_SET_RAW_MEM;
2418
2419   if (_mc_property_automaton == NULL)
2420     _mc_property_automaton = xbt_automaton_new();
2421   
2422   xbt_automaton_load(_mc_property_automaton,file);
2423
2424   MC_UNSET_RAW_MEM;
2425
2426   if(raw_mem_set)
2427     MC_SET_RAW_MEM;
2428
2429 }
2430
2431 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
2432
2433   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2434
2435   MC_SET_RAW_MEM;
2436
2437   if (_mc_property_automaton == NULL)
2438     _mc_property_automaton = xbt_automaton_new();
2439
2440   xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
2441
2442   MC_UNSET_RAW_MEM;
2443
2444   if(raw_mem_set)
2445     MC_SET_RAW_MEM;
2446   
2447 }
2448
2449
2450