X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/9ec4c698631ec44c39b691c6eef8e847379e2e66..5a567ca84bc683ed919ed447667bf525cc21552d:/src/mc/ModelChecker.cpp diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index fe5d743d15..051a8462d8 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -1,10 +1,11 @@ -/* 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. */ #include "src/mc/ModelChecker.hpp" #include "src/mc/explo/Exploration.hpp" +#include "src/mc/explo/LivenessChecker.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_private.hpp" @@ -66,8 +67,13 @@ void ModelChecker::start() 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()) - MC_init_dot_output(); + 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(); @@ -87,6 +93,16 @@ 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", "*"), @@ -125,7 +141,7 @@ void ModelChecker::resume() remote_process_->clear_cache(); } -static void MC_report_crash(int status) +static void MC_report_crash(Exploration* explorer, int status) { XBT_INFO("**************************"); XBT_INFO("** CRASH IN THE PROGRAM **"); @@ -136,12 +152,14 @@ static void MC_report_crash(int 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 (mc_model_checker->get_exploration()) { + if (explorer) { XBT_INFO("Counter-example execution trace:"); - for (auto const& s : mc_model_checker->get_exploration()->get_textual_trace()) + for (auto const& s : explorer->get_textual_trace()) XBT_INFO(" %s", s.c_str()); - XBT_INFO("Path = %s", mc_model_checker->get_exploration()->get_record_trace().to_string().c_str()); - Api::get().get_session().log_state(); + 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 { @@ -211,14 +229,7 @@ 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()); - if (property_automaton == nullptr) - property_automaton = xbt_automaton_new(); - - const RemoteProcess* process = &this->get_remote_process(); - RemotePtr address = remote((int*)message.data); - xbt::add_proposition(property_automaton, message.name.data(), - [process, address]() { return process->read(address); }); - + LivenessChecker::automaton_register_symbol(get_remote_process(), message.name.data(), remote((int*)message.data)); break; } @@ -232,8 +243,10 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) 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()); - Api::get().get_session().log_state(); + 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); @@ -271,9 +284,11 @@ void ModelChecker::handle_waitpid() // 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"); + 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(status); + MC_report_crash(exploration_, status); this->get_remote_process().terminate(); this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); } @@ -293,7 +308,7 @@ void ModelChecker::handle_waitpid() } else if (WIFSIGNALED(status)) { - MC_report_crash(status); + MC_report_crash(exploration_, status); this->get_remote_process().terminate(); this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); } else if (WIFEXITED(status)) { @@ -313,8 +328,7 @@ void ModelChecker::wait_for_requests() 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; @@ -342,8 +356,7 @@ Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool n void ModelChecker::finalize_app(bool terminate_asap) { - s_mc_message_int_t m; - memset(&m, 0, sizeof m); + 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");