X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e9b99cc75875aaffe31d627aceb45a3583770d55..ce2d9960deb26e9c6216164a37f7c3d2382035c4:/src/mc/ModelChecker.cpp?ds=sidebyside diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index e4024eabaf..71a7f08aa6 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -9,7 +9,7 @@ #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_private.hpp" -#include "src/mc/remote/RemoteProcess.hpp" +#include "src/mc/sosp/RemoteProcessMemory.hpp" #include "src/mc/transition/TransitionComm.hpp" #include "xbt/automaton.hpp" #include "xbt/system_error.hpp" @@ -23,132 +23,11 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker"); ::simgrid::mc::ModelChecker* mc_model_checker = nullptr; -#ifdef __linux__ -# define WAITPID_CHECKED_FLAGS __WALL -#else -# define WAITPID_CHECKED_FLAGS 0 -#endif - namespace simgrid::mc { -ModelChecker::ModelChecker(std::unique_ptr remote_simulation, int sockfd) - : checker_side_(sockfd), remote_process_(std::move(remote_simulation)) -{ -} - -void ModelChecker::start() -{ - 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"); - } - }, - this); - - XBT_DEBUG("Waiting for the model-checked process"); - int status; - - // The model-checked process SIGSTOP itself to signal it's ready: - const pid_t pid = remote_process_->pid(); - - xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP, - "Could not wait model-checked process"); - - setup_ignore(); - - errno = 0; -#ifdef __linux__ - ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT); - ptrace(PTRACE_CONT, pid, 0, 0); -#elif defined BSD - ptrace(PT_CONTINUE, pid, (caddr_t)1, 0); -#else -# error "no ptrace equivalent coded for this platform" -#endif - xbt_assert(errno == 0, - "Ptrace does not seem to be usable in your setup (errno: %d). " - "If you run from within a docker, adding `--cap-add SYS_PTRACE` to the docker line may help. " - "If it does not help, please report this bug.", - errno); -} - -static constexpr auto ignored_local_variables = { - std::make_pair("e", "*"), - std::make_pair("_log_ev", "*"), - - /* Ignore local variable about time used for tracing */ - std::make_pair("start_time", "*"), -}; - -void ModelChecker::setup_ignore() -{ - const RemoteProcess& process = this->get_remote_process(); - for (auto const& [var, frame] : ignored_local_variables) - process.ignore_local_variable(var, frame); - - /* Static variable used for tracing */ - process.ignore_global_variable("counter"); -} - -void ModelChecker::shutdown() -{ - XBT_DEBUG("Shutting down model-checker"); - - RemoteProcess& process = get_remote_process(); - if (process.running()) { - XBT_DEBUG("Killing process"); - finalize_app(true); - kill(process.pid(), SIGKILL); - process.terminate(); - } -} - -void ModelChecker::resume() +ModelChecker::ModelChecker(std::unique_ptr remote_memory) + : remote_process_memory_(std::move(remote_memory)) { - if (checker_side_.get_channel().send(MessageType::CONTINUE) != 0) - throw xbt::errno_error(); - remote_process_->clear_cache(); -} - -static void MC_report_crash(Exploration* explorer, int status) -{ - XBT_INFO("**************************"); - XBT_INFO("** CRASH IN THE PROGRAM **"); - XBT_INFO("**************************"); - if (WIFSIGNALED(status)) - XBT_INFO("From signal: %s", strsignal(WTERMSIG(status))); - else if (WIFEXITED(status)) - XBT_INFO("From exit: %i", WEXITSTATUS(status)); - if (not xbt_log_no_loc) - XBT_INFO("%s core dump was generated by the system.", WCOREDUMP(status) ? "A" : "No"); - if (explorer) { - XBT_INFO("Counter-example execution trace:"); - for (auto const& s : explorer->get_textual_trace()) - XBT_INFO(" %s", s.c_str()); - XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with " - "--cfg=model-check/replay:'%s'", - explorer->get_record_trace().to_string().c_str()); - explorer->log_state(); - if (xbt_log_no_loc) { - XBT_INFO("Stack trace not displayed because you passed --log=no_loc"); - } else { - XBT_INFO("Stack trace:"); - mc_model_checker->get_remote_process().dump_stack(); - } - } } bool ModelChecker::handle_message(const char* buffer, ssize_t size) @@ -163,7 +42,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message)); memcpy(&message, buffer, sizeof(message)); - get_remote_process().init(message.mmalloc_default_mdp, message.maxpid); + get_remote_process_memory().init(message.mmalloc_default_mdp); break; } @@ -177,7 +56,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) region.fragment = message.fragment; region.address = message.address; region.size = message.size; - get_remote_process().ignore_heap(region); + get_remote_process_memory().ignore_heap(region); break; } @@ -185,7 +64,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) s_mc_message_ignore_memory_t message; xbt_assert(size == sizeof(message), "Broken message"); memcpy(&message, buffer, sizeof(message)); - get_remote_process().unignore_heap((void*)(std::uintptr_t)message.addr, message.size); + get_remote_process_memory().unignore_heap((void*)(std::uintptr_t)message.addr, message.size); break; } @@ -193,7 +72,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) s_mc_message_ignore_memory_t message; xbt_assert(size == sizeof(message), "Broken message"); memcpy(&message, buffer, sizeof(message)); - this->get_remote_process().ignore_region(message.addr, message.size); + this->get_remote_process_memory().ignore_region(message.addr, message.size); break; } @@ -201,7 +80,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) s_mc_message_stack_region_t message; xbt_assert(size == sizeof(message), "Broken message"); memcpy(&message, buffer, sizeof(message)); - this->get_remote_process().stack_areas().push_back(message.stack_region); + this->get_remote_process_memory().stack_areas().push_back(message.stack_region); } break; case MessageType::REGISTER_SYMBOL: { @@ -211,7 +90,8 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) xbt_assert(not message.callback, "Support for client-side function proposition is not implemented."); XBT_DEBUG("Received symbol: %s", message.name.data()); - LivenessChecker::automaton_register_symbol(get_remote_process(), message.name.data(), remote((int*)message.data)); + LivenessChecker::automaton_register_symbol(get_remote_process_memory(), message.name.data(), + remote((int*)message.data)); break; } @@ -219,18 +99,8 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) return false; case MessageType::ASSERTION_FAILED: - XBT_INFO("**************************"); - XBT_INFO("*** PROPERTY NOT VALID ***"); - XBT_INFO("**************************"); - XBT_INFO("Counter-example execution trace:"); - for (auto const& s : get_exploration()->get_textual_trace()) - XBT_INFO(" %s", s.c_str()); - XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with " - "--cfg=model-check/replay:'%s'", - get_exploration()->get_record_trace().to_string().c_str()); - exploration_->log_state(); - - this->exit(SIMGRID_MC_EXIT_SAFETY); + Exploration::get_instance()->report_assertion_failure(); + break; default: xbt_die("Unexpected message from model-checked application"); @@ -238,117 +108,4 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) return true; } -/** Terminate the model-checker application */ -void ModelChecker::exit(int status) -{ - shutdown(); - ::exit(status); -} - -void ModelChecker::handle_waitpid() -{ - XBT_DEBUG("Check for wait event"); - int status; - pid_t pid; - while ((pid = waitpid(-1, &status, WNOHANG)) != 0) { - if (pid == -1) { - if (errno == ECHILD) { - // No more children: - xbt_assert(not this->get_remote_process().running(), "Inconsistent state"); - break; - } else { - XBT_ERROR("Could not wait for pid"); - throw simgrid::xbt::errno_error(); - } - } - - if (pid == this->get_remote_process().pid()) { - // From PTRACE_O_TRACEEXIT: -#ifdef __linux__ - if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) { - unsigned long eventmsg; - xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &eventmsg) != -1, "Could not get exit status"); - status = static_cast(eventmsg); - if (WIFSIGNALED(status)) { - MC_report_crash(exploration_, status); - this->get_remote_process().terminate(); - this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); - } - } -#endif - - // We don't care about signals, just reinject them: - if (WIFSTOPPED(status)) { - XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status)); - errno = 0; -#ifdef __linux__ - ptrace(PTRACE_CONT, remote_process_->pid(), 0, WSTOPSIG(status)); -#elif defined BSD - ptrace(PT_CONTINUE, remote_process_->pid(), (caddr_t)1, WSTOPSIG(status)); -#endif - xbt_assert(errno == 0, "Could not PTRACE_CONT"); - } - - else if (WIFSIGNALED(status)) { - MC_report_crash(exploration_, status); - this->get_remote_process().terminate(); - this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); - } else if (WIFEXITED(status)) { - XBT_DEBUG("Child process is over"); - this->get_remote_process().terminate(); - } - } - } -} - -void ModelChecker::wait_for_requests() -{ - this->resume(); - if (this->get_remote_process().running()) - checker_side_.dispatch(); -} - -Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition) -{ - s_mc_message_simcall_execute_t m = {}; - m.type = MessageType::SIMCALL_EXECUTE; - m.aid_ = aid; - m.times_considered_ = times_considered; - checker_side_.get_channel().send(m); - - this->remote_process_->clear_cache(); - if (this->remote_process_->running()) - checker_side_.dispatch(); // The app may send messages while processing the transition - - s_mc_message_simcall_execute_answer_t answer; - ssize_t s = checker_side_.get_channel().receive(answer); - xbt_assert(s != -1, "Could not receive message"); - xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_EXECUTE_ANSWER, - "Received unexpected message %s (%i, size=%i) " - "expected MessageType::SIMCALL_EXECUTE_ANSWER (%i, size=%i)", - to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_EXECUTE_ANSWER, - (int)sizeof(answer)); - - if (new_transition) { - std::stringstream stream(answer.buffer.data()); - return deserialize_transition(aid, times_considered, stream); - } else - return nullptr; -} - -void ModelChecker::finalize_app(bool terminate_asap) -{ - s_mc_message_int_t m = {}; - m.type = MessageType::FINALIZE; - m.value = terminate_asap; - xbt_assert(checker_side_.get_channel().send(m) == 0, "Could not ask the app to finalize on need"); - - s_mc_message_t answer; - ssize_t s = checker_side_.get_channel().receive(answer); - xbt_assert(s != -1, "Could not receive answer to FINALIZE"); - xbt_assert(s == sizeof(answer) && answer.type == MessageType::FINALIZE_REPLY, - "Received unexpected message %s (%i, size=%i) expected MessageType::FINALIZE_REPLY (%i, size=%i)", - to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::FINALIZE_REPLY, (int)sizeof(answer)); -} - } // namespace simgrid::mc