* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/ModelChecker.hpp"
-#include "src/mc/Session.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"
::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
-using simgrid::mc::remote;
-
#ifdef __linux__
# define WAITPID_CHECKED_FLAGS __WALL
#else
# define WAITPID_CHECKED_FLAGS 0
#endif
-namespace simgrid {
-namespace mc {
+namespace simgrid::mc {
ModelChecker::ModelChecker(std::unique_ptr<RemoteProcess> remote_simulation, int sockfd)
: checker_side_(sockfd), remote_process_(std::move(remote_simulation))
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();
+ errno = 0;
#ifdef __linux__
ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
ptrace(PTRACE_CONT, pid, 0, 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);
+}
+
+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 = {
void ModelChecker::setup_ignore()
{
const RemoteProcess& process = this->get_remote_process();
- for (auto const& var : ignored_local_variables)
- process.ignore_local_variable(var.first, var.second);
+ 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::resume()
{
- int res = checker_side_.get_channel().send(MessageType::CONTINUE);
- if (res)
+ if (checker_side_.get_channel().send(MessageType::CONTINUE) != 0)
throw xbt::errno_error();
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 **");
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());
- session_singleton->log_state();
+ 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_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, message.actors, message.dead_actors);
+ get_remote_process().init(message.mmalloc_default_mdp, message.maxpid);
break;
}
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<int> 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;
}
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());
- session_singleton->log_state();
+ exploration_->log_state();
this->exit(SIMGRID_MC_EXIT_SAFETY);
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(status);
+ MC_report_crash(exploration_, status);
this->get_remote_process().terminate();
this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
}
}
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)) {
xbt_assert(checker_side_.get_channel().send(m) == 0, "Could not ask the app to finalize on need");
s_mc_message_t answer;
- xbt_assert(checker_side_.get_channel().receive(answer) != -1, "Could not receive answer to FINALIZE");
+ 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 mc
-} // namespace simgrid
+} // namespace simgrid::mc
