From 6683699b87d403572f776668ac4d3ee3fc1b3e27 Mon Sep 17 00:00:00 2001
From: Arnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Date: Thu, 24 Feb 2022 11:42:33 +0100
Subject: [PATCH] Ensure that MC session and checker are deleted.

---
 src/mc/Session.cpp          |  2 +-
 src/mc/Session.hpp          |  2 +-
 src/mc/api.cpp              | 13 ++++++-------
 src/mc/explo/simgrid_mc.cpp |  4 ++--
 4 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index dffeed7e56..e8b1726234 100644
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -177,6 +177,6 @@ void Session::check_deadlock() const
   }
 }
 
-simgrid::mc::Session* session_singleton;
+std::unique_ptr<simgrid::mc::Session> session_singleton;
 }
 }
diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
index 8185115521..4c0269c931 100644
--- a/src/mc/Session.hpp
+++ b/src/mc/Session.hpp
@@ -57,7 +57,7 @@ public:
 };
 
 // Temporary :)
-extern simgrid::mc::Session* session_singleton;
+extern std::unique_ptr<simgrid::mc::Session> session_singleton;
 }
 }
 
diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index fcb42d8f38..29b0608dd8 100644
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -87,7 +87,7 @@ xbt::string const& Api::get_actor_name(smx_actor_t actor) const
 
 simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const
 {
-  auto session = new simgrid::mc::Session([argv] {
+  simgrid::mc::session_singleton = std::make_unique<simgrid::mc::Session>([argv] {
     int i = 1;
     while (argv[i] != nullptr && argv[i][0] == '-')
       i++;
@@ -100,27 +100,25 @@ simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgor
   simgrid::mc::Exploration* explo;
   switch (algo) {
     case CheckerAlgorithm::CommDeterminism:
-      explo = simgrid::mc::create_communication_determinism_checker(session);
+      explo = simgrid::mc::create_communication_determinism_checker(session_singleton.get());
       break;
 
     case CheckerAlgorithm::UDPOR:
-      explo = simgrid::mc::create_udpor_checker(session);
+      explo = simgrid::mc::create_udpor_checker(session_singleton.get());
       break;
 
     case CheckerAlgorithm::Safety:
-      explo = simgrid::mc::create_safety_checker(session);
+      explo = simgrid::mc::create_safety_checker(session_singleton.get());
       break;
 
     case CheckerAlgorithm::Liveness:
-      explo = simgrid::mc::create_liveness_checker(session);
+      explo = simgrid::mc::create_liveness_checker(session_singleton.get());
       break;
 
     default:
       THROW_IMPOSSIBLE;
   }
 
-  // FIXME: session and checker are never deleted
-  simgrid::mc::session_singleton = session;
   mc_model_checker->set_exploration(explo);
   return explo;
 }
@@ -176,6 +174,7 @@ simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const
 void Api::s_close() const
 {
   session_singleton->close();
+  session_singleton.reset();
   if (simgrid::mc::property_automaton != nullptr) {
     xbt_automaton_free(simgrid::mc::property_automaton);
     simgrid::mc::property_automaton = nullptr;
diff --git a/src/mc/explo/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp
index 7087b000c2..99dd4a3a98 100644
--- a/src/mc/explo/simgrid_mc.cpp
+++ b/src/mc/explo/simgrid_mc.cpp
@@ -47,7 +47,7 @@ int main(int argc, char** argv)
     algo = simgrid::mc::CheckerAlgorithm::Liveness;
 
   int res      = SIMGRID_MC_EXIT_SUCCESS;
-  auto checker = api::get().initialize(argv_copy.data(), algo);
+  std::unique_ptr<simgrid::mc::Exploration> checker{api::get().initialize(argv_copy.data(), algo)};
   try {
     checker->run();
   } catch (const simgrid::mc::DeadlockError&) {
@@ -58,6 +58,6 @@ int main(int argc, char** argv)
     res = SIMGRID_MC_EXIT_LIVENESS;
   }
   api::get().s_close();
-  // delete checker; SEGFAULT in liveness
+  checker.release(); // FIXME: this line should not exist, but it segfaults in liveness
   return res;
 }
-- 
2.20.1