-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()) {
- dot_output_ = fopen(_sg_mc_dot_output_file.get().c_str(), "w");
- xbt_assert(dot_output_ != nullptr, "Error open dot output file: %s", strerror(errno));
-
- fprintf(dot_output_, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node "
- "[fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
- }
-
- 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);
-}
-
-void ModelChecker::dot_output(const char* fmt, ...)
-{
- if (dot_output_ != nullptr) {
- va_list ap;
- va_start(ap, fmt);
- vfprintf(dot_output_, fmt, ap);
- va_end(ap);
- }
-}
-
-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()