Logo AND Algorithmique Numérique Distribuée

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