+ModelChecker::ModelChecker(std::unique_ptr<Process> process) :
+ page_store_(500),
+ process_(std::move(process)),
+ parent_snapshot_(nullptr)
+{
+
+}
+
+ModelChecker::~ModelChecker() {}
+
+void ModelChecker::start()
+{
+ const pid_t pid = process_->pid();
+
+ // Block SIGCHLD (this will be handled with accept/signalfd):
+ sigset_t set;
+ sigemptyset(&set);
+ sigaddset(&set, SIGCHLD);
+ if (sigprocmask(SIG_BLOCK, &set, nullptr) == -1)
+ throw simgrid::xbt::errno_error();
+
+ sigset_t full_set;
+ sigfillset(&full_set);
+
+ // Prepare data for poll:
+
+ struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
+ socket_pollfd->fd = process_->getChannel().getSocket();
+ socket_pollfd->events = POLLIN;
+ socket_pollfd->revents = 0;
+
+ int signal_fd = signalfd(-1, &set, 0);
+ if (signal_fd == -1)
+ throw simgrid::xbt::errno_error();
+
+ struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
+ signalfd_pollfd->fd = signal_fd;
+ signalfd_pollfd->events = POLLIN;
+ signalfd_pollfd->revents = 0;
+
+ XBT_DEBUG("Waiting for the model-checked process");
+ int status;
+
+ // The model-checked process SIGSTOP itself to signal it's ready:
+ pid_t res = waitpid(pid, &status, __WALL);
+ if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
+ xbt_die("Could not wait model-checked process");
+
+ process_->init();
+
+ if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0'))
+ MC_init_dot_output();
+
+ setup_ignore();
+
+ ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
+ ptrace(PTRACE_CONT, pid, 0, 0);
+}
+
+static const std::pair<const char*, const char*> ignored_local_variables[] = {
+ std::pair<const char*, const char*>{ "e", "*" },
+ std::pair<const char*, const char*>{ "__ex_cleanup", "*" },
+ std::pair<const char*, const char*>{ "__ex_mctx_en", "*" },
+ std::pair<const char*, const char*>{ "__ex_mctx_me", "*" },
+ std::pair<const char*, const char*>{ "__xbt_ex_ctx_ptr", "*" },
+ std::pair<const char*, const char*>{ "_log_ev", "*" },
+ std::pair<const char*, const char*>{ "_throw_ctx", "*" },
+ std::pair<const char*, const char*>{ "ctx", "*" },
+
+ std::pair<const char*, const char*>{ "self", "simcall_BODY_mc_snapshot" },
+ std::pair<const char*, const char*>{ "next_context", "smx_ctx_sysv_suspend_serial" },
+ std::pair<const char*, const char*>{ "i", "smx_ctx_sysv_suspend_serial" },
+
+ /* Ignore local variable about time used for tracing */
+ std::pair<const char*, const char*>{ "start_time", "*" },
+};
+
+void ModelChecker::setup_ignore()
+{
+ Process& process = this->process();
+ for (std::pair<const char*, const char*> const& var :
+ ignored_local_variables)
+ process.ignore_local_variable(var.first, var.second);
+
+ /* Static variable used for tracing */
+ process.ignore_global_variable("counter");
+}
+
+void ModelChecker::shutdown()
+{
+ XBT_DEBUG("Shuting down model-checker");
+
+ simgrid::mc::Process* process = &this->process();
+ if (process->running()) {
+ XBT_DEBUG("Killing process");
+ kill(process->pid(), SIGTERM);
+ process->terminate();
+ }
+}
+
+void ModelChecker::resume(simgrid::mc::Process& process)
+{
+ int res = process.getChannel().send(MC_MESSAGE_CONTINUE);
+ if (res)
+ throw simgrid::xbt::errno_error();
+ process.clear_cache();
+}
+
+static
+void throw_socket_error(int fd)
+{
+ int error = 0;
+ socklen_t errlen = sizeof(error);
+ if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
+ error = errno;
+ throw simgrid::xbt::errno_error();
+}
+
+static void MC_report_crash(int status)
+{
+ XBT_INFO("**************************");
+ XBT_INFO("** CRASH IN THE PROGRAM **");
+ XBT_INFO("**************************");
+ if (WIFSIGNALED(status))
+ XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
+ else if (WIFEXITED(status))
+ XBT_INFO("From exit: %i", WEXITSTATUS(status));
+ if (WCOREDUMP(status))
+ XBT_INFO("A core dump was generated by the system.");
+ else
+ XBT_INFO("No core dump was generated by the system.");
+ XBT_INFO("Counter-example execution trace:");
+ simgrid::mc::dumpRecordPath();
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
+ simgrid::mc::session->logState();
+ XBT_INFO("Stack trace:");
+ mc_model_checker->process().dumpStack();
+}
+
+static void MC_report_assertion_error(void)
+{
+ XBT_INFO("**************************");
+ XBT_INFO("*** PROPERTY NOT VALID ***");
+ XBT_INFO("**************************");
+ XBT_INFO("Counter-example execution trace:");
+ simgrid::mc::dumpRecordPath();
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
+ simgrid::mc::session->logState();
+}
+
+bool ModelChecker::handle_message(char* buffer, ssize_t size)
+{
+ s_mc_message_t base_message;
+ if (size < (ssize_t) sizeof(base_message))
+ xbt_die("Broken message");
+ memcpy(&base_message, buffer, sizeof(base_message));
+
+ switch(base_message.type) {
+
+ case MC_MESSAGE_IGNORE_HEAP:
+ {
+ s_mc_ignore_heap_message_t message;
+ if (size != sizeof(message))
+ xbt_die("Broken messsage");
+ memcpy(&message, buffer, sizeof(message));
+
+ IgnoredHeapRegion region;
+ region.block = message.block;
+ region.fragment = message.fragment;
+ region.address = message.address;
+ region.size = message.size;
+ process().ignore_heap(region);
+ break;
+ }
+
+ case MC_MESSAGE_UNIGNORE_HEAP:
+ {
+ s_mc_ignore_memory_message_t message;
+ if (size != sizeof(message))
+ xbt_die("Broken messsage");
+ memcpy(&message, buffer, sizeof(message));
+ process().unignore_heap(
+ (void *)(std::uintptr_t) message.addr, message.size);
+ break;
+ }
+
+ case MC_MESSAGE_IGNORE_MEMORY:
+ {
+ s_mc_ignore_memory_message_t message;
+ if (size != sizeof(message))
+ xbt_die("Broken messsage");
+ memcpy(&message, buffer, sizeof(message));
+ this->process().ignore_region(message.addr, message.size);
+ break;
+ }
+
+ case MC_MESSAGE_STACK_REGION:
+ {
+ s_mc_stack_region_message_t message;
+ if (size != sizeof(message))
+ xbt_die("Broken messsage");
+ memcpy(&message, buffer, sizeof(message));
+ this->process().stack_areas().push_back(message.stack_region);
+ }
+ break;
+
+ case MC_MESSAGE_REGISTER_SYMBOL:
+ {
+ s_mc_register_symbol_message_t message;
+ if (size != sizeof(message))
+ xbt_die("Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ if (message.callback)
+ xbt_die("Support for client-side function proposition is not implemented.");
+ XBT_DEBUG("Received symbol: %s", message.name);
+
+ if (simgrid::mc::property_automaton == nullptr)
+ simgrid::mc::property_automaton = xbt_automaton_new();
+
+ simgrid::mc::Process* process = &this->process();
+ simgrid::mc::RemotePtr<int> address
+ = simgrid::mc::remote((int*) message.data);
+ simgrid::xbt::add_proposition(simgrid::mc::property_automaton,
+ message.name,
+ [process, address]() { return process->read(address); }
+ );
+
+ break;
+ }
+
+ case MC_MESSAGE_WAITING:
+ return false;
+
+ case MC_MESSAGE_ASSERTION_FAILED:
+ MC_report_assertion_error();
+ this->exit(SIMGRID_MC_EXIT_SAFETY);
+ break;
+
+ default:
+ xbt_die("Unexpected message from model-checked application");
+
+ }
+ return true;
+}
+
+/** Terminate the model-checker application */
+void ModelChecker::exit(int status)
+{
+ // TODO, terminate the model checker politely instead of exiting rudely
+ if (process().running())
+ kill(process().pid(), SIGKILL);
+ ::exit(status);
+}
+
+bool ModelChecker::handle_events()
+{
+ char buffer[MC_MESSAGE_LENGTH];
+ struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
+ struct pollfd* signalfd_pollfd = &fds_[SIGNAL_FD_INDEX];
+
+ while(poll(fds_, 2, -1) == -1) {
+ switch(errno) {
+ case EINTR:
+ continue;
+ default:
+ throw simgrid::xbt::errno_error();
+ }
+ }
+
+ if (socket_pollfd->revents) {
+ if (socket_pollfd->revents & POLLIN) {
+ ssize_t size = process_->getChannel().receive(buffer, sizeof(buffer), false);
+ if (size == -1 && errno != EAGAIN)
+ throw simgrid::xbt::errno_error();
+ return handle_message(buffer, size);
+ }
+ if (socket_pollfd->revents & POLLERR)
+ throw_socket_error(socket_pollfd->fd);
+ if (socket_pollfd->revents & POLLHUP)
+ xbt_die("Socket hang up?");
+ }
+
+ if (signalfd_pollfd->revents) {
+ if (signalfd_pollfd->revents & POLLIN) {
+ this->handle_signals();
+ return true;
+ }
+ if (signalfd_pollfd->revents & POLLERR)
+ throw_socket_error(signalfd_pollfd->fd);
+ if (signalfd_pollfd->revents & POLLHUP)
+ xbt_die("Signalfd hang up?");
+ }
+
+ return true;
+}
+
+void ModelChecker::loop()