namespace simgrid {
namespace mc {
-ModelChecker::ModelChecker(std::unique_ptr<RemoteClient> process)
- : base_(nullptr)
- , socket_event_(nullptr)
- , signal_event_(nullptr)
- , page_store_(500)
- , process_(std::move(process))
-{
-
-}
+ModelChecker::ModelChecker(std::unique_ptr<RemoteClient> process) : process_(std::move(process)) {}
-ModelChecker::~ModelChecker() {
+ModelChecker::~ModelChecker()
+{
if (socket_event_ != nullptr)
event_free(socket_event_);
if (signal_event_ != nullptr)
{
XBT_DEBUG("Shuting down model-checker");
- simgrid::mc::RemoteClient* process = &this->process();
+ RemoteClient* process = &this->process();
if (process->running()) {
XBT_DEBUG("Killing process");
kill(process->pid(), SIGKILL);
}
}
-void ModelChecker::resume(simgrid::mc::RemoteClient& process)
+void ModelChecker::resume(RemoteClient& process)
{
int res = process.get_channel().send(MC_MESSAGE_CONTINUE);
if (res)
- throw simgrid::xbt::errno_error();
+ throw xbt::errno_error();
process.clear_cache();
}
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();
+ dumpRecordPath();
+ session->log_state();
if (xbt_log_no_loc) {
XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
} else {
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();
+ dumpRecordPath();
+ session->log_state();
}
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)
- simgrid::mc::property_automaton = xbt_automaton_new();
+ if (property_automaton == nullptr)
+ property_automaton = xbt_automaton_new();
- simgrid::mc::RemoteClient* process = &this->process();
- simgrid::mc::RemotePtr<int> address = simgrid::mc::remote((int*)message.data);
- simgrid::xbt::add_proposition(simgrid::mc::property_automaton, message.name,
- [process, address]() { return process->read(address); });
+ RemoteClient* process = &this->process();
+ RemotePtr<int> address = remote((int*)message.data);
+ xbt::add_proposition(property_automaton, message.name, [process, address]() { return process->read(address); });
break;
}
default:
xbt_die("Unexpected message from model-checked application");
-
}
return true;
}
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();
}
if (pid == this->process().pid()) {
-
// 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 (WIFSIGNALED(status)) {
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;
}
-}
-}
+} // namespace mc
+} // namespace simgrid
