mc: change 3 static functions into private methods

And inline a fourth one

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 8bb58f6..e79fa47 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -112,7 +112,7 @@ void Session::execute(Transition const& transition)
 
 void Session::restoreInitialState()
 {
-  simgrid::mc::restore_snapshot(this->initialSnapshot_);
+  this->initialSnapshot_->restore(&mc_model_checker->process());
 }
 
 void Session::logState()

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index c3bf8b1..84f3f18 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -359,7 +359,7 @@ void CommunicationDeterminismChecker::restoreState()
   /* Intermediate backtracking */
   simgrid::mc::State* last_state = stack_.back().get();
   if (last_state->system_state) {
-    simgrid::mc::restore_snapshot(last_state->system_state);
+    last_state->system_state->restore(&mc_model_checker->process());
     MC_restore_communications_pattern(last_state);
     return;
   }

diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp
index d70ac11..411e4f5 100644 (file)
--- a/src/mc/checker/LivenessChecker.cpp
+++ b/src/mc/checker/LivenessChecker.cpp
@@ -132,7 +132,7 @@ void LivenessChecker::replay()
   if(_sg_mc_checkpoint > 0) {
     simgrid::mc::Pair* pair = explorationStack_.back().get();
     if(pair->graph_state->system_state){
-      simgrid::mc::restore_snapshot(pair->graph_state->system_state);
+      pair->graph_state->system_state->restore(&mc_model_checker->process());
       return;
     }
   }

diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp
index e3c741b..bd9ccd8 100644 (file)
--- a/src/mc/checker/SafetyChecker.cpp
+++ b/src/mc/checker/SafetyChecker.cpp
@@ -271,7 +271,7 @@ void SafetyChecker::restoreState()
   /* Intermediate backtracking */
   simgrid::mc::State* last_state = stack_.back().get();
   if (last_state->system_state) {
-    simgrid::mc::restore_snapshot(last_state->system_state);
+    last_state->system_state->restore(&mc_model_checker->process());
     return;
   }
 

