X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/7757612e2826fd790cbcf39d5fd8e8904747104d..3ae4039533d80613612bb81524c164f33384df92:/src/mc/mc_server.cpp diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp index fb123fa750..0e567b10e4 100644 --- a/src/mc/mc_server.cpp +++ b/src/mc/mc_server.cpp @@ -15,11 +15,16 @@ #include -#include "mc_model_checker.h" +#include "ModelChecker.hpp" #include "mc_protocol.h" #include "mc_server.h" #include "mc_private.h" #include "mc_ignore.h" +#include "mcer_ignore.h" + +using simgrid::mc::remote; + +extern "C" { XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic"); @@ -29,6 +34,20 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic"); mc_server_t mc_server; +struct mc_symbol_pointer_callback +{ + mc_process_t process; + void* value; +}; + +static int mc_symbol_pointer_callback_evaluate(void* p) +{ + struct mc_symbol_pointer_callback* callback = (struct mc_symbol_pointer_callback*) p; + int value; + callback->process->read_bytes(&value, sizeof(value), remote(callback->value)); + return value; +} + s_mc_server::s_mc_server(pid_t pid, int socket) { this->pid = pid; @@ -40,11 +59,9 @@ void s_mc_server::start() /* Wait for the target process to initialize and exchange a HELLO messages * before trying to look at its memory map. */ - XBT_DEBUG("Greeting the MC client"); int res = MC_protocol_hello(socket); if (res != 0) throw std::system_error(res, std::system_category()); - XBT_DEBUG("Greeted the MC client"); // Block SIGCHLD (this will be handled with accept/signalfd): sigset_t set; @@ -77,7 +94,7 @@ void s_mc_server::shutdown() { XBT_DEBUG("Shuting down model-checker"); - mc_process_t process = &mc_model_checker->process; + mc_process_t process = &mc_model_checker->process(); int status = process->status; if (process->running) { XBT_DEBUG("Killing process"); @@ -92,13 +109,13 @@ void s_mc_server::shutdown() void s_mc_server::exit() { // Finished: - int status = mc_model_checker->process.status; + int status = mc_model_checker->process().status; if (WIFEXITED(status)) ::exit(WEXITSTATUS(status)); else if (WIFSIGNALED(status)) { // Try to uplicate the signal of the model-checked process. // This is a temporary hack so we don't try too hard. - kill(mc_model_checker->process.pid, WTERMSIG(status)); + kill(mc_model_checker->process().pid, WTERMSIG(status)); abort(); } else { xbt_die("Unexpected status from model-checked process"); @@ -111,6 +128,7 @@ void s_mc_server::resume(mc_process_t process) int res = MC_protocol_send_simple_message(socket, MC_MESSAGE_CONTINUE); if (res) throw std::system_error(res, std::system_category()); + process->cache_flags = (mc_process_cache_flags_t) 0; } static @@ -123,7 +141,7 @@ void throw_socket_error(int fd) throw std::system_error(error, std::system_category()); } -void s_mc_server::handle_events() +bool s_mc_server::handle_events() { char buffer[MC_MESSAGE_LENGTH]; struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX]; @@ -141,7 +159,7 @@ void s_mc_server::handle_events() if (socket_pollfd->revents) { if (socket_pollfd->revents & POLLIN) { - ssize_t size = recv(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT); + ssize_t size = MC_receive_message(socket_pollfd->fd, buffer, sizeof(buffer), MSG_DONTWAIT); if (size == -1 && errno != EAGAIN) throw std::system_error(errno, std::system_category()); @@ -153,36 +171,82 @@ void s_mc_server::handle_events() switch(base_message.type) { case MC_MESSAGE_IGNORE_HEAP: - XBT_DEBUG("Received ignored region"); - if (size != sizeof(s_mc_ignore_heap_message_t)) - xbt_die("Broken messsage"); - // TODO, handle the message - break; + { + s_mc_ignore_heap_message_t message; + if (size != sizeof(message)) + xbt_die("Broken messsage"); + memcpy(&message, buffer, sizeof(message)); + mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1); + *region = message.region; + MC_heap_region_ignore_insert(region); + break; + } case MC_MESSAGE_UNIGNORE_HEAP: - XBT_DEBUG("Received unignored region"); - if (size != sizeof(s_mc_ignore_memory_message_t)) - xbt_die("Broken messsage"); - // TODO, handle the message - break; + { + s_mc_ignore_memory_message_t message; + if (size != sizeof(message)) + xbt_die("Broken messsage"); + memcpy(&message, buffer, sizeof(message)); + MC_heap_region_ignore_remove(message.addr, message.size); + break; + } case MC_MESSAGE_IGNORE_MEMORY: { - XBT_DEBUG("Received ignored memory"); - if (size != sizeof(s_mc_ignore_memory_message_t)) - xbt_die("Broken messsage"); s_mc_ignore_memory_message_t message; + if (size != sizeof(message)) + xbt_die("Broken messsage"); + memcpy(&message, buffer, sizeof(message)); + mc_model_checker->process().ignore_region( + (std::uint64_t)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)); - MC_process_ignore_memory(&mc_model_checker->process, - message.addr, message.size); + stack_region_t stack_region = xbt_new(s_stack_region_t, 1); + *stack_region = message.stack_region; + MC_stack_area_add(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 callbacks/functions symbols not implemented in client/server mode."); + XBT_DEBUG("Received symbol: %s", message.name); + + struct mc_symbol_pointer_callback* callback = xbt_new(struct mc_symbol_pointer_callback, 1); + callback->process = &mc_model_checker->process(); + callback->value = message.data; + + MC_automaton_new_propositional_symbol_callback(message.name, + mc_symbol_pointer_callback_evaluate, callback, free); + break; + } + + case MC_MESSAGE_WAITING: + return false; + + case MC_MESSAGE_ASSERTION_FAILED: + MC_report_assertion_error(); + xbt_abort(); + break; + default: xbt_die("Unexpected message from model-checked application"); } - return; + return true; } if (socket_pollfd->revents & POLLERR) { throw_socket_error(socket_pollfd->fd); @@ -194,7 +258,7 @@ void s_mc_server::handle_events() if (signalfd_pollfd->revents) { if (signalfd_pollfd->revents & POLLIN) { this->handle_signals(); - return; + return true; } if (signalfd_pollfd->revents & POLLERR) { throw_socket_error(signalfd_pollfd->fd); @@ -202,11 +266,13 @@ void s_mc_server::handle_events() if (signalfd_pollfd->revents & POLLHUP) xbt_die("Signalfd hang up?"); } + + return true; } void s_mc_server::loop() { - while (mc_model_checker->process.running) + while (mc_model_checker->process().running) this->handle_events(); } @@ -239,21 +305,21 @@ void s_mc_server::handle_waitpid() if (pid == -1) { if (errno == ECHILD) { // No more children: - if (mc_model_checker->process.running) + if (mc_model_checker->process().running) xbt_die("Inconsistent state"); else break; } else { - XBT_ERROR("Could not wait for pid: %s", strerror(errno)); + XBT_ERROR("Could not wait for pid"); throw std::system_error(errno, std::system_category()); } } - if (pid == mc_model_checker->process.pid) { + if (pid == mc_model_checker->process().pid) { if (WIFEXITED(status) || WIFSIGNALED(status)) { XBT_DEBUG("Child process is over"); - mc_model_checker->process.status = status; - mc_model_checker->process.running = false; + mc_model_checker->process().status = status; + mc_model_checker->process().running = false; } } } @@ -269,3 +335,34 @@ void s_mc_server::on_signal(const struct signalfd_siginfo* info) break; } } + +void MC_server_wait_client(mc_process_t process) +{ + mc_server->resume(process); + while (mc_model_checker->process().running) { + if (!mc_server->handle_events()) + return; + } +} + +void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value) +{ + s_mc_simcall_handle_message m; + memset(&m, 0, sizeof(m)); + m.type = MC_MESSAGE_SIMCALL_HANDLE; + m.pid = pid; + m.value = value; + MC_protocol_send(mc_model_checker->process().socket, &m, sizeof(m)); + process->cache_flags = (mc_process_cache_flags_t) 0; + while (mc_model_checker->process().running) { + if (!mc_server->handle_events()) + return; + } +} + +void MC_server_loop(mc_server_t server) +{ + server->loop(); +} + +}