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 if (process->running()) {
99 XBT_DEBUG("Killing process");
100 kill(process->pid(), SIGTERM);
101 process->terminate();
105 void Server::resume(simgrid::mc::Process& process)
107 int res = process.send_message(MC_MESSAGE_CONTINUE);
109 throw std::system_error(res, std::system_category());
110 process.cache_flags = (mc_process_cache_flags_t) 0;
114 void throw_socket_error(int fd)
117 socklen_t errlen = sizeof(error);
118 if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
120 throw std::system_error(error, std::system_category());
123 bool Server::handle_message(char* buffer, ssize_t size)
125 s_mc_message_t base_message;
126 if (size < (ssize_t) sizeof(base_message))
127 xbt_die("Broken message");
128 memcpy(&base_message, buffer, sizeof(base_message));
130 switch(base_message.type) {
132 case MC_MESSAGE_IGNORE_HEAP:
134 s_mc_ignore_heap_message_t message;
135 if (size != sizeof(message))
136 xbt_die("Broken messsage");
137 memcpy(&message, buffer, sizeof(message));
138 mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
139 *region = message.region;
140 MC_heap_region_ignore_insert(region);
144 case MC_MESSAGE_UNIGNORE_HEAP:
146 s_mc_ignore_memory_message_t message;
147 if (size != sizeof(message))
148 xbt_die("Broken messsage");
149 memcpy(&message, buffer, sizeof(message));
150 MC_heap_region_ignore_remove(
151 (void *)(std::uintptr_t) message.addr, message.size);
155 case MC_MESSAGE_IGNORE_MEMORY:
157 s_mc_ignore_memory_message_t message;
158 if (size != sizeof(message))
159 xbt_die("Broken messsage");
160 memcpy(&message, buffer, sizeof(message));
161 mc_model_checker->process().ignore_region(
162 message.addr, message.size);
166 case MC_MESSAGE_STACK_REGION:
168 s_mc_stack_region_message_t message;
169 if (size != sizeof(message))
170 xbt_die("Broken messsage");
171 memcpy(&message, buffer, sizeof(message));
172 stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
173 *stack_region = message.stack_region;
174 MC_stack_area_add(stack_region);
178 case MC_MESSAGE_REGISTER_SYMBOL:
180 s_mc_register_symbol_message_t message;
181 if (size != sizeof(message))
182 xbt_die("Broken message");
183 memcpy(&message, buffer, sizeof(message));
184 if (message.callback)
185 xbt_die("Support for client-side function proposition is not implemented.");
186 XBT_DEBUG("Received symbol: %s", message.name);
188 if (_mc_property_automaton == NULL)
189 _mc_property_automaton = xbt_automaton_new();
191 simgrid::mc::Process* process = &mc_model_checker->process();
192 simgrid::mc::remote_ptr<int> address
193 = simgrid::mc::remote((int*) message.data);
194 simgrid::xbt::add_proposition(_mc_property_automaton,
196 [process, address]() { return process->read(address); }
202 case MC_MESSAGE_WAITING:
205 case MC_MESSAGE_ASSERTION_FAILED:
206 MC_report_assertion_error();
207 ::exit(SIMGRID_MC_EXIT_SAFETY);
211 xbt_die("Unexpected message from model-checked application");
217 bool Server::handle_events()
219 char buffer[MC_MESSAGE_LENGTH];
220 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
221 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
223 while(poll(fds, 2, -1) == -1) {
228 throw std::system_error(errno, std::system_category());
232 if (socket_pollfd->revents) {
233 if (socket_pollfd->revents & POLLIN) {
234 ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
235 if (size == -1 && errno != EAGAIN)
236 throw std::system_error(errno, std::system_category());
237 return handle_message(buffer, size);
239 if (socket_pollfd->revents & POLLERR) {
240 throw_socket_error(socket_pollfd->fd);
242 if (socket_pollfd->revents & POLLHUP)
243 xbt_die("Socket hang up?");
246 if (signalfd_pollfd->revents) {
247 if (signalfd_pollfd->revents & POLLIN) {
248 this->handle_signals();
251 if (signalfd_pollfd->revents & POLLERR) {
252 throw_socket_error(signalfd_pollfd->fd);
254 if (signalfd_pollfd->revents & POLLHUP)
255 xbt_die("Signalfd hang up?");
263 while (mc_model_checker->process().running())
264 this->handle_events();
267 void Server::handle_signals()
269 struct signalfd_siginfo info;
270 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
272 ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
277 throw std::system_error(errno, std::system_category());
278 } else if (size != sizeof(info))
279 return throw std::runtime_error(
280 "Bad communication with model-checked application");
284 this->on_signal(&info);
287 void Server::handle_waitpid()
289 XBT_DEBUG("Check for wait event");
292 while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
294 if (errno == ECHILD) {
296 if (mc_model_checker->process().running())
297 xbt_die("Inconsistent state");
301 XBT_ERROR("Could not wait for pid");
302 throw std::system_error(errno, std::system_category());
306 if (pid == mc_model_checker->process().pid()) {
308 // From PTRACE_O_TRACEEXIT:
309 if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
310 if (ptrace(PTRACE_GETEVENTMSG, pid, 0, &status) == -1)
311 xbt_die("Could not get exit status");
312 if (WIFSIGNALED(status)) {
313 MC_report_crash(status);
314 ::exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
318 // We don't care about signals, just reinject them:
319 if (WIFSTOPPED(status)) {
320 XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
321 if (ptrace(PTRACE_CONT, pid, 0, WSTOPSIG(status)) == -1)
322 xbt_die("Could not PTRACE_CONT");
325 else if (WIFEXITED(status) || WIFSIGNALED(status)) {
326 XBT_DEBUG("Child process is over");
327 mc_model_checker->process().terminate();
333 void Server::on_signal(const struct signalfd_siginfo* info)
335 switch(info->ssi_signo) {
337 this->handle_waitpid();
344 void Server::wait_client(simgrid::mc::Process& process)
346 this->resume(process);
347 while (mc_model_checker->process().running()) {
348 if (!simgrid::mc::server->handle_events())
353 void Server::simcall_handle(simgrid::mc::Process& process, unsigned long pid, int value)
355 s_mc_simcall_handle_message m;
356 memset(&m, 0, sizeof(m));
357 m.type = MC_MESSAGE_SIMCALL_HANDLE;
360 process.send_message(m);
361 process.cache_flags = (mc_process_cache_flags_t) 0;
362 while (process.running()) {
363 if (!simgrid::mc::server->handle_events())