, signal_event_(nullptr)
, page_store_(500)
, process_(std::move(process))
- , parent_snapshot_(nullptr)
{
}
void ModelChecker::start()
{
- const pid_t pid = process_->pid();
-
base_ = event_base_new();
event_callback_fn event_callback = [](evutil_socket_t fd, short events, void *arg)
{
int status;
// The model-checked process SIGSTOP itself to signal it's ready:
+ const pid_t pid = process_->pid();
+
pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS);
if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
xbt_die("Could not wait model-checked process");
XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
else if (WIFEXITED(status))
XBT_INFO("From exit: %i", WEXITSTATUS(status));
- if (WCOREDUMP(status))
- XBT_INFO("A core dump was generated by the system.");
- else
- XBT_INFO("No core dump was generated by the system.");
+ if (not xbt_log_no_loc)
+ XBT_INFO("%s core dump was generated by the system.", WCOREDUMP(status) ? "A" : "No");
XBT_INFO("Counter-example execution trace:");
for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
XBT_INFO(" %s", s.c_str());
simgrid::mc::dumpRecordPath();
simgrid::mc::session->log_state();
- XBT_INFO("Stack trace:");
- mc_model_checker->process().dump_stack();
+ 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->process().dump_stack();
+ }
}
static void MC_report_assertion_error()
bool ModelChecker::handle_message(char* buffer, ssize_t size)
{
s_mc_message_t base_message;
- if (size < (ssize_t) sizeof(base_message))
- xbt_die("Broken message");
+ xbt_assert(size >= (ssize_t)sizeof(base_message), "Broken message");
memcpy(&base_message, buffer, sizeof(base_message));
switch(base_message.type) {
case MC_MESSAGE_IGNORE_HEAP:
{
s_mc_message_ignore_heap_t message;
- if (size != sizeof(message))
- xbt_die("Broken messsage");
+ xbt_assert(size == sizeof(message), "Broken messsage");
memcpy(&message, buffer, sizeof(message));
IgnoredHeapRegion region;
case MC_MESSAGE_UNIGNORE_HEAP:
{
s_mc_message_ignore_memory_t message;
- if (size != sizeof(message))
- xbt_die("Broken messsage");
+ xbt_assert(size == sizeof(message), "Broken messsage");
memcpy(&message, buffer, sizeof(message));
process().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
break;
case MC_MESSAGE_IGNORE_MEMORY:
{
s_mc_message_ignore_memory_t message;
- if (size != sizeof(message))
- xbt_die("Broken messsage");
+ xbt_assert(size == sizeof(message), "Broken messsage");
memcpy(&message, buffer, sizeof(message));
this->process().ignore_region(message.addr, message.size);
break;
case MC_MESSAGE_STACK_REGION:
{
s_mc_message_stack_region_t message;
- if (size != sizeof(message))
- xbt_die("Broken messsage");
+ xbt_assert(size == sizeof(message), "Broken messsage");
memcpy(&message, buffer, sizeof(message));
this->process().stack_areas().push_back(message.stack_region);
}
case MC_MESSAGE_REGISTER_SYMBOL:
{
s_mc_message_register_symbol_t message;
- if (size != sizeof(message))
- xbt_die("Broken message");
+ xbt_assert(size == sizeof(message), "Broken message");
memcpy(&message, buffer, sizeof(message));
- if (message.callback)
- xbt_die("Support for client-side function proposition is not implemented.");
+ xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
XBT_DEBUG("Received symbol: %s", message.name);
if (simgrid::mc::property_automaton == nullptr)
if (pid == -1) {
if (errno == ECHILD) {
// No more children:
- if (this->process().running())
- xbt_die("Inconsistent state");
- else
- break;
+ xbt_assert(not this->process().running(), "Inconsistent state");
+ break;
} else {
XBT_ERROR("Could not wait for pid");
throw simgrid::xbt::errno_error();
// From PTRACE_O_TRACEEXIT:
#ifdef __linux__
if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
- if (ptrace(PTRACE_GETEVENTMSG, this->process().pid(), 0, &status) == -1)
- xbt_die("Could not get exit status");
+ xbt_assert(ptrace(PTRACE_GETEVENTMSG, this->process().pid(), 0, &status) != -1, "Could not get exit status");
if (WIFSIGNALED(status)) {
MC_report_crash(status);
mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
#elif defined BSD
ptrace(PT_CONTINUE, this->process().pid(), (caddr_t)1, WSTOPSIG(status));
#endif
- if (errno != 0)
- xbt_die("Could not PTRACE_CONT");
+ xbt_assert(errno == 0, "Could not PTRACE_CONT");
}
- else if (WIFEXITED(status) || WIFSIGNALED(status)) {
+ else if (WIFSIGNALED(status)) {
+ MC_report_crash(status);
+ mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+ } else if (WIFEXITED(status)) {
XBT_DEBUG("Child process is over");
this->process().terminate();
}
s_mc_message_simcall_handle_t m;
memset(&m, 0, sizeof(m));
m.type = MC_MESSAGE_SIMCALL_HANDLE;
- m.pid = transition.pid;
- m.value = transition.argument;
+ m.pid = transition.pid_;
+ m.value = transition.argument_;
this->process_->get_channel().send(m);
this->process_->clear_cache();
if (this->process_->running())
bool ModelChecker::checkDeadlock()
{
- int res;
- if ((res = this->process().get_channel().send(MC_MESSAGE_DEADLOCK_CHECK)))
- xbt_die("Could not check deadlock state");
+ int res = this->process().get_channel().send(MC_MESSAGE_DEADLOCK_CHECK);
+ xbt_assert(res == 0, "Could not check deadlock state");
s_mc_message_int_t message;
ssize_t s = mc_model_checker->process().get_channel().receive(message);
- if (s == -1)
- xbt_die("Could not receive message");
- if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
- xbt_die("Received unexpected message %s (%i, size=%i) "
- "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
- MC_message_type_name(message.type), (int) message.type, (int) s,
- (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
- );
+ xbt_assert(s != -1, "Could not receive message");
+ xbt_assert(s == sizeof(message) && message.type == MC_MESSAGE_DEADLOCK_CHECK_REPLY,
+ "Received unexpected message %s (%i, size=%i) "
+ "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
+ MC_message_type_name(message.type), (int)message.type, (int)s, (int)MC_MESSAGE_DEADLOCK_CHECK_REPLY,
+ (int)sizeof(message));
return message.value != 0;
}
