Logo AND Algorithmique Numérique Distribuée

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