MC/compare: cleanup++

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index 2d39ded..99781cf 100644 (file)
--- 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 {
 
 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)
 {
 /** @brief Save the current state */
 VisitedState::VisitedState(unsigned long state_number) : num(state_number)
 {


@@ -68,7 +61,7 @@ std::unique_ptr<simgrid::mc::VisitedState> VisitedStates::addVisitedState(
   if (compare_snpashots)
     for (auto i = range.first; i != range.second; ++i) {
       auto& visited_state = *i;
   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<simgrid::mc::VisitedState> old_state =
         // The state has been visited:
 
         std::unique_ptr<simgrid::mc::VisitedState> old_state =

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index 4638611..2ed9954 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -80,13 +80,6 @@ std::shared_ptr<const std::vector<int>> LivenessChecker::get_proposition_values(
   return std::make_shared<const std::vector<int>>(std::move(values));
 }
 
   return std::make_shared<const std::vector<int>>(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<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair)
 {
   std::shared_ptr<VisitedPair> new_pair = std::make_shared<VisitedPair>(
 std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc::Pair* pair)
 {
   std::shared_ptr<VisitedPair> new_pair = std::make_shared<VisitedPair>(


@@ -98,10 +91,9 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
 
   if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) {
     std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
 
   if (pair->search_cycle) for (auto i = res.first; i != res.second; ++i) {
     std::shared_ptr<simgrid::mc::VisitedPair> 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();
       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<VisitedPair> visited_pa
 
   for (auto i = range.first; i != range.second; ++i) {
     VisitedPair* pair_test = i->get();
 
   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
     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 e90523c..3867a9e 100644 (file)
--- a/src/mc/checker/LivenessChecker.hpp
+++ b/src/mc/checker/LivenessChecker.hpp
@@ -63,7 +63,6 @@ public:
   void log_state() override;
 
 private:
   void log_state() override;
 
 private:

-  int compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2);

   std::shared_ptr<const std::vector<int>> get_proposition_values();
   std::shared_ptr<VisitedPair> insert_acceptance_pair(simgrid::mc::Pair* pair);
   int insert_visited_pair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair);
   std::shared_ptr<const std::vector<int>> get_proposition_values();
   std::shared_ptr<VisitedPair> insert_acceptance_pair(simgrid::mc::Pair* pair);
   int insert_visited_pair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair);

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index bdda1e7..d64486a 100644 (file)
--- 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 {
 
 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)
 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 ***");
       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 81937fb..6ab5200 100644 (file)
--- 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);
 }
 
   } 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.");
 
 {
   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);
       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");
 {
   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++) {
   }
 
   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);
                "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
 
     }
     // 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());
       // 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 {
 }
 
 namespace simgrid {


@@ -1363,7 +1358,7 @@ namespace mc {
 
 static std::unique_ptr<simgrid::mc::StateComparator> state_comparator;
 
 
 static std::unique_ptr<simgrid::mc::StateComparator> 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)
 {
   // 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_);
   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_);
     } 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 */
   }
 
   /* 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);
     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_);
 
   if (res_init == -1) {
     XBT_VERB("(%d - %d) Different heap information", s1->num_state_, s2->num_state_);

-    return 1;
+    return false;

   }
 
   /* Stacks comparison */
   }
 
   /* 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];
 
     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);
       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())
     }
   }
 
   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();
 
   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 */
     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());
       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_);
     }
   }
 
   /* 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_);
 
   }
 
     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 aa749a4..8372ee3 100644 (file)
--- a/src/mc/mc_private.hpp
+++ b/src/mc/mc_private.hpp
@@ -40,7 +40,7 @@ XBT_PRIVATE void find_object_address(std::vector<simgrid::xbt::VmMap> const& map
                                      simgrid::mc::ObjectInformation* result);
 
 XBT_PRIVATE
                                      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;
 
 // Move is somewhere else (in the LivenessChecker class, in the Session class?):
 extern XBT_PRIVATE xbt_automaton_t property_automaton;