Logo AND Algorithmique Numérique Distribuée

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