-ModelChecker::ModelChecker(std::unique_ptr<RemoteProcess> remote_simulation, int sockfd)
- : checker_side_(sockfd), remote_process_(std::move(remote_simulation))
-{
-}
-
-void ModelChecker::start()
-{
- checker_side_.start(
- [](evutil_socket_t sig, short events, void* arg) {
- auto mc = static_cast<simgrid::mc::ModelChecker*>(arg);
- if (events == EV_READ) {
- std::array<char, MC_MESSAGE_LENGTH> buffer;
- ssize_t size = mc->checker_side_.get_channel().receive(buffer.data(), buffer.size(), false);
- if (size == -1 && errno != EAGAIN)
- throw simgrid::xbt::errno_error();
-
- if (not mc->handle_message(buffer.data(), size))
- mc->checker_side_.break_loop();
- } else if (events == EV_SIGNAL) {
- if (sig == SIGCHLD)
- mc->handle_waitpid();
- } else {
- xbt_die("Unexpected event");
- }
- },
- this);
-
- XBT_DEBUG("Waiting for the model-checked process");
- int status;
-
- // The model-checked process SIGSTOP itself to signal it's ready:
- const pid_t pid = remote_process_->pid();
-
- xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
- "Could not wait model-checked process");
-
- if (not _sg_mc_dot_output_file.get().empty())
- MC_init_dot_output();
-
- setup_ignore();
-
- errno = 0;
-#ifdef __linux__
- ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
- ptrace(PTRACE_CONT, pid, 0, 0);
-#elif defined BSD
- ptrace(PT_CONTINUE, pid, (caddr_t)1, 0);
-#else
-# error "no ptrace equivalent coded for this platform"
-#endif
- xbt_assert(errno == 0,
- "Ptrace does not seem to be usable in your setup (errno: %d). "
- "If you run from within a docker, adding `--cap-add SYS_PTRACE` to the docker line may help. "
- "If it does not help, please report this bug.",
- errno);
-}
-
-static constexpr auto ignored_local_variables = {
- std::make_pair("e", "*"),
- std::make_pair("_log_ev", "*"),
-
- /* Ignore local variable about time used for tracing */
- std::make_pair("start_time", "*"),
-};
-
-void ModelChecker::setup_ignore()
-{
- const RemoteProcess& process = this->get_remote_process();
- for (auto const& [var, frame] : ignored_local_variables)
- process.ignore_local_variable(var, frame);
-
- /* Static variable used for tracing */
- process.ignore_global_variable("counter");
-}
-
-void ModelChecker::shutdown()
-{
- XBT_DEBUG("Shutting down model-checker");
-
- RemoteProcess& process = get_remote_process();
- if (process.running()) {
- XBT_DEBUG("Killing process");
- finalize_app(true);
- kill(process.pid(), SIGKILL);
- process.terminate();
- }
-}
-
-void ModelChecker::resume()