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>
18 #include "mc_model_checker.h"
19 #include "mc_protocol.h"
20 #include "mc_server.h"
21 #include "mc_private.h"
22 #include "mc_ignore.h"
24 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
26 // HArdcoded index for now:
27 #define SOCKET_FD_INDEX 0
28 #define SIGNAL_FD_INDEX 1
30 mc_server_t mc_server;
32 struct mc_symbol_pointer_callback
38 static int mc_symbol_pointer_callback_evaluate(void* p)
40 struct mc_symbol_pointer_callback* callback = (struct mc_symbol_pointer_callback*) p;
42 MC_process_read(callback->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
43 &value, callback->value, sizeof(value), MC_PROCESS_INDEX_ANY);
47 s_mc_server::s_mc_server(pid_t pid, int socket)
50 this->socket = socket;
53 void s_mc_server::start()
55 /* Wait for the target process to initialize and exchange a HELLO messages
56 * before trying to look at its memory map.
58 int res = MC_protocol_hello(socket);
60 throw std::system_error(res, std::system_category());
62 // Block SIGCHLD (this will be handled with accept/signalfd):
65 sigaddset(&set, SIGCHLD);
66 if (sigprocmask(SIG_BLOCK, &set, NULL) == -1)
67 throw std::system_error(errno, std::system_category());
70 sigfillset(&full_set);
72 // Prepare data for poll:
74 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
75 socket_pollfd->fd = socket;
76 socket_pollfd->events = POLLIN;
77 socket_pollfd->revents = 0;
79 int signal_fd = signalfd(-1, &set, 0);
81 throw std::system_error(errno, std::system_category());
83 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
84 signalfd_pollfd->fd = signal_fd;
85 signalfd_pollfd->events = POLLIN;
86 signalfd_pollfd->revents = 0;
89 void s_mc_server::shutdown()
91 XBT_DEBUG("Shuting down model-checker");
93 mc_process_t process = &mc_model_checker->process;
94 int status = process->status;
95 if (process->running) {
96 XBT_DEBUG("Killing process");
97 kill(process->pid, SIGTERM);
98 if (waitpid(process->pid, &status, 0) == -1)
99 throw std::system_error(errno, std::system_category());
100 // TODO, handle the case when the process does not want to die with a timeout
101 process->status = status;
105 void s_mc_server::exit()
108 int status = mc_model_checker->process.status;
109 if (WIFEXITED(status))
110 ::exit(WEXITSTATUS(status));
111 else if (WIFSIGNALED(status)) {
112 // Try to uplicate the signal of the model-checked process.
113 // This is a temporary hack so we don't try too hard.
114 kill(mc_model_checker->process.pid, WTERMSIG(status));
117 xbt_die("Unexpected status from model-checked process");
121 void s_mc_server::resume(mc_process_t process)
123 int socket = process->socket;
124 int res = MC_protocol_send_simple_message(socket, MC_MESSAGE_CONTINUE);
126 throw std::system_error(res, std::system_category());
127 process->cache_flags = (e_mc_process_cache_flags_t) 0;
131 void throw_socket_error(int fd)
134 socklen_t errlen = sizeof(error);
135 if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
137 throw std::system_error(error, std::system_category());
140 bool s_mc_server::handle_events()
142 char buffer[MC_MESSAGE_LENGTH];
143 struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
144 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
146 while(poll(fds, 2, -1) == -1) {
151 throw std::system_error(errno, std::system_category());
155 if (socket_pollfd->revents) {
156 if (socket_pollfd->revents & POLLIN) {
158 ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT);
159 if (size == -1 && errno != EAGAIN)
160 throw std::system_error(errno, std::system_category());
162 s_mc_message_t base_message;
163 if (size < (ssize_t) sizeof(base_message))
164 xbt_die("Broken message");
165 memcpy(&base_message, buffer, sizeof(base_message));
167 switch(base_message.type) {
169 case MC_MESSAGE_IGNORE_HEAP:
171 s_mc_ignore_heap_message_t message;
172 if (size != sizeof(message))
173 xbt_die("Broken messsage");
174 memcpy(&message, buffer, sizeof(message));
175 mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
176 *region = message.region;
177 MC_heap_region_ignore_insert(region);
181 case MC_MESSAGE_UNIGNORE_HEAP:
183 s_mc_ignore_memory_message_t message;
184 if (size != sizeof(message))
185 xbt_die("Broken messsage");
186 memcpy(&message, buffer, sizeof(message));
187 MC_remove_ignore_heap(message.addr, message.size);
191 case MC_MESSAGE_IGNORE_MEMORY:
193 s_mc_ignore_memory_message_t message;
194 if (size != sizeof(message))
195 xbt_die("Broken messsage");
196 memcpy(&message, buffer, sizeof(message));
197 MC_process_ignore_memory(&mc_model_checker->process,
198 message.addr, message.size);
202 case MC_MESSAGE_STACK_REGION:
204 s_mc_stack_region_message_t message;
205 if (size != sizeof(message))
206 xbt_die("Broken messsage");
207 memcpy(&message, buffer, sizeof(message));
208 stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
209 *stack_region = message.stack_region;
210 MC_stack_area_add(stack_region);
214 case MC_MESSAGE_REGISTER_SYMBOL:
216 s_mc_register_symbol_message_t message;
217 if (size != sizeof(message))
218 xbt_die("Broken message");
219 memcpy(&message, buffer, sizeof(message));
220 if (message.callback)
221 xbt_die("Support for callbacks/functions symbols not implemented in client/server mode.");
222 XBT_DEBUG("Received symbol: %s", message.name);
224 struct mc_symbol_pointer_callback* callback = xbt_new(struct mc_symbol_pointer_callback, 1);
225 callback->process = &mc_model_checker->process;
226 callback->value = message.data;
228 MC_automaton_new_propositional_symbol_callback(message.name,
229 mc_symbol_pointer_callback_evaluate, callback, free);
233 case MC_MESSAGE_WAITING:
236 case MC_MESSAGE_ASSERTION_FAILED:
237 MC_report_assertion_error();
242 xbt_die("Unexpected message from model-checked application");
247 if (socket_pollfd->revents & POLLERR) {
248 throw_socket_error(socket_pollfd->fd);
250 if (socket_pollfd->revents & POLLHUP)
251 xbt_die("Socket hang up?");
254 if (signalfd_pollfd->revents) {
255 if (signalfd_pollfd->revents & POLLIN) {
256 this->handle_signals();
259 if (signalfd_pollfd->revents & POLLERR) {
260 throw_socket_error(signalfd_pollfd->fd);
262 if (signalfd_pollfd->revents & POLLHUP)
263 xbt_die("Signalfd hang up?");
269 void s_mc_server::loop()
271 while (mc_model_checker->process.running)
272 this->handle_events();
275 void s_mc_server::handle_signals()
277 struct signalfd_siginfo info;
278 struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
280 ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
285 throw std::system_error(errno, std::system_category());
286 } else if (size != sizeof(info))
287 return throw std::runtime_error(
288 "Bad communication with model-checked application");
292 this->on_signal(&info);
295 void s_mc_server::handle_waitpid()
297 XBT_DEBUG("Check for wait event");
300 while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
302 if (errno == ECHILD) {
304 if (mc_model_checker->process.running)
305 xbt_die("Inconsistent state");
309 XBT_ERROR("Could not wait for pid");
310 throw std::system_error(errno, std::system_category());
314 if (pid == mc_model_checker->process.pid) {
315 if (WIFEXITED(status) || WIFSIGNALED(status)) {
316 XBT_DEBUG("Child process is over");
317 mc_model_checker->process.status = status;
318 mc_model_checker->process.running = false;
324 void s_mc_server::on_signal(const struct signalfd_siginfo* info)
326 switch(info->ssi_signo) {
328 this->handle_waitpid();
335 void MC_server_wait_client(mc_process_t process)
337 mc_server->resume(process);
338 while (mc_model_checker->process.running) {
339 if (!mc_server->handle_events())
344 void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value)
346 s_mc_simcall_handle_message m;
347 memset(&m, 0, sizeof(m));
348 m.type = MC_MESSAGE_SIMCALL_HANDLE;
351 MC_protocol_send(mc_model_checker->process.socket, &m, sizeof(m));
352 process->cache_flags = (e_mc_process_cache_flags_t) 0;
353 while (mc_model_checker->process.running) {
354 if (!mc_server->handle_events())