X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f2df13795e01302813a6aef10825ec7e922ce530..5334ced8ad322f88a152cc6f8213d1a42569f4e7:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 0c6c04d46e..5972642263 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -8,6 +8,7 @@ #include #include #include +#include #include #include "simgrid/sg_config.h" @@ -159,6 +160,7 @@ void mc_frame_free(dw_frame_t frame){ xbt_free(frame->name); mc_dwarf_location_list_clear(&(frame->frame_base)); xbt_dynar_free(&(frame->variables)); + xbt_dynar_free(&(frame->scopes)); xbt_free(frame); } @@ -212,6 +214,8 @@ void MC_free_object_info(mc_object_info_t* info) { // ***** Helpers void* MC_object_base_address(mc_object_info_t info) { + if(info->flags & MC_OBJECT_INFO_EXECUTABLE) + return 0; void* result = info->start_exec; if(info->start_rw!=NULL && result > (void*) info->start_rw) result = info->start_rw; if(info->start_ro!=NULL && result > (void*) info->start_ro) result = info->start_ro; @@ -276,7 +280,7 @@ static dw_frame_t MC_find_function_by_ip_and_object(void* ip, mc_object_info_t i int k = i + ((j-i)/2); if(ip < base[k].low_pc) { j = k-1; - } else if(ip > base[k].high_pc) { + } else if(ip >= base[k].high_pc) { i = k+1; } else { return base[k].function; @@ -303,18 +307,41 @@ static void MC_post_process_variables(mc_object_info_t info) { } } +static void mc_post_process_scope(mc_object_info_t info, dw_frame_t scope) { + + if(scope->tag == DW_TAG_inlined_subroutine) { + + // Attach correct namespaced name in inlined subroutine: + char* key = bprintf("%" PRIx64, (uint64_t) scope->abstract_origin_id); + dw_frame_t abstract_origin = xbt_dict_get_or_null(info->subprograms, key); + xbt_assert(abstract_origin, "Could not lookup abstract origin %s", key); + xbt_free(key); + scope->name = xbt_strdup(abstract_origin->name); + + } + + // Direct: + unsigned cursor = 0; + dw_variable_t variable = NULL; + xbt_dynar_foreach(scope->variables, cursor, variable) { + if(variable->type_origin) { + variable->type = xbt_dict_get_or_null(info->types, variable->type_origin); + } + } + + // Recursive post-processing of nested-scopes: + dw_frame_t nested_scope = NULL; + xbt_dynar_foreach(scope->scopes, cursor, nested_scope) + mc_post_process_scope(info, nested_scope); + +} + static void MC_post_process_functions(mc_object_info_t info) { xbt_dict_cursor_t cursor; char* key; - dw_frame_t function = NULL; - xbt_dict_foreach(info->subprograms, cursor, key, function) { - unsigned cursor2 = 0; - dw_variable_t variable = NULL; - xbt_dynar_foreach(function->variables, cursor2, variable) { - if(variable->type_origin) { - variable->type = xbt_dict_get_or_null(info->types, variable->type_origin); - } - } + dw_frame_t subprogram = NULL; + xbt_dict_foreach(info->subprograms, cursor, key, subprogram) { + mc_post_process_scope(info, subprogram); } } @@ -335,41 +362,6 @@ mc_object_info_t MC_find_object_info(memory_map_t maps, char* name, int executab /*************************************************************************/ -/** \brief Finds a frame (DW_TAG_subprogram) from an DWARF offset in the rangd of this subprogram - * - * The offset can be an offset of a child DW_TAG_variable. - */ -static dw_frame_t MC_dwarf_get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset){ - - xbt_dict_cursor_t cursor = NULL; - char *name; - dw_frame_t res; - - xbt_dict_foreach(all_variables, cursor, name, res) { - if(offset >= res->start && offset < res->end){ - xbt_dict_cursor_free(&cursor); - return res; - } - } - - xbt_dict_cursor_free(&cursor); - return NULL; - -} - -static dw_variable_t MC_dwarf_get_variable_by_name(dw_frame_t frame, char *var){ - - unsigned int cursor = 0; - dw_variable_t current_var; - - xbt_dynar_foreach(frame->variables, cursor, current_var){ - if(strcmp(var, current_var->name) == 0) - return current_var; - } - - return NULL; -} - static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *address){ if(xbt_dynar_is_empty(variables)) @@ -480,9 +472,9 @@ static void checkpoint_ignore_region_free_voidp(void *r){ void MC_ignore_heap(void *address, size_t size){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; mc_heap_ignore_region_t region = NULL; region = xbt_new0(s_mc_heap_ignore_region_t, 1); @@ -503,7 +495,7 @@ void MC_ignore_heap(void *address, size_t size){ mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp); xbt_dynar_push(mc_heap_comparison_ignore, ®ion); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return; } @@ -518,7 +510,7 @@ void MC_ignore_heap(void *address, size_t size){ if(current_region->address == address){ heap_ignore_region_free(region); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return; }else if(current_region->address < address){ start = cursor + 1; @@ -533,14 +525,14 @@ void MC_ignore_heap(void *address, size_t size){ xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_remove_ignore_heap(void *address, size_t size){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; unsigned int cursor = 0; int start = 0; @@ -572,15 +564,15 @@ void MC_remove_ignore_heap(void *address, size_t size){ } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_ignore_global_variable(const char *name){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; xbt_assert(mc_libsimgrid_info, "MC subsystem not initialized"); @@ -604,64 +596,98 @@ void MC_ignore_global_variable(const char *name){ } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } -static void MC_ignore_local_variable_in_object(const char *var_name, const char *frame_name, mc_object_info_t info) { - xbt_dict_cursor_t cursor2; - dw_frame_t frame; - int start, end; - int cursor = 0; - dw_variable_t current_var; - char* key; - xbt_dict_foreach(info->subprograms, cursor2, key, frame) { +/** \brief Ignore a local variable in a scope + * + * Ignore all instances of variables with a given name in + * any (possibly inlined) subprogram with a given namespaced + * name. + * + * \param var_name Name of the local variable (or parameter to ignore) + * \param subprogram_name Name of the subprogram fo ignore (NULL for any) + * \param subprogram (possibly inlined) Subprogram of the scope + * \param scope Current scope + */ +static void mc_ignore_local_variable_in_scope( + const char *var_name, const char *subprogram_name, + dw_frame_t subprogram, dw_frame_t scope) { + // Processing of direct variables: - if(frame_name && strcmp(frame_name, frame->name)) - continue; + // If the current subprogram matche the given name: + if(subprogram_name==NULL || strcmp(subprogram_name, subprogram->name)==0) { + + // Try to find the variable and remove it: + int start = 0; + int end = xbt_dynar_length(scope->variables) - 1; - start = 0; - end = xbt_dynar_length(frame->variables) - 1; + // Dichotomic search: while(start <= end){ - cursor = (start + end) / 2; - current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t); + int cursor = (start + end) / 2; + dw_variable_t current_var = (dw_variable_t)xbt_dynar_get_as(scope->variables, cursor, dw_variable_t); int compare = strcmp(current_var->name, var_name); if(compare == 0){ - xbt_dynar_remove_at(frame->variables, cursor, NULL); + // Variable found, remove it: + xbt_dynar_remove_at(scope->variables, cursor, NULL); + + // and start again: start = 0; - end = xbt_dynar_length(frame->variables) - 1; + end = xbt_dynar_length(scope->variables) - 1; }else if(compare < 0){ start = cursor + 1; }else{ end = cursor - 1; } } + + } + + // And recursive processing in nested scopes: + unsigned cursor = 0; + dw_frame_t nested_scope = NULL; + xbt_dynar_foreach(scope->scopes, cursor, nested_scope) { + // The new scope may be an inlined subroutine, in this case we want to use its + // namespaced name in recursive calls: + dw_frame_t nested_subprogram = nested_scope->tag == DW_TAG_inlined_subroutine ? nested_scope : subprogram; + + mc_ignore_local_variable_in_scope(var_name, subprogram_name, nested_subprogram, nested_scope); + } +} + +static void MC_ignore_local_variable_in_object(const char *var_name, const char *subprogram_name, mc_object_info_t info) { + xbt_dict_cursor_t cursor2; + dw_frame_t frame; + char* key; + xbt_dict_foreach(info->subprograms, cursor2, key, frame) { + mc_ignore_local_variable_in_scope(var_name, subprogram_name, frame, frame); } } void MC_ignore_local_variable(const char *var_name, const char *frame_name){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); if(strcmp(frame_name, "*") == 0) frame_name = NULL; - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; MC_ignore_local_variable_in_object(var_name, frame_name, mc_libsimgrid_info); if(frame_name!=NULL) MC_ignore_local_variable_in_object(var_name, frame_name, mc_binary_info); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_new_stack_area(void *stack, char *name, void* context, size_t size){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(stacks_areas == NULL) stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL); @@ -676,14 +702,14 @@ void MC_new_stack_area(void *stack, char *name, void* context, size_t size){ xbt_dynar_push(stacks_areas, ®ion); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_ignore(void *addr, size_t size){ - int raw_mem_set= (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set= (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if(mc_checkpoint_ignore == NULL) mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp); @@ -708,7 +734,7 @@ void MC_ignore(void *addr, size_t size){ if(current_region->size == size){ checkpoint_ignore_region_free(region); if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; return; }else if(current_region->size < size){ start = cursor + 1; @@ -736,7 +762,7 @@ void MC_ignore(void *addr, size_t size){ } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } /******************************* Initialisation of MC *******************************/ @@ -784,14 +810,14 @@ static void MC_init_debug_info(void) { void MC_init(){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); compare = 0; /* Initialize the data structures that must be persistent across every iteration of the model-checker (in RAW memory) */ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; MC_init_memory_map_info(); MC_init_debug_info(); @@ -799,7 +825,7 @@ void MC_init(){ /* Init parmap */ parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */ MC_ignore_local_variable("e", "*"); @@ -839,7 +865,7 @@ void MC_init(){ } if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; } @@ -875,9 +901,9 @@ static void MC_init_dot_output(){ /* FIXME : more colors */ void MC_do_the_modelcheck_for_real() { - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') { if (mc_reduce_kind==e_mc_reduce_unset) @@ -899,7 +925,7 @@ void MC_do_the_modelcheck_for_real() { void MC_modelcheck_safety(void) { - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); /* Check if MC is already initialized */ if (initial_state_safety) @@ -913,7 +939,7 @@ void MC_modelcheck_safety(void) /* Initialize the data structures that must be persistent across every iteration of the model-checker (in RAW memory) */ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Initialize statistics */ mc_stats = xbt_new0(s_mc_stats_t, 1); @@ -925,32 +951,32 @@ void MC_modelcheck_safety(void) if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')) MC_init_dot_output(); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(_sg_mc_visited > 0){ MC_init(); }else{ - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; MC_init_memory_map_info(); MC_init_debug_info(); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } MC_dpor_init(); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Save the initial state */ initial_state_safety = xbt_new0(s_mc_global_t, 1); initial_state_safety->snapshot = MC_take_snapshot(0); initial_state_safety->initial_communications_pattern_done = 0; initial_state_safety->comm_deterministic = 1; initial_state_safety->send_deterministic = 1; - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_dpor(); if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; xbt_abort(); //MC_exit(); @@ -958,7 +984,7 @@ void MC_modelcheck_safety(void) void MC_modelcheck_liveness(){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); MC_init(); @@ -967,7 +993,7 @@ void MC_modelcheck_liveness(){ /* mc_time refers to clock for each process -> ignore it for heap comparison */ MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double)); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; /* Initialize statistics */ mc_stats = xbt_new0(s_mc_stats_t, 1); @@ -982,7 +1008,7 @@ void MC_modelcheck_liveness(){ if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')) MC_init_dot_output(); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; MC_ddfs_init(); @@ -991,7 +1017,7 @@ void MC_modelcheck_liveness(){ xbt_free(mc_time); if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; } @@ -1060,7 +1086,7 @@ int MC_deadlock_check() */ void MC_replay(xbt_fifo_t stack, int start) { - int raw_mem = (mmalloc_get_current_heap() == raw_heap); + int raw_mem = (mmalloc_get_current_heap() == mc_heap); int value, i = 1, count = 1; char *req_str; @@ -1069,6 +1095,7 @@ void MC_replay(xbt_fifo_t stack, int start) mc_state_t state; smx_process_t process = NULL; int comm_pattern = 0; + smx_action_t current_comm; XBT_DEBUG("**** Begin Replay ****"); @@ -1077,7 +1104,7 @@ void MC_replay(xbt_fifo_t stack, int start) MC_restore_snapshot(initial_state_safety->snapshot); /* At the moment of taking the snapshot the raw heap was set, so restoring * it will set it back again, we have to unset it to continue */ - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } start_item = xbt_fifo_get_last_item(stack); @@ -1088,19 +1115,26 @@ void MC_replay(xbt_fifo_t stack, int start) } } - MC_SET_RAW_MEM; - xbt_dict_reset(first_enabled_state); - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process)){ + MC_SET_MC_HEAP; + + if(mc_reduce_kind == e_mc_reduce_dpor){ + xbt_dict_reset(first_enabled_state); + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process)){ char *key = bprintf("%lu", process->pid); char *data = bprintf("%d", count); xbt_dict_set(first_enabled_state, key, data, NULL); xbt_free(key); + } } } - if(_sg_mc_comms_determinism || _sg_mc_send_determinism) + + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ xbt_dynar_reset(communications_pattern); - MC_UNSET_RAW_MEM; + xbt_dynar_reset(incomplete_communications_pattern); + } + + MC_SET_STD_HEAP; /* Traverse the stack from the state at position start and re-execute the transitions */ @@ -1111,11 +1145,13 @@ void MC_replay(xbt_fifo_t stack, int start) state = (mc_state_t) xbt_fifo_get_item_content(item); saved_req = MC_state_get_executed_request(state, &value); - MC_SET_RAW_MEM; - char *key = bprintf("%lu", saved_req->issuer->pid); - xbt_dict_remove(first_enabled_state, key); - xbt_free(key); - MC_UNSET_RAW_MEM; + if(mc_reduce_kind == e_mc_reduce_dpor){ + MC_SET_MC_HEAP; + char *key = bprintf("%lu", saved_req->issuer->pid); + xbt_dict_remove(first_enabled_state, key); + xbt_free(key); + MC_SET_STD_HEAP; + } if(saved_req){ /* because we got a copy of the executed request, we have to fetch the @@ -1128,43 +1164,61 @@ void MC_replay(xbt_fifo_t stack, int start) XBT_DEBUG("Replay: %s (%p)", req_str, state); xbt_free(req_str); } - } - if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ - if(req->call == SIMCALL_COMM_ISEND) - comm_pattern = 1; - else if(req->call == SIMCALL_COMM_IRECV) - comm_pattern = 2; - } + /* TODO : handle test and testany simcalls */ + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ + if(req->call == SIMCALL_COMM_ISEND) + comm_pattern = 1; + else if(req->call == SIMCALL_COMM_IRECV) + comm_pattern = 2; + else if(req->call == SIMCALL_COMM_WAIT) + comm_pattern = 3; + else if(req->call == SIMCALL_COMM_WAITANY) + comm_pattern = 4; + } - SIMIX_simcall_pre(req, value); + SIMIX_simcall_pre(req, value); - if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ - MC_SET_RAW_MEM; - if(comm_pattern != 0){ - get_comm_pattern(communications_pattern, req, comm_pattern); + if(_sg_mc_comms_determinism || _sg_mc_send_determinism){ + MC_SET_MC_HEAP; + if(comm_pattern == 1 || comm_pattern == 2){ + get_comm_pattern(communications_pattern, req, comm_pattern); + }else if (comm_pattern == 3/* || comm_pattern == 4*/){ + current_comm = simcall_comm_wait__get__comm(req); + if(current_comm->comm.refcount == 1){ /* First wait only must be considered */ + complete_comm_pattern(communications_pattern, current_comm); + } + }else if (comm_pattern == 4/* || comm_pattern == 4*/){ + current_comm = xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_action_t); + if(current_comm->comm.refcount == 1){ /* First wait only must be considered */ + complete_comm_pattern(communications_pattern, current_comm); + } + } + MC_SET_STD_HEAP; + comm_pattern = 0; } - MC_UNSET_RAW_MEM; - comm_pattern = 0; - } - MC_wait_for_requests(); - - count++; - - MC_SET_RAW_MEM; - /* Insert in dict all enabled processes */ - xbt_swag_foreach(process, simix_global->process_list){ - if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){ - char *key = bprintf("%lu", process->pid); - if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){ - char *data = bprintf("%d", count); - xbt_dict_set(first_enabled_state, key, data, NULL); + + MC_wait_for_requests(); + + count++; + + if(mc_reduce_kind == e_mc_reduce_dpor){ + MC_SET_MC_HEAP; + /* Insert in dict all enabled processes */ + xbt_swag_foreach(process, simix_global->process_list){ + if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){ + char *key = bprintf("%lu", process->pid); + if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){ + char *data = bprintf("%d", count); + xbt_dict_set(first_enabled_state, key, data, NULL); + } + xbt_free(key); + } } - xbt_free(key); + MC_SET_STD_HEAP; } } - MC_UNSET_RAW_MEM; /* Update statistics */ mc_stats->visited_states++; @@ -1175,9 +1229,9 @@ void MC_replay(xbt_fifo_t stack, int start) XBT_DEBUG("**** End Replay ****"); if(raw_mem) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; else - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } @@ -1185,7 +1239,7 @@ void MC_replay(xbt_fifo_t stack, int start) void MC_replay_liveness(xbt_fifo_t stack, int all_stack) { - initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == mc_heap); int value; char *req_str; @@ -1203,7 +1257,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) /* At the moment of taking the snapshot the raw heap was set, so restoring * it will set it back again, we have to unset it to continue */ if(!initial_state_liveness->raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(all_stack){ @@ -1292,9 +1346,9 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) XBT_DEBUG("**** End Replay ****"); if(initial_state_liveness->raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; else - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } @@ -1306,7 +1360,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack) void MC_dump_stack_safety(xbt_fifo_t stack) { - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); MC_show_stack_safety(stack); @@ -1314,17 +1368,17 @@ void MC_dump_stack_safety(xbt_fifo_t stack) mc_state_t state; - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL) MC_state_delete(state); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; else - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } @@ -1332,9 +1386,9 @@ void MC_dump_stack_safety(xbt_fifo_t stack) void MC_show_stack_safety(xbt_fifo_t stack) { - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; int value; mc_state_t state; @@ -1354,7 +1408,7 @@ void MC_show_stack_safety(xbt_fifo_t stack) } if(!raw_mem_set) - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_show_deadlock(smx_simcall_t req) @@ -1398,17 +1452,17 @@ void MC_show_stack_liveness(xbt_fifo_t stack){ void MC_dump_stack_liveness(xbt_fifo_t stack){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); mc_pair_t pair; - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL) MC_pair_delete(pair); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; } @@ -1423,7 +1477,7 @@ void MC_print_statistics(mc_stats_t stats) XBT_INFO("Visited pairs = %lu", stats->visited_pairs); } XBT_INFO("Executed transitions = %lu", stats->executed_transitions); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){ fprintf(dot_output, "}\n"); fclose(dot_output); @@ -1434,7 +1488,7 @@ void MC_print_statistics(mc_stats_t stats) if (_sg_mc_send_determinism) XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes"); } - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; } void MC_assert(int prop) @@ -1473,37 +1527,37 @@ double MC_process_clock_get(smx_process_t process) void MC_automaton_load(const char *file){ - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); xbt_automaton_load(_mc_property_automaton,file); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; } void MC_automaton_new_propositional_symbol(const char* id, void* fct) { - int raw_mem_set = (mmalloc_get_current_heap() == raw_heap); + int raw_mem_set = (mmalloc_get_current_heap() == mc_heap); - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; if (_mc_property_automaton == NULL) _mc_property_automaton = xbt_automaton_new(); xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct); - MC_UNSET_RAW_MEM; + MC_SET_STD_HEAP; if(raw_mem_set) - MC_SET_RAW_MEM; + MC_SET_MC_HEAP; }