1 /* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
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. */
6 #include "src/mc/ModelChecker.hpp"
7 #include "src/mc/explo/Exploration.hpp"
8 #include "src/mc/explo/LivenessChecker.hpp"
9 #include "src/mc/mc_config.hpp"
10 #include "src/mc/mc_exit.hpp"
11 #include "src/mc/mc_private.hpp"
12 #include "src/mc/sosp/RemoteProcessMemory.hpp"
13 #include "src/mc/transition/TransitionComm.hpp"
14 #include "xbt/automaton.hpp"
15 #include "xbt/system_error.hpp"
19 #include <sys/ptrace.h>
22 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
24 ::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
27 # define WAITPID_CHECKED_FLAGS __WALL
29 # define WAITPID_CHECKED_FLAGS 0
32 namespace simgrid::mc {
34 ModelChecker::ModelChecker(std::unique_ptr<RemoteProcessMemory> remote_memory, int sockfd)
35 : checker_side_(sockfd), remote_process_memory_(std::move(remote_memory))
39 void ModelChecker::start()
42 [](evutil_socket_t sig, short events, void* arg) {
43 auto mc = static_cast<simgrid::mc::ModelChecker*>(arg);
44 if (events == EV_READ) {
45 std::array<char, MC_MESSAGE_LENGTH> buffer;
46 ssize_t size = recv(mc->checker_side_.get_channel().get_socket(), buffer.data(), buffer.size(), MSG_DONTWAIT);
48 XBT_ERROR("Channel::receive failure: %s", strerror(errno));
50 throw simgrid::xbt::errno_error();
53 if (not mc->handle_message(buffer.data(), size))
54 mc->checker_side_.break_loop();
55 } else if (events == EV_SIGNAL) {
59 xbt_die("Unexpected signal: %d", sig);
61 xbt_die("Unexpected event");
66 XBT_DEBUG("Waiting for the model-checked process");
69 // The model-checked process SIGSTOP itself to signal it's ready:
70 const pid_t pid = remote_process_memory_->pid();
72 xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
73 "Could not wait model-checked process");
77 ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
78 ptrace(PTRACE_CONT, pid, 0, 0);
80 ptrace(PT_CONTINUE, pid, (caddr_t)1, 0);
82 # error "no ptrace equivalent coded for this platform"
84 xbt_assert(errno == 0,
85 "Ptrace does not seem to be usable in your setup (errno: %d). "
86 "If you run from within a docker, adding `--cap-add SYS_PTRACE` to the docker line may help. "
87 "If it does not help, please report this bug.",
91 bool ModelChecker::handle_message(const char* buffer, ssize_t size)
93 s_mc_message_t base_message;
94 xbt_assert(size >= (ssize_t)sizeof(base_message), "Broken message");
95 memcpy(&base_message, buffer, sizeof(base_message));
97 switch(base_message.type) {
98 case MessageType::INITIAL_ADDRESSES: {
99 s_mc_message_initial_addresses_t message;
100 xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message));
101 memcpy(&message, buffer, sizeof(message));
103 get_remote_process_memory().init(message.mmalloc_default_mdp);
107 case MessageType::IGNORE_HEAP: {
108 s_mc_message_ignore_heap_t message;
109 xbt_assert(size == sizeof(message), "Broken message");
110 memcpy(&message, buffer, sizeof(message));
112 IgnoredHeapRegion region;
113 region.block = message.block;
114 region.fragment = message.fragment;
115 region.address = message.address;
116 region.size = message.size;
117 get_remote_process_memory().ignore_heap(region);
121 case MessageType::UNIGNORE_HEAP: {
122 s_mc_message_ignore_memory_t message;
123 xbt_assert(size == sizeof(message), "Broken message");
124 memcpy(&message, buffer, sizeof(message));
125 get_remote_process_memory().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
129 case MessageType::IGNORE_MEMORY: {
130 s_mc_message_ignore_memory_t message;
131 xbt_assert(size == sizeof(message), "Broken message");
132 memcpy(&message, buffer, sizeof(message));
133 this->get_remote_process_memory().ignore_region(message.addr, message.size);
137 case MessageType::STACK_REGION: {
138 s_mc_message_stack_region_t message;
139 xbt_assert(size == sizeof(message), "Broken message");
140 memcpy(&message, buffer, sizeof(message));
141 this->get_remote_process_memory().stack_areas().push_back(message.stack_region);
144 case MessageType::REGISTER_SYMBOL: {
145 s_mc_message_register_symbol_t message;
146 xbt_assert(size == sizeof(message), "Broken message");
147 memcpy(&message, buffer, sizeof(message));
148 xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
149 XBT_DEBUG("Received symbol: %s", message.name.data());
151 LivenessChecker::automaton_register_symbol(get_remote_process_memory(), message.name.data(),
152 remote((int*)message.data));
156 case MessageType::WAITING:
159 case MessageType::ASSERTION_FAILED:
160 exploration_->report_assertion_failure();
164 xbt_die("Unexpected message from model-checked application");
169 void ModelChecker::handle_waitpid()
171 XBT_DEBUG("Check for wait event");
174 while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
176 if (errno == ECHILD) {
178 xbt_assert(not this->get_remote_process_memory().running(), "Inconsistent state");
181 XBT_ERROR("Could not wait for pid");
182 throw simgrid::xbt::errno_error();
186 if (pid == this->get_remote_process_memory().pid()) {
187 // From PTRACE_O_TRACEEXIT:
189 if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
190 unsigned long eventmsg;
191 xbt_assert(ptrace(PTRACE_GETEVENTMSG, get_remote_process_memory().pid(), 0, &eventmsg) != -1,
192 "Could not get exit status");
193 status = static_cast<int>(eventmsg);
194 if (WIFSIGNALED(status))
195 exploration_->report_crash(status);
199 // We don't care about non-lethal signals, just reinject them:
200 if (WIFSTOPPED(status)) {
201 XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
204 ptrace(PTRACE_CONT, get_remote_process_memory().pid(), 0, WSTOPSIG(status));
206 ptrace(PT_CONTINUE, get_remote_process_memory().pid(), (caddr_t)1, WSTOPSIG(status));
208 xbt_assert(errno == 0, "Could not PTRACE_CONT");
211 else if (WIFSIGNALED(status)) {
212 exploration_->report_crash(status);
213 } else if (WIFEXITED(status)) {
214 XBT_DEBUG("Child process is over");
215 this->get_remote_process_memory().terminate();
221 } // namespace simgrid::mc