1 /* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved. */
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. */
11 #include "../surf/surf_private.h"
12 #include "../simix/smx_private.h"
13 #include "../xbt/mmalloc/mmprivate.h"
15 #include "mc_private.h"
16 #include "xbt/automaton.h"
18 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
19 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
20 "Logging specific to MC (global)");
22 /* Configuration support */
23 e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
25 extern int _surf_init_status;
26 void _mc_cfg_cb_reduce(const char *name, int pos) {
27 if (_surf_init_status && !_surf_do_model_check) {
28 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.");
30 char *val= xbt_cfg_get_string(_surf_cfg_set, name);
31 if (!strcasecmp(val,"none")) {
32 mc_reduce_kind = e_mc_reduce_none;
33 } else if (!strcasecmp(val,"dpor")) {
34 mc_reduce_kind = e_mc_reduce_dpor;
36 xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
38 xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
41 void _mc_cfg_cb_checkpoint(const char *name, int pos) {
42 if (_surf_init_status && !_surf_do_model_check) {
43 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.");
45 _surf_mc_checkpoint = xbt_cfg_get_int(_surf_cfg_set, name);
46 xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
48 void _mc_cfg_cb_property(const char *name, int pos) {
49 if (_surf_init_status && !_surf_do_model_check) {
50 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.");
52 _surf_mc_property_file= xbt_cfg_get_string(_surf_cfg_set, name);
53 xbt_cfg_set_int(_surf_cfg_set,"model-check",1);
57 /* MC global data structures */
59 mc_state_t mc_current_state = NULL;
60 char mc_replay_mode = FALSE;
61 double *mc_time = NULL;
62 mc_snapshot_t initial_snapshot = NULL;
67 xbt_fifo_t mc_stack_safety = NULL;
68 mc_stats_t mc_stats = NULL;
72 mc_stats_pair_t mc_stats_pair = NULL;
73 xbt_fifo_t mc_stack_liveness = NULL;
74 mc_snapshot_t initial_snapshot_liveness = NULL;
78 xbt_dict_t mc_local_variables = NULL;
80 /* Ignore mechanism */
81 extern xbt_dynar_t mc_comparison_ignore;
82 extern xbt_dynar_t stacks_areas;
84 xbt_automaton_t _mc_property_automaton = NULL;
86 /* Static functions */
88 static void MC_assert_pair(int prop);
89 static dw_location_t get_location(xbt_dict_t location_list, char *expr);
90 static dw_frame_t get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset);
92 void MC_do_the_modelcheck_for_real() {
93 if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') {
94 if (mc_reduce_kind==e_mc_reduce_unset)
95 mc_reduce_kind=e_mc_reduce_dpor;
97 XBT_INFO("Check a safety property");
102 if (mc_reduce_kind==e_mc_reduce_unset)
103 mc_reduce_kind=e_mc_reduce_none;
105 XBT_INFO("Check the liveness property %s",_surf_mc_property_file);
106 MC_automaton_load(_surf_mc_property_file);
107 MC_modelcheck_liveness();
112 * \brief Initialize the model-checker data structures
114 void MC_init_safety(void)
117 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
119 /* Check if MC is already initialized */
120 if (initial_snapshot)
123 mc_time = xbt_new0(double, simix_process_maxpid);
125 /* Initialize the data structures that must be persistent across every
126 iteration of the model-checker (in RAW memory) */
130 /* Initialize statistics */
131 mc_stats = xbt_new0(s_mc_stats_t, 1);
132 mc_stats->state_size = 1;
134 /* Create exploration stack */
135 mc_stack_safety = xbt_fifo_new();
142 /* Save the initial state */
143 initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
144 MC_take_snapshot(initial_snapshot);
155 void MC_compare(void){
160 void MC_modelcheck(void)
167 void MC_modelcheck_liveness(){
169 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
172 XBT_DEBUG("Start init mc");
174 mc_time = xbt_new0(double, simix_process_maxpid);
176 /* mc_time refers to clock for each process -> ignore it for heap comparison */
178 for(i = 0; i<simix_process_maxpid; i++)
179 MC_ignore(&(mc_time[i]), sizeof(double));
183 /* Initialize the data structures that must be persistent across every
184 iteration of the model-checker (in RAW memory) */
188 /* Get local variables in binary for state equality detection */
189 MC_get_binary_local_variables();
191 /* Initialize statistics */
192 mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
194 XBT_DEBUG("Creating stack");
196 /* Create exploration stack */
197 mc_stack_liveness = xbt_fifo_new();
204 MC_print_statistics_pairs(mc_stats_pair);
213 MC_print_statistics(mc_stats);
219 int MC_random(int min, int max)
221 /*FIXME: return mc_current_state->executed_transition->random.value;*/
226 * \brief Schedules all the process that are ready to run
228 void MC_wait_for_requests(void)
230 smx_process_t process;
234 while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
235 SIMIX_process_runall();
236 xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
237 req = &process->simcall;
238 if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
239 SIMIX_simcall_pre(req, 0);
244 int MC_deadlock_check()
246 int deadlock = FALSE;
247 smx_process_t process;
248 if(xbt_swag_size(simix_global->process_list)){
250 xbt_swag_foreach(process, simix_global->process_list){
251 if(process->simcall.call != SIMCALL_NONE
252 && MC_request_is_enabled(&process->simcall)){
262 * \brief Re-executes from the state at position start all the transitions indicated by
263 * a given model-checker stack.
264 * \param stack The stack with the transitions to execute.
265 * \param start Start index to begin the re-execution.
267 void MC_replay(xbt_fifo_t stack, int start)
269 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
273 smx_simcall_t req = NULL, saved_req = NULL;
274 xbt_fifo_item_t item, start_item;
277 XBT_DEBUG("**** Begin Replay ****");
280 /* Restore the initial state */
281 MC_restore_snapshot(initial_snapshot);
282 /* At the moment of taking the snapshot the raw heap was set, so restoring
283 * it will set it back again, we have to unset it to continue */
287 start_item = xbt_fifo_get_last_item(stack);
290 start_item = xbt_fifo_get_prev_item(start_item);
295 /* Traverse the stack from the state at position start and re-execute the transitions */
296 for (item = start_item;
297 item != xbt_fifo_get_first_item(stack);
298 item = xbt_fifo_get_prev_item(item)) {
300 state = (mc_state_t) xbt_fifo_get_item_content(item);
301 saved_req = MC_state_get_executed_request(state, &value);
304 /* because we got a copy of the executed request, we have to fetch the
305 real one, pointed by the request field of the issuer process */
306 req = &saved_req->issuer->simcall;
308 /* Debug information */
309 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
310 req_str = MC_request_to_string(req, value);
311 XBT_DEBUG("Replay: %s (%p)", req_str, state);
316 SIMIX_simcall_pre(req, value);
317 MC_wait_for_requests();
319 /* Update statistics */
320 mc_stats->visited_states++;
321 mc_stats->executed_transitions++;
323 XBT_DEBUG("**** End Replay ****");
333 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
336 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
340 smx_simcall_t req = NULL, saved_req = NULL;
341 xbt_fifo_item_t item;
343 mc_pair_stateless_t pair;
346 XBT_DEBUG("**** Begin Replay ****");
348 /* Restore the initial state */
349 MC_restore_snapshot(initial_snapshot_liveness);
350 /* At the moment of taking the snapshot the raw heap was set, so restoring
351 * it will set it back again, we have to unset it to continue */
356 item = xbt_fifo_get_last_item(stack);
358 while(depth <= xbt_fifo_size(stack)){
360 pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
361 state = (mc_state_t) pair->graph_state;
363 if(pair->requests > 0){
365 saved_req = MC_state_get_executed_request(state, &value);
366 //XBT_DEBUG("SavedReq->call %u", saved_req->call);
368 if(saved_req != NULL){
369 /* because we got a copy of the executed request, we have to fetch the
370 real one, pointed by the request field of the issuer process */
371 req = &saved_req->issuer->simcall;
372 //XBT_DEBUG("Req->call %u", req->call);
374 /* Debug information */
375 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
376 req_str = MC_request_to_string(req, value);
377 XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
383 SIMIX_simcall_pre(req, value);
384 MC_wait_for_requests();
389 /* Update statistics */
390 mc_stats_pair->visited_pairs++;
392 item = xbt_fifo_get_prev_item(item);
397 /* Traverse the stack from the initial state and re-execute the transitions */
398 for (item = xbt_fifo_get_last_item(stack);
399 item != xbt_fifo_get_first_item(stack);
400 item = xbt_fifo_get_prev_item(item)) {
402 pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
403 state = (mc_state_t) pair->graph_state;
405 if(pair->requests > 0){
407 saved_req = MC_state_get_executed_request(state, &value);
408 //XBT_DEBUG("SavedReq->call %u", saved_req->call);
410 if(saved_req != NULL){
411 /* because we got a copy of the executed request, we have to fetch the
412 real one, pointed by the request field of the issuer process */
413 req = &saved_req->issuer->simcall;
414 //XBT_DEBUG("Req->call %u", req->call);
416 /* Debug information */
417 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
418 req_str = MC_request_to_string(req, value);
419 XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
425 SIMIX_simcall_pre(req, value);
426 MC_wait_for_requests();
431 /* Update statistics */
432 mc_stats_pair->visited_pairs++;
436 XBT_DEBUG("**** End Replay ****");
446 * \brief Dumps the contents of a model-checker's stack and shows the actual
448 * \param stack The stack to dump
450 void MC_dump_stack_safety(xbt_fifo_t stack)
453 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
455 MC_show_stack_safety(stack);
457 if(!_surf_mc_checkpoint){
462 while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
463 MC_state_delete(state);
476 void MC_show_stack_safety(xbt_fifo_t stack)
480 xbt_fifo_item_t item;
482 char *req_str = NULL;
484 for (item = xbt_fifo_get_last_item(stack);
485 (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
486 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
487 req = MC_state_get_executed_request(state, &value);
489 req_str = MC_request_to_string(req, value);
490 XBT_INFO("%s", req_str);
496 void MC_show_deadlock(smx_simcall_t req)
498 /*char *req_str = NULL;*/
499 XBT_INFO("**************************");
500 XBT_INFO("*** DEAD-LOCK DETECTED ***");
501 XBT_INFO("**************************");
502 XBT_INFO("Locked request:");
503 /*req_str = MC_request_to_string(req);
504 XBT_INFO("%s", req_str);
506 XBT_INFO("Counter-example execution trace:");
507 MC_dump_stack_safety(mc_stack_safety);
511 void MC_show_stack_liveness(xbt_fifo_t stack){
513 mc_pair_stateless_t pair;
514 xbt_fifo_item_t item;
516 char *req_str = NULL;
518 for (item = xbt_fifo_get_last_item(stack);
519 (item ? (pair = (mc_pair_stateless_t) (xbt_fifo_get_item_content(item)))
520 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
521 req = MC_state_get_executed_request(pair->graph_state, &value);
523 if(pair->requests>0){
524 req_str = MC_request_to_string(req, value);
525 XBT_INFO("%s", req_str);
528 XBT_INFO("End of system requests but evolution in Büchi automaton");
534 void MC_dump_stack_liveness(xbt_fifo_t stack){
536 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
538 mc_pair_stateless_t pair;
541 while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
542 MC_pair_stateless_delete(pair);
553 void MC_print_statistics(mc_stats_t stats)
555 //XBT_INFO("State space size ~= %lu", stats->state_size);
556 XBT_INFO("Expanded states = %lu", stats->expanded_states);
557 XBT_INFO("Visited states = %lu", stats->visited_states);
558 XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
559 XBT_INFO("Expanded / Visited = %lf",
560 (double) stats->visited_states / stats->expanded_states);
561 /*XBT_INFO("Exploration coverage = %lf",
562 (double)stats->expanded_states / stats->state_size); */
565 void MC_print_statistics_pairs(mc_stats_pair_t stats)
567 XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
568 XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
569 //XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
570 XBT_INFO("Expanded / Visited = %lf",
571 (double) stats->visited_pairs / stats->expanded_pairs);
572 /*XBT_INFO("Exploration coverage = %lf",
573 (double)stats->expanded_states / stats->state_size); */
576 void MC_assert(int prop)
578 if (MC_IS_ENABLED && !prop){
579 XBT_INFO("**************************");
580 XBT_INFO("*** PROPERTY NOT VALID ***");
581 XBT_INFO("**************************");
582 XBT_INFO("Counter-example execution trace:");
583 MC_dump_stack_safety(mc_stack_safety);
584 MC_print_statistics(mc_stats);
589 static void MC_assert_pair(int prop){
590 if (MC_IS_ENABLED && !prop) {
591 XBT_INFO("**************************");
592 XBT_INFO("*** PROPERTY NOT VALID ***");
593 XBT_INFO("**************************");
594 //XBT_INFO("Counter-example execution trace:");
595 MC_show_stack_liveness(mc_stack_liveness);
596 //MC_dump_snapshot_stack(mc_snapshot_stack);
597 MC_print_statistics_pairs(mc_stats_pair);
602 void MC_process_clock_add(smx_process_t process, double amount)
604 mc_time[process->pid] += amount;
607 double MC_process_clock_get(smx_process_t process)
610 return mc_time[process->pid];
615 void MC_automaton_load(const char *file){
617 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
621 if (_mc_property_automaton == NULL)
622 _mc_property_automaton = xbt_automaton_new();
624 xbt_automaton_load(_mc_property_automaton,file);
635 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
637 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
641 if (_mc_property_automaton == NULL)
642 _mc_property_automaton = xbt_automaton_new();
644 xbt_new_propositional_symbol(_mc_property_automaton,id,fct);
655 /************ MC_ignore ***********/
657 void MC_ignore(void *address, size_t size){
661 if(mc_comparison_ignore == NULL)
662 mc_comparison_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL);
664 mc_ignore_region_t region = NULL;
665 region = xbt_new0(s_mc_ignore_region_t, 1);
666 region->address = address;
669 if((address >= std_heap) && (address <= (void*)((char *)std_heap + STD_HEAP_SIZE))){
671 region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
673 if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
674 region->fragment = -1;
676 region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
681 unsigned int cursor = 0;
682 mc_ignore_region_t current_region;
683 xbt_dynar_foreach(mc_comparison_ignore, cursor, current_region){
684 if(current_region->address > address)
688 xbt_dynar_insert_at(mc_comparison_ignore, cursor, ®ion);
693 void MC_new_stack_area(void *stack, char *name){
695 if(stacks_areas == NULL)
696 stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
699 stack_region_t region = NULL;
700 region = xbt_new0(s_stack_region_t, 1);
701 region->address = stack;
702 region->process_name = strdup(name);
703 xbt_dynar_push(stacks_areas, ®ion);
707 /************ DWARF ***********/
709 static void MC_get_binary_local_variables(){
711 mc_binary_local_variables = xbt_dynar_new(sizeof(dw_frame_t), NULL);
713 char *command = bprintf("dwarfdump -i %s", xbt_binary_name);
715 FILE* fp = popen(command, "r");
718 perror("popen failed");
720 char *line = NULL, *tmp_line = NULL, *tmp_location, *frame_name = NULL;
723 int valid_variable = 1, valid_frame = 1;
724 char *node_type, *location_type, *variable_name = NULL, *lowpc, *highpc;
725 xbt_dynar_t split = NULL;
727 void *low_pc = NULL, *old_low_pc = NULL;
729 int compile_unit_found = 0; /* Detect if the program has been compiled with -g */
731 read = getline(&line, &n, fp);
738 /* Wipeout the new line character */
739 line[read - 1] = '\0';
743 /* If the program hasn't been compiled with -g, no symbol (line starting with '<' ) found */
744 compile_unit_found = 1;
749 node_type = strtok(NULL, " ");
751 if(strcmp(node_type, "DW_TAG_subprogram") == 0){ /* New frame */
753 read = getline(&line, &n, fp);
755 while(read != -1 && line[0] != '<'){
760 node_type = strtok(line, " ");
762 if(node_type != NULL && strcmp(node_type, "DW_AT_name") == 0){
764 frame_name = strdup(strtok(NULL, " "));
765 xbt_str_trim(frame_name, NULL);
766 xbt_str_trim(frame_name, "\"");
767 read = getline(&line, &n, fp);
769 }else if(node_type != NULL && strcmp(node_type, "DW_AT_frame_base") == 0){
771 if(valid_frame == 1){
773 dw_frame_t frame = xbt_new0(s_dw_frame_t, 1);
774 frame->name = strdup(frame_name);
775 frame->variables = xbt_dynar_new(sizeof(dw_local_variable_t), NULL);
776 frame->location = xbt_new0(s_dw_location_t, 1);
779 location_type = strtok(NULL, " ");
781 if(strcmp(location_type, "<loclist") == 0){
783 frame->location->type = e_dw_loclist;
784 frame->location->location.loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL);
786 read = getline(&line, &n, fp);
787 xbt_str_ltrim(line, NULL);
789 while(read != -1 && line[0] == '['){
792 lowpc = strtok(NULL, "<");
793 highpc = strtok(NULL, ">");
794 tmp_location = strtok(NULL, ">");
795 lowpc[strlen(lowpc) - 1] = '\0'; /* Remove last character '>' */
797 dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
801 new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
803 new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
806 old_low_pc = (void *)strtoul(strtok(NULL, "="), NULL, 16);
807 new_entry->lowpc = (char *)low_pc + (long)old_low_pc;
809 new_entry->highpc = (char*)low_pc + ((char *)((void *)strtoul(strtok(NULL, "="), NULL, 16)) - (char*)old_low_pc);
812 new_entry->location = xbt_new0(s_dw_location_t, 1);
814 get_location(tmp_location, new_entry->location);
816 xbt_dynar_push(frame->location->location.loclist, &new_entry);
818 read = getline(&line, &n, fp);
819 xbt_str_ltrim(line, NULL);
824 read = getline(&line, &n, fp);
825 frame->location->type = get_location(location_type, frame->location);
829 xbt_dynar_push(mc_binary_local_variables, &frame);
833 read = getline(&line, &n, fp);
837 }else if(node_type != NULL && (strcmp(node_type, "DW_AT_declaration") == 0 || strcmp(node_type, "DW_AT_abstract_origin") == 0 || strcmp(node_type, "DW_AT_artificial") == 0)){
839 read = getline(&line, &n, fp);
844 read = getline(&line, &n, fp);
852 }else if(strcmp(node_type, "DW_TAG_variable") == 0){ /* New variable */
854 read = getline(&line, &n, fp);
856 while(read != -1 && line[0] != '<'){
861 tmp_line = strdup(line);
863 node_type = strtok(line, " ");
865 if(node_type != NULL && strcmp(node_type, "DW_AT_name") == 0){
867 variable_name = strdup(strtok(NULL, " "));
868 xbt_str_trim(variable_name, NULL);
869 xbt_str_trim(variable_name, "\"");
870 read = getline(&line, &n, fp);
872 }else if(node_type != NULL && strcmp(node_type, "DW_AT_location") == 0){
874 if(valid_variable == 1){
876 location_type = strtok(NULL, " ");
878 dw_local_variable_t variable = xbt_new0(s_dw_local_variable_t, 1);
879 variable->name = strdup(variable_name);
880 variable->location = xbt_new0(s_dw_location_t, 1);
883 if(strcmp(location_type, "<loclist") == 0){
885 variable->location->type = e_dw_loclist;
886 variable->location->location.loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL);
888 read = getline(&line, &n, fp);
889 xbt_str_ltrim(line, NULL);
891 while(read != -1 && line[0] == '['){
894 lowpc = strtok(NULL, "<");
895 highpc = strtok(NULL, ">");
896 tmp_location = strtok(NULL, ">");
897 lowpc[strlen(lowpc) - 1] = '\0'; /* Remove last character '>' */
899 dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
903 new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
905 new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
908 old_low_pc = (void *)strtoul(strtok(NULL, "="), NULL, 16);
909 new_entry->lowpc = (char *)low_pc + (long)old_low_pc;
911 new_entry->highpc = (char*)low_pc + ((char *)((void *)strtoul(strtok(NULL, "="), NULL, 16)) - (char*)old_low_pc);
914 new_entry->location = xbt_new0(s_dw_location_t, 1);
916 get_location(tmp_location, new_entry->location);
918 xbt_dynar_push(variable->location->location.loclist, &new_entry);
920 read = getline(&line, &n, fp);
921 xbt_str_ltrim(line, NULL);
927 xbt_str_strip_spaces(tmp_line);
928 split = xbt_str_split(tmp_line, " ");
929 xbt_dynar_remove_at(split, 0, NULL);
930 location_type = xbt_str_join(split, " ");
932 variable->location->type = get_location(location_type, variable->location);
933 read = getline(&line, &n, fp);
935 xbt_dynar_free(&split);
940 xbt_dynar_push(((dw_frame_t)xbt_dynar_get_as(mc_binary_local_variables, xbt_dynar_length(mc_binary_local_variables) - 1, dw_frame_t))->variables, &variable);
944 read = getline(&line, &n, fp);
948 }else if(node_type != NULL && (strcmp(node_type, "DW_AT_artificial") == 0 || strcmp(node_type, "DW_AT_external") == 0)){
951 read = getline(&line, &n, fp);
955 read = getline(&line, &n, fp);
965 }else if(strcmp(node_type, "DW_TAG_compile_unit") == 0){
967 read = getline(&line, &n, fp);
969 while(read != -1 && line[0] != '<'){
974 node_type = strtok(line, " ");
976 if(node_type != NULL && strcmp(node_type, "DW_AT_low_pc") == 0){
977 low_pc = (void *) strtoul(strtok(NULL, " "), NULL, 16);
980 read = getline(&line, &n, fp);
986 read = getline(&line, &n, fp);
993 read = getline(&line, &n, fp);
1004 if(compile_unit_found == 0){
1005 XBT_INFO("Your program must be compiled with -g");
1009 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug))
1010 print_local_variables(mc_binary_local_variables);
1015 void print_local_variables(xbt_dynar_t list){
1018 dw_local_variable_t variable;
1019 dw_location_entry_t entry;
1020 dw_location_t location_entry;
1021 unsigned int cursor = 0, cursor2 = 0, cursor3 = 0, cursor4 = 0;
1023 xbt_dynar_foreach(list, cursor, frame){
1024 fprintf(stderr, "Frame name : %s", frame->name);
1025 fprintf(stderr, "Location type : %d\n", frame->location->type);
1026 fprintf(stderr, "Variables : (%lu)\n", xbt_dynar_length(frame->variables));
1027 xbt_dynar_foreach(frame->variables, cursor2, variable){
1028 fprintf(stderr, "Name : %s", variable->name);
1029 fprintf(stderr, "Location type : %d\n", variable->location->type);
1030 switch(variable->location->type){
1032 xbt_dynar_foreach(variable->location->location.loclist, cursor3, entry){
1033 fprintf(stderr, "Lowpc : %p, Highpc : %p,", entry->lowpc, entry->highpc);
1034 switch(entry->location->type){
1035 case e_dw_register :
1036 fprintf(stderr, " Location : in register %d\n", entry->location->location.reg);
1038 case e_dw_bregister_op:
1039 fprintf(stderr, " Location : Add %d to the value in register %d\n", entry->location->location.breg_op.offset, entry->location->location.breg_op.reg);
1042 fprintf(stderr, "Value already kwnown : %d\n", entry->location->location.lit);
1044 case e_dw_fbregister_op:
1045 fprintf(stderr, " Location : %d bytes from logical frame pointer\n", entry->location->location.fbreg_op);
1048 fprintf(stderr, " Location :\n");
1049 xbt_dynar_foreach(entry->location->location.compose, cursor4, location_entry){
1050 switch(location_entry->type){
1051 case e_dw_register :
1052 fprintf(stderr, " %d) in register %d\n", cursor4 + 1, location_entry->location.reg);
1054 case e_dw_bregister_op:
1055 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);
1058 fprintf(stderr, "%d) Value already kwnown : %d\n", cursor4 + 1, location_entry->location.lit);
1060 case e_dw_fbregister_op:
1061 fprintf(stderr, " %d) %d bytes from logical frame pointer\n", cursor4 + 1, location_entry->location.fbreg_op);
1064 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);
1066 case e_dw_arithmetic :
1067 fprintf(stderr, "%d) arithmetic operation : %s\n", cursor4 + 1, location_entry->location.arithmetic);
1070 fprintf(stderr, "%d) The %d byte(s) previous value\n", cursor4 + 1, location_entry->location.piece);
1072 case e_dw_constant :
1073 fprintf(stderr, "%d) Constant %d\n", cursor4 + 1, location_entry->location.constant.value);
1076 fprintf(stderr, "%d) Location type not supported\n", cursor4 + 1);
1082 fprintf(stderr, "Location type not supported\n");
1089 fprintf(stderr, "Location :\n");
1090 xbt_dynar_foreach(variable->location->location.compose, cursor4, location_entry){
1091 switch(location_entry->type){
1092 case e_dw_register :
1093 fprintf(stderr, " %d) in register %d\n", cursor4 + 1, location_entry->location.reg);
1095 case e_dw_bregister_op:
1096 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);
1099 fprintf(stderr, "%d) Value already kwnown : %d\n", cursor4 + 1, location_entry->location.lit);
1101 case e_dw_fbregister_op:
1102 fprintf(stderr, " %d) %d bytes from logical frame pointer\n", cursor4 + 1, location_entry->location.fbreg_op);
1105 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);
1107 case e_dw_arithmetic :
1108 fprintf(stderr, "%d) arithmetic operation : %s\n", cursor4 + 1, location_entry->location.arithmetic);
1111 fprintf(stderr, "%d) The %d byte(s) previous value\n", cursor4 + 1, location_entry->location.piece);
1113 case e_dw_constant :
1114 fprintf(stderr, "%d) Constant %d\n", cursor4 + 1, location_entry->location.constant.value);
1117 fprintf(stderr, "%d) Location type not supported\n", cursor4 + 1);
1123 fprintf(stderr, "Location type not supported\n");
1131 static e_dw_location_type get_location(char *expr, dw_location_t entry){
1134 char *tok = NULL, *tmp_tok = NULL;
1136 xbt_dynar_t tokens = xbt_str_split(expr, NULL);
1137 xbt_dynar_remove_at(tokens, xbt_dynar_length(tokens) - 1, NULL);
1139 if(xbt_dynar_length(tokens) > 1){
1141 entry->type = e_dw_compose;
1142 entry->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL);
1144 while(cursor < xbt_dynar_length(tokens)){
1146 tok = xbt_dynar_get_as(tokens, cursor, char*);
1148 if(strncmp(tok, "DW_OP_reg", 9) == 0){
1149 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1150 new_element->type = e_dw_register;
1152 new_element->location.reg = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1154 new_element->location.reg = atoi(strtok(tok, "DW_OP_reg"));
1156 xbt_dynar_push(entry->location.compose, &new_element);
1157 }else if(strcmp(tok, "DW_OP_fbreg") == 0){
1158 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1159 new_element->type = e_dw_fbregister_op;
1160 new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1161 xbt_dynar_push(entry->location.compose, &new_element);
1162 }else if(strncmp(tok, "DW_OP_breg", 10) == 0){
1163 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1164 new_element->type = e_dw_bregister_op;
1166 new_element->location.breg_op.reg = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1167 new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1169 if(strchr(tok,'+') != NULL){
1170 tmp_tok = strtok(tok,"DW_OP_breg");
1171 new_element->location.breg_op.reg = atoi(strtok(tmp_tok,"+"));
1172 new_element->location.breg_op.offset = atoi(strtok(NULL,"+"));
1174 new_element->location.breg_op.reg = atoi(strtok(tok, "DW_OP_breg"));
1175 new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1178 xbt_dynar_push(entry->location.compose, &new_element);
1179 }else if(strncmp(tok, "DW_OP_lit", 9) == 0){
1180 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1181 new_element->type = e_dw_lit;
1182 new_element->location.lit = atoi(strtok(tok, "DW_OP_lit"));
1183 xbt_dynar_push(entry->location.compose, &new_element);
1184 }else if(strcmp(tok, "DW_OP_piece") == 0){
1185 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1186 new_element->type = e_dw_piece;
1187 if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
1188 new_element->location.piece = atoi(xbt_dynar_get_as(tokens, cursor, char*));
1190 new_element->location.piece = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';
1191 xbt_dynar_push(entry->location.compose, &new_element);
1193 }else if(strcmp(tok, "DW_OP_abs") == 0 ||
1194 strcmp(tok, "DW_OP_and") == 0 ||
1195 strcmp(tok, "DW_OP_div") == 0 ||
1196 strcmp(tok, "DW_OP_minus") == 0 ||
1197 strcmp(tok, "DW_OP_mod") == 0 ||
1198 strcmp(tok, "DW_OP_mul") == 0 ||
1199 strcmp(tok, "DW_OP_neg") == 0 ||
1200 strcmp(tok, "DW_OP_not") == 0 ||
1201 strcmp(tok, "DW_OP_or") == 0 ||
1202 strcmp(tok, "DW_OP_plus") == 0 ||
1203 strcmp(tok, "DW_OP_plus_uconst") == 0){
1204 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1205 new_element->type = e_dw_arithmetic;
1206 new_element->location.arithmetic = strdup(strtok(tok, "DW_OP_"));
1207 xbt_dynar_push(entry->location.compose, &new_element);
1208 }else if(strcmp(tok, "DW_OP_stack_value") == 0){
1210 }else if(strcmp(tok, "DW_OP_deref_size") == 0){
1211 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1212 new_element->type = e_dw_deref;
1213 if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
1214 new_element->location.deref_size = atoi(xbt_dynar_get_as(tokens, cursor, char*));
1216 new_element->location.deref_size = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';
1217 xbt_dynar_push(entry->location.compose, &new_element);
1218 }else if(strcmp(tok, "DW_OP_deref") == 0){
1219 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1220 new_element->type = e_dw_deref;
1221 new_element->location.deref_size = sizeof(void *);
1222 xbt_dynar_push(entry->location.compose, &new_element);
1223 }else if(strcmp(tok, "DW_OP_constu") == 0){
1224 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1225 new_element->type = e_dw_constant;
1226 new_element->location.constant.is_signed = 0;
1227 new_element->location.constant.bytes = 1;
1228 if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
1229 new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, cursor, char*));
1231 new_element->location.constant.value = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';
1232 xbt_dynar_push(entry->location.compose, &new_element);
1233 }else if(strcmp(tok, "DW_OP_consts") == 0){
1234 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1235 new_element->type = e_dw_constant;
1236 new_element->location.constant.is_signed = 1;
1237 new_element->location.constant.bytes = 1;
1238 new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1239 xbt_dynar_push(entry->location.compose, &new_element);
1240 }else if(strcmp(tok, "DW_OP_const1u") == 0 ||
1241 strcmp(tok, "DW_OP_const2u") == 0 ||
1242 strcmp(tok, "DW_OP_const4u") == 0 ||
1243 strcmp(tok, "DW_OP_const8u") == 0){
1244 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1245 new_element->type = e_dw_constant;
1246 new_element->location.constant.is_signed = 0;
1247 new_element->location.constant.bytes = tok[11] - '0';
1248 if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
1249 new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, cursor, char*));
1251 new_element->location.constant.value = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';
1252 xbt_dynar_push(entry->location.compose, &new_element);
1253 }else if(strcmp(tok, "DW_OP_const1s") == 0 ||
1254 strcmp(tok, "DW_OP_const2s") == 0 ||
1255 strcmp(tok, "DW_OP_const4s") == 0 ||
1256 strcmp(tok, "DW_OP_const8s") == 0){
1257 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1258 new_element->type = e_dw_constant;
1259 new_element->location.constant.is_signed = 1;
1260 new_element->location.constant.bytes = tok[11] - '0';
1261 new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1262 xbt_dynar_push(entry->location.compose, &new_element);
1264 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1265 new_element->type = e_dw_unsupported;
1266 xbt_dynar_push(entry->location.compose, &new_element);
1273 xbt_dynar_free(&tokens);
1275 return e_dw_compose;
1279 if(strncmp(expr, "DW_OP_reg", 9) == 0){
1280 entry->type = e_dw_register;
1281 entry->location.reg = atoi(strtok(expr,"DW_OP_reg"));
1282 }else if(strncmp(expr, "DW_OP_breg", 10) == 0){
1283 entry->type = e_dw_bregister_op;
1284 tok = strtok(expr, "+");
1285 entry->location.breg_op.offset = atoi(strtok(NULL, "+"));
1286 entry->location.breg_op.reg = atoi(strtok(tok, "DW_OP_breg"));
1288 entry->type = e_dw_unsupported;
1291 xbt_dynar_free(&tokens);