From c47736071b39439589e5262e612bb86d50db6cb2 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Tue, 29 May 2012 15:19:16 +0200 Subject: [PATCH] model-checker : replace all XBT_DEBUG by XBT_INFO --- src/mc/mc_liveness.c | 199 +++++++++++++++++-------------------------- 1 file changed, 79 insertions(+), 120 deletions(-) diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index cd16a82d57..9ea615fa67 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -128,7 +128,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, void* s_heap, void* r_h if(s1->num_reg != s2->num_reg){ - XBT_DEBUG("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg); + XBT_INFO("Different num_reg (s1 = %u, s2 = %u)", s1->num_reg, s2->num_reg); return 1; } @@ -138,91 +138,51 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, void* s_heap, void* r_h for(i=0 ; i< s1->num_reg ; i++){ if(s1->regions[i]->type != s2->regions[i]->type){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different type of region"); + XBT_INFO("Different type of region"); errors++; - }else{ - return 1; - } } switch(s1->regions[i]->type){ case 0: if(s1->regions[i]->size != s2->regions[i]->size){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - }else{ - return 1; - } + XBT_INFO("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - }else{ - return 1; - } + XBT_INFO("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; } if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data, s_heap, r_heap)){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different heap (mmalloc_compare)"); - errors++; - }else{ - return 1; - } + XBT_INFO("Different heap (mmalloc_compare)"); + errors++; } break; case 1 : if(s1->regions[i]->size != s2->regions[i]->size){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - }else{ - return 1; - } + XBT_INFO("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - }else{ - return 1; - } + XBT_INFO("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; } if(data_libsimgrid_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different memcmp for data in libsimgrid"); - errors++; - }else{ - return 1; - } + XBT_INFO("Different memcmp for data in libsimgrid"); + errors++; } break; case 2 : if(s1->regions[i]->size != s2->regions[i]->size){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); - errors++; - }else{ - return 1; - } + XBT_INFO("Different size of data program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size); + errors++; } if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); - errors++; - }else{ - return 1; - } + XBT_INFO("Different start addr of data program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr); + errors++; } if(data_program_region_compare(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - XBT_DEBUG("Different memcmp for data in program"); - errors++; - }else{ - return 1; - } + XBT_INFO("Different memcmp for data in program"); + errors++; } break; default: @@ -267,10 +227,10 @@ int reached(xbt_state_t st){ //xbt_dict_t current_rdv_points = SIMIX_get_rdv_points(); xbt_dynar_foreach(reached_pairs, cursor, pair_test){ - XBT_DEBUG("Pair reached #%u", cursor+1); + XBT_INFO("Pair reached #%u", cursor+1); if(automaton_state_compare(pair_test->automaton_state, st) == 0){ if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){ - //XBT_DEBUG("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points)); + //XBT_INFO("Rdv points size %d - %d", xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points)); //if(xbt_dict_length(pair_test->rdv_points) == xbt_dict_length(current_rdv_points)){ //if(rdv_points_compare(pair_test->rdv_points, current_rdv_points) == 0){ if(snapshot_compare(pair_test->system_state, sn, std_heap, raw_heap) == 0){ @@ -282,13 +242,13 @@ int reached(xbt_state_t st){ } /* } }else{ - XBT_DEBUG("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) ); + XBT_INFO("Different size of rdv points (%d - %d)",xbt_dict_length(pair_test->rdv_points), xbt_dict_length(current_rdv_points) ); }*/ }else{ - XBT_DEBUG("Different values of propositional symbols"); + XBT_INFO("Different values of propositional symbols"); } }else{ - XBT_DEBUG("Different automaton state"); + XBT_INFO("Different automaton state"); } } @@ -318,15 +278,15 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu rdv1 = (smx_rdv_t)data; rdv2 = xbt_dict_get_or_null(d2, rdv1->name); if(rdv2 == NULL){ - XBT_DEBUG("Rdv point unknown"); + XBT_INFO("Rdv point unknown"); return 1; }else{ if(xbt_fifo_size(rdv1->comm_fifo) != xbt_fifo_size(rdv2->comm_fifo)){ - XBT_DEBUG("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) ); + XBT_INFO("Different total of actions in mailbox \"%s\" (%d - %d)", rdv1->name, xbt_fifo_size(rdv1->comm_fifo),xbt_fifo_size(rdv2->comm_fifo) ); return 1; }else{ - XBT_DEBUG("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo)); + XBT_INFO("Total of actions in mailbox \"%s\" : %d", rdv1->name, xbt_fifo_size(rdv1->comm_fifo)); item1 = xbt_fifo_get_first_item(rdv1->comm_fifo); item2 = xbt_fifo_get_first_item(rdv2->comm_fifo); @@ -336,17 +296,17 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu action2 = (smx_action_t) xbt_fifo_get_item_content(item2); if(action1->type != action2->type){ - XBT_DEBUG("Different type of action"); + XBT_INFO("Different type of action"); return 1; } if(action1->state != action2->state){ - XBT_DEBUG("Different state of action"); + XBT_INFO("Different state of action"); return 1; } if(xbt_fifo_size(action1->simcalls) != xbt_fifo_size(action2->simcalls)){ - XBT_DEBUG("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls)); + XBT_INFO("Different size of simcall list (%d - %d", xbt_fifo_size(action1->simcalls), xbt_fifo_size(action2->simcalls)); return 1; }else{ @@ -359,11 +319,11 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu req2 = (smx_simcall_t) xbt_fifo_get_item_content(item_req2); if(req1->call != req2->call){ - XBT_DEBUG("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call); + XBT_INFO("Different simcall call in simcalls of action (%d - %d)", (int)req1->call, (int)req2->call); return 1; } if(req1->issuer->pid != req2->issuer->pid){ - XBT_DEBUG("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid); + XBT_INFO("Different simcall issuer in simcalls of action (%lu- %lu)", req1->issuer->pid, req2->issuer->pid); return 1; } @@ -383,7 +343,7 @@ int rdv_points_compare(xbt_dict_t d1, xbt_dict_t d2){ /* d1 = pair_test, d2 = cu case 2: /* comm */ if(action1->comm.type != action2->comm.type) return 1; - //XBT_DEBUG("Type of comm : %d", action1->comm.type); + //XBT_INFO("Type of comm : %d", action1->comm.type); switch(action1->comm.type){ case 0: /* SEND */ @@ -503,9 +463,9 @@ void set_pair_reached(xbt_state_t st){ smx_action_t a = xbt_new0(s_smx_action_t, 1); memcpy(a, action, sizeof(s_smx_action_t)); xbt_fifo_push(new_rdv->comm_fifo, a); - XBT_DEBUG("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key); + XBT_INFO("New action (type = %d, state = %d) in mailbox \"%s\"", action->type, action->state, key); if(action->type==2) - XBT_DEBUG("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount); + XBT_INFO("Type of communication : %d, Ref count = %d", action->comm.type, action->comm.refcount); } //new_rdv->comm_fifo = xbt_fifo_copy(((smx_rdv_t)data)->comm_fifo); xbt_dict_set(pair->rdv_points, new_rdv->name, new_rdv, NULL); @@ -574,13 +534,13 @@ int reached_hash(xbt_state_t st){ MC_UNSET_RAW_MEM; return 1; }else{ - XBT_DEBUG("Different snapshot"); + XBT_INFO("Different snapshot"); } }else{ - XBT_DEBUG("Different values of propositional symbols"); + XBT_INFO("Different values of propositional symbols"); } }else{ - XBT_DEBUG("Different automaton state"); + XBT_INFO("Different automaton state"); } region_diff = 0; @@ -680,16 +640,16 @@ int visited(xbt_state_t st, int sc){ return 1; }else{ - XBT_DEBUG("Different snapshot"); + XBT_INFO("Different snapshot"); } }else{ - XBT_DEBUG("Different values of propositional symbols"); + XBT_INFO("Different values of propositional symbols"); } }else{ - XBT_DEBUG("Different automaton state"); + XBT_INFO("Different automaton state"); } }else{ - XBT_DEBUG("Different value of search_cycle"); + XBT_INFO("Different value of search_cycle"); } } @@ -760,16 +720,16 @@ int visited_hash(xbt_state_t st, int sc){ MC_UNSET_RAW_MEM; return 1; }else{ - //XBT_DEBUG("Different snapshot"); + //XBT_INFO("Different snapshot"); } }else{ - //XBT_DEBUG("Different values of propositional symbols"); + //XBT_INFO("Different values of propositional symbols"); } }else{ - //XBT_DEBUG("Different automaton state"); + //XBT_INFO("Different automaton state"); } }else{ - //XBT_DEBUG("Different value of search_cycle"); + //XBT_INFO("Different value of search_cycle"); } region_diff = 0; @@ -923,9 +883,9 @@ mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){ void MC_ddfs_init(void){ - XBT_DEBUG("**************************************************"); - XBT_DEBUG("Double-DFS init"); - XBT_DEBUG("**************************************************"); + XBT_INFO("**************************************************"); + XBT_INFO("Double-DFS init"); + XBT_INFO("**************************************************"); mc_pair_stateless_t mc_initial_pair = NULL; mc_state_t initial_graph_state = NULL; @@ -1014,8 +974,8 @@ void MC_ddfs(int search_cycle){ automaton->current_state = current_pair->automaton_state; - XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle); - XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id, MC_state_interleave_size(current_pair->graph_state)); + XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle); + XBT_INFO("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id, MC_state_interleave_size(current_pair->graph_state)); mc_stats_pair->visited_pairs++; @@ -1038,19 +998,18 @@ void MC_ddfs(int search_cycle){ //set_pair_visited(current_pair->automaton_state, search_cycle); set_pair_visited_hash(current_pair->automaton_state, search_cycle); - //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); - XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash)); + //XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs)); + XBT_INFO("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash)); if(current_pair->requests > 0){ while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){ /* Debug information */ - if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){ - req_str = MC_request_to_string(req, value); - XBT_DEBUG("Execute: %s", req_str); - xbt_free(req_str); - } + + req_str = MC_request_to_string(req, value); + XBT_INFO("Execute: %s", req_str); + xbt_free(req_str); MC_state_set_executed_request(current_pair->graph_state, req, value); @@ -1118,7 +1077,7 @@ void MC_ddfs(int search_cycle){ if(reached(pair_succ->automaton_state)){ //if(reached_hash(pair_succ->automaton_state)){ - XBT_DEBUG("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state)); + XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state)); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); @@ -1131,13 +1090,13 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); set_pair_reached(pair_succ->automaton_state); //set_pair_reached_hash(pair_succ->automaton_state); - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness, pair_succ); @@ -1160,7 +1119,7 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); } @@ -1170,15 +1129,15 @@ void MC_ddfs(int search_cycle){ if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){ - XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + XBT_INFO("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); set_pair_reached(pair_succ->automaton_state); //set_pair_reached_hash(pair_succ->automaton_state); search_cycle = 1; - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); } @@ -1193,7 +1152,7 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); } @@ -1208,7 +1167,7 @@ void MC_ddfs(int search_cycle){ } if(MC_state_interleave_size(current_pair->graph_state) > 0){ - XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness)); + XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness)); MC_replay_liveness(mc_stack_liveness, 0); } } @@ -1266,7 +1225,7 @@ void MC_ddfs(int search_cycle){ if(reached(pair_succ->automaton_state)){ //if(reached_hash(pair_succ->automaton_state)){ - XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1); + XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1); XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); XBT_INFO("| ACCEPTANCE CYCLE |"); @@ -1279,13 +1238,13 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); + XBT_INFO("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id); set_pair_reached(pair_succ->automaton_state); //set_pair_reached_hash(pair_succ->automaton_state); - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); MC_SET_RAW_MEM; xbt_fifo_unshift(mc_stack_liveness, pair_succ); @@ -1308,7 +1267,7 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); } } @@ -1323,8 +1282,8 @@ void MC_ddfs(int search_cycle){ search_cycle = 1; - XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); - //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); + XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs)); + //XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash)); } @@ -1339,7 +1298,7 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Next pair already visited ! "); + XBT_INFO("Next pair already visited ! "); } @@ -1356,14 +1315,14 @@ void MC_ddfs(int search_cycle){ }else{ - XBT_DEBUG("Max depth reached"); + XBT_INFO("Max depth reached"); } if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){ - XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) ); + XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) ); }else{ - XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) ); + XBT_INFO("Pair (graph=%p, automaton =%p, search_cycle = %d, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) ); } -- 2.20.1