X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/d239d3b23481b30b2a17c1d5b1fdb5fec70fd23b..40334ce6fe520b2fa7d1e240716e4f34a5fdc74e:/src/mc/mc_server.cpp diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp index cd6653e79e..cf45be1343 100644 --- a/src/mc/mc_server.cpp +++ b/src/mc/mc_server.cpp @@ -15,10 +15,14 @@ #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" + +extern "C" { XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic"); @@ -28,6 +32,21 @@ 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; + MC_process_read(callback->process, MC_ADDRESS_SPACE_READ_FLAGS_NONE, + &value, callback->value, sizeof(value), MC_PROCESS_INDEX_ANY); + return value; +} + s_mc_server::s_mc_server(pid_t pid, int socket) { this->pid = pid; @@ -39,11 +58,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; @@ -76,7 +93,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"); @@ -91,13 +108,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"); @@ -110,6 +127,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 @@ -122,9 +140,9 @@ 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() { - s_mc_message_t message; + char buffer[MC_MESSAGE_LENGTH]; struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX]; struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX]; @@ -139,14 +157,95 @@ void s_mc_server::handle_events() if (socket_pollfd->revents) { if (socket_pollfd->revents & POLLIN) { - ssize_t size = recv(socket_pollfd->fd, &message, sizeof(message), 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()); - else switch(message.type) { + + s_mc_message_t base_message; + if (size < (ssize_t) sizeof(base_message)) + xbt_die("Broken message"); + memcpy(&base_message, buffer, sizeof(base_message)); + + switch(base_message.type) { + + case MC_MESSAGE_IGNORE_HEAP: + { + 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: + { + 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: + { + s_mc_ignore_memory_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); + 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)); + 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); @@ -158,7 +257,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); @@ -166,11 +265,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(); } @@ -203,21 +304,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; } } } @@ -233,3 +334,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(); +} + +}