include src/kernel/xml/simgrid_dtd.c
include src/kernel/xml/simgrid_dtd.h
include src/mc/AddressSpace.hpp
-include src/mc/ModelChecker.cpp
-include src/mc/ModelChecker.hpp
include src/mc/VisitedState.cpp
include src/mc/VisitedState.hpp
include src/mc/api/ActorState.hpp
include src/mc/api/RemoteApp.hpp
include src/mc/api/State.cpp
include src/mc/api/State.hpp
+include src/mc/api/guide/BasicGuide.hpp
+include src/mc/api/guide/GuidedState.hpp
include src/mc/compare.cpp
include src/mc/datatypes.h
include src/mc/explo/CommunicationDeterminismChecker.cpp
include tools/cmake/Modules/FindNS3.cmake
include tools/cmake/Modules/FindPAPI.cmake
include tools/cmake/Modules/FindValgrind.cmake
+include tools/cmake/Modules/nlohmann_jsonConfig.cmake
include tools/cmake/Modules/pybind11Config.cmake
include tools/cmake/Option.cmake
include tools/cmake/Tests.cmake
} // namespace kernel
namespace mc {
class State;
+class RemoteApp;
}
} // namespace simgrid
+++ /dev/null
-/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include "src/mc/ModelChecker.hpp"
-#include "src/mc/explo/Exploration.hpp"
-#include "src/mc/explo/LivenessChecker.hpp"
-#include "src/mc/mc_config.hpp"
-#include "src/mc/mc_exit.hpp"
-#include "src/mc/mc_private.hpp"
-#include "src/mc/sosp/RemoteProcessMemory.hpp"
-#include "src/mc/transition/TransitionComm.hpp"
-#include "xbt/automaton.hpp"
-#include "xbt/system_error.hpp"
-
-#include <array>
-#include <csignal>
-#include <sys/ptrace.h>
-#include <sys/wait.h>
-
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
-
-::simgrid::mc::ModelChecker* mc_model_checker = nullptr;
-
-namespace simgrid::mc {
-
-ModelChecker::ModelChecker(std::unique_ptr<RemoteProcessMemory> remote_memory)
- : remote_process_memory_(std::move(remote_memory))
-{
-}
-
-bool ModelChecker::handle_message(const char* buffer, ssize_t size)
-{
- s_mc_message_t base_message;
- xbt_assert(size >= (ssize_t)sizeof(base_message), "Broken message");
- memcpy(&base_message, buffer, sizeof(base_message));
-
- switch(base_message.type) {
- case MessageType::INITIAL_ADDRESSES: {
- s_mc_message_initial_addresses_t message;
- xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message));
- memcpy(&message, buffer, sizeof(message));
-
- get_remote_process_memory().init(message.mmalloc_default_mdp);
- break;
- }
-
- case MessageType::IGNORE_HEAP: {
- s_mc_message_ignore_heap_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
-
- IgnoredHeapRegion region;
- region.block = message.block;
- region.fragment = message.fragment;
- region.address = message.address;
- region.size = message.size;
- get_remote_process_memory().ignore_heap(region);
- break;
- }
-
- case MessageType::UNIGNORE_HEAP: {
- s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- get_remote_process_memory().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
- break;
- }
-
- case MessageType::IGNORE_MEMORY: {
- s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- this->get_remote_process_memory().ignore_region(message.addr, message.size);
- break;
- }
-
- case MessageType::STACK_REGION: {
- s_mc_message_stack_region_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- this->get_remote_process_memory().stack_areas().push_back(message.stack_region);
- } break;
-
- case MessageType::REGISTER_SYMBOL: {
- s_mc_message_register_symbol_t message;
- xbt_assert(size == sizeof(message), "Broken message");
- memcpy(&message, buffer, sizeof(message));
- xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
- XBT_DEBUG("Received symbol: %s", message.name.data());
-
- LivenessChecker::automaton_register_symbol(get_remote_process_memory(), message.name.data(),
- remote((int*)message.data));
- break;
- }
-
- case MessageType::WAITING:
- return false;
-
- case MessageType::ASSERTION_FAILED:
- exploration_->report_assertion_failure();
- break;
-
- default:
- xbt_die("Unexpected message from model-checked application");
- }
- return true;
-}
-
-void ModelChecker::handle_waitpid(pid_t pid_to_wait)
-{
- XBT_DEBUG("Check for wait event");
- int status;
- pid_t pid;
- while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
- if (pid == -1) {
- if (errno == ECHILD) { // No more children:
- xbt_assert(not this->get_remote_process_memory().running(), "Inconsistent state");
- break;
- } else {
- XBT_ERROR("Could not wait for pid");
- throw simgrid::xbt::errno_error();
- }
- }
-
- if (pid == pid_to_wait) {
- // From PTRACE_O_TRACEEXIT:
-#ifdef __linux__
- if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
- unsigned long eventmsg;
- xbt_assert(ptrace(PTRACE_GETEVENTMSG, pid_to_wait, 0, &eventmsg) != -1, "Could not get exit status");
- status = static_cast<int>(eventmsg);
- if (WIFSIGNALED(status))
- exploration_->report_crash(status);
- }
-#endif
-
- // We don't care about non-lethal signals, just reinject them:
- if (WIFSTOPPED(status)) {
- XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
- errno = 0;
-#ifdef __linux__
- ptrace(PTRACE_CONT, pid_to_wait, 0, WSTOPSIG(status));
-#elif defined BSD
- ptrace(PT_CONTINUE, pid_to_wait, (caddr_t)1, WSTOPSIG(status));
-#endif
- xbt_assert(errno == 0, "Could not PTRACE_CONT");
- }
-
- else if (WIFSIGNALED(status)) {
- exploration_->report_crash(status);
- } else if (WIFEXITED(status)) {
- XBT_DEBUG("Child process is over");
- this->get_remote_process_memory().terminate();
- }
- }
- }
-}
-
-} // namespace simgrid::mc
+++ /dev/null
-/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#ifndef SIMGRID_MC_MODEL_CHECKER_HPP
-#define SIMGRID_MC_MODEL_CHECKER_HPP
-
-#include "src/mc/remote/CheckerSide.hpp"
-#include "src/mc/remote/RemotePtr.hpp"
-#include "src/mc/sosp/PageStore.hpp"
-#include "xbt/base.h"
-
-#include <memory>
-
-namespace simgrid::mc {
-
-/** State of the model-checker (global variables for the model checker)
- */
-class ModelChecker {
- std::unique_ptr<RemoteProcessMemory> remote_process_memory_;
- Exploration* exploration_ = nullptr;
-
-public:
- ModelChecker(ModelChecker const&) = delete;
- ModelChecker& operator=(ModelChecker const&) = delete;
- explicit ModelChecker(std::unique_ptr<RemoteProcessMemory> remote_simulation);
-
- RemoteProcessMemory& get_remote_process_memory() { return *remote_process_memory_; }
-
- Exploration* get_exploration() const { return exploration_; }
- void set_exploration(Exploration* exploration) { exploration_ = exploration; }
-
- void handle_waitpid(pid_t pid_to_wait); // FIXME move to RemoteApp
- bool handle_message(const char* buffer, ssize_t size); // FIXME move to RemoteApp
-};
-
-} // namespace simgrid::mc
-
-#endif
for (auto i = range_begin; i != range_end; ++i) {
auto& visited_state = *i;
- if (*visited_state->system_state_.get() == *new_state->system_state_.get()) {
+ if (visited_state->system_state_->equals_to(*new_state->system_state_.get(),
+ remote_app.get_remote_process_memory())) {
// The state has been visited:
std::unique_ptr<simgrid::mc::VisitedState> old_state = std::move(visited_state);
#include <algorithm>
#include <array>
-#include <boost/tokenizer.hpp>
#include <memory>
#include <numeric>
#include <string>
-#include <fcntl.h>
-#ifdef __linux__
-#include <sys/prctl.h>
-#endif
#include <sys/ptrace.h>
#include <sys/wait.h>
-#ifdef __linux__
-#define WAITPID_CHECKED_FLAGS __WALL
-#else
-#define WAITPID_CHECKED_FLAGS 0
-#endif
-
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
XBT_LOG_EXTERNAL_CATEGORY(mc_global);
-static simgrid::config::Flag<std::string> _sg_mc_setenv{
- "model-check/setenv", "Extra environment variables to pass to the child process (ex: 'AZE=aze;QWE=qwe').", "",
- [](std::string_view value) {
- xbt_assert(value.empty() || value.find('=', 0) != std::string_view::npos,
- "The 'model-check/setenv' parameter must be like 'AZE=aze', but it does not contain an equal sign.");
- }};
-
namespace simgrid::mc {
-XBT_ATTRIB_NORETURN static void run_child_process(int socket, const std::vector<char*>& args)
-{
- /* On startup, simix_global_init() calls simgrid::mc::Client::initialize(), which checks whether the MC_ENV_SOCKET_FD
- * env variable is set. If so, MC mode is assumed, and the client is setup from its side
- */
-
-#ifdef __linux__
- // Make sure we do not outlive our parent
- sigset_t mask;
- sigemptyset(&mask);
- xbt_assert(sigprocmask(SIG_SETMASK, &mask, nullptr) >= 0, "Could not unblock signals");
- xbt_assert(prctl(PR_SET_PDEATHSIG, SIGHUP) == 0, "Could not PR_SET_PDEATHSIG");
-#endif
-
- // Remove CLOEXEC to pass the socket to the application
- int fdflags = fcntl(socket, F_GETFD, 0);
- xbt_assert(fdflags != -1 && fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) != -1,
- "Could not remove CLOEXEC for socket");
-
- setenv(MC_ENV_SOCKET_FD, std::to_string(socket).c_str(), 1);
-
- /* Setup the tokenizer that parses the cfg:model-check/setenv parameter */
- using Tokenizer = boost::tokenizer<boost::char_separator<char>>;
- boost::char_separator<char> semicol_sep(";");
- boost::char_separator<char> equal_sep("=");
- Tokenizer token_vars(_sg_mc_setenv.get(), semicol_sep); /* Iterate over all FOO=foo parts */
- for (const auto& token : token_vars) {
- std::vector<std::string> kv;
- Tokenizer token_kv(token, equal_sep);
- for (const auto& t : token_kv) /* Iterate over 'FOO' and then 'foo' in that 'FOO=foo' */
- kv.push_back(t);
- xbt_assert(kv.size() == 2, "Parse error on 'model-check/setenv' value %s. Does it contain an equal sign?",
- token.c_str());
- XBT_INFO("setenv '%s'='%s'", kv[0].c_str(), kv[1].c_str());
- setenv(kv[0].c_str(), kv[1].c_str(), 1);
- }
-
- /* And now, exec the child process */
- int i = 1;
- while (args[i] != nullptr && args[i][0] == '-')
- i++;
-
- xbt_assert(args[i] != nullptr,
- "Unable to find a binary to exec on the command line. Did you only pass config flags?");
-
- execvp(args[i], args.data() + i);
- XBT_CRITICAL("The model-checked process failed to exec(%s): %s.\n"
- " Make sure that your binary exists on disk and is executable.",
- args[i], strerror(errno));
- if (strchr(args[i], '=') != nullptr)
- XBT_CRITICAL("If you want to pass environment variables to the application, please use --cfg=model-check/setenv:%s",
- args[i]);
-
- xbt_die("Aborting now.");
-}
-
RemoteApp::RemoteApp(const std::vector<char*>& args)
{
- // Create an AF_LOCAL socketpair used for exchanging messages
- // between the model-checker process (ourselves) and the model-checked
- // process:
- int sockets[2];
- xbt_assert(socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets) != -1, "Could not create socketpair");
-
- pid_t pid = fork();
- xbt_assert(pid >= 0, "Could not fork model-checked process");
-
- if (pid == 0) { // Child
- ::close(sockets[1]);
- run_child_process(sockets[0], args);
- DIE_IMPOSSIBLE;
- }
+ checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(args);
- // Parent (model-checker):
- ::close(sockets[0]);
-
- xbt_assert(mc_model_checker == nullptr, "Did you manage to start the MC twice in this process?");
-
- auto memory = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid);
- model_checker_ = std::make_unique<simgrid::mc::ModelChecker>(std::move(memory));
- mc_model_checker = model_checker_.get();
- checker_side_ = std::make_unique<simgrid::mc::CheckerSide>(sockets[1], model_checker_.get());
-
- start();
-
- /* Take the initial snapshot */
- wait_for_requests();
- initial_snapshot_ =
- std::make_shared<simgrid::mc::Snapshot>(0, page_store_, model_checker_->get_remote_process_memory());
+ initial_snapshot_ = std::make_shared<simgrid::mc::Snapshot>(0, page_store_, checker_side_->get_remote_memory());
}
RemoteApp::~RemoteApp()
{
initial_snapshot_ = nullptr;
- if (model_checker_) {
- shutdown();
- model_checker_ = nullptr;
- mc_model_checker = nullptr;
- }
-}
-void RemoteApp::start()
-{
- XBT_DEBUG("Waiting for the model-checked process");
- int status;
-
- // The model-checked process SIGSTOP itself to signal it's ready:
- const pid_t pid = get_remote_process_memory().pid();
-
- xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
- "Could not wait model-checked process");
-
- errno = 0;
-#ifdef __linux__
- ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
- ptrace(PTRACE_CONT, pid, 0, 0);
-#elif defined BSD
- ptrace(PT_CONTINUE, pid, (caddr_t)1, 0);
-#else
-#error "no ptrace equivalent coded for this platform"
-#endif
- xbt_assert(errno == 0,
- "Ptrace does not seem to be usable in your setup (errno: %d). "
- "If you run from within a docker, adding `--cap-add SYS_PTRACE` to the docker line may help. "
- "If it does not help, please report this bug.",
- errno);
+ shutdown();
}
+
void RemoteApp::restore_initial_state() const
{
- this->initial_snapshot_->restore(model_checker_->get_remote_process_memory());
+ this->initial_snapshot_->restore(checker_side_->get_remote_memory());
}
unsigned long RemoteApp::get_maxpid() const
to_c_str(message.type), (int)message.type, (int)MessageType::DEADLOCK_CHECK_REPLY);
if (message.value != 0) {
+ auto* explo = Exploration::get_instance();
XBT_CINFO(mc_global, "Counter-example execution trace:");
- for (auto const& frame : model_checker_->get_exploration()->get_textual_trace())
+ for (auto const& frame : explo->get_textual_trace())
XBT_CINFO(mc_global, " %s", frame.c_str());
XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
"--cfg=model-check/replay:'%s'",
- model_checker_->get_exploration()->get_record_trace().to_string().c_str());
- model_checker_->get_exploration()->log_state();
+ explo->get_record_trace().to_string().c_str());
+ explo->log_state();
throw DeadlockError();
}
}
void RemoteApp::wait_for_requests()
{
- /* Resume the application */
- if (checker_side_->get_channel().send(MessageType::CONTINUE) != 0)
- throw xbt::errno_error();
- get_remote_process_memory().clear_cache();
-
- if (this->get_remote_process_memory().running())
- checker_side_->dispatch();
+ checker_side_->wait_for_requests();
}
void RemoteApp::shutdown()
{
XBT_DEBUG("Shutting down model-checker");
- RemoteProcessMemory& process = get_remote_process_memory();
- if (process.running()) {
+ if (checker_side_->running()) {
XBT_DEBUG("Killing process");
finalize_app(true);
- kill(process.pid(), SIGKILL);
- process.terminate();
+ kill(checker_side_->get_pid(), SIGKILL);
+ checker_side_->terminate();
}
}
checker_side_->get_channel().send(m);
get_remote_process_memory().clear_cache();
- if (this->get_remote_process_memory().running())
- checker_side_->dispatch(); // The app may send messages while processing the transition
+ if (checker_side_->running())
+ checker_side_->dispatch_events(); // The app may send messages while processing the transition
s_mc_message_simcall_execute_answer_t answer;
ssize_t s = checker_side_->get_channel().receive(answer);
#define SIMGRID_MC_REMOTE_APP_HPP
#include "simgrid/forward.h"
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/api/ActorState.hpp"
+#include "src/mc/remote/CheckerSide.hpp"
#include "src/mc/remote/RemotePtr.hpp"
+#include "src/mc/sosp/PageStore.hpp"
#include <functional>
/** High-level view of the verified application, from the model-checker POV
*
- * This is expected to become the interface used by model-checking
- * algorithms to control the execution of the model-checked process
- * and the exploration of the execution graph. Model-checking
- * algorithms should be able to be written in high-level languages
- * (e.g. Python) using bindings on this interface.
+ * This is expected to become the interface used by model-checking algorithms to control the execution of
+ * the application process during the exploration of the execution graph.
+ *
+ * One day, this will allow parallel exploration, ie, the handling of several application processes (each encapsulated
+ * in a separate CheckerSide objects) that explore several parts of the exploration graph.
*/
class XBT_PUBLIC RemoteApp {
private:
std::unique_ptr<CheckerSide> checker_side_;
- std::unique_ptr<ModelChecker> model_checker_;
PageStore page_store_{500};
std::shared_ptr<simgrid::mc::Snapshot> initial_snapshot_;
~RemoteApp();
- void start();
void restore_initial_state() const;
void wait_for_requests();
Transition* handle_simcall(aid_t aid, int times_considered, bool new_transition);
/* Get the memory of the remote process */
- RemoteProcessMemory& get_remote_process_memory() { return model_checker_->get_remote_process_memory(); }
+ RemoteProcessMemory& get_remote_process_memory() { return checker_side_->get_remote_memory(); }
PageStore& get_page_store() { return page_store_; }
};
}
namespace simgrid::mc {
-
-bool Snapshot::operator==(const Snapshot& other)
+bool Snapshot::equals_to(const Snapshot& other, RemoteProcessMemory& memory)
{
- // TODO, make this a field of ModelChecker or something similar
- static StateComparator state_comparator;
+ /* TODO: the memory parameter should be eventually removed. It seems to be there because each snapshot lacks some sort
+ of metadata. That's OK for now (letting appart the fact that we cannot have a nice operator== because we need that
+ extra parameter), but it will fall short when we want to have parallel explorations, with more than one
+ RemoteProcess. At the very least, snapshots will need to know the remote process they are corresponding to, and more
+ probably they will need to embeed all their metadata to let the remoteprocesses die before the end of the
+ exploration. */
+
+ /* TODO: This method should moved to Snapshot.cpp, but it needs the StateComparator that is declared locally to this
+ * file only. */
- RemoteProcessMemory& memory = mc_model_checker->get_remote_process_memory();
+ static StateComparator state_comparator; // TODO, make this a field of a persistant state object
if (hash_ != other.hash_) {
XBT_VERB("(%ld - %ld) Different hash: 0x%" PRIx64 "--0x%" PRIx64, this->num_state_, other.num_state_, this->hash_,
void DFSExplorer::check_non_termination(const State* current_state)
{
for (auto const& state : stack_) {
- if (*state->get_system_state() == *current_state->get_system_state()) {
+ if (state->get_system_state()->equals_to(*current_state->get_system_state(),
+ get_remote_app().get_remote_process_memory())) {
XBT_INFO("Non-progressive cycle: state %ld -> state %ld", state->get_num(), current_state->get_num());
XBT_INFO("******************************************");
XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
for (std::unique_ptr<State> const& state : stack_) {
if (state == stack_.back()) /* If we are arrived on the target state, don't replay the outgoing transition */
break;
- state->get_transition()->replay();
+ state->get_transition()->replay(get_remote_app());
on_transition_replay_signal(state->get_transition(), get_remote_app());
visited_states_count_++;
}
static simgrid::config::Flag<std::string> cfg_dot_output_file{
"model-check/dot-output", "Name of dot output file corresponding to graph state", ""};
+Exploration* Exploration::instance_ = nullptr; // singleton instance
+
Exploration::Exploration(const std::vector<char*>& args) : remote_app_(std::make_unique<RemoteApp>(args))
{
- mc_model_checker->set_exploration(this);
+ xbt_assert(instance_ == nullptr, "Cannot have more than one exploration instance");
+ instance_ = this;
if (not cfg_dot_output_file.get().empty()) {
dot_output_ = fopen(cfg_dot_output_file.get().c_str(), "w");
{
if (dot_output_ != nullptr)
fclose(dot_output_);
+ instance_ = nullptr;
}
void Exploration::dot_output(const char* fmt, ...)
get_remote_app().get_remote_process_memory().dump_stack();
}
- get_remote_app().get_remote_process_memory().terminate();
system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
}
void Exploration::report_assertion_failure()
// abstract
class Exploration : public xbt::Extendable<Exploration> {
std::unique_ptr<RemoteApp> remote_app_;
+ static Exploration* instance_;
FILE* dot_output_ = nullptr;
explicit Exploration(const std::vector<char*>& args);
virtual ~Exploration();
+ static Exploration* get_instance() { return instance_; }
// No copy:
Exploration(Exploration const&) = delete;
Exploration& operator=(Exploration const&) = delete;
RemoteApp& remote_app)
: num(pair_num), prop_state_(prop_state)
{
- auto& memory = mc_model_checker->get_remote_process_memory();
+ auto& memory = remote_app.get_remote_process_memory();
this->app_state_ = std::move(app_state);
if (not this->app_state_->get_system_state())
this->app_state_->set_system_state(std::make_shared<Snapshot>(pair_num, remote_app.get_page_store(), memory));
std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
if (xbt_automaton_state_compare(pair_test->prop_state_, new_pair->prop_state_) != 0 ||
*(pair_test->atomic_propositions) != *(new_pair->atomic_propositions) ||
- (*pair_test->app_state_->get_system_state() != *new_pair->app_state_->get_system_state()))
+ (not pair_test->app_state_->get_system_state()->equals_to(*new_pair->app_state_->get_system_state(),
+ get_remote_app().get_remote_process_memory())))
continue;
XBT_INFO("Pair %d already reached (equal to pair %d) !", new_pair->num, pair_test->num);
exploration_stack_.pop_back();
std::shared_ptr<State> state = pair->app_state_;
if (pair->exploration_started) {
- state->get_transition()->replay();
+ state->get_transition()->replay(get_remote_app());
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->get_transition()->to_string().c_str(), state.get());
}
const VisitedPair* pair_test = i->get();
if (xbt_automaton_state_compare(pair_test->prop_state_, visited_pair->prop_state_) != 0 ||
*(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions) ||
- (*pair_test->app_state_->get_system_state() != *visited_pair->app_state_->get_system_state()))
+ (not pair_test->app_state_->get_system_state()->equals_to(*visited_pair->app_state_->get_system_state(),
+ get_remote_app().get_remote_process_memory())))
continue;
if (pair_test->other_num == -1)
visited_pair->other_num = pair_test->num;
#include "src/mc/mc_replay.hpp"
#if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/remote/AppSide.hpp"
#include "src/mc/sosp/RemoteProcessMemory.hpp"
class PageStore;
class ChunkedData;
-class ModelChecker;
class AddressSpace;
class RemoteProcessMemory;
class Snapshot;
class Variable;
class Transition;
class Frame;
-class ActorInformation;
class Session;
class Exploration;
} // namespace simgrid::mc
-// TODO, try to get rid of the global ModelChecker variable
-extern simgrid::mc::ModelChecker* mc_model_checker;
-
#endif
template <class M> static constexpr bool messageType() { return std::is_class_v<M> && std::is_trivial_v<M>; }
public:
+ Channel() = default;
explicit Channel(int sock) : socket_(sock) {}
~Channel();
}
int get_socket() const { return socket_; }
+ void reset_socket(int socket) { socket_ = socket; }
};
} // namespace simgrid::mc
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/remote/CheckerSide.hpp"
-#include "src/mc/ModelChecker.hpp"
+#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/LivenessChecker.hpp"
#include "src/mc/sosp/RemoteProcessMemory.hpp"
#include "xbt/system_error.hpp"
+
+#ifdef __linux__
+#include <sys/personality.h>
+#include <sys/prctl.h>
+#endif
+
+#include <boost/tokenizer.hpp>
#include <csignal>
+#include <fcntl.h>
+#include <sys/ptrace.h>
#include <sys/wait.h>
+#ifdef __linux__
+#define WAITPID_CHECKED_FLAGS __WALL
+#else
+#define WAITPID_CHECKED_FLAGS 0
+#endif
+
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_checkerside, mc, "MC communication with the application");
+static simgrid::config::Flag<std::string> _sg_mc_setenv{
+ "model-check/setenv", "Extra environment variables to pass to the child process (ex: 'AZE=aze;QWE=qwe').", "",
+ [](std::string_view value) {
+ xbt_assert(value.empty() || value.find('=', 0) != std::string_view::npos,
+ "The 'model-check/setenv' parameter must be like 'AZE=aze', but it does not contain an equal sign.");
+ }};
+
namespace simgrid::mc {
-CheckerSide::CheckerSide(int sockfd, ModelChecker* mc) : channel_(sockfd)
+
+XBT_ATTRIB_NORETURN static void run_child_process(int socket, const std::vector<char*>& args)
+{
+ /* On startup, simix_global_init() calls simgrid::mc::Client::initialize(), which checks whether the MC_ENV_SOCKET_FD
+ * env variable is set. If so, MC mode is assumed, and the client is setup from its side
+ */
+
+#ifdef __linux__
+ // Make sure we do not outlive our parent
+ sigset_t mask;
+ sigemptyset(&mask);
+ xbt_assert(sigprocmask(SIG_SETMASK, &mask, nullptr) >= 0, "Could not unblock signals");
+ xbt_assert(prctl(PR_SET_PDEATHSIG, SIGHUP) == 0, "Could not PR_SET_PDEATHSIG");
+
+ // Make sure that the application process layout is not randomized, so that the info we gather is stable over re-execs
+ if (personality(ADDR_NO_RANDOMIZE) == -1) {
+ XBT_ERROR("Could not set the NO_RANDOMIZE personality");
+ throw xbt::errno_error();
+ }
+#endif
+
+ // Remove CLOEXEC to pass the socket to the application
+ int fdflags = fcntl(socket, F_GETFD, 0);
+ xbt_assert(fdflags != -1 && fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) != -1,
+ "Could not remove CLOEXEC for socket");
+
+ setenv(MC_ENV_SOCKET_FD, std::to_string(socket).c_str(), 1);
+
+ /* Setup the tokenizer that parses the cfg:model-check/setenv parameter */
+ using Tokenizer = boost::tokenizer<boost::char_separator<char>>;
+ boost::char_separator<char> semicol_sep(";");
+ boost::char_separator<char> equal_sep("=");
+ Tokenizer token_vars(_sg_mc_setenv.get(), semicol_sep); /* Iterate over all FOO=foo parts */
+ for (const auto& token : token_vars) {
+ std::vector<std::string> kv;
+ Tokenizer token_kv(token, equal_sep);
+ for (const auto& t : token_kv) /* Iterate over 'FOO' and then 'foo' in that 'FOO=foo' */
+ kv.push_back(t);
+ xbt_assert(kv.size() == 2, "Parse error on 'model-check/setenv' value %s. Does it contain an equal sign?",
+ token.c_str());
+ XBT_INFO("setenv '%s'='%s'", kv[0].c_str(), kv[1].c_str());
+ setenv(kv[0].c_str(), kv[1].c_str(), 1);
+ }
+
+ /* And now, exec the child process */
+ int i = 1;
+ while (args[i] != nullptr && args[i][0] == '-')
+ i++;
+
+ xbt_assert(args[i] != nullptr,
+ "Unable to find a binary to exec on the command line. Did you only pass config flags?");
+
+ execvp(args[i], args.data() + i);
+ XBT_CRITICAL("The model-checked process failed to exec(%s): %s.\n"
+ " Make sure that your binary exists on disk and is executable.",
+ args[i], strerror(errno));
+ if (strchr(args[i], '=') != nullptr)
+ XBT_CRITICAL("If you want to pass environment variables to the application, please use --cfg=model-check/setenv:%s",
+ args[i]);
+
+ xbt_die("Aborting now.");
+}
+
+static void wait_application_process(pid_t pid)
+{
+ XBT_DEBUG("Waiting for the model-checked process");
+ int status;
+
+ // The model-checked process SIGSTOP itself to signal it's ready:
+ xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
+ "Could not wait model-checked process");
+
+ errno = 0;
+#ifdef __linux__
+ ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
+ ptrace(PTRACE_CONT, pid, 0, 0);
+#elif defined BSD
+ ptrace(PT_CONTINUE, pid, (caddr_t)1, 0);
+#else
+#error "no ptrace equivalent coded for this platform"
+#endif
+ xbt_assert(errno == 0,
+ "Ptrace does not seem to be usable in your setup (errno: %d). "
+ "If you run from within a docker, adding `--cap-add SYS_PTRACE` to the docker line may help. "
+ "If it does not help, please report this bug.",
+ errno);
+}
+
+void CheckerSide::setup_events()
{
auto* base = event_base_new();
base_.reset(base);
throw simgrid::xbt::errno_error();
}
- if (not mc_model_checker->handle_message(buffer.data(), size))
+ if (not checker->handle_message(buffer.data(), size))
checker->break_loop();
} else {
xbt_die("Unexpected event");
auto* signal_event = event_new(
base, SIGCHLD, EV_SIGNAL | EV_PERSIST,
[](evutil_socket_t sig, short events, void* arg) {
- auto mc = static_cast<simgrid::mc::ModelChecker*>(arg);
+ auto checker = static_cast<simgrid::mc::CheckerSide*>(arg);
if (events == EV_SIGNAL) {
if (sig == SIGCHLD)
- mc->handle_waitpid(mc->get_remote_process_memory().pid());
+ checker->handle_waitpid();
else
xbt_die("Unexpected signal: %d", sig);
} else {
xbt_die("Unexpected event");
}
},
- mc);
+ this);
event_add(signal_event, nullptr);
signal_event_.reset(signal_event);
}
-void CheckerSide::dispatch() const
+CheckerSide::CheckerSide(const std::vector<char*>& args) : running_(true)
+{
+ // Create an AF_LOCAL socketpair used for exchanging messages between the model-checker process (ancestor)
+ // and the application process (child)
+ int sockets[2];
+ xbt_assert(socketpair(AF_LOCAL, SOCK_SEQPACKET | SOCK_CLOEXEC, 0, sockets) != -1, "Could not create socketpair");
+
+ pid_ = fork();
+ xbt_assert(pid_ >= 0, "Could not fork model-checked process");
+
+ if (pid_ == 0) { // Child
+ ::close(sockets[1]);
+ run_child_process(sockets[0], args);
+ DIE_IMPOSSIBLE;
+ }
+
+ // Parent (model-checker):
+ ::close(sockets[0]);
+ channel_.reset_socket(sockets[1]);
+
+ setup_events();
+ wait_application_process(pid_);
+
+ wait_for_requests();
+}
+
+void CheckerSide::dispatch_events() const
{
event_base_dispatch(base_.get());
}
event_base_loopbreak(base_.get());
}
+bool CheckerSide::handle_message(const char* buffer, ssize_t size)
+{
+ s_mc_message_t base_message;
+ xbt_assert(size >= (ssize_t)sizeof(base_message), "Broken message");
+ memcpy(&base_message, buffer, sizeof(base_message));
+
+ switch (base_message.type) {
+ case MessageType::INITIAL_ADDRESSES: {
+ s_mc_message_initial_addresses_t message;
+ xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size,
+ (int)sizeof(message));
+ memcpy(&message, buffer, sizeof(message));
+ /* Create the memory address space, now that we have the mandatory information */
+ remote_memory_ = std::make_unique<simgrid::mc::RemoteProcessMemory>(pid_, message.mmalloc_default_mdp);
+ break;
+ }
+
+ case MessageType::IGNORE_HEAP: {
+ s_mc_message_ignore_heap_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+
+ IgnoredHeapRegion region;
+ region.block = message.block;
+ region.fragment = message.fragment;
+ region.address = message.address;
+ region.size = message.size;
+ get_remote_memory().ignore_heap(region);
+ break;
+ }
+
+ case MessageType::UNIGNORE_HEAP: {
+ s_mc_message_ignore_memory_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
+ break;
+ }
+
+ case MessageType::IGNORE_MEMORY: {
+ s_mc_message_ignore_memory_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory().ignore_region(message.addr, message.size);
+ break;
+ }
+
+ case MessageType::STACK_REGION: {
+ s_mc_message_stack_region_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ get_remote_memory().stack_areas().push_back(message.stack_region);
+ } break;
+
+ case MessageType::REGISTER_SYMBOL: {
+ s_mc_message_register_symbol_t message;
+ xbt_assert(size == sizeof(message), "Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ xbt_assert(not message.callback, "Support for client-side function proposition is not implemented.");
+ XBT_DEBUG("Received symbol: %s", message.name.data());
+
+ LivenessChecker::automaton_register_symbol(get_remote_memory(), message.name.data(), remote((int*)message.data));
+ break;
+ }
+
+ case MessageType::WAITING:
+ return false;
+
+ case MessageType::ASSERTION_FAILED:
+ Exploration::get_instance()->report_assertion_failure();
+ break;
+
+ default:
+ xbt_die("Unexpected message from model-checked application");
+ }
+ return true;
+}
+
+void CheckerSide::wait_for_requests()
+{
+ /* Resume the application */
+ if (get_channel().send(MessageType::CONTINUE) != 0)
+ throw xbt::errno_error();
+ clear_memory_cache();
+
+ if (running())
+ dispatch_events();
+}
+
+void CheckerSide::clear_memory_cache()
+{
+ if (remote_memory_)
+ remote_memory_->clear_cache();
+}
+
+void CheckerSide::handle_waitpid()
+{
+ XBT_DEBUG("Check for wait event");
+ int status;
+ pid_t pid;
+ while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
+ if (pid == -1) {
+ if (errno == ECHILD) { // No more children:
+ xbt_assert(not this->running(), "Inconsistent state");
+ break;
+ } else {
+ XBT_ERROR("Could not wait for pid");
+ throw simgrid::xbt::errno_error();
+ }
+ }
+
+ if (pid == get_pid()) {
+ // From PTRACE_O_TRACEEXIT:
+#ifdef __linux__
+ if (status >> 8 == (SIGTRAP | (PTRACE_EVENT_EXIT << 8))) {
+ unsigned long eventmsg;
+ xbt_assert(ptrace(PTRACE_GETEVENTMSG, pid, 0, &eventmsg) != -1, "Could not get exit status");
+ status = static_cast<int>(eventmsg);
+ if (WIFSIGNALED(status)) {
+ this->terminate();
+ Exploration::get_instance()->report_crash(status);
+ }
+ }
+#endif
+
+ // We don't care about non-lethal signals, just reinject them:
+ if (WIFSTOPPED(status)) {
+ XBT_DEBUG("Stopped with signal %i", (int)WSTOPSIG(status));
+ errno = 0;
+#ifdef __linux__
+ ptrace(PTRACE_CONT, pid, 0, WSTOPSIG(status));
+#elif defined BSD
+ ptrace(PT_CONTINUE, pid, (caddr_t)1, WSTOPSIG(status));
+#endif
+ xbt_assert(errno == 0, "Could not PTRACE_CONT");
+ }
+
+ else if (WIFSIGNALED(status)) {
+ this->terminate();
+ Exploration::get_instance()->report_crash(status);
+ } else if (WIFEXITED(status)) {
+ XBT_DEBUG("Child process is over");
+ this->terminate();
+ }
+ }
+ }
+}
+
} // namespace simgrid::mc
namespace simgrid::mc {
+/* CheckerSide: All what the checker needs to interact with a given application process */
+
class CheckerSide {
std::unique_ptr<event_base, decltype(&event_base_free)> base_{nullptr, &event_base_free};
std::unique_ptr<event, decltype(&event_free)> socket_event_{nullptr, &event_free};
std::unique_ptr<event, decltype(&event_free)> signal_event_{nullptr, &event_free};
-
+ std::unique_ptr<RemoteProcessMemory> remote_memory_;
Channel channel_;
+ bool running_ = false;
+ pid_t pid_;
+
+ void setup_events(); // Part of the initialization
+ void clear_memory_cache();
+ void handle_waitpid();
+
public:
- explicit CheckerSide(int sockfd, ModelChecker* mc);
+ explicit CheckerSide(const std::vector<char*>& args);
// No copy:
CheckerSide(CheckerSide const&) = delete;
CheckerSide& operator=(CheckerSide const&) = delete;
CheckerSide& operator=(CheckerSide&&) = delete;
+ /* Communicating with the application */
Channel const& get_channel() const { return channel_; }
Channel& get_channel() { return channel_; }
- void dispatch() const;
+ bool handle_message(const char* buffer, ssize_t size);
+ void dispatch_events() const;
void break_loop() const;
+ void wait_for_requests();
+
+ /* Interacting with the application process */
+ pid_t get_pid() const { return pid_; }
+ bool running() const { return running_; }
+ void terminate() { running_ = false; }
+ RemoteProcessMemory& get_remote_memory() { return *remote_memory_.get(); }
};
} // namespace simgrid::mc
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/sosp/Region.hpp"
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_forward.hpp"
#include "src/mc/sosp/RemoteProcessMemory.hpp"
namespace simgrid::mc {
-Region::Region(PageStore& store, RegionType region_type, void* start_addr, size_t size)
+Region::Region(PageStore& store, RemoteProcessMemory& memory, RegionType region_type, void* start_addr, size_t size)
: region_type_(region_type), start_addr_(start_addr), size_(size)
{
xbt_assert((((uintptr_t)start_addr) & (xbt_pagesize - 1)) == 0, "Start address not at the beginning of a page");
- chunks_ = ChunkedData(store, mc_model_checker->get_remote_process_memory(), RemotePtr<void>(start_addr),
- mmu::chunk_count(size));
+ chunks_ = ChunkedData(store, memory, RemotePtr<void>(start_addr), mmu::chunk_count(size));
}
/** @brief Restore a region from a snapshot
*
* @param region Target region
*/
-void Region::restore() const
+void Region::restore(RemoteProcessMemory& memory) const
{
xbt_assert(((start().address()) & (xbt_pagesize - 1)) == 0, "Not at the beginning of a page");
xbt_assert(simgrid::mc::mmu::chunk_count(size()) == get_chunks().page_count());
for (size_t i = 0; i != get_chunks().page_count(); ++i) {
auto* target_page = (void*)simgrid::mc::mmu::join(i, (std::uintptr_t)(void*)start().address());
const void* source_page = get_chunks().page(i);
- mc_model_checker->get_remote_process_memory().write_bytes(source_page, xbt_pagesize, remote(target_page));
+ memory.write_bytes(source_page, xbt_pagesize, remote(target_page));
}
}
ChunkedData chunks_;
public:
- Region(PageStore& store, RegionType type, void* start_addr, size_t size);
+ Region(PageStore& store, RemoteProcessMemory& memory, RegionType type, void* start_addr, size_t size);
Region(Region const&) = delete;
Region& operator=(Region const&) = delete;
Region(Region&& that) = delete;
bool contain(RemotePtr<void> p) const { return p >= start() && p < end(); }
/** @brief Restore a region from a snapshot */
- void restore() const;
+ void restore(RemoteProcessMemory& memory) const;
/** @brief Read memory that was snapshotted in this region
*
#include "src/mc/sosp/RemoteProcessMemory.hpp"
+#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/LivenessChecker.hpp"
#include "src/mc/sosp/Snapshot.hpp"
#include "xbt/file.hpp"
#include "xbt/log.h"
+#include "xbt/system_error.hpp"
#include <fcntl.h>
#include <libunwind-ptrace.h>
// ***** RemoteProcessMemory
-RemoteProcessMemory::RemoteProcessMemory(pid_t pid) : AddressSpace(this), pid_(pid), running_(true) {}
-
-void RemoteProcessMemory::init(xbt_mheap_t mmalloc_default_mdp)
+RemoteProcessMemory::RemoteProcessMemory(pid_t pid, xbt_mheap_t mmalloc_default_mdp) : AddressSpace(this), pid_(pid)
{
this->heap_address = remote(mmalloc_default_mdp);
_UPT_destroy(context);
unw_destroy_addr_space(as);
}
+
} // namespace simgrid::mc
namespace simgrid::mc {
-class ActorInformation {
-public:
- /** MCed address of the process */
- RemotePtr<kernel::actor::ActorImpl> address{nullptr};
- Remote<kernel::actor::ActorImpl> copy;
-
- /** Hostname (owned by `mc_model_checker->hostnames_`) */
- const std::string* hostname = nullptr;
- std::string name;
-
- void clear()
- {
- name.clear();
- address = nullptr;
- hostname = nullptr;
- }
-};
-
struct IgnoredRegion {
std::uint64_t addr;
std::size_t size;
std::size_t size;
};
-/** The Application's process memory, seen from the Checker perspective
- *
- * Responsibilities:
+/** The Application's process memory, seen from the Checker perspective. This class is not needed if you don't need to
+ * introspect the application process.
*
- * - reading from the process memory (`AddressSpace`);
- * - accessing the system state of the process (heap, …);
- * - stack unwinding;
- * - etc.
+ * Responsabilities:
+ * - reading from the process memory (`AddressSpace`);
+ * - accessing the system state of the process (heap, …);
+ * - stack unwinding;
+ * - etc.
*/
class RemoteProcessMemory final : public AddressSpace {
private:
static constexpr int cache_malloc = 2;
public:
- explicit RemoteProcessMemory(pid_t pid);
+ explicit RemoteProcessMemory(pid_t pid, xbt_mheap_t mmalloc_default_mdp);
~RemoteProcessMemory() override;
- void init(xbt_mheap_t mmalloc_default_mdp);
RemoteProcessMemory(RemoteProcessMemory const&) = delete;
RemoteProcessMemory(RemoteProcessMemory&&) = delete;
std::vector<IgnoredRegion> const& ignored_regions() const { return ignored_regions_; }
void ignore_region(std::uint64_t address, std::size_t size);
- pid_t pid() const { return pid_; }
-
bool in_maestro_stack(RemotePtr<void> p) const
{
return p >= this->maestro_stack_start_ && p < this->maestro_stack_end_;
}
- bool running() const { return running_; }
-
- void terminate() { running_ = false; }
-
void ignore_global_variable(const char* name) const
{
for (std::shared_ptr<ObjectInformation> const& info : this->object_infos)
void refresh_heap();
void refresh_malloc_info();
- pid_t pid_ = -1;
- bool running_ = false;
+ pid_t pid_ = -1;
std::vector<xbt::VmMap> memory_map_;
RemotePtr<void> maestro_stack_start_;
RemotePtr<void> maestro_stack_end_;
/************************************* Take Snapshot ************************************/
/****************************************************************************************/
-void Snapshot::snapshot_regions(RemoteProcessMemory& process_memory)
+void Snapshot::snapshot_regions(RemoteProcessMemory& memory)
{
snapshot_regions_.clear();
- for (auto const& object_info : process_memory.object_infos)
- add_region(RegionType::Data, object_info.get(), object_info->start_rw, object_info->end_rw - object_info->start_rw);
+ for (auto const& object_info : memory.object_infos)
+ add_region(RegionType::Data, memory, object_info.get(), object_info->start_rw,
+ object_info->end_rw - object_info->start_rw);
- const s_xbt_mheap_t* heap = process_memory.get_heap();
+ const s_xbt_mheap_t* heap = memory.get_heap();
void* start_heap = heap->base;
void* end_heap = heap->breakval;
- add_region(RegionType::Heap, nullptr, start_heap, (char*)end_heap - (char*)start_heap);
- heap_bytes_used_ = mmalloc_get_bytes_used_remote(heap->heaplimit, process_memory.get_malloc_info());
+ add_region(RegionType::Heap, memory, nullptr, start_heap, (char*)end_heap - (char*)start_heap);
+ heap_bytes_used_ = mmalloc_get_bytes_used_remote(heap->heaplimit, memory.get_malloc_info());
}
/** @brief Checks whether the variable is in scope for a given IP.
}
static void fill_local_variables_values(mc_stack_frame_t stack_frame, Frame* scope,
- std::vector<s_local_variable_t>& result)
+ std::vector<s_local_variable_t>& result, AddressSpace* memory)
{
if (not scope || not scope->range.contain(stack_frame->ip))
return;
if (current_variable.address != nullptr)
new_var.address = current_variable.address;
else if (not current_variable.location_list.empty()) {
- dwarf::Location location = simgrid::dwarf::resolve(current_variable.location_list, current_variable.object_info,
- &(stack_frame->unw_cursor), (void*)stack_frame->frame_base,
- &mc_model_checker->get_remote_process_memory());
+ dwarf::Location location =
+ simgrid::dwarf::resolve(current_variable.location_list, current_variable.object_info,
+ &(stack_frame->unw_cursor), (void*)stack_frame->frame_base, memory);
xbt_assert(location.in_memory(), "Cannot handle non-address variable");
new_var.address = location.address();
// Recursive processing of nested scopes:
for (Frame& nested_scope : scope->scopes)
- fill_local_variables_values(stack_frame, &nested_scope, result);
+ fill_local_variables_values(stack_frame, &nested_scope, result, memory);
}
-static std::vector<s_local_variable_t> get_local_variables_values(std::vector<s_mc_stack_frame_t>& stack_frames)
+static std::vector<s_local_variable_t> get_local_variables_values(std::vector<s_mc_stack_frame_t>& stack_frames,
+ AddressSpace* memory)
{
std::vector<s_local_variable_t> variables;
for (s_mc_stack_frame_t& stack_frame : stack_frames)
- fill_local_variables_values(&stack_frame, stack_frame.frame, variables);
+ fill_local_variables_values(&stack_frame, stack_frame.frame, variables, memory);
return variables;
}
-static std::vector<s_mc_stack_frame_t> unwind_stack_frames(UnwindContext* stack_context)
+static std::vector<s_mc_stack_frame_t> unwind_stack_frames(UnwindContext* stack_context,
+ const RemoteProcessMemory* process_memory)
{
- const RemoteProcessMemory* process_memory = &mc_model_checker->get_remote_process_memory();
std::vector<s_mc_stack_frame_t> result;
unw_cursor_t c = stack_context->cursor();
st.context.initialize(process_memory, &context);
- st.stack_frames = unwind_stack_frames(&st.context);
- st.local_variables = get_local_variables_values(st.stack_frames);
+ st.stack_frames = unwind_stack_frames(&st.context, &process_memory);
+ st.local_variables = get_local_variables_values(st.stack_frames, &process_memory);
unw_word_t sp = st.stack_frames[0].sp;
ignore_restore();
}
-void Snapshot::add_region(RegionType type, ObjectInformation* object_info, void* start_addr, std::size_t size)
+void Snapshot::add_region(RegionType type, RemoteProcessMemory& memory, ObjectInformation* object_info,
+ void* start_addr, std::size_t size)
{
if (type == RegionType::Data)
xbt_assert(object_info, "Missing object info for object.");
else if (type == RegionType::Heap)
xbt_assert(not object_info, "Unexpected object info for heap region.");
- auto* region = new Region(page_store_, type, start_addr, size);
+ auto* region = new Region(page_store_, memory, type, start_addr, size);
region->object_info(object_info);
snapshot_regions_.push_back(std::unique_ptr<Region>(region));
}
// Restore regions
for (std::unique_ptr<Region> const& region : snapshot_regions_) {
- region->restore();
+ region->restore(memory);
}
ignore_restore();
#ifndef SIMGRID_MC_SNAPSHOT_HPP
#define SIMGRID_MC_SNAPSHOT_HPP
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/inspect/mc_unw.hpp"
#include "src/mc/sosp/Region.hpp"
#include "src/mc/sosp/RemoteProcessMemory.hpp"
Region* get_region(const void* addr, Region* hinted_region) const;
void restore(RemoteProcessMemory& memory) const;
- bool operator==(const Snapshot& other);
- bool operator!=(const Snapshot& other) { return not(*this == other); }
+ bool equals_to(const Snapshot& other, RemoteProcessMemory& memory);
// To be private
long num_state_;
std::vector<s_mc_snapshot_ignored_data_t> ignored_data_;
private:
- void add_region(RegionType type, ObjectInformation* object_info, void* start_addr, std::size_t size);
- void snapshot_regions(RemoteProcessMemory& process_memory);
- void snapshot_stacks(RemoteProcessMemory& process_memory);
+ void add_region(RegionType type, RemoteProcessMemory& memory, ObjectInformation* object_info, void* start_addr,
+ std::size_t size);
+ void snapshot_regions(RemoteProcessMemory& memory);
+ void snapshot_stacks(RemoteProcessMemory& memory);
void handle_ignore();
void ignore_restore() const;
hash_type do_hash() const;
using simgrid::mc::Region;
class snap_test_helper {
static simgrid::mc::PageStore page_store_;
+ static std::unique_ptr<simgrid::mc::RemoteProcessMemory> memory_;
public:
static void init_memory(void* mem, size_t size);
static void compare_region_parts();
static void read_pointer();
- static void cleanup()
- {
- delete mc_model_checker;
- mc_model_checker = nullptr;
- }
-
- static std::unique_ptr<simgrid::mc::RemoteProcessMemory> process;
+ static void cleanup() { memory_ = nullptr; }
};
// static member variables init.
-std::unique_ptr<simgrid::mc::RemoteProcessMemory> snap_test_helper::process = nullptr;
simgrid::mc::PageStore snap_test_helper::page_store_(500);
+std::unique_ptr<simgrid::mc::RemoteProcessMemory> snap_test_helper::memory_ = nullptr;
void snap_test_helper::init_memory(void* mem, size_t size)
{
REQUIRE(xbt_pagesize == getpagesize());
REQUIRE(1 << xbt_pagebits == xbt_pagesize);
- process = std::make_unique<simgrid::mc::RemoteProcessMemory>(getpid());
- process->init(nullptr);
- mc_model_checker = new ::simgrid::mc::ModelChecker(std::move(process));
+ memory_ = std::make_unique<simgrid::mc::RemoteProcessMemory>(getpid(), nullptr);
}
snap_test_helper::prologue_return snap_test_helper::prologue(int n)
// Init memory and take snapshots:
init_memory(source, byte_size);
- auto* region0 = new simgrid::mc::Region(page_store_, simgrid::mc::RegionType::Data, source, byte_size);
+ auto* region0 =
+ new simgrid::mc::Region(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, source, byte_size);
for (int i = 0; i < n; i += 2) {
init_memory((char*)source + i * xbt_pagesize, xbt_pagesize);
}
- auto* region = new simgrid::mc::Region(page_store_, simgrid::mc::RegionType::Data, source, byte_size);
+ auto* region = new simgrid::mc::Region(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, source, byte_size);
void* destination = mmap(nullptr, byte_size, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
INFO("Could not allocate destination memory");
}
}
+int some_global_variable = 42;
+void* some_global_pointer = &some_global_variable;
void snap_test_helper::read_pointer()
{
prologue_return ret = prologue(1);
- memcpy(ret.src, &mc_model_checker, sizeof(void*));
- const simgrid::mc::Region region2(page_store_, simgrid::mc::RegionType::Data, ret.src, ret.size);
+ memcpy(ret.src, &some_global_pointer, sizeof(void*));
+ const simgrid::mc::Region region2(page_store_, *memory_.get(), simgrid::mc::RegionType::Data, ret.src, ret.size);
INFO("Mismtach in MC_region_read_pointer()");
- REQUIRE(MC_region_read_pointer(®ion2, ret.src) == mc_model_checker);
+ REQUIRE(MC_region_read_pointer(®ion2, ret.src) == some_global_pointer);
munmap(ret.dstn, ret.size);
munmap(ret.src, ret.size);
#include <simgrid/config.h>
#if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/transition/TransitionActorJoin.hpp"
#include "src/mc/transition/TransitionAny.hpp"
return xbt::string_printf("label = \"[(%ld)] %s\", color = %s, fontcolor = %s", aid_, Transition::to_c_str(type_),
color, color);
}
-void Transition::replay() const
+void Transition::replay(RemoteApp& app) const
{
replayed_transitions_++;
#if SIMGRID_HAVE_MC
- mc_model_checker->get_exploration()->get_remote_app().handle_simcall(aid_, times_considered_, false);
- mc_model_checker->get_exploration()->get_remote_app().wait_for_requests();
+ app.handle_simcall(aid_, times_considered_, false);
+ app.wait_for_requests();
#endif
}
virtual std::string dot_string() const;
/* Moves the application toward a path that was already explored, but don't change the current transition */
- void replay() const;
+ void replay(RemoteApp& app) const;
virtual bool depends(const Transition* other) const { return true; }
#include "xbt/asserts.h"
#include "xbt/string.hpp"
#if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/api/State.hpp"
#endif
#include "xbt/asserts.h"
#include "xbt/string.hpp"
#if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/api/State.hpp"
#endif
#include "xbt/asserts.h"
#include "xbt/string.hpp"
#if SIMGRID_HAVE_MC
-#include "src/mc/ModelChecker.hpp"
#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/api/State.hpp"
#endif
int main()
{
- auto* process = new simgrid::mc::RemoteProcessMemory(getpid());
- process->init(nullptr);
+ auto* process = new simgrid::mc::RemoteProcessMemory(getpid(), nullptr);
simgrid::dwarf::ExpressionContext state;
state.address_space = (simgrid::mc::AddressSpace*) process;
const simgrid::mc::Variable* var;
simgrid::mc::Type* type;
- simgrid::mc::RemoteProcessMemory process(getpid());
- process.init(nullptr);
+ simgrid::mc::RemoteProcessMemory process(getpid(), nullptr);
test_global_variable(process, process.binary_info.get(), "some_local_variable", &some_local_variable, sizeof(int));
src/mc/transition/TransitionSynchro.cpp
src/mc/transition/TransitionSynchro.hpp
- src/mc/AddressSpace.hpp
- src/mc/ModelChecker.cpp
- src/mc/ModelChecker.hpp
- src/mc/VisitedState.cpp
- src/mc/VisitedState.hpp
+ src/mc/api/guide/BasicGuide.hpp
+ src/mc/api/guide/GuidedState.hpp
src/mc/api/ActorState.hpp
src/mc/api/State.cpp
src/mc/api/State.hpp
src/mc/api/RemoteApp.cpp
src/mc/api/RemoteApp.hpp
+
+ src/mc/AddressSpace.hpp
+ src/mc/VisitedState.cpp
+ src/mc/VisitedState.hpp
src/mc/compare.cpp
src/mc/mc_exit.hpp
src/mc/mc_forward.hpp
tools/cmake/Modules/FindNS3.cmake
tools/cmake/Modules/FindPAPI.cmake
tools/cmake/Modules/FindValgrind.cmake
+ tools/cmake/Modules/nlohmann_jsonConfig.cmake
tools/cmake/Modules/pybind11Config.cmake
tools/cmake/Option.cmake
tools/cmake/Tests.cmake
