1 /* Copyright (c) 2015. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
8 #include <system_error>
11 #include <sys/types.h>
13 #include <sys/socket.h>
14 #include <sys/signalfd.h>
15 #include <sys/ptrace.h>
18 #include <xbt/automaton.h>
19 #include <xbt/automaton.hpp>
21 #include "ModelChecker.hpp"
22 #include "mc_protocol.h"
23 #include "src/mc/Server.hpp"
24 #include "mc_private.h"
25 #include "mc_ignore.h"
26 #include "mcer_ignore.h"
28 #include "src/mc/mc_liveness.h"
30 using simgrid::mc::remote;
34 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Server, mc, "MC server logic");
38 // HArdcoded index for now:
39 #define SOCKET_FD_INDEX 0
40 #define SIGNAL_FD_INDEX 1
45 Server* server = nullptr;
47 Server::Server(pid_t pid_, int socket_)
48 : pid(pid_), socket(socket_) {}
52 // Block SIGCHLD (this will be handled with accept/signalfd):
55 sigaddset(&set, SIGCHLD);
56 if (sigprocmask(SIG_BLOCK, &set, NULL) == -1)
57 throw std::system_error(errno, std::system_category());
60 sigfillset(&full_set);
62 // Prepare data for poll:
64 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
65 socket_pollfd->fd = socket;
66 socket_pollfd->events = POLLIN;
67 socket_pollfd->revents = 0;
69 int signal_fd = signalfd(-1, &set, 0);
71 throw std::system_error(errno, std::system_category());
73 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
74 signalfd_pollfd->fd = signal_fd;
75 signalfd_pollfd->events = POLLIN;
76 signalfd_pollfd->revents = 0;
78 XBT_DEBUG("Waiting for the model-checked process");
81 // The model-checked process SIGSTOP itself to signal it's ready:
82 pid_t res = waitpid(pid, &status, __WALL);
83 if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
84 xbt_die("Could not wait model-checked process");
86 // The model-checked process is ready, we can read its memory layout:
87 MC_init_model_checker(pid, socket);
89 ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
90 ptrace(PTRACE_CONT, pid, 0, 0);
93 void Server::shutdown()
95 XBT_DEBUG("Shuting down model-checker");
97 simgrid::mc::Process* process = &mc_model_checker->process();
98 int status = process->status();
99 if (process->running()) {
100 XBT_DEBUG("Killing process");
101 kill(process->pid(), SIGTERM);
102 if (waitpid(process->pid(), &status, 0) == -1)
103 throw std::system_error(errno, std::system_category());
104 // TODO, handle the case when the process does not want to die with a timeout
105 process->terminate(status);
112 int status = mc_model_checker->process().status();
113 if (WIFEXITED(status))
114 ::exit(WEXITSTATUS(status));
115 else if (WIFSIGNALED(status)) {
116 // Try to uplicate the signal of the model-checked process.
117 // This is a temporary hack so we don't try too hard.
118 kill(mc_model_checker->process().pid(), WTERMSIG(status));
121 xbt_die("Unexpected status from model-checked process");
125 void Server::resume(simgrid::mc::Process& process)
127 int res = process.send_message(MC_MESSAGE_CONTINUE);
129 throw std::system_error(res, std::system_category());
130 process.cache_flags = (mc_process_cache_flags_t) 0;
134 void throw_socket_error(int fd)
137 socklen_t errlen = sizeof(error);
138 if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
140 throw std::system_error(error, std::system_category());
143 bool Server::handle_message(char* buffer, ssize_t size)
145 s_mc_message_t base_message;
146 if (size < (ssize_t) sizeof(base_message))
147 xbt_die("Broken message");
148 memcpy(&base_message, buffer, sizeof(base_message));
150 switch(base_message.type) {
152 case MC_MESSAGE_IGNORE_HEAP:
154 s_mc_ignore_heap_message_t message;
155 if (size != sizeof(message))
156 xbt_die("Broken messsage");
157 memcpy(&message, buffer, sizeof(message));
158 mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
159 *region = message.region;
160 MC_heap_region_ignore_insert(region);
164 case MC_MESSAGE_UNIGNORE_HEAP:
166 s_mc_ignore_memory_message_t message;
167 if (size != sizeof(message))
168 xbt_die("Broken messsage");
169 memcpy(&message, buffer, sizeof(message));
170 MC_heap_region_ignore_remove(
171 (void *)(std::uintptr_t) message.addr, message.size);
175 case MC_MESSAGE_IGNORE_MEMORY:
177 s_mc_ignore_memory_message_t message;
178 if (size != sizeof(message))
179 xbt_die("Broken messsage");
180 memcpy(&message, buffer, sizeof(message));
181 mc_model_checker->process().ignore_region(
182 message.addr, message.size);
186 case MC_MESSAGE_STACK_REGION:
188 s_mc_stack_region_message_t message;
189 if (size != sizeof(message))
190 xbt_die("Broken messsage");
191 memcpy(&message, buffer, sizeof(message));
192 stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
193 *stack_region = message.stack_region;
194 MC_stack_area_add(stack_region);
198 case MC_MESSAGE_REGISTER_SYMBOL:
200 s_mc_register_symbol_message_t message;
201 if (size != sizeof(message))
202 xbt_die("Broken message");
203 memcpy(&message, buffer, sizeof(message));
204 if (message.callback)
205 xbt_die("Support for client-side function proposition is not implemented.");
206 XBT_DEBUG("Received symbol: %s", message.name);
208 if (_mc_property_automaton == NULL)
209 _mc_property_automaton = xbt_automaton_new();
211 simgrid::mc::Process* process = &mc_model_checker->process();
212 simgrid::mc::remote_ptr<int> address
213 = simgrid::mc::remote((int*) message.data);
214 simgrid::xbt::add_proposition(_mc_property_automaton,
216 [process, address]() { return process->read(address); }
222 case MC_MESSAGE_WAITING:
225 case MC_MESSAGE_ASSERTION_FAILED:
226 MC_report_assertion_error();
227 ::exit(SIMGRID_EXIT_SAFETY);
231 xbt_die("Unexpected message from model-checked application");
237 bool Server::handle_events()
239 char buffer[MC_MESSAGE_LENGTH];
240 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
241 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
243 while(poll(fds, 2, -1) == -1) {
248 throw std::system_error(errno, std::system_category());
252 if (socket_pollfd->revents) {
253 if (socket_pollfd->revents & POLLIN) {
254 ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
255 if (size == -1 && errno != EAGAIN)
256 throw std::system_error(errno, std::system_category());
257 return handle_message(buffer, size);
259 if (socket_pollfd->revents & POLLERR) {
260 throw_socket_error(socket_pollfd->fd);
262 if (socket_pollfd->revents & POLLHUP)
263 xbt_die("Socket hang up?");
266 if (signalfd_pollfd->revents) {
267 if (signalfd_pollfd->revents & POLLIN) {
268 this->handle_signals();
271 if (signalfd_pollfd->revents & POLLERR) {
272 throw_socket_error(signalfd_pollfd->fd);
274 if (signalfd_pollfd->revents & POLLHUP)
275 xbt_die("Signalfd hang up?");
283 while (mc_model_checker->process().running())
284 this->handle_events();
287 void Server::handle_signals()
289 struct signalfd_siginfo info;
290 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
292 ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
297 throw std::system_error(errno, std::system_category());
298 } else if (size != sizeof(info))
299 return throw std::runtime_error(
300 "Bad communication with model-checked application");
304 this->on_signal(&info);
307 void Server::handle_waitpid()
309 XBT_DEBUG("Check for wait event");
312 while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
314 if (errno == ECHILD) {
316 if (mc_model_checker->process().running())
317 xbt_die("Inconsistent state");
321 XBT_ERROR("Could not wait for pid");
322 throw std::system_error(errno, std::system_category());
326 if (pid == mc_model_checker->process().pid()) {
328 // From PTRACE_O_TRACEEXIT:
329 if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
330 if (ptrace(PTRACE_GETEVENTMSG, pid, 0, &status) == -1)
331 xbt_die("Could not get exit status");
332 if (WIFSIGNALED(status)) {
333 MC_report_crash(status);
334 ::exit(SIMGRID_PROGRAM_CRASH);
338 // We don't care about signals, just reinject them:
339 if (WIFSTOPPED(status)) {
340 XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
341 if (ptrace(PTRACE_CONT, pid, 0, WSTOPSIG(status)) == -1)
342 xbt_die("Could not PTRACE_CONT");
345 else if (WIFEXITED(status) || WIFSIGNALED(status)) {
346 XBT_DEBUG("Child process is over");
347 mc_model_checker->process().terminate(status);
353 void Server::on_signal(const struct signalfd_siginfo* info)
355 switch(info->ssi_signo) {
357 this->handle_waitpid();
364 void Server::wait_client(simgrid::mc::Process& process)
366 this->resume(process);
367 while (mc_model_checker->process().running()) {
368 if (!simgrid::mc::server->handle_events())
373 void Server::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value)
375 s_mc_simcall_handle_message m;
376 memset(&m, 0, sizeof(m));
377 m.type = MC_MESSAGE_SIMCALL_HANDLE;
380 process.send_message(m);
381 process.cache_flags = (mc_process_cache_flags_t) 0;
382 while (process.running()) {
383 if (!simgrid::mc::server->handle_events())