diff --git a/src/mc/sosp/mc_snapshot.cpp b/src/mc/sosp/mc_snapshot.cpp
index 6ba9b6a..c7296a6 100644 (file)
--- a/src/mc/sosp/mc_snapshot.cpp
+++ b/src/mc/sosp/mc_snapshot.cpp
@@ -93,30 +93,29 @@ namespace mc {
 /************************************* Take Snapshot ************************************/
 /****************************************************************************************/
 
-static void get_memory_regions(simgrid::mc::RemoteClient* process, simgrid::mc::Snapshot* snapshot)
+void simgrid::mc::Snapshot::snapshot_regions(simgrid::mc::RemoteClient* process)
 {
-  snapshot->snapshot_regions_.clear();
+  snapshot_regions_.clear();
 
   for (auto const& object_info : process->object_infos)
-    snapshot->add_region(simgrid::mc::RegionType::Data, object_info.get(), object_info->start_rw, object_info->start_rw,
-                         object_info->end_rw - object_info->start_rw);
+    add_region(simgrid::mc::RegionType::Data, object_info.get(), object_info->start_rw, object_info->start_rw,
+               object_info->end_rw - object_info->start_rw);
 
   xbt_mheap_t heap = process->get_heap();
   void* start_heap = heap->base;
   void* end_heap   = heap->breakval;
 
-  snapshot->add_region(simgrid::mc::RegionType::Heap, nullptr, start_heap, start_heap,
-                       (char*)end_heap - (char*)start_heap);
-  snapshot->heap_bytes_used_     = mmalloc_get_bytes_used_remote(heap->heaplimit, process->get_malloc_info());
-  snapshot->privatization_index_ = simgrid::mc::ProcessIndexMissing;
+  add_region(simgrid::mc::RegionType::Heap, nullptr, start_heap, start_heap, (char*)end_heap - (char*)start_heap);
+  heap_bytes_used_     = mmalloc_get_bytes_used_remote(heap->heaplimit, process->get_malloc_info());
+  privatization_index_ = simgrid::mc::ProcessIndexMissing;
 
 #if HAVE_SMPI
   if (mc_model_checker->process().privatized() && MC_smpi_process_count())
     // snapshot->privatization_index = smpi_loaded_page
-    mc_model_checker->process().read_variable("smpi_loaded_page", &snapshot->privatization_index_,
-                                              sizeof(snapshot->privatization_index_));
+    mc_model_checker->process().read_variable("smpi_loaded_page", &privatization_index_, sizeof(privatization_index_));
 #endif
 }
+
 /** @brief Checks whether the variable is in scope for a given IP.
  *
  *  A variable may be defined only from a given value of IP.
@@ -239,9 +238,9 @@ static std::vector<s_mc_stack_frame_t> unwind_stack_frames(simgrid::mc::UnwindCo
   return result;
 }
 
-static void take_snapshot_stacks(simgrid::mc::Snapshot* snapshot)
+void simgrid::mc::Snapshot::snapshot_stacks(simgrid::mc::RemoteClient* process)
 {
-  for (auto const& stack : mc_model_checker->process().stack_areas()) {
+  for (auto const& stack : process->stack_areas()) {
     s_mc_snapshot_stack_t st;
 
     // Read the context from remote process:
@@ -256,10 +255,10 @@ static void take_snapshot_stacks(simgrid::mc::Snapshot* snapshot)
 
     unw_word_t sp = st.stack_frames[0].sp;
 
-    snapshot->stacks_.push_back(std::move(st));
+    stacks_.push_back(std::move(st));
 
     size_t stack_size = (char*)stack.address + stack.size - (char*)sp;
-    snapshot->stack_sizes_.push_back(stack_size);
+    stack_sizes_.push_back(stack_size);
   }
 }
 
@@ -296,18 +295,18 @@ Snapshot::Snapshot(int _num_state, RemoteClient* process)
     , privatization_index_(0)
     , hash_(0)
 {
-  for (auto const& p : mc_model_checker->process().actors())
+  for (auto const& p : process->actors())
     enabled_processes_.insert(p.copy.getBuffer()->get_pid());
 
   snapshot_handle_ignore(this);
 
   /* Save the std heap and the writable mapped pages of libsimgrid and binary */
-  get_memory_regions(process, this);
+  snapshot_regions(process);
 
-  to_ignore_ = mc_model_checker->process().ignored_heap();
+  to_ignore_ = process->ignored_heap();
 
   if (_sg_mc_max_visited_states > 0 || not _sg_mc_property_file.get().empty()) {
-    take_snapshot_stacks(this);
+    snapshot_stacks(process);
     if (_sg_mc_hash)
       hash_ = simgrid::mc::hash(*this);
   }
@@ -395,29 +394,24 @@ RegionSnapshot* Snapshot::get_region(const void* addr, int process_index, Region
     return get_region(addr, process_index);
 }
 
-static inline void restore_snapshot_regions(simgrid::mc::Snapshot* snapshot)
+void Snapshot::restore(RemoteClient* process)
 {
-  for (std::unique_ptr<simgrid::mc::RegionSnapshot> const& region : snapshot->snapshot_regions_) {
-    // For privatized, variables we decided it was not necessary to take the snapshot:
-    if (region)
+  XBT_DEBUG("Restore snapshot %i", num_state_);
+
+  // Restore regions
+  for (std::unique_ptr<simgrid::mc::RegionSnapshot> const& region : snapshot_regions_) {
+    if (region) // privatized variables are not snapshoted
       region.get()->restore();
   }
 
-#if HAVE_SMPI
-  if (snapshot->privatization_index_ >= 0) {
-    // Fix the privatization mmap:
-    s_mc_message_restore_t message{MC_MESSAGE_RESTORE, snapshot->privatization_index_};
-    mc_model_checker->process().getChannel().send(message);
+  // Fix the privatization mmap if needed
+  if (privatization_index_ >= 0) {
+    s_mc_message_restore_t message{MC_MESSAGE_RESTORE, privatization_index_};
+    process->getChannel().send(message);
   }
-#endif
-}
 
-void restore_snapshot(std::shared_ptr<simgrid::mc::Snapshot> snapshot)
-{
-  XBT_DEBUG("Restore snapshot %i", snapshot->num_state_);
-  restore_snapshot_regions(snapshot.get());
-  snapshot_ignore_restore(snapshot.get());
-  mc_model_checker->process().clear_cache();
+  snapshot_ignore_restore(this);
+  process->clear_cache();
 }
 
 } // namespace mc

diff --git a/src/mc/sosp/mc_snapshot.hpp b/src/mc/sosp/mc_snapshot.hpp
index c1d09df..233b19c 100644 (file)
--- a/src/mc/sosp/mc_snapshot.hpp
+++ b/src/mc/sosp/mc_snapshot.hpp
@@ -94,26 +94,31 @@ public:
   ~Snapshot() = default;
 
   /* Initialization */
-  void add_region(RegionType type, ObjectInformation* object_info, void* start_addr, void* permanent_addr,
-                  std::size_t size);
 
   /* Regular use */
   const void* read_bytes(void* buffer, std::size_t size, RemotePtr<void> address, int process_index = ProcessIndexAny,
                          ReadOptions options = ReadOptions::none()) const override;
   RegionSnapshot* get_region(const void* addr, int process_index) const;
   RegionSnapshot* get_region(const void* addr, int process_index, RegionSnapshot* hinted_region) const;
+  void restore(RemoteClient* process);
 
   // To be private
   int num_state_;
   std::size_t heap_bytes_used_;
   std::vector<std::unique_ptr<RegionSnapshot>> snapshot_regions_;
   std::set<pid_t> enabled_processes_;
-  int privatization_index_;
+  int privatization_index_ = 0;
   std::vector<std::size_t> stack_sizes_;
   std::vector<s_mc_snapshot_stack_t> stacks_;
   std::vector<simgrid::mc::IgnoredHeapRegion> to_ignore_;
   std::uint64_t hash_ = 0;
   std::vector<s_mc_snapshot_ignored_data_t> ignored_data_;
+
+private:
+  void add_region(RegionType type, ObjectInformation* object_info, void* start_addr, void* permanent_addr,
+                  std::size_t size);
+  void snapshot_regions(simgrid::mc::RemoteClient* process);
+  void snapshot_stacks(simgrid::mc::RemoteClient* process);
 };
 } // namespace mc
 } // namespace simgrid
@@ -124,7 +129,6 @@ namespace simgrid {
 namespace mc {
 
 XBT_PRIVATE std::shared_ptr<Snapshot> take_snapshot(int num_state);
-XBT_PRIVATE void restore_snapshot(std::shared_ptr<Snapshot> snapshot);
 } // namespace mc
 } // namespace simgrid