X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/18f3ec7b57418d4881c22646dfbb991ac6f9b7a7..28b9e83a90c238b71d27f5cb3c6596906a3d4641:/src/mc/ModelChecker.cpp diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 17e2bce738..10f0ba30c6 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2008-2022. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2023. 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. */ @@ -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" @@ -31,8 +31,8 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker"); namespace simgrid::mc { -ModelChecker::ModelChecker(std::unique_ptr remote_simulation, int sockfd) - : checker_side_(sockfd), remote_process_(std::move(remote_simulation)) +ModelChecker::ModelChecker(std::unique_ptr remote_memory, int sockfd) + : checker_side_(sockfd), remote_process_memory_(std::move(remote_memory)) { } @@ -52,6 +52,8 @@ void ModelChecker::start() } else if (events == EV_SIGNAL) { if (sig == SIGCHLD) mc->handle_waitpid(); + else + xbt_die("Unexpected signal: %d", sig); } else { xbt_die("Unexpected event"); } @@ -62,21 +64,11 @@ void ModelChecker::start() int status; // The model-checked process SIGSTOP itself to signal it's ready: - const pid_t pid = remote_process_->pid(); + const pid_t pid = remote_process_memory_->pid(); xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP, "Could not wait model-checked process"); - if (not _sg_mc_dot_output_file.get().empty()) { - dot_output_ = fopen(_sg_mc_dot_output_file.get().c_str(), "w"); - xbt_assert(dot_output_ != nullptr, "Error open dot output file: %s", strerror(errno)); - - fprintf(dot_output_, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node " - "[fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n"); - } - - setup_ignore(); - errno = 0; #ifdef __linux__ ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT); @@ -93,80 +85,6 @@ void ModelChecker::start() errno); } -void ModelChecker::dot_output(const char* fmt, ...) -{ - if (dot_output_ != nullptr) { - va_list ap; - va_start(ap, fmt); - vfprintf(dot_output_, fmt, ap); - va_end(ap); - } -} - -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() -{ - 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("Path = %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) { s_mc_message_t base_message; @@ -179,7 +97,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; } @@ -193,7 +111,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; } @@ -201,7 +119,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; } @@ -209,7 +127,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; } @@ -217,7 +135,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: { @@ -227,7 +145,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; } @@ -235,16 +154,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("Path = %s", get_exploration()->get_record_trace().to_string().c_str()); - exploration_->log_state(); - - this->exit(SIMGRID_MC_EXIT_SAFETY); + exploration_->report_assertion_failure(); + break; default: xbt_die("Unexpected message from model-checked application"); @@ -252,13 +163,6 @@ 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"); @@ -268,7 +172,7 @@ void ModelChecker::handle_waitpid() if (pid == -1) { if (errno == ECHILD) { // No more children: - xbt_assert(not this->get_remote_process().running(), "Inconsistent state"); + xbt_assert(not this->get_remote_process_memory().running(), "Inconsistent state"); break; } else { XBT_ERROR("Could not wait for pid"); @@ -276,71 +180,60 @@ void ModelChecker::handle_waitpid() } } - if (pid == this->get_remote_process().pid()) { + if (pid == this->get_remote_process_memory().pid()) { // From PTRACE_O_TRACEEXIT: #ifdef __linux__ if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) { - xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &status) != -1, "Could not get exit status"); - if (WIFSIGNALED(status)) { - MC_report_crash(exploration_, status); - this->get_remote_process().terminate(); - this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); - } + unsigned long eventmsg; + xbt_assert(ptrace(PTRACE_GETEVENTMSG, get_remote_process_memory().pid(), 0, &eventmsg) != -1, + "Could not get exit status"); + status = static_cast(eventmsg); + if (WIFSIGNALED(status)) + exploration_->report_crash(status); } #endif - // We don't care about signals, just reinject them: + // We don't care about non-lethal 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)); + ptrace(PTRACE_CONT, get_remote_process_memory().pid(), 0, WSTOPSIG(status)); #elif defined BSD - ptrace(PT_CONTINUE, remote_process_->pid(), (caddr_t)1, WSTOPSIG(status)); + ptrace(PT_CONTINUE, get_remote_process_memory().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); + exploration_->report_crash(status); } else if (WIFEXITED(status)) { XBT_DEBUG("Child process is over"); - this->get_remote_process().terminate(); + this->get_remote_process_memory().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; - memset(&m, 0, sizeof(m)); + 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()) + this->remote_process_memory_->clear_cache(); + if (this->remote_process_memory_->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)); + xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer); + xbt_assert(answer.type == MessageType::SIMCALL_EXECUTE_ANSWER, + "Received unexpected message %s (%i); expected MessageType::SIMCALL_EXECUTE_ANSWER (%i)", + to_c_str(answer.type), (int)answer.type, (int)MessageType::SIMCALL_EXECUTE_ANSWER); if (new_transition) { std::stringstream stream(answer.buffer.data()); @@ -349,20 +242,4 @@ Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool n return nullptr; } -void ModelChecker::finalize_app(bool terminate_asap) -{ - s_mc_message_int_t m; - memset(&m, 0, sizeof 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