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);
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 RemoteProcessMemory& process = this->get_remote_process_memory();
- 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()
-{
- if (checker_side_.get_channel().send(MessageType::CONTINUE) != 0)
- throw xbt::errno_error();
- remote_process_memory_->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:");
- explorer->get_remote_app().get_remote_process_memory().dump_stack();
- }
- }
-}
-
bool ModelChecker::handle_message(const char* buffer, ssize_t size)
{
s_mc_message_t base_message;
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_->report_assertion_failure();
+ break;
default:
xbt_die("Unexpected message from model-checked application");
return true;
}
-/** Terminate the model-checker application */
-void ModelChecker::exit(int status)
-{
- get_exploration()->get_remote_app().shutdown();
- ::exit(status);
-}
-
void ModelChecker::handle_waitpid()
{
XBT_DEBUG("Check for wait event");
xbt_assert(ptrace(PTRACE_GETEVENTMSG, get_remote_process_memory().pid(), 0, &eventmsg) != -1,
"Could not get exit status");
status = static_cast<int>(eventmsg);
- if (WIFSIGNALED(status)) {
- MC_report_crash(exploration_, status);
- this->get_remote_process_memory().terminate();
- this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
- }
+ if (WIFSIGNALED(status))
+ exploration_->report_crash(status);
}
#endif
}
else if (WIFSIGNALED(status)) {
- MC_report_crash(exploration_, status);
- this->get_remote_process_memory().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_memory().terminate();
}
}
-void ModelChecker::wait_for_requests()
-{
- this->resume();
- if (this->get_remote_process_memory().running())
- checker_side_.dispatch();
-}
-
Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition)
{
s_mc_message_simcall_execute_t m = {};