Logo AND Algorithmique Numérique Distribuée

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