Logo AND Algorithmique Numérique Distribuée

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