#include "simgrid/sg_config.h"
-#include "ModelChecker.hpp"
-#include "PageStore.hpp"
-#include "ModelChecker.hpp"
-#include "mc_protocol.h"
-#include "mc_private.h"
-#include "mc_ignore.h"
-#include "mcer_ignore.h"
-#include "mc_exit.h"
+#include "src/mc/ModelChecker.hpp"
+#include "src/mc/PageStore.hpp"
+#include "src/mc/ModelChecker.hpp"
+#include "src/mc/mc_protocol.h"
+#include "src/mc/mc_private.h"
+#include "src/mc/mc_ignore.h"
+#include "src/mc/mc_exit.h"
#include "src/mc/mc_liveness.h"
extern "C" {
namespace simgrid {
namespace mc {
-ModelChecker::ModelChecker(pid_t pid, int socket) :
- pid_(pid), socket_(socket),
+ModelChecker::ModelChecker(std::unique_ptr<Process> process) :
hostnames_(xbt_dict_new()),
page_store_(500),
+ process_(std::move(process)),
parent_snapshot_(nullptr)
{
+
}
ModelChecker::~ModelChecker()
void ModelChecker::start()
{
+ const pid_t pid = process_->pid();
+
// Block SIGCHLD (this will be handled with accept/signalfd):
sigset_t set;
sigemptyset(&set);
// Prepare data for poll:
struct pollfd* socket_pollfd = &fds_[SOCKET_FD_INDEX];
- socket_pollfd->fd = socket_;
+ socket_pollfd->fd = process_->socket();;
socket_pollfd->events = POLLIN;
socket_pollfd->revents = 0;
int status;
// The model-checked process SIGSTOP itself to signal it's ready:
- pid_t res = waitpid(pid_, &status, __WALL);
+ pid_t res = waitpid(pid, &status, __WALL);
if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
xbt_die("Could not wait model-checked process");
- assert(process_ == nullptr);
- process_ = std::unique_ptr<Process>(new Process(pid_, socket_));
- // TODO, avoid direct dependency on sg_cfg
- process_->privatized(sg_cfg_get_boolean("smpi/privatize_global_variables"));
+ process_->init();
/* Initialize statistics */
mc_stats = xbt_new0(s_mc_stats_t, 1);
setup_ignore();
- ptrace(PTRACE_SETOPTIONS, pid_, nullptr, PTRACE_O_TRACEEXIT);
- ptrace(PTRACE_CONT, pid_, 0, 0);
+ ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
+ ptrace(PTRACE_CONT, pid, 0, 0);
}
-void ModelChecker::setup_ignore()
-{
- /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
- MC_ignore_local_variable("e", "*");
- MC_ignore_local_variable("__ex_cleanup", "*");
- MC_ignore_local_variable("__ex_mctx_en", "*");
- MC_ignore_local_variable("__ex_mctx_me", "*");
- MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
- MC_ignore_local_variable("_log_ev", "*");
- MC_ignore_local_variable("_throw_ctx", "*");
- MC_ignore_local_variable("ctx", "*");
-
- MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
- MC_ignore_local_variable("next_cont"
- "ext", "smx_ctx_sysv_suspend_serial");
- MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
+static const std::pair<const char*, const char*> ignored_local_variables[] = {
+ std::pair<const char*, const char*>{ "e", "*" },
+ std::pair<const char*, const char*>{ "__ex_cleanup", "*" },
+ std::pair<const char*, const char*>{ "__ex_mctx_en", "*" },
+ std::pair<const char*, const char*>{ "__ex_mctx_me", "*" },
+ std::pair<const char*, const char*>{ "__xbt_ex_ctx_ptr", "*" },
+ std::pair<const char*, const char*>{ "_log_ev", "*" },
+ std::pair<const char*, const char*>{ "_throw_ctx", "*" },
+ std::pair<const char*, const char*>{ "ctx", "*" },
+
+ std::pair<const char*, const char*>{ "self", "simcall_BODY_mc_snapshot" },
+ std::pair<const char*, const char*>{ "next_context", "smx_ctx_sysv_suspend_serial" },
+ std::pair<const char*, const char*>{ "i", "smx_ctx_sysv_suspend_serial" },
/* Ignore local variable about time used for tracing */
- MC_ignore_local_variable("start_time", "*");
+ std::pair<const char*, const char*>{ "start_time", "*" },
+};
+
+void ModelChecker::setup_ignore()
+{
+ Process& process = this->process();
+ for (std::pair<const char*, const char*> const& var :
+ ignored_local_variables)
+ process.ignore_local_variable(var.first, var.second);
/* Static variable used for tracing */
- this->process().ignore_global_variable("counter");
+ process.ignore_global_variable("counter");
/* SIMIX */
- this->process().ignore_global_variable("smx_total_comms");
+ process.ignore_global_variable("smx_total_comms");
}
void ModelChecker::shutdown()
if (size != sizeof(message))
xbt_die("Broken messsage");
memcpy(&message, buffer, sizeof(message));
- mc_heap_ignore_region_t region = xbt_new(s_mc_heap_ignore_region_t, 1);
- *region = message.region;
- MC_heap_region_ignore_insert(region);
+
+ IgnoredHeapRegion region;
+ region.block = message.block;
+ region.fragment = message.fragment;
+ region.address = message.address;
+ region.size = message.size;
+ process().ignore_heap(region);
break;
}
if (size != sizeof(message))
xbt_die("Broken messsage");
memcpy(&message, buffer, sizeof(message));
- MC_heap_region_ignore_remove(
+ process().unignore_heap(
(void *)(std::uintptr_t) message.addr, message.size);
break;
}
// From PTRACE_O_TRACEEXIT:
if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
- if (ptrace(PTRACE_GETEVENTMSG, pid_, 0, &status) == -1)
+ if (ptrace(PTRACE_GETEVENTMSG, this->process().pid(), 0, &status) == -1)
xbt_die("Could not get exit status");
if (WIFSIGNALED(status)) {
MC_report_crash(status);
// We don't care about signals, just reinject them:
if (WIFSTOPPED(status)) {
XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
- if (ptrace(PTRACE_CONT, pid_, 0, WSTOPSIG(status)) == -1)
+ if (ptrace(PTRACE_CONT, this->process().pid(), 0, WSTOPSIG(status)) == -1)
xbt_die("Could not PTRACE_CONT");
}
