Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : fix soundness of DPOR algorithm if max depth is reached
[simgrid.git] / src / mc / mc_global.c
1 /* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved.            */
2
3 /* This program is free software; you can redistribute it and/or modify it
4  * under the terms of the license (GNU LGPL) which comes with this package. */
5
6 #include <unistd.h>
7 #include <sys/types.h>
8 #include <sys/wait.h>
9 #include <sys/time.h>
10
11 #include "simgrid/sg_config.h"
12 #include "../surf/surf_private.h"
13 #include "../simix/smx_private.h"
14 #include "../xbt/mmalloc/mmprivate.h"
15 #include "xbt/fifo.h"
16 #include "mc_private.h"
17 #include "xbt/automaton.h"
18 #include "xbt/dict.h"
19
20 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
21 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
22                                 "Logging specific to MC (global)");
23
24 /* Configuration support */
25 e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
26
27 int _sg_do_model_check = 0;
28 int _sg_mc_checkpoint=0;
29 char* _sg_mc_property_file=NULL;
30 int _sg_mc_timeout=0;
31 int _sg_mc_max_depth=1000;
32 int _sg_mc_visited=0;
33 char *_sg_mc_dot_output_file = NULL;
34
35 extern int _sg_init_status;
36 void _mc_cfg_cb_reduce(const char *name, int pos) {
37   if (_sg_init_status && !_sg_do_model_check) {
38     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.");
39   }
40   char *val= xbt_cfg_get_string(_sg_cfg_set, name);
41   if (!strcasecmp(val,"none")) {
42     mc_reduce_kind = e_mc_reduce_none;
43   } else if (!strcasecmp(val,"dpor")) {
44     mc_reduce_kind = e_mc_reduce_dpor;
45   } else {
46     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
47   }
48 }
49
50 void _mc_cfg_cb_checkpoint(const char *name, int pos) {
51   if (_sg_init_status && !_sg_do_model_check) {
52     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.");
53   }
54   _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
55 }
56 void _mc_cfg_cb_property(const char *name, int pos) {
57   if (_sg_init_status && !_sg_do_model_check) {
58     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.");
59   }
60   _sg_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
61 }
62
63 void _mc_cfg_cb_timeout(const char *name, int pos) {
64   if (_sg_init_status && !_sg_do_model_check) {
65     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.");
66   }
67   _sg_mc_timeout= xbt_cfg_get_int(_sg_cfg_set, name);
68 }
69
70 void _mc_cfg_cb_max_depth(const char *name, int pos) {
71   if (_sg_init_status && !_sg_do_model_check) {
72     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.");
73   }
74   _sg_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
75 }
76
77 void _mc_cfg_cb_visited(const char *name, int pos) {
78   if (_sg_init_status && !_sg_do_model_check) {
79     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.");
80   }
81   _sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
82 }
83
84 void _mc_cfg_cb_dot_output(const char *name, int pos) {
85   if (_sg_init_status && !_sg_do_model_check) {
86     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.");
87   }
88   _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
89 }
90
91 /* MC global data structures */
92
93 mc_state_t mc_current_state = NULL;
94 char mc_replay_mode = FALSE;
95 double *mc_time = NULL;
96 mc_comparison_times_t mc_comp_times = NULL;
97 double mc_snapshot_comparison_time;
98 mc_stats_t mc_stats = NULL;
99
100 /* Safety */
101
102 xbt_fifo_t mc_stack_safety = NULL;
103 mc_global_t initial_state_safety = NULL;
104
105 /* Liveness */
106
107 xbt_fifo_t mc_stack_liveness = NULL;
108 mc_global_t initial_state_liveness = NULL;
109 int compare;
110
111 /* Local */
112 xbt_dict_t mc_local_variables = NULL;
113 /* Global */
114 xbt_dynar_t mc_global_variables = 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 FILE *dot_output = NULL;
123 const char* colors[10];
124
125 xbt_automaton_t _mc_property_automaton = NULL;
126
127 /* Static functions */
128
129 static void MC_assert_pair(int prop);
130 static dw_location_t get_location(xbt_dict_t location_list, char *expr);
131 static dw_frame_t get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset);
132 static size_t data_bss_ignore_size(void *address);
133 static void MC_get_global_variables(char *elf_file);
134
135 void MC_do_the_modelcheck_for_real() {
136
137   MC_SET_RAW_MEM;
138   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
139   MC_UNSET_RAW_MEM;
140   
141   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
142     MC_init_dot_output();
143
144   if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
145     if (mc_reduce_kind==e_mc_reduce_unset)
146       mc_reduce_kind=e_mc_reduce_dpor;
147
148     XBT_INFO("Check a safety property");
149     MC_modelcheck_safety();
150
151   } else  {
152
153     if (mc_reduce_kind==e_mc_reduce_unset)
154       mc_reduce_kind=e_mc_reduce_none;
155
156     XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
157     MC_automaton_load(_sg_mc_property_file);
158     MC_modelcheck_liveness();
159   }
160 }
161
162
163 void MC_compare(void){
164   compare = 1;
165 }
166
167 void MC_init(){
168
169   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
170   
171   compare = 0;
172
173   /* Initialize the data structures that must be persistent across every
174      iteration of the model-checker (in RAW memory) */
175
176   MC_SET_RAW_MEM;
177
178   MC_init_memory_map_info();
179   
180   mc_local_variables = xbt_dict_new_homogeneous(NULL);
181
182   /* Get local variables in binary for state equality detection */
183   xbt_dict_t binary_location_list = MC_get_location_list(xbt_binary_name);
184   MC_get_local_variables(xbt_binary_name, binary_location_list, &mc_local_variables);
185
186   /* Get local variables in libsimgrid for state equality detection */
187   xbt_dict_t libsimgrid_location_list = MC_get_location_list(libsimgrid_path);
188   MC_get_local_variables(libsimgrid_path, libsimgrid_location_list, &mc_local_variables);
189
190   xbt_dict_free(&libsimgrid_location_list);
191   xbt_dict_free(&binary_location_list);
192   
193   /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
194   get_libsimgrid_plt_section();
195   get_binary_plt_section();
196
197   /* Get global variables */
198   MC_get_global_variables(xbt_binary_name);
199   MC_get_global_variables(libsimgrid_path);
200
201   MC_UNSET_RAW_MEM;
202
203    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
204   MC_ignore_stack("e", "*");
205   MC_ignore_stack("__ex_cleanup", "*");
206   MC_ignore_stack("__ex_mctx_en", "*");
207   MC_ignore_stack("__ex_mctx_me", "*");
208   MC_ignore_stack("__xbt_ex_ctx_ptr", "*");
209   MC_ignore_stack("_log_ev", "*");
210   MC_ignore_stack("_throw_ctx", "*");
211   MC_ignore_stack("ctx", "*");
212
213   MC_ignore_stack("next_context", "smx_ctx_sysv_suspend_serial");
214   MC_ignore_stack("i", "smx_ctx_sysv_suspend_serial");
215
216   MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
217   MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time)); 
218   MC_ignore_data_bss(&mc_time, sizeof(mc_time));
219
220   if(raw_mem_set)
221     MC_SET_RAW_MEM;
222
223 }
224
225 void MC_init_dot_output(){
226
227   colors[0] = "blue";
228   colors[1] = "red";
229   colors[2] = "green";
230   colors[3] = "pink";
231   colors[4] = "brown";
232   colors[5] = "purple";
233   colors[6] = "yellow";
234   colors[7] = "orange";
235   
236   dot_output = fopen(_sg_mc_dot_output_file, "w");
237   
238   if(dot_output == NULL){
239     perror("Error open dot output file");
240     xbt_abort();
241   }
242
243   fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.20; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
244
245 }
246
247 void MC_modelcheck_safety(void)
248 {
249   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
250
251   /* Check if MC is already initialized */
252   if (initial_state_safety)
253     return;
254
255   mc_time = xbt_new0(double, simix_process_maxpid);
256
257   /* mc_time refers to clock for each process -> ignore it for heap comparison */  
258   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
259
260   /* Initialize the data structures that must be persistent across every
261      iteration of the model-checker (in RAW memory) */
262   
263   MC_SET_RAW_MEM;
264
265   /* Initialize statistics */
266   mc_stats = xbt_new0(s_mc_stats_t, 1);
267   mc_stats->state_size = 1;
268
269   /* Create exploration stack */
270   mc_stack_safety = xbt_fifo_new();
271
272   MC_UNSET_RAW_MEM;
273
274   if(_sg_mc_visited > 0){
275     MC_init();
276   }else{
277     MC_SET_RAW_MEM;
278     MC_init_memory_map_info();
279     get_libsimgrid_plt_section();
280     get_binary_plt_section();
281     MC_UNSET_RAW_MEM;
282   }
283
284   MC_dpor_init();
285
286   MC_SET_RAW_MEM;
287   /* Save the initial state */
288   initial_state_safety = xbt_new0(s_mc_global_t, 1);
289   initial_state_safety->snapshot = MC_take_snapshot();
290   MC_UNSET_RAW_MEM;
291
292   MC_dpor();
293
294   if(raw_mem_set)
295     MC_SET_RAW_MEM;
296
297   MC_exit();
298 }
299
300 void MC_modelcheck_liveness(){
301
302   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
303
304   MC_init();
305
306   mc_time = xbt_new0(double, simix_process_maxpid);
307
308   /* mc_time refers to clock for each process -> ignore it for heap comparison */  
309   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
310  
311   MC_SET_RAW_MEM;
312  
313   /* Initialize statistics */
314   mc_stats = xbt_new0(s_mc_stats_t, 1);
315   mc_stats->state_size = 1;
316
317   /* Create exploration stack */
318   mc_stack_liveness = xbt_fifo_new();
319
320   /* Create the initial state */
321   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
322
323   MC_UNSET_RAW_MEM;
324
325   MC_ddfs_init();
326
327   /* We're done */
328   MC_print_statistics(mc_stats);
329   xbt_free(mc_time);
330
331   if(raw_mem_set)
332     MC_SET_RAW_MEM;
333
334 }
335
336
337 void MC_exit(void)
338 {
339   MC_SET_RAW_MEM;
340   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
341     fprintf(dot_output, "}\n");
342     fclose(dot_output);
343   }
344   MC_UNSET_RAW_MEM;
345
346   xbt_free(mc_time);
347   MC_memory_exit();
348   xbt_abort();
349 }
350
351 int SIMIX_pre_mc_random(smx_simcall_t simcall){
352
353   return simcall->mc_value;
354 }
355
356
357 int MC_random(void)
358 {
359   /*FIXME: return mc_current_state->executed_transition->random.value;*/
360   return simcall_mc_random();
361 }
362
363 /**
364  * \brief Schedules all the process that are ready to run
365  */
366 void MC_wait_for_requests(void)
367 {
368   smx_process_t process;
369   smx_simcall_t req;
370   unsigned int iter;
371
372   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
373     SIMIX_process_runall();
374     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
375       req = &process->simcall;
376       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
377         SIMIX_simcall_pre(req, 0);
378     }
379   }
380 }
381
382 int MC_deadlock_check()
383 {
384   int deadlock = FALSE;
385   smx_process_t process;
386   if(xbt_swag_size(simix_global->process_list)){
387     deadlock = TRUE;
388     xbt_swag_foreach(process, simix_global->process_list){
389       if(process->simcall.call != SIMCALL_NONE
390          && MC_request_is_enabled(&process->simcall)){
391         deadlock = FALSE;
392         break;
393       }
394     }
395   }
396   return deadlock;
397 }
398
399 /**
400  * \brief Re-executes from the state at position start all the transitions indicated by
401  *        a given model-checker stack.
402  * \param stack The stack with the transitions to execute.
403  * \param start Start index to begin the re-execution.
404  */
405 void MC_replay(xbt_fifo_t stack, int start)
406 {
407   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
408
409   int value, i = 1, count = 1;
410   char *req_str;
411   smx_simcall_t req = NULL, saved_req = NULL;
412   xbt_fifo_item_t item, start_item;
413   mc_state_t state;
414   smx_process_t process = NULL;
415
416   XBT_DEBUG("**** Begin Replay ****");
417
418   if(start == -1){
419     /* Restore the initial state */
420     MC_restore_snapshot(initial_state_safety->snapshot);
421     /* At the moment of taking the snapshot the raw heap was set, so restoring
422      * it will set it back again, we have to unset it to continue  */
423     MC_UNSET_RAW_MEM;
424   }
425
426   start_item = xbt_fifo_get_last_item(stack);
427   if(start != -1){
428     while (i != start){
429       start_item = xbt_fifo_get_prev_item(start_item);
430       i++;
431     }
432   }
433
434   MC_SET_RAW_MEM;
435   xbt_dict_reset(first_enabled_state);
436   xbt_swag_foreach(process, simix_global->process_list){
437     if(MC_process_is_enabled(process)){
438       char *key = bprintf("%lu", process->pid);
439       char *data = bprintf("%d", count);
440       xbt_dict_set(first_enabled_state, key, data, NULL);
441       xbt_free(key);
442     }
443   }
444   MC_UNSET_RAW_MEM;
445   
446
447   /* Traverse the stack from the state at position start and re-execute the transitions */
448   for (item = start_item;
449        item != xbt_fifo_get_first_item(stack);
450        item = xbt_fifo_get_prev_item(item)) {
451
452     state = (mc_state_t) xbt_fifo_get_item_content(item);
453     saved_req = MC_state_get_executed_request(state, &value);
454    
455     MC_SET_RAW_MEM;
456     char *key = bprintf("%lu", saved_req->issuer->pid);
457     xbt_dict_remove(first_enabled_state, key); 
458     xbt_free(key);
459     MC_UNSET_RAW_MEM;
460    
461     if(saved_req){
462       /* because we got a copy of the executed request, we have to fetch the  
463          real one, pointed by the request field of the issuer process */
464       req = &saved_req->issuer->simcall;
465
466       /* Debug information */
467       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
468         req_str = MC_request_to_string(req, value);
469         XBT_DEBUG("Replay: %s (%p)", req_str, state);
470         xbt_free(req_str);
471       }
472     }
473     
474     SIMIX_simcall_pre(req, value);
475     MC_wait_for_requests();
476
477     count++;
478
479     MC_SET_RAW_MEM;
480     /* Insert in dict all enabled processes */
481     xbt_swag_foreach(process, simix_global->process_list){
482       if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
483         char *key = bprintf("%lu", process->pid);
484         if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
485           char *data = bprintf("%d", count);
486           xbt_dict_set(first_enabled_state, key, data, NULL);
487         }
488         xbt_free(key);
489       }
490     }
491     MC_UNSET_RAW_MEM;
492          
493     /* Update statistics */
494     mc_stats->visited_states++;
495     mc_stats->executed_transitions++;
496
497   }
498
499   XBT_DEBUG("**** End Replay ****");
500
501   if(raw_mem)
502     MC_SET_RAW_MEM;
503   else
504     MC_UNSET_RAW_MEM;
505   
506
507 }
508
509 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
510 {
511
512   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
513
514   int value;
515   char *req_str;
516   smx_simcall_t req = NULL, saved_req = NULL;
517   xbt_fifo_item_t item;
518   mc_state_t state;
519   mc_pair_t pair;
520   int depth = 1;
521
522   XBT_DEBUG("**** Begin Replay ****");
523
524   /* Restore the initial state */
525   MC_restore_snapshot(initial_state_liveness->snapshot);
526
527   /* At the moment of taking the snapshot the raw heap was set, so restoring
528    * it will set it back again, we have to unset it to continue  */
529   if(!initial_state_liveness->raw_mem_set)
530     MC_UNSET_RAW_MEM;
531
532   if(all_stack){
533
534     item = xbt_fifo_get_last_item(stack);
535
536     while(depth <= xbt_fifo_size(stack)){
537
538       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
539       state = (mc_state_t) pair->graph_state;
540
541       if(pair->requests > 0){
542    
543         saved_req = MC_state_get_executed_request(state, &value);
544         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
545       
546         if(saved_req != NULL){
547           /* because we got a copy of the executed request, we have to fetch the  
548              real one, pointed by the request field of the issuer process */
549           req = &saved_req->issuer->simcall;
550           //XBT_DEBUG("Req->call %u", req->call);
551   
552           /* Debug information */
553           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
554             req_str = MC_request_to_string(req, value);
555             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
556             xbt_free(req_str);
557           }
558   
559         }
560  
561         SIMIX_simcall_pre(req, value);
562         MC_wait_for_requests();
563       }
564
565       depth++;
566     
567       /* Update statistics */
568       mc_stats->visited_pairs++;
569       mc_stats->executed_transitions++;
570
571       item = xbt_fifo_get_prev_item(item);
572     }
573
574   }else{
575
576     /* Traverse the stack from the initial state and re-execute the transitions */
577     for (item = xbt_fifo_get_last_item(stack);
578          item != xbt_fifo_get_first_item(stack);
579          item = xbt_fifo_get_prev_item(item)) {
580
581       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
582       state = (mc_state_t) pair->graph_state;
583
584       if(pair->requests > 0){
585    
586         saved_req = MC_state_get_executed_request(state, &value);
587         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
588       
589         if(saved_req != NULL){
590           /* because we got a copy of the executed request, we have to fetch the  
591              real one, pointed by the request field of the issuer process */
592           req = &saved_req->issuer->simcall;
593           //XBT_DEBUG("Req->call %u", req->call);
594   
595           /* Debug information */
596           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
597             req_str = MC_request_to_string(req, value);
598             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
599             xbt_free(req_str);
600           }
601   
602         }
603  
604         SIMIX_simcall_pre(req, value);
605         MC_wait_for_requests();
606       }
607
608       depth++;
609     
610       /* Update statistics */
611       mc_stats->visited_pairs++;
612       mc_stats->executed_transitions++;
613     }
614   }  
615
616   XBT_DEBUG("**** End Replay ****");
617
618   if(initial_state_liveness->raw_mem_set)
619     MC_SET_RAW_MEM;
620   else
621     MC_UNSET_RAW_MEM;
622   
623 }
624
625 /**
626  * \brief Dumps the contents of a model-checker's stack and shows the actual
627  *        execution trace
628  * \param stack The stack to dump
629  */
630 void MC_dump_stack_safety(xbt_fifo_t stack)
631 {
632   
633   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
634
635   MC_show_stack_safety(stack);
636
637   if(!_sg_mc_checkpoint){
638
639     mc_state_t state;
640
641     MC_SET_RAW_MEM;
642     while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
643       MC_state_delete(state);
644     MC_UNSET_RAW_MEM;
645
646   }
647
648   if(raw_mem_set)
649     MC_SET_RAW_MEM;
650   else
651     MC_UNSET_RAW_MEM;
652   
653 }
654
655
656 void MC_show_stack_safety(xbt_fifo_t stack)
657 {
658   int value;
659   mc_state_t state;
660   xbt_fifo_item_t item;
661   smx_simcall_t req;
662   char *req_str = NULL;
663   
664   for (item = xbt_fifo_get_last_item(stack);
665        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
666         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
667     req = MC_state_get_executed_request(state, &value);
668     if(req){
669       req_str = MC_request_to_string(req, value);
670       XBT_INFO("%s", req_str);
671       xbt_free(req_str);
672     }
673   }
674 }
675
676 void MC_show_deadlock(smx_simcall_t req)
677 {
678   /*char *req_str = NULL;*/
679   XBT_INFO("**************************");
680   XBT_INFO("*** DEAD-LOCK DETECTED ***");
681   XBT_INFO("**************************");
682   XBT_INFO("Locked request:");
683   /*req_str = MC_request_to_string(req);
684     XBT_INFO("%s", req_str);
685     xbt_free(req_str);*/
686   XBT_INFO("Counter-example execution trace:");
687   MC_dump_stack_safety(mc_stack_safety);
688 }
689
690
691 void MC_show_stack_liveness(xbt_fifo_t stack){
692   int value;
693   mc_pair_t pair;
694   xbt_fifo_item_t item;
695   smx_simcall_t req;
696   char *req_str = NULL;
697   
698   for (item = xbt_fifo_get_last_item(stack);
699        (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
700         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
701     req = MC_state_get_executed_request(pair->graph_state, &value);
702     if(req){
703       if(pair->requests>0){
704         req_str = MC_request_to_string(req, value);
705         XBT_INFO("%s", req_str);
706         xbt_free(req_str);
707       }else{
708         XBT_INFO("End of system requests but evolution in B├╝chi automaton");
709       }
710     }
711   }
712 }
713
714 void MC_dump_stack_liveness(xbt_fifo_t stack){
715
716   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
717
718   mc_pair_t pair;
719
720   MC_SET_RAW_MEM;
721   while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
722     MC_pair_delete(pair);
723   MC_UNSET_RAW_MEM;
724
725   if(raw_mem_set)
726     MC_SET_RAW_MEM;
727
728 }
729
730
731 void MC_print_statistics(mc_stats_t stats)
732 {
733   if(stats->expanded_pairs == 0){
734     XBT_INFO("Expanded states = %lu", stats->expanded_states);
735     XBT_INFO("Visited states = %lu", stats->visited_states);
736   }else{
737     XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
738     XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
739   }
740   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
741 }
742
743 void MC_assert(int prop)
744 {
745   if (MC_is_active() && !prop){
746     XBT_INFO("**************************");
747     XBT_INFO("*** PROPERTY NOT VALID ***");
748     XBT_INFO("**************************");
749     XBT_INFO("Counter-example execution trace:");
750     MC_dump_stack_safety(mc_stack_safety);
751     MC_print_statistics(mc_stats);
752     xbt_abort();
753   }
754 }
755
756 static void MC_assert_pair(int prop){
757   if (MC_is_active() && !prop) {
758     XBT_INFO("**************************");
759     XBT_INFO("*** PROPERTY NOT VALID ***");
760     XBT_INFO("**************************");
761     //XBT_INFO("Counter-example execution trace:");
762     MC_show_stack_liveness(mc_stack_liveness);
763     //MC_dump_snapshot_stack(mc_snapshot_stack);
764     MC_print_statistics(mc_stats);
765     xbt_abort();
766   }
767 }
768
769 void MC_process_clock_add(smx_process_t process, double amount)
770 {
771   mc_time[process->pid] += amount;
772 }
773
774 double MC_process_clock_get(smx_process_t process)
775 {
776   if(mc_time){
777     if(process != NULL)
778       return mc_time[process->pid];
779     else 
780       return -1;
781   }else{
782     return 0;
783   }
784 }
785
786 void MC_automaton_load(const char *file){
787
788   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
789
790   MC_SET_RAW_MEM;
791
792   if (_mc_property_automaton == NULL)
793     _mc_property_automaton = xbt_automaton_new();
794   
795   xbt_automaton_load(_mc_property_automaton,file);
796
797   MC_UNSET_RAW_MEM;
798
799   if(raw_mem_set)
800     MC_SET_RAW_MEM;
801
802 }
803
804 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
805
806   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
807
808   MC_SET_RAW_MEM;
809
810   if (_mc_property_automaton == NULL)
811     _mc_property_automaton = xbt_automaton_new();
812
813   xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
814
815   MC_UNSET_RAW_MEM;
816
817   if(raw_mem_set)
818     MC_SET_RAW_MEM;
819   
820 }
821
822 /************ MC_ignore ***********/ 
823
824 void heap_ignore_region_free(mc_heap_ignore_region_t r){
825   xbt_free(r);
826 }
827
828 void heap_ignore_region_free_voidp(void *r){
829   heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
830 }
831
832 void MC_ignore_heap(void *address, size_t size){
833
834   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
835
836   MC_SET_RAW_MEM;
837
838   mc_heap_ignore_region_t region = NULL;
839   region = xbt_new0(s_mc_heap_ignore_region_t, 1);
840   region->address = address;
841   region->size = size;
842   
843   region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
844   
845   if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
846     region->fragment = -1;
847     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore = 1;
848   }else{
849     region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
850     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment] = 1;
851   }
852   
853   if(mc_heap_comparison_ignore == NULL){
854     mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
855     xbt_dynar_push(mc_heap_comparison_ignore, &region);
856     if(!raw_mem_set)
857       MC_UNSET_RAW_MEM;
858     return;
859   }
860
861   unsigned int cursor = 0;
862   mc_heap_ignore_region_t current_region = NULL;
863   int start = 0;
864   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
865   
866   while(start <= end){
867     cursor = (start + end) / 2;
868     current_region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
869     if(current_region->address == address){
870       heap_ignore_region_free(region);
871       if(!raw_mem_set)
872         MC_UNSET_RAW_MEM;
873       return;
874     }
875     if(current_region->address < address)
876       start = cursor + 1;
877     if(current_region->address > address)
878       end = cursor - 1;   
879   }
880
881   if(current_region->address < address)
882     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
883   else
884     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
885
886   MC_UNSET_RAW_MEM;
887
888   if(raw_mem_set)
889     MC_SET_RAW_MEM;
890 }
891
892 void MC_remove_ignore_heap(void *address, size_t size){
893
894   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
895
896   MC_SET_RAW_MEM;
897
898   unsigned int cursor = 0;
899   int start = 0;
900   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
901   mc_heap_ignore_region_t region;
902   int ignore_found = 0;
903
904   while(start <= end){
905     cursor = (start + end) / 2;
906     region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
907     if(region->address == address){
908       ignore_found = 1;
909       break;
910     }
911     if(region->address < address)
912       start = cursor + 1;
913     if(region->address > address){
914       if((char * )region->address <= ((char *)address + size)){
915         ignore_found = 1;
916         break;
917       }else
918         end = cursor - 1;   
919     }
920   }
921   
922   if(ignore_found == 1){
923     xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
924     MC_remove_ignore_heap(address, size);
925   }
926
927   MC_UNSET_RAW_MEM;
928   
929   if(raw_mem_set)
930     MC_SET_RAW_MEM;
931
932 }
933
934 void MC_ignore_data_bss(void *address, size_t size){
935
936   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
937
938   MC_SET_RAW_MEM;
939   
940   if(mc_data_bss_comparison_ignore == NULL)
941     mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), NULL);
942
943   mc_data_bss_ignore_variable_t var = NULL;
944   var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
945   var->address = address;
946   var->size = size;
947
948   if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
949
950     xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
951
952   }else{
953     
954     unsigned int cursor = 0;
955     int start = 0;
956     int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
957     mc_data_bss_ignore_variable_t current_var = NULL;
958
959     while(start <= end){
960       cursor = (start + end) / 2;
961       current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
962       if(current_var->address == address){
963         MC_UNSET_RAW_MEM;
964         if(raw_mem_set)
965           MC_SET_RAW_MEM;
966         return;
967       }
968       if(current_var->address < address)
969         start = cursor + 1;
970       if(current_var->address > address)
971         end = cursor - 1;
972     }
973
974     if(current_var->address < address)
975       xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
976     else
977       xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);
978
979   }
980
981   /* Remove variable from mc_global_variables */
982
983   if(mc_global_variables != NULL){
984
985     unsigned int cursor = 0;
986     int start = 0;
987     int end = xbt_dynar_length(mc_global_variables) - 1;
988     global_variable_t current_var;
989     int var_found;
990
991     while(start <= end){
992       cursor = (start + end) / 2;
993       current_var = (global_variable_t)xbt_dynar_get_as(mc_global_variables, cursor, global_variable_t);
994       if(current_var->address == var->address){
995         var_found = 1;
996         break;
997       }
998       if(current_var->address < address)
999         start = cursor + 1;
1000       if(current_var->address > address)
1001         end = cursor - 1;
1002     }
1003
1004     if(var_found)
1005       xbt_dynar_remove_at(mc_global_variables, cursor, NULL);
1006     
1007   }
1008
1009   MC_UNSET_RAW_MEM;
1010
1011   if(raw_mem_set)
1012     MC_SET_RAW_MEM;
1013 }
1014
1015 static size_t data_bss_ignore_size(void *address){
1016   unsigned int cursor = 0;
1017   int start = 0;
1018   int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
1019   mc_data_bss_ignore_variable_t var;
1020
1021   while(start <= end){
1022     cursor = (start + end) / 2;
1023     var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
1024     if(var->address == address)
1025       return var->size;
1026     if(var->address < address){
1027       if((void *)((char *)var->address + var->size) > address)
1028         return (char *)var->address + var->size - (char*)address;
1029       else
1030         start = cursor + 1;
1031     }
1032     if(var->address > address)
1033       end = cursor - 1;   
1034   }
1035
1036   return 0;
1037 }
1038
1039
1040
1041 void MC_ignore_stack(const char *var_name, const char *frame_name){
1042   
1043   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1044
1045   MC_SET_RAW_MEM;
1046
1047   if(mc_stack_comparison_ignore == NULL)
1048     mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), NULL);
1049
1050   if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){
1051
1052     mc_stack_ignore_variable_t var = NULL;
1053     var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
1054     var->var_name = strdup(var_name);
1055     var->frame = strdup(frame_name);
1056
1057     xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
1058
1059   }else{
1060     
1061     unsigned int cursor = 0;
1062     int start = 0;
1063     int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
1064     mc_stack_ignore_variable_t current_var = NULL;
1065
1066     while(start <= end){
1067       cursor = (start + end) / 2;
1068       current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
1069       if(strcmp(current_var->frame, frame_name) == 0){
1070         if(strcmp(current_var->var_name, var_name) == 0){
1071           MC_UNSET_RAW_MEM;
1072           if(raw_mem_set)
1073             MC_SET_RAW_MEM;
1074           return;
1075         }
1076         if(strcmp(current_var->var_name, var_name) < 0)
1077           start = cursor + 1;
1078         if(strcmp(current_var->var_name, var_name) > 0)
1079           end = cursor - 1;
1080       }
1081       if(strcmp(current_var->frame, frame_name) < 0)
1082         start = cursor + 1;
1083       if(strcmp(current_var->frame, frame_name) > 0)
1084         end = cursor - 1;
1085     }
1086
1087     mc_stack_ignore_variable_t var = NULL;
1088     var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
1089     var->var_name = strdup(var_name);
1090     var->frame = strdup(frame_name);
1091
1092     if(strcmp(current_var->frame, frame_name) < 0)
1093       xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
1094     else
1095       xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
1096
1097   }
1098
1099  /* Remove variable from mc_local_variables */
1100
1101   if(mc_local_variables != NULL){
1102
1103     if(strcmp(frame_name, "*") != 0){
1104       dw_frame_t frame = xbt_dict_get_or_null(mc_local_variables, frame_name);
1105       if(frame != NULL)
1106         xbt_dict_remove(frame->variables, var_name);
1107     }
1108
1109   }
1110
1111   MC_UNSET_RAW_MEM;
1112   
1113   if(raw_mem_set)
1114     MC_SET_RAW_MEM;
1115
1116 }
1117
1118 void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
1119
1120   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1121
1122   MC_SET_RAW_MEM;
1123   if(stacks_areas == NULL)
1124     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
1125   
1126   stack_region_t region = NULL;
1127   region = xbt_new0(s_stack_region_t, 1);
1128   region->address = stack;
1129   region->process_name = strdup(name);
1130   region->context = context;
1131   region->size = size;
1132   region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
1133   xbt_dynar_push(stacks_areas, &region);
1134   
1135   MC_UNSET_RAW_MEM;
1136
1137   if(raw_mem_set)
1138     MC_SET_RAW_MEM;
1139 }
1140
1141 /************ DWARF ***********/
1142
1143 xbt_dict_t MC_get_location_list(const char *elf_file){
1144
1145   char *command = bprintf("objdump -Wo %s", elf_file);
1146
1147   FILE *fp = popen(command, "r");
1148
1149   if(fp == NULL){
1150     perror("popen for objdump failed");
1151     xbt_abort();
1152   }
1153
1154   int debug = 0; /*Detect if the program has been compiled with -g */
1155
1156   xbt_dict_t location_list = xbt_dict_new_homogeneous(NULL);
1157   char *line = NULL, *loc_expr = NULL;
1158   ssize_t read;
1159   size_t n = 0;
1160   int cursor_remove;
1161   xbt_dynar_t split = NULL;
1162
1163   while ((read = xbt_getline(&line, &n, fp)) != -1) {
1164
1165     /* Wipeout the new line character */
1166     line[read - 1] = '\0';
1167
1168     xbt_str_trim(line, NULL);
1169     
1170     if(n == 0)
1171       continue;
1172
1173     if(strlen(line) == 0)
1174       continue;
1175
1176     if(debug == 0){
1177
1178       if(strncmp(line, elf_file, strlen(elf_file)) == 0)
1179         continue;
1180       
1181       if(strncmp(line, "Contents", 8) == 0)
1182         continue;
1183
1184       if(strncmp(line, "Offset", 6) == 0){
1185         debug = 1;
1186         continue;
1187       }
1188     }
1189
1190     if(debug == 0){
1191       XBT_INFO("Your program must be compiled with -g");
1192       xbt_abort();
1193     }
1194
1195     xbt_dynar_t loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL);
1196
1197     xbt_str_strip_spaces(line);
1198     split = xbt_str_split(line, " ");
1199
1200     while(read != -1 && strcmp("<End", (char *)xbt_dynar_get_as(split, 1, char *)) != 0){
1201       
1202       dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
1203       new_entry->lowpc = strtoul((char *)xbt_dynar_get_as(split, 1, char *), NULL, 16);
1204       new_entry->highpc = strtoul((char *)xbt_dynar_get_as(split, 2, char *), NULL, 16);
1205       
1206       cursor_remove =0;
1207       while(cursor_remove < 3){
1208         xbt_dynar_remove_at(split, 0, NULL);
1209         cursor_remove++;
1210       }
1211
1212       loc_expr = xbt_str_join(split, " ");
1213       xbt_str_ltrim(loc_expr, "(");
1214       xbt_str_rtrim(loc_expr, ")");
1215       new_entry->location = get_location(NULL, loc_expr);
1216
1217       xbt_dynar_push(loclist, &new_entry);
1218
1219       xbt_dynar_free(&split);
1220       free(loc_expr);
1221
1222       read = xbt_getline(&line, &n, fp);
1223       if(read != -1){
1224         line[read - 1] = '\0';
1225         xbt_str_strip_spaces(line);
1226         split = xbt_str_split(line, " ");
1227       }
1228
1229     }
1230
1231
1232     char *key = bprintf("%d", (int)strtoul((char *)xbt_dynar_get_as(split, 0, char *), NULL, 16));
1233     xbt_dict_set(location_list, key, loclist, NULL);
1234     xbt_free(key);
1235     
1236     xbt_dynar_free(&split);
1237
1238   }
1239
1240   xbt_free(line);
1241   xbt_free(command);
1242   pclose(fp);
1243
1244   return location_list;
1245 }
1246
1247 static dw_frame_t get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset){
1248
1249   xbt_dict_cursor_t cursor = NULL;
1250   char *name;
1251   dw_frame_t res;
1252
1253   xbt_dict_foreach(all_variables, cursor, name, res) {
1254     if(offset >= res->start && offset < res->end){
1255       xbt_dict_cursor_free(&cursor);
1256       return res;
1257     }
1258   }
1259
1260   xbt_dict_cursor_free(&cursor);
1261   return NULL;
1262   
1263 }
1264
1265 void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_dict_t *all_variables){
1266
1267   char *command = bprintf("objdump -Wi %s", elf_file);
1268   
1269   FILE *fp = popen(command, "r");
1270
1271   if(fp == NULL)
1272     perror("popen for objdump failed");
1273
1274   char *line = NULL, *origin, *abstract_origin, *current_frame = NULL;
1275   ssize_t read =0;
1276   size_t n = 0;
1277   int valid_variable = 1;
1278   char *node_type = NULL, *location_type = NULL, *variable_name = NULL, *loc_expr = NULL;
1279   xbt_dynar_t split = NULL, split2 = NULL;
1280
1281   xbt_dict_t variables_origin = xbt_dict_new_homogeneous(NULL);
1282   xbt_dict_t subprograms_origin = xbt_dict_new_homogeneous(NULL);
1283   char *subprogram_name = NULL, *subprogram_start = NULL, *subprogram_end = NULL;
1284   int new_frame = 0, new_variable = 0;
1285   dw_frame_t variable_frame, subroutine_frame = NULL;
1286
1287   read = xbt_getline(&line, &n, fp);
1288
1289   while (read != -1) {
1290
1291     if(n == 0){
1292       read = xbt_getline(&line, &n, fp);
1293       continue;
1294     }
1295  
1296     /* Wipeout the new line character */
1297     line[read - 1] = '\0';
1298    
1299     if(strlen(line) == 0){
1300       read = xbt_getline(&line, &n, fp);
1301       continue;
1302     }
1303
1304     xbt_str_ltrim(line, NULL);
1305     xbt_str_strip_spaces(line);
1306     
1307     if(line[0] != '<'){
1308       read = xbt_getline(&line, &n, fp);
1309       continue;
1310     }
1311     
1312     xbt_dynar_free(&split);
1313     split = xbt_str_split(line, " ");
1314
1315     /* Get node type */
1316     node_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
1317
1318     if(strcmp(node_type, "(DW_TAG_subprogram)") == 0){ /* New frame */
1319
1320       dw_frame_t frame = NULL;
1321
1322       strtok(xbt_dynar_get_as(split, 0, char *), "<");
1323       subprogram_start = strdup(strtok(NULL, "<"));
1324       xbt_str_rtrim(subprogram_start, ">:");
1325
1326       read = xbt_getline(&line, &n, fp);
1327    
1328       while(read != -1){
1329
1330         if(n == 0){
1331           read = xbt_getline(&line, &n, fp);
1332           continue;
1333         }
1334
1335         /* Wipeout the new line character */
1336         line[read - 1] = '\0';
1337         
1338         if(strlen(line) == 0){
1339           read = xbt_getline(&line, &n, fp);
1340           continue;
1341         }
1342       
1343         xbt_dynar_free(&split);
1344         xbt_str_rtrim(line, NULL);
1345         xbt_str_strip_spaces(line);
1346         split = xbt_str_split(line, " ");
1347           
1348         node_type = xbt_dynar_get_as(split, 1, char *);
1349
1350         if(strncmp(node_type, "DW_AT_", 6) != 0)
1351           break;
1352
1353         if(strcmp(node_type, "DW_AT_sibling") == 0){
1354
1355           subprogram_end = strdup(xbt_dynar_get_as(split, 3, char*));
1356           xbt_str_ltrim(subprogram_end, "<0x");
1357           xbt_str_rtrim(subprogram_end, ">");
1358           
1359         }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){ /* Frame already in dict */
1360           
1361           new_frame = 0;
1362           abstract_origin = strdup(xbt_dynar_get_as(split, 2, char*));
1363           xbt_str_ltrim(abstract_origin, "<0x");
1364           xbt_str_rtrim(abstract_origin, ">");
1365           subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, abstract_origin);
1366           frame = xbt_dict_get_or_null(*all_variables, subprogram_name); 
1367           xbt_free(abstract_origin);
1368
1369         }else if(strcmp(node_type, "DW_AT_name") == 0){
1370
1371           new_frame = 1;
1372           xbt_free(current_frame);
1373           frame = xbt_new0(s_dw_frame_t, 1);
1374           frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *)); 
1375           frame->variables = xbt_dict_new_homogeneous(NULL);
1376           frame->frame_base = xbt_new0(s_dw_location_t, 1); 
1377           current_frame = strdup(frame->name);
1378
1379           xbt_dict_set(subprograms_origin, subprogram_start, frame->name, NULL);
1380         
1381         }else if(strcmp(node_type, "DW_AT_frame_base") == 0){
1382
1383           location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
1384
1385           if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
1386
1387             frame->frame_base = get_location(location_list, xbt_dynar_get_as(split, 3, char *));
1388              
1389           }else{
1390                 
1391             xbt_str_strip_spaces(line);
1392             split2 = xbt_str_split(line, "(");
1393             xbt_dynar_remove_at(split2, 0, NULL);
1394             loc_expr = xbt_str_join(split2, " ");
1395             xbt_str_rtrim(loc_expr, ")");
1396             frame->frame_base = get_location(NULL, loc_expr);
1397             xbt_dynar_free(&split2);
1398             xbt_free(loc_expr);
1399
1400           }
1401  
1402         }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
1403           
1404           if(frame != NULL)
1405             frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
1406
1407         }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
1408
1409           if(frame != NULL)
1410             frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
1411
1412         }else if(strcmp(node_type, "DW_AT_MIPS_linkage_name:") == 0){
1413
1414           xbt_free(frame->name);
1415           xbt_free(current_frame);
1416           frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));   
1417           current_frame = strdup(frame->name);
1418           xbt_dict_set(subprograms_origin, subprogram_start, frame->name, NULL);
1419
1420         }
1421
1422         read = xbt_getline(&line, &n, fp);
1423
1424       }
1425  
1426       if(new_frame == 1){
1427         frame->start = strtoul(subprogram_start, NULL, 16);
1428         if(subprogram_end != NULL)
1429           frame->end = strtoul(subprogram_end, NULL, 16);
1430         xbt_dict_set(*all_variables, frame->name, frame, NULL);
1431       }
1432
1433       xbt_free(subprogram_start);
1434       xbt_free(subprogram_end);
1435       subprogram_end = NULL;
1436         
1437
1438     }else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
1439
1440       dw_local_variable_t var = NULL;
1441       
1442       strtok(xbt_dynar_get_as(split, 0, char *), "<");
1443       origin = strdup(strtok(NULL, "<"));
1444       xbt_str_rtrim(origin, ">:");
1445       
1446       read = xbt_getline(&line, &n, fp);
1447       
1448       while(read != -1){
1449
1450         if(n == 0){
1451           read = xbt_getline(&line, &n, fp);
1452           continue;
1453         }
1454
1455         /* Wipeout the new line character */
1456         line[read - 1] = '\0'; 
1457
1458         if(strlen(line) == 0){
1459           read = xbt_getline(&line, &n, fp);
1460           continue;
1461         }
1462        
1463         xbt_dynar_free(&split);
1464         xbt_str_rtrim(line, NULL);
1465         xbt_str_strip_spaces(line);
1466         split = xbt_str_split(line, " ");
1467   
1468         node_type = xbt_dynar_get_as(split, 1, char *);
1469
1470         if(strncmp(node_type, "DW_AT_", 6) != 0)
1471           break;
1472
1473         if(strcmp(node_type, "DW_AT_name") == 0){
1474
1475           new_variable = 1;
1476           var = xbt_new0(s_dw_local_variable_t, 1);
1477           var->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
1478
1479           xbt_dict_set(variables_origin, origin, var->name, NULL);
1480          
1481         }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
1482
1483           new_variable = 0;
1484           abstract_origin = xbt_dynar_get_as(split, 2, char *);
1485           xbt_str_ltrim(abstract_origin, "<0x");
1486           xbt_str_rtrim(abstract_origin, ">");
1487           
1488           variable_name = (char *)xbt_dict_get_or_null(variables_origin, abstract_origin);
1489           variable_frame = get_frame_by_offset(*all_variables, strtoul(abstract_origin, NULL, 16));
1490           var = xbt_dict_get_or_null(variable_frame->variables, variable_name);   
1491
1492         }else if(strcmp(node_type, "DW_AT_location") == 0){
1493
1494           if(valid_variable == 1 && var != NULL){
1495
1496             var->location = xbt_new0(s_dw_location_t, 1);
1497
1498             location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
1499
1500             if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
1501
1502               var->location = get_location(location_list, xbt_dynar_get_as(split, 3, char *));
1503              
1504             }else{
1505                 
1506               xbt_str_strip_spaces(line);
1507               split2 = xbt_str_split(line, "(");
1508               xbt_dynar_remove_at(split2, 0, NULL);
1509               loc_expr = xbt_str_join(split2, " ");
1510               xbt_str_rtrim(loc_expr, ")");
1511               var->location = get_location(NULL, loc_expr);
1512               xbt_dynar_free(&split2);
1513               xbt_free(loc_expr);
1514
1515             }
1516
1517           }
1518            
1519         }else if(strcmp(node_type, "DW_AT_external") == 0){
1520
1521           valid_variable = 0;
1522         
1523         }
1524
1525         read = xbt_getline(&line, &n, fp);
1526  
1527       }
1528
1529       if(new_variable == 1 && valid_variable == 1){
1530         
1531         variable_frame = xbt_dict_get_or_null(*all_variables, current_frame);
1532         xbt_dict_set(variable_frame->variables, var->name, var, NULL);
1533       }
1534
1535       valid_variable = 1;
1536       new_variable = 0;
1537
1538     }else if(strcmp(node_type, "(DW_TAG_inlined_subroutine)") == 0){
1539
1540       strtok(xbt_dynar_get_as(split, 0, char *), "<");
1541       origin = strdup(strtok(NULL, "<"));
1542       xbt_str_rtrim(origin, ">:");
1543
1544       read = xbt_getline(&line, &n, fp);
1545
1546       while(read != -1){
1547
1548         /* Wipeout the new line character */
1549         line[read - 1] = '\0'; 
1550
1551         if(n == 0){
1552           read = xbt_getline(&line, &n, fp);
1553           continue;
1554         }
1555
1556         if(strlen(line) == 0){
1557           read = xbt_getline(&line, &n, fp);
1558           continue;
1559         }
1560
1561         xbt_dynar_free(&split);
1562         xbt_str_rtrim(line, NULL);
1563         xbt_str_strip_spaces(line);
1564         split = xbt_str_split(line, " ");
1565         
1566         if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
1567           break;
1568           
1569         node_type = xbt_dynar_get_as(split, 1, char *);
1570
1571         if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
1572
1573           origin = xbt_dynar_get_as(split, 2, char *);
1574           xbt_str_ltrim(origin, "<0x");
1575           xbt_str_rtrim(origin, ">");
1576           
1577           subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, origin);
1578           subroutine_frame = xbt_dict_get_or_null(*all_variables, subprogram_name);
1579         
1580         }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
1581
1582           subroutine_frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
1583
1584         }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
1585
1586           subroutine_frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
1587         }
1588
1589         read = xbt_getline(&line, &n, fp);
1590       
1591       }
1592
1593     }else{
1594
1595       read = xbt_getline(&line, &n, fp);
1596
1597     }
1598
1599   }
1600   
1601   xbt_dynar_free(&split);
1602   xbt_free(line);
1603   xbt_free(command);
1604   pclose(fp);
1605   
1606 }
1607
1608 static dw_location_t get_location(xbt_dict_t location_list, char *expr){
1609
1610   dw_location_t loc = xbt_new0(s_dw_location_t, 1);
1611
1612   if(location_list != NULL){
1613     
1614     char *key = bprintf("%d", (int)strtoul(expr, NULL, 16));
1615     loc->type = e_dw_loclist;
1616     loc->location.loclist =  (xbt_dynar_t)xbt_dict_get_or_null(location_list, key);
1617     if(loc->location.loclist == NULL)
1618       XBT_INFO("Key not found in loclist");
1619     xbt_free(key);
1620     return loc;
1621
1622   }else{
1623
1624     int cursor = 0;
1625     char *tok = NULL, *tok2 = NULL; 
1626     
1627     xbt_dynar_t tokens1 = xbt_str_split(expr, ";");
1628     xbt_dynar_t tokens2;
1629
1630     loc->type = e_dw_compose;
1631     loc->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL);
1632
1633     while(cursor < xbt_dynar_length(tokens1)){
1634
1635       tok = xbt_dynar_get_as(tokens1, cursor, char*);
1636       tokens2 = xbt_str_split(tok, " ");
1637       tok2 = xbt_dynar_get_as(tokens2, 0, char*);
1638       
1639       if(strncmp(tok2, "DW_OP_reg", 9) == 0){
1640         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1641         new_element->type = e_dw_register;
1642         new_element->location.reg = atoi(strtok(tok2, "DW_OP_reg"));
1643         xbt_dynar_push(loc->location.compose, &new_element);     
1644       }else if(strcmp(tok2, "DW_OP_fbreg:") == 0){
1645         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1646         new_element->type = e_dw_fbregister_op;
1647         new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
1648         xbt_dynar_push(loc->location.compose, &new_element);
1649       }else if(strncmp(tok2, "DW_OP_breg", 10) == 0){
1650         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1651         new_element->type = e_dw_bregister_op;
1652         new_element->location.breg_op.reg = atoi(strtok(tok2, "DW_OP_breg"));
1653         new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
1654         xbt_dynar_push(loc->location.compose, &new_element);
1655       }else if(strncmp(tok2, "DW_OP_lit", 9) == 0){
1656         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1657         new_element->type = e_dw_lit;
1658         new_element->location.lit = atoi(strtok(tok2, "DW_OP_lit"));
1659         xbt_dynar_push(loc->location.compose, &new_element);
1660       }else if(strcmp(tok2, "DW_OP_piece:") == 0){
1661         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1662         new_element->type = e_dw_piece;
1663         new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
1664         /*if(strlen(xbt_dynar_get_as(tokens2, 1, char*)) > 1)
1665           new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, 1, char*));
1666         else
1667         new_element->location.piece = xbt_dynar_get_as(tokens2, 1, char*)[0] - '0';*/
1668         xbt_dynar_push(loc->location.compose, &new_element);
1669       }else if(strcmp(tok2, "DW_OP_plus_uconst:") == 0){
1670         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1671         new_element->type = e_dw_plus_uconst;
1672         new_element->location.plus_uconst = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char *));
1673         xbt_dynar_push(loc->location.compose, &new_element);
1674       }else if(strcmp(tok, "DW_OP_abs") == 0 || 
1675                strcmp(tok, "DW_OP_and") == 0 ||
1676                strcmp(tok, "DW_OP_div") == 0 ||
1677                strcmp(tok, "DW_OP_minus") == 0 ||
1678                strcmp(tok, "DW_OP_mod") == 0 ||
1679                strcmp(tok, "DW_OP_mul") == 0 ||
1680                strcmp(tok, "DW_OP_neg") == 0 ||
1681                strcmp(tok, "DW_OP_not") == 0 ||
1682                strcmp(tok, "DW_OP_or") == 0 ||
1683                strcmp(tok, "DW_OP_plus") == 0){               
1684         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1685         new_element->type = e_dw_arithmetic;
1686         new_element->location.arithmetic = strdup(strtok(tok2, "DW_OP_"));
1687         xbt_dynar_push(loc->location.compose, &new_element);
1688       }else if(strcmp(tok, "DW_OP_stack_value") == 0){
1689       }else if(strcmp(tok2, "DW_OP_deref_size:") == 0){
1690         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1691         new_element->type = e_dw_deref;
1692         new_element->location.deref_size = (unsigned int short) atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
1693         /*if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
1694           new_element->location.deref_size = atoi(xbt_dynar_get_as(tokens, cursor, char*));
1695         else
1696         new_element->location.deref_size = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';*/
1697         xbt_dynar_push(loc->location.compose, &new_element);
1698       }else if(strcmp(tok, "DW_OP_deref") == 0){
1699         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1700         new_element->type = e_dw_deref;
1701         new_element->location.deref_size = sizeof(void *);
1702         xbt_dynar_push(loc->location.compose, &new_element);
1703       }else if(strcmp(tok2, "DW_OP_constu:") == 0){
1704         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1705         new_element->type = e_dw_uconstant;
1706         new_element->location.uconstant.bytes = 1;
1707         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
1708         /*if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
1709           new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens, cursor, char*)));
1710         else
1711         new_element->location.uconstant.value = (unsigned long int)(xbt_dynar_get_as(tokens, cursor, char*)[0] - '0');*/
1712         xbt_dynar_push(loc->location.compose, &new_element);
1713       }else if(strcmp(tok2, "DW_OP_consts:") == 0){
1714         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1715         new_element->type = e_dw_sconstant;
1716         new_element->location.sconstant.bytes = 1;
1717         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
1718         xbt_dynar_push(loc->location.compose, &new_element);
1719       }else if(strcmp(tok2, "DW_OP_const1u:") == 0 ||
1720                strcmp(tok2, "DW_OP_const2u:") == 0 ||
1721                strcmp(tok2, "DW_OP_const4u:") == 0 ||
1722                strcmp(tok2, "DW_OP_const8u:") == 0){
1723         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1724         new_element->type = e_dw_uconstant;
1725         new_element->location.uconstant.bytes = tok2[11] - '0';
1726         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
1727         /*if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
1728           new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, cursor, char*));
1729         else
1730         new_element->location.constant.value = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';*/
1731         xbt_dynar_push(loc->location.compose, &new_element);
1732       }else if(strcmp(tok, "DW_OP_const1s") == 0 ||
1733                strcmp(tok, "DW_OP_const2s") == 0 ||
1734                strcmp(tok, "DW_OP_const4s") == 0 ||
1735                strcmp(tok, "DW_OP_const8s") == 0){
1736         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1737         new_element->type = e_dw_sconstant;
1738         new_element->location.sconstant.bytes = tok2[11] - '0';
1739         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
1740         xbt_dynar_push(loc->location.compose, &new_element);
1741       }else{
1742         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1743         new_element->type = e_dw_unsupported;
1744         xbt_dynar_push(loc->location.compose, &new_element);
1745       }
1746
1747       cursor++;
1748       xbt_dynar_free(&tokens2);
1749
1750     }
1751     
1752     xbt_dynar_free(&tokens1);
1753
1754     return loc;
1755     
1756   }
1757
1758 }
1759
1760
1761 void print_local_variables(xbt_dict_t list){
1762   
1763   dw_location_entry_t entry;
1764   dw_location_t location_entry;
1765   unsigned int cursor3 = 0, cursor4 = 0;
1766   xbt_dict_cursor_t cursor = 0, cursor2 = 0;
1767
1768   char *frame_name, *variable_name;
1769   dw_frame_t current_frame;
1770   dw_local_variable_t current_variable;
1771
1772   xbt_dict_foreach(list, cursor, frame_name, current_frame){ 
1773     fprintf(stderr, "Frame name : %s\n", current_frame->name);
1774     fprintf(stderr, "Location type : %d\n", current_frame->frame_base->type);
1775     xbt_dict_foreach((xbt_dict_t)current_frame->variables, cursor2, variable_name, current_variable){
1776       fprintf(stderr, "Name : %s\n", current_variable->name);
1777       if(current_variable->location == NULL)
1778         continue;
1779       fprintf(stderr, "Location type : %d\n", current_variable->location->type);
1780       switch(current_variable->location->type){
1781       case e_dw_loclist :
1782         xbt_dynar_foreach(current_variable->location->location.loclist, cursor3, entry){
1783           fprintf(stderr, "Lowpc : %lx, Highpc : %lx,", entry->lowpc, entry->highpc);
1784           switch(entry->location->type){
1785           case e_dw_register :
1786             fprintf(stderr, " Location : in register %d\n", entry->location->location.reg);
1787             break;
1788           case e_dw_bregister_op:
1789             fprintf(stderr, " Location : Add %d to the value in register %d\n", entry->location->location.breg_op.offset, entry->location->location.breg_op.reg);
1790             break;
1791           case e_dw_lit:
1792             fprintf(stderr, "Value already kwnown : %d\n", entry->location->location.lit);
1793             break;
1794           case e_dw_fbregister_op:
1795             fprintf(stderr, " Location : %d bytes from logical frame pointer\n", entry->location->location.fbreg_op);
1796             break;
1797           case e_dw_compose:
1798             fprintf(stderr, " Location :\n");
1799             xbt_dynar_foreach(entry->location->location.compose, cursor4, location_entry){
1800               switch(location_entry->type){
1801               case e_dw_register :
1802                 fprintf(stderr, " %d) in register %d\n", cursor4 + 1, location_entry->location.reg);
1803                 break;
1804               case e_dw_bregister_op:
1805                 fprintf(stderr, " %d) add %d to the value in register %d\n", cursor4 + 1, location_entry->location.breg_op.offset, location_entry->location.breg_op.reg);
1806                 break;
1807               case e_dw_lit:
1808                 fprintf(stderr, "%d) Value already kwnown : %d\n", cursor4 + 1, location_entry->location.lit);
1809                 break;
1810               case e_dw_fbregister_op:
1811                 fprintf(stderr, " %d) %d bytes from logical frame pointer\n", cursor4 + 1, location_entry->location.fbreg_op);
1812                 break;
1813               case e_dw_deref:
1814                 fprintf(stderr, " %d) Pop the stack entry and treats it as an address (size of data %d)\n", cursor4 + 1, location_entry->location.deref_size);
1815                 break;
1816               case e_dw_arithmetic :
1817                 fprintf(stderr, "%d) arithmetic operation : %s\n", cursor4 + 1, location_entry->location.arithmetic);
1818                 break;
1819               case e_dw_piece:
1820                 fprintf(stderr, "%d) The %d byte(s) previous value\n", cursor4 + 1, location_entry->location.piece);
1821                 break;
1822               case e_dw_uconstant :
1823                 fprintf(stderr, "%d) Unsigned constant %lu\n", cursor4 + 1, location_entry->location.uconstant.value);
1824                 break;
1825               case e_dw_sconstant :
1826                 fprintf(stderr, "%d) Signed constant %lu\n", cursor4 + 1, location_entry->location.sconstant.value);
1827                 break;
1828               default :
1829                 fprintf(stderr, "%d) Location type not supported\n", cursor4 + 1);
1830                 break;
1831               }
1832             }
1833             break;
1834           default:
1835             fprintf(stderr, "Location type not supported\n");
1836             break;
1837           }
1838         }
1839         break;
1840       case e_dw_compose:
1841         cursor4 = 0;
1842         fprintf(stderr, "Location :\n");
1843         xbt_dynar_foreach(current_variable->location->location.compose, cursor4, location_entry){
1844           switch(location_entry->type){
1845           case e_dw_register :
1846             fprintf(stderr, " %d) in register %d\n", cursor4 + 1, location_entry->location.reg);
1847             break;
1848           case e_dw_bregister_op:
1849             fprintf(stderr, " %d) add %d to the value in register %d\n", cursor4 + 1, location_entry->location.breg_op.offset, location_entry->location.breg_op.reg);
1850             break;
1851           case e_dw_lit:
1852             fprintf(stderr, "%d) Value already kwnown : %d\n", cursor4 + 1, location_entry->location.lit);
1853             break;
1854           case e_dw_fbregister_op:
1855             fprintf(stderr, " %d) %d bytes from logical frame pointer\n", cursor4 + 1, location_entry->location.fbreg_op);
1856             break;
1857           case e_dw_deref:
1858             fprintf(stderr, " %d) Pop the stack entry and treats it as an address (size of data %d)\n", cursor4 + 1, location_entry->location.deref_size);
1859             break;
1860           case e_dw_arithmetic :
1861             fprintf(stderr, "%d) arithmetic operation : %s\n", cursor4 + 1, location_entry->location.arithmetic);
1862             break;
1863           case e_dw_piece:
1864             fprintf(stderr, "%d) The %d byte(s) previous value\n", cursor4 + 1, location_entry->location.piece);
1865             break;
1866           case e_dw_uconstant :
1867             fprintf(stderr, "%d) Unsigned constant %lu\n", cursor4 + 1, location_entry->location.uconstant.value);
1868             break;
1869           case e_dw_sconstant :
1870             fprintf(stderr, "%d) Signed constant %lu\n", cursor4 + 1, location_entry->location.sconstant.value);
1871             break;
1872           default :
1873             fprintf(stderr, "%d) Location type not supported\n", cursor4 + 1);
1874             break;
1875           }
1876         }
1877         break;
1878       default :
1879         fprintf(stderr, "Location type not supported\n");
1880         break;
1881       }
1882     }
1883   }
1884
1885 }
1886
1887 static void MC_get_global_variables(char *elf_file){
1888
1889   FILE *fp;
1890
1891   char *command = bprintf("objdump -t -j .data -j .bss %s", elf_file);
1892
1893   fp = popen(command, "r");
1894
1895   if(fp == NULL){
1896     perror("popen failed");
1897     xbt_abort();
1898   }
1899
1900   if(mc_global_variables == NULL)
1901     mc_global_variables = xbt_dynar_new(sizeof(global_variable_t), global_variable_free_voidp);
1902
1903   char *line = NULL;
1904   ssize_t read;
1905   size_t n = 0;
1906
1907   xbt_dynar_t line_tokens = NULL;
1908   unsigned long offset;
1909
1910   int type = strcmp(elf_file, xbt_binary_name); /* 0 = binary, other = libsimgrid */
1911
1912   while ((read = xbt_getline(&line, &n, fp)) != -1){
1913
1914     if(n == 0)
1915       continue;
1916
1917      /* Wipeout the new line character */
1918     line[read - 1] = '\0';
1919
1920     xbt_str_strip_spaces(line);
1921     xbt_str_ltrim(line, NULL);
1922
1923     line_tokens = xbt_str_split(line, NULL);
1924
1925     if(xbt_dynar_length(line_tokens) <= 4 || strcmp(xbt_dynar_get_as(line_tokens, 0, char *), "SYMBOL") == 0)
1926       continue;
1927
1928     if((strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "__gcov", 6) == 0)
1929        || (strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "gcov", 4) == 0)
1930        || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), ".data") == 0)
1931        || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), ".bss") == 0)
1932        || (strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "stderr", 6) == 0)
1933        || ((size_t)strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char*), NULL, 16) == 0))
1934       continue;
1935
1936     global_variable_t var = xbt_new0(s_global_variable_t, 1);
1937
1938     if(type == 0){
1939       var->address = (void *)strtoul(xbt_dynar_get_as(line_tokens, 0, char*), NULL, 16);
1940     }else{
1941       offset = strtoul(xbt_dynar_get_as(line_tokens, 0, char*), NULL, 16);
1942       var->address = (char *)start_text_libsimgrid+offset;
1943     }
1944
1945     var->size = (size_t)strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char*), NULL, 16);
1946     var->name = strdup(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*));
1947
1948     if(data_bss_ignore_size(var->address) > 0){
1949       global_variable_free(var);
1950     }else{
1951       if(xbt_dynar_is_empty(mc_global_variables)){
1952         xbt_dynar_push(mc_global_variables, &var);
1953       }else{
1954         unsigned int cursor = 0;
1955         int start = 0;
1956         int end = xbt_dynar_length(mc_global_variables) - 1;
1957         global_variable_t current_var = NULL;
1958       
1959         while(start <= end){
1960           cursor = (start + end) / 2;
1961           current_var = (global_variable_t)xbt_dynar_get_as(mc_global_variables, cursor, global_variable_t);
1962           if(current_var->address == var->address)
1963             break;
1964           if(current_var->address < var->address)
1965             start = cursor + 1;
1966           if(current_var->address > var->address)
1967             end = cursor - 1;
1968         }
1969  
1970         if(current_var->address < var->address)
1971           xbt_dynar_insert_at(mc_global_variables, cursor + 1, &var);
1972         else
1973           xbt_dynar_insert_at(mc_global_variables, cursor, &var);
1974       }
1975     }
1976
1977     xbt_dynar_free(&line_tokens);
1978
1979   }
1980
1981   xbt_free(command);
1982   xbt_free(line);
1983   pclose(fp);
1984
1985 }
1986
1987 void global_variable_free(global_variable_t v){
1988   xbt_free(v->name);
1989   xbt_free(v);
1990 }
1991
1992 void global_variable_free_voidp(void *v){
1993   global_variable_free((global_variable_t) * (void **) v);
1994 }