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 "mc_server.h"
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");
36 // HArdcoded index for now:
37 #define SOCKET_FD_INDEX 0
38 #define SIGNAL_FD_INDEX 1
40 mc_server_t mc_server;
42 s_mc_server::s_mc_server(pid_t pid_, int socket_)
43 : pid(pid_), socket(socket_) {}
45 void s_mc_server::start()
47 // Block SIGCHLD (this will be handled with accept/signalfd):
50 sigaddset(&set, SIGCHLD);
51 if (sigprocmask(SIG_BLOCK, &set, NULL) == -1)
52 throw std::system_error(errno, std::system_category());
55 sigfillset(&full_set);
57 // Prepare data for poll:
59 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
60 socket_pollfd->fd = socket;
61 socket_pollfd->events = POLLIN;
62 socket_pollfd->revents = 0;
64 int signal_fd = signalfd(-1, &set, 0);
66 throw std::system_error(errno, std::system_category());
68 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
69 signalfd_pollfd->fd = signal_fd;
70 signalfd_pollfd->events = POLLIN;
71 signalfd_pollfd->revents = 0;
73 XBT_DEBUG("Waiting for the model-checked process");
76 // The model-checked process SIGSTOP itself to signal it's ready:
77 pid_t res = waitpid(pid, &status, __WALL);
78 if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
79 xbt_die("Could not wait model-checked process");
81 // The model-checked process is ready, we can read its memory layout:
82 MC_init_model_checker(pid, socket);
84 ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
85 ptrace(PTRACE_CONT, pid, 0, 0);
88 void s_mc_server::shutdown()
90 XBT_DEBUG("Shuting down model-checker");
92 simgrid::mc::Process* process = &mc_model_checker->process();
93 int status = process->status();
94 if (process->running()) {
95 XBT_DEBUG("Killing process");
96 kill(process->pid(), SIGTERM);
97 if (waitpid(process->pid(), &status, 0) == -1)
98 throw std::system_error(errno, std::system_category());
99 // TODO, handle the case when the process does not want to die with a timeout
100 process->terminate(status);
104 void s_mc_server::exit()
107 int status = mc_model_checker->process().status();
108 if (WIFEXITED(status))
109 ::exit(WEXITSTATUS(status));
110 else if (WIFSIGNALED(status)) {
111 // Try to uplicate the signal of the model-checked process.
112 // This is a temporary hack so we don't try too hard.
113 kill(mc_model_checker->process().pid(), WTERMSIG(status));
116 xbt_die("Unexpected status from model-checked process");
120 void s_mc_server::resume(simgrid::mc::Process* process)
122 int res = process->send_message(MC_MESSAGE_CONTINUE);
124 throw std::system_error(res, std::system_category());
125 process->cache_flags = (mc_process_cache_flags_t) 0;
129 void throw_socket_error(int fd)
132 socklen_t errlen = sizeof(error);
133 if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
135 throw std::system_error(error, std::system_category());
138 bool s_mc_server::handle_message(char* buffer, ssize_t size)
140 s_mc_message_t base_message;
141 if (size < (ssize_t) sizeof(base_message))
142 xbt_die("Broken message");
143 memcpy(&base_message, buffer, sizeof(base_message));
145 switch(base_message.type) {
147 case MC_MESSAGE_IGNORE_HEAP:
149 s_mc_ignore_heap_message_t message;
150 if (size != sizeof(message))
151 xbt_die("Broken messsage");
152 memcpy(&message, buffer, sizeof(message));
153 mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
154 *region = message.region;
155 MC_heap_region_ignore_insert(region);
159 case MC_MESSAGE_UNIGNORE_HEAP:
161 s_mc_ignore_memory_message_t message;
162 if (size != sizeof(message))
163 xbt_die("Broken messsage");
164 memcpy(&message, buffer, sizeof(message));
165 MC_heap_region_ignore_remove(
166 (void *)(std::uintptr_t) message.addr, message.size);
170 case MC_MESSAGE_IGNORE_MEMORY:
172 s_mc_ignore_memory_message_t message;
173 if (size != sizeof(message))
174 xbt_die("Broken messsage");
175 memcpy(&message, buffer, sizeof(message));
176 mc_model_checker->process().ignore_region(
177 message.addr, message.size);
181 case MC_MESSAGE_STACK_REGION:
183 s_mc_stack_region_message_t message;
184 if (size != sizeof(message))
185 xbt_die("Broken messsage");
186 memcpy(&message, buffer, sizeof(message));
187 stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
188 *stack_region = message.stack_region;
189 MC_stack_area_add(stack_region);
193 case MC_MESSAGE_REGISTER_SYMBOL:
195 s_mc_register_symbol_message_t message;
196 if (size != sizeof(message))
197 xbt_die("Broken message");
198 memcpy(&message, buffer, sizeof(message));
199 if (message.callback)
200 xbt_die("Support for client-side function proposition is not implemented.");
201 XBT_DEBUG("Received symbol: %s", message.name);
203 if (_mc_property_automaton == NULL)
204 _mc_property_automaton = xbt_automaton_new();
206 simgrid::mc::Process* process = &mc_model_checker->process();
207 simgrid::mc::remote_ptr<int> address
208 = simgrid::mc::remote((int*) message.data);
209 simgrid::xbt::add_proposition(_mc_property_automaton,
211 [process, address]() { return process->read(address); }
217 case MC_MESSAGE_WAITING:
220 case MC_MESSAGE_ASSERTION_FAILED:
221 MC_report_assertion_error();
222 ::exit(SIMGRID_EXIT_SAFETY);
226 xbt_die("Unexpected message from model-checked application");
232 bool s_mc_server::handle_events()
234 char buffer[MC_MESSAGE_LENGTH];
235 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
236 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
238 while(poll(fds, 2, -1) == -1) {
243 throw std::system_error(errno, std::system_category());
247 if (socket_pollfd->revents) {
248 if (socket_pollfd->revents & POLLIN) {
249 ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
250 if (size == -1 && errno != EAGAIN)
251 throw std::system_error(errno, std::system_category());
252 return handle_message(buffer, size);
254 if (socket_pollfd->revents & POLLERR) {
255 throw_socket_error(socket_pollfd->fd);
257 if (socket_pollfd->revents & POLLHUP)
258 xbt_die("Socket hang up?");
261 if (signalfd_pollfd->revents) {
262 if (signalfd_pollfd->revents & POLLIN) {
263 this->handle_signals();
266 if (signalfd_pollfd->revents & POLLERR) {
267 throw_socket_error(signalfd_pollfd->fd);
269 if (signalfd_pollfd->revents & POLLHUP)
270 xbt_die("Signalfd hang up?");
276 void s_mc_server::loop()
278 while (mc_model_checker->process().running())
279 this->handle_events();
282 void s_mc_server::handle_signals()
284 struct signalfd_siginfo info;
285 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
287 ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
292 throw std::system_error(errno, std::system_category());
293 } else if (size != sizeof(info))
294 return throw std::runtime_error(
295 "Bad communication with model-checked application");
299 this->on_signal(&info);
302 void s_mc_server::handle_waitpid()
304 XBT_DEBUG("Check for wait event");
307 while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
309 if (errno == ECHILD) {
311 if (mc_model_checker->process().running())
312 xbt_die("Inconsistent state");
316 XBT_ERROR("Could not wait for pid");
317 throw std::system_error(errno, std::system_category());
321 if (pid == mc_model_checker->process().pid()) {
323 // From PTRACE_O_TRACEEXIT:
324 if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
325 if (ptrace(PTRACE_GETEVENTMSG, pid, 0, &status) == -1)
326 xbt_die("Could not get exit status");
327 if (WIFSIGNALED(status)) {
328 MC_report_crash(status);
329 ::exit(SIMGRID_PROGRAM_CRASH);
333 // We don't care about signals, just reinject them:
334 if (WIFSTOPPED(status)) {
335 XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
336 if (ptrace(PTRACE_CONT, pid, 0, WSTOPSIG(status)) == -1)
337 xbt_die("Could not PTRACE_CONT");
340 else if (WIFEXITED(status) || WIFSIGNALED(status)) {
341 XBT_DEBUG("Child process is over");
342 mc_model_checker->process().terminate(status);
348 void s_mc_server::on_signal(const struct signalfd_siginfo* info)
350 switch(info->ssi_signo) {
352 this->handle_waitpid();
359 void MC_server_wait_client(simgrid::mc::Process* process)
361 mc_server->resume(process);
362 while (mc_model_checker->process().running()) {
363 if (!mc_server->handle_events())
368 void MC_server_simcall_handle(simgrid::mc::Process* process, unsigned long pid, int value)
370 s_mc_simcall_handle_message m;
371 memset(&m, 0, sizeof(m));
372 m.type = MC_MESSAGE_SIMCALL_HANDLE;
375 mc_model_checker->process().send_message(m);
376 process->cache_flags = (mc_process_cache_flags_t) 0;
377 while (mc_model_checker->process().running()) {
378 if (!mc_server->handle_events())
383 void MC_server_loop(mc_server_t server)