From 31f6ec7370f6689eed6b87f882dc578c9682b2e8 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 8 Mar 2016 13:10:41 +0100 Subject: [PATCH 1/1] [mc] Use C++ ctor/new/delete for VisitedPair --- src/mc/mc_liveness.cpp | 11 +++++---- src/mc/mc_liveness.h | 26 ++++++++++---------- src/mc/mc_visited.cpp | 54 ++++++++++++++++++++---------------------- 3 files changed, 46 insertions(+), 45 deletions(-) diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp index 1cb632c6e1..b45c70c3ae 100644 --- a/src/mc/mc_liveness.cpp +++ b/src/mc/mc_liveness.cpp @@ -66,8 +66,9 @@ static simgrid::xbt::unique_ptr get_atomic_propositions_values() static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* pair) { - simgrid::mc::VisitedPair* new_pair = nullptr; - new_pair = simgrid::mc::visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions.get(), pair->graph_state); + simgrid::mc::VisitedPair* new_pair = new VisitedPair( + pair->num, pair->automaton_state, pair->atomic_propositions.get(), + pair->graph_state); new_pair->acceptance_pair = 1; if (xbt_dynar_is_empty(acceptance_pairs)) @@ -88,7 +89,9 @@ static simgrid::mc::VisitedPair* is_reached_acceptance_pair(simgrid::mc::Pair* p while (cursor <= max) { pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(acceptance_pairs, cursor, simgrid::mc::VisitedPair*); if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) == 0) { - if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_pair->atomic_propositions) == 0) { + if (xbt_automaton_propositional_symbols_compare_value( + pair_test->atomic_propositions.get(), + new_pair->atomic_propositions.get()) == 0) { if (snapshot_compare(pair_test, new_pair) == 0) { XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); xbt_fifo_shift(mc_stack); @@ -133,7 +136,7 @@ static void remove_acceptance_pair(int pair_num) pair_test->acceptance_removed = 1; if (_sg_mc_visited == 0 || pair_test->visited_removed == 1) - simgrid::mc::visited_pair_delete(pair_test); + delete pair_test; } } diff --git a/src/mc/mc_liveness.h b/src/mc/mc_liveness.h index ececec48af..b8fbd019f0 100644 --- a/src/mc/mc_liveness.h +++ b/src/mc/mc_liveness.h @@ -45,20 +45,20 @@ struct XBT_PRIVATE Pair { }; struct XBT_PRIVATE VisitedPair { - int num; - int other_num; /* Dot output for */ - int acceptance_pair; - mc_state_t graph_state; /* System state included */ - xbt_automaton_state_t automaton_state; - xbt_dynar_t atomic_propositions; - size_t heap_bytes_used; - int nb_processes; - int acceptance_removed; - int visited_removed; -}; + int num = 0; + int other_num = 0; /* Dot output for */ + int acceptance_pair = 0; + mc_state_t graph_state = nullptr; /* System state included */ + xbt_automaton_state_t automaton_state = nullptr; + simgrid::xbt::unique_ptr atomic_propositions; + size_t heap_bytes_used = 0; + int nb_processes = 0; + int acceptance_removed = 0; + int visited_removed = 0; -XBT_PRIVATE simgrid::mc::VisitedPair* visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state); -XBT_PRIVATE void visited_pair_delete(simgrid::mc::VisitedPair* p); + VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state); + ~VisitedPair(); +}; int modelcheck_liveness(void); XBT_PRIVATE void show_stack_liveness(xbt_fifo_t stack); diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp index 95bb48c382..80525901c7 100644 --- a/src/mc/mc_visited.cpp +++ b/src/mc/mc_visited.cpp @@ -88,34 +88,34 @@ static mc_visited_state_t visited_state_new() namespace simgrid { namespace mc { -simgrid::mc::VisitedPair* visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state) +VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state) { simgrid::mc::Process* process = &(mc_model_checker->process()); - simgrid::mc::VisitedPair* pair = nullptr; - pair = xbt_new0(simgrid::mc::VisitedPair, 1); - pair->graph_state = graph_state; - if(pair->graph_state->system_state == nullptr) - pair->graph_state->system_state = simgrid::mc::take_snapshot(pair_num); - pair->heap_bytes_used = mmalloc_get_bytes_used_remote( + + this->graph_state = graph_state; + if(this->graph_state->system_state == nullptr) + this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num); + this->heap_bytes_used = mmalloc_get_bytes_used_remote( process->get_heap()->heaplimit, process->get_malloc_info()); MC_process_smx_refresh(&mc_model_checker->process()); - pair->nb_processes = + this->nb_processes = mc_model_checker->process().smx_process_infos.size(); - pair->automaton_state = automaton_state; - pair->num = pair_num; - pair->other_num = -1; - pair->acceptance_removed = 0; - pair->visited_removed = 0; - pair->acceptance_pair = 0; - pair->atomic_propositions = xbt_dynar_new(sizeof(int), nullptr); + this->automaton_state = automaton_state; + this->num = pair_num; + this->other_num = -1; + this->acceptance_removed = 0; + this->visited_removed = 0; + this->acceptance_pair = 0; + this->atomic_propositions = simgrid::xbt::unique_ptr( + xbt_dynar_new(sizeof(int), nullptr)); + unsigned int cursor = 0; int value; xbt_dynar_foreach(atomic_propositions, cursor, value) - xbt_dynar_push_as(pair->atomic_propositions, int, value); - return pair; + xbt_dynar_push_as(this->atomic_propositions.get(), int, value); } static int is_exploration_stack_pair(simgrid::mc::VisitedPair* pair){ @@ -130,14 +130,10 @@ static int is_exploration_stack_pair(simgrid::mc::VisitedPair* pair){ return 0; } -void visited_pair_delete(simgrid::mc::VisitedPair* p) +VisitedPair::~VisitedPair() { - p->automaton_state = nullptr; - if( !is_exploration_stack_pair(p)) - MC_state_delete(p->graph_state, 1); - xbt_dynar_free(&(p->atomic_propositions)); - xbt_free(p); - p = nullptr; + if( !is_exploration_stack_pair(this)) + MC_state_delete(this->graph_state, 1); } } @@ -380,7 +376,7 @@ int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* p simgrid::mc::VisitedPair* new_visited_pair = nullptr; if (visited_pair == nullptr) - new_visited_pair = simgrid::mc::visited_pair_new( + new_visited_pair = new simgrid::mc::VisitedPair( pair->num, pair->automaton_state, pair->atomic_propositions.get(), pair->graph_state); else @@ -403,7 +399,9 @@ int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* p while (cursor <= max) { pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*); if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) { - if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) { + if (xbt_automaton_propositional_symbols_compare_value( + pair_test->atomic_propositions.get(), + new_visited_pair->atomic_propositions.get()) == 0) { if (snapshot_compare(pair_test, new_visited_pair) == 0) { if (pair_test->other_num == -1) new_visited_pair->other_num = pair_test->num; @@ -418,7 +416,7 @@ int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* p pair_test->visited_removed = 1; if (!pair_test->acceptance_pair || pair_test->acceptance_removed == 1) - simgrid::mc::visited_pair_delete(pair_test); + delete pair_test; return new_visited_pair->other_num; } } @@ -450,7 +448,7 @@ int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* p xbt_dynar_remove_at(visited_pairs, index2, &pair_test); pair_test->visited_removed = 1; if (!pair_test->acceptance_pair || pair_test->acceptance_removed) - simgrid::mc::visited_pair_delete(pair_test); + delete pair_test; } return -1; } -- 2.20.1