From b72e8264dccedfa1c53042e99f94d3a8e5387316 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 18 Oct 2012 10:51:58 +0200 Subject: [PATCH] model-checker : fix some memory leaks --- include/xbt/automaton.h | 18 ++-- src/include/mc/datatypes.h | 3 + src/mc/mc_checkpoint.c | 15 +++ src/mc/mc_compare.c | 67 +++++++++++++- src/mc/mc_global.c | 2 +- src/mc/mc_liveness.c | 23 ++++- src/mc/mc_private.h | 7 +- src/xbt/automaton/automaton.c | 170 +++++++++++++++++----------------- 8 files changed, 205 insertions(+), 100 deletions(-) diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h index 49df4630c0..9f577477f2 100644 --- a/include/xbt/automaton.h +++ b/include/xbt/automaton.h @@ -60,6 +60,7 @@ typedef struct xbt_propositional_symbol* xbt_propositional_symbol_t; XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new(void); + XBT_PUBLIC(void) xbt_automaton_load(xbt_automaton_t automaton, const char *file); XBT_PUBLIC(xbt_state_t) xbt_automaton_new_state(xbt_automaton_t a, int type, char* id); @@ -74,12 +75,6 @@ XBT_PUBLIC(xbt_dynar_t) xbt_automaton_get_transitions(xbt_automaton_t a); XBT_PUBLIC(xbt_transition_t) xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst); -XBT_PUBLIC(void) xbt_automaton_free_automaton(xbt_automaton_t a, void_f_pvoid_t transition_free_function); - -XBT_PUBLIC(void) xbt_automaton_free_state(xbt_automaton_t a, xbt_state_t s, void_f_pvoid_t transition_free_function); - -XBT_PUBLIC(void) xbt_automaton_free_transition(xbt_automaton_t a, xbt_transition_t t, void_f_pvoid_t transition_free_function); - XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_source(xbt_transition_t t); XBT_PUBLIC(xbt_state_t) xbt_automaton_transition_get_destination(xbt_transition_t t); @@ -110,6 +105,17 @@ XBT_PUBLIC(int) automaton_transition_compare(const void *t1, const void *t2); XBT_PUBLIC(int) automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2); +XBT_PUBLIC(void) xbt_state_free_voidp(void *s); + +XBT_PUBLIC(void) xbt_state_free(xbt_state_t s); + +XBT_PUBLIC(void) xbt_transition_free_voidp(void *t); + +XBT_PUBLIC(void) xbt_exp_label_free_voidp(void *e); + +XBT_PUBLIC(void) xbt_propositional_symbol_free_voidp(void *ps); + +XBT_PUBLIC(void) xbt_automaton_free(xbt_automaton_t a); SG_END_DECL() diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h index a31625a9f8..61cef5d85c 100644 --- a/src/include/mc/datatypes.h +++ b/src/include/mc/datatypes.h @@ -37,5 +37,8 @@ typedef struct s_heap_equality{ void *address2; }s_heap_equality_t, *heap_equality_t; +void heap_equality_free_voidp(void *e); +void stack_region_free_voidp(void *s); + SG_END_DECL() #endif /* _MC_MC_H */ diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c index 8a5861c566..5384c3893f 100644 --- a/src/mc/mc_checkpoint.c +++ b/src/mc/mc_checkpoint.c @@ -34,6 +34,8 @@ static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap) static void print_local_variables_values(xbt_dynar_t all_variables); static void *get_stack_pointer(void *stack_context, void *heap); +static void snapshot_stack_free(mc_snapshot_stack_t s); + static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size) { mc_mem_region_t new_reg = xbt_new0(s_mc_mem_region_t, 1); @@ -191,6 +193,7 @@ void MC_free_snapshot(mc_snapshot_t snapshot) for(i=0; i < snapshot->num_reg; i++) MC_region_destroy(snapshot->regions[i]); + xbt_dynar_free(&(snapshot->stacks)); xbt_free(snapshot); } @@ -545,3 +548,15 @@ static void print_local_variables_values(xbt_dynar_t all_variables){ } } + +static void snapshot_stack_free(mc_snapshot_stack_t s){ + if(s){ + xbt_free(s->local_variables->data); + xbt_free(s->local_variables); + xbt_free(s); + } +} + +void snapshot_stack_free_voidp(void *s){ + snapshot_stack_free((mc_snapshot_stack_t) * (void **) s); +} diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c index 503d498941..1510ccaff8 100644 --- a/src/mc/mc_compare.c +++ b/src/mc/mc_compare.c @@ -18,6 +18,9 @@ static int compare_stack(stack_region_t s1, stack_region_t s2, void *sp1, void * static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2); static size_t ignore(void *address); +static void stack_region_free(stack_region_t s); +static void heap_equality_free(heap_equality_t e); + static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals); static size_t ignore(void *address){ @@ -114,12 +117,33 @@ static int heap_region_compare(void *d1, void *d2, size_t size){ return distance; } +static void stack_region_free(stack_region_t s){ + if(s){ + xbt_free(s->process_name); + xbt_free(s); + } +} + +void stack_region_free_voidp(void *s){ + stack_region_free((stack_region_t) * (void **) s); +} + +static void heap_equality_free(heap_equality_t e){ + if(e){ + xbt_free(e); + } +} + +void heap_equality_free_voidp(void *e){ + heap_equality_free((heap_equality_t) * (void **) e); +} + int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ int errors = 0, i; - xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), NULL); - xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), NULL); - xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), NULL); + xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp); + xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp); + xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), heap_equality_free_voidp); void *heap1 = NULL, *heap2 = NULL; @@ -140,14 +164,23 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ /* Compare heapregion */ if(s1->regions[i]->size != s2->regions[i]->size){ XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + xbt_dynar_free(&stacks1); + xbt_dynar_free(&stacks2); + xbt_dynar_free(&equals); return 1; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + xbt_dynar_free(&stacks1); + xbt_dynar_free(&stacks2); + xbt_dynar_free(&equals); return 1; } if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[i]->data, (xbt_mheap_t)s2->regions[i]->data, &stacks1, &stacks2, &equals)){ XBT_INFO("Different heap (mmalloc_compare)"); + xbt_dynar_free(&stacks1); + xbt_dynar_free(&stacks2); + xbt_dynar_free(&equals); return 1; } heap1 = s1->regions[i]->data; @@ -157,14 +190,23 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ /* Compare data libsimgrid region */ if(s1->regions[i]->size != s2->regions[i]->size){ XBT_INFO("Different size of libsimgrid (data) (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + xbt_dynar_free(&stacks1); + xbt_dynar_free(&stacks2); + xbt_dynar_free(&equals); return 1; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ XBT_INFO("Different start addr of libsimgrid (data) (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + xbt_dynar_free(&stacks1); + xbt_dynar_free(&stacks2); + xbt_dynar_free(&equals); return 1; } if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ XBT_INFO("Different memcmp for data in libsimgrid"); + xbt_dynar_free(&stacks1); + xbt_dynar_free(&stacks2); + xbt_dynar_free(&equals); return 1; } break; @@ -173,14 +215,23 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ /* Compare data program region */ if(s1->regions[i]->size != s2->regions[i]->size){ XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + xbt_dynar_free(&stacks1); + xbt_dynar_free(&stacks2); + xbt_dynar_free(&equals); return 1; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + xbt_dynar_free(&stacks1); + xbt_dynar_free(&stacks2); + xbt_dynar_free(&equals); return 1; } if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ XBT_INFO("Different memcmp for data in program"); + xbt_dynar_free(&stacks1); + xbt_dynar_free(&stacks2); + xbt_dynar_free(&equals); return 1; } break; @@ -207,6 +258,9 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ diff_local = compare_local_variables(((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, equals); if(diff_local > 0){ XBT_INFO("Hamming distance between stacks : %d", diff); + xbt_dynar_free(&stacks1); + xbt_dynar_free(&stacks2); + xbt_dynar_free(&equals); return 1; }else{ XBT_INFO("Local variables are equals in stack %d", cursor + 1); @@ -217,6 +271,9 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){ cursor++; } + xbt_dynar_free(&stacks1); + xbt_dynar_free(&stacks2); + xbt_dynar_free(&equals); return 0; } @@ -245,9 +302,13 @@ static int compare_local_variables(char *s1, char *s2, xbt_dynar_t heap_equals){ } } } + xbt_dynar_free(&s_tokens1); + xbt_dynar_free(&s_tokens2); cursor++; } + xbt_dynar_free(&tokens1); + xbt_dynar_free(&tokens2); return diff; } diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 2efb2d09e2..ce251a370c 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -550,7 +550,7 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){ MC_SET_RAW_MEM; while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL) - MC_pair_stateless_delete(pair); + pair_stateless_free(pair); MC_UNSET_RAW_MEM; if(raw_mem_set) diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index d11136815a..f04ea984fc 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -217,12 +217,14 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){ /********************* Double-DFS stateless *******************/ -void MC_pair_stateless_delete(mc_pair_stateless_t pair){ - xbt_free(pair->graph_state->proc_status); - xbt_free(pair->graph_state); +void pair_stateless_free(mc_pair_stateless_t pair){ xbt_free(pair); } +void pair_stateless_free_voidp(void *p){ + pair_stateless_free((mc_pair_stateless_t) * (void **) p); +} + mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){ mc_pair_stateless_t p = NULL; p = xbt_new0(s_mc_pair_stateless_t, 1); @@ -233,6 +235,19 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){ return p; } +void pair_reached_free(mc_pair_reached_t pair){ + if(pair){ + pair->automaton_state = NULL; + xbt_dynar_free(&(pair->prop_ato)); + MC_free_snapshot(pair->system_state); + xbt_free(pair); + } +} + +void pair_reached_free_voidp(void *p){ + pair_reached_free((mc_pair_reached_t) * (void **) p); +} + void MC_ddfs_init(void){ raw_mem_set = (mmalloc_get_current_heap() == raw_heap); @@ -257,7 +272,7 @@ void MC_ddfs_init(void){ } } - reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); + reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp); successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL); /* Save the initial state */ diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index af91f56019..9c0f06516c 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -46,7 +46,7 @@ void MC_take_snapshot(mc_snapshot_t); void MC_take_snapshot_liveness(mc_snapshot_t s); void MC_restore_snapshot(mc_snapshot_t); void MC_free_snapshot(mc_snapshot_t); - +void snapshot_stack_free_voidp(void *s); /********************************* MC Global **********************************/ extern double *mc_time; @@ -243,6 +243,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2); void MC_pair_delete(mc_pair_t pair); void MC_exit_liveness(void); mc_state_t MC_state_pair_new(void); +void pair_reached_free(mc_pair_reached_t pair); +void pair_reached_free_voidp(void *p); /* **** Double-DFS stateless **** */ @@ -257,7 +259,8 @@ void MC_ddfs_init(void); void MC_ddfs(int search_cycle); void MC_show_stack_liveness(xbt_fifo_t stack); void MC_dump_stack_liveness(xbt_fifo_t stack); -void MC_pair_stateless_delete(mc_pair_stateless_t pair); +void pair_stateless_free(mc_pair_stateless_t pair); +void pair_stateless_free_voidp(void *p); /********************************** Configuration of MC **************************************/ extern xbt_fifo_t mc_stack_safety; diff --git a/src/xbt/automaton/automaton.c b/src/xbt/automaton/automaton.c index 97c397cfc1..6cfff43af6 100644 --- a/src/xbt/automaton/automaton.c +++ b/src/xbt/automaton/automaton.c @@ -11,9 +11,9 @@ xbt_automaton_t xbt_automaton_new(){ xbt_automaton_t automaton = NULL; automaton = xbt_new0(struct xbt_automaton, 1); - automaton->states = xbt_dynar_new(sizeof(xbt_state_t), NULL); - automaton->transitions = xbt_dynar_new(sizeof(xbt_transition_t), NULL); - automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_propositional_symbol_t), NULL); + automaton->states = xbt_dynar_new(sizeof(xbt_state_t), xbt_state_free_voidp); + automaton->transitions = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp); + automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_propositional_symbol_t), xbt_propositional_symbol_free_voidp); return automaton; } @@ -22,8 +22,8 @@ xbt_state_t xbt_automaton_new_state(xbt_automaton_t a, int type, char* id){ state = xbt_new0(struct xbt_state, 1); state->type = type; state->id = strdup(id); - state->in = xbt_dynar_new(sizeof(xbt_transition_t), NULL); - state->out = xbt_dynar_new(sizeof(xbt_transition_t), NULL); + state->in = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp); + state->out = xbt_dynar_new(sizeof(xbt_transition_t), xbt_transition_free_voidp); xbt_dynar_push(a->states, &state); return state; } @@ -100,85 +100,6 @@ xbt_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src return NULL; } -void xbt_automaton_free_automaton(xbt_automaton_t a, void_f_pvoid_t transition_free_function){ - unsigned int cursor = 0; - xbt_state_t state = NULL; - xbt_transition_t transition = NULL; - - xbt_dynar_foreach(a->states, cursor, state){ - xbt_dynar_free(&(state->out)); - xbt_dynar_free(&(state->in)); - } - - xbt_dynar_foreach(a->transitions, cursor, transition){ - if(transition_free_function) - (*transition_free_function) (transition->label); - } - - xbt_dynar_foreach(a->states, cursor, state) - free(state); - xbt_dynar_free(&(a->states)); - - xbt_dynar_foreach(a->transitions, cursor, state) - free(transition); - xbt_dynar_free(&(a->transitions)); - - free(a); - - return; -} - -void xbt_automaton_free_state(xbt_automaton_t a, xbt_state_t s, void_f_pvoid_t transition_free_function){ - unsigned long nbr; - unsigned long i; - unsigned int cursor = 0; - xbt_state_t state = NULL; - xbt_transition_t transition = NULL; - - nbr = xbt_dynar_length(a->transitions); - for(i = 0; i transitions, cursor, &transition); - if((transition->src == s) || (transition->dst == s)){ - xbt_automaton_free_transition(a, transition, transition_free_function); - }else{ - cursor++; - } - } - - cursor = 0; - xbt_dynar_foreach(a->states, cursor, state) - if(state == s) - xbt_dynar_cursor_rm(a->states, &cursor); - - xbt_dynar_free(&(s->in)); - xbt_dynar_free(&(s->out)); - - free(s); - - return; -} - -void xbt_automaton_free_transition(xbt_automaton_t a, xbt_transition_t t, void_f_pvoid_t transition_free_function){ - int index; - unsigned int cursor = 0; - xbt_transition_t transition = NULL; - - if((transition_free_function) && (t->label)) - (*transition_free_function) (t->label); - - xbt_dynar_foreach(a->transitions, cursor, transition) { - if(transition == t){ - index = __xbt_find_in_dynar(transition->dst->in, transition); - xbt_dynar_remove_at(transition->dst->in, index, NULL); - index = __xbt_find_in_dynar(transition->src->out, transition); - xbt_dynar_remove_at(transition->src->out, index, NULL); - xbt_dynar_cursor_rm(a->transitions, & cursor); - free(transition); - break; - } - } -} - xbt_state_t xbt_automaton_transition_get_source(xbt_transition_t t){ return t->src; } @@ -364,3 +285,84 @@ int propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){ return 0; } + +/************ Free functions ****************/ + +static void xbt_transition_free(xbt_transition_t t); +static void xbt_exp_label_free(xbt_exp_label_t e); +static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps); + +void xbt_state_free(xbt_state_t s){ + if(s){ + xbt_free(s->id); + xbt_dynar_free(&(s->in)); + xbt_dynar_free(&(s->out)); + xbt_free(s); + s = NULL; + } +} + +void xbt_state_free_voidp(void *s){ + xbt_state_free((xbt_state_t) * (void **) s); +} + +static void xbt_transition_free(xbt_transition_t t){ + if(t){ + xbt_exp_label_free(t->label); + xbt_free(t); + t = NULL; + } +} + +void xbt_transition_free_voidp(void *t){ + xbt_transition_free((xbt_transition_t) * (void **) t); +} + +static void xbt_exp_label_free(xbt_exp_label_t e){ + if(e){ + switch(e->type){ + case 0: + case 1: + xbt_exp_label_free(e->u.or_and.left_exp); + xbt_exp_label_free(e->u.or_and.right_exp); + break; + case 2: + xbt_exp_label_free(e->u.exp_not); + break; + case 3: + xbt_free(e->u.predicat); + break; + default: + break; + } + xbt_free(e); + e = NULL; + } +} + +void xbt_exp_label_free_voidp(void *e){ + xbt_exp_label_free((xbt_exp_label_t) * (void **) e); +} + +static void xbt_propositional_symbol_free(xbt_propositional_symbol_t ps){ + if(ps){ + xbt_free(ps->pred); + xbt_free(ps); + ps = NULL; + } +} + +void xbt_propositional_symbol_free_voidp(void *ps){ + xbt_propositional_symbol_free((xbt_propositional_symbol_t) * (void **) ps); +} + +void xbt_automaton_free(xbt_automaton_t a){ + if(a){ + xbt_dynar_free(&(a->propositional_symbols)); + xbt_dynar_free(&(a->transitions)); + xbt_dynar_free(&(a->states)); + xbt_state_free(a->current_state); + xbt_free(a); + a = NULL; + } +} -- 2.20.1