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);
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);
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()
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 */
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);
for(i=0; i < snapshot->num_reg; i++)
MC_region_destroy(snapshot->regions[i]);
+ xbt_dynar_free(&(snapshot->stacks));
xbt_free(snapshot);
}
}
}
+
+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);
+}
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){
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;
/* 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;
/* 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;
/* 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;
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);
cursor++;
}
+ xbt_dynar_free(&stacks1);
+ xbt_dynar_free(&stacks2);
+ xbt_dynar_free(&equals);
return 0;
}
}
}
}
+ xbt_dynar_free(&s_tokens1);
+ xbt_dynar_free(&s_tokens2);
cursor++;
}
+ xbt_dynar_free(&tokens1);
+ xbt_dynar_free(&tokens2);
return diff;
}
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)
/********************* 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);
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);
}
}
- 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 */
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;
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 **** */
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;
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;
}
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;
}
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 <nbr; i++){
- xbt_dynar_get_cpy(a->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;
}
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;
+ }
+}