From 1716090883038167211da78d54336cca61af6b85 Mon Sep 17 00:00:00 2001 From: Arnaud Giersch Date: Wed, 10 Jul 2019 17:54:40 +0200 Subject: [PATCH 1/1] MC/compare: cleanup++ --- src/mc/VisitedState.cpp | 9 +---- src/mc/checker/LivenessChecker.cpp | 23 ++++-------- src/mc/checker/LivenessChecker.hpp | 1 - src/mc/checker/SafetyChecker.cpp | 9 +---- src/mc/compare.cpp | 59 ++++++++++++++---------------- src/mc/mc_private.hpp | 2 +- 6 files changed, 37 insertions(+), 66 deletions(-) diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp index 2d39dedf8e..99781cfae3 100644 --- a/src/mc/VisitedState.cpp +++ b/src/mc/VisitedState.cpp @@ -16,13 +16,6 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_VisitedState, mc, "Logging specific to state namespace simgrid { namespace mc { -static int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2) -{ - simgrid::mc::Snapshot* s1 = state1->system_state.get(); - simgrid::mc::Snapshot* s2 = state2->system_state.get(); - return snapshot_compare(s1, s2); -} - /** @brief Save the current state */ VisitedState::VisitedState(unsigned long state_number) : num(state_number) { @@ -68,7 +61,7 @@ std::unique_ptr VisitedStates::addVisitedState( if (compare_snpashots) for (auto i = range.first; i != range.second; ++i) { auto& visited_state = *i; - if (snapshot_compare(visited_state.get(), new_state.get()) == 0) { + if (snapshot_equal(visited_state->system_state.get(), new_state->system_state.get())) { // The state has been visited: std::unique_ptr old_state = diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index 4638611d09..2ed9954b8c 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -80,13 +80,6 @@ std::shared_ptr> LivenessChecker::get_proposition_values( return std::make_shared>(std::move(values)); } -int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2) -{ - simgrid::mc::Snapshot* s1 = state1->graph_state->system_state.get(); - simgrid::mc::Snapshot* s2 = state2->graph_state->system_state.get(); - return simgrid::mc::snapshot_compare(s1, s2); -} - std::shared_ptr LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair) { std::shared_ptr new_pair = std::make_shared( @@ -98,10 +91,9 @@ std::shared_ptr LivenessChecker::insert_acceptance_pair(simgrid::mc if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) { std::shared_ptr const& pair_test = *i; - if (xbt_automaton_state_compare( - pair_test->automaton_state, new_pair->automaton_state) != 0 - || *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) - || this->compare(pair_test.get(), new_pair.get()) != 0) + if (xbt_automaton_state_compare(pair_test->automaton_state, new_pair->automaton_state) != 0 || + *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) || + not snapshot_equal(pair_test->graph_state->system_state.get(), new_pair->graph_state->system_state.get())) continue; XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num); exploration_stack_.pop_back(); @@ -200,11 +192,10 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr visited_pa for (auto i = range.first; i != range.second; ++i) { VisitedPair* pair_test = i->get(); - if (xbt_automaton_state_compare( - pair_test->automaton_state, visited_pair->automaton_state) != 0 - || *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) - || this->compare(pair_test, visited_pair.get()) != 0) - continue; + if (xbt_automaton_state_compare(pair_test->automaton_state, visited_pair->automaton_state) != 0 || + *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) || + not snapshot_equal(pair_test->graph_state->system_state.get(), visited_pair->graph_state->system_state.get())) + continue; if (pair_test->other_num == -1) visited_pair->other_num = pair_test->num; else diff --git a/src/mc/checker/LivenessChecker.hpp b/src/mc/checker/LivenessChecker.hpp index e90523ca9d..3867a9e8ff 100644 --- a/src/mc/checker/LivenessChecker.hpp +++ b/src/mc/checker/LivenessChecker.hpp @@ -63,7 +63,6 @@ public: void log_state() override; private: - int compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2); std::shared_ptr> get_proposition_values(); std::shared_ptr insert_acceptance_pair(simgrid::mc::Pair* pair); int insert_visited_pair(std::shared_ptr visited_pair, simgrid::mc::Pair* pair); diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index bdda1e75d9..d64486ac47 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -31,17 +31,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, namespace simgrid { namespace mc { -static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2) -{ - simgrid::mc::Snapshot* s1 = state1->system_state.get(); - simgrid::mc::Snapshot* s2 = state2->system_state.get(); - return snapshot_compare(s1, s2); -} - void SafetyChecker::check_non_termination(simgrid::mc::State* current_state) { for (auto state = stack_.rbegin(); state != stack_.rend(); ++state) - if (snapshot_compare(state->get(), current_state) == 0) { + if (snapshot_equal((*state)->system_state.get(), current_state->system_state.get())) { XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num); XBT_INFO("******************************************"); XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***"); diff --git a/src/mc/compare.cpp b/src/mc/compare.cpp index 81937fb8d7..6ab52008d3 100644 --- a/src/mc/compare.cpp +++ b/src/mc/compare.cpp @@ -1285,9 +1285,9 @@ static int compare_areas_with_type(simgrid::mc::StateComparator& state, void* re } while (true); } -static int compare_global_variables(simgrid::mc::StateComparator& state, simgrid::mc::ObjectInformation* object_info, - simgrid::mc::Region* r1, simgrid::mc::Region* r2, simgrid::mc::Snapshot* snapshot1, - simgrid::mc::Snapshot* snapshot2) +static bool global_variables_equal(simgrid::mc::StateComparator& state, simgrid::mc::ObjectInformation* object_info, + simgrid::mc::Region* r1, simgrid::mc::Region* r2, simgrid::mc::Snapshot* snapshot1, + simgrid::mc::Snapshot* snapshot2) { xbt_assert(r1 && r2, "Missing region."); @@ -1309,22 +1309,20 @@ static int compare_global_variables(simgrid::mc::StateComparator& state, simgrid XBT_VERB("Global variable %s (%p) is different between snapshots", current_var.name.c_str(), (char *) current_var.address); - return 1; + return false; } } - return 0; + return true; } -static int compare_local_variables(simgrid::mc::StateComparator& state, - simgrid::mc::Snapshot* snapshot1, - simgrid::mc::Snapshot* snapshot2, - mc_snapshot_stack_t stack1, - mc_snapshot_stack_t stack2) +static bool local_variables_equal(simgrid::mc::StateComparator& state, simgrid::mc::Snapshot* snapshot1, + simgrid::mc::Snapshot* snapshot2, mc_snapshot_stack_t stack1, + mc_snapshot_stack_t stack2) { if (stack1->local_variables.size() != stack2->local_variables.size()) { XBT_VERB("Different number of local variables"); - return 1; + return false; } for (unsigned int cursor = 0; cursor < stack1->local_variables.size(); cursor++) { @@ -1337,25 +1335,22 @@ static int compare_local_variables(simgrid::mc::StateComparator& state, "or frame (%s - %s) or ip (%lu - %lu)", current_var1->name.c_str(), current_var2->name.c_str(), current_var1->subprogram->name.c_str(), current_var2->subprogram->name.c_str(), current_var1->ip, current_var2->ip); - return 1; + return false; } // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram - simgrid::mc::Type* subtype = current_var1->type; - int res = compare_areas_with_type(state, current_var1->address, snapshot1, - snapshot1->get_region(current_var1->address), current_var2->address, snapshot2, - snapshot2->get_region(current_var2->address), subtype, 0); - - if (res == 1) { + if (compare_areas_with_type(state, current_var1->address, snapshot1, snapshot1->get_region(current_var1->address), + current_var2->address, snapshot2, snapshot2->get_region(current_var2->address), + current_var1->type, 0) == 1) { // TODO, fix current_varX->subprogram->name to include name if DW_TAG_inlined_subprogram XBT_VERB("Local variable %s (%p - %p) in frame %s " "is different between snapshots", current_var1->name.c_str(), current_var1->address, current_var2->address, current_var1->subprogram->name.c_str()); - return res; + return false; } } - return 0; + return true; } namespace simgrid { @@ -1363,7 +1358,7 @@ namespace mc { static std::unique_ptr state_comparator; -int snapshot_compare(Snapshot* s1, Snapshot* s2) +bool snapshot_equal(Snapshot* s1, Snapshot* s2) { // TODO, make this a field of ModelChecker or something similar if (state_comparator == nullptr) @@ -1376,14 +1371,14 @@ int snapshot_compare(Snapshot* s1, Snapshot* s2) if (s1->hash_ != s2->hash_) { XBT_VERB("(%d - %d) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_, s2->hash_); - return 1; + return false; } else XBT_VERB("(%d - %d) Same hash: 0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_); /* Compare enabled processes */ if (s1->enabled_processes_ != s2->enabled_processes_) { XBT_VERB("(%d - %d) Different amount of enabled processes", s1->num_state_, s2->num_state_); - return 1; + return false; } /* Compare size of stacks */ @@ -1393,7 +1388,7 @@ int snapshot_compare(Snapshot* s1, Snapshot* s2) if (size_used1 != size_used2) { XBT_VERB("(%d - %d) Different size used in stacks: %zu - %zu", s1->num_state_, s2->num_state_, size_used1, size_used2); - return 1; + return false; } } @@ -1406,7 +1401,7 @@ int snapshot_compare(Snapshot* s1, Snapshot* s2) if (res_init == -1) { XBT_VERB("(%d - %d) Different heap information", s1->num_state_, s2->num_state_); - return 1; + return false; } /* Stacks comparison */ @@ -1414,15 +1409,15 @@ int snapshot_compare(Snapshot* s1, Snapshot* s2) mc_snapshot_stack_t stack1 = &s1->stacks_[cursor]; mc_snapshot_stack_t stack2 = &s2->stacks_[cursor]; - if (compare_local_variables(*state_comparator, s1, s2, stack1, stack2) > 0) { + if (not local_variables_equal(*state_comparator, s1, s2, stack1, stack2)) { XBT_VERB("(%d - %d) Different local variables between stacks %u", s1->num_state_, s2->num_state_, cursor + 1); - return 1; + return false; } } size_t regions_count = s1->snapshot_regions_.size(); if (regions_count != s2->snapshot_regions_.size()) - return 1; + return false; for (size_t k = 0; k != regions_count; ++k) { Region* region1 = s1->snapshot_regions_[k].get(); @@ -1437,22 +1432,22 @@ int snapshot_compare(Snapshot* s1, Snapshot* s2) xbt_assert(region1->object_info()); /* Compare global variables */ - if (compare_global_variables(*state_comparator, region1->object_info(), region1, region2, s1, s2)) { + if (not global_variables_equal(*state_comparator, region1->object_info(), region1, region2, s1, s2)) { std::string const& name = region1->object_info()->file_name; XBT_VERB("(%d - %d) Different global variables in %s", s1->num_state_, s2->num_state_, name.c_str()); - return 1; + return false; } } /* Compare heap */ if (mmalloc_compare_heap(*state_comparator, s1, s2) > 0) { XBT_VERB("(%d - %d) Different heap (mmalloc_compare)", s1->num_state_, s2->num_state_); - return 1; + return false; } XBT_VERB("(%d - %d) No difference found", s1->num_state_, s2->num_state_); - return 0; + return true; } } diff --git a/src/mc/mc_private.hpp b/src/mc/mc_private.hpp index aa749a46b9..8372ee315a 100644 --- a/src/mc/mc_private.hpp +++ b/src/mc/mc_private.hpp @@ -40,7 +40,7 @@ XBT_PRIVATE void find_object_address(std::vector const& map simgrid::mc::ObjectInformation* result); XBT_PRIVATE -int snapshot_compare(Snapshot* s1, Snapshot* s2); +bool snapshot_equal(Snapshot* s1, Snapshot* s2); // Move is somewhere else (in the LivenessChecker class, in the Session class?): extern XBT_PRIVATE xbt_automaton_t property_automaton; -- 2.20.1