Logo AND Algorithmique Numérique Distribuée

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