X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/9c40447cb76e20937a7c2a5acedcd84a22990514..e7c2b72c7328c4aade5049a3cc21603a9d27842c:/src/mc/mc_server.cpp diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp index d9a024f443..869dd75818 100644 --- a/src/mc/mc_server.cpp +++ b/src/mc/mc_server.cpp @@ -29,6 +29,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; @@ -40,11 +55,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; @@ -111,6 +124,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 = (e_mc_process_cache_flags_t) 0; } static @@ -123,7 +137,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 +155,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,34 +167,40 @@ 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_remove_ignore_heap(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_process_ignore_memory(&mc_model_checker->process, message.addr, message.size); + break; } - break; case MC_MESSAGE_STACK_REGION: { - XBT_DEBUG("Received stack area"); s_mc_stack_region_message_t message; if (size != sizeof(message)) xbt_die("Broken messsage"); @@ -191,11 +211,38 @@ void s_mc_server::handle_events() } 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); @@ -207,7 +254,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); @@ -215,6 +262,8 @@ void s_mc_server::handle_events() if (signalfd_pollfd->revents & POLLHUP) xbt_die("Signalfd hang up?"); } + + return true; } void s_mc_server::loop() @@ -257,7 +306,7 @@ void s_mc_server::handle_waitpid() 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()); } } @@ -282,3 +331,27 @@ 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 = (e_mc_process_cache_flags_t) 0; + while (mc_model_checker->process.running) { + if (!mc_server->handle_events()) + return; + } +}