Convert simgrid::mc::snapshot_equal() into Snapshot::operator==()

Also inline 2 more functions from mc::api

diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp
index fa2302a..790d90a 100644 (file)
--- a/src/mc/VisitedState.cpp
+++ b/src/mc/VisitedState.cpp
@@ -52,7 +52,7 @@ VisitedStates::addVisitedState(unsigned long state_number, simgrid::mc::State* g
   if (compare_snapshots)
     for (auto i = range_begin; i != range_end; ++i) {
       auto& visited_state = *i;
-      if (Api::get().snapshot_equal(visited_state->system_state.get(), new_state->system_state.get())) {
+      if (*visited_state->system_state.get() == *new_state->system_state.get()) {
         // The state has been visited:
 
         std::unique_ptr<simgrid::mc::VisitedState> old_state =

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 70f4c57..d866d44 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -35,16 +35,4 @@ std::size_t Api::get_remote_heap_bytes() const
   auto heap_bytes_used      = mmalloc_get_bytes_used_remote(process.get_heap()->heaplimit, process.get_malloc_info());
   return heap_bytes_used;
 }
-
-bool Api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const
-{
-  return simgrid::mc::snapshot_equal(s1, s2);
-}
-
-simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const
-{
-  auto snapshot = new simgrid::mc::Snapshot(num_state);
-  return snapshot;
-}
-
 } // namespace simgrid::mc

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 7c084d6..b5422c2 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -54,10 +54,6 @@ public:
   // REMOTE APIs
   std::size_t get_remote_heap_bytes() const;
 
-  // SNAPSHOT APIs
-  bool snapshot_equal(const Snapshot* s1, const Snapshot* s2) const;
-  simgrid::mc::Snapshot* take_snapshot(long num_state) const;
-
   // AUTOMATION APIs
   inline DerefAndCompareByActorsCountAndUsedHeap compare_pair() const
   {

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index 7467b6a..c2b8af5 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -22,8 +22,7 @@ State::State(RemoteApp& remote_app) : num_(++expended_states_)
   transition_.reset(new Transition());
   /* Stateful model checking */
   if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
-    auto snapshot_ptr = Api::get().take_snapshot(num_);
-    system_state_     = std::shared_ptr<simgrid::mc::Snapshot>(snapshot_ptr);
+    system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_);
   }
 }
 

