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;
76 xbt_dynar_t mc_binary_local_variables = NULL;
78 extern xbt_dynar_t mmalloc_ignore;
80 xbt_automaton_t _mc_property_automaton = NULL;
82 static void MC_assert_pair(int prop);
84 void MC_do_the_modelcheck_for_real() {
85 if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') {
86 if (mc_reduce_kind==e_mc_reduce_unset)
87 mc_reduce_kind=e_mc_reduce_dpor;
89 XBT_INFO("Check a safety property");
94 if (mc_reduce_kind==e_mc_reduce_unset)
95 mc_reduce_kind=e_mc_reduce_none;
97 XBT_INFO("Check the liveness property %s",_surf_mc_property_file);
98 MC_automaton_load(_surf_mc_property_file);
99 MC_modelcheck_liveness();
104 * \brief Initialize the model-checker data structures
106 void MC_init_safety(void)
109 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
111 /* Check if MC is already initialized */
112 if (initial_snapshot)
115 mc_time = xbt_new0(double, simix_process_maxpid);
117 /* Initialize the data structures that must be persistent across every
118 iteration of the model-checker (in RAW memory) */
122 /* Initialize statistics */
123 mc_stats = xbt_new0(s_mc_stats_t, 1);
124 mc_stats->state_size = 1;
126 /* Create exploration stack */
127 mc_stack_safety = xbt_fifo_new();
134 /* Save the initial state */
135 initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
136 MC_take_snapshot(initial_snapshot);
147 void MC_compare(void){
152 void MC_modelcheck(void)
159 void MC_modelcheck_liveness(){
161 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
164 XBT_DEBUG("Start init mc");
166 mc_time = xbt_new0(double, simix_process_maxpid);
168 /* mc_time refers to clock for each process -> ignore it for heap comparison */
170 for(i = 0; i<simix_process_maxpid; i++)
171 MC_ignore(&(mc_time[i]), sizeof(double));
175 /* Initialize the data structures that must be persistent across every
176 iteration of the model-checker (in RAW memory) */
180 mc_binary_local_variables = xbt_dynar_new(sizeof(dw_frame_t), NULL);
182 /* Initialize statistics */
183 mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
185 XBT_DEBUG("Creating stack");
187 /* Create exploration stack */
188 mc_stack_liveness = xbt_fifo_new();
192 /* Get local variables in binary for state equality detection */
193 MC_get_binary_local_variables();
198 MC_print_statistics_pairs(mc_stats_pair);
207 MC_print_statistics(mc_stats);
213 int MC_random(int min, int max)
215 /*FIXME: return mc_current_state->executed_transition->random.value;*/
220 * \brief Schedules all the process that are ready to run
222 void MC_wait_for_requests(void)
224 smx_process_t process;
228 while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
229 SIMIX_process_runall();
230 xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
231 req = &process->simcall;
232 if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
233 SIMIX_simcall_pre(req, 0);
238 int MC_deadlock_check()
240 int deadlock = FALSE;
241 smx_process_t process;
242 if(xbt_swag_size(simix_global->process_list)){
244 xbt_swag_foreach(process, simix_global->process_list){
245 if(process->simcall.call != SIMCALL_NONE
246 && MC_request_is_enabled(&process->simcall)){
256 * \brief Re-executes from the state at position start all the transitions indicated by
257 * a given model-checker stack.
258 * \param stack The stack with the transitions to execute.
259 * \param start Start index to begin the re-execution.
261 void MC_replay(xbt_fifo_t stack, int start)
263 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
267 smx_simcall_t req = NULL, saved_req = NULL;
268 xbt_fifo_item_t item, start_item;
271 XBT_DEBUG("**** Begin Replay ****");
274 /* Restore the initial state */
275 MC_restore_snapshot(initial_snapshot);
276 /* At the moment of taking the snapshot the raw heap was set, so restoring
277 * it will set it back again, we have to unset it to continue */
281 start_item = xbt_fifo_get_last_item(stack);
284 start_item = xbt_fifo_get_prev_item(start_item);
289 /* Traverse the stack from the state at position start and re-execute the transitions */
290 for (item = start_item;
291 item != xbt_fifo_get_first_item(stack);
292 item = xbt_fifo_get_prev_item(item)) {
294 state = (mc_state_t) xbt_fifo_get_item_content(item);
295 saved_req = MC_state_get_executed_request(state, &value);
298 /* because we got a copy of the executed request, we have to fetch the
299 real one, pointed by the request field of the issuer process */
300 req = &saved_req->issuer->simcall;
302 /* Debug information */
303 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
304 req_str = MC_request_to_string(req, value);
305 XBT_DEBUG("Replay: %s (%p)", req_str, state);
310 SIMIX_simcall_pre(req, value);
311 MC_wait_for_requests();
313 /* Update statistics */
314 mc_stats->visited_states++;
315 mc_stats->executed_transitions++;
317 XBT_DEBUG("**** End Replay ****");
327 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
330 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
334 smx_simcall_t req = NULL, saved_req = NULL;
335 xbt_fifo_item_t item;
337 mc_pair_stateless_t pair;
340 XBT_DEBUG("**** Begin Replay ****");
342 /* Restore the initial state */
343 MC_restore_snapshot(initial_snapshot_liveness);
344 /* At the moment of taking the snapshot the raw heap was set, so restoring
345 * it will set it back again, we have to unset it to continue */
350 item = xbt_fifo_get_last_item(stack);
352 while(depth <= xbt_fifo_size(stack)){
354 pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
355 state = (mc_state_t) pair->graph_state;
357 if(pair->requests > 0){
359 saved_req = MC_state_get_executed_request(state, &value);
360 //XBT_DEBUG("SavedReq->call %u", saved_req->call);
362 if(saved_req != NULL){
363 /* because we got a copy of the executed request, we have to fetch the
364 real one, pointed by the request field of the issuer process */
365 req = &saved_req->issuer->simcall;
366 //XBT_DEBUG("Req->call %u", req->call);
368 /* Debug information */
369 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
370 req_str = MC_request_to_string(req, value);
371 XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
377 SIMIX_simcall_pre(req, value);
378 MC_wait_for_requests();
383 /* Update statistics */
384 mc_stats_pair->visited_pairs++;
386 item = xbt_fifo_get_prev_item(item);
391 /* Traverse the stack from the initial state and re-execute the transitions */
392 for (item = xbt_fifo_get_last_item(stack);
393 item != xbt_fifo_get_first_item(stack);
394 item = xbt_fifo_get_prev_item(item)) {
396 pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
397 state = (mc_state_t) pair->graph_state;
399 if(pair->requests > 0){
401 saved_req = MC_state_get_executed_request(state, &value);
402 //XBT_DEBUG("SavedReq->call %u", saved_req->call);
404 if(saved_req != NULL){
405 /* because we got a copy of the executed request, we have to fetch the
406 real one, pointed by the request field of the issuer process */
407 req = &saved_req->issuer->simcall;
408 //XBT_DEBUG("Req->call %u", req->call);
410 /* Debug information */
411 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
412 req_str = MC_request_to_string(req, value);
413 XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
419 SIMIX_simcall_pre(req, value);
420 MC_wait_for_requests();
425 /* Update statistics */
426 mc_stats_pair->visited_pairs++;
430 XBT_DEBUG("**** End Replay ****");
440 * \brief Dumps the contents of a model-checker's stack and shows the actual
442 * \param stack The stack to dump
444 void MC_dump_stack_safety(xbt_fifo_t stack)
447 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
449 MC_show_stack_safety(stack);
451 if(!_surf_mc_checkpoint){
456 while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
457 MC_state_delete(state);
470 void MC_show_stack_safety(xbt_fifo_t stack)
474 xbt_fifo_item_t item;
476 char *req_str = NULL;
478 for (item = xbt_fifo_get_last_item(stack);
479 (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
480 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
481 req = MC_state_get_executed_request(state, &value);
483 req_str = MC_request_to_string(req, value);
484 XBT_INFO("%s", req_str);
490 void MC_show_deadlock(smx_simcall_t req)
492 /*char *req_str = NULL;*/
493 XBT_INFO("**************************");
494 XBT_INFO("*** DEAD-LOCK DETECTED ***");
495 XBT_INFO("**************************");
496 XBT_INFO("Locked request:");
497 /*req_str = MC_request_to_string(req);
498 XBT_INFO("%s", req_str);
500 XBT_INFO("Counter-example execution trace:");
501 MC_dump_stack_safety(mc_stack_safety);
505 void MC_show_stack_liveness(xbt_fifo_t stack){
507 mc_pair_stateless_t pair;
508 xbt_fifo_item_t item;
510 char *req_str = NULL;
512 for (item = xbt_fifo_get_last_item(stack);
513 (item ? (pair = (mc_pair_stateless_t) (xbt_fifo_get_item_content(item)))
514 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
515 req = MC_state_get_executed_request(pair->graph_state, &value);
517 if(pair->requests>0){
518 req_str = MC_request_to_string(req, value);
519 XBT_INFO("%s", req_str);
522 XBT_INFO("End of system requests but evolution in Büchi automaton");
528 void MC_dump_stack_liveness(xbt_fifo_t stack){
530 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
532 mc_pair_stateless_t pair;
535 while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
536 MC_pair_stateless_delete(pair);
547 void MC_print_statistics(mc_stats_t stats)
549 //XBT_INFO("State space size ~= %lu", stats->state_size);
550 XBT_INFO("Expanded states = %lu", stats->expanded_states);
551 XBT_INFO("Visited states = %lu", stats->visited_states);
552 XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
553 XBT_INFO("Expanded / Visited = %lf",
554 (double) stats->visited_states / stats->expanded_states);
555 /*XBT_INFO("Exploration coverage = %lf",
556 (double)stats->expanded_states / stats->state_size); */
559 void MC_print_statistics_pairs(mc_stats_pair_t stats)
561 XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
562 XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
563 //XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
564 XBT_INFO("Expanded / Visited = %lf",
565 (double) stats->visited_pairs / stats->expanded_pairs);
566 /*XBT_INFO("Exploration coverage = %lf",
567 (double)stats->expanded_states / stats->state_size); */
570 void MC_assert(int prop)
572 if (MC_IS_ENABLED && !prop){
573 XBT_INFO("**************************");
574 XBT_INFO("*** PROPERTY NOT VALID ***");
575 XBT_INFO("**************************");
576 XBT_INFO("Counter-example execution trace:");
577 MC_dump_stack_safety(mc_stack_safety);
578 MC_print_statistics(mc_stats);
583 static void MC_assert_pair(int prop){
584 if (MC_IS_ENABLED && !prop) {
585 XBT_INFO("**************************");
586 XBT_INFO("*** PROPERTY NOT VALID ***");
587 XBT_INFO("**************************");
588 //XBT_INFO("Counter-example execution trace:");
589 MC_show_stack_liveness(mc_stack_liveness);
590 //MC_dump_snapshot_stack(mc_snapshot_stack);
591 MC_print_statistics_pairs(mc_stats_pair);
596 void MC_process_clock_add(smx_process_t process, double amount)
598 mc_time[process->pid] += amount;
601 double MC_process_clock_get(smx_process_t process)
604 return mc_time[process->pid];
609 void MC_automaton_load(const char *file){
611 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
615 if (_mc_property_automaton == NULL)
616 _mc_property_automaton = xbt_automaton_new();
618 xbt_automaton_load(_mc_property_automaton,file);
629 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
631 raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
635 if (_mc_property_automaton == NULL)
636 _mc_property_automaton = xbt_automaton_new();
638 xbt_new_propositional_symbol(_mc_property_automaton,id,fct);
649 /************ MC_ignore ***********/
651 void MC_ignore_init(){
653 mmalloc_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL);
657 void MC_ignore(void *address, size_t size){
661 mc_ignore_region_t region = NULL;
662 region = xbt_new0(s_mc_ignore_region_t, 1);
663 region->address = address;
665 region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
667 if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
668 region->fragment = -1;
670 region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
673 unsigned int cursor = 0;
674 mc_ignore_region_t current_region;
675 xbt_dynar_foreach(mmalloc_ignore, cursor, current_region){
676 if(current_region->address > address)
680 xbt_dynar_insert_at(mmalloc_ignore, cursor, ®ion);
685 /************ DWARF ***********/
687 static e_dw_location_type get_location(char *expr, dw_location_t entry);
689 void MC_get_binary_local_variables(){
691 char *command = bprintf("dwarfdump -i %s", xbt_binary_name);
693 FILE* fp = popen(command, "r");
696 perror("popen failed");
698 char *line = NULL, *tmp_line = NULL, *tmp_location = NULL, *frame_name = NULL;
701 int valid_variable = 1, valid_frame = 1;
702 char *node_type = NULL, *location_type = NULL, *variable_name = NULL, *lowpc = NULL, *highpc = NULL;
703 xbt_dynar_t split = NULL;
705 read = getline(&line, &n, fp);
712 /* Wipeout the new line character */
713 line[read - 1] = '\0';
720 node_type = strtok(NULL, " ");
722 if(strcmp(node_type, "DW_TAG_subprogram") == 0){ /* New frame */
724 read = getline(&line, &n, fp);
726 while(read != -1 && line[0] != '<'){
731 node_type = strtok(line, " ");
733 if(node_type != NULL && strcmp(node_type, "DW_AT_name") == 0){
735 frame_name = strdup(strtok(NULL, " "));
736 read = getline(&line, &n, fp);
738 }else if(node_type != NULL && strcmp(node_type, "DW_AT_frame_base") == 0){
740 if(valid_frame == 1){
742 dw_frame_t frame = xbt_new0(s_dw_frame_t, 1);
743 frame->name = strdup(frame_name);
744 frame->variables = xbt_dynar_new(sizeof(dw_local_variable_t), NULL);
745 frame->location = xbt_new0(s_dw_location_t, 1);
747 location_type = strtok(NULL, " ");
749 if(strcmp(location_type, "<loclist") == 0){
751 frame->location->type = e_dw_loclist;
752 frame->location->location.loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL);
754 read = getline(&line, &n, fp);
755 xbt_str_ltrim(line, NULL);
757 while(read != -1 && line[0] == '['){
760 lowpc = strdup(strtok(NULL, "<"));
761 highpc = strdup(strtok(NULL, ">"));
762 tmp_location = strdup(strtok(NULL, ">"));
763 lowpc[strlen(lowpc) - 1] = '\0'; /* Remove last character '>' */
765 dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
768 new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
770 new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
772 new_entry->location = xbt_new0(s_dw_location_t, 1);
774 get_location(tmp_location, new_entry->location);
776 xbt_dynar_push(frame->location->location.loclist, &new_entry);
778 read = getline(&line, &n, fp);
779 xbt_str_ltrim(line, NULL);
783 read = getline(&line, &n, fp);
784 frame->location->type = get_location(location_type, frame->location);
788 xbt_dynar_push(mc_binary_local_variables, &frame);
792 read = getline(&line, &n, fp);
796 }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)){
798 read = getline(&line, &n, fp);
803 read = getline(&line, &n, fp);
811 }else if(strcmp(node_type, "DW_TAG_variable") == 0){ /* New variable */
813 variable_name = NULL;
814 location_type = NULL;
816 read = getline(&line, &n, fp);
818 while(read != -1 && line[0] != '<'){
823 tmp_line = strdup(line);
825 node_type = strtok(line, " ");
827 if(node_type != NULL && strcmp(node_type, "DW_AT_name") == 0){
829 variable_name = strdup(strtok(NULL, " "));
830 read = getline(&line, &n, fp);
832 }else if(node_type != NULL && strcmp(node_type, "DW_AT_location") == 0){
834 if(valid_variable == 1){
836 location_type = strdup(strtok(NULL, " "));
838 dw_local_variable_t variable = xbt_new0(s_dw_local_variable_t, 1);
839 variable->name = strdup(variable_name);
840 variable->location = xbt_new0(s_dw_location_t, 1);
842 if(strcmp(location_type, "<loclist") == 0){
844 variable->location->type = e_dw_loclist;
845 variable->location->location.loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL);
847 read = getline(&line, &n, fp);
848 xbt_str_ltrim(line, NULL);
850 while(read != -1 && line[0] == '['){
853 lowpc = strdup(strtok(NULL, "<"));
854 highpc = strdup(strtok(NULL, ">"));
855 tmp_location = strdup(strtok(NULL, ">"));
856 lowpc[strlen(lowpc) - 1] = '\0'; /* Remove last character '>' */
858 dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
861 new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
863 new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16);
865 new_entry->location = xbt_new0(s_dw_location_t, 1);
867 get_location(tmp_location, new_entry->location);
869 xbt_dynar_push(variable->location->location.loclist, &new_entry);
871 read = getline(&line, &n, fp);
872 xbt_str_ltrim(line, NULL);
877 xbt_str_strip_spaces(tmp_line);
878 split = xbt_str_split(tmp_line, " ");
879 xbt_dynar_remove_at(split, 0, NULL);
880 location_type = xbt_str_join(split, " ");
882 variable->location->type = get_location(location_type, variable->location);
883 read = getline(&line, &n, fp);
887 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);
891 read = getline(&line, &n, fp);
895 }else if(node_type != NULL && (strcmp(node_type, "DW_AT_artificial") == 0 || strcmp(node_type, "DW_AT_external") == 0)){
898 read = getline(&line, &n, fp);
902 read = getline(&line, &n, fp);
912 read = getline(&line, &n, fp);
918 read = getline(&line, &n, fp);
924 print_local_variables(mc_binary_local_variables);
926 free(line); free(tmp_line); free(tmp_location); free(frame_name);
927 free(node_type); free(location_type); free(variable_name); free(lowpc); free(highpc);
932 void print_local_variables(xbt_dynar_t list){
935 dw_local_variable_t variable;
936 dw_location_entry_t entry;
937 dw_location_t location_entry;
938 unsigned int cursor = 0, cursor2 = 0, cursor3 = 0, cursor4 = 0;
940 xbt_dynar_foreach(list, cursor, frame){
941 fprintf(stderr, "Frame name : %s", frame->name);
942 fprintf(stderr, "Location type : %d\n", frame->location->type);
943 fprintf(stderr, "Variables : (%lu)\n", xbt_dynar_length(frame->variables));
944 xbt_dynar_foreach(frame->variables, cursor2, variable){
945 fprintf(stderr, "Name : %s", variable->name);
946 fprintf(stderr, "Location type : %d\n", variable->location->type);
947 switch(variable->location->type){
949 xbt_dynar_foreach(variable->location->location.loclist, cursor3, entry){
950 fprintf(stderr, "Lowpc : %p, Highpc : %p,", entry->lowpc, entry->highpc);
951 switch(entry->location->type){
953 fprintf(stderr, " Location : in register %d\n", entry->location->location.reg);
955 case e_dw_bregister_op:
956 fprintf(stderr, " Location : Add %d to the value in register %d\n", entry->location->location.breg_op.offset, entry->location->location.breg_op.reg);
959 fprintf(stderr, "Value already kwnown : %d\n", entry->location->location.lit);
961 case e_dw_fbregister_op:
962 fprintf(stderr, " Location : %d bytes from logical frame pointer\n", entry->location->location.fbreg_op);
965 fprintf(stderr, " Location :\n");
966 xbt_dynar_foreach(entry->location->location.compose, cursor4, location_entry){
967 switch(location_entry->type){
969 fprintf(stderr, " %d) in register %d\n", cursor4 + 1, location_entry->location.reg);
971 case e_dw_bregister_op:
972 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);
975 fprintf(stderr, "%d) Value already kwnown : %d\n", cursor4 + 1, location_entry->location.lit);
977 case e_dw_fbregister_op:
978 fprintf(stderr, " %d) %d bytes from logical frame pointer\n", cursor4 + 1, location_entry->location.fbreg_op);
981 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);
983 case e_dw_arithmetic :
984 fprintf(stderr, "%d) arithmetic operation : %s\n", cursor4 + 1, location_entry->location.arithmetic);
987 fprintf(stderr, "%d) The %d byte(s) previous value\n", cursor4 + 1, location_entry->location.piece);
990 fprintf(stderr, "%d) Constant %d\n", cursor4 + 1, location_entry->location.constant.value);
993 fprintf(stderr, "%d) Location type not supported\n", cursor4 + 1);
999 fprintf(stderr, "Location type not supported\n");
1006 fprintf(stderr, "Location :\n");
1007 xbt_dynar_foreach(variable->location->location.compose, cursor4, location_entry){
1008 switch(location_entry->type){
1009 case e_dw_register :
1010 fprintf(stderr, " %d) in register %d\n", cursor4 + 1, location_entry->location.reg);
1012 case e_dw_bregister_op:
1013 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);
1016 fprintf(stderr, "%d) Value already kwnown : %d\n", cursor4 + 1, location_entry->location.lit);
1018 case e_dw_fbregister_op:
1019 fprintf(stderr, " %d) %d bytes from logical frame pointer\n", cursor4 + 1, location_entry->location.fbreg_op);
1022 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);
1024 case e_dw_arithmetic :
1025 fprintf(stderr, "%d) arithmetic operation : %s\n", cursor4 + 1, location_entry->location.arithmetic);
1028 fprintf(stderr, "%d) The %d byte(s) previous value\n", cursor4 + 1, location_entry->location.piece);
1030 case e_dw_constant :
1031 fprintf(stderr, "%d) Constant %d\n", cursor4 + 1, location_entry->location.constant.value);
1034 fprintf(stderr, "%d) Location type not supported\n", cursor4 + 1);
1040 fprintf(stderr, "Location type not supported\n");
1048 static e_dw_location_type get_location(char *expr, dw_location_t entry){
1051 char *tok = NULL, *tmp_tok = NULL;
1053 xbt_dynar_t tokens = xbt_str_split(expr, NULL);
1054 xbt_dynar_remove_at(tokens, xbt_dynar_length(tokens) - 1, NULL);
1056 if(xbt_dynar_length(tokens) > 1){
1058 entry->type = e_dw_compose;
1059 entry->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL);
1061 while(cursor < xbt_dynar_length(tokens)){
1063 tok = xbt_dynar_get_as(tokens, cursor, char*);
1065 if(strncmp(tok, "DW_OP_reg", 9) == 0){
1066 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1067 new_element->type = e_dw_register;
1069 new_element->location.reg = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1071 new_element->location.reg = atoi(strtok(tok, "DW_OP_reg"));
1073 xbt_dynar_push(entry->location.compose, &new_element);
1074 }else if(strcmp(tok, "DW_OP_fbreg") == 0){
1075 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1076 new_element->type = e_dw_fbregister_op;
1077 new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1078 xbt_dynar_push(entry->location.compose, &new_element);
1079 }else if(strncmp(tok, "DW_OP_breg", 10) == 0){
1080 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1081 new_element->type = e_dw_bregister_op;
1083 new_element->location.breg_op.reg = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1084 new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1086 if(strchr(tok,'+') != NULL){
1087 tmp_tok = strtok(tok,"DW_OP_breg");
1088 new_element->location.breg_op.reg = atoi(strtok(tmp_tok,"+"));
1089 new_element->location.breg_op.offset = atoi(strtok(NULL,"+"));
1091 new_element->location.breg_op.reg = atoi(strtok(tok, "DW_OP_breg"));
1092 new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1095 xbt_dynar_push(entry->location.compose, &new_element);
1096 }else if(strncmp(tok, "DW_OP_lit", 9) == 0){
1097 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1098 new_element->type = e_dw_lit;
1099 new_element->location.lit = atoi(strtok(tok, "DW_OP_lit"));
1100 xbt_dynar_push(entry->location.compose, &new_element);
1101 }else if(strcmp(tok, "DW_OP_piece") == 0){
1102 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1103 new_element->type = e_dw_piece;
1104 if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
1105 new_element->location.piece = atoi(xbt_dynar_get_as(tokens, cursor, char*));
1107 new_element->location.piece = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';
1108 xbt_dynar_push(entry->location.compose, &new_element);
1110 }else if(strcmp(tok, "DW_OP_abs") == 0 ||
1111 strcmp(tok, "DW_OP_and") == 0 ||
1112 strcmp(tok, "DW_OP_div") == 0 ||
1113 strcmp(tok, "DW_OP_minus") == 0 ||
1114 strcmp(tok, "DW_OP_mod") == 0 ||
1115 strcmp(tok, "DW_OP_mul") == 0 ||
1116 strcmp(tok, "DW_OP_neg") == 0 ||
1117 strcmp(tok, "DW_OP_not") == 0 ||
1118 strcmp(tok, "DW_OP_or") == 0 ||
1119 strcmp(tok, "DW_OP_plus") == 0 ||
1120 strcmp(tok, "DW_OP_plus_uconst") == 0){
1121 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1122 new_element->type = e_dw_arithmetic;
1123 new_element->location.arithmetic = strdup(strtok(tok, "DW_OP_"));
1124 xbt_dynar_push(entry->location.compose, &new_element);
1125 }else if(strcmp(tok, "DW_OP_stack_value") == 0){
1127 }else if(strcmp(tok, "DW_OP_deref_size") == 0){
1128 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1129 new_element->type = e_dw_deref;
1130 if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
1131 new_element->location.deref_size = atoi(xbt_dynar_get_as(tokens, cursor, char*));
1133 new_element->location.deref_size = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';
1134 xbt_dynar_push(entry->location.compose, &new_element);
1135 }else if(strcmp(tok, "DW_OP_deref") == 0){
1136 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1137 new_element->type = e_dw_deref;
1138 new_element->location.deref_size = sizeof(void *);
1139 xbt_dynar_push(entry->location.compose, &new_element);
1140 }else if(strcmp(tok, "DW_OP_constu") == 0){
1141 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1142 new_element->type = e_dw_constant;
1143 new_element->location.constant.is_signed = 0;
1144 new_element->location.constant.bytes = 1;
1145 if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
1146 new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, cursor, char*));
1148 new_element->location.constant.value = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';
1149 xbt_dynar_push(entry->location.compose, &new_element);
1150 }else if(strcmp(tok, "DW_OP_consts") == 0){
1151 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1152 new_element->type = e_dw_constant;
1153 new_element->location.constant.is_signed = 1;
1154 new_element->location.constant.bytes = 1;
1155 new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1156 xbt_dynar_push(entry->location.compose, &new_element);
1157 }else if(strcmp(tok, "DW_OP_const1u") == 0 ||
1158 strcmp(tok, "DW_OP_const2u") == 0 ||
1159 strcmp(tok, "DW_OP_const4u") == 0 ||
1160 strcmp(tok, "DW_OP_const8u") == 0){
1161 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1162 new_element->type = e_dw_constant;
1163 new_element->location.constant.is_signed = 0;
1164 new_element->location.constant.bytes = tok[11] - '0';
1165 if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
1166 new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, cursor, char*));
1168 new_element->location.constant.value = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';
1169 xbt_dynar_push(entry->location.compose, &new_element);
1170 }else if(strcmp(tok, "DW_OP_const1s") == 0 ||
1171 strcmp(tok, "DW_OP_const2s") == 0 ||
1172 strcmp(tok, "DW_OP_const4s") == 0 ||
1173 strcmp(tok, "DW_OP_const8s") == 0){
1174 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1175 new_element->type = e_dw_constant;
1176 new_element->location.constant.is_signed = 1;
1177 new_element->location.constant.bytes = tok[11] - '0';
1178 new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, ++cursor, char*));
1179 xbt_dynar_push(entry->location.compose, &new_element);
1181 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
1182 new_element->type = e_dw_unsupported;
1183 xbt_dynar_push(entry->location.compose, &new_element);
1192 /*xbt_dynar_free(&tokens);*/
1194 return e_dw_compose;
1198 if(strncmp(expr, "DW_OP_reg", 9) == 0){
1199 entry->type = e_dw_register;
1200 entry->location.reg = atoi(strtok(expr,"DW_OP_reg"));
1201 }else if(strncmp(expr, "DW_OP_breg", 10) == 0){
1202 entry->type = e_dw_bregister_op;
1203 tok = strtok(expr, "+");
1204 entry->location.breg_op.offset = atoi(strtok(NULL, "+"));
1205 entry->location.breg_op.reg = atoi(strtok(tok, "DW_OP_breg"));
1207 entry->type = e_dw_unsupported;