From b31e581e1422bec5a4088d3cadb53f8bf39c38ee Mon Sep 17 00:00:00 2001
From: Martin Quinson <martin.quinson@ens-rennes.fr>
Date: Mon, 11 Jul 2022 00:08:30 +0200
Subject: [PATCH] MC: allow to pass env variables to the verified application

---
 docs/source/Configuring_SimGrid.rst | 10 ++++++++++
 src/mc/api.cpp                      | 11 +++++++++--
 src/mc/api.hpp                      |  3 ++-
 src/mc/explo/simgrid_mc.cpp         | 27 ++++++++++++++++++++++++++-
 4 files changed, 47 insertions(+), 4 deletions(-)

diff --git a/docs/source/Configuring_SimGrid.rst b/docs/source/Configuring_SimGrid.rst
index f907c9dd30..4ea92064af 100644
--- a/docs/source/Configuring_SimGrid.rst
+++ b/docs/source/Configuring_SimGrid.rst
@@ -119,6 +119,7 @@ Existing Configuration Items
 - **model-check/reduction:** :ref:`cfg=model-check/reduction`
 - **model-check/replay:** :ref:`cfg=model-check/replay`
 - **model-check/send-determinism:** :ref:`cfg=model-check/send-determinism`
+- **model-check/setenv:** :ref:`cfg=model-check/setenv`
 - **model-check/termination:** :ref:`cfg=model-check/termination`
 - **model-check/timeout:** :ref:`cfg=model-check/timeout`
 - **model-check/visited:** :ref:`cfg=model-check/visited`
@@ -769,6 +770,15 @@ The ``model-check/communications-determinism`` and
 communication determinism mode of the model checker, which checks
 determinism properties of the communications of an application.
 
+.. _cfg=model-check/setenv:
+
+Passing environment variables
+.............................
+
+You can specify extra environment variables to be set in the verified application
+with ``model-check/setenv``. For example, you can preload a library as follows:
+``-cfg=model-check/setenv:LD_PRELOAD=toto;LD_LIBRARY_PATH=/tmp``.
+
 .. _options_mc_perf:
 
 Verification Performance Considerations
diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index 840ffef2c4..7a8c8db261 100644
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -30,12 +30,19 @@ XBT_LOG_EXTERNAL_CATEGORY(mc_global);
 
 namespace simgrid::mc {
 
-simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::ExplorationAlgorithm algo)
+simgrid::mc::Exploration* Api::initialize(char** argv, const std::unordered_map<std::string, std::string>& env,
+                                          simgrid::mc::ExplorationAlgorithm algo)
 {
-  session_ = std::make_unique<simgrid::mc::Session>([argv] {
+  session_ = std::make_unique<simgrid::mc::Session>([argv, &env] {
     int i = 1;
     while (argv[i] != nullptr && argv[i][0] == '-')
       i++;
+    for (auto const& kv : env) {
+      const char* key = kv.first.c_str();
+      const char* val = kv.second.c_str();
+      XBT_INFO("setenv '%s'='%s'", key, val);
+      setenv(key, val, 1);
+    }
     xbt_assert(argv[i] != nullptr,
                "Unable to find a binary to exec on the command line. Did you only pass config flags?");
     execvp(argv[i], argv + i);
diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 88b2e0c802..3edcb07a37 100644
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -53,7 +53,8 @@ public:
     return api;
   }
 
-  simgrid::mc::Exploration* initialize(char** argv, simgrid::mc::ExplorationAlgorithm algo);
+  simgrid::mc::Exploration* initialize(char** argv, const std::unordered_map<std::string, std::string>& env,
+                                       simgrid::mc::ExplorationAlgorithm algo);
 
   // ACTOR APIs
   std::vector<simgrid::mc::ActorInformation>& get_actors() const;
diff --git a/src/mc/explo/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp
index afd997a249..769c14c81f 100644
--- a/src/mc/explo/simgrid_mc.cpp
+++ b/src/mc/explo/simgrid_mc.cpp
@@ -13,10 +13,18 @@
 #include "smpi/smpi.h"
 #endif
 
+#include <boost/tokenizer.hpp>
 #include <cstring>
 #include <memory>
 #include <unistd.h>
 
+static simgrid::config::Flag<std::string> _sg_mc_setenv{
+    "model-check/setenv", "Extra environment variables to pass to the child process (ex: 'AZE=aze;QWE=qwe').", "",
+    [](std::string_view value) {
+      xbt_assert(value.empty() || value.find('=', 0) != std::string_view::npos,
+                 "The 'model-check/setenv' parameter must be like 'AZE=aze', but it does not contain an equal sign.");
+    }};
+
 int main(int argc, char** argv)
 {
   xbt_assert(argc >= 2, "Missing arguments");
@@ -44,8 +52,25 @@ int main(int argc, char** argv)
   else
     algo = simgrid::mc::ExplorationAlgorithm::Liveness;
 
+  std::unordered_map<std::string, std::string> environment;
+  /** Setup the tokenizer that parses the string **/
+  using Tokenizer = boost::tokenizer<boost::char_separator<char>>;
+  boost::char_separator<char> semicol_sep(";");
+  boost::char_separator<char> equal_sep("=");
+  Tokenizer token_vars(_sg_mc_setenv.get(), semicol_sep); /* Iterate over all FOO=foo parts */
+  for (const auto& token : token_vars) {
+    std::vector<std::string> kv;
+    Tokenizer token_kv(token, equal_sep);
+    for (const auto& t : token_kv) /* Iterate over 'FOO' and then 'foo' in that 'FOO=foo' */
+      kv.push_back(t);
+    xbt_assert(kv.size() == 2, "Parse error on 'model-check/setenv' value %s. Does it contain an equal sign?",
+               token.c_str());
+    environment[kv[0]] = kv[1];
+  }
+
   int res      = SIMGRID_MC_EXIT_SUCCESS;
-  std::unique_ptr<simgrid::mc::Exploration> checker{simgrid::mc::Api::get().initialize(argv_copy.data(), algo)};
+  std::unique_ptr<simgrid::mc::Exploration> checker{
+      simgrid::mc::Api::get().initialize(argv_copy.data(), environment, algo)};
   try {
     checker->run();
   } catch (const simgrid::mc::DeadlockError&) {
-- 
2.20.1