diff --git a/src/mc/compare.cpp b/src/mc/compare.cpp
index a59f4c7..8acb0dd 100644 (file)
--- a/src/mc/compare.cpp
+++ b/src/mc/compare.cpp
@@ -1174,61 +1174,62 @@ static bool local_variables_differ(const simgrid::mc::RemoteProcess& process, si
 
 namespace simgrid::mc {
 
-bool snapshot_equal(const Snapshot* s1, const Snapshot* s2)
+bool Snapshot::operator==(const Snapshot& other)
 {
   // TODO, make this a field of ModelChecker or something similar
   static StateComparator state_comparator;
 
   const RemoteProcess& process = mc_model_checker->get_remote_process();
 
-  if (s1->hash_ != s2->hash_) {
-    XBT_VERB("(%ld - %ld) Different hash: 0x%" PRIx64 "--0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_,
-             s2->hash_);
+  if (hash_ != other.hash_) {
+    XBT_VERB("(%ld - %ld) Different hash: 0x%" PRIx64 "--0x%" PRIx64, this->num_state_, other.num_state_, this->hash_,
+             other.hash_);
     return false;
   }
-  XBT_VERB("(%ld - %ld) Same hash: 0x%" PRIx64, s1->num_state_, s2->num_state_, s1->hash_);
+  XBT_VERB("(%ld - %ld) Same hash: 0x%" PRIx64, this->num_state_, other.num_state_, this->hash_);
 
   /* TODO: re-enable the quick filter of counting enabled processes in each snapshots */
 
   /* Compare size of stacks */
-  for (unsigned long i = 0; i < s1->stacks_.size(); i++) {
-    size_t size_used1 = s1->stack_sizes_[i];
-    size_t size_used2 = s2->stack_sizes_[i];
+  for (unsigned long i = 0; i < this->stacks_.size(); i++) {
+    size_t size_used1 = this->stack_sizes_[i];
+    size_t size_used2 = other.stack_sizes_[i];
     if (size_used1 != size_used2) {
-      XBT_VERB("(%ld - %ld) Different size used in stacks: %zu - %zu", s1->num_state_, s2->num_state_, size_used1,
+      XBT_VERB("(%ld - %ld) Different size used in stacks: %zu - %zu", num_state_, other.num_state_, size_used1,
                size_used2);
       return false;
     }
   }
 
   /* Init heap information used in heap comparison algorithm */
-  const s_xbt_mheap_t* heap1 = static_cast<xbt_mheap_t>(
-      s1->read_bytes(alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), process.heap_address, ReadOptions::lazy()));
-  const s_xbt_mheap_t* heap2 = static_cast<xbt_mheap_t>(
-      s2->read_bytes(alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), process.heap_address, ReadOptions::lazy()));
-  if (state_comparator.initHeapInformation(heap1, heap2, s1->to_ignore_, s2->to_ignore_) == -1) {
-    XBT_VERB("(%ld - %ld) Different heap information", s1->num_state_, s2->num_state_);
+  const s_xbt_mheap_t* heap1 = static_cast<xbt_mheap_t>(this->read_bytes(
+      alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), process.heap_address, ReadOptions::lazy()));
+  const s_xbt_mheap_t* heap2 = static_cast<xbt_mheap_t>(other.read_bytes(
+      alloca(sizeof(s_xbt_mheap_t)), sizeof(s_xbt_mheap_t), process.heap_address, ReadOptions::lazy()));
+  if (state_comparator.initHeapInformation(heap1, heap2, this->to_ignore_, other.to_ignore_) == -1) {
+    XBT_VERB("(%ld - %ld) Different heap information", this->num_state_, other.num_state_);
     return false;
   }
 
   /* Stacks comparison */
-  for (unsigned int cursor = 0; cursor < s1->stacks_.size(); cursor++) {
-    const_mc_snapshot_stack_t stack1 = &s1->stacks_[cursor];
-    const_mc_snapshot_stack_t stack2 = &s2->stacks_[cursor];
+  for (unsigned int cursor = 0; cursor < this->stacks_.size(); cursor++) {
+    const_mc_snapshot_stack_t stack1 = &this->stacks_[cursor];
+    const_mc_snapshot_stack_t stack2 = &other.stacks_[cursor];
 
-    if (local_variables_differ(process, state_comparator, *s1, *s2, stack1, stack2)) {
-      XBT_VERB("(%ld - %ld) Different local variables between stacks %u", s1->num_state_, s2->num_state_, cursor + 1);
+    if (local_variables_differ(process, state_comparator, *this, other, stack1, stack2)) {
+      XBT_VERB("(%ld - %ld) Different local variables between stacks %u", this->num_state_, other.num_state_,
+               cursor + 1);
       return false;
     }
   }
 
-  size_t regions_count = s1->snapshot_regions_.size();
-  if (regions_count != s2->snapshot_regions_.size())
+  size_t regions_count = this->snapshot_regions_.size();
+  if (regions_count != other.snapshot_regions_.size())
     return false;
 
   for (size_t k = 0; k != regions_count; ++k) {
-    Region* region1 = s1->snapshot_regions_[k].get();
-    Region* region2 = s2->snapshot_regions_[k].get();
+    Region* region1 = this->snapshot_regions_[k].get();
+    Region* region2 = other.snapshot_regions_[k].get();
 
     // Preconditions:
     if (region1->region_type() != RegionType::Data)
@@ -1239,20 +1240,20 @@ bool snapshot_equal(const Snapshot* s1, const Snapshot* s2)
     xbt_assert(region1->object_info());
 
     /* Compare global variables */
-    if (global_variables_differ(process, state_comparator, region1->object_info(), region1, region2, *s1, *s2)) {
+    if (global_variables_differ(process, state_comparator, region1->object_info(), region1, region2, *this, other)) {
       std::string const& name = region1->object_info()->file_name;
-      XBT_VERB("(%ld - %ld) Different global variables in %s", s1->num_state_, s2->num_state_, name.c_str());
+      XBT_VERB("(%ld - %ld) Different global variables in %s", this->num_state_, other.num_state_, name.c_str());
       return false;
     }
   }
 
   /* Compare heap */
-  if (mmalloc_heap_differ(process, state_comparator, *s1, *s2)) {
-    XBT_VERB("(%ld - %ld) Different heap (mmalloc_compare)", s1->num_state_, s2->num_state_);
+  if (mmalloc_heap_differ(process, state_comparator, *this, other)) {
+    XBT_VERB("(%ld - %ld) Different heap (mmalloc_compare)", this->num_state_, other.num_state_);
     return false;
   }
 
-  XBT_VERB("(%ld - %ld) No difference found", s1->num_state_, s2->num_state_);
+  XBT_VERB("(%ld - %ld) No difference found", this->num_state_, other.num_state_);
 
   return true;
 }

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 1bd4125..f2fb7ab 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -41,7 +41,7 @@ xbt::signal<void(RemoteApp&)> DFSExplorer::on_log_state_signal;
 void DFSExplorer::check_non_termination(const State* current_state)
 {
   for (auto state = stack_.rbegin(); state != stack_.rend(); ++state)
-    if (Api::get().snapshot_equal((*state)->get_system_state(), current_state->get_system_state())) {
+    if (*(*state)->get_system_state() == *current_state->get_system_state()) {
       XBT_INFO("Non-progressive cycle: state %ld -> state %ld", (*state)->get_num(), current_state->get_num());
       XBT_INFO("******************************************");
       XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 3d45e8d..fac5334 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -69,8 +69,7 @@ std::shared_ptr<VisitedPair> LivenessChecker::insert_acceptance_pair(simgrid::mc
       std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
       if (xbt_automaton_state_compare(pair_test->prop_state_, new_pair->prop_state_) != 0 ||
           *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
-          not Api::get().snapshot_equal(pair_test->app_state_->get_system_state(),
-                                        new_pair->app_state_->get_system_state()))
+          (*pair_test->app_state_->get_system_state() != *new_pair->app_state_->get_system_state()))
         continue;
       XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
       exploration_stack_.pop_back();
@@ -146,8 +145,7 @@ int LivenessChecker::insert_visited_pair(std::shared_ptr<VisitedPair> visited_pa
     const VisitedPair* pair_test = i->get();
     if (xbt_automaton_state_compare(pair_test->prop_state_, visited_pair->prop_state_) != 0 ||
         *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
-        not Api::get().snapshot_equal(pair_test->app_state_->get_system_state(),
-                                      visited_pair->app_state_->get_system_state()))
+        (*pair_test->app_state_->get_system_state() != *visited_pair->app_state_->get_system_state()))
       continue;
     if (pair_test->other_num == -1)
       visited_pair->other_num = pair_test->num;

diff --git a/src/mc/sosp/Snapshot.hpp b/src/mc/sosp/Snapshot.hpp
index dec7ffe..2548423 100644 (file)
--- a/src/mc/sosp/Snapshot.hpp
+++ b/src/mc/sosp/Snapshot.hpp
@@ -74,6 +74,9 @@ public:
   Region* get_region(const void* addr, Region* hinted_region) const;
   void restore(RemoteProcess* process) const;
 
+  bool operator==(const Snapshot& other);
+  bool operator!=(const Snapshot& other) { return not(*this == other); }
+
   // To be private
   long num_state_;
   std::size_t heap_bytes_used_ = 0;