Logo AND Algorithmique Numérique Distribuée

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