X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/012a604e0ccb1e677bf9d538d06c9adc34740aed..1ac47fb418e3ed32ad12b3db4d1c02aa50c17091:/src/mc/ModelChecker.cpp diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 0f9601f61d..bce70eb9b2 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2020. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2021. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ @@ -14,6 +14,7 @@ #include "xbt/automaton.hpp" #include "xbt/system_error.hpp" +#include #include #include @@ -39,8 +40,23 @@ ModelChecker::ModelChecker(std::unique_ptr remote_simulation, void ModelChecker::start() { - checker_side_.start( - [](evutil_socket_t sig, short events, void* arg) { ((ModelChecker*)arg)->handle_events(sig, events); }); + checker_side_.start([](evutil_socket_t sig, short events, void* arg) { + auto mc = static_cast(arg); + if (events == EV_READ) { + std::array buffer; + ssize_t size = mc->checker_side_.get_channel().receive(buffer.data(), buffer.size(), false); + if (size == -1 && errno != EAGAIN) + throw simgrid::xbt::errno_error(); + + if (not mc->handle_message(buffer.data(), size)) + mc->checker_side_.break_loop(); + } else if (events == EV_SIGNAL) { + if (sig == SIGCHLD) + mc->handle_waitpid(); + } else { + xbt_die("Unexpected event"); + } + }); XBT_DEBUG("Waiting for the model-checked process"); int status; @@ -69,19 +85,18 @@ void ModelChecker::start() #endif } -static const std::pair ignored_local_variables[] = { - std::pair{ "e", "*" }, - std::pair{ "_log_ev", "*" }, +static constexpr auto ignored_local_variables = { + std::make_pair("e", "*"), + std::make_pair("_log_ev", "*"), - /* Ignore local variable about time used for tracing */ - std::pair{ "start_time", "*" }, + /* Ignore local variable about time used for tracing */ + std::make_pair("start_time", "*"), }; void ModelChecker::setup_ignore() { - RemoteSimulation& process = this->get_remote_simulation(); - for (std::pair const& var : - ignored_local_variables) + const RemoteSimulation& process = this->get_remote_simulation(); + for (auto const& var : ignored_local_variables) process.ignore_local_variable(var.first, var.second); /* Static variable used for tracing */ @@ -90,7 +105,7 @@ void ModelChecker::setup_ignore() void ModelChecker::shutdown() { - XBT_DEBUG("Shuting down model-checker"); + XBT_DEBUG("Shutting down model-checker"); RemoteSimulation* process = &this->get_remote_simulation(); if (process->running()) { @@ -102,7 +117,7 @@ void ModelChecker::shutdown() void ModelChecker::resume(RemoteSimulation& process) { - int res = checker_side_.get_channel().send(MC_MESSAGE_CONTINUE); + int res = checker_side_.get_channel().send(MessageType::CONTINUE); if (res) throw xbt::errno_error(); process.clear_cache(); @@ -151,75 +166,70 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) memcpy(&base_message, buffer, sizeof(base_message)); switch(base_message.type) { - case MC_MESSAGE_IGNORE_HEAP: - { - s_mc_message_ignore_heap_t message; - xbt_assert(size == sizeof(message), "Broken messsage"); - memcpy(&message, buffer, sizeof(message)); - - IgnoredHeapRegion region; - region.block = message.block; - region.fragment = message.fragment; - region.address = message.address; - region.size = message.size; - get_remote_simulation().ignore_heap(region); - break; + case MessageType::IGNORE_HEAP: { + s_mc_message_ignore_heap_t message; + xbt_assert(size == sizeof(message), "Broken message"); + memcpy(&message, buffer, sizeof(message)); + + IgnoredHeapRegion region; + region.block = message.block; + region.fragment = message.fragment; + region.address = message.address; + region.size = message.size; + get_remote_simulation().ignore_heap(region); + break; } - case MC_MESSAGE_UNIGNORE_HEAP: - { - s_mc_message_ignore_memory_t message; - xbt_assert(size == sizeof(message), "Broken messsage"); - memcpy(&message, buffer, sizeof(message)); - get_remote_simulation().unignore_heap((void*)(std::uintptr_t)message.addr, message.size); - break; + case MessageType::UNIGNORE_HEAP: { + s_mc_message_ignore_memory_t message; + xbt_assert(size == sizeof(message), "Broken message"); + memcpy(&message, buffer, sizeof(message)); + get_remote_simulation().unignore_heap((void*)(std::uintptr_t)message.addr, message.size); + break; } - case MC_MESSAGE_IGNORE_MEMORY: - { - s_mc_message_ignore_memory_t message; - xbt_assert(size == sizeof(message), "Broken messsage"); - memcpy(&message, buffer, sizeof(message)); - this->get_remote_simulation().ignore_region(message.addr, message.size); - break; + case MessageType::IGNORE_MEMORY: { + s_mc_message_ignore_memory_t message; + xbt_assert(size == sizeof(message), "Broken message"); + memcpy(&message, buffer, sizeof(message)); + this->get_remote_simulation().ignore_region(message.addr, message.size); + break; } - case MC_MESSAGE_STACK_REGION: - { - s_mc_message_stack_region_t message; - xbt_assert(size == sizeof(message), "Broken messsage"); - memcpy(&message, buffer, sizeof(message)); - this->get_remote_simulation().stack_areas().push_back(message.stack_region); - } - break; - - case MC_MESSAGE_REGISTER_SYMBOL: - { - s_mc_message_register_symbol_t message; - xbt_assert(size == sizeof(message), "Broken message"); - memcpy(&message, buffer, sizeof(message)); - xbt_assert(not message.callback, "Support for client-side function proposition is not implemented."); - XBT_DEBUG("Received symbol: %s", message.name); - - if (property_automaton == nullptr) - property_automaton = xbt_automaton_new(); - - RemoteSimulation* process = &this->get_remote_simulation(); - RemotePtr address = remote((int*)message.data); - xbt::add_proposition(property_automaton, message.name, [process, address]() { return process->read(address); }); - - break; + case MessageType::STACK_REGION: { + s_mc_message_stack_region_t message; + xbt_assert(size == sizeof(message), "Broken message"); + memcpy(&message, buffer, sizeof(message)); + this->get_remote_simulation().stack_areas().push_back(message.stack_region); + } break; + + case MessageType::REGISTER_SYMBOL: { + s_mc_message_register_symbol_t message; + xbt_assert(size == sizeof(message), "Broken message"); + memcpy(&message, buffer, sizeof(message)); + xbt_assert(not message.callback, "Support for client-side function proposition is not implemented."); + XBT_DEBUG("Received symbol: %s", message.name.data()); + + if (property_automaton == nullptr) + property_automaton = xbt_automaton_new(); + + const RemoteSimulation* process = &this->get_remote_simulation(); + RemotePtr address = remote((int*)message.data); + xbt::add_proposition(property_automaton, message.name.data(), + [process, address]() { return process->read(address); }); + + break; } - case MC_MESSAGE_WAITING: - return false; + case MessageType::WAITING: + return false; - case MC_MESSAGE_ASSERTION_FAILED: - MC_report_assertion_error(); - this->exit(SIMGRID_MC_EXIT_SAFETY); + case MessageType::ASSERTION_FAILED: + MC_report_assertion_error(); + this->exit(SIMGRID_MC_EXIT_SAFETY); - default: - xbt_die("Unexpected message from model-checked application"); + default: + xbt_die("Unexpected message from model-checked application"); } return true; } @@ -233,26 +243,6 @@ void ModelChecker::exit(int status) ::exit(status); } -void ModelChecker::handle_events(int sig, short events) -{ - if (events == EV_READ) { - char buffer[MC_MESSAGE_LENGTH]; - ssize_t size = checker_side_.get_channel().receive(buffer, sizeof(buffer), false); - if (size == -1 && errno != EAGAIN) - throw simgrid::xbt::errno_error(); - - if (not handle_message(buffer, size)) - checker_side_.break_loop(); - } - else if (events == EV_SIGNAL) { - if (sig == SIGCHLD) - this->handle_waitpid(); - } - else { - xbt_die("Unexpected event"); - } -} - void ModelChecker::handle_waitpid() { XBT_DEBUG("Check for wait event"); @@ -317,7 +307,7 @@ void ModelChecker::handle_simcall(Transition const& transition) { s_mc_message_simcall_handle_t m; memset(&m, 0, sizeof(m)); - m.type = MC_MESSAGE_SIMCALL_HANDLE; + m.type = MessageType::SIMCALL_HANDLE; m.pid = transition.pid_; m.value = transition.argument_; checker_side_.get_channel().send(m); @@ -328,15 +318,15 @@ void ModelChecker::handle_simcall(Transition const& transition) bool ModelChecker::checkDeadlock() { - int res = checker_side_.get_channel().send(MC_MESSAGE_DEADLOCK_CHECK); + int res = checker_side_.get_channel().send(MessageType::DEADLOCK_CHECK); xbt_assert(res == 0, "Could not check deadlock state"); s_mc_message_int_t message; ssize_t s = checker_side_.get_channel().receive(message); xbt_assert(s != -1, "Could not receive message"); - xbt_assert(s == sizeof(message) && message.type == MC_MESSAGE_DEADLOCK_CHECK_REPLY, + xbt_assert(s == sizeof(message) && message.type == MessageType::DEADLOCK_CHECK_REPLY, "Received unexpected message %s (%i, size=%i) " - "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)", - MC_message_type_name(message.type), (int)message.type, (int)s, (int)MC_MESSAGE_DEADLOCK_CHECK_REPLY, + "expected MessageType::DEADLOCK_CHECK_REPLY (%i, size=%i)", + MC_message_type_name(message.type), (int)message.type, (int)s, (int)MessageType::DEADLOCK_CHECK_REPLY, (int)sizeof(message)); return message.value != 0; }