src/mc/ModelChecker.cpp

   1 /* Copyright (c) 2008-2019. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "src/mc/ModelChecker.hpp"
   7 #include "src/mc/Session.hpp"
   8 #include "src/mc/Transition.hpp"
   9 #include "src/mc/checker/Checker.hpp"
  10 #include "src/mc/mc_config.hpp"
  11 #include "src/mc/mc_exit.hpp"
  12 #include "src/mc/mc_private.hpp"
  13 #include "src/mc/remote/RemoteClient.hpp"
  14 #include "xbt/automaton.hpp"
  15 #include "xbt/system_error.hpp"
  16
  17 #include <sys/ptrace.h>
  18 #include <sys/wait.h>
  19
  20 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
  21
  22 ::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
  23
  24 using simgrid::mc::remote;
  25
  26 #ifdef __linux__
  27 # define WAITPID_CHECKED_FLAGS __WALL
  28 #else
  29 # define WAITPID_CHECKED_FLAGS 0
  30 #endif
  31
  32 namespace simgrid {
  33 namespace mc {
  34
  35 ModelChecker::ModelChecker(std::unique_ptr<RemoteClient> process)
  36     : base_(nullptr)
  37     , socket_event_(nullptr)
  38     , signal_event_(nullptr)
  39     , page_store_(500)
  40     , process_(std::move(process))
  41     , parent_snapshot_(nullptr)
  42 {
  43
  44 }
  45
  46 ModelChecker::~ModelChecker() {
  47   if (socket_event_ != nullptr)
  48     event_free(socket_event_);
  49   if (signal_event_ != nullptr)
  50     event_free(signal_event_);
  51   if (base_ != nullptr)
  52     event_base_free(base_);
  53 }
  54
  55 void ModelChecker::start()
  56 {
  57   const pid_t pid = process_->pid();
  58
  59   base_ = event_base_new();
  60   event_callback_fn event_callback = [](evutil_socket_t fd, short events, void *arg)
  61   {
  62     ((ModelChecker *)arg)->handle_events(fd, events);
  63   };
  64   socket_event_ = event_new(base_, process_->get_channel().get_socket(), EV_READ | EV_PERSIST, event_callback, this);
  65   event_add(socket_event_, NULL);
  66   signal_event_ = event_new(base_,
  67                             SIGCHLD,
  68                             EV_SIGNAL|EV_PERSIST,
  69                             event_callback, this);
  70   event_add(signal_event_, NULL);
  71
  72   XBT_DEBUG("Waiting for the model-checked process");
  73   int status;
  74
  75   // The model-checked process SIGSTOP itself to signal it's ready:
  76   pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS);
  77   if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
  78     xbt_die("Could not wait model-checked process");
  79
  80   process_->init();
  81
  82   if (not _sg_mc_dot_output_file.get().empty())
  83     MC_init_dot_output();
  84
  85   setup_ignore();
  86
  87 #ifdef __linux__
  88   ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
  89   ptrace(PTRACE_CONT, pid, 0, 0);
  90 #elif defined BSD
  91   ptrace(PT_CONTINUE, pid, (caddr_t)1, 0);
  92 #else
  93 # error "no ptrace equivalent coded for this platform"
  94 #endif
  95 }
  96
  97 static const std::pair<const char*, const char*> ignored_local_variables[] = {
  98   std::pair<const char*, const char*>{  "e", "*" },
  99   std::pair<const char*, const char*>{ "_log_ev", "*" },
 100
 101   /* Ignore local variable about time used for tracing */
 102   std::pair<const char*, const char*>{ "start_time", "*" },
 103 };
 104
 105 void ModelChecker::setup_ignore()
 106 {
 107   RemoteClient& process = this->process();
 108   for (std::pair<const char*, const char*> const& var :
 109       ignored_local_variables)
 110     process.ignore_local_variable(var.first, var.second);
 111
 112   /* Static variable used for tracing */
 113   process.ignore_global_variable("counter");
 114 }
 115
 116 void ModelChecker::shutdown()
 117 {
 118   XBT_DEBUG("Shuting down model-checker");
 119
 120   simgrid::mc::RemoteClient* process = &this->process();
 121   if (process->running()) {
 122     XBT_DEBUG("Killing process");
 123     kill(process->pid(), SIGKILL);
 124     process->terminate();
 125   }
 126 }
 127
 128 void ModelChecker::resume(simgrid::mc::RemoteClient& process)
 129 {
 130   int res = process.get_channel().send(MC_MESSAGE_CONTINUE);
 131   if (res)
 132     throw simgrid::xbt::errno_error();
 133   process.clear_cache();
 134 }
 135
 136 static void MC_report_crash(int status)
 137 {
 138   XBT_INFO("**************************");
 139   XBT_INFO("** CRASH IN THE PROGRAM **");
 140   XBT_INFO("**************************");
 141   if (WIFSIGNALED(status))
 142     XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
 143   else if (WIFEXITED(status))
 144     XBT_INFO("From exit: %i", WEXITSTATUS(status));
 145   if (WCOREDUMP(status))
 146     XBT_INFO("A core dump was generated by the system.");
 147   else
 148     XBT_INFO("No core dump was generated by the system.");
 149   XBT_INFO("Counter-example execution trace:");
 150   for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
 151     XBT_INFO("  %s", s.c_str());
 152   simgrid::mc::dumpRecordPath();
 153   simgrid::mc::session->log_state();
 154   XBT_INFO("Stack trace:");
 155   mc_model_checker->process().dump_stack();
 156 }
 157
 158 static void MC_report_assertion_error()
 159 {
 160   XBT_INFO("**************************");
 161   XBT_INFO("*** PROPERTY NOT VALID ***");
 162   XBT_INFO("**************************");
 163   XBT_INFO("Counter-example execution trace:");
 164   for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
 165     XBT_INFO("  %s", s.c_str());
 166   simgrid::mc::dumpRecordPath();
 167   simgrid::mc::session->log_state();
 168 }
 169
 170 bool ModelChecker::handle_message(char* buffer, ssize_t size)
 171 {
 172   s_mc_message_t base_message;
 173   if (size < (ssize_t) sizeof(base_message))
 174     xbt_die("Broken message");
 175   memcpy(&base_message, buffer, sizeof(base_message));
 176
 177   switch(base_message.type) {
 178
 179   case MC_MESSAGE_IGNORE_HEAP:
 180     {
 181     s_mc_message_ignore_heap_t message;
 182     if (size != sizeof(message))
 183       xbt_die("Broken messsage");
 184     memcpy(&message, buffer, sizeof(message));
 185
 186     IgnoredHeapRegion region;
 187     region.block    = message.block;
 188     region.fragment = message.fragment;
 189     region.address  = message.address;
 190     region.size     = message.size;
 191     process().ignore_heap(region);
 192     break;
 193     }
 194
 195   case MC_MESSAGE_UNIGNORE_HEAP:
 196     {
 197     s_mc_message_ignore_memory_t message;
 198     if (size != sizeof(message))
 199       xbt_die("Broken messsage");
 200     memcpy(&message, buffer, sizeof(message));
 201     process().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
 202     break;
 203     }
 204
 205   case MC_MESSAGE_IGNORE_MEMORY:
 206     {
 207     s_mc_message_ignore_memory_t message;
 208     if (size != sizeof(message))
 209       xbt_die("Broken messsage");
 210     memcpy(&message, buffer, sizeof(message));
 211     this->process().ignore_region(message.addr, message.size);
 212     break;
 213     }
 214
 215   case MC_MESSAGE_STACK_REGION:
 216     {
 217     s_mc_message_stack_region_t message;
 218     if (size != sizeof(message))
 219       xbt_die("Broken messsage");
 220     memcpy(&message, buffer, sizeof(message));
 221     this->process().stack_areas().push_back(message.stack_region);
 222     }
 223     break;
 224
 225   case MC_MESSAGE_REGISTER_SYMBOL:
 226     {
 227     s_mc_message_register_symbol_t message;
 228     if (size != sizeof(message))
 229       xbt_die("Broken message");
 230     memcpy(&message, buffer, sizeof(message));
 231     if (message.callback)
 232       xbt_die("Support for client-side function proposition is not implemented.");
 233     XBT_DEBUG("Received symbol: %s", message.name);
 234
 235     if (simgrid::mc::property_automaton == nullptr)
 236       simgrid::mc::property_automaton = xbt_automaton_new();
 237
 238     simgrid::mc::RemoteClient* process  = &this->process();
 239     simgrid::mc::RemotePtr<int> address = simgrid::mc::remote((int*)message.data);
 240     simgrid::xbt::add_proposition(simgrid::mc::property_automaton, message.name,
 241                                   [process, address]() { return process->read(address); });
 242
 243     break;
 244     }
 245
 246   case MC_MESSAGE_WAITING:
 247     return false;
 248
 249   case MC_MESSAGE_ASSERTION_FAILED:
 250     MC_report_assertion_error();
 251     this->exit(SIMGRID_MC_EXIT_SAFETY);
 252
 253   default:
 254     xbt_die("Unexpected message from model-checked application");
 255
 256   }
 257   return true;
 258 }
 259
 260 /** Terminate the model-checker application */
 261 void ModelChecker::exit(int status)
 262 {
 263   // TODO, terminate the model checker politely instead of exiting rudely
 264   if (process().running())
 265     kill(process().pid(), SIGKILL);
 266   ::exit(status);
 267 }
 268
 269 void ModelChecker::handle_events(int fd, short events)
 270 {
 271   if (events == EV_READ) {
 272     char buffer[MC_MESSAGE_LENGTH];
 273     ssize_t size = process_->get_channel().receive(buffer, sizeof(buffer), false);
 274     if (size == -1 && errno != EAGAIN)
 275       throw simgrid::xbt::errno_error();
 276     if (not handle_message(buffer, size)) {
 277       event_base_loopbreak(base_);
 278     }
 279   }
 280   else if (events == EV_SIGNAL) {
 281     on_signal(fd);
 282   }
 283   else {
 284     xbt_die("Unexpected event");
 285   }
 286 }
 287
 288 void ModelChecker::loop()
 289 {
 290   if (this->process().running())
 291     event_base_dispatch(base_);
 292 }
 293
 294 void ModelChecker::handle_waitpid()
 295 {
 296   XBT_DEBUG("Check for wait event");
 297   int status;
 298   pid_t pid;
 299   while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
 300     if (pid == -1) {
 301       if (errno == ECHILD) {
 302         // No more children:
 303         if (this->process().running())
 304           xbt_die("Inconsistent state");
 305         else
 306           break;
 307       } else {
 308         XBT_ERROR("Could not wait for pid");
 309         throw simgrid::xbt::errno_error();
 310       }
 311     }
 312
 313     if (pid == this->process().pid()) {
 314
 315       // From PTRACE_O_TRACEEXIT:
 316 #ifdef __linux__
 317       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
 318         if (ptrace(PTRACE_GETEVENTMSG, this->process().pid(), 0, &status) == -1)
 319           xbt_die("Could not get exit status");
 320         if (WIFSIGNALED(status)) {
 321           MC_report_crash(status);
 322           mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
 323         }
 324       }
 325 #endif
 326
 327       // We don't care about signals, just reinject them:
 328       if (WIFSTOPPED(status)) {
 329         XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
 330         errno = 0;
 331 #ifdef __linux__
 332         ptrace(PTRACE_CONT, this->process().pid(), 0, WSTOPSIG(status));
 333 #elif defined BSD
 334         ptrace(PT_CONTINUE, this->process().pid(), (caddr_t)1, WSTOPSIG(status));
 335 #endif
 336         if (errno != 0)
 337           xbt_die("Could not PTRACE_CONT");
 338       }
 339
 340       else if (WIFEXITED(status) || WIFSIGNALED(status)) {
 341         XBT_DEBUG("Child process is over");
 342         this->process().terminate();
 343       }
 344     }
 345   }
 346 }
 347
 348 void ModelChecker::on_signal(int signo)
 349 {
 350   if (signo == SIGCHLD)
 351     this->handle_waitpid();
 352 }
 353
 354 void ModelChecker::wait_for_requests()
 355 {
 356   this->resume(process());
 357   if (this->process().running())
 358     event_base_dispatch(base_);
 359 }
 360
 361 void ModelChecker::handle_simcall(Transition const& transition)
 362 {
 363   s_mc_message_simcall_handle_t m;
 364   memset(&m, 0, sizeof(m));
 365   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
 366   m.pid   = transition.pid;
 367   m.value = transition.argument;
 368   this->process_->get_channel().send(m);
 369   this->process_->clear_cache();
 370   if (this->process_->running())
 371     event_base_dispatch(base_);
 372 }
 373
 374 bool ModelChecker::checkDeadlock()
 375 {
 376   int res;
 377   if ((res = this->process().get_channel().send(MC_MESSAGE_DEADLOCK_CHECK)))
 378     xbt_die("Could not check deadlock state");
 379   s_mc_message_int_t message;
 380   ssize_t s = mc_model_checker->process().get_channel().receive(message);
 381   if (s == -1)
 382     xbt_die("Could not receive message");
 383   if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)
 384     xbt_die("Received unexpected message %s (%i, size=%i) "
 385       "expected MC_MESSAGE_DEADLOCK_CHECK_REPLY (%i, size=%i)",
 386       MC_message_type_name(message.type), (int) message.type, (int) s,
 387       (int) MC_MESSAGE_DEADLOCK_CHECK_REPLY, (int) sizeof(message)
 388       );
 389   return message.value != 0;
 390 }
 391
 392 }
 393 }