X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/26af220e017a088b56105b2f21fadecf7d6e2a88..28e3d706d2b879fc7e84f569cd8cd72a86e0c550:/src/mc/simgrid_mc.cpp diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index 29d5fe2093..b8b4b08e76 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -10,156 +10,93 @@ #include #include -#include -#include +#include #include -#include -#include -#include -#include - #include #include "simgrid/sg_config.h" -#include "xbt_modinter.h" - -#include "mc_base.h" -#include "mc_private.h" -#include "mc_protocol.h" -#include "mc_server.h" -#include "mc_safety.h" -#include "mc_comm_pattern.h" -#include "mc_liveness.h" +#include "src/xbt_modinter.h" + +#include "src/mc/mc_base.h" +#include "src/mc/mc_private.h" +#include "src/mc/mc_protocol.h" +#include "src/mc/mc_safety.h" +#include "src/mc/mc_comm_pattern.h" +#include "src/mc/mc_liveness.h" +#include "src/mc/mc_exit.h" +#include "src/mc/Session.hpp" +#include "src/mc/Checker.hpp" +#include "src/mc/SafetyChecker.hpp" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc"); -static const bool trace = true; - -static int do_child(int socket, char** argv) -{ - XBT_DEBUG("Inside the child process PID=%i", (int) getpid()); - if (prctl(PR_SET_PDEATHSIG, SIGHUP) != 0) { - std::perror("simgrid-mc"); - return MC_SERVER_ERROR; - } - int res; - - // Remove CLOEXEC in order to pass the socket to the exec-ed program: - int fdflags = fcntl(socket, F_GETFD, 0); - if (fdflags == -1) { - std::perror("simgrid-mc"); - return MC_SERVER_ERROR; - } - if (fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1) { - std::perror("simgrid-mc"); - return MC_SERVER_ERROR; - } - - XBT_DEBUG("CLOEXEC removed on socket %i", socket); - - // Set environment: - setenv(MC_ENV_VARIABLE, "1", 1); - - char buffer[64]; - res = std::snprintf(buffer, sizeof(buffer), "%i", socket); - if ((size_t) res >= sizeof(buffer) || res == -1) - return MC_SERVER_ERROR; - setenv(MC_ENV_SOCKET_FD, buffer, 1); - - execvp(argv[1], argv+1); - std::perror("simgrid-mc"); - return MC_SERVER_ERROR; -} - -static int do_parent(int socket, pid_t child) -{ - XBT_DEBUG("Inside the parent process"); - if (mc_server) - xbt_die("MC server already present"); - try { - mc_mode = MC_MODE_SERVER; - mc_server = new s_mc_server(child, socket); - mc_server->start(); - MC_init_pid(child, socket); - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - MC_modelcheck_comm_determinism(); - else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') - MC_modelcheck_safety(); - else - MC_modelcheck_liveness(); - mc_server->shutdown(); - mc_server->exit(); - } - catch(std::exception& e) { - XBT_ERROR(e.what()); - } - exit(MC_SERVER_ERROR); -} - -static char** argvdup(int argc, char** argv) +static inline +char** argvdup(int argc, char** argv) { char** argv_copy = xbt_new(char*, argc+1); std::memcpy(argv_copy, argv, sizeof(char*) * argc); - argv_copy[argc] = NULL; + argv_copy[argc] = nullptr; return argv_copy; } -int main(int argc, char** argv) +static +std::unique_ptr createChecker(simgrid::mc::Session& session) { - // We need to keep the original parameters in order to pass them to the - // model-checked process: - int argc_copy = argc; - char** argv_copy = argvdup(argc, argv); - xbt_log_init(&argc_copy, argv_copy); - sg_config_init(&argc_copy, argv_copy); - - if (argc < 2) - xbt_die("Missing arguments.\n"); - - bool server_mode = true; - char* env = std::getenv("SIMGRID_MC_MODE"); - if (env) { - if (std::strcmp(env, "server") == 0) - server_mode = true; - else if (std::strcmp(env, "standalone") == 0) - server_mode = false; - else - xbt_die("Unrecognised value for SIMGRID_MC_MODE (server/standalone)"); - } + using simgrid::mc::Session; + using simgrid::mc::FunctionalChecker; + + std::function code; + if (_sg_mc_comms_determinism || _sg_mc_send_determinism) + code = [](Session& session) { + return MC_modelcheck_comm_determinism(); }; + else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') + return std::unique_ptr( + new simgrid::mc::SafetyChecker(session)); + else + code = [](Session& session) { + return simgrid::mc::modelcheck_liveness(); }; + + return std::unique_ptr( + new FunctionalChecker(session, std::move(code))); +} - if (!server_mode) { - setenv(MC_ENV_VARIABLE, "1", 1); - execvp(argv[1], argv+1); +int main(int argc, char** argv) +{ + using simgrid::mc::Session; - std::perror("simgrid-mc"); - return 127; - } + try { + if (argc < 2) + xbt_die("Missing arguments.\n"); - // Create a AF_LOCAL socketpair: - int res; + // Currently, we need this before sg_config_init: + _sg_do_model_check = 1; + mc_mode = MC_MODE_SERVER; - int sockets[2]; - res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets); - if (res == -1) { - perror("simgrid-mc"); - return MC_SERVER_ERROR; + // The initialisation function can touch argv. + // We make a copy of argv before modifying it in order to pass the original + // value to the model-checked: + char** argv_copy = argvdup(argc, argv); + xbt_log_init(&argc, argv); + sg_config_init(&argc, argv); + + std::unique_ptr session = + std::unique_ptr(Session::spawnvp(argv_copy[1], argv_copy+1)); + free(argv_copy); + + simgrid::mc::session = session.get(); + std::unique_ptr checker = createChecker(*session); + int res = checker->run(); + session->close(); + return res; } - - XBT_DEBUG("Created socketpair"); - - pid_t pid = fork(); - if (pid < 0) { - perror("simgrid-mc"); - return MC_SERVER_ERROR; - } else if (pid == 0) { - close(sockets[1]); - return do_child(sockets[0], argv); - } else { - close(sockets[0]); - return do_parent(sockets[1], pid); + catch(std::exception& e) { + XBT_ERROR("Exception: %s", e.what()); + return SIMGRID_MC_EXIT_ERROR; + } + catch(...) { + XBT_ERROR("Unknown exception"); + return SIMGRID_MC_EXIT_ERROR; } - - return 0